examples

examples/tests/leaderelection_withB.spec

 Workflow
 
-forallmay a,b
-    B(a,b) -> msg += (a,b)
+forall a,b,i
+    (Inext(a,b) ∧ B(i,a,b)) -> msg += (i,b)
 loop {
 	forall a
 		msg(a,a) -> leader += (a)
-	forallmay a,b,c
+	forall a,b,c
 		(Inext(b, c) ∧ msg(a, b) ∧ Ile(b, a)) -> msg += (a,c)
 }