## lustrec / bench / distrib / misc / durationThm_1_e2_3 / conds / durationThm_1_e2_3.ec @ 43a2cae9

History | View | Annotate | Download (781 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 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 |

33 |