lustrec / test / src / kind_fmcad08 / misc / traffic_e7_46.lus @ 0cbf0839
History | View | Annotate | Download (513 Bytes)
1 |
|
---|---|
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 and 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 |