make omittings work

examples/tests/simpleChoiceOmittingNoOracle.spec

@@ -3,9 +3,6 @@ Workflow
 forallmay x,s
     True -> R += (x,s)
 
-forallmay x,s
-    R(x,s) -> S += (x)
-
 Target
 
 S(x)

examples/tests/simpleChoiceOmittingNoOracleTwice.spec

+Workflow
+
+forallmay x,s
+    True -> R += (x,s)
+
+forallmay x,s
+    R(x,s) -> S += (x)
+
+Target
+
+S(x)

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

@@ -12,8 +12,9 @@ import de.tum.workflows.ltl.FOTransformers
 object Preconditions extends LazyLogging {
   
   def weakestPrecondition(f: Formula, b: SimpleBlock) = {
-    // TODO: f can't be temporal yet
     val choice = b.pred.map(n => Fun(n, b.agents))
+    
+    // TODO: Only introduce quantifiers if not already in scope
 
     val updates = b.steps.map(s => {
       s.fun -> (s.tuple, {
@@ -61,7 +62,13 @@ object Preconditions extends LazyLogging {
     } else precond
     
     // Abstract away inner existentials
-    val universalinv = FOTransformers.abstractExistentials(stubprecond).simplify()
+    val universalinv = if (b.isomitting) {
+      FOTransformers.abstractExistentials(stubprecond).simplify()
+    } else {
+      stubprecond
+    }
+    
+    val cnf = universalinv.toCNF().simplify()
     
     // Abstract away auxilliaries
     val auxless = if (b.pred.isDefined) {

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

@@ -3,6 +3,7 @@ package de.tum.workflows.foltl
 import FOLTL._
 import com.typesafe.scalalogging.LazyLogging
 import de.tum.workflows.blocks.Workflow
+import scala.annotation.tailrec
 
 object FormulaFunctions extends LazyLogging {
 
@@ -301,7 +302,7 @@ object FormulaFunctions extends LazyLogging {
         val ex2 = q2.takeWhile(_._1).map(q =>
           (q._1, q._2.filterNot(exset.contains _))
         )
-        val rest2 = q2.drop(ex1.size).map(q =>
+        val rest2 = q2.drop(ex2.size).map(q =>
           (q._1, q._2.filterNot(univset.contains _))
         )
         ex1 ++ ex2 ++ rest1 ++ rest2
@@ -388,22 +389,24 @@ object FormulaFunctions extends LazyLogging {
 
     quants.foldRight(stripped)((quant, inner) => {
       if (quant._1) Exists(quant._2, inner) else Forall(quant._2, inner)
-    })
+    }).simplify()
   }
 
   def toCNF(f: Formula) = {
+    @tailrec
     def toCNFSub(f: Formula): Formula = {
-      f.everywhere({
-        case Or(And(f1, f2), f3) => And(toCNFSub(Or(f1, f3)), toCNFSub(Or(f2, f3)))
-        case Or(f1, And(f2, f3)) => And(toCNFSub(Or(f1, f2)), toCNFSub(Or(f1, f3)))
+      val sub = f.everywhere({
+        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)
     }
 
     // FIXME: can we do it without prenex? may be expensive later on
-    val normalized = f.toNegNf().toPrenex()
+    val normalized = f.toNegNf().toPrenex().simplify()
 
     // normalized is now Quantifiers, then only And/Or with Negation inside
-    toCNFSub(normalized)
+    toCNFSub(normalized).simplify()
   }
 
   /**

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

@@ -43,7 +43,7 @@ object FOTransformers extends LazyLogging {
   }
   
   def eliminateAuxiliaryPredicate(f:Formula, AUX:String) = {
-    val cnf = f.toCNF()
+    val cnf = f.toCNF().simplify()
     
     val quantifiers = FormulaFunctions.collectQuantifiers(cnf)
     
@@ -84,7 +84,8 @@ object FOTransformers extends LazyLogging {
       // don't go over Globally
       case Globally(_) => List.empty
     }
-    val agents = t.collect(coll)
+    // TODO: this only works if the a's are not in scope of one another
+    val agents = t.collect(coll).distinct
     
     def elim:PartialFunction[Formula, Formula] = {
       case Exists(a, term) => term.everywhere(elim)
@@ -181,9 +182,9 @@ object FOTransformers extends LazyLogging {
       logger.error(s"Formula was $f")
     }
     
-//    val (agents, inner) = LTL.eliminateExistentials(nf)
-//    val existbound = Exists(agents, inner)
-    val res = FOTransformers.eliminateUniversals(neg, List())
+    val (agents, inner) = FOTransformers.eliminateExistentials(neg)
+    val existbound = Exists(agents, inner)
+    val res = FOTransformers.eliminateUniversals(existbound, List())
     Neg(res).simplify()
   }
 }
\ No newline at end of file

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

@@ -63,23 +63,16 @@ class FOLTLTest extends FlatSpec {
     f.toPrenex() should be (Forall("x", Exists("y", Forall("z", Exists("a", And("x", Or(Neg("a"), "z")))))))
   }
   
-  it should "rebind variable names for prenex" in {
-    val f = Forall("x", And(Exists("z", "z"), Forall("z", Or(Neg(Forall("a", "a")), "z"))))
-    
-    f.toPrenex() should be (Forall("x", Exists("z", Forall("z1", Exists("a", And("z", Or(Neg("a"), "z1"))))))) 
-  }
-  
   it should "rebind several things" in {
     val f = And.make(Forall("x", "x"), Forall("x", "x"), Forall("x","x"))
     val p = f.toPrenex().simplify()
-    p should be (Forall(List("x","x1","x2"), And.make("x", "x1","x2")))
-    f.simplify().toPrenex() should be (Forall("x","x"))
+    p should be (Forall("x","x"))
   }
   
   it should "work on implication" in {
     val f = Implies(Forall("a", "a"), Exists("x", "x"))
     
-    f.toPrenex() should be (Exists("a", Exists("x", Or(Neg("a"), "x"))))
+    f.toPrenex() should be (Exists(List("a","x"), Or(Neg("a"), "x")))
   }
   
   it should "preserve BS" in {
@@ -92,20 +85,20 @@ class FOLTLTest extends FlatSpec {
     val f = Or(And("a", "b"), And("c","d"))
     
     f.toCNF() should be (
-      And(
-          And(Or("a", "c"), Or("a","d")), 
-          And(Or("b","c"), Or("b","d"))
-      )    
+      And.make(
+          Or("a", "c"), Or("a","d"), 
+          Or("b","c"), Or("b","d")
+      )
     )
   }
   
   it should "compute CNF for formulas with quantifiers" in {
     val f = Or(And(Exists("c", "c"), "b"), And(Exists("c", "c"),"d"))
-    f.toCNF().simplify() should be (
-      Exists(List("c", "c1"), And.make(
-          Or("c", "c1"), 
+    f.toCNF() should be (
+      Exists(List("c"), And.make(
+          "c", 
           Or("c","d"), 
-          Or("b","c1"), 
+          Or("b","c"), 
           Or("b","d")
       ))    
     )

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

@@ -24,6 +24,12 @@ class NonOmittingInvariantFilesTest extends FlatSpec {
     val inv = Forall(List("x", "s"), genEq("R", List("x", "s")))
     assert(checkSafe(name, inv))
   }
+  
+  it should "prove simple may blocks safe" in {
+    val name = "tests/simpleChoiceNoOracle"
+    val inv = Forall(List("x", "s"), genEq("R", List("x", "s")))
+    assert(checkSafe(name, inv))
+  }
 
   it should "prove simple loops safe" in {
     val name = "tests/loopexampleNoOracle"

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

@@ -17,32 +17,27 @@ import de.tum.workflows.Encoding
 
 class OmittingInvariantFilesTest extends FlatSpec {
 
-//  "InvariantChecker" should "prove simple things safe" in {
-//    val name = "tests/simpleOmittingNoChoice"
-//    val inv = Forall(List("x","s"), genEq("R",List("x","s")))
-//    assert(checkSafe(name, inv))
-//  }
   
-  it should "prove simple things safe" in {
-    val name = "tests/simpleOmittingNoChoice"
-    val inv = Forall(List("x"), genEq("S",List("x")))
+  "InvariantChecker" should "prove simple may things safe" in {
+    val name = "tests/simpleChoiceOmittingNoOracle"
+    val inv = 
+      And(Forall(List("x"), genEq("S", List("x"))), 
+        Forall(List("x","s"), genEq("R",List("x","s")))
+        )
     assert(checkSafe(name, inv))
   }
-  
-//    "InvariantChecker" should "prove simple things safe" in {
-//    val name = "tests/simpleChoiceOmittingNoOracle"
-//    val inv = 
-//      And(Forall(List("x"), genEq("S", List("x"))), 
-//        Forall(List("x","s"), genEq("R",List("x","s")))
-//        )
-//    assert(checkSafe(name, inv))
-//  }
     
-//  it should "infer simple things safe" in {
-//    val name = "tests/simpleChoiceOmittingNoOracle"
-//    val inv = Forall(List("a"), genEq("S", List("a")))
-//    assert(checkSafe(name, inv))
-//  }
+  it should "prove simple things safe" in {
+	  val name = "tests/simpleOmittingNoChoice"
+			  val inv = Forall(List("x"), genEq("S",List("x")))
+			  assert(checkSafe(name, inv))
+  }
+  
+  it should "fail on oracly things" in {
+    val name = "tests/simpleChoiceOmitting"
+    val inv = Forall(List("x"), genEq("R", List("x")))
+    assert(!checkSafe(name, inv))
+  }
 
   def checkSafe(name: String, inv: Formula) = {
     val spec = ExampleWorkflows.parseExample(name).get