1 |
b8dc00eb
|
bourbouh
|
node First( X : int ) returns ( First : int );
|
2 |
|
|
let
|
3 |
|
|
First = X -> pre First;
|
4 |
|
|
tel
|
5 |
|
|
node Sofar( X : bool ) returns ( Sofar : bool );
|
6 |
|
|
let
|
7 |
|
|
Sofar = X -> X or pre Sofar;
|
8 |
|
|
tel
|
9 |
|
|
node excludes3( X1, X2, X3 : bool ) returns ( excludes : bool );
|
10 |
|
|
let
|
11 |
|
|
excludes = not ( X1 and X2 or X1 and X3 or X2 and X3 );
|
12 |
|
|
tel
|
13 |
|
|
node synapse(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
|
14 |
|
|
returns(invalid_s, valid_s, dirty_s : int; mem_init_s : int );
|
15 |
|
|
var
|
16 |
|
|
garde_s1, garde_s2, garde_s3 : bool;
|
17 |
|
|
let
|
18 |
|
|
garde_s1 = pre invalid_s>=1;
|
19 |
|
|
garde_s2 = pre valid_s>=1;
|
20 |
|
|
garde_s3 = pre invalid_s>=1;
|
21 |
|
|
mem_init_s = init_invalid_s -> pre mem_init_s;
|
22 |
|
|
invalid_s = mem_init_s ->
|
23 |
|
|
if(e_s1) then if(garde_s1) then pre invalid_s + pre dirty_s -1 else pre invalid_s else
|
24 |
|
|
if(e_s2) then if(garde_s2) then pre invalid_s + pre dirty_s + pre valid_s -1 else pre invalid_s else
|
25 |
|
|
if(e_s3) then if(garde_s3) then pre invalid_s + pre dirty_s + pre valid_s -1 else pre invalid_s else
|
26 |
|
|
pre invalid_s;
|
27 |
|
|
valid_s = 0 ->
|
28 |
|
|
if(e_s1) then if(garde_s1) then pre valid_s +1 else pre valid_s else
|
29 |
|
|
if(e_s2) then if(garde_s2) then 0 else pre valid_s else
|
30 |
|
|
if(e_s3) then if(garde_s3) then 0 else pre valid_s else
|
31 |
|
|
pre valid_s;
|
32 |
|
|
dirty_s = 0 ->
|
33 |
|
|
if(e_s1) then if(garde_s1) then 0 else pre dirty_s else
|
34 |
|
|
if(e_s2) then if(garde_s2) then 1 else pre dirty_s else
|
35 |
|
|
if(e_s3) then if(garde_s3) then 1 else pre dirty_s else
|
36 |
|
|
pre dirty_s;
|
37 |
|
|
tel
|
38 |
|
|
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
|
39 |
|
|
returns( OK : bool );
|
40 |
2d37a1e1
|
ploc
|
--@ contract guarantees OK;
|
41 |
b8dc00eb
|
bourbouh
|
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
|
42 |
|
|
env : bool;
|
43 |
|
|
let
|
44 |
|
|
( invalid_s, valid_s, dirty_s, mem_init_s ) =
|
45 |
|
|
synapse(e_s1, e_s2, e_s3, init_invalid_s );
|
46 |
|
|
env = Sofar( excludes3(e_s1, e_s2, e_s3) and init_invalid_s >= 0 );
|
47 |
|
|
OK = env => invalid_s+valid_s+dirty_s = First( init_invalid_s );
|
48 |
|
|
--%MAIN;
|
49 |
|
|
--%PROPERTY OK=true;
|
50 |
|
|
tel
|