lustrec / bench / distrib / misc / durationThm_1_e1_350 / mutants / durationThm_1_e1_350.mutant.n100.lus @ 43a2cae9
History | View | Annotate | Download (799 Bytes)
1 |
node top |
---|---|
2 |
(ik: int; |
3 |
im: int; |
4 |
p: bool; |
5 |
q: bool; |
6 |
r: bool) |
7 |
returns |
8 |
(OK: bool); |
9 |
|
10 |
var |
11 |
V14_k: int; |
12 |
V15_m: int; |
13 |
V16_env: bool; |
14 |
V45_age_of_p: int; |
15 |
V52_age_of_p: int; |
16 |
V55_X: bool; |
17 |
V68_age_of_p: int; |
18 |
|
19 |
let |
20 |
OK = (V16_env => (true -> ((V68_age_of_p >= (V14_k + V15_m)) => r))); |
21 |
V14_k = (ik -> (pre V14_k)); |
22 |
V15_m = (im -> (pre V15_m)); |
23 |
V16_env = (V55_X -> (V55_X and (pre V16_env))); |
24 |
V45_age_of_p = (0 -> (if (pre p) then (((pre (pre V45_age_of_p)) + 1) + 1) |
25 |
else 0)); |
26 |
V52_age_of_p = (0 -> (if (pre q) then (((pre (pre V52_age_of_p)) + 1) + 1) |
27 |
else 0)); |
28 |
V55_X = ((((V14_k >= 1) and (V15_m >= 1)) and ((V45_age_of_p >= V14_k) => q)) |
29 |
and ((V52_age_of_p >= V15_m) => r)); |
30 |
V68_age_of_p = (0 -> (if (pre p) then (((pre (pre V68_age_of_p)) + 1) + 1) |
31 |
else 0)); |
32 |
tel |
33 |
|