Revision 2d37a1e1
Added by Pierre-Loïc Garoche over 6 years ago
| regression_tests/lustre_files/success/kind_fmcad08/simulation/ums_e7_1700.lus | ||
|---|---|---|
| 41 | 41 |
empty_section = not(on_A or on_B or on_C); |
| 42 | 42 |
only_on_B = on_B and not(on_A or on_C); |
| 43 | 43 |
tel |
| 44 |
--@ ensures OK; |
|
| 45 | 44 |
node top(on_A, on_B, on_C, ack_AB, ack_BC: bool) |
| 46 | 45 |
returns(OK: bool); |
| 46 |
--@ contract guarantees OK; |
|
| 47 | 47 |
var |
| 48 | 48 |
grant_access, grant_exit: bool; |
| 49 | 49 |
do_AB, do_BC: bool; |
Also available in: Unified diff
Renaminig lustre contracts from ensures to guarantees
Will require the latest cocospec branch to compile (before it is integrated in the unstable/master branches)