improve tests

examples/nonomitting/conference.spec

@@ -13,11 +13,11 @@ loop {
 
 Declassify
 
-O(x:A,p:P,r:R): ¬ Conf(at:A,p:P)
+O(x:A,p:P,r:R): ¬ Conf(xa:A,p:P)
 
 Target
 
-Read(at:A, bt:A, pt:P, rt:R)
+Read(xa:A, xb:A, p:P, r:R)
 
 Causality
 

examples/tests/conferenceNoOracle.spec

+Workflow
+
+forallmay x:A,p:P
+    True → Conf += (x,p)
+forallmay x:A,p:P
+    !Conf(x,p) → Assign += (x,p)
+forall x:A,p:P
+    (Assign(x,p)) → Review += (x,p)
+loop {
+    forall xa:A,xb:A,p:P (Assign(xa,p) ∧ Review(xb,p)) → Read += (xa,xb,p)
+    forallmay x:A,p:P Assign(x,p) → Review += (x,p)
+}
+
+Target
+
+Read(xa:A, xb:A, p:P)

examples/tests/omittingConferenceNoOracle.spec

+Workflow
+
+forallmay x:A,p:P
+    True → Conf += (x,p)
+forallmay x:A,p:P
+    !Conf(x,p) → Assign += (x,p)
+forall x:A,p:P
+    Assign(x,p) → Review += (x,p)
+loop {
+    forall xa:A,xb:A,p:P (Assign(xa,p) ∧ Review(xb,p)) → Read += (xa,xb)
+    forallmay x:A,p:P Assign(x,p) → Review += (x,p)
+}
+
+Target
+
+Read(xa:A, xb:A)

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

@@ -48,7 +48,10 @@ object Preconditions extends LazyLogging {
         }
       }
     }
-    replaced
+    // TODO: have we proven this correct?
+    val removed = FOTransformers.eliminateDoubleQuantifiers(replaced)
+    
+    removed
   }
   
   def abstractPrecondition(f:Formula, b:SimpleBlock, stubborn:Boolean) = {

src/main/scala/de/tum/workflows/ltl/FOTransformers.scala

@@ -42,6 +42,16 @@ object FOTransformers extends LazyLogging {
     collectMultiClause(f)
   }
   
+  def eliminateDoubleQuantifiers(f:Formula) = {
+    def elimSub(f:Formula, bound:Set[Var]):Formula = {
+      f everywhere {
+        // filter out all that are contained in bound
+        case Quantifier(make, vars, inner) => make(vars.filterNot(bound.contains).distinct, elimSub(inner, bound ++ vars))
+      }
+    }
+    elimSub(f, Set())
+  }
+  
   def eliminateAuxiliaryPredicate(f:Formula, AUX:String) = {
     val cnf = f.toCNF().simplify()
     

src/test/scala/de/tum/workflows/ltl/tests/InvariantEasychairTest.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.ExampleWorkflows
+import de.tum.workflows.toz3.InvariantChecker
+import de.tum.workflows.toz3.InvariantGenerator
+
+class InvariantEasychairTest extends FlatSpec {
+
+  "InvariantChecker" should "prove nonomitting/conference safe" in {
+    val name = "nonomitting/conference"
+    val x = Var("x", "A")
+    val p = Var("p","P")
+    val inv = Forall(List(x, p), genEq("Conf", List(x, p)))
+    assert(checkSafe(name, inv))
+  }
+  
+  it should "prove tests/conferenceNoOracle safe" in {
+    val name = "tests/conferenceNoOracle"
+    val xa = Var("xa","A")
+    val xb = Var("xb","A")
+    val p = Var("p","P")
+    val inv = Forall(List(xa, xb, p), genEq("Read", List(xa, xb, p)))
+    assert(checkSafe(name, inv))
+  }
+  
+  it should "prove tests/omittingConferenceNoOracle safe" in {
+    val name = "tests/omittingConferenceNoOracle"
+    val xa = Var("xa","A")
+    val xb = Var("xb","A")
+    val inv = Forall(List(xa, xb), genEq("Read", List(xa, xb)))
+    assert(checkSafe(name, inv))
+  }
+  
+  it should "fail on oracly nonomitting/conference without declass" in {
+    val name = "nonomitting/conference"
+    val xa = Var("xa","A")
+    val xb = Var("xb","A")
+    val p = Var("p", "P")
+    val r = Var("r", "R")
+    val inv = Forall(List(xa, xb, p, r), genEq("Read", List(xa, xb, p, r)))
+    assert(!checkSafe(name, inv))
+  }
+  
+  it should "prove oracly nonomitting/conference with declass" ignore {
+    val name = "nonomitting/conference"
+    val xa = Var("xa","A")
+    val xb = Var("xb","A")
+    val p = Var("p", "P")
+    val r = Var("r", "R")
+        
+    val spec = ExampleWorkflows.parseExample(name).get
+    val inv = InvariantGenerator.invariantNoninterStubbornSingleBS(spec)
+    assert(checkSafe(name, inv))
+  }
+  
+  def checkSafe(name: String, inv: Formula) = {
+    val spec = ExampleWorkflows.parseExample(name).get
+    val (res, dot) = InvariantChecker.checkInvariantFP(spec.w, inv, true)
+    Utils.write(s"${name}.dot", dot)
+    res
+  }
+
+  def genEq(name: String, params: List[Var]) = {
+    val o1 = Fun(name, Some("t1"), params)
+    val o2 = Fun(name, Some("t2"), params)
+    Eq(o1, o2)
+  }
+}
\ No newline at end of file

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

@@ -42,7 +42,7 @@ class InvariantTest extends FlatSpec {
 //
 //    val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
 //
-//    val (safe, msg) = InvariantChecker.checkInvariant(wf, inv, true)
+//    val (safe, msg) = InvariantChecker.checkInvariantFP(wf, inv, true)
 //
 //    safe should be(true)
 //  }