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