|
1
|
--
|
|
2
|
-- Source: David Merchat (node swimingpool)
|
|
3
|
--
|
|
4
|
|
|
5
|
node First( X : int ) returns ( First : int );
|
|
6
|
let
|
|
7
|
First = X -> pre First;
|
|
8
|
tel
|
|
9
|
|
|
10
|
node Sofar( X : bool ) returns ( Sofar : bool );
|
|
11
|
let
|
|
12
|
Sofar = X -> X and pre Sofar;
|
|
13
|
tel
|
|
14
|
|
|
15
|
node excludes6( X1, X2, X3, X4, X5, X6 : bool ) returns ( excludes : bool );
|
|
16
|
let
|
|
17
|
excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 or
|
|
18
|
X1 and not X2 and not X3 and not X4 and not X5 and not X6 or
|
|
19
|
not X1 and X2 and not X3 and not X4 and not X5 and not X6 or
|
|
20
|
not X1 and not X2 and X3 and not X4 and not X5 and not X6 or
|
|
21
|
not X1 and not X2 and not X3 and X4 and not X5 and not X6 or
|
|
22
|
not X1 and not X2 and not X3 and not X4 and X5 and not X6 or
|
|
23
|
not X1 and not X2 and not X3 and not X4 and not X5 and X6;
|
|
24
|
tel
|
|
25
|
|
|
26
|
node swimingpool(e1, e2, e3, e4, e5, e6 : bool;init_p1, init_p2 : int)returns
|
|
27
|
(x1, x2, x3, x4, x5, x6, x7, p1, p2 : int);
|
|
28
|
var
|
|
29
|
g1, g2, g3, g4, g5, g6 : bool;
|
|
30
|
let
|
|
31
|
|
|
32
|
g1 = false -> pre x6>=1;
|
|
33
|
g2 = false -> pre x1>=1 and pre x7>=1;
|
|
34
|
g3 = false -> pre x2>=1;
|
|
35
|
g4 = false -> pre x3>=1 and pre x6>=1;
|
|
36
|
g5 = false -> pre x4>=1;
|
|
37
|
g6 = false -> pre x5>=1;
|
|
38
|
|
|
39
|
x1 = 0 ->
|
|
40
|
if(e1) then if(g1) then pre x1+1 else pre x1 else
|
|
41
|
if(e2) then if(g2) then pre x1-1 else pre x1 else
|
|
42
|
pre x1;
|
|
43
|
|
|
44
|
x2 = 0 ->
|
|
45
|
if(e2) then if(g2) then pre x2+1 else pre x2 else
|
|
46
|
if(e3) then if(g3) then pre x2-1 else pre x2 else
|
|
47
|
pre x2;
|
|
48
|
|
|
49
|
x3 = 0 ->
|
|
50
|
if(e3) then if(g3) then pre x3+1 else pre x3 else
|
|
51
|
if(e4) then if(g4) then pre x3-1 else pre x3 else
|
|
52
|
pre x3;
|
|
53
|
|
|
54
|
x4 = 0 ->
|
|
55
|
if(e4) then if(g4) then pre x4+1 else pre x4 else
|
|
56
|
if(e5) then if(g4) then pre x4-1 else pre x4 else
|
|
57
|
pre x4;
|
|
58
|
|
|
59
|
x5 = 0 ->
|
|
60
|
if(e5) then if(g5) then pre x5+1 else pre x5 else
|
|
61
|
if(e6) then if(g6) then pre x5-1 else pre x5 else
|
|
62
|
pre x5;
|
|
63
|
|
|
64
|
x6 = p1 ->
|
|
65
|
if(e1) then if(g1) then pre x6-1 else pre x6 else
|
|
66
|
if(e3) then if(g3) then pre x6+1 else pre x6 else
|
|
67
|
if(e4) then if(g4) then pre x6-1 else pre x6 else
|
|
68
|
if(e6) then if(g6) then pre x6+1 else pre x6 else
|
|
69
|
pre x6;
|
|
70
|
|
|
71
|
x7 = p2 ->
|
|
72
|
if(e2) then if(g2) then pre x7-1 else pre x7 else
|
|
73
|
if(e5) then if(g5) then pre x7+1 else pre x7 else
|
|
74
|
pre x7;
|
|
75
|
|
|
76
|
p1 = init_p1 ->
|
|
77
|
pre p1;
|
|
78
|
|
|
79
|
p2 = init_p2 ->
|
|
80
|
pre p2;
|
|
81
|
|
|
82
|
tel
|
|
83
|
|
|
84
|
node top(e1, e2, e3, e4, e5, e6 : bool;init_p1, init_p2 : int)
|
|
85
|
returns ( OK : bool );
|
|
86
|
--@ contract guarantees OK;
|
|
87
|
var x1, x2, x3, x4, x5, x6, x7, p1, p2 : int;
|
|
88
|
env : bool;
|
|
89
|
let
|
|
90
|
(x1, x2, x3, x4, x5, x6, x7, p1, p2) =
|
|
91
|
swimingpool(e1, e2, e3, e4, e5, e6, init_p1, init_p2);
|
|
92
|
env = Sofar( excludes6( e1, e2, e3, e4, e5, e6 ) ) and
|
|
93
|
0 <= First(init_p1) and 0 <= First(init_p2) and First(init_p1) < 1000 and First(init_p2) < 1000;
|
|
94
|
OK = env => x1+x2+x3+x4+x5+x6+x7 <= p1+p2;
|
|
95
|
--%PROPERTY OK=true;
|
|
96
|
--%MAIN;
|
|
97
|
tel
|