model-checker : new examples for verification of liveness properties

[simgrid.git] / examples / msg / mc / promela1_bugged1_liveness

diff --git a/examples/msg/mc/automaton2_PROMELA b/examples/msg/mc/promela1_bugged1_liveness
similarity index 50%
rename from examples/msg/mc/automaton2_PROMELA
rename to examples/msg/mc/promela1_bugged1_liveness
index ba1afda..96b491d 100644 (file)
--- a/examples/msg/mc/automaton2_PROMELA
+++ b/examples/msg/mc/promela1_bugged1_liveness
@@ -1,11 +1,11 @@
-never { /* !G(p->Fq) */
+never { /* !G(r->Fcs) */
 T0_init :    /* init */
        if
        :: (1) -> goto T0_init
-       :: (!q && p) -> goto accept_S2
+       :: (!cs && r) -> goto accept_S2
        fi;
 accept_S2 :    /* 1 */
        if
-       :: (!q) -> goto accept_S2
+       :: (!cs) -> goto accept_S2
        fi;
-}
\ No newline at end of file
+}