|
1
|
|
|
2
|
-- Source: David Merchat (node DRAGON + property v1)
|
|
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 excludes12( X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12 : 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 and not X10 and not X11 and not X12 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 and not X10 and not X11 and not X12 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 and not X10 and not X11 and not X12 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 and not X10 and not X11 and not X12 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 and not X10 and not X11 and not X12 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 and not X10 and not X11 and not X12 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 and not X10 and not X11 and not X12 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 and not X10 and not X11 and not X12 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 and not X10 and not X11 and not X12 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 and not X10 and not X11 and not X12 or
|
|
27
|
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 and X10 and not X11 and not X12 or
|
|
28
|
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 and not X10 and X11 and not X12 or
|
|
29
|
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 and not X10 and not X11 and X12;
|
|
30
|
tel
|
|
31
|
|
|
32
|
node DRAGON(e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
|
|
33
|
init_invalid : int)
|
|
34
|
returns(exclusive, shared, shared_dirty, dirty, invalid : int; erreur : bool);
|
|
35
|
var
|
|
36
|
g01, g02, g03, g04, g05, g06, g07, g08, g09, g10, g11, g12 : bool;
|
|
37
|
mem_init : int;
|
|
38
|
let
|
|
39
|
|
|
40
|
mem_init = init_invalid -> pre mem_init;
|
|
41
|
|
|
42
|
erreur = if(exclusive >= 2) then true else false;
|
|
43
|
|
|
44
|
g01 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0 and pre shared_dirty=0;
|
|
45
|
g02 = pre invalid>=1 and pre dirty + pre shared + pre exclusive + pre shared_dirty>=1;
|
|
46
|
g03 = pre exclusive>=1;
|
|
47
|
g04 = pre shared_dirty=1 and pre shared=0;
|
|
48
|
g05 = pre shared_dirty=0 and pre shared=1;
|
|
49
|
g06 = pre shared_dirty + pre shared>=2;
|
|
50
|
g07 = pre invalid>=1 and pre dirty=0 and pre shared=0 and pre exclusive=0 and pre shared_dirty=0;
|
|
51
|
g08 = pre invalid>=1 and pre dirty + pre shared + pre exclusive + pre shared_dirty>=1;
|
|
52
|
g09 = pre dirty>=1;
|
|
53
|
g10 = pre shared>=1;
|
|
54
|
g11 = pre shared_dirty>=1;
|
|
55
|
g12 = pre exclusive>=1;
|
|
56
|
|
|
57
|
exclusive = 0 ->
|
|
58
|
if(e01) then if(g01) then pre exclusive+1 else pre exclusive else
|
|
59
|
if(e02) then if(g02) then 0 else pre exclusive else
|
|
60
|
if(e03) then if(g03) then pre exclusive-1 else pre exclusive else
|
|
61
|
if(e08) then if(g08) then 0 else pre exclusive else
|
|
62
|
if(e12) then if(g12) then pre exclusive-1 else pre exclusive else
|
|
63
|
pre exclusive;
|
|
64
|
|
|
65
|
shared = 0 ->
|
|
66
|
if(e02) then if(g02) then pre shared+pre exclusive+1 else pre shared else
|
|
67
|
if(e05) then if(g05) then 0 else pre shared else
|
|
68
|
if(e06) then if(g06) then pre shared+pre shared_dirty-1 else pre shared else
|
|
69
|
if(e08) then if(g08) then pre shared+pre exclusive+pre shared_dirty+pre dirty else pre shared else
|
|
70
|
if(e10) then if(g10) then pre shared-1 else pre shared else
|
|
71
|
pre shared;
|
|
72
|
|
|
73
|
shared_dirty = 0 ->
|
|
74
|
if(e02) then if(g02) then pre shared_dirty+pre dirty else pre shared_dirty else
|
|
75
|
if(e04) then if(g04) then 0 else pre shared_dirty else
|
|
76
|
if(e06) then if(g06) then 1 else pre shared_dirty else
|
|
77
|
if(e08) then if(g08) then 1 else pre shared_dirty else
|
|
78
|
if(e11) then if(g11) then pre shared_dirty-1 else pre shared_dirty else
|
|
79
|
pre shared_dirty;
|
|
80
|
|
|
81
|
dirty = 0 ->
|
|
82
|
if(e02) then if(g02) then 0 else pre dirty else
|
|
83
|
if(e03) then if(g03) then pre dirty+1 else pre dirty else
|
|
84
|
if(e04) then if(g04) then pre dirty+1 else pre dirty else
|
|
85
|
if(e05) then if(g05) then pre dirty+1 else pre dirty else
|
|
86
|
if(e07) then if(g07) then pre dirty+1 else pre dirty else
|
|
87
|
if(e08) then if(g08) then 0 else pre dirty else
|
|
88
|
if(e09) then if(g09) then pre dirty-1 else pre dirty else
|
|
89
|
pre dirty;
|
|
90
|
|
|
91
|
invalid = mem_init ->
|
|
92
|
if(e01) then if(g01) then pre invalid-1 else pre invalid else
|
|
93
|
if(e02) then if(g02) then pre invalid-1 else pre invalid else
|
|
94
|
if(e07) then if(g07) then pre invalid-1 else pre invalid else
|
|
95
|
if(e08) then if(g08) then pre invalid-1 else pre invalid else
|
|
96
|
if(e09) then if(g09) then pre invalid+1 else pre invalid else
|
|
97
|
if(e10) then if(g10) then pre invalid+1 else pre invalid else
|
|
98
|
if(e11) then if(g11) then pre invalid+1 else pre invalid else
|
|
99
|
if(e12) then if(g12) then pre invalid+1 else pre invalid else
|
|
100
|
pre invalid;
|
|
101
|
tel
|
|
102
|
|
|
103
|
-- Only provable in nbac
|
|
104
|
node top( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool;
|
|
105
|
init_invalid : int ) returns ( OK : bool );
|
|
106
|
--@ contract guarantees OK;
|
|
107
|
var exclusive, shared, shared_dirty, dirty, invalid : int;
|
|
108
|
erreur : bool;
|
|
109
|
env : bool;
|
|
110
|
let
|
|
111
|
( exclusive, shared, shared_dirty, dirty, invalid, erreur ) =
|
|
112
|
DRAGON( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12,
|
|
113
|
init_invalid );
|
|
114
|
env = Sofar( excludes12( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10,
|
|
115
|
e11, e12 ) and
|
|
116
|
init_invalid > 0);
|
|
117
|
OK = env => dirty <= First( init_invalid );
|
|
118
|
--%PROPERTY OK=true;
|
|
119
|
--%MAIN;
|
|
120
|
tel
|