lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / misc / ex8_e7_74.lus @ b745c1a8
History | View | Annotate | Download (804 Bytes)
1 | b8dc00eb | bourbouh | 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 or 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 | bd3f748f | ploc | --@ contract guarantee OK; |
24 | b8dc00eb | bourbouh | var late,early: bool; |
25 | let |
||
26 | (late,early) = speed(beacon,second); |
||
27 | OK = true -> not late and pre early; |
||
28 | --%MAIN; |
||
29 | --%PROPERTY OK=true; |
||
30 | tel |