add causal tests

examples/tests/simpleChoiceCausal.spec

+Workflow
+
+forall x
+    O(x) -> R += (x)
+
+forallmay x
+    True -> S += (x)
+
+Target
+
+S(xt)

examples/tests/simpleChoiceOmittingNoOracle.spec

@@ -5,4 +5,4 @@ forallmay x,s
 
 Target
 
-S(x)
+R(xt,st)

renderpngs.sh

@@ -4,6 +4,7 @@ TIMEOUT=1m
 
 for FILE in results/*/*.png
 do
+	echo "Deleting ${FILE}"
 	rm $FILE
 done
 

src/main/scala/de/tum/workflows/Preconditions.scala

@@ -73,7 +73,7 @@ object Preconditions extends LazyLogging {
     
     val b = elaborateOraclyBlock(outerb, spec)
     // elaborate only if non-stubborn
-    val steps = if (stubborn) elaborateSteps(b, spec) else b.steps
+    val steps = if (!stubborn) elaborateSteps(b, spec) else b.steps
     
     val choice = b.pred.map(n => Fun(n, b.agents))
     
@@ -150,8 +150,6 @@ object Preconditions extends LazyLogging {
       precond
     }
     
-//    val cnf = universalinv.toCNF().simplify()
-    
     // Abstract away auxilliaries
     val auxless = if (b.pred.isDefined) {
       FOTransformers.eliminateAuxiliaryPredicate(universalinv, b.pred.get).simplify()

src/main/scala/de/tum/workflows/Utils.scala

@@ -49,7 +49,7 @@ object Utils {
     fol.mkdirs()
     recclear(fol)
   }
-
+  
   def write(name: String, prop: String) {
     val file = new File(s"$RESULTSFOLDER/$name")
     if (file.exists()) {

src/main/scala/de/tum/workflows/foltl/FormulaFunctions.scala

@@ -419,11 +419,11 @@ object FormulaFunctions extends LazyLogging {
   def toCNF(f: Formula) = {
     @tailrec
     def toCNFSub(f: Formula): Formula = {
-      val sub = f.everywhere({
+      val (changed, sub) = everywhereFP({
         case Or(And(f1, f2), f3) => And(Or(f1, f3), Or(f2, f3))
         case Or(f1, And(f2, f3)) => And(Or(f1, f2), Or(f1, f3))
-      })
-      if (sub == f) f else toCNFSub(sub)
+      }, f)
+      if (!changed) sub else toCNFSub(sub)
     }
 
     // FIXME: can we do it without prenex? may be expensive later on

src/main/scala/de/tum/workflows/toz3/InvariantChecker.scala

@@ -17,6 +17,7 @@ import de.tum.workflows.foltl.FOLTL._
 import de.tum.workflows.foltl.FormulaFunctions
 import de.tum.workflows.ltl.FOTransformers
 import de.tum.workflows.Utils
+import de.tum.workflows.foltl.Properties
 
 object InvariantChecker extends LazyLogging {
 
@@ -69,7 +70,7 @@ object InvariantChecker extends LazyLogging {
 
     // TODO: do we do this here?
     val firstprecond = if (isfirst) {
-      precond.assumeEmpty(spec.w.sig.preds.map(_.name).toList)
+      precond.assumeEmpty(Properties.INFNAME :: spec.w.sig.preds.map(_.name).toList)
     } else { precond }
 
     //      val test1 = inv.toPrenex()

src/test/scala/de/tum/workflows/ltl/tests/InvariantCausalFilesTest.scala

+package de.tum.workflows.ltl.tests
+
+import org.scalatest.FlatSpec
+import org.scalatest.Matchers._
+import org.scalatest.Inspectors._
+
+import de.tum.workflows.foltl.FOLTL._
+import de.tum.workflows.Implicits._
+import de.tum.workflows.blocks._
+import de.tum.workflows.Preconditions
+import de.tum.workflows.foltl.FormulaFunctions
+import de.tum.workflows.ExampleWorkflows
+import de.tum.workflows.toz3.InvariantChecker
+import de.tum.workflows.Encoding._
+import de.tum.workflows.Utils
+import de.tum.workflows.Encoding
+
+import de.tum.workflows.tests.TestUtils._
+
+class InvariantCausalFilesTest extends FlatSpec {
+  
+  "InvariantChecker" should "prove simple causal may things safe" in {
+    val name = "tests/simpleChoiceOmittingNoOracle"
+    val inv = Forall(List("xt"), genEq("R", List("xt", "st")))
+    assert(checkSafeCausal(name, inv))
+  }
+  
+  it should "fail to prove simple causal may things" in {
+    val name = "tests/simpleChoiceCausal"
+    val inv = Forall(List("xt"), genEq("S", List("xt")))
+    assert(!checkSafeCausal(name, inv))
+  }
+  
+  it should "fail to prove conference/linear" ignore {
+    val name = "nonomitting/conference_linear"
+    val xt = Var("xt","X")
+    val yt = Var("yt","X")
+    val pt = Var("pt","P")
+    val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
+    assert(!checkSafeCausal(name, inv))
+  }
+    
+}
\ No newline at end of file

src/test/scala/de/tum/workflows/ltl/tests/InvariantEasychairTest.scala

@@ -27,7 +27,7 @@ class InvariantEasychairTest extends FlatSpec {
     val x = Var("xt", "A")
     val p = Var("pt","P")
     val inv = Forall(List(x, p), genEq("Conf", List(x, p)))
-    assert(checkSafe(name, inv))
+    assert(checkSafeStubborn(name, inv))
   }
   
   it should "prove nonomitting/conference_linear with declass safe" in {
@@ -36,7 +36,7 @@ class InvariantEasychairTest extends FlatSpec {
     val y = Var("yt","X")
     val p = Var("pt","P")
     val inv = Forall(List(x, p), genEq("Comm", List(x, y, p)))
-    assert(checkSafe(name, inv))
+    assert(checkSafeStubborn(name, inv))
   }
   
   
@@ -46,7 +46,7 @@ class InvariantEasychairTest extends FlatSpec {
     val xb = Var("xbt","A")
     val p = Var("pt","P")
     val inv = Forall(List(xa, xb, p), genEq("Read", List(xa, xb, p)))
-    assert(checkSafe(name, inv))
+    assert(checkSafeStubborn(name, inv))
   }
   
   it should "prove tests/omittingConferenceNoOracle safe" in {
@@ -54,7 +54,7 @@ class InvariantEasychairTest extends FlatSpec {
     val xa = Var("xat","A")
     val xb = Var("xbt","A")
     val inv = Forall(List(xa, xb), genEq("Read", List(xa, xb)))
-    assert(checkSafe(name, inv))
+    assert(checkSafeStubborn(name, inv))
   }
   
   it should "fail on oracly nonomitting/conference without declass" in {
@@ -64,7 +64,7 @@ class InvariantEasychairTest extends FlatSpec {
     val p = Var("pt", "P")
     val r = Var("rt", "R")
     val inv = Forall(List(xa, xb, p, r), genEq("Read", List(xa, xb, p, r)))
-    assert(!checkSafe(name, inv))
+    assert(!checkSafeStubborn(name, inv))
   }
   
   it should "prove oracly nonomitting/conference with declass" in {
@@ -74,6 +74,6 @@ class InvariantEasychairTest extends FlatSpec {
     val p = Var("pt", "P")
     val r = Var("rt", "R")
     val inv = Forall(List(xa, xb, p, r), genEq("Read", List(xa, xb, p, r)))
-    assert(checkSafe(name, inv))
+    assert(checkSafeStubborn(name, inv))
   }
 }
\ No newline at end of file

src/test/scala/de/tum/workflows/ltl/tests/NonOmittingInvariantFilesTest.scala

@@ -24,36 +24,36 @@ class NonOmittingInvariantFilesTest extends FlatSpec {
   "InvariantChecker" should "prove simple things safe" in {
     val name = "tests/simpleNoChoice2"
     val inv = Forall(List("xt", "st"), genEq("R", List("xt", "st")))
-    assert(checkSafe(name, inv))
+    assert(checkSafeStubborn(name, inv))
   }
   
   it should "prove simple may blocks safe" in {
     val name = "tests/simpleChoiceNoOracle"
     val inv = Forall(List("xt", "st"), genEq("R", List("xt", "st")))
-    assert(checkSafe(name, inv))
+    assert(checkSafeStubborn(name, inv))
   }
 
   it should "prove simple loops safe" in {
     val name = "tests/loopexampleNoOracle"
     val inv = Forall(List("xt", "st"), genEq("R", List("xt", "st")))
-    assert(checkSafe(name, inv))
+    assert(checkSafeStubborn(name, inv))
   }
   
   it should "prove simple loops safe and iterate" in {
     val name = "tests/loopexampleNoOracle"
     val inv = Forall(List("xt", "yt", "st"), genEq("S", List("xt", "yt", "st")))
-    assert(checkSafe(name, inv))
+    assert(checkSafeStubborn(name, inv))
   }
 
   it should "fail on oracly things" in {
     val name = "tests/simpleOracle"
     val inv = Forall(List("xt", "st"), genEq("R", List("xt", "st")))
-    assert(!checkSafe(name, inv))
+    assert(!checkSafeStubborn(name, inv))
   }
   
   it should "fail on loopy oracly things" in {
     val name = "tests/loopexample"
     val inv = Forall(List("xt", "yt", "st"), genEq("S", List("xt", "yt", "st")))
-    assert(!checkSafe(name, inv))
+    assert(!checkSafeStubborn(name, inv))
   }
 }
\ No newline at end of file

src/test/scala/de/tum/workflows/ltl/tests/OmittingInvariantFilesTest.scala

@@ -25,24 +25,24 @@ class OmittingInvariantFilesTest extends FlatSpec {
       And(Forall(List("xt"), genEq("S", List("xt"))), 
         Forall(List("xt","st"), genEq("R",List("xt","st")))
         )
-    assert(checkSafe(name, inv))
+    assert(checkSafeStubborn(name, inv))
   }
     
   it should "prove simple things safe" in {
 	  val name = "tests/simpleOmittingNoChoice"
 			  val inv = Forall(List("xt"), genEq("S",List("xt")))
-			  assert(checkSafe(name, inv))
+			  assert(checkSafeStubborn(name, inv))
   }
   
   it should "fail on oracly things" in {
     val name = "tests/simpleChoiceOmitting"
     val inv = Forall(List("xt"), genEq("R", List("xt")))
-    assert(!checkSafe(name, inv))
+    assert(!checkSafeStubborn(name, inv))
   }
   
   it should "work on declassified oracly things" in {
     val name = "tests/simpleChoiceDeclassified"
     val inv = Forall(List("xt"), genEq("R", List("xt")))
-    assert(checkSafe(name, inv))
+    assert(checkSafeStubborn(name, inv))
   }
 }
\ No newline at end of file

src/test/scala/de/tum/workflows/ltl/tests/TestUtils.scala

@@ -6,7 +6,7 @@ import de.tum.workflows._
 
 object TestUtils {
     
-  def checkSafe(name: String, inv: Formula) = {
+  def checkSafeStubborn(name: String, inv: Formula) = {
     val spec = ExampleWorkflows.parseExample(name).get
     val (res, dot) = InvariantChecker.checkInvariantFP(spec, inv, true)
     for ((s, i) <- dot.zipWithIndex) {
@@ -15,6 +15,15 @@ object TestUtils {
     res
   }
   
+  def checkSafeCausal(name: String, inv: Formula) = {
+    val spec = ExampleWorkflows.parseExample(name).get
+    val (res, dot) = InvariantChecker.checkInvariantFP(spec, inv, false)
+    for ((s, i) <- dot.zipWithIndex) {
+      Utils.write(s"${name}_${i}.dot", s)
+    }
+    res
+  }
+  
   def genEq(name: String, params: List[Var]) = {
     val o1 = Fun(name, Some("t1"), params)
     val o2 = Fun(name, Some("t2"), params)