## lustrec / bench / distrib / misc / durationThm_1_e1_350 / mutants / durationThm_1_e1_350.mutant.n49.lus @ 43a2cae9

History | View | Annotate | Download (781 Bytes)

1 | 43a2cae9 | ploc | 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 V45_age_of_p) + 1) - 1) else 0)) |
||

25 | ; |
||

26 | V52_age_of_p = (0 -> (if (pre q) then (((pre V52_age_of_p) + 1) - 1) else 0)) |
||

27 | ; |
||

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 V68_age_of_p) + 1) - 1) else 0)) |
||

31 | ; |
||

32 | tel |