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