## lustrec / bench / distrib / misc / durationThm_1_e3_389_e4_294 / mutants / durationThm_1_e3_389_e4_294.mutant.n56.lus @ 43a2cae9

History | View | Annotate | Download (833 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 |
V60_Sofar: bool; |

18 |
V68_age_of_p: int; |

19 | |

20 |
let |

21 |
OK = (V16_env => (true -> ((V68_age_of_p >= (V14_k + V15_m)) => r))); |

22 |
V14_k = (ik -> (pre V14_k)); |

23 |
V15_m = (im -> (pre V15_m)); |

24 |
V16_env = (not V60_Sofar); |

25 |
V45_age_of_p = (0 -> (if (pre p) then (((pre V45_age_of_p) + 1) - 1) else 0)) |

26 |
; |

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

28 |
; |

29 |
V55_X = ((((V14_k >= 1) and (V15_m >= 1)) and ((V45_age_of_p >= V14_k) => q)) |

30 |
and ((V52_age_of_p >= V15_m) => r)); |

31 |
V60_Sofar = (V55_X -> (V55_X and (pre V60_Sofar))); |

32 |
V68_age_of_p = (0 -> (if (pre p) then (((pre V68_age_of_p) + 1) - 1) else 0)) |

33 |
; |

34 |
tel |

35 |