lustrec / test / src / kind_fmcad08 / misc / durationThm_1.lus @ 22fe1c93
History | View | Annotate | Download (684 Bytes)
1 |
-- |
---|---|
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 |
var k,m : int; |
23 |
env : bool; |
24 |
let |
25 |
k = ik -> pre k; |
26 |
m = im -> pre m; |
27 |
env = Sofar((k>=1 and m>=1) and (Age(p)>=k => q) and (Age(q)>=m => r)); |
28 |
OK = env => (true -> ( (Age(p)>=k+m) => r )); |
29 |
--%PROPERTY OK=true; |
30 |
--%MAIN; |
31 |
tel |