Revision 2d37a1e1 regression_tests/lustre_files/success/kind_fmcad08/simulation/PRODUCER_CONSUMER_vt_e2_1352.lus
| regression_tests/lustre_files/success/kind_fmcad08/simulation/PRODUCER_CONSUMER_vt_e2_1352.lus | ||
|---|---|---|
| 37 | 37 |
if(etat3) then if(garde3) then pre o2+1 else pre o2 else |
| 38 | 38 |
pre o2; |
| 39 | 39 |
tel |
| 40 |
--@ ensures OK; |
|
| 41 | 40 |
node top(etat1, etat2, etat3 : bool; a_init : int) returns ( OK : bool ); |
| 41 |
--@ contract guarantees OK; |
|
| 42 | 42 |
var i, b, a, o1, o2 : int; |
| 43 | 43 |
env : bool; |
| 44 | 44 |
let |
Also available in: Unified diff