stronger invariant

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

@@ -55,7 +55,7 @@ object LTL extends LazyLogging {
   def eliminateUniversals(t: Formula, agents: List[Var]):Formula = {
     
     if (agents.isEmpty) {
-      logger.error("Agent list should never be empty")
+      logger.warn("Agent list empty")
     }
     val universe = agents.groupBy(_.typ)
     

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

@@ -16,78 +16,99 @@ class InvariantTest extends FlatSpec {
 
   "InvariantChecker" should "prove simple things safe" in {
 
-    val wf = ExampleWorkflows.parseExample("tests/simpleChoiceNoOracle").get.w
+    val spec = ExampleWorkflows.parseExample("nonomitting/conference").get
 
-    val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
+//    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)
-
-    safe should be(true)
-  }
-
-  it should "fail to prove unsafe workflows safe" in {
+    val inv = InvariantChecker.invariantNoninterStubbornBS(spec)
     
-    val wf = ExampleWorkflows.parseExample("tests/simpleChoice").get.w
-
-    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)
-
-    safe should be(false)
-  }
-
-  it should "prove the paper example" in {
-    val wf = ExampleWorkflows.parseExample("omitting/conference").get.w
-
-    val x = Var("x", "A")
-    val y = Var("y", "A")
-    val p = Var("p","P")
-    val r = Var("r","R")
-    val c = Fun("Conf", Some("t1"), List(x,p))
-
-//    
-    val ceq = genEq("Conf", List(x,p))
-    val oeq = genEq("O", List(x,p,r))
-    val readeq = genEq("Read", List(x,p,r)) 
-    val assigneq = genEq("Assign", List(x,p))
-    val revieweq = genEq("Review", List(x,p,r))
-//    val premise = And(Neg(c), oeq)
-//    val conclusion = And.make(ceq, readeq, assigneq, Forall(y, revieweq))
+    val added = Or(Neg(Fun("Assign", List(Var("x","A"), Var("p","P")))),
+          Neg(Fun("Conf", List(Var("x","A"), Var("p","P")))))
     
-    val premise = Forall(List(p,r), And(Neg(c), oeq))
-    val conclusion = Forall(List(p,r), And.make(ceq, readeq, assigneq, revieweq))
+    val both = Forall(List(Var("x","A"), Var("p","P")), And(added.in("t1"), added.in("t2")))
     
-    val inv = Forall(List(x), 
-        Implies(premise, conclusion)
-    )
-    val (safe, msg) = InvariantChecker.checkInvariant(wf, inv, true)
+    val newinv = And(inv, both)
     
-    safe should be (true)
+    val (safe, msg) = InvariantChecker.checkInvariant(spec.w, newinv, true)
+
+    println(msg.toString())
+    safe should be(true)
   }
   
-
+//  "InvariantChecker" should "prove simple things safe" in {
+//
+//    val wf = ExampleWorkflows.parseExample("tests/simpleChoiceNoOracle").get.w
+//
+//    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)
+//
+//    safe should be(true)
+//  }
+//
+//  it should "fail to prove unsafe workflows safe" in {
+//    
+//    val wf = ExampleWorkflows.parseExample("tests/simpleChoice").get.w
+//
+//    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)
+//
+//    safe should be(false)
+//  }
+//
+//  it should "prove the paper example" in {
+//    val wf = ExampleWorkflows.parseExample("omitting/conference").get.w
+//
+//    val x = Var("x", "A")
+//    val y = Var("y", "A")
+//    val p = Var("p","P")
+//    val r = Var("r","R")
+//    val c = Fun("Conf", Some("t1"), List(x,p))
+//
+////    
+//    val ceq = genEq("Conf", List(x,p))
+//    val oeq = genEq("O", List(x,p,r))
+//    val readeq = genEq("Read", List(x,p,r)) 
+//    val assigneq = genEq("Assign", List(x,p))
+//    val revieweq = genEq("Review", List(x,p,r))
+////    val premise = And(Neg(c), oeq)
+////    val conclusion = And.make(ceq, readeq, assigneq, Forall(y, revieweq))
+//    
+//    val premise = Forall(List(p,r), And(Neg(c), oeq))
+//    val conclusion = Forall(List(p,r), And.make(ceq, readeq, assigneq, revieweq))
+//    
+//    val inv = Forall(List(x), 
+//        Implies(premise, conclusion)
+//    )
+//    val (safe, msg) = InvariantChecker.checkInvariant(wf, inv, true)
+//    
+//    safe should be (true)
+//  }
+//  
+//
   def genEq(name:String, params: List[Var]) = {
     val o1 = Fun(name, Some("t1"), params)
     val o2 = Fun(name, Some("t2"), params)
     Eq(o1, o2)
   }
-  
-  it should "prove noninter invariants" in {
-    val spec = ExampleWorkflows.parseExample("tests/simpleChoice").get
-
-    val inv = InvariantChecker.invariantNoninterStubborn(spec)
-    val (safe, msg) = InvariantChecker.checkInvariant(spec.w, inv, true)
-
-    safe should be(false)
-  }
-
-  it should "prove the paper example as noninter invariant" in {
-    val spec = ExampleWorkflows.parseExample("omitting/conference").get
-
-    val inv = InvariantChecker.invariantNoninterStubborn(spec)
-    val (safe, msg) = InvariantChecker.checkInvariant(spec.w, inv,true)
-
-    safe should be(true)
-  }
+//  
+//  it should "prove noninter invariants" in {
+//    val spec = ExampleWorkflows.parseExample("tests/simpleChoice").get
+//
+//    val inv = InvariantChecker.invariantNoninterStubborn(spec)
+//    val (safe, msg) = InvariantChecker.checkInvariant(spec.w, inv, true)
+//
+//    safe should be(false)
+//  }
+//
+//  it should "prove the paper example as noninter invariant" in {
+//    val spec = ExampleWorkflows.parseExample("omitting/conference").get
+//
+//    val inv = InvariantChecker.invariantNoninterStubborn(spec)
+//    val (safe, msg) = InvariantChecker.checkInvariant(spec.w, inv,true)
+//
+//    safe should be(true)
+//  }
 
 }
\ No newline at end of file