lustrec / test / src / kind_fmcad08 / simulation / Gas.lus @ 22fe1c93
History | View | Annotate | Download (1.19 KB)
1 |
|
---|---|
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 |
-- Counts the number of steps P has been continuously true |
11 |
node Age(P1: bool) returns (Count:int); |
12 |
let |
13 |
Count = 0 -> if pre(P1) then pre(Count)+1 else 0; |
14 |
tel |
15 |
|
16 |
-- Counts the number of time Q has been true |
17 |
-- since P has became false |
18 |
node Dursince(P1,Q:bool) returns (Count:int); |
19 |
let |
20 |
Count = 0 -> |
21 |
if pre(P1) |
22 |
then 0 |
23 |
else (if pre(Q) then pre(Count)+1 else pre(Count)); |
24 |
tel |
25 |
|
26 |
node RaisingEdge(P1 : bool) returns (res : bool); |
27 |
let |
28 |
res = false -> not pre(P1) and P1; |
29 |
tel |
30 |
|
31 |
-- original version |
32 |
|
33 |
-- leak is an input indicating a leak |
34 |
-- P is a an input used to define the start of an observation |
35 |
|
36 |
-- Not provable? |
37 |
node top (leak,P1:bool) returns (OK : bool); |
38 |
var env : bool; |
39 |
let |
40 |
-- we suppose that a leak lasts at most 10 steps, |
41 |
-- and that a raising edge of P implies |
42 |
-- no leak has happened since at least 300 steps. |
43 |
env = Sofar( Age(leak) <= 10) and |
44 |
(not RaisingEdge(P1) or (300 <= Age(not leak)) ); |
45 |
|
46 |
OK = env => ( (Age(not P1) <= 600) or |
47 |
(2*Dursince(P1,leak) <= Age(not P1))); |
48 |
--%PROPERTY OK=true; |
49 |
--%MAIN; |
50 |
tel |