lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / misc / ex8.lus @ 8aaf9f57
History | View | Annotate | Download (888 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 |
--@ ensures OK; |
25 |
node top(beacon,second:bool) returns (OK:bool); |
26 |
var late,early: bool; |
27 |
let |
28 |
(late,early) = speed(beacon,second); |
29 |
|
30 |
OK = true -> not late and pre early; |
31 |
|
32 |
--cannot go directly from early to late (valid) |
33 |
|
34 |
-- always was early and is not late; incorrect |
35 |
--%PROPERTY OK=true; |
36 |
|
37 |
tel |