lustrec / test / src / kind_fmcad08 / memory2 / ILLINOIS_4_e7_2651_e7_2847.lus @ 22fe1c93
History | View | Annotate | Download (3.83 KB)
1 |
|
---|---|
2 |
node Sofar( X : bool ) returns ( Sofar : bool ); |
3 |
let |
4 |
Sofar = X -> X or pre Sofar; |
5 |
tel |
6 |
node excludes9( X1, X2, X3, X4, X5, X6, X7, X8, X9 : bool ) returns ( excludes : bool ); |
7 |
let |
8 |
excludes = not X1 or not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or |
9 |
X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or |
10 |
not X1 and X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or |
11 |
not X1 and not X2 and X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or |
12 |
not X1 and not X2 and not X3 and X4 and not X5 and not X6 and not X7 and not X8 and not X9 or |
13 |
not X1 and not X2 and not X3 and not X4 and X5 and not X6 and not X7 and not X8 and not X9 or |
14 |
not X1 and not X2 and not X3 and not X4 and not X5 and X6 and not X7 and not X8 and not X9 or |
15 |
not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and X7 and not X8 and not X9 or |
16 |
not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and X8 and not X9 or |
17 |
not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and X9; |
18 |
tel |
19 |
node illinois(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int) |
20 |
returns(invalid, dirty, exclusive, shared : int); |
21 |
var |
22 |
g1, g2, g3, g4, g5, g6, g7, g8, g9 : bool; |
23 |
let |
24 |
g1 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0; |
25 |
g2 = pre invalid>=1 and pre dirty>=1; |
26 |
g3 = pre invalid>=1 and pre shared+pre exclusive>=1; |
27 |
g4 = pre exclusive>=1; |
28 |
g5 = pre shared>=1; |
29 |
g6 = pre invalid>=1; |
30 |
g7 = pre dirty>=1; |
31 |
g8 = pre shared>=1; |
32 |
g9 = pre exclusive>=1; |
33 |
invalid = (if(init_invalid>0) then init_invalid else 1-init_invalid) -> |
34 |
if(e1) then if(g1) then pre invalid-1 else pre invalid else |
35 |
if(e2) then if(g2) then pre invalid-1 else pre invalid else |
36 |
if(e3) then if(g3) then pre invalid-1 else pre invalid else |
37 |
if(e5) then if(g5) then pre invalid+pre shared-1 else pre invalid else |
38 |
if(e6) then if(g6) then pre invalid+pre dirty+pre shared+pre exclusive-1 else pre invalid else |
39 |
if(e7) then if(g7) then pre invalid+1 else pre invalid else |
40 |
if(e8) then if(g8) then pre invalid+1 else pre invalid else |
41 |
if(e9) then if(g9) then pre invalid+1 else pre invalid else |
42 |
pre invalid; |
43 |
dirty = 0 -> |
44 |
if(e2) then if(g2) then pre dirty-1 else pre dirty else |
45 |
if(e4) then if(g4) then pre dirty+1 else pre dirty else |
46 |
if(e5) then if(g5) then pre dirty+1 else pre dirty else |
47 |
if(e6) then if(g6) then 1 else pre dirty else |
48 |
if(e7) then if(g7) then pre dirty-1 else pre dirty else |
49 |
pre dirty; |
50 |
exclusive = 0 -> |
51 |
if(e1) then if(g1) then pre exclusive+1 else pre exclusive else |
52 |
if(e3) then if(g3) then pre 0 else pre exclusive else |
53 |
if(e4) then if(g4) then pre exclusive-1 else pre exclusive else |
54 |
if(e6) then if(g6) then 0 else pre exclusive else |
55 |
if(e9) then if(g9) then pre exclusive-1 else pre exclusive else |
56 |
pre exclusive; |
57 |
shared = 0 -> |
58 |
if(e2) then if(g2) then pre shared+2 else pre shared else |
59 |
if(e3) then if(g3) then pre shared+pre exclusive+1 else pre shared else |
60 |
if(e5) then if(g5) then 0 else pre shared else |
61 |
if(e6) then if(g6) then 0 else pre shared else |
62 |
if(e8) then if(g8) then pre shared-1 else pre shared else |
63 |
pre shared; |
64 |
tel |
65 |
node top(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int) |
66 |
returns( OK : bool); |
67 |
var invalid, dirty, exclusive, shared : int; |
68 |
env : bool; |
69 |
let |
70 |
( invalid, dirty, exclusive, shared ) = |
71 |
illinois( e1, e2, e3, e4, e5, e6, e7, e8, e9, init_invalid ); |
72 |
env = Sofar( excludes9( e1, e2, e3, e4, e5, e6, e7, e8, e9 ) and |
73 |
init_invalid > 0 ); |
74 |
OK = env => dirty >= 0; |
75 |
--%MAIN; |
76 |
--%PROPERTY OK=true; |
77 |
tel |