From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Tue, 10 Jan 2012 12:07:48 +0000 (+0100)
Subject: model-checker : new LTL property for bugged2_liveness example
X-Git-Tag: exp_20120216~133^2~8
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/a941e1f7d2bca6b2e3ef7f83b954d26f990cd9a6

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
index 0000000000..880cfeaf1f
--- /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;
+}