lustrec / test / src / kind_fmcad08 / memory1 / FIREFLY_9.lus @ 22fe1c93
History | View | Annotate | Download (3.76 KB)
1 |
-- |
---|---|
2 |
-- Source: David Merchat (node firefly) |
3 |
-- |
4 |
|
5 |
node First( X : int ) returns ( First : int ); |
6 |
let |
7 |
First = X -> pre First; |
8 |
tel |
9 |
|
10 |
node Sofar( X : bool ) returns ( Sofar : bool ); |
11 |
let |
12 |
Sofar = X -> X and pre Sofar; |
13 |
tel |
14 |
|
15 |
node excludes8( X1, X2, X3, X4, X5, X6, X7, X8 : bool ) returns ( excludes : bool ); |
16 |
let |
17 |
excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or |
18 |
X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or |
19 |
not X1 and X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or |
20 |
not X1 and not X2 and X3 and not X4 and not X5 and not X6 and not X7 and not X8 or |
21 |
not X1 and not X2 and not X3 and X4 and not X5 and not X6 and not X7 and not X8 or |
22 |
not X1 and not X2 and not X3 and not X4 and X5 and not X6 and not X7 and not X8 or |
23 |
not X1 and not X2 and not X3 and not X4 and not X5 and X6 and not X7 and not X8 or |
24 |
not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and X7 and not X8 or |
25 |
not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and X8; |
26 |
tel |
27 |
|
28 |
node firefly(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int) |
29 |
returns(invalid, dirty, exclusive, shared : int); |
30 |
var |
31 |
|
32 |
garde1, garde2, garde3, garde4, garde5, garde6, garde7, garde8 : bool; |
33 |
mem_invalid : int; |
34 |
|
35 |
let |
36 |
|
37 |
mem_invalid = i_invalid -> pre mem_invalid; |
38 |
|
39 |
garde1 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0 ; |
40 |
garde2 = pre invalid>=1 and pre dirty>=1; |
41 |
garde3 = pre invalid>=1 and pre shared+pre exclusive>=1; |
42 |
garde4 = pre exclusive>=1; |
43 |
garde5 = pre shared=1; |
44 |
garde6 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0; |
45 |
garde7 = pre invalid>=1 and pre dirty>=1; |
46 |
garde8 = pre invalid>=1 and pre shared+pre exclusive>=1; |
47 |
|
48 |
invalid = mem_invalid -> |
49 |
if(e1) then if(garde1) then pre invalid-1 else pre invalid else |
50 |
if(e2) then if(garde2) then pre invalid-1 else pre invalid else |
51 |
if(e3) then if(garde3) then pre invalid-1 else pre invalid else |
52 |
if(e6) then if(garde6) then pre invalid-1 else pre invalid else |
53 |
if(e7) then if(garde7) then pre invalid-1 else pre invalid else |
54 |
if(e8) then if(garde8) then pre invalid-1 else pre invalid else |
55 |
pre invalid; |
56 |
|
57 |
|
58 |
dirty = 0 -> |
59 |
if(e2) then if(garde2) then pre dirty-1 else pre dirty else |
60 |
if(e4) then if(garde4) then pre dirty+1 else pre dirty else |
61 |
if(e6) then if(garde6) then 1 else pre dirty else |
62 |
if(e7) then if(garde7) then pre dirty-1 else pre dirty else |
63 |
pre dirty; |
64 |
|
65 |
exclusive = 0 -> |
66 |
if(e1) then if(garde1) then pre exclusive+1 else pre exclusive else |
67 |
if(e3) then if(garde3) then 0 else pre exclusive else |
68 |
if(e4) then if(garde4) then pre exclusive-1 else pre exclusive else |
69 |
if(e5) then if(garde5) then pre exclusive+1 else pre exclusive else |
70 |
if(e8) then if(garde8) then 0 else pre exclusive else |
71 |
pre exclusive; |
72 |
|
73 |
shared = 0 -> |
74 |
if(e2) then if(garde2) then pre shared+2 else pre shared else |
75 |
if(e3) then if(garde3) then pre shared + pre exclusive + 1 else pre shared else |
76 |
if(e5) then if(garde5) then pre 0 else pre shared else |
77 |
if(e7) then if(garde7) then pre shared+2 else pre shared else |
78 |
if(e8) then if(garde8) then pre shared + pre exclusive + 1 else pre shared else |
79 |
pre shared; |
80 |
|
81 |
tel |
82 |
|
83 |
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int) |
84 |
returns( OK : bool ); |
85 |
var invalid, dirty, exclusive, shared : int; |
86 |
env : bool; |
87 |
procs : int; |
88 |
let |
89 |
( invalid, dirty, exclusive, shared ) = |
90 |
firefly( e1, e2, e3, e4, e5, e6, e7, e8, i_invalid ); |
91 |
|
92 |
env = Sofar( excludes8( e1, e2, e3, e4, e5, e6, e7, e8 ) and |
93 |
i_invalid >= 0 and i_invalid < 5 ); |
94 |
procs = First( i_invalid ); |
95 |
|
96 |
OK = env => invalid <= procs; |
97 |
--%PROPERTY OK=true; |
98 |
--%MAIN; |
99 |
tel |