model-checker : bugged2_liveness with promela of LTL properties checked

diff --git a/examples/msg/mc/bugged2_liveness.c b/examples/msg/mc/bugged2_liveness.c
index 4ab7ab2..305771f 100644 (file)
--- 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                  */
 /***************** 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 880cfea..1b4359d 100644 (file)
--- 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
 T1_init :    /* init */
        if
        :: (1) -> goto T1_init