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

History | View | Annotate | Download (1005 Bytes)

1 | b8dc00eb | bourbouh | |
---|---|---|---|

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

3 | let |
||

4 | Sofar = X -> X or pre Sofar; |
||

5 | tel |
||

6 | node Environment(diff: int; plus,minus: bool) returns (ok: bool); |
||

7 | let |
||

8 | ok = (-4 <= diff and diff <= 4) and |
||

9 | (if (true -> pre plus) then diff >= 1 else true) and |
||

10 | (if (false -> pre minus) then diff <= -1 else true); |
||

11 | tel |
||

12 | node Controller(diff: int) returns (speed: int; plus,minus: bool); |
||

13 | let |
||

14 | speed = 0 -> pre(speed)+diff; |
||

15 | plus = speed <= 9; |
||

16 | minus = speed >= 11; |
||

17 | tel |
||

18 | node Property(speed: int) returns (ok: bool); |
||

19 | var cpt: int; |
||

20 | acceptable: bool; |
||

21 | let |
||

22 | acceptable = 8 <= speed and speed <= 12; |
||

23 | cpt = 0 -> if acceptable then 0 else pre(cpt)+1; |
||

24 | ok = true -> (pre cpt<=7); |
||

25 | tel |
||

26 | node top(diff:int) returns (OK: bool); |
||

27 | 2d37a1e1 | ploc | --@ contract guarantees OK; |

28 | b8dc00eb | bourbouh | var speed: int; |

29 | plus,minus,realistic: bool; |
||

30 | let |
||

31 | (speed,plus,minus) = Controller(diff); |
||

32 | realistic = Environment(diff,plus,minus); |
||

33 | OK = Sofar( realistic and 0 <= speed and speed < 16 ) => Property(speed); |
||

34 | --%MAIN; |
||

35 | --%PROPERTY OK=true; |
||

36 | tel |