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

History | View | Annotate | Download (1.01 KB)

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

2 | -- Source Bertrand Jeannet, NBAC tutorial |
||

3 | -- |
||

4 | |||

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

6 | let |
||

7 | Sofar = X -> X and pre Sofar; |
||

8 | tel |
||

9 | |||

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

11 | let |
||

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

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

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

15 | tel |
||

16 | |||

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

18 | let |
||

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

20 | plus = speed <= 9; |
||

21 | minus = speed >= 11; |
||

22 | tel |
||

23 | |||

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

25 | var cpt: int; |
||

26 | acceptable: bool; |
||

27 | let |
||

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

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

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

31 | tel |
||

32 | |||

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

34 | var speed: int; |
||

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

36 | let |
||

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

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

39 | |||

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

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

42 | --%MAIN; |
||

43 | tel |