|
1
|
|
|
2
|
node Sofar( X : bool ) returns ( Sofar : bool );
|
|
3
|
let
|
|
4
|
Sofar = X -> X and pre Sofar;
|
|
5
|
tel
|
|
6
|
|
|
7
|
node excludes4( X1, X2, X3, X4 : bool ) returns ( excludes : bool );
|
|
8
|
let
|
|
9
|
excludes = not ( X1 and X2 or X1 and X3 or X1 and X4 or
|
|
10
|
X2 and X3 or X2 and X4 or
|
|
11
|
X3 and X4 );
|
|
12
|
tel
|
|
13
|
|
|
14
|
node moesi(init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool)returns(
|
|
15
|
modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int; erreur_mo : bool
|
|
16
|
);
|
|
17
|
var
|
|
18
|
garde_mo1, garde_mo2, garde_mo3, garde_mo4 : bool;
|
|
19
|
let
|
|
20
|
|
|
21
|
garde_mo1 = pre invalid_mo >= 1;
|
|
22
|
garde_mo2 = pre exclusive_mo>=1;
|
|
23
|
garde_mo3 = pre shared_mo + pre owned_mo>=1;
|
|
24
|
garde_mo4 = pre invalid_mo>=1;
|
|
25
|
|
|
26
|
erreur_mo = false -> exclusive_mo >= 2;
|
|
27
|
|
|
28
|
modified_mo = 0 ->
|
|
29
|
if(etat_mo1) then if(garde_mo1) then 0 else pre modified_mo else
|
|
30
|
if(etat_mo2) then if(garde_mo2) then pre modified_mo+1 else pre modified_mo else
|
|
31
|
if(etat_mo3) then if(garde_mo3) then 0 else pre modified_mo else
|
|
32
|
if(etat_mo4) then if(garde_mo4) then 0 else pre modified_mo else
|
|
33
|
pre modified_mo;
|
|
34
|
|
|
35
|
exclusive_mo = 0 ->
|
|
36
|
if(etat_mo1) then if(garde_mo1) then 0 else pre exclusive_mo else
|
|
37
|
if(etat_mo2) then if(garde_mo2) then pre exclusive_mo-1 else pre exclusive_mo else
|
|
38
|
if(etat_mo3) then if(garde_mo3) then 1 else pre exclusive_mo else
|
|
39
|
if(etat_mo4) then if(garde_mo4) then 1 else pre exclusive_mo else
|
|
40
|
pre exclusive_mo;
|
|
41
|
|
|
42
|
shared_mo = 0 ->
|
|
43
|
if(etat_mo1) then if(garde_mo1) then pre shared_mo + pre exclusive_mo + 1 else pre shared_mo else
|
|
44
|
if(etat_mo3) then if(garde_mo3) then 0 else pre shared_mo else
|
|
45
|
if(etat_mo4) then if(garde_mo4) then 0 else pre shared_mo else
|
|
46
|
pre shared_mo;
|
|
47
|
|
|
48
|
invalid_mo = init_invalid_mo ->
|
|
49
|
if(etat_mo1) then if(garde_mo1) then pre invalid_mo-1 else pre invalid_mo else
|
|
50
|
if(etat_mo3) then if(garde_mo3) then pre invalid_mo + pre modified_mo + pre exclusive_mo + pre shared_mo + pre owned_mo -1 else pre invalid_mo else
|
|
51
|
if(etat_mo4) then if(garde_mo4) then pre invalid_mo + pre modified_mo + pre exclusive_mo + pre shared_mo + pre owned_mo -1 else pre invalid_mo else
|
|
52
|
pre invalid_mo;
|
|
53
|
|
|
54
|
owned_mo = 0 ->
|
|
55
|
if(etat_mo1) then if(garde_mo1) then pre owned_mo + pre modified_mo else pre owned_mo else
|
|
56
|
if(etat_mo3) then if(garde_mo3) then 0 else pre owned_mo else
|
|
57
|
if(etat_mo4) then if(garde_mo4) then 0 else pre owned_mo else
|
|
58
|
pre owned_mo;
|
|
59
|
|
|
60
|
tel
|
|
61
|
|
|
62
|
node top( init_invalid_mo : int;
|
|
63
|
etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool )
|
|
64
|
returns ( OK : bool );
|
|
65
|
--@ contract guarantees OK;
|
|
66
|
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int;
|
|
67
|
erreur_mo : bool;
|
|
68
|
let
|
|
69
|
( modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo, erreur_mo ) =
|
|
70
|
moesi(init_invalid_mo, etat_mo1, etat_mo2, etat_mo3, etat_mo4 );
|
|
71
|
OK = Sofar( excludes4(etat_mo1, etat_mo2, etat_mo3, etat_mo4)
|
|
72
|
and init_invalid_mo > 0 )
|
|
73
|
=> not erreur_mo;
|
|
74
|
--%PROPERTY OK=true;
|
|
75
|
--%MAIN;
|
|
76
|
tel
|