Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (5.66 KB)

1

    
2
node Sofar( X : bool ) returns ( Sofar : bool );
3
let
4
    Sofar = X -> X and pre Sofar;
5
tel
6

    
7
node excludes12( X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12 : bool ) returns ( excludes : bool );
8
let
9
    excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 and not X10 and not X11 and not X12 or
10
                  X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 and not X10 and not X11 and not X12 or
11
              not X1 and     X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 and not X10 and not X11 and not X12 or
12
              not X1 and not X2 and     X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 and not X10 and not X11 and not X12 or
13
              not X1 and not X2 and not X3 and     X4 and not X5 and not X6 and not X7 and not X8 and not X9 and not X10 and not X11 and not X12 or
14
              not X1 and not X2 and not X3 and not X4 and     X5 and not X6 and not X7 and not X8 and not X9 and not X10 and not X11 and not X12 or
15
              not X1 and not X2 and not X3 and not X4 and not X5 and     X6 and not X7 and not X8 and not X9 and not X10 and not X11 and not X12 or
16
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and     X7 and not X8 and not X9 and not X10 and not X11 and not X12 or
17
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and     X8 and not X9 and not X10 and not X11 and not X12 or
18
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and     X9 and not X10 and not X11 and not X12 or
19
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 and     X10 and not X11 and not X12 or
20
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 and not X10 and     X11 and not X12 or
21
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 and not X10 and not X11 and     X12;
22
tel
23

    
24
node peterson(e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool) returns (x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13 : int);
25
var
26
   g01, g02, g03, g04, g05, g06, g07, g08, g09, g10, g11, g12 : bool;
27
let
28

    
29
   g01 = pre x0>=1 and pre x4>=1;
30
   g02 = pre x1 >= 1 and pre x6 >= 1;
31
   g03 = pre x1>=1 and pre x7>=1;
32
   g04 = pre x2>=1 and pre x9>=1;
33
   g05 = pre x2>=1 and pre x6>=1;
34
   g06 = pre x3>=1 and pre x5>=1;
35
   g07 = pre x9>=1 and pre x10>=1;
36
   g08 = pre x7>=1 and pre x11>=1;
37
   g09 = pre x6>=1 and pre x11>=1;
38
   g10 = pre x4>=1 and pre x12>=1;
39
   g11 = pre x7>=1 and pre x12>=1;
40
   g12 = pre x8>=1 and pre x13>=1;
41

    
42
   x0 = 1 -> 
43
   if(e01) then if(g01) then pre x0-1 else pre x0 else 
44
   if(e06) then if(g06) then pre x0+1 else pre x0 else 
45
   pre x0;
46

    
47
   x1 = 0 -> 
48
   if(e01) then if(g01) then pre x1+1 else pre x1 else 
49
   if(e02) then if(g02) then pre x1-1 else pre x1 else 
50
   if(e03) then if(g03) then pre x1-1 else pre x1 else 
51
   pre x1;
52

    
53
   x2 = 0 -> 
54
   if(e02) then if(g02) then pre x2+1 else pre x2 else 
55
   if(e03) then if(g03) then pre x2+1 else pre x2 else 
56
   if(e04) then if(g04) then pre x2-1 else pre x2 else 
57
   if(e05) then if(g05) then pre x2-1 else pre x2 else 
58
   pre x2;
59

    
60
   x3 = 0 -> 
61
   if(e04) then if(g04) then pre x3+1 else pre x3 else 
62
   if(e05) then if(g05) then pre x3+1 else pre x3 else 
63
   if(e06) then if(g06) then pre x3-1 else pre x3 else 
64
   pre x3;
65

    
66
   x4 = 1 -> 
67
   if(e01) then if(g01) then pre x4-1 else pre x4 else 
68
   if(e06) then if(g06) then pre x4+1 else pre x4 else 
69
   pre x4;
70

    
71
   x5 = 0 -> 
72
   if(e01) then if(g01) then pre x5+1 else pre x5 else 
73
   if(e06) then if(g06) then pre x5-1 else pre x5 else 
74
   pre x5;
75

    
76
   x6 = 0 -> 
77
   if(e02) then if(g02) then pre x6-1 else pre x6 else 
78
   if(e08) then if(g08) then pre x6+1 else pre x6 else 
79
   pre x6;
80

    
81
   x7 = 1 -> 
82
   if(e02) then if(g02) then pre x7+1 else pre x7 else 
83
   if(e08) then if(g08) then pre x7-1 else pre x7 else 
84
   pre x7;
85

    
86
   x8 = 0 -> 
87
   if(e07) then if(g07) then pre x8+1 else pre x8 else 
88
   if(e12) then if(g12) then pre x8-1 else pre x8 else 
89
   pre x8;
90

    
91
   x9 = 1 -> 
92
   if(e07) then if(g07) then pre x9-1 else pre x9 else 
93
   if(e12) then if(g12) then pre x9+1 else pre x9 else 
94
   pre x9;
95

    
96
   x10 = 1 -> 
97
   if(e07) then if(g07) then pre x10-1 else pre x10 else 
98
   if(e12) then if(g12) then pre x10+1 else pre x10 else 
99
   pre x10;
100

    
101
   x11 = 0 -> 
102
   if(e07) then if(g07) then pre x11+1 else pre x11 else 
103
   if(e08) then if(g08) then pre x11-1 else pre x11 else 
104
   if(e09) then if(g09) then pre x11-1 else pre x11 else 
105
   pre x11;
106

    
107
   x12 = 0 -> 
108
   if(e08) then if(g08) then pre x12+1 else pre x12 else 
109
   if(e09) then if(g09) then pre x12+1 else pre x12 else 
110
   if(e10) then if(g10) then pre x12-1 else pre x12 else 
111
   if(e11) then if(g11) then pre x12-1 else pre x12 else 
112
   pre x12;
113

    
114
   x13 = 0 -> 
115
   if(e10) then if(g10) then pre x13+1 else pre x13 else 
116
   if(e11) then if(g11) then pre x13+1 else pre x13 else 
117
   if(e12) then if(g12) then pre x13-1 else pre x13 else 
118
   pre x13;
119

    
120
tel
121

    
122
node top(e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool)
123
returns ( OK : bool );
124
    var x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13 : int;
125
        env : bool;
126
let
127
   (x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = peterson(e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12);
128

    
129
    env = Sofar( excludes12( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 ) and x0 < 32767 and x1 < 32767 and x2 < 32767 and x3 < 32767 );
130
    OK = env => x0 >= 0 and x1 >= 0 and x2 >= 0 and x3 >= 0;
131
    --%PROPERTY OK=true;
132
    --%MAIN;
133
tel