A
lgorithmique
N
umérique
D
istribuée
Public GIT Repository
projects
/
simgrid.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
model-checker : DPOR (independant transitions) algorithm for liveness properties
[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
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
fi;
T1_S4:
if
- :: (
1
) -> goto T1_S4
- :: (
r) -> goto accept_S1
+ :: (
!r
) -> goto T1_S4
+ :: (
!r && p) -> goto accept_S4
fi;
fi;
-accept_S
1
:
+accept_S
4
:
if
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;
}
fi;
}