lustrec / test / src / kind_fmcad08 / memory2 / ILLINOIS_all.lus @ 0cbf0839
History | View | Annotate | Download (4.2 KB)
| 1 |
-- |
|---|---|
| 2 |
-- Source: David Merchat (node illinois) |
| 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 excludes9( X1, X2, X3, X4, X5, X6, X7, X8, X9 : 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 and not X9 or |
| 18 |
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 |
| 19 |
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 |
| 20 |
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 |
| 21 |
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 |
| 22 |
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 |
| 23 |
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 |
| 24 |
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 |
| 25 |
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 |
| 26 |
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; |
| 27 |
tel |
| 28 |
|
| 29 |
node illinois(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int) |
| 30 |
returns(invalid, dirty, exclusive, shared : int); |
| 31 |
var |
| 32 |
g1, g2, g3, g4, g5, g6, g7, g8, g9 : bool; |
| 33 |
let |
| 34 |
|
| 35 |
g1 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0; |
| 36 |
g2 = pre invalid>=1 and pre dirty>=1; |
| 37 |
g3 = pre invalid>=1 and pre shared+pre exclusive>=1; |
| 38 |
g4 = pre exclusive>=1; |
| 39 |
g5 = pre shared>=1; |
| 40 |
g6 = pre invalid>=1; |
| 41 |
g7 = pre dirty>=1; |
| 42 |
g8 = pre shared>=1; |
| 43 |
g9 = pre exclusive>=1; |
| 44 |
|
| 45 |
invalid = (if(init_invalid>0) then init_invalid else 1-init_invalid) -> |
| 46 |
if(e1) then if(g1) then pre invalid-1 else pre invalid else |
| 47 |
if(e2) then if(g2) then pre invalid-1 else pre invalid else |
| 48 |
if(e3) then if(g3) then pre invalid-1 else pre invalid else |
| 49 |
if(e5) then if(g5) then pre invalid+pre shared-1 else pre invalid else |
| 50 |
if(e6) then if(g6) then pre invalid+pre dirty+pre shared+pre exclusive-1 else pre invalid else |
| 51 |
if(e7) then if(g7) then pre invalid+1 else pre invalid else |
| 52 |
if(e8) then if(g8) then pre invalid+1 else pre invalid else |
| 53 |
if(e9) then if(g9) then pre invalid+1 else pre invalid else |
| 54 |
pre invalid; |
| 55 |
|
| 56 |
dirty = 0 -> |
| 57 |
if(e2) then if(g2) then pre dirty-1 else pre dirty else |
| 58 |
if(e4) then if(g4) then pre dirty+1 else pre dirty else |
| 59 |
if(e5) then if(g5) then pre dirty+1 else pre dirty else |
| 60 |
if(e6) then if(g6) then 1 else pre dirty else |
| 61 |
if(e7) then if(g7) then pre dirty-1 else pre dirty else |
| 62 |
pre dirty; |
| 63 |
|
| 64 |
exclusive = 0 -> |
| 65 |
if(e1) then if(g1) then pre exclusive+1 else pre exclusive else |
| 66 |
if(e3) then if(g3) then pre 0 else pre exclusive else |
| 67 |
if(e4) then if(g4) then pre exclusive-1 else pre exclusive else |
| 68 |
if(e6) then if(g6) then 0 else pre exclusive else |
| 69 |
if(e9) then if(g9) then pre exclusive-1 else pre exclusive else |
| 70 |
pre exclusive; |
| 71 |
|
| 72 |
shared = 0 -> |
| 73 |
if(e2) then if(g2) then pre shared+2 else pre shared else |
| 74 |
if(e3) then if(g3) then pre shared+pre exclusive+1 else pre shared else |
| 75 |
if(e5) then if(g5) then 0 else pre shared else |
| 76 |
if(e6) then if(g6) then 0 else pre shared else |
| 77 |
if(e8) then if(g8) then pre shared-1 else pre shared else |
| 78 |
pre shared; |
| 79 |
|
| 80 |
tel |
| 81 |
|
| 82 |
node top(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool; init_invalid : int) |
| 83 |
returns( OK : bool); |
| 84 |
var invalid, dirty, exclusive, shared : int; |
| 85 |
env : bool; |
| 86 |
let |
| 87 |
( invalid, dirty, exclusive, shared ) = |
| 88 |
illinois( e1, e2, e3, e4, e5, e6, e7, e8, e9, init_invalid ); |
| 89 |
|
| 90 |
env = Sofar( excludes9( e1, e2, e3, e4, e5, e6, e7, e8, e9 ) and |
| 91 |
init_invalid > 0 ); |
| 92 |
|
| 93 |
OK = env => |
| 94 |
exclusive < 2 and |
| 95 |
(true -> invalid + dirty + exclusive + shared = |
| 96 |
pre ( invalid + dirty + exclusive + shared ) ) and |
| 97 |
invalid + dirty + exclusive + shared = First( init_invalid ) and |
| 98 |
exclusive >= 0; |
| 99 |
--%PROPERTY OK=true; |
| 100 |
--%MAIN; |
| 101 |
tel |