From 1817e908617a7ac2fd9cd68dc222117c368477a1 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 10 Jan 2012 13:37:17 +0100 Subject: [PATCH 1/1] model-checker : bugged2_liveness with promela of LTL properties checked --- examples/msg/mc/bugged2_liveness.c | 3 --- examples/msg/mc/promela2_bugged2_liveness | 2 +- 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/examples/msg/mc/bugged2_liveness.c b/examples/msg/mc/bugged2_liveness.c index 4ab7ab2514..305771fbdc 100644 --- a/examples/msg/mc/bugged2_liveness.c +++ b/examples/msg/mc/bugged2_liveness.c @@ -1,9 +1,6 @@ /***************** Producer/Consumer Algorithm *************************/ /* This example implements a producer/consumer algorithm. */ /* If consumer work before producer, message is empty */ -/* LTL property checked : GF((pready U produce) -> (cready U consume)) */ -/* (pready = producer got CS, produce=message pushed in the buffer) */ -/* (cready = consumer got CS, consume=message display by consumer) */ /***********************************************************************/ diff --git a/examples/msg/mc/promela2_bugged2_liveness b/examples/msg/mc/promela2_bugged2_liveness index 880cfeaf1f..1b4359d9f6 100644 --- a/examples/msg/mc/promela2_bugged2_liveness +++ b/examples/msg/mc/promela2_bugged2_liveness @@ -1,4 +1,4 @@ -never { /* !(G((pready U produce) -> Fconsume)) */ +never { /* !(G((pready U produce) -> F(cready U consume))) */ T1_init : /* init */ if :: (1) -> goto T1_init -- 2.20.1