Revision 2d37a1e1
Added by Pierre-Loïc Garoche over 6 years ago
| regression_tests/lustre_files/success/kind_fmcad08/simulation/metros_1_e1_846_e3_1060.lus | ||
|---|---|---|
| 38 | 38 |
(diff1,avance1,retard1) = controleur(nB1,nS); |
| 39 | 39 |
ast = H0 and H1; |
| 40 | 40 |
tel |
| 41 |
--@ ensures OK; |
|
| 42 | 41 |
node top(B0, B1 : bool; S : bool) |
| 43 | 42 |
returns (OK:bool); |
| 43 |
--@ contract guarantees OK; |
|
| 44 | 44 |
var nB0, nB1 : int; |
| 45 | 45 |
nS : int; |
| 46 | 46 |
diff0, diff1 :int; |
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)