CristalCaveGem » LustreC » Lustrec-Tests

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

let

    Sofar = X -> X or pre Sofar;

tel

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

let

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

tel

node top (k0, m0: int; p, q : bool) returns (OK: bool);

--@ contract guarantees OK;

var k,m: int;

    env : bool;

let

    k = k0-> pre(k);

    m = m0-> pre(m);

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

    OK = env => (Age(p) <= k+m);

  --%MAIN;

  --%PROPERTY  OK=true;

tel