|
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 mesi(etat_me1, etat_me2, etat_me3, etat_me4 : bool
|
|
15
|
) returns (
|
|
16
|
modified_me, exclusive_me, shared_me, invalid_me : int
|
|
17
|
);
|
|
18
|
var
|
|
19
|
garde_me1, garde_me2, garde_me3, garde_me4 : bool;
|
|
20
|
let
|
|
21
|
|
|
22
|
garde_me1 = pre invalid_me >= 1;
|
|
23
|
garde_me2 = pre exclusive_me>=1;
|
|
24
|
garde_me3 = pre shared_me>=1;
|
|
25
|
garde_me4 = pre invalid_me>=1;
|
|
26
|
|
|
27
|
modified_me = 0 ->
|
|
28
|
if(etat_me1) then if(garde_me1) then 0 else pre modified_me else
|
|
29
|
if(etat_me2) then if(garde_me2) then pre modified_me -1 else pre modified_me else
|
|
30
|
if(etat_me3) then if(garde_me3) then 0 else pre modified_me else
|
|
31
|
if(etat_me4) then if(garde_me4) then 0 else pre modified_me else
|
|
32
|
pre modified_me;
|
|
33
|
|
|
34
|
exclusive_me = 0 ->
|
|
35
|
if(etat_me1) then if(garde_me1) then 0 else pre exclusive_me else
|
|
36
|
if(etat_me2) then if(garde_me2) then pre exclusive_me -1 else pre exclusive_me else
|
|
37
|
if(etat_me3) then if(garde_me3) then 1 else pre exclusive_me else
|
|
38
|
if(etat_me4) then if(garde_me4) then 1 else pre exclusive_me else
|
|
39
|
pre exclusive_me;
|
|
40
|
|
|
41
|
shared_me = 0 ->
|
|
42
|
if(etat_me1) then if(garde_me1) then pre shared_me + pre exclusive_me + pre modified_me - 1 else pre shared_me else
|
|
43
|
if(etat_me2) then if(garde_me2) then pre shared_me else pre shared_me else
|
|
44
|
if(etat_me3) then if(garde_me3) then 0 else pre shared_me else
|
|
45
|
if(etat_me4) then if(garde_me4) then 0 else pre shared_me else
|
|
46
|
pre shared_me;
|
|
47
|
|
|
48
|
invalid_me = 3 ->
|
|
49
|
if(etat_me1) then if(garde_me1) then pre invalid_me -1 else pre invalid_me else
|
|
50
|
if(etat_me2) then if(garde_me2) then pre invalid_me else pre invalid_me else
|
|
51
|
if(etat_me3) then if(garde_me3) then pre invalid_me + pre modified_me + pre exclusive_me + pre shared_me -1 else pre invalid_me else
|
|
52
|
if(etat_me4) then if(garde_me4) then pre invalid_me + pre modified_me + pre exclusive_me + pre shared_me -1 else pre invalid_me else
|
|
53
|
pre invalid_me;
|
|
54
|
|
|
55
|
tel
|
|
56
|
|
|
57
|
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool );
|
|
58
|
--@ contract guarantees OK;
|
|
59
|
var modified_me, exclusive_me, shared_me, invalid_me : int;
|
|
60
|
env : bool;
|
|
61
|
let
|
|
62
|
( modified_me, exclusive_me, shared_me, invalid_me ) =
|
|
63
|
mesi( etat_me1, etat_me2, etat_me3, etat_me4 );
|
|
64
|
env = Sofar( excludes4( etat_me1, etat_me2, etat_me3, etat_me4 ) and
|
|
65
|
modified_me >= 0 );
|
|
66
|
OK = env => modified_me <= 1 or shared_me <= 1;
|
|
67
|
--%PROPERTY OK=true;
|
|
68
|
--%MAIN;
|
|
69
|
tel
|