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