Revision 2d37a1e1 regression_tests/lustre_files/success/kind_fmcad08/simulation/PRODUCER_CONSUMER_vt.lus
regression_tests/lustre_files/success/kind_fmcad08/simulation/PRODUCER_CONSUMER_vt.lus | ||
---|---|---|
48 | 48 |
|
49 | 49 |
tel |
50 | 50 |
|
51 |
--@ ensures OK; |
|
52 | 51 |
node top(etat1, etat2, etat3 : bool; a_init : int) returns ( OK : bool ); |
52 |
--@ contract guarantees OK; |
|
53 | 53 |
var i, b, a, o1, o2 : int; |
54 | 54 |
env : bool; |
55 | 55 |
let |
Also available in: Unified diff