Commit 663f1e49 authored by Christian Müller's avatar Christian Müller

newer sbt

parent 6dbc2d68
No preview for this file type
G ((n0() → X n1()) ∧
(n1() → X n1())) ∧
n0() ∧
¬ n1() ∧
G ¬ (n0() ∧
n1()) ∧
∀ x:T,s:T. ¬ R(t1)(x,s) ∧
G (((n0() ∧
X n1()) → ∀ x:T,s:T. (X R(t1)(x,s) ↔ (R(t1)(x,s) ∨
(O(t1)(s) ∧
choice0(x,s))))) ∧
((n1() ∧
X n1()) → ∀ x:T,s:T. (X R(t1)(x,s) ↔ R(t1)(x,s)))) ∧
∀ x:T,s:T. ¬ R(t2)(x,s) ∧
G (((n0() ∧
X n1()) → ∀ x:T,s:T. (X R(t2)(x,s) ↔ (R(t2)(x,s) ∨
(O(t2)(s) ∧
choice0(x,s))))) ∧
((n1() ∧
X n1()) → ∀ x:T,s:T. (X R(t2)(x,s) ↔ R(t2)(x,s)))) ∧
∃ x:T,s:T. (True ∧
F ¬ (R(t1)(x,s) ↔ eq()))
\ No newline at end of file
G ((n0 → X n1) ∧ (n1 → X n1)) ∧ n0 ∧ ¬ n1 ∧ G ¬ (n0 ∧ n1) ∧ ¬ R#t1_x#T_x#T ∧ ¬ R#t1_x#T_s#T ∧ ¬ R#t1_s#T_x#T ∧ ¬ R#t1_s#T_s#T ∧ G (((n0 ∧ X n1) → ((X R#t1_x#T_x#T ↔ (R#t1_x#T_x#T ∨ (O#t1_x#T ∧ choice0_x#T_x#T))) ∧ (X R#t1_x#T_s#T ↔ (R#t1_x#T_s#T ∨ (O#t1_s#T ∧ choice0_x#T_s#T))) ∧ (X R#t1_s#T_x#T ↔ (R#t1_s#T_x#T ∨ (O#t1_x#T ∧ choice0_s#T_x#T))) ∧ (X R#t1_s#T_s#T ↔ (R#t1_s#T_s#T ∨ (O#t1_s#T ∧ choice0_s#T_s#T))))) ∧ ((n1 ∧ X n1) → ((X R#t1_x#T_x#T ↔ R#t1_x#T_x#T) ∧ (X R#t1_x#T_s#T ↔ R#t1_x#T_s#T) ∧ (X R#t1_s#T_x#T ↔ R#t1_s#T_x#T) ∧ (X R#t1_s#T_s#T ↔ R#t1_s#T_s#T)))) ∧ ¬ R#t2_x#T_x#T ∧ ¬ R#t2_x#T_s#T ∧ ¬ R#t2_s#T_x#T ∧ ¬ R#t2_s#T_s#T ∧ G (((n0 ∧ X n1) → ((X R#t2_x#T_x#T ↔ (R#t2_x#T_x#T ∨ (O#t2_x#T ∧ choice0_x#T_x#T))) ∧ (X R#t2_x#T_s#T ↔ (R#t2_x#T_s#T ∨ (O#t2_s#T ∧ choice0_x#T_s#T))) ∧ (X R#t2_s#T_x#T ↔ (R#t2_s#T_x#T ∨ (O#t2_x#T ∧ choice0_s#T_x#T))) ∧ (X R#t2_s#T_s#T ↔ (R#t2_s#T_s#T ∨ (O#t2_s#T ∧ choice0_s#T_s#T))))) ∧ ((n1 ∧ X n1) → ((X R#t2_x#T_x#T ↔ R#t2_x#T_x#T) ∧ (X R#t2_x#T_s#T ↔ R#t2_x#T_s#T) ∧ (X R#t2_s#T_x#T ↔ R#t2_s#T_x#T) ∧ (X R#t2_s#T_s#T ↔ R#t2_s#T_s#T)))) ∧ True ∧ F ¬ (R#t1_x#T_s#T ↔ R#t2_x#T_s#T)
\ No newline at end of file
simplechoice_stubborn.foltl: 92
simplechoice_stubborn.ltl: 187
Universe: x:T, s:T
Satisfiable: true
Owl runtime: 156107 ms
(G(X!p4|!p9|((((!p1|!p11)&!p8&X!p8)|(Xp8&(p8|(p1&p11))))&((!p3&X!p3&(!p2|!p11))|((p3|(p2&p11))&Xp3))&(((p15|(p6&p14))&Xp15)|(!p15&X!p15&(!p6|!p14)))&((X!p17&!p17&(!p5|!p14))|(Xp17&(p17|(p5&p14))))))&G(X!p4|!p9|(((X!p0&(!p1|!p10)&!p0)|(Xp0&(p0|(p1&p10))))&(((!p2|!p10)&!p13&X!p13)|(Xp13&((p2&p10)|p13)))&(((p16|(p6&p7))&Xp16)|((!p6|!p7)&X!p16&!p16))&(((!p5|!p7)&X!p12&!p12)|(Xp12&(p12|(p5&p7))))))&!p17&!p16&G(!p4|!p9)&p9&!p8&!p15&!p13&!p12&!p3&!p0&G(!p4|Xp4)&G(X!p4|!p4|(((X!p8&!p8)|(Xp8&p8))&((!p17&X!p17)|(p17&Xp17))&((p3&Xp3)|(!p3&X!p3))&((p15&Xp15)|(X!p15&!p15))))&!p4&F((!p17|!p12)&(p17|p12))&G(X!p4|!p4|(((!p0&X!p0)|(p0&Xp0))&((Xp12&p12)|(X!p12&!p12))&((Xp13&p13)|(X!p13&!p13))&((!p16&X!p16)|(p16&Xp16))))&G(!p9|Xp4))
\ No newline at end of file
G ((n0 → X n1) ∧
(n1 → X n1)) ∧
n0 ∧
¬ n1 ∧
G ¬ (n0 ∧
n1) ∧
¬ R#t1_x#T_x#T ∧
¬ R#t1_x#T_s#T ∧
¬ R#t1_s#T_x#T ∧
¬ R#t1_s#T_s#T ∧
G (((n0 ∧
X n1) → ((X R#t1_x#T_x#T ↔ (R#t1_x#T_x#T ∨
(O#t1_x#T ∧
choice0_x#T_x#T))) ∧
(X R#t1_x#T_s#T ↔ (R#t1_x#T_s#T ∨
(O#t1_s#T ∧
choice0_x#T_s#T))) ∧
(X R#t1_s#T_x#T ↔ (R#t1_s#T_x#T ∨
(O#t1_x#T ∧
choice0_s#T_x#T))) ∧
(X R#t1_s#T_s#T ↔ (R#t1_s#T_s#T ∨
(O#t1_s#T ∧
choice0_s#T_s#T))))) ∧
((n1 ∧
X n1) → ((X R#t1_x#T_x#T ↔ R#t1_x#T_x#T) ∧
(X R#t1_x#T_s#T ↔ R#t1_x#T_s#T) ∧
(X R#t1_s#T_x#T ↔ R#t1_s#T_x#T) ∧
(X R#t1_s#T_s#T ↔ R#t1_s#T_s#T)))) ∧
¬ R#t2_x#T_x#T ∧
¬ R#t2_x#T_s#T ∧
¬ R#t2_s#T_x#T ∧
¬ R#t2_s#T_s#T ∧
G (((n0 ∧
X n1) → ((X R#t2_x#T_x#T ↔ (R#t2_x#T_x#T ∨
(O#t2_x#T ∧
choice0_x#T_x#T))) ∧
(X R#t2_x#T_s#T ↔ (R#t2_x#T_s#T ∨
(O#t2_s#T ∧
choice0_x#T_s#T))) ∧
(X R#t2_s#T_x#T ↔ (R#t2_s#T_x#T ∨
(O#t2_x#T ∧
choice0_s#T_x#T))) ∧
(X R#t2_s#T_s#T ↔ (R#t2_s#T_s#T ∨
(O#t2_s#T ∧
choice0_s#T_s#T))))) ∧
((n1 ∧
X n1) → ((X R#t2_x#T_x#T ↔ R#t2_x#T_x#T) ∧
(X R#t2_x#T_s#T ↔ R#t2_x#T_s#T) ∧
(X R#t2_s#T_x#T ↔ R#t2_s#T_x#T) ∧
(X R#t2_s#T_s#T ↔ R#t2_s#T_s#T)))) ∧
True ∧
F ¬ (R#t1_x#T_s#T ↔ R#t2_x#T_s#T)
\ No newline at end of file
G ((n0() → X n1()) ∧
(n1() → X n1())) ∧
n0() ∧
¬ n1() ∧
G ¬ (n0() ∧
n1()) ∧
∀ x:T,s:T. ¬ R(t1)(x,s) ∧
G (((n0() ∧
X n1()) → ∀ x:T,s:T. (X R(t1)(x,s) ↔ (R(t1)(x,s) ∨
(O(t1)(s) ∧
choice0(x,s))))) ∧
((n1() ∧
X n1()) → ∀ x:T,s:T. (X R(t1)(x,s) ↔ R(t1)(x,s)))) ∧
∀ x:T,s:T. ¬ R(t2)(x,s) ∧
G (((n0() ∧
X n1()) → ∀ x:T,s:T. (X R(t2)(x,s) ↔ (R(t2)(x,s) ∨
(O(t2)(s) ∧
choice0(x,s))))) ∧
((n1() ∧
X n1()) → ∀ x:T,s:T. (X R(t2)(x,s) ↔ R(t2)(x,s)))) ∧
∃ x:T,s:T. (True ∧
F ¬ (R(t1)(x,s) ↔ eq()))
\ No newline at end of file
G ((n0 → X n1) ∧ (n1 → X n1)) ∧ n0 ∧ ¬ n1 ∧ G ¬ (n0 ∧ n1) ∧ ¬ R#t1_x#T_x#T ∧ ¬ R#t1_x#T_s#T ∧ ¬ R#t1_s#T_x#T ∧ ¬ R#t1_s#T_s#T ∧ G (((n0 ∧ X n1) → ((X R#t1_x#T_x#T ↔ (R#t1_x#T_x#T ∨ (O#t1_x#T ∧ choice0_x#T_x#T))) ∧ (X R#t1_x#T_s#T ↔ (R#t1_x#T_s#T ∨ (O#t1_s#T ∧ choice0_x#T_s#T))) ∧ (X R#t1_s#T_x#T ↔ (R#t1_s#T_x#T ∨ (O#t1_x#T ∧ choice0_s#T_x#T))) ∧ (X R#t1_s#T_s#T ↔ (R#t1_s#T_s#T ∨ (O#t1_s#T ∧ choice0_s#T_s#T))))) ∧ ((n1 ∧ X n1) → ((X R#t1_x#T_x#T ↔ R#t1_x#T_x#T) ∧ (X R#t1_x#T_s#T ↔ R#t1_x#T_s#T) ∧ (X R#t1_s#T_x#T ↔ R#t1_s#T_x#T) ∧ (X R#t1_s#T_s#T ↔ R#t1_s#T_s#T)))) ∧ ¬ R#t2_x#T_x#T ∧ ¬ R#t2_x#T_s#T ∧ ¬ R#t2_s#T_x#T ∧ ¬ R#t2_s#T_s#T ∧ G (((n0 ∧ X n1) → ((X R#t2_x#T_x#T ↔ (R#t2_x#T_x#T ∨ (O#t2_x#T ∧ choice0_x#T_x#T))) ∧ (X R#t2_x#T_s#T ↔ (R#t2_x#T_s#T ∨ (O#t2_s#T ∧ choice0_x#T_s#T))) ∧ (X R#t2_s#T_x#T ↔ (R#t2_s#T_x#T ∨ (O#t2_x#T ∧ choice0_s#T_x#T))) ∧ (X R#t2_s#T_s#T ↔ (R#t2_s#T_s#T ∨ (O#t2_s#T ∧ choice0_s#T_s#T))))) ∧ ((n1 ∧ X n1) → ((X R#t2_x#T_x#T ↔ R#t2_x#T_x#T) ∧ (X R#t2_x#T_s#T ↔ R#t2_x#T_s#T) ∧ (X R#t2_s#T_x#T ↔ R#t2_s#T_x#T) ∧ (X R#t2_s#T_s#T ↔ R#t2_s#T_s#T)))) ∧ True ∧ F ¬ (R#t1_x#T_s#T ↔ R#t2_x#T_s#T)
\ No newline at end of file
simplechoice_stubborn.foltl: 92
simplechoice_stubborn.ltl: 187
Universe: x:T, s:T
Satisfiable: true
Owl runtime: 90339 ms
(G(!p4|Xp4)&G(!p9|Xp4)&F((p17|p12)&(!p17|!p12))&G((((!p17&X!p17)|(p17&Xp17))&((p3&Xp3)|(!p3&X!p3))&((Xp8&p8)|(X!p8&!p8))&((p15&Xp15)|(X!p15&!p15)))|X!p4|!p4)&G(!p4|!p9)&G((((Xp12&p12)|(X!p12&!p12))&((Xp13&p13)|(X!p13&!p13))&((p0&Xp0)|(!p0&X!p0))&((p16&Xp16)|(!p16&X!p16)))|X!p4|!p4)&!p16&p9&!p17&!p8&G(X!p4|((((p0|(p1&p10))&Xp0)|(!p0&(!p1|!p10)&X!p0))&(((!p2|!p10)&X!p13&!p13)|((p13|(p2&p10))&Xp13))&(((p16|(p6&p7))&Xp16)|((!p6|!p7)&!p16&X!p16))&(((!p5|!p7)&X!p12&!p12)|((p12|(p5&p7))&Xp12)))|!p9)&G(X!p4|(((Xp8&(p8|(p1&p11)))|((!p1|!p11)&X!p8&!p8))&(((p3|(p2&p11))&Xp3)|((!p2|!p11)&X!p3&!p3))&((Xp15&(p15|(p6&p14)))|(!p15&X!p15&(!p6|!p14)))&((X!p17&(!p5|!p14)&!p17)|(Xp17&(p17|(p5&p14)))))|!p9)&!p15&!p12&!p13&!p3&!p0&!p4)
\ No newline at end of file
G ((n0 → X n1) ∧
(n1 → X n1)) ∧
n0 ∧
¬ n1 ∧
G ¬ (n0 ∧
n1) ∧
¬ R#t1_x#T_x#T ∧
¬ R#t1_x#T_s#T ∧
¬ R#t1_s#T_x#T ∧
¬ R#t1_s#T_s#T ∧
G (((n0 ∧
X n1) → ((X R#t1_x#T_x#T ↔ (R#t1_x#T_x#T ∨
(O#t1_x#T ∧
choice0_x#T_x#T))) ∧
(X R#t1_x#T_s#T ↔ (R#t1_x#T_s#T ∨
(O#t1_s#T ∧
choice0_x#T_s#T))) ∧
(X R#t1_s#T_x#T ↔ (R#t1_s#T_x#T ∨
(O#t1_x#T ∧
choice0_s#T_x#T))) ∧
(X R#t1_s#T_s#T ↔ (R#t1_s#T_s#T ∨
(O#t1_s#T ∧
choice0_s#T_s#T))))) ∧
((n1 ∧
X n1) → ((X R#t1_x#T_x#T ↔ R#t1_x#T_x#T) ∧
(X R#t1_x#T_s#T ↔ R#t1_x#T_s#T) ∧
(X R#t1_s#T_x#T ↔ R#t1_s#T_x#T) ∧
(X R#t1_s#T_s#T ↔ R#t1_s#T_s#T)))) ∧
¬ R#t2_x#T_x#T ∧
¬ R#t2_x#T_s#T ∧
¬ R#t2_s#T_x#T ∧
¬ R#t2_s#T_s#T ∧
G (((n0 ∧
X n1) → ((X R#t2_x#T_x#T ↔ (R#t2_x#T_x#T ∨
(O#t2_x#T ∧
choice0_x#T_x#T))) ∧
(X R#t2_x#T_s#T ↔ (R#t2_x#T_s#T ∨
(O#t2_s#T ∧
choice0_x#T_s#T))) ∧
(X R#t2_s#T_x#T ↔ (R#t2_s#T_x#T ∨
(O#t2_x#T ∧
choice0_s#T_x#T))) ∧
(X R#t2_s#T_s#T ↔ (R#t2_s#T_s#T ∨
(O#t2_s#T ∧
choice0_s#T_s#T))))) ∧
((n1 ∧
X n1) → ((X R#t2_x#T_x#T ↔ R#t2_x#T_x#T) ∧
(X R#t2_x#T_s#T ↔ R#t2_x#T_s#T) ∧
(X R#t2_s#T_x#T ↔ R#t2_s#T_x#T) ∧
(X R#t2_s#T_s#T ↔ R#t2_s#T_s#T)))) ∧
True ∧
F ¬ (R#t1_x#T_s#T ↔ R#t2_x#T_s#T)
\ No newline at end of file
......@@ -16,6 +16,13 @@ libraryDependencies ++= Seq(
"org.scala-lang.modules" %% "scala-parser-combinators" % "1.0.5"
)
assemblyJarName in assembly := "invariants.jar"
test in assembly := {}
mainClass in assembly := Some("de.tum.workflows.InvariantCLI")
Compile / unmanagedJars ++= {
val base = baseDirectory.value
val baseDirectories = (base / "lib") +++ (base / "lib" / "owl")
val customJars = (baseDirectories ** "*.jar") +++ (base / "d" / "my.jar")
customJars.classpath
}
//assemblyJarName in assembly := "invariants.jar"
//test in assembly := {}
//mainClass in assembly := Some("de.tum.workflows.InvariantCLI")
addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "0.14.6")
// addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "0.14.6")
sbt.version=0.13.15
sbt.version=1.1.2
addSbtPlugin("com.artima.supersafe" % "sbtplugin" % "1.1.2")
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");
var owlform = BooleanConstant.FALSE;
var checksat = LanguageAnalysis.isSatisfiable(owlform);
System.out.println(checksat);
}
}
\ No newline at end of file
......@@ -75,7 +75,8 @@ object Encoding extends LazyLogging {
def toGraph(w: Workflow): WorkflowGraph = {
var n1 = 0;
var n1 = 0
def newnode() = {
n1 = n1 + 1
n1
......@@ -92,7 +93,7 @@ object Encoding extends LazyLogging {
makeblock(step, n1, newnode(), newnode, makeid)
}
}).flatten
var nodes = (0 until n1).toList
val nodes = (0 until n1).toList
Graph.from(nodes, edges)
}
......
......@@ -48,29 +48,29 @@ object ExampleWorkflows extends LazyLogging {
}
def parsedExamples(prefix:String, folder:File):Map[String, Spec] = {
val map = (for ((name, f) <- examples) yield {
val map = for ((name, f) <- examples) yield {
val s = Source.fromFile(f).mkString
val spec = WorkflowParser.parseSpec(s)
logger.info(s"Parsing file $f")
if (!spec.successful) {
logger.error(s"Parsing of $f unsuccessful: $spec")
name -> None
logger.error(s"Parsing of $f unsuccessful: $spec")
name -> None
} else {
if (!spec.get.checkSanity()) {
logger.error(s"Sanity check of $f failed. Skipping file.")
name -> None
name -> None
} else {
name -> Some(spec.get)
name -> Some(spec.get)
}
}
}) toMap
}
// filter out all empty specs and those that are not sane
(for ((k, v) <- map if (v.isDefined)) yield {
for ((k, v) <- map if (v.isDefined)) yield {
(k, v.get)
}) toMap
}
}
val examples = listExamples("", FOLDER)
......
......@@ -33,9 +33,9 @@ object MainInvariants extends App with LazyLogging {
}
val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"
write(s"${name}.inv", msg)
write(s"$name.inv", msg)
for ((s, i) <- dot.zipWithIndex) {
write(s"${name}_${i}.dot", s)
write(s"${name}_$i.dot", s)
}
}
......@@ -43,11 +43,11 @@ object MainInvariants extends App with LazyLogging {
logger.info(s"Generating $name")
val spec = ExampleWorkflows.parseExample(name)
if (!spec.isDefined) {
if (spec.isEmpty) {
logger.error(s"Not a valid spec: $name")
}
spec.map(generate(name, _))
spec.foreach(generate(name, _))
}
def generateAllExamples() {
......
......@@ -20,8 +20,8 @@ object MainLTL extends App with LazyLogging {
var metrics = List[String]()
write(s"${name}.foltl", prop.pretty())
metrics :+= s"${name}.foltl: ${prop.opsize()}"
write(s"$name.foltl", prop.pretty())
metrics :+= s"$name.foltl: ${prop.opsize()}"
if (!FormulaFunctions.checkSanity(prop)) {
logger.error("Property didn't pass sanity check")
......@@ -41,19 +41,19 @@ object MainLTL extends App with LazyLogging {
val quantfree = FOTransformers.eliminateUniversals(res, agents)
val ltlprop = FOTransformers.eliminatePredicates(quantfree)
metrics :+= s"${name}.ltl: ${ltlprop.opsize()}"
metrics :+= s"$name.ltl: ${ltlprop.opsize()}"
metrics :+= s"Universe: $universe"
write(s"${name}.ltl", ltlprop.toString())
write(s"${name}.ppltl", ltlprop.pretty())
write(s"$name.ltl", ltlprop.toString())
write(s"$name.ppltl", ltlprop.pretty())
val owlform = OwlTransformer.toOwl(ltlprop)
val (t, sat) = time {
// simplify owl
val simped = SimplifierFactory.applyDefault(owlform.formula())
write(s"${name}.owlltl", simped.toString)
val simped = SimplifierFactory.applyDefault(owlform.formula()).nnf()
write(s"$name.owlltl", simped.toString)
logger.info("Simplified owl formula")
// check owl sat
logger.info("Checking satisfiability")
......@@ -65,7 +65,7 @@ object MainLTL extends App with LazyLogging {
metrics :+= s"Satisfiable: $sat"
metrics :+= s"Owl runtime: $t ms"
write(s"${name}.metrics", metrics.mkString("", "\n", "\n"))
write(s"$name.metrics", metrics.mkString("", "\n", "\n"))
}
def generate(name: String, spec: Spec, onlystubborn:Boolean) {
......@@ -92,7 +92,7 @@ object MainLTL extends App with LazyLogging {
logger.info(s"Generating $name")
val spec = ExampleWorkflows.parseExample(name)
if (!spec.isDefined) {
if (spec.isEmpty) {
logger.error(s"Not a valid spec: $name")
}
......@@ -110,7 +110,7 @@ object MainLTL extends App with LazyLogging {
// clear()
// generateExample("nonomitting/conference")
// generateExample("tests/declasstest")
generateExample("tests/simpleChoice")
// generateExample("tests/simpleChoiceNoOracle")
// generateExample("tests/simpleChoice")
generateExample("tests/simpleChoiceNoOracle")
// generateAllExamples()
}
\ No newline at end of file
......@@ -18,7 +18,7 @@ object Utils extends LazyLogging {
def collectChoices(w: Block): List[Fun] = {
w match {
case Loop(steps) => steps.flatMap(collectChoices _)
case Loop(steps) => steps.flatMap(collectChoices)
case ForallMayBlock(agents, pred, _) => List(Fun(pred, agents))
case b: ForallBlock => List()
case NondetChoice(l, r) => l.flatMap(collectChoices) ++ r.flatMap(collectChoices)
......@@ -26,7 +26,7 @@ object Utils extends LazyLogging {
}
def allchoices(w: Workflow) = {
w.steps flatMap (collectChoices _) toSet
w.steps flatMap collectChoices toSet
}
def indentLines(s: String) = {
......@@ -67,13 +67,13 @@ object Utils extends LazyLogging {
def check(name:String, desc:String, inv:Formula, spec:Spec, properties:InvProperties) = {
val model = if (properties.stubborn) "stubborn" else "causal"
val filenames = s"${name}_${model}${if (desc.isEmpty()) "" else s"_$desc"}"
val filenames = s"${name}_$model${if (desc.isEmpty()) "" else s"_$desc"}"
// do not blow up the formula with auxilliary elimination
val (res, graph, labelling, provens, dot, time) =
InvariantChecker.checkInvariantFPLabelling(spec, inv, properties)
for ((s, i) <- dot.zipWithIndex) {
Utils.write(s"${filenames}_${i}.dot", s)
Utils.write(s"${filenames}_$i.dot", s)
}
val strengthenings = for (List(a, b) <- labelling.sliding(2) if (a != b)) yield {
true
......@@ -89,7 +89,7 @@ object Utils extends LazyLogging {
val invsizes = labelling.last.map(_._2.opsize())
val maxsize = invsizes.max
val avgsize = invsizes.sum / invsizes.size
Utils.write(s"${filenames}.metrics",
Utils.write(s"$filenames.metrics",
s"""Name: $name
Description: $desc
Invariant: $inv
......@@ -99,8 +99,8 @@ object Utils extends LazyLogging {
Time: $time ms
Proof steps: ${dot.size}
Strengthenings: ${strengthenings.size}
Largest Inv: ${maxsize}
Average Inv: ${avgsize}""")
Largest Inv: $maxsize
Average Inv: $avgsize""")
res
}
......
......@@ -40,8 +40,8 @@ object WorkflowParser extends RegexParsers with LazyLogging {
def predicates(b: Block): Set[Fun] = {
b match {
case Loop(blocks) => blocks flatMap(predicates _) toSet
case b:SimpleBlock => b.steps.flatMap(predicatesStmt _) toSet
case Loop(blocks) => blocks flatMap predicates toSet
case b:SimpleBlock => b.steps.flatMap(predicatesStmt) toSet
case NondetChoice(l,r) => (l.flatMap(predicates) ++ r.flatMap(predicates)) toSet
}
}
......@@ -110,7 +110,7 @@ object WorkflowParser extends RegexParsers with LazyLogging {
// all variable names contained in bound
val names = bound.map(_.name)
val unbound = stmts.flatMap(_.freeVars()).filterNot(v => names.contains(v.name))
if (!unbound.isEmpty) {
if (unbound.nonEmpty) {
logger.error(s"Variables $unbound appear unbound.")
}
distinct && unbound.isEmpty
......@@ -123,13 +123,13 @@ object WorkflowParser extends RegexParsers with LazyLogging {
// logics
def tt = "True" ^^^ True
def ff = "False" ^^^ False
def AND = "(" ~> (repsep(TERM, "∧") | repsep(TERM, "&&")) <~ ")" ^^ { case ts => And.make(ts) }
def OR = "(" ~> (repsep(TERM, "∨") | repsep(TERM, "||")) <~ ")" ^^ { case ts => Or.make(ts) }
def AND = "(" ~> (repsep(TERM, "∧") | repsep(TERM, "&&")) <~ ")" ^^ (ts => And.make(ts))
def OR = "(" ~> (repsep(TERM, "∨") | repsep(TERM, "||")) <~ ")" ^^ (ts => Or.make(ts))
def NEG = ("¬" | "!") ~ SIMPLETERM ^^ { case _ ~ t => Neg(t) }
// temporals
def GLOBALLY = ("G" | "☐") ~> TERM ^^ { case t => Globally(t) }
def FINALLY = ("F" | "♢") ~> TERM ^^ { case t => Finally(t) }
def GLOBALLY = ("G" | "☐") ~> TERM ^^ (t => Globally(t))
def FINALLY = ("F" | "♢") ~> TERM ^^ (t => Finally(t))
def TUPLE = "(" ~> repsep(TYPEDVAR, ",") <~ ")"
def FUN = VAR ~ TUPLE ^^ { case f ~ tup => Fun(f.name, tup) }
......@@ -157,7 +157,7 @@ object WorkflowParser extends RegexParsers with LazyLogging {
}
}, t => s"$t is not a valid block (check free variables, duplicate variables, ...)" )
def LOOP = "loop" ~> "{" ~> BLOCKLIST <~ "}" ^^ { case bs => Loop(bs) }
def LOOP = "loop" ~> "{" ~> BLOCKLIST <~ "}" ^^ (bs => Loop(bs))
def NDCHOICE = "choose" ~> "{" ~> (BLOCKLIST <~ "}" <~ "{")~ (BLOCK+) <~ "}" ^^ { case l ~ r => NondetChoice(l,r) }
def BLOCKLIST:Parser[List[Block]] = (BLOCK | LOOP | NDCHOICE)+
......
......@@ -31,7 +31,7 @@ case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target:
// TODO: check target types
// TODO: check declass arities and types (o should be an Oracle relation etc)
val ta = target.params(0)
val ta = target.params.head
// check declass bindings
for ((o, (f, t)) <- declass if !t.freeVars().forall(v => (f.contains(v) || (v == ta)))) {
logger.error(s"Not all variables of the declassification condition for $o bound by the oracle")
......@@ -52,22 +52,22 @@ case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target:
// check same relation only updated once per block
def isSane(steps:List[Block]):Boolean = {
val sanes = steps map {s =>
s match {
case b:SimpleBlock => {
// all predicates should only appear at most once
val pred = w.sig.preds.find(p => b.steps.count(s => s.fun == p.name) > 1)
pred.map(p =>
logger.error(s"Predicate $p updated more than once in $b")
)
// if using oracle, only single stmt
val saneoracly = if (b.isoracly) { b.pred.isEmpty && b.steps.size == 1 && saneoraclestmt(b.steps.head, b.agents) } else true
// if (!saneoracly) { logger.warn(s"Oracles used wrongly in $b") }
pred.isEmpty // && saneoracly TODO: enable this later?
}
case Loop(steps) => isSane(steps)
case NondetChoice(left, right) => isSane(left) && isSane(right)
val sanes = steps map {
case b: SimpleBlock => {
// all predicates should only appear at most once
val pred = w.sig.preds.find(p => b.steps.count(s => s.fun == p.name) > 1)
pred.foreach(p =>
logger.error(s"Predicate $p updated more than once in $b")
)
// if using oracle, only single stmt
val saneoracly = if (b.isoracly) {
b.pred.isEmpty && b.steps.size == 1 && saneoraclestmt(b.steps.head, b.agents)
} else true
// if (!saneoracly) { logger.warn(s"Oracles used wrongly in $b") }
pred.isEmpty // && saneoracly TODO: enable this later?
}
case Loop(steps) => isSane(steps)
case NondetChoice(left, right) => isSane(left) && isSane(right)
}
sanes reduce (_ && _)
}
......@@ -95,7 +95,7 @@ abstract sealed class SimpleBlock extends Block {
}
def isoracly = {
steps.exists(s => s.guard.hasSubFormula {
steps.exists(_.guard.hasSubFormula {
case f:Fun => f.isOracle()
})
}
......
......@@ -46,7 +46,7 @@ object FOLTL {
val broken = s replace ("∧ ", "∧\n") replace ("∨ ", "∨\n")
// indent
var opens = 0;
var opens = 0
val indented = for (line <- broken.lines) yield {
val indent = " " * (opens * 2)
val ret = indent + line
......@@ -128,11 +128,11 @@ object FOLTL {
case class Exists(vars: List[Var], t: Formula) extends Quantifier {
val qname = "∃"
val qmake = Exists.apply _
val qmake = Exists.apply
}
case class Forall(vars: List[Var], t: Formula) extends Quantifier {
val qname = "∀"
val qmake = Forall.apply _
val qmake = Forall.apply
}
case class ForallOtherThan(vars: List[Var], otherthan: List[Var], t: Formula) extends Quantifier {
val qname = "∀"
......@@ -145,21 +145,21 @@ object FOLTL {
trait TemporalFormula extends Formula
case class Next(t: Formula) extends TemporalFormula with UnOp {
val make = Next.apply _
val make = Next.apply
val opname = "X"
}
case class Globally(t: Formula) extends TemporalFormula with UnOp {
val make = Globally.apply _
val make = Globally.apply
val opname = "G"
}
case class Finally(t: Formula) extends TemporalFormula with UnOp {
val make = Finally.apply _
val make = Finally.apply
val opname = "F"
}
case class Until(t1: Formula, t2: Formula) extends TemporalFormula with BinOp {
val make = Until.apply _
val make = Until.apply
val opname = "U"
}
......@@ -214,52 +214,52 @@ object FOLTL {
object Or {
def make(terms: List[Formula]) = {
BinOp.makeL(Or.apply _, terms, False)
BinOp.makeL(Or.apply, terms, False)
}
def make(terms: Formula*) = {
BinOp.makeL(Or.apply _, terms, False)
BinOp.makeL(Or.apply, terms, False)
}
}
case class Or(t1: Formula, t2: Formula) extends BinOp {
val opname = "∨"
val make = Or.apply _
val make = Or.apply
}
object And {
def make(terms: List[Formula]) = {
BinOp.makeL(And.apply _, terms, True)
BinOp.makeL(And.apply, terms, True)
}
def make(terms: Formula*) = {
BinOp.makeL(And.apply _, terms, True)
BinOp.makeL(And.apply, terms, True)
}
}
case class And(t1: Formula, t2: Formula) extends BinOp {
val opname = "∧"
val make = And.apply _
val make = And.apply
}
case class Eq(t1: Formula, t2: Formula) extends BinOp {
val opname = "↔"
val make = Eq.apply _
val make = Eq.apply
}
object Eq {
def make(terms: List[Formula]) = {
BinOp.makeL(Eq.apply _, terms, True)
BinOp.makeL(Eq.apply, terms, True)
}
def make(terms: Formula*) = {
BinOp.makeL(Eq.apply _, terms, True)
BinOp.makeL(Eq.apply, terms, True)
}
}
case class Implies(t1: Formula, t2: Formula) extends BinOp {
val opname = "→"
val make = Implies.apply _
val make = Implies.apply
}
case class Neg(t: Formula) extends UnOp {
val make = Neg.apply _
val make = Neg.apply
val opname = "¬"
}
......
......@@ -280,7 +280,7 @@ object FormulaFunctions extends LazyLogging {
// TODO add more things, f.e. existentials
// T1, T2 can appear freely
val frees = t.freeVars() -- Set(Var(Properties.T1), Var(Properties.T2))
if (!frees.isEmpty) {
if (frees.nonEmpty) {
logger.warn(s"Sanity check failed: $frees appear free in the property.")
}
......@@ -356,10 +356,10 @@ object FormulaFunctions extends LazyLogging {
val univset = univbound.toSet
val ex2 = q2.takeWhile(_._1).map(q =>
(q._1, q._2.filterNot(exset.contains _))
(q._1, q._2.filterNot(exset.contains))
)
val rest2 = q2.drop(ex2.size).map(q =>
(q._1, q._2.filterNot(univset.contains _))
(q._1, q._2.filterNot(univset.contains))
)
ex1 ++ ex2 ++ rest1 ++ rest2
}
......@@ -370,7 +370,7 @@ object FormulaFunctions extends LazyLogging {
def checkBindingsSub(f: Formula, bound:Set[Var]):List[Var] = {
f collect {
case Quantifier(make, xs, inner) => {
val conflicts = xs.filter(bound.contains _)
val conflicts = xs.filter(bound.contains)
conflicts ++ checkBindingsSub(inner, bound ++ xs)
}
}
......@@ -381,7 +381,7 @@ object FormulaFunctions extends LazyLogging {
def isBS(f: Formula) = {
val quantprefix = collectQuantifiers(f.toNegNf())
// has no forall exists in quantifier prefix
!quantprefix.sliding(2).exists(list => !list(0)._1 && list(1)._1)
!quantprefix.sliding(2).exists(list => !list.head._1 && list(1)._1)
}
def toNegNf(f: Formula) = {
......@@ -420,7 +420,7 @@ object FormulaFunctions extends LazyLogging {
(make(newf1, newf2), newbound2)
}
case Quantifier(make, vars, fsub) => {
val alreadybounds = vars.filter(bound.contains(_))
val alreadybounds = vars.filter(bound.contains)
val newnames = alreadybounds.map(generateName(_, bound))
val renamed = fsub.parallelRename(alreadybounds, newnames)
val binding = (vars.toSet -- alreadybounds) ++ newnames
......@@ -485,7 +485,7 @@ object FormulaFunctions extends LazyLogging {