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 |