|
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 and pre Sofar;
|
|
9
|
tel
|
|
10
|
node excludes8( X1, X2, X3, X4, X5, X6, X7, X8 : 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 or
|
|
13
|
X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or
|
|
14
|
not X1 and X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 or
|
|
15
|
not X1 and not X2 and X3 and not X4 and not X5 and not X6 and not X7 and not X8 or
|
|
16
|
not X1 and not X2 and not X3 and X4 and not X5 and not X6 and not X7 and not X8 or
|
|
17
|
not X1 and not X2 and not X3 and not X4 and X5 and not X6 and not X7 and not X8 or
|
|
18
|
not X1 and not X2 and not X3 and not X4 and not X5 and X6 and not X7 and not X8 or
|
|
19
|
not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and X7 and not X8 or
|
|
20
|
not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and X8;
|
|
21
|
tel
|
|
22
|
node firefly(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
|
|
23
|
returns(invalid, dirty, exclusive, shared : int);
|
|
24
|
var
|
|
25
|
garde1, garde2, garde3, garde4, garde5, garde6, garde7, garde8 : bool;
|
|
26
|
mem_invalid : int;
|
|
27
|
let
|
|
28
|
mem_invalid = i_invalid -> pre mem_invalid;
|
|
29
|
garde1 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0 ;
|
|
30
|
garde2 = pre invalid>=1 and pre dirty>=1;
|
|
31
|
garde3 = pre invalid>=1 and pre shared+pre exclusive>=1;
|
|
32
|
garde4 = pre exclusive>=1;
|
|
33
|
garde5 = pre shared=1;
|
|
34
|
garde6 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0;
|
|
35
|
garde7 = pre invalid>=1 and pre dirty>=1;
|
|
36
|
garde8 = pre invalid>=1 and pre shared+pre exclusive>=1;
|
|
37
|
invalid = mem_invalid ->
|
|
38
|
if(e1) then if(garde1) then pre invalid-1 else pre invalid else
|
|
39
|
if(e2) then if(garde2) then pre invalid-1 else pre invalid else
|
|
40
|
if(e3) then if(garde3) then pre invalid-1 else pre invalid else
|
|
41
|
if(e6) then if(garde6) then pre invalid-1 else pre invalid else
|
|
42
|
if(e7) then if(garde7) then pre invalid-1 else pre invalid else
|
|
43
|
if(e8) then if(garde8) then pre invalid-1 else pre invalid else
|
|
44
|
pre invalid;
|
|
45
|
dirty = 0 ->
|
|
46
|
if(e2) then if(garde2) then pre dirty-1 else pre dirty else
|
|
47
|
if(e4) then if(garde4) then pre dirty+1 else pre dirty else
|
|
48
|
if(e6) then if(garde6) then 1 else pre dirty else
|
|
49
|
if(e7) then if(garde7) then pre dirty-1 else pre dirty else
|
|
50
|
pre dirty;
|
|
51
|
exclusive = 0 ->
|
|
52
|
if(e1) then if(garde1) then pre exclusive+1 else pre exclusive else
|
|
53
|
if(e3) then if(garde3) then 0 else pre exclusive else
|
|
54
|
if(e4) then if(garde4) then pre exclusive-1 else pre exclusive else
|
|
55
|
if(e5) then if(garde5) then pre exclusive+1 else pre exclusive else
|
|
56
|
if(e8) then if(garde8) then 0 else pre exclusive else
|
|
57
|
pre exclusive;
|
|
58
|
shared = 0 ->
|
|
59
|
if(e2) then if(garde2) then pre shared+2 else pre shared else
|
|
60
|
if(e3) then if(garde3) then pre shared -1+ pre exclusive + 1 else pre shared else
|
|
61
|
if(e5) then if(garde5) then pre 0 else pre shared else
|
|
62
|
if(e7) then if(garde7) then pre shared+2 else pre shared else
|
|
63
|
if(e8) then if(garde8) then pre shared + pre exclusive + 1 else pre shared else
|
|
64
|
pre shared;
|
|
65
|
tel
|
|
66
|
node top(e1, e2, e3, e4, e5, e6, e7, e8 : bool; i_invalid : int)
|
|
67
|
returns( OK : bool );
|
|
68
|
--@ contract guarantees OK;
|
|
69
|
var invalid, dirty, exclusive, shared : int;
|
|
70
|
env : bool;
|
|
71
|
procs : int;
|
|
72
|
let
|
|
73
|
( invalid, dirty, exclusive, shared ) =
|
|
74
|
firefly( e1, e2, e3, e4, e5, e6, e7, e8, i_invalid );
|
|
75
|
env = Sofar( excludes8( e1, e2, e3, e4, e5, e6, e7, e8 ) and
|
|
76
|
i_invalid >= 0 and i_invalid < 5 );
|
|
77
|
procs = First( i_invalid );
|
|
78
|
OK = env =>
|
|
79
|
( true -> invalid+dirty+exclusive+shared =
|
|
80
|
pre(invalid+dirty+exclusive+shared)) and
|
|
81
|
invalid + dirty + exclusive + shared = First( i_invalid ) and
|
|
82
|
invalid + dirty + exclusive + shared <= procs and
|
|
83
|
invalid >= 0 and
|
|
84
|
invalid <= procs;
|
|
85
|
--%MAIN;
|
|
86
|
--%PROPERTY OK=true;
|
|
87
|
tel
|