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 |