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

History | View | Annotate | Download (1004 Bytes)

1 | |
---|---|

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 or 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 |
--@ contract guarantees OK; |

28 |
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 |