examples

examples/examplestrategies.txt

+Stubborn:
+
+BSFO SOQE: strategy for B(x1,p1): 
+
+∀ xt:X,pt:P. (
+(¬ Conf(xt,pt) ∨ ¬ (x1 = xt) ∨ ¬ (p1 = pt)) ∧ 
+(¬ Conf(xt,pt) ∨ ∀ yt:X. ¬ (x1 = yt) ∨ ¬ (p1 = pt)))
+
+Causal
+
+BSFO SOQE: strategy for B(x1,p1): 
+∀ xt:X,p:P,pt:P. (
+	(Conf(xt,p) ∨ ¬ Conf(xt,pt) ∨ ¬ (x1 = xt) ∨ ¬ (p1 = pt)) ∧ 
+	∀ yt:X. (
+		(Conf(xt,p) ∨ ¬ Conf(xt,pt) ∨ ¬ (x1 = yt) ∨ ¬ (p = p1)) ∧ 
+		(Conf(xt,p) ∨ ¬ Conf(xt,pt) ∨ ¬ (x1 = yt) ∨ ¬ (pt = p1)) ∧ 
+		(¬ Conf(xt,p) ∨ ¬ Conf(xt,pt) ∨ ¬ (x1 = xt) ∨ ¬ (pt = p1)) ∧ 
+		(¬ Conf(xt,p) ∨ ¬ Conf(xt,pt) ∨ ¬ (x1 = yt) ∨ ¬ (p = p1)) ∧ 
+		(¬ Conf(xt,p) ∨ ¬ Conf(xt,pt) ∨ ¬ (x1 = yt) ∨ ¬ (pt = p1))
+	)
+)
+
+Simpl BSFO SOQE: strategy for B(x1,p1): 
+∀ xt:X,p:P,pt:P. (
+	(Conf(xt,p) ∨ ¬ Conf(xt,pt) ∨ ¬ (x1 = xt) ∨ ¬ (p1 = pt)) ∧ 
+		(Conf(xt,p) ∨ ¬ Conf(xt,pt) ∨ ¬ (p = p1)) ∧ 
+		(Conf(xt,p) ∨ ¬ Conf(xt,pt) ∨ ¬ (pt = p1)) ∧ 
+		(¬ Conf(xt,p) ∨ ¬ Conf(xt,pt) ∨ ¬ (pt = p1)) ∧ 
+		(¬ Conf(xt,p) ∨ ¬ Conf(xt,pt) ∨ ¬ (p = p1)) ∧ 
+		(¬ Conf(xt,p) ∨ ¬ Conf(xt,pt) ∨ ¬ (pt = p1))
+)

examples/tests/conference_linear_small_unsafe.spec

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

examples/tests/conference_stubborn_withB.spec

@@ -2,7 +2,7 @@ Workflow
 
 forallmay x:A,p:P
     True → Conf += (x,p)
-forallmay x:A,p:P
+forall x:A,p:P
     B(x,p) → Assign += (x,p)
 forall x:A,p:P
     (Assign(x,p) ∧ Oracle(x,p)) → Review += (x,p)

examples/tests/leaderelection.spec

+Workflow
+
+forall a,b
+    Inext(a,b) -> msg += (a,b)
+loop {
+	forall a
+		msg(a,a) -> leader += (a)
+	forall a,b,c
+		(Inext(b, c) ∧ msg(a, b) ∧ Ile(b, a)) -> msg += (a,c)
+}
+
+Target
+
+msg(a1, a2)
+
+Causality

examples/tests/leaderelection_nonext.spec

+Workflow
+
+forall a,b
+    ∀d. (d = a ∨ d = b ∨ Ibtw(a,b,d)) -> msg += (a,b)
+loop {
+	forall a
+		msg(a,a) -> leader += (a)
+	forall a,b,c
+		(∀d. (d = b ∨ d = c ∨ Ibtw(b,c,d)) ∧ msg(a, b) ∧ Ile(b,a)) -> msg += (a,c)
+}
+
+Target
+
+msg(a1, a2)
+
+Causality

examples/tests/leaderelection_nonext_unsafe.spec

+Workflow
+
+forall a,b
+    ∀d. (d = a ∨ d = b ∨ Ibtw(a,b,d)) -> msg += (a,b)
+loop {
+	forall a
+		msg(a,a) -> leader += (a)
+	forall a,b,c
+		(∀d. (d = b ∨ d = c ∨ Ibtw(b,c,d)) ∧ msg(a, b)) -> msg += (a,c)
+}
+
+Target
+
+msg(a1, a2)
+
+Causality

examples/tests/leaderelection_unsafe.spec

+Workflow
+
+forall a,b
+    Inext(a,b) -> msg += (a,b)
+loop {
+	forall a
+		msg(a,a) -> leader += (a)
+	forall a,b,c
+		(Inext(b, c) ∧ msg(a, b)) -> msg += (a,c)
+}
+
+Target
+
+msg(a1, a2)
+
+Causality

examples/tests/loopexample.spec

 Workflow
 
-forallmay x,s O(s) -> Q += (x,s)
+forall x,s O(s) -> Q += (x,s)
 loop {
 	forall x,y,s R(y,s) -> S += (x,y,s)
 	forall x,s Q(x,s) -> R += (x,s)

examples/tests/simpleChoice.spec

 Workflow
 
-forallmay x,s
+forall x,s
 	O(s) -> R += (x,s)
 
 Target