Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / misc / durationThm_1.lus @ 65f71d05

History | View | Annotate | Download (700 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
--@ ensures OK;
22
node top (ik, im: int; p, q, r : bool) returns (OK: bool);
23
var k,m : int;
24
    env : bool;
25
let
26
    k = ik -> pre k;
27
    m = im -> pre m;
28
    env = Sofar((k>=1 and m>=1) and (Age(p)>=k => q)  and (Age(q)>=m => r));
29
    OK = env => (true -> ( (Age(p)>=k+m) => r ));
30
    --%PROPERTY OK=true;
31
    --%MAIN;
32
tel