lustrec / test / src / kind_fmcad08 / simulation / cd_e7_8.lus @ 22fe1c93
History | View | Annotate | Download (977 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 and 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 |
var speed: int; |
28 |
plus,minus,realistic: bool; |
29 |
let |
30 |
(speed,plus,minus) = Controller(diff); |
31 |
realistic = Environment(diff,plus,minus); |
32 |
OK = Sofar( realistic and 0 <= speed and speed < 16 ) => Property(speed); |
33 |
--%MAIN; |
34 |
--%PROPERTY OK=true; |
35 |
tel |