lustrec / test / src / kind_fmcad08 / misc / durationThm_3_e7_334.lus @ 65f71d05
History | View | Annotate | Download (495 Bytes)
1 |
|
---|---|
2 |
node Sofar( X : bool ) returns ( Sofar : bool ); |
3 |
let |
4 |
Sofar = X -> X or 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 |
--@ ensures OK; |
11 |
node top (k0, m0: int; p, q : bool) returns (OK: bool); |
12 |
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 |