## lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / simulation / Gas.lus @ 2d37a1e1

History | View | Annotate | Download (1.22 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 |
--@ contract guarantees OK; |

39 |
var env : bool; |

40 |
let |

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

42 |
-- and that a raising edge of P implies |

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

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

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

46 | |

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

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

49 |
--%PROPERTY OK=true; |

50 |
--%MAIN; |

51 |
tel |