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