Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (2.65 KB)

1

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