### Profile

Statistics
| Branch: | Tag: | Revision:

## lustrec / test / src / kind_fmcad08 / simulation / Gas.lus @ 22fe1c93

1 2 3 22fe1c93 ploc ```-- 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); ``` ``` 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`