CristalCaveGem » LustreC » Lustrec-Tests

-- Source: Bertrand Jeannet

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

let

    Sofar = X -> X and pre Sofar;

tel

-- Counts the number of steps P has been continuously true

node Age(P1: bool) returns (Count:int);

let

  Count = 0 -> if pre(P1) then pre(Count)+1 else 0;             

tel 

-- Counts the number of time Q has been true 

-- since P has became false

node Dursince(P1,Q:bool) returns (Count:int);

let

  Count = 0 -> 

	if pre(P1) 

	then 0

        else (if pre(Q) then pre(Count)+1 else pre(Count));

tel

node RaisingEdge(P1 : bool) returns (res : bool);

let

  res = false -> not pre(P1) and P1;

tel

-- original version

-- leak is an input indicating a leak

-- P is a an input used to define the start of an observation

-- Not provable?

node top (leak,P1:bool) returns (OK : bool);

--@ contract guarantees OK;

   var env : bool;

let

 -- we suppose that a leak lasts at most 10 steps,

 -- and that a raising edge of P implies

 -- no leak has happened since at least 300 steps.

    env = Sofar( Age(leak) <= 10) and

                 (not RaisingEdge(P1) or (300 <= Age(not leak)) );

     OK = env => ( (Age(not P1) <= 600) or

                   (2*Dursince(P1,leak) <= Age(not P1)));

     --%PROPERTY OK=true;

     --%MAIN;

 tel