|
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
|
--@ ensures OK;
|
|
123
|
node top(e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 : bool)
|
|
124
|
returns ( OK : bool );
|
|
125
|
var x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13 : int;
|
|
126
|
env : bool;
|
|
127
|
let
|
|
128
|
(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);
|
|
129
|
|
|
130
|
env = Sofar( excludes12( e01, e02, e03, e04, e05, e06, e07, e08, e09, e10, e11, e12 ) and x1 < 32767 );
|
|
131
|
OK = env => x1 >= 0;
|
|
132
|
--!k:2;
|
|
133
|
--!PROPERTY: OK=true;
|
|
134
|
--%MAIN;
|
|
135
|
tel
|