## lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / misc / durationThm_3_e3_207.lus @ b745c1a8

History | View | Annotate | Download (507 Bytes)

1 | b8dc00eb | bourbouh | |
---|---|---|---|

2 | node Sofar( X : bool ) returns ( Sofar : bool ); |
||

3 | let |
||

4 | Sofar = X -> X and pre Sofar; |
||

5 | tel |
||

6 | node Age (p: bool) returns (age_of_p: int); |
||

7 | let |
||

8 | age_of_p = 0 -> if pre(p) then pre(age_of_p) - 1 else 0; |
||

9 | tel |
||

10 | node top (k0, m0: int; p, q : bool) returns (OK: bool); |
||

11 | bd3f748f | ploc | --@ contract guarantee OK; |

12 | b8dc00eb | bourbouh | var k,m: int; |

13 | env : bool; |
||

14 | let |
||

15 | k = k0-> pre(k); |
||

16 | m = m0-> pre(m); |
||

17 | env = Sofar( (k>=1 and m>=1) and (Age(p)>=k => q) and (Age(q)<= m) ); |
||

18 | OK = env => (Age(p) <= k+m); |
||

19 | --%MAIN; |
||

20 | --%PROPERTY OK=true; |
||

21 | tel |