model-checker : new properties in promela for centralized_liveness examples

diff --git a/examples/msg/mc/promela2_centralized_liveness b/examples/msg/mc/promela2_centralized_liveness
new file mode 100644 (file)
index 0000000..94bbde2
--- /dev/null
+++ b/examples/msg/mc/promela2_centralized_liveness
@@ -0,0 +1,11 @@
+never { /* !(GFcs) */
+T0_init :    /* init */
+       if
+       :: (1) -> goto T0_init
+       :: (!cs) -> goto accept_S2
+       fi;
+accept_S2 :    /* 1 */
+       if
+       :: (!cs) -> goto accept_S2
+       fi;
+}

diff --git a/examples/msg/mc/promela_centralized_liveness b/examples/msg/mc/promela_centralized_liveness
index c5169d1..5361f88 100644 (file)
--- a/examples/msg/mc/promela_centralized_liveness
+++ b/examples/msg/mc/promela_centralized_liveness
@@ -1,11 +1,12 @@
-never { /* !(GFcs2) */
+never { /* !(!(GFcs)) */
 T0_init :    /* init */
        if
+       :: (cs) -> goto accept_S1
        :: (1) -> goto T0_init
-       :: (!cs2) -> goto accept_S2
        fi;
-accept_S2 :    /* 1 */
+accept_S1 :    /* 1 */
        if
-       :: (!cs2) -> goto accept_S2
+       :: (cs) -> goto accept_S1
+       :: (1) -> goto T0_init
        fi;
-}
\ No newline at end of file
+}