Revision 2d37a1e1 regression_tests/lustre_files/success/kind_fmcad08/simulation/speed_e8_649.lus
regression_tests/lustre_files/success/kind_fmcad08/simulation/speed_e8_649.lus | ||
---|---|---|
19 | 19 |
late = false -> if pre late then (diff < 0) |
20 | 20 |
else (diff <= -10); |
21 | 21 |
tel |
22 |
--@ ensures OK; |
|
23 | 22 |
node top(beacon,second:bool) returns (OK:bool); |
23 |
--@ contract guarantees OK; |
|
24 | 24 |
var late,early: bool; |
25 | 25 |
let |
26 | 26 |
OK = not (late and early); |
Also available in: Unified diff