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