lustrec / test / src / kind_fmcad08 / simulation / speed2_e7_223_e8_329.lus @ 0cbf0839
History | View | Annotate | Download (776 Bytes)
1 |
node COUNTER(init,incr:int;X,reset:bool) returns (C:int); |
---|---|
2 |
var PC: int; |
3 |
let |
4 |
PC = init -> pre C; |
5 |
C = if reset then init |
6 |
else if X then (PC+incr) |
7 |
else PC; |
8 |
tel |
9 |
node speed(beacon,second:bool) returns (late,early:bool); |
10 |
var |
11 |
diff,incr:int; |
12 |
let |
13 |
incr = if (beacon and not second) then 1 |
14 |
else if (second and not beacon) then 2 |
15 |
else 0; |
16 |
diff = COUNTER(0,incr,(beacon or second),false); |
17 |
early = false -> if pre early then (diff > 0) |
18 |
else (diff >= 10); |
19 |
late = false -> if pre late then (diff < 0) |
20 |
else (diff <= -10); |
21 |
tel |
22 |
node top(beacon,second:bool) returns (OK:bool); |
23 |
var late,early: bool; |
24 |
let |
25 |
(late,early) = speed(beacon,second); |
26 |
OK = true -> not pre early or not late; |
27 |
--%MAIN; |
28 |
--%PROPERTY OK; |
29 |
tel |