model-checker : new LTL property for bugged2_liveness example

diff --git a/examples/msg/mc/promela2_bugged2_liveness b/examples/msg/mc/promela2_bugged2_liveness
new file mode 100644 (file)
index 0000000..880cfea
--- /dev/null
+++ b/examples/msg/mc/promela2_bugged2_liveness
@@ -0,0 +1,17 @@
+never { /* !(G((pready U produce) -> Fconsume)) */
+T1_init :    /* init */
+       if
+       :: (1) -> goto T1_init
+       :: (pready && !consume) -> goto T0_S2
+       :: (produce && !consume) -> goto accept_S3
+       fi;
+T0_S2 :    /* 1 */
+       if
+       :: (pready && !consume) -> goto T0_S2
+       :: (produce && !consume) -> goto accept_S3
+       fi;
+accept_S3 :    /* 2 */
+       if
+       :: (!consume) -> goto accept_S3
+       fi;
+}