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

History | View | Annotate | Download (1.19 KB)

1 | 22fe1c93 | ploc | |
---|---|---|---|

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 |