Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (690 Bytes)

1 22fe1c93 ploc
--
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 5:
18
-- ((p -k-> q and ([[q]] => length <= m))  => ([[p]] => length <= k+m)
19
20
-- Not provable in luke-*
21
node top (k0, m0: int; p, q : bool) returns (OK: bool);
22
var k,m: int;
23
    env : bool;
24
let
25
    k = k0-> pre(k);
26
    m = m0-> pre(m);
27
    env = Sofar( (k>=1 and m>=1) and (Age(p)>=k => q) and (Age(q)<= m) );
28
    OK = env => (Age(p) <= k+m);
29
    --%PROPERTY OK=true;
30
    --%MAIN;
31
tel