Revision 2d37a1e1 regression_tests/lustre_files/success/kind_fmcad08/memory2/MESI_i4_e4_1689.lus
regression_tests/lustre_files/success/kind_fmcad08/memory2/MESI_i4_e4_1689.lus | ||
---|---|---|
45 | 45 |
if(etat_me4) then if(garde_me4) then pre invalid_me + pre modified_me + pre exclusive_me + pre shared_me -1 else pre invalid_me else |
46 | 46 |
pre invalid_me; |
47 | 47 |
tel |
48 |
--@ ensures OK; |
|
49 | 48 |
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool ); |
49 |
--@ contract guarantees OK; |
|
50 | 50 |
var modified_me, exclusive_me, shared_me, invalid_me : int; |
51 | 51 |
env : bool; |
52 | 52 |
let |
Also available in: Unified diff