Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (2.7 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

    
16

    
17
node excludes6( X1, X2, X3, X4, X5, X6 : bool ) returns ( excludes : bool );
18
let
19
    excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 or
20
                  X1 and not X2 and not X3 and not X4 and not X5 and not X6 or
21
              not X1 and     X2 and not X3 and not X4 and not X5 and not X6 or
22
              not X1 and not X2 and     X3 and not X4 and not X5 and not X6 or
23
              not X1 and not X2 and not X3 and     X4 and not X5 and not X6 or
24
              not X1 and not X2 and not X3 and not X4 and     X5 and not X6 or
25
              not X1 and not X2 and not X3 and not X4 and not X5 and     X6;
26
tel
27

    
28
node swimingpool(e1, e2, e3, e4, e5, e6 : bool;init_p1, init_p2 : int)returns 
29
(x1, x2, x3, x4, x5, x6, x7, p1, p2 : int);
30
var
31
	g1, g2, g3, g4, g5, g6 : bool;
32
let
33

    
34
	g1 = false -> pre x6>=1;
35
	g2 = false -> pre x1>=1 and pre x7>=1;
36
	g3 = false -> pre x2>=1;
37
	g4 = false -> pre x3>=1 and pre x6>=1;
38
	g5 = false -> pre x4>=1;
39
	g6 = false -> pre x5>=1;
40

    
41
	x1 = 0 -> 
42
	if(e1) then if(g1) then pre x1+1 else pre x1 else 
43
	if(e2) then if(g2) then pre x1-1 else pre x1 else 
44
	pre x1;
45

    
46
	x2 = 0 -> 
47
	if(e2) then if(g2) then pre x2+1 else pre x2 else 
48
	if(e3) then if(g3) then pre x2-1 else pre x2 else 
49
	pre x2;
50

    
51
	x3 = 0 -> 
52
	if(e3) then if(g3) then pre x3+1 else pre x3 else 
53
	if(e4) then if(g4) then pre x3-1 else pre x3 else 
54
	pre x3;
55

    
56
	x4 = 0 -> 
57
	if(e4) then if(g4) then pre x4+1 else pre x4 else 
58
	if(e5) then if(g4) then pre x4-1 else pre x4 else 
59
	pre x4;
60

    
61
	x5 = 0 -> 
62
	if(e5) then if(g5) then pre x5+1 else pre x5 else 
63
	if(e6) then if(g6) then pre x5-1 else pre x5 else 
64
	pre x5;
65

    
66
	x6 = p1 -> 
67
	if(e1) then if(g1) then pre x6-1 else pre x6 else 
68
	if(e3) then if(g3) then pre x6+1 else pre x6 else 
69
	if(e4) then if(g4) then pre x6-1 else pre x6 else 
70
	if(e6) then if(g6) then pre x6+1 else pre x6 else 
71
	pre x6;
72

    
73
	x7 = p2 -> 
74
	if(e2) then if(g2) then pre x7-1 else pre x7 else 
75
	if(e5) then if(g5) then pre x7+1 else pre x7 else 
76
	pre x7;
77

    
78
	p1 = init_p1 -> 
79
	pre p1;
80

    
81
	p2 = init_p2 -> 
82
	pre p2;
83

    
84
tel
85

    
86
node top(e1, e2, e3, e4, e5, e6 : bool;init_p1, init_p2 : int)
87
returns ( OK : bool );
88
    var x1, x2, x3, x4, x5, x6, x7, p1, p2 : int;
89
        env : bool;
90
let
91
    (x1, x2, x3, x4, x5, x6, x7, p1, p2) =
92
        swimingpool(e1, e2, e3, e4, e5, e6, init_p1, init_p2);
93
    env = Sofar( excludes6( e1, e2, e3, e4, e5, e6 ) ) and
94
          0 <= First(init_p1) and 0 <= First(init_p2) and First(init_p1) < 1000 and First(init_p2) < 1000;
95
    OK = env => x3 < 1;
96
    --%PROPERTY OK=true;
97
    --%MAIN;
98
tel