lustrec / test / src / kind_fmcad08 / misc / ex3.lus @ 0cbf0839
History | View | Annotate | Download (876 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 |
|
10 |
node speed(beacon,second:bool) returns (late,early:bool); |
11 |
var |
12 |
diff,incr:int; |
13 |
let |
14 |
incr = if (beacon and not second) then 1 |
15 |
else if (second and not beacon) then 2 |
16 |
else 0; |
17 |
diff = COUNTER(0,incr,(beacon or second),false); |
18 |
early = false -> if pre early then (diff > 0) |
19 |
else (diff >= 10); |
20 |
late = false -> if pre late then (diff < 0) |
21 |
else (diff <= -10); |
22 |
tel |
23 |
|
24 |
node top(beacon,second:bool) returns (OK:bool); |
25 |
var late,early: bool; |
26 |
let |
27 |
(late,early) = speed(beacon,second); |
28 |
|
29 |
OK = true -> not pre early or not late; |
30 |
|
31 |
--cannot go directly from early to late (valid) |
32 |
|
33 |
-- if was early, will not next be late; correct |
34 |
--%PROPERTY OK=true; |
35 |
tel |