## lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / misc / durationThm_1.lus @ 2d37a1e1

History | View | Annotate | Download (712 Bytes)

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

2 | -- Source: Bertrand Jeannet |
||

3 | -- |
||

4 | |||

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

6 | let |
||

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

8 | tel |
||

9 | |||

10 | |||

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

12 | -- how long has p been maintained true in the strict past |
||

13 | let |
||

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

15 | tel |
||

16 | |||

17 | -- Theorem 1: |
||

18 | -- (p -k-> q and q -m-> r) => p -k+m-> r |
||

19 | |||

20 | -- Not provable in luke-* |
||

21 | node top (ik, im: int; p, q, r : bool) returns (OK: bool); |
||

22 | 2d37a1e1 | ploc | --@ contract guarantees OK; |

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

24 | env : bool; |
||

25 | let |
||

26 | k = ik -> pre k; |
||

27 | m = im -> pre m; |
||

28 | env = Sofar((k>=1 and m>=1) and (Age(p)>=k => q) and (Age(q)>=m => r)); |
||

29 | OK = env => (true -> ( (Age(p)>=k+m) => r )); |
||

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

31 | --%MAIN; |
||

32 | tel |