Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / misc / durationThm_1_e7_217.lus @ b745c1a8

History | View | Annotate | Download (530 Bytes)

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 (ik, im: int; p, q, r : bool) returns (OK: bool);
11 bd3f748f ploc
--@ contract guarantee OK;
12 b8dc00eb bourbouh
var k,m : int;
13
    env : bool;
14
let
15
    k = ik -> pre k;
16
    m = im -> pre m;
17
    env = Sofar((k>=1 and m>=1) and (Age(p)>=k => q)  and (Age(q)>=m => r));
18
    OK = env => (true -> ( (Age(p)>=k+m) => r ));
19
  --%MAIN;
20
  --%PROPERTY  OK=true;
21
tel