model-checker : bugged2_liveness with promela of LTL properties checked

[simgrid.git] / examples / msg / mc / promela2_bugged2_liveness

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