CristalCaveGem » LustreC

--

-- Source: Bertrand Jeannet

--

node Sofar( X : bool ) returns ( Sofar : bool );

let

    Sofar = X -> X and pre Sofar;

tel

node Age (p: bool) returns (age_of_p: int);

-- how long has p been maintained true in the strict past

let

 age_of_p = 0 -> if pre(p) then pre(age_of_p) + 1 else 0;

tel

-- Theorem 1:

-- (p -k-> q and q -m-> r) => p -k+m-> r

-- Not provable in luke-*

node top (ik, im: int; p, q, r : bool) returns (OK: bool);

var k,m : int;

    env : bool;

let

    k = ik -> pre k;

    m = im -> pre m;

    env = Sofar((k>=1 and m>=1) and (Age(p)>=k => q)  and (Age(q)>=m => r));

    OK = env => (true -> ( (Age(p)>=k+m) => r ));

    --%PROPERTY OK=true;

    --%MAIN;

tel