model-checker : create mc directory in smpi examples and add new example for liveness...

[simgrid.git] / examples / smpi / mc / promela_bugged1_liveness

diff --git a/examples/smpi/mc/promela_bugged1_liveness b/examples/smpi/mc/promela_bugged1_liveness
new file mode 100644 (file)
index 0000000..96b491d
--- /dev/null
+++ b/examples/smpi/mc/promela_bugged1_liveness
@@ -0,0 +1,11 @@
+never { /* !G(r->Fcs) */
+T0_init :    /* init */
+       if
+       :: (1) -> goto T0_init
+       :: (!cs && r) -> goto accept_S2
+       fi;
+accept_S2 :    /* 1 */
+       if
+       :: (!cs) -> goto accept_S2
+       fi;
+}