model checker : dfs algorithm corrected

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

diff --git a/examples/msg/mc/result_parse b/examples/msg/mc/result_parse
index 43f7fc5..92702b1 100644 (file)
--- a/examples/msg/mc/result_parse
+++ b/examples/msg/mc/result_parse
@@ -1,29 +1,17 @@
-never { /* []<>e->[](d-><>r) */
-
+never { /* !([]<>p->[](q-><>r)) */
 T0_init:
        if
-       :: (!d) || (r) -> goto accept_S1
-       :: (1) -> goto T1_S4
-       :: (1) -> goto T0_S2
-       :: (!e) -> goto accept_S3
+       :: (1) -> goto T0_init
+       :: (!r && q) -> goto T1_S4
        fi;
 T1_S4:
        if
-       :: (1) -> goto T1_S4
-       :: (r) -> goto accept_S1
+       :: (!r) -> goto T1_S4
+       :: (!r && p) -> goto accept_S4
        fi;
-accept_S1:
+accept_S4:
        if
-       :: (!d) || (r) -> goto accept_S1
-       :: (1) -> goto T1_S4
-       fi;
-T0_S2:
-       if
-       :: (1) -> goto T0_S2
-       :: (!e) -> goto accept_S3
-       fi;
-accept_S3:
-       if
-       :: (!e) -> goto accept_S3
+       :: (!r) -> goto T1_S4
+       :: (!r && p) -> goto accept_S4
        fi;
 }