vmcai submission examples

examples/tests/leaderelection_withB.spec

 Workflow
 
 forall a,b,i
-    (Inext(a,b) ∧ B(a,b,i)) -> msg += (i,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)
+		(Inext(b, c) ∧ msg(a, b) ∧ B(b, a)) -> msg += (a,c)
 }
 
 Target

examples/tstests/leaderelection_inductive_withB2.spec

 Signature
-    EmptyPredicates:    msg(a, b), leader(a)
+    EmptyPredicates:    msg(a, i, b), leader(a)
     AxiomPredicates:    next(a, b), leq(a, b), btw(a, b, c)
-    As:                 -
-    Bs:                 B(a,b)
+    As:                 A(a)
+    Bs:                 B(a,i,b)
     Constants:          -
 
 Transition System
-    msg(a,b) := B(a,b)
+    msg(a,i,b) := (next(a,b) ∧ B(a,i,b))
     loop {
-        leader(a) := msg(a, a)
-        msg(a,c) := ∃b. (next(b, c) ∧ msg(a, b) ∧ leq(b, a))
+        leader(b) := ∃a. msg(a, b, b)
+        msg(a,i,b) := (A(a) ∧ next(a, b) ∧ ∃c. msg(c, i, a) ∧ leq(a, i))
     }
 
 Invariant
     ∀n1,n2. (¬leader(n1) ∨ ¬leader(n2) ∨ n1 = n2),
     ∀n1,n2. (n1 = n2 ∨ ¬leader(n1) ∨ ¬leq(n1, n2)),
-    ∀n1,n2. (n1 = n2 ∨ ¬msg(n1, n1) ∨ ¬leq(n1, n2)),
-    ∀n1,n2,n3. (¬btw(n1,n2,n3) ∨ ¬msg(n2,n1) ∨ ¬leq(n2,n3))
+    ∀n1,n2,n3. (n1 = n2 ∨ ¬msg(n3, n1, n1) ∨ ¬leq(n1, n2)),
+    ∀n1,n2,n3,n4. (¬btw(n1,n2,n3) ∨ ¬msg(n4,n2,n1) ∨ ¬leq(n2,n3))
 
 Axioms
     ∀x. leq(x,x),

examples/tstests/leaderelection_inductive_withB_uni.spec

+Signature
+    EmptyPredicates:    msg(a, b), leader(a)
+    AxiomPredicates:    next(a, b), leq(a, b), btw(a, b, c)
+    As:                 -
+    Bs:                 B(a,b)
+    Constants:          -
+
+Transition System
+    msg(a,b) := (next(a,b) ∧ B(a,b))
+    loop {
+        leader(a) := msg(a, a)
+        msg(a,c) := ∃b. (next(b, c) ∧ msg(a, b) ∧ leq(b, a))
+    }
+
+Invariant
+    ∀n1,n2. (¬leader(n1) ∨ ¬leader(n2) ∨ n1 = n2),
+    ∀n1,n2. (n1 = n2 ∨ ¬leader(n1) ∨ ¬leq(n1, n2)),
+    ∀n1,n2. (n1 = n2 ∨ ¬msg(n1, n1) ∨ ¬leq(n1, n2)),
+    ∀n1,n2,n3. (¬btw(n1,n2,n3) ∨ ¬msg(n2,n1) ∨ ¬leq(n2,n3))
+
+Axioms
+    ∀x. leq(x,x),
+    ∀x,y,z. (¬leq(x,y) ∨ ¬leq(y,z) ∨ leq(x,z)),
+    ∀x,y. (¬leq(x,y) ∨ ¬leq(y,x) ∨ x = y),
+    ∀x,y. (leq(x,y) ∨ leq(y,x)),
+
+    ∀x,y,z. (¬btw(x,y,z) ∨ btw(y,z,x)),
+    ∀w,x,y,z. (¬btw(w,x,y) ∨ ¬btw(w,y,z) ∨ btw(w,x,z)),
+    ∀w,x,y. (¬btw(w,x,y) ∨ ¬btw(w,y,x)),
+    ∀w,x,y. (w = x ∨ w = y ∨ x = y ∨ btw(w, x, y) ∨ btw(w, y, x)),
+
+    ∀a,b. (¬next(a,b) ∨ ∀x. (x = a ∨ x = b ∨ btw(a,b,x)))

examples/tstests/leaderelection_inductive_withLoopB.spec

+Signature
+    EmptyPredicates:    msg(a, b), leader(a)
+    AxiomPredicates:    next(a, b), leq(a, b), btw(a, b, c)
+    As:                 -
+    Bs:                 B(a,b)
+    Constants:          -
+
+Transition System
+    msg(a,b) := next(a,b)
+    loop {
+        leader(a) := msg(a, a)
+        msg(a,c) := ∃b. (next(b, c) ∧ msg(a, b) ∧ B(a, b))
+    }
+
+Invariant
+    ∀n1,n2. (¬leader(n1) ∨ ¬leader(n2) ∨ n1 = n2),
+    ∀n1,n2. (n1 = n2 ∨ ¬leader(n1) ∨ ¬leq(n1, n2)),
+    ∀n1,n2. (n1 = n2 ∨ ¬msg(n1, n1) ∨ ¬leq(n1, n2)),
+    ∀n1,n2,n3. (¬btw(n1,n2,n3) ∨ ¬msg(n2,n1) ∨ ¬leq(n2,n3))
+
+Axioms
+    ∀x. leq(x,x),
+    ∀x,y,z. (¬leq(x,y) ∨ ¬leq(y,z) ∨ leq(x,z)),
+    ∀x,y. (¬leq(x,y) ∨ ¬leq(y,x) ∨ x = y),
+    ∀x,y. (leq(x,y) ∨ leq(y,x)),
+
+    ∀x,y,z. (¬btw(x,y,z) ∨ btw(y,z,x)),
+    ∀w,x,y,z. (¬btw(w,x,y) ∨ ¬btw(w,y,z) ∨ btw(w,x,z)),
+    ∀w,x,y. (¬btw(w,x,y) ∨ ¬btw(w,y,x)),
+    ∀w,x,y. (w = x ∨ w = y ∨ x = y ∨ btw(w, x, y) ∨ btw(w, y, x)),
+
+    ∀a,b. (¬next(a,b) ∨ ∀x. (x = a ∨ x = b ∨ btw(a,b,x)))

examples/tstests/leaderelection_inductive_withNegB2.spec

+Signature
+    EmptyPredicates:    msg(a, i, b), leader(a)
+    AxiomPredicates:    next(a, b), leq(a, b), btw(a, b, c)
+    As:                 A(a)
+    Bs:                 B(a,i,b)
+    Constants:          -
+
+Transition System
+    msg(a,i,b) := (next(a,b) ∧ B(a,i,b))
+    loop {
+        leader(b) := ∃a. msg(a, b, b)
+        msg(a,i,b) := (A(a) ∧ next(a, b) ∧ ∃c. msg(c, i, a) ∧ leq(a, i))
+    }
+
+Invariant
+    ∀n1,n2. (¬leader(n1) ∨ ¬leader(n2) ∨ n1 = n2),
+    ∀n1,n2. (n1 = n2 ∨ ¬leader(n1) ∨ ¬leq(n1, n2)),
+    ∀n1,n2,n3. (n1 = n2 ∨ ¬msg(n3, n1, n1) ∨ ¬leq(n1, n2)),
+    ∀n1,n2,n3,n4. (¬btw(n1,n2,n3) ∨ ¬msg(n4,n2,n1) ∨ ¬leq(n2,n3))
+
+Axioms
+    ∀x. leq(x,x),
+    ∀x,y,z. (¬leq(x,y) ∨ ¬leq(y,z) ∨ leq(x,z)),
+    ∀x,y. (¬leq(x,y) ∨ ¬leq(y,x) ∨ x = y),
+    ∀x,y. (leq(x,y) ∨ leq(y,x)),
+
+    ∀x,y,z. (¬btw(x,y,z) ∨ btw(y,z,x)),
+    ∀w,x,y,z. (¬btw(w,x,y) ∨ ¬btw(w,y,z) ∨ btw(w,x,z)),
+    ∀w,x,y. (¬btw(w,x,y) ∨ ¬btw(w,y,x)),
+    ∀w,x,y. (w = x ∨ w = y ∨ x = y ∨ btw(w, x, y) ∨ btw(w, y, x)),
+
+    ∀a,b. (¬next(a,b) ∨ ∀x. (x = a ∨ x = b ∨ btw(a,b,x)))

results/tests/simpleChoice_stubborn/tests/simpleChoice_stubborn.owlltl

-((F(!p13&p8)|F(p13&!p8))&!p2&!p1&!p0&G(!p5|!p2)&p5&G(!p2|(((X!p4&!p4)|(p4&Xp4))&((!p13&X!p13)|(p13&Xp13))&((Xp1&p1)|(X!p1&!p1))&((p11&Xp11)|(!p11&X!p11)))|X!p2)&G(!p2|(((Xp0&p0)|(X!p0&!p0))&((!p12&X!p12)|(p12&Xp12))&((Xp9&p9)|(X!p9&!p9))&((Xp8&p8)|(X!p8&!p8)))|X!p2)&G(X!p2|((((p13|p10)&Xp13)|(X!p13&!p13&!p10))&(((p11|p10)&Xp11)|(!p11&X!p11&!p10))&(((p7|p4)&Xp4)|(X!p4&!p7&!p4))&((!p1&X!p1&!p7)|((p7|p1)&Xp1)))|!p5)&G(X!p2|((((p8|p3)&Xp8)|(!p3&!p8&X!p8))&((Xp12&(p12|p3))|(!p3&X!p12&!p12))&((!p0&!p6&X!p0)|((p6|p0)&Xp0))&((!p9&X!p9&!p6)|(Xp9&(p9|p6))))|!p5)&!p13&!p12&!p11&G(!p5|Xp2)&!p9&!p8&G(Xp2|!p2)&!p4)
\ No newline at end of file
+(!p4&!p2&!p1&!p0&G((((Xp4&p4)|(!p4&X!p4))&((p13&Xp13)|(!p13&X!p13))&((X!p1&!p1)|(Xp1&p1))&((p11&Xp11)|(!p11&X!p11)))|X!p2|!p2)&G((((X!p0&!p0)|(Xp0&p0))&((!p8&X!p8)|(p8&Xp8))&((p12&Xp12)|(!p12&X!p12))&((!p9&X!p9)|(p9&Xp9)))|X!p2|!p2)&(F(!p13&p8)|F(p13&!p8))&G(!p5|X!p2|((((p7|p1)&Xp1)|(!p7&X!p1&!p1))&((!p10&X!p13&!p13)|((p13|p10)&Xp13))&((!p11&!p10&X!p11)|((p11|p10)&Xp11))&((X!p4&!p4&!p7)|(Xp4&(p7|p4)))))&G(!p5|!p2)&G(!p5|X!p2|(((X!p8&!p3&!p8)|(Xp8&(p8|p3)))&((!p12&!p3&X!p12)|((p12|p3)&Xp12))&((Xp0&(p6|p0))|(!p0&!p6&X!p0))&(((p9|p6)&Xp9)|(!p6&X!p9&!p9))))&p5&G(Xp2|!p5)&!p13&!p12&!p11&G(Xp2|!p2)&!p9&!p8)
\ No newline at end of file

src/test/scala/de/tum/niwo/tests/papertests/CCSSubmissionTest.scala

@@ -45,6 +45,12 @@ class CCSSubmissionTest extends FlatSpec with LazyLogging {
     assert(checkTS(name, properties))
   }
 
+  it should "be proven safe with looping Bs" in {
+    val name = "tstests/leaderelection_inductive_withLoopB"
+
+    assert(checkTS(name, properties))
+  }
+
   "Easychair" should "prove stubborn conference" in {
     val name = "omitting/conference_stubborn"
     val inv = InvariantGenerator.invariantNoninterSingleBS _

src/test/scala/de/tum/niwo/tests/papertests/TSLeaderElectionTest.scala

@@ -26,10 +26,23 @@ class TSLeaderElectionTest extends FlatSpec {
     assert(check(name, properties))
   }
 
+  it should "be proven safe with universal Bs" in {
+    val name = "tstests/leaderelection_inductive_withB_uni"
+
+    assert(check(name, properties))
+  }
+
+
   it should "be proven safe with easier B" in {
     val name = "tstests/leaderelection_inductive_withB2"
 
     assert(check(name, properties))
   }
 
+  it should "be proven safe with negated B" in {
+    val name = "tstests/leaderelection_inductive_withNegB2"
+
+    assert(check(name, properties))
+  }
+
 }