## lustrec / test / src / kind_fmcad08 / simulation / cd.lus @ 0cbf0839

History | View | Annotate | Download (1.01 KB)

1 |
-- |
---|---|

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 |