diff --git a/examples/tests/leaderelection_withB.spec b/examples/tests/leaderelection_withB.spec index 2bfe5fe672b6b91bb2fee1f66ddf61e6d63fb3e6..dd53f1481d80ee212607552b1d101b48ce799d2e 100644 --- a/examples/tests/leaderelection_withB.spec +++ b/examples/tests/leaderelection_withB.spec @@ -1,12 +1,12 @@ 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 diff --git a/examples/tstests/leaderelection_inductive_withB2.spec b/examples/tstests/leaderelection_inductive_withB2.spec index 6a8b657da747c8c087deb763245329c1ccefa300..e387118d30fb790fa135c4cd22449fc2b09e2deb 100644 --- a/examples/tstests/leaderelection_inductive_withB2.spec +++ b/examples/tstests/leaderelection_inductive_withB2.spec @@ -1,22 +1,22 @@ 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), diff --git a/examples/tstests/leaderelection_inductive_withB_uni.spec b/examples/tstests/leaderelection_inductive_withB_uni.spec new file mode 100644 index 0000000000000000000000000000000000000000..08a672c18d1aa6698df4816dda9aced14563de10 --- /dev/null +++ b/examples/tstests/leaderelection_inductive_withB_uni.spec @@ -0,0 +1,32 @@ +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))) diff --git a/examples/tstests/leaderelection_inductive_withLoopB.spec b/examples/tstests/leaderelection_inductive_withLoopB.spec new file mode 100644 index 0000000000000000000000000000000000000000..7782d377da911530a7a8b11284365e163ae0a050 --- /dev/null +++ b/examples/tstests/leaderelection_inductive_withLoopB.spec @@ -0,0 +1,32 @@ +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))) diff --git a/examples/tstests/leaderelection_inductive_withNegB2.spec b/examples/tstests/leaderelection_inductive_withNegB2.spec new file mode 100644 index 0000000000000000000000000000000000000000..e387118d30fb790fa135c4cd22449fc2b09e2deb --- /dev/null +++ b/examples/tstests/leaderelection_inductive_withNegB2.spec @@ -0,0 +1,32 @@ +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))) diff --git a/results/tests/simpleChoice_stubborn/tests/simpleChoice_stubborn.owlltl b/results/tests/simpleChoice_stubborn/tests/simpleChoice_stubborn.owlltl index c2a9e9ca7cbab2ef61e8bd3712463a6c0b89ce92..39b6c1a3407d7cb50ee1842479f4df484a7c0c4e 100644 --- a/results/tests/simpleChoice_stubborn/tests/simpleChoice_stubborn.owlltl +++ b/results/tests/simpleChoice_stubborn/tests/simpleChoice_stubborn.owlltl @@ -1 +1 @@ -((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 diff --git a/src/test/scala/de/tum/niwo/tests/papertests/CCSSubmissionTest.scala b/src/test/scala/de/tum/niwo/tests/papertests/CCSSubmissionTest.scala index 3946a20933f1e011d579f263b134a28a6c33966a..846151403f1aa58682994a50b71739505521a2da 100644 --- a/src/test/scala/de/tum/niwo/tests/papertests/CCSSubmissionTest.scala +++ b/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 _ diff --git a/src/test/scala/de/tum/niwo/tests/papertests/TSLeaderElectionTest.scala b/src/test/scala/de/tum/niwo/tests/papertests/TSLeaderElectionTest.scala index 4c724647137f0a04f3e692d7be37851b97506da3..3383b8b30c89db14afd9c1cb28fb1fed4c836f6f 100644 --- a/src/test/scala/de/tum/niwo/tests/papertests/TSLeaderElectionTest.scala +++ b/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)) + } + }