Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / protocol / swimmingpool_5.lus @ 22fe1c93

History | View | Annotate | Download (2.7 KB)

1 22fe1c93 ploc
--
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 => x4 < 1;
94
    --%PROPERTY OK=true;
95
    --%MAIN;
96
tel