## lustrec / test / src / kind_fmcad08 / misc / traffic_e7_46_e7_171.lus @ 22fe1c93

History | View | Annotate | Download (512 Bytes)

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

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

3 | let |
||

4 | Y = (true -> pre Y) or X; |
||

5 | tel |
||

6 | node Store( Delta : int ) returns ( Total : int ); |
||

7 | var Prev : int; |
||

8 | let |
||

9 | Prev = 0 -> pre Total; |
||

10 | Total = if Delta < 0 or Prev > 0 then Prev+Delta |
||

11 | else if Delta > 0 and Prev < 10 then Prev+Delta |
||

12 | else Prev; |
||

13 | tel |
||

14 | node top( Delta : int ) returns ( OK : bool ); |
||

15 | var Total : int; |
||

16 | let |
||

17 | Total = Store( Delta ); |
||

18 | OK = Sofar( -1 <= Delta and Delta <= 1 ) => 0 <= Total and Total <= 20; |
||

19 | --%MAIN; |
||

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

21 | tel |