1 |
b8dc00eb
|
bourbouh
|
|
2 |
|
|
node Sofar( X : bool ) returns ( Sofar : bool );
|
3 |
|
|
let
|
4 |
|
|
Sofar = X -> X and pre Sofar;
|
5 |
|
|
tel
|
6 |
|
|
node excludes4( X1, X2, X3, X4 : bool ) returns ( excludes : bool );
|
7 |
|
|
let
|
8 |
|
|
excludes = not ( X1 and X2 or X1 and X3 or X1 and X4 or
|
9 |
|
|
X2 and X3 or X2 and X4 or
|
10 |
|
|
X3 and X4 );
|
11 |
|
|
tel
|
12 |
|
|
node mesi(etat_me1, etat_me2, etat_me3, etat_me4 : bool
|
13 |
|
|
) returns (
|
14 |
|
|
modified_me, exclusive_me, shared_me, invalid_me : int
|
15 |
|
|
);
|
16 |
|
|
var
|
17 |
|
|
garde_me1, garde_me2, garde_me3, garde_me4 : bool;
|
18 |
|
|
let
|
19 |
|
|
garde_me1 = pre invalid_me >= 1;
|
20 |
|
|
garde_me2 = pre exclusive_me>=1;
|
21 |
|
|
garde_me3 = pre shared_me>=1;
|
22 |
|
|
garde_me4 = pre invalid_me>=1;
|
23 |
|
|
modified_me = 0 ->
|
24 |
|
|
if(etat_me1) then if(garde_me1) then 0 else pre modified_me else
|
25 |
|
|
if(etat_me2) then if(garde_me2) then pre modified_me -1 else pre modified_me else
|
26 |
|
|
if(etat_me3) then if(garde_me3) then 0 else pre modified_me else
|
27 |
|
|
if(etat_me4) then if(garde_me4) then 0 else pre modified_me else
|
28 |
|
|
pre modified_me;
|
29 |
|
|
exclusive_me = 0 ->
|
30 |
|
|
if(etat_me1) then if(garde_me1) then 0 else pre exclusive_me else
|
31 |
|
|
if(etat_me2) then if(garde_me2) then pre exclusive_me -1 else pre exclusive_me else
|
32 |
|
|
if(etat_me3) then if(garde_me3) then 1 else pre exclusive_me else
|
33 |
|
|
if(etat_me4) then if(garde_me4) then 1 else pre exclusive_me else
|
34 |
|
|
pre exclusive_me;
|
35 |
|
|
shared_me = 0 ->
|
36 |
|
|
if(etat_me1) then if(garde_me1) then pre shared_me +1+ pre exclusive_me + pre modified_me - 1 else pre shared_me else
|
37 |
|
|
if(etat_me2) then if(garde_me2) then pre shared_me else pre shared_me else
|
38 |
|
|
if(etat_me3) then if(garde_me3) then 0 else pre shared_me else
|
39 |
|
|
if(etat_me4) then if(garde_me4) then 0 else pre shared_me else
|
40 |
|
|
pre shared_me;
|
41 |
|
|
invalid_me = 3 ->
|
42 |
|
|
if(etat_me1) then if(garde_me1) then pre invalid_me -1 else pre invalid_me else
|
43 |
|
|
if(etat_me2) then if(garde_me2) then pre invalid_me else pre invalid_me else
|
44 |
|
|
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
|
45 |
|
|
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
|
46 |
|
|
pre invalid_me;
|
47 |
|
|
tel
|
48 |
|
|
node top( etat_me1, etat_me2, etat_me3, etat_me4 : bool ) returns ( OK : bool );
|
49 |
2d37a1e1
|
ploc
|
--@ contract guarantees OK;
|
50 |
b8dc00eb
|
bourbouh
|
var modified_me, exclusive_me, shared_me, invalid_me : int;
|
51 |
|
|
env : bool;
|
52 |
|
|
let
|
53 |
|
|
( modified_me, exclusive_me, shared_me, invalid_me ) =
|
54 |
|
|
mesi( etat_me1, etat_me2, etat_me3, etat_me4 );
|
55 |
|
|
env = Sofar( excludes4( etat_me1, etat_me2, etat_me3, etat_me4 ) );
|
56 |
|
|
OK = env => shared_me >= 0;
|
57 |
|
|
--%MAIN;
|
58 |
|
|
--%PROPERTY OK=true;
|
59 |
|
|
tel
|