From a941e1f7d2bca6b2e3ef7f83b954d26f990cd9a6 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 10 Jan 2012 13:07:48 +0100 Subject: [PATCH] model-checker : new LTL property for bugged2_liveness example --- examples/msg/mc/promela2_bugged2_liveness | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 examples/msg/mc/promela2_bugged2_liveness 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; +} -- 2.20.1