From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Sun, 3 Jun 2012 07:46:45 +0000 (+0200)
Subject: model-checker : new properties in promela for centralized_liveness examples
X-Git-Tag: v3_8~649
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/3f15bf3b50e2ff094894fea17c7cfb44cb98ab23

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
index 0000000000..94bbde252e
--- /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 c5169d114f..5361f88099 100644
--- 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
+}