From 3f15bf3b50e2ff094894fea17c7cfb44cb98ab23 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Sun, 3 Jun 2012 09:46:45 +0200 Subject: [PATCH] model-checker : new properties in promela for centralized_liveness examples --- examples/msg/mc/promela2_centralized_liveness | 11 +++++++++++ examples/msg/mc/promela_centralized_liveness | 11 ++++++----- 2 files changed, 17 insertions(+), 5 deletions(-) create mode 100644 examples/msg/mc/promela2_centralized_liveness 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 +} -- 2.20.1