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