|
1
|
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 and pre Sofar;
|
|
8
|
tel
|
|
9
|
node excludes3( X1, X2, X3 : bool ) returns ( excludes : bool );
|
|
10
|
let
|
|
11
|
excludes = not ( X1 and X2 and 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 -1+ 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
|
--@ contract guarantees OK;
|
|
41
|
var invalid_s, valid_s, dirty_s : int; mem_init_s : int;
|
|
42
|
R1, R2, R3 : bool;
|
|
43
|
env : bool;
|
|
44
|
let
|
|
45
|
( invalid_s, valid_s, dirty_s, mem_init_s ) =
|
|
46
|
synapse(e_s1, e_s2, e_s3, init_invalid_s );
|
|
47
|
env = Sofar( excludes3(e_s1, e_s2, e_s3) and init_invalid_s >= 0 );
|
|
48
|
R1 = env => dirty_s < 2;
|
|
49
|
R2 = env => (true -> invalid_s+valid_s+dirty_s = pre(invalid_s+valid_s+dirty_s));
|
|
50
|
R3 = env => invalid_s+valid_s+dirty_s = First( init_invalid_s );
|
|
51
|
--%MAIN;
|
|
52
|
OK = R2 and R1 and R3;
|
|
53
|
--%PROPERTY OK=true;
|
|
54
|
tel
|