| 1 |
b8dc00eb
|
bourbouh
|
|
| 2 |
|
|
node Sofar( X : bool ) returns ( Sofar : bool );
|
| 3 |
|
|
let
|
| 4 |
|
|
Sofar = X -> X and pre Sofar;
|
| 5 |
|
|
tel
|
| 6 |
|
|
node excludes4( X1, X2, X3, X4 : bool ) returns ( excludes : bool );
|
| 7 |
|
|
let
|
| 8 |
|
|
excludes = not ( X1 and X2 or X1 and X3 or X1 and X4 or
|
| 9 |
|
|
X2 and X3 or X2 and X4 or
|
| 10 |
|
|
X3 and X4 );
|
| 11 |
|
|
tel
|
| 12 |
|
|
node moesi(init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool)returns(
|
| 13 |
|
|
modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int; erreur_mo : bool
|
| 14 |
|
|
);
|
| 15 |
|
|
var
|
| 16 |
|
|
garde_mo1, garde_mo2, garde_mo3, garde_mo4 : bool;
|
| 17 |
|
|
let
|
| 18 |
|
|
garde_mo1 = pre invalid_mo >= 1;
|
| 19 |
|
|
garde_mo2 = pre exclusive_mo>=1;
|
| 20 |
|
|
garde_mo3 = pre shared_mo +1+ pre owned_mo>=1;
|
| 21 |
|
|
garde_mo4 = pre invalid_mo>=1;
|
| 22 |
|
|
erreur_mo = false -> exclusive_mo >= 2;
|
| 23 |
|
|
modified_mo = 0 ->
|
| 24 |
|
|
if(etat_mo1) then if(garde_mo1) then 0 else pre modified_mo else
|
| 25 |
|
|
if(etat_mo2) then if(garde_mo2) then pre modified_mo+1 else pre modified_mo else
|
| 26 |
|
|
if(etat_mo3) then if(garde_mo3) then 0 else pre modified_mo else
|
| 27 |
|
|
if(etat_mo4) then if(garde_mo4) then 0 else pre modified_mo else
|
| 28 |
|
|
pre modified_mo;
|
| 29 |
|
|
exclusive_mo = 0 ->
|
| 30 |
|
|
if(etat_mo1) then if(garde_mo1) then 0 else pre exclusive_mo else
|
| 31 |
|
|
if(etat_mo2) then if(garde_mo2) then pre exclusive_mo-1 else pre exclusive_mo else
|
| 32 |
|
|
if(etat_mo3) then if(garde_mo3) then 1 else pre exclusive_mo else
|
| 33 |
|
|
if(etat_mo4) then if(garde_mo4) then 1 else pre exclusive_mo else
|
| 34 |
|
|
pre exclusive_mo;
|
| 35 |
|
|
shared_mo = 0 ->
|
| 36 |
|
|
if(etat_mo1) then if(garde_mo1) then pre shared_mo -1+ pre exclusive_mo + 1 else pre shared_mo else
|
| 37 |
|
|
if(etat_mo3) then if(garde_mo3) then 0 else pre shared_mo else
|
| 38 |
|
|
if(etat_mo4) then if(garde_mo4) then 0 else pre shared_mo else
|
| 39 |
|
|
pre shared_mo;
|
| 40 |
|
|
invalid_mo = init_invalid_mo ->
|
| 41 |
|
|
if(etat_mo1) then if(garde_mo1) then pre invalid_mo-1 else pre invalid_mo else
|
| 42 |
|
|
if(etat_mo3) then if(garde_mo3) then pre invalid_mo + pre modified_mo + pre exclusive_mo + pre shared_mo + pre owned_mo -1 else pre invalid_mo else
|
| 43 |
|
|
if(etat_mo4) then if(garde_mo4) then pre invalid_mo + pre modified_mo + pre exclusive_mo + pre shared_mo + pre owned_mo -1 else pre invalid_mo else
|
| 44 |
|
|
pre invalid_mo;
|
| 45 |
|
|
owned_mo = 0 ->
|
| 46 |
|
|
if(etat_mo1) then if(garde_mo1) then pre owned_mo + pre modified_mo else pre owned_mo else
|
| 47 |
|
|
if(etat_mo3) then if(garde_mo3) then 0 else pre owned_mo else
|
| 48 |
|
|
if(etat_mo4) then if(garde_mo4) then 0 else pre owned_mo else
|
| 49 |
|
|
pre owned_mo;
|
| 50 |
|
|
tel
|
| 51 |
|
|
node top( init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
|
| 52 |
|
|
returns ( OK : bool );
|
| 53 |
2d37a1e1
|
ploc
|
--@ contract guarantees OK;
|
| 54 |
b8dc00eb
|
bourbouh
|
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
|
| 55 |
|
|
erreur_mo : bool;
|
| 56 |
|
|
env : bool;
|
| 57 |
|
|
let
|
| 58 |
|
|
( modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo, erreur_mo ) =
|
| 59 |
|
|
moesi(init_invalid_mo, etat_mo1, etat_mo2, etat_mo3, etat_mo4 );
|
| 60 |
|
|
env = Sofar( excludes4( etat_mo1, etat_mo2, etat_mo3, etat_mo4 ) );
|
| 61 |
|
|
OK = env => (true ->
|
| 62 |
|
|
(modified_mo+exclusive_mo+shared_mo+invalid_mo+owned_mo) =
|
| 63 |
|
|
pre(modified_mo+exclusive_mo+shared_mo+invalid_mo+owned_mo));
|
| 64 |
|
|
--%MAIN;
|
| 65 |
|
|
--%PROPERTY OK=true;
|
| 66 |
|
|
tel
|