X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/2be0e4648c5b7055580df1c265b7c43ee6763a46..0c13871d73e933c1847faf8debea7b7745a3ff44:/examples/msg/mc/promela_bugged2_liveness

diff --git a/examples/msg/mc/promela_bugged2_liveness b/examples/msg/mc/promela_bugged2_liveness
index 5d5edc9ddc..5361f88099 100644
--- a/examples/msg/mc/promela_bugged2_liveness
+++ b/examples/msg/mc/promela_bugged2_liveness
@@ -1,23 +1,12 @@
-never { /* !(GF((pready U produce) -> (cready U consume))) */
+never { /* !(!(GFcs)) */
 T0_init :    /* init */
 	if
-	:: (1) -> goto T1_S1
-	:: (produce && !consume) -> goto accept_S5
-	:: (pready && !consume) -> goto T0_S5
+	:: (cs) -> goto accept_S1
+	:: (1) -> goto T0_init
 	fi;
-T1_S1 :    /* 1 */
+accept_S1 :    /* 1 */
 	if
-	:: (1) -> goto T1_S1
-	:: (produce && !consume) || (pready && !consume) -> goto accept_S5
+	:: (cs) -> goto accept_S1
+	:: (1) -> goto T0_init
 	fi;
-accept_S5 :    /* 2 */
-	if
-	:: (pready && !consume) -> goto T0_S5
-	:: (produce && !consume) -> goto accept_S5
-	fi;
-T0_S5 :    /* 3 */
-	if
-	:: (pready && !consume) -> goto T0_S5
-	:: (produce && !consume) -> goto accept_S5
-	fi;
-}
\ No newline at end of file
+}