model-checker : cleanup in mc examples

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

diff --git a/examples/msg/mc/promela2_bugged2_liveness b/examples/msg/mc/promela2_bugged2_liveness
deleted file mode 100644 (file)
index 1b4359d..0000000
--- a/examples/msg/mc/promela2_bugged2_liveness
+++ /dev/null
@@ -1,17 +0,0 @@
-never { /* !(G((pready U produce) -> F(cready U consume))) */
-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;
-}