Skip to content

N
NIWO
Commit 9601f1c5 authored by Christian Müller's avatar Christian Müller
Browse files
Options

assembly bin

parent 0c668bda
Hide whitespace changes
Inline Side-by-side
Showing with 107 additions and 149 deletions
build.sbt
View file @ 9601f1c5
name := "loopingWorkflows"
name := "niwo"
version := "0.1"
version := "0.9"
scalaVersion := "2.12.8"
......@@ -27,7 +27,18 @@ Compile / unmanagedJars ++= {
customJars.classpath
}
//assemblyJarName in assembly := "invariants.jar"
//test in assembly := {}
//mainClass in assembly := Some("de.tum.workflows.InvariantCLI")
// Exclude Z3 jar
assemblyExcludedJars in assembly := {
val cp = (fullClasspath in assembly).value
cp filter {_.data.getName == "com.microsoft.z3.jar"}
}
test in assembly := {}
assemblyJarName in assembly := "niwo-ts.jar"
mainClass in assembly := Some("de.tum.niwo.TSCLI")
//test in assembly := {}
//assemblyJarName in assembly := "niwo-wf.jar"
//mainClass in assembly := Some("de.tum.niwo.WFCLI")
logback.xml 0 → 100644
View file @ 9601f1c5
<configuration>
<appender name="STDOUT" class="ch.qos.logback.core.ConsoleAppender">
<!-- encoders are assigned the type
ch.qos.logback.classic.encoder.PatternLayoutEncoder by default -->
<encoder>
<pattern>%d{HH:mm:ss.SSS} [%thread] %-5level %logger{36} - %msg%n</pattern>
</encoder>
</appender>
<root level="info">
<appender-ref ref="STDOUT" />
</root>
</configuration>
project/plugins.sbt
View file @ 9601f1c5
addSbtPlugin("com.github.xuwei-k" % "sbt-class-diagram" % "0.2.1")
addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "0.14.10")
results/tests/conference_linear_small_withB/conference_linear_small_withB_causal__elim.strategies 0 → 100644
View file @ 9601f1c5
Strategies:
strategy for B(x1,p1): False
\ No newline at end of file
results/tests/conference_stubborn_withB/conference_stubborn_withB_causal__elim.strategies 0 → 100644
View file @ 9601f1c5
Strategies:
strategy for B(x1,p1): ¬ Conf(x1,p1) ∧ ∀ xat:A. ¬ Conf(xat,p1)
\ No newline at end of file
results/tests/leaderelection_withB/leaderelection_withB_stubborn.strategies 0 → 100644
View file @ 9601f1c5
Strategies:
strategy for B(a1,b1,i1): ∀ n2:T. ((b1 = n2) ∨ ¬ Ile(b1,n2) ∨ ¬ Inext(a1,b1) ∨ ¬ (b1 = i1)) ∧ ∀ n3:T. (¬ Ibtw(b1,i1,n3) ∨ ¬ Ile(i1,n3) ∨ ¬ Inext(a1,b1))
\ No newline at end of file
results/tstests/easychair_singletrace/easychair_singletrace_stubborn.strategies 0 → 100644
View file @ 9601f1c5
Strategies:
strategy for B1(x1,p1): (∀ y:A. Conf(y,p1) ∨ ¬ Conf(x1,p1)) ∧ (Conf(x1,p1) ∨ ∀ x:A. ¬ Conf(x,p1)) ∧ (∀ y1:A. Conf(y1,p1) ∨ ¬ Conf(x1,p1))
\ No newline at end of file
results/tstests/leaderelection_inductive_withB/leaderelection_inductive_withB_stubborn.strategies 0 → 100644
View file @ 9601f1c5
Strategies:
strategy for B(a1,b1,i1): ∀ n2:T. ((b1 = n2) ∨ ¬ leq(b1,n2) ∨ ¬ next(a1,b1) ∨ ¬ (b1 = i1)) ∧ ∀ n3:T. (¬ btw(b1,i1,n3) ∨ ¬ leq(i1,n3) ∨ ¬ next(a1,b1))
\ No newline at end of file
src/main/java/BrokenDowncastMWE.java deleted 100644 → 0
View file @ 0c668bda
import com.microsoft.z3.Context;
import com.microsoft.z3.Quantifier;
import com.microsoft.z3.Sort;
import com.microsoft.z3.Symbol;
import java.util.HashMap;
public class BrokenDowncastMWE {
public static void main(String[] args) {
var cfg = new HashMap<String, String>();
var ctx = new Context(cfg);
var simp = ctx.mkTactic("tseitin-cnf");
var goal = ctx.mkGoal(false, false, false);
var names = new Symbol[1];
names[0] = ctx.mkSymbol("x");
var sorts = new Sort[1];
sorts[0] = ctx.mkUninterpretedSort("T");
var fundecl = ctx.mkFuncDecl("fun", sorts, ctx.getBoolSort());
var boundvar = ctx.mkBound(0, sorts[0]);
var application = fundecl.apply(boundvar);
var expr = ctx.mkForall(sorts, names, application, 0, null, null, null, null);
goal.add(expr);
var ar = simp.apply(goal);
var sub = ar.getSubgoals();
var resultexpr = sub[0].AsBoolExpr();
System.out.println(expr);
System.out.println(expr.isQuantifier());
System.out.println(expr.getClass().getName());
System.out.println(resultexpr);
System.out.println(resultexpr.isQuantifier());
System.out.println(resultexpr.getClass().getName());
((Quantifier) resultexpr).getBody();
}
}
src/main/java/Test.java deleted 100644 → 0
View file @ 0c668bda
import owl.ltl.BooleanConstant;
import owl.ltl.algorithms.LanguageAnalysis;
import java.io.FileDescriptor;
import java.io.FileOutputStream;
import java.io.PrintStream;
class Test {
public static void main(String[] args) {
System.out.println("Test");
BooleanConstant owlform = BooleanConstant.FALSE;
boolean checksat = LanguageAnalysis.isSatisfiable(owlform);
System.out.println(checksat);
}
}
\ No newline at end of file
src/main/scala/de/tum/niwo/InvariantCLI.scala deleted 100644 → 0
View file @ 0c668bda
package de.tum.niwo
import scala.io.Source
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Utils._
import de.tum.niwo.blocks.NISpec
import de.tum.niwo.invariants.InvariantChecker
import java.io.File
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
import de.tum.niwo.parser.WorkflowParser
object InvariantCLI extends App with LazyLogging {
lazy val usage = """
Usage invariants.jar [--causal] [--elimChoice] FILE
FILE should be a path to a Workflow Description File.
If --causal is given, all agents are assumed to be causal, otherwise all agents are assumed to be stubborn.
If --elimChoice is given, all choice predicates are immediately eliminated, while otherwise they will be eliminated after termination of the fixpoint algorithm. (may affect performance)
With elimChoice turned off, that corresponds to choice predicates not changing over time.
"""
if (args.length == 0) {
logger.info(usage)
} else {
var causal = false
var elim = false
args.collect {
case "--causal" => causal = true
case "--elimChoice" => elim = true
}
val properties = InvProperties(!causal, elim)
val file = args.last
logger.info(s"Using $file")
val source = Source.fromFile(file).mkString
val spec = WorkflowParser.parseSpec(source)
if (!spec.successful) {
logger.error(s"Parsing of $file unsuccessful: $spec")
None
} else {
if (!spec.get.isSane()) {
logger.error(s"Sanity check of $file failed. Skipping file.")
None
} else {
Some(spec.get)
}
}
spec.map(generate(new File(file).getName.stripSuffix(".spec"), _, properties))
}
def generate(name: String, spec: NISpec, properties: InvProperties) {
logger.info(s"Encoding Spec:\n$spec")
def invariant = InvariantGenerator.invariantNoninterSingleBS _
Utils.check(name, "", invariant, spec, properties)
}
}
\ No newline at end of file
src/main/scala/de/tum/niwo/WFCLI.scala
View file @ 9601f1c5
......@@ -2,48 +2,64 @@ package de.tum.niwo
import scala.io.Source
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Utils._
import de.tum.niwo.blocks.NISpec
import de.tum.niwo.invariants.InvariantChecker
import java.io.File
import de.tum.niwo.LTLCLI.args
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
import de.tum.niwo.parser.WorkflowParser
object TSCLI extends App with LazyLogging {
object WFCLI extends App with LazyLogging {
lazy val usage = """
Usage niwo-ts.jar FILE
Usage niwo-wf.jar [--stubborn] [--elimChoice] FILE
FILE should be a path to a Workflow Description File.
It will be transformed into a First Order Safety Game and then solved.
If --stubborn is given, all agents are assumed to be stubborn, regardless of the specification in the file.
If --stubborn is given, all agents are assumed to be stubborn ignoring the model given in the specification file.
If --elimChoice is given, all choice predicates are immediately eliminated, while otherwise they will be eliminated after termination of the fixpoint algorithm. (may affect performance)
With elimChoice turned off, that corresponds to choice predicates not changing over time.
"""
if (args.length == 0) {
logger.info(usage)
} else {
var stubborn = false
var causal = true
var elim = false
args.collect {
case "--stubborn" => stubborn = true
case "--stubborn" => causal = false
case "--elimChoice" => elim = true
}
val properties = InvProperties(!causal, elim)
val file = args.last
logger.info(s"Using $file")
val source = Utils.using(Source.fromFile(file)) { source => source.mkString }
val spec = WorkflowParser.parseSpec(source)
if (!spec.successful) {
logger.error(s"Parsing of $file unsuccessful: $spec")
None
} else {
if (!spec.get.isSane) {
if (!spec.get.isSane()) {
logger.error(s"Sanity check of $file failed. Skipping file.")
None
} else {
val inv = InvariantGenerator.invariantNoninterSingleBS _
val properties = InvProperties(stubborn = stubborn, approxElim = true, eliminateA = true, eliminateB = true)
Utils.check(new File(file).getName.stripSuffix(".spec"), "", inv, spec.get, properties)
Some(spec.get)
}
}
spec.map(generate(new File(file).getName.stripSuffix(".spec"), _, properties))
}
}
def generate(name: String, spec: NISpec, properties: InvProperties) {
logger.info(s"Encoding Spec:\n$spec")
def invariant = InvariantGenerator.invariantNoninterSingleBS _
Utils.check(name, "", invariant, spec, properties)
}
}
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment