## lustrec / bench / distrib / misc / durationThm_1_e7_217_e7_31 / durationThm_1_e7_217_e7_31.lus_top_flatten.lus @ 43a2cae9

History | View | Annotate | Download (752 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 or (pre V16_env))); |

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

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

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

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

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

29 |
tel |

30 |