Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / misc / durationThm_2_e7_145_e8_73.lus @ 22fe1c93

History | View | Annotate | Download (470 Bytes)

1

    
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: int; p, q, r, t : bool) returns (OK: bool);
11
var k: int;
12
    env : bool;
13
let
14
    k = k0-> pre(k);
15
    env = Sofar((k>=1) and (Age(p)>=k => q)  and (Age(r)>=k => t));
16
    OK = env => ((Age(p and r)>=k) => (q and t));
17
  --%MAIN;
18
  --%PROPERTY  OK=true;
19
tel