withB

examples/tests/conference_linear_small.spec

@@ -2,10 +2,12 @@ Workflow
 
 forallmay x:X,p:P
 	True -> Conf += (x,p)
+forallmay x:x,p:P
+    ¬Conf(x,p) -> Assign += (x,p)
 forall x:X,p:P,r:R
-	(¬ Conf(x,p) ∧ O(x,p,r)) -> Read += (x,p,r)
+	(Assign(x,p) ∧ O(x,p,r)) -> Read += (x,p,r)
 forallmay y:X,x:X,p:P
-	(¬ Conf(x,p) ∧ ¬ Conf(y,p)) -> Comm += (x,y,p)
+	(Assign(x,p) ∧ Assign(y,p)) -> Comm += (x,y,p)
 
 Declassify
 

examples/tests/conference_linear_small_withB.spec

+Workflow
+
+forallmay x:X,p:P
+    True -> Conf += (x,p)
+forall x:x,p:P
+    B(x,p) -> Assign += (x,p)
+forall x:X,p:P,r:R
+    (Assign(x,p) ∧ O(x,p,r)) -> Read += (x,p,r)
+forallmay y:X,x:X,p:P
+    (Assign(x,p) ∧ Assign(y,p)) -> Comm += (x,y,p)
+
+Declassify
+
+O(x:X,p:P,r:R): ¬ Conf(xt:X,p:P)
+
+Target
+
+Comm(xt:X, yt:X, pt:P)
+
+Causality
+
+a:X

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

@@ -36,7 +36,7 @@ object MainInvariantsInference extends App with LazyLogging {
 
     val inv = invariant(spec)
 //    val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, inv, props)
-    val res = Utils.check("tests/conference_linear_small", "elimB", inv, props)
+    val res = Utils.check(name, "elimB", inv, props)
 
   }
 
@@ -62,7 +62,7 @@ object MainInvariantsInference extends App with LazyLogging {
 
   //  clear()
   //  generateExample("nonomitting/conference")
-  generateExample("tests/conference_linear_small", 1)
+  generateExample("tests/conference_linear_small_withB", 1)
   //  generateExample("nonomitting/conference_linear", 2)
   //  generateExample("tests/loopexampleNoOracle")
   //  generateAllExamples()