Revision 2d37a1e1
Added by Pierre-Loïc Garoche over 6 years ago
| regression_tests/lustre_files/success/kind_fmcad08/memory2/MOESI_2_e8_926_e2_349.lus | ||
|---|---|---|
| 48 | 48 |
if(etat_mo4) then if(garde_mo4) then 0 else pre owned_mo else |
| 49 | 49 |
pre owned_mo; |
| 50 | 50 |
tel |
| 51 |
--@ ensures OK; |
|
| 52 | 51 |
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool ) |
| 53 | 52 |
returns ( OK : bool ); |
| 53 |
--@ contract guarantees OK; |
|
| 54 | 54 |
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int; |
| 55 | 55 |
erreur_mo : bool; |
| 56 | 56 |
env : bool; |
Also available in: Unified diff
Renaminig lustre contracts from ensures to guarantees
Will require the latest cocospec branch to compile (before it is integrated in the unstable/master branches)