1 |
b8dc00eb
|
bourbouh
|
|
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 |
|
|
node top (k0, m0: int; p, q : bool) returns (OK: bool);
|
11 |
2d37a1e1
|
ploc
|
--@ contract guarantees 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
|