Revision 2d37a1e1 regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_17.lus
regression_tests/lustre_files/success/kind_fmcad08/large/cruise_controller_17.lus | ||
---|---|---|
1 | 1 |
|
2 | 2 |
|
3 |
--@ ensures OK; |
|
4 | 3 |
node top(onOff: bool; |
5 | 4 |
decelSet: bool; |
6 | 5 |
accelResume: bool; |
... | ... | |
11 | 10 |
validInputs: bool) |
12 | 11 |
returns (OK:bool); |
13 | 12 |
|
13 |
--@ contract guarantees OK; |
|
14 | 14 |
var |
15 | 15 |
mode: int; |
16 | 16 |
cruiseThrottle: real; |
Also available in: Unified diff