lustrec / test / src / kind_fmcad08 / memory2 / MESI_3.lus @ 22fe1c93
History | View | Annotate | Download (2.73 KB)
| 1 |
|
|---|---|
| 2 |
node Sofar( X : bool ) returns ( Sofar : bool ); |
| 3 |
let |
| 4 |
Sofar = X -> X and pre Sofar; |
| 5 |
tel |
| 6 |
|
| 7 |
node Abs( X : int ) returns ( Abs : int ); |
| 8 |
let |
| 9 |
Abs = if X < 0 then -X else X; |
| 10 |
tel |
| 11 |
|
| 12 |
node excludes4( X1, X2, X3, X4 : bool ) returns ( excludes : bool ); |
| 13 |
let |
| 14 |
excludes = not ( X1 and X2 or X1 and X3 or X1 and X4 or |
| 15 |
X2 and X3 or X2 and X4 or |
| 16 |
X3 and X4 ); |
| 17 |
tel |
| 18 |
|
| 19 |
node mesi(etat_me1, etat_me2, etat_me3, etat_me4 : bool |
| 20 |
) returns ( |
| 21 |
modified_me, exclusive_me, shared_me, invalid_me : int |
| 22 |
); |
| 23 |
var |
| 24 |
garde_me1, garde_me2, garde_me3, garde_me4 : bool; |
| 25 |
let |
| 26 |
|
| 27 |
garde_me1 = pre invalid_me >= 1; |
| 28 |
garde_me2 = pre exclusive_me>=1; |
| 29 |
garde_me3 = pre shared_me>=1; |
| 30 |
garde_me4 = pre invalid_me>=1; |
| 31 |
|
| 32 |
modified_me = 0 -> |
| 33 |
if(etat_me1) then if(garde_me1) then 0 else pre modified_me else |
| 34 |
if(etat_me2) then if(garde_me2) then pre modified_me -1 else pre modified_me else |
| 35 |
if(etat_me3) then if(garde_me3) then 0 else pre modified_me else |
| 36 |
if(etat_me4) then if(garde_me4) then 0 else pre modified_me else |
| 37 |
pre modified_me; |
| 38 |
|
| 39 |
exclusive_me = 0 -> |
| 40 |
if(etat_me1) then if(garde_me1) then 0 else pre exclusive_me else |
| 41 |
if(etat_me2) then if(garde_me2) then pre exclusive_me -1 else pre exclusive_me else |
| 42 |
if(etat_me3) then if(garde_me3) then 1 else pre exclusive_me else |
| 43 |
if(etat_me4) then if(garde_me4) then 1 else pre exclusive_me else |
| 44 |
pre exclusive_me; |
| 45 |
|
| 46 |
shared_me = 0 -> |
| 47 |
if(etat_me1) then if(garde_me1) then pre shared_me + pre exclusive_me + pre modified_me - 1 else pre shared_me else |
| 48 |
if(etat_me2) then if(garde_me2) then pre shared_me else pre shared_me else |
| 49 |
if(etat_me3) then if(garde_me3) then 0 else pre shared_me else |
| 50 |
if(etat_me4) then if(garde_me4) then 0 else pre shared_me else |
| 51 |
pre shared_me; |
| 52 |
|
| 53 |
invalid_me = 3 -> |
| 54 |
if(etat_me1) then if(garde_me1) then pre invalid_me -1 else pre invalid_me else |
| 55 |
if(etat_me2) then if(garde_me2) then pre invalid_me else pre invalid_me else |
| 56 |
if(etat_me3) then if(garde_me3) then pre invalid_me + pre modified_me + pre exclusive_me + pre shared_me -1 else pre invalid_me else |
| 57 |
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 |
| 58 |
pre invalid_me; |
| 59 |
|
| 60 |
tel |
| 61 |
|
| 62 |
-- Only provable in nbac |
| 63 |
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool ); |
| 64 |
var modified_me, exclusive_me, shared_me, invalid_me : int; |
| 65 |
env : bool; |
| 66 |
let |
| 67 |
( modified_me, exclusive_me, shared_me, invalid_me ) = |
| 68 |
mesi( etat_me1, etat_me2, etat_me3, etat_me4 ); |
| 69 |
env = Sofar( excludes4( etat_me1, etat_me2, etat_me3, etat_me4 ) ); |
| 70 |
OK = env => (Abs(modified_me)+Abs(exclusive_me)+ |
| 71 |
Abs(shared_me)+Abs(invalid_me)) <= 3; |
| 72 |
--%PROPERTY OK=true; |
| 73 |
--%MAIN; |
| 74 |
tel |