lustrec / test / src / kind_fmcad08 / protocol / swimmingpool_1.lus @ 22fe1c93
History | View | Annotate | Download (2.72 KB)
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 |
var x1, x2, x3, x4, x5, x6, x7, p1, p2 : int; |
87 |
env : bool; |
88 |
let |
89 |
(x1, x2, x3, x4, x5, x6, x7, p1, p2) = |
90 |
swimingpool(e1, e2, e3, e4, e5, e6, init_p1, init_p2); |
91 |
env = Sofar( excludes6( e1, e2, e3, e4, e5, e6 ) ) and |
92 |
0 <= First(init_p1) and 0 <= First(init_p2) and First(init_p1) < 1000 and First(init_p2) < 1000; |
93 |
OK = env => x1+x2+x3+x4+x5+x6+x7 <= p1+p2; |
94 |
--%PROPERTY OK=true; |
95 |
--%MAIN; |
96 |
tel |