← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2000/lusk-mccune/lusk-mccune-final/fence

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2000/lusk-mccune/lusk-mccune-final/fence
 
1
(in-package "ACL2")
 
2
 
 
3
(include-book "simulator")
 
4
(include-book "compile")
 
5
 
 
6
(sim
 
7
 
 
8
 '(
 
9
   (DELIVER . 4171) (DELIVER . 8601) (STEP . 2628) (STEP . 5460)
 
10
   (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200)
 
11
   (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124)
 
12
   (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229)
 
13
   (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593)
 
14
   (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074)
 
15
   (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518)
 
16
   (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460)
 
17
   (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326)
 
18
   (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137)
 
19
   (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715)
 
20
   (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379)
 
21
   (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157)
 
22
   (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482)
 
23
   (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398)
 
24
   (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265)
 
25
   (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958)
 
26
   (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573)
 
27
   (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629)
 
28
   (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772)
 
29
   (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976)
 
30
   (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251)
 
31
   (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840)
 
32
   (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336)
 
33
   (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028)
 
34
   (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379)
 
35
   (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157)
 
36
   (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482)
 
37
   (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398)
 
38
   (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265)
 
39
   (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958)
 
40
   (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573)
 
41
   (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629)
 
42
   (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772)
 
43
   (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976)
 
44
   (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251)
 
45
   (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840)
 
46
   (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336)
 
47
   (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028)
 
48
   (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392)
 
49
   (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888)
 
50
   (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904)
 
51
   (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200)
 
52
   (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124)
 
53
   (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229)
 
54
   (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593)
 
55
   (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074)
 
56
   (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518)
 
57
   (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460)
 
58
   (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326)
 
59
   (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137)
 
60
   (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715)
 
61
   (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379)
 
62
   (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157)
 
63
   (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482)
 
64
   (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398)
 
65
   (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265)
 
66
   (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958)
 
67
   (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573)
 
68
   (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629)
 
69
   (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772)
 
70
   (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976)
 
71
   (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251)
 
72
   (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840)
 
73
   (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336)
 
74
   (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028)
 
75
   (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379)
 
76
   (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157)
 
77
   (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482)
 
78
   (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398)
 
79
   (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265)
 
80
   (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958)
 
81
   (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573)
 
82
   (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629)
 
83
   (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772)
 
84
   (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976)
 
85
   (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251)
 
86
   (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840)
 
87
   (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336)
 
88
   (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028)
 
89
   (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392)
 
90
   (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888)
 
91
   (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904)
 
92
   (DELIVER . 7828)
 
93
 
 
94
   (DELIVER . 4171) (DELIVER . 8601) (STEP . 2628) (STEP . 5460)
 
95
   (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200)
 
96
   (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124)
 
97
   (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229)
 
98
   (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593)
 
99
   (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074)
 
100
   (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518)
 
101
   (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460)
 
102
   (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326)
 
103
   (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137)
 
104
   (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715)
 
105
   (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379)
 
106
   (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157)
 
107
   (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482)
 
108
   (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398)
 
109
   (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265)
 
110
   (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958)
 
111
   (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573)
 
112
   (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629)
 
113
   (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772)
 
114
   (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976)
 
115
   (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251)
 
116
   (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840)
 
117
   (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336)
 
118
   (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028)
 
119
   (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379)
 
120
   (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157)
 
121
   (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482)
 
122
   (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398)
 
123
   (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265)
 
124
   (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958)
 
125
   (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573)
 
126
   (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629)
 
127
   (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772)
 
128
   (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976)
 
129
   (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251)
 
130
   (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840)
 
131
   (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336)
 
132
   (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028)
 
133
   (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392)
 
134
   (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888)
 
135
   (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904)
 
136
   (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200)
 
137
   (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124)
 
138
   (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229)
 
139
   (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593)
 
140
   (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074)
 
141
   (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518)
 
142
   (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460)
 
143
   (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326)
 
144
   (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137)
 
145
   (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715)
 
146
   (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379)
 
147
   (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157)
 
148
   (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482)
 
149
   (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398)
 
150
   (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265)
 
151
   (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958)
 
152
   (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573)
 
153
   (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629)
 
154
   (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772)
 
155
   (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976)
 
156
   (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251)
 
157
   (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840)
 
158
   (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336)
 
159
   (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028)
 
160
   (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379)
 
161
   (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157)
 
162
   (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482)
 
163
   (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398)
 
164
   (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265)
 
165
   (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958)
 
166
   (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573)
 
167
   (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629)
 
168
   (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772)
 
169
   (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976)
 
170
   (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251)
 
171
   (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840)
 
172
   (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336)
 
173
   (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028)
 
174
   (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392)
 
175
   (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888)
 
176
   (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904)
 
177
   (DELIVER . 7828)
 
178
 
 
179
   (DELIVER . 4171) (DELIVER . 8601) (STEP . 2628) (STEP . 5460)
 
180
   (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200)
 
181
   (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124)
 
182
   (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229)
 
183
   (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593)
 
184
   (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074)
 
185
   (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518)
 
186
   (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460)
 
187
   (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326)
 
188
   (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137)
 
189
   (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715)
 
190
   (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379)
 
191
   (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157)
 
192
   (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482)
 
193
   (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398)
 
194
   (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265)
 
195
   (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958)
 
196
   (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573)
 
197
   (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629)
 
198
   (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772)
 
199
   (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976)
 
200
   (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251)
 
201
   (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840)
 
202
   (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336)
 
203
   (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028)
 
204
   (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379)
 
205
   (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157)
 
206
   (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482)
 
207
   (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398)
 
208
   (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265)
 
209
   (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958)
 
210
   (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573)
 
211
   (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629)
 
212
   (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772)
 
213
   (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976)
 
214
   (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251)
 
215
   (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840)
 
216
   (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336)
 
217
   (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028)
 
218
   (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392)
 
219
   (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888)
 
220
   (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904)
 
221
   (STEP . 91) (DELIVER . 1679) (STEP . 7016) (STEP . 1200)
 
222
   (DELIVER . 4466) (DELIVER . 3037) (DELIVER . 297) (DELIVER . 6124)
 
223
   (DELIVER . 318) (DELIVER . 8179) (STEP . 30) (STEP . 9229)
 
224
   (STEP . 2578) (DELIVER . 397) (DELIVER . 8538) (STEP . 8593)
 
225
   (STEP . 3167) (STEP . 7727) (STEP . 6736) (STEP . 7074)
 
226
   (DELIVER . 3575) (DELIVER . 7403) (STEP . 5457) (STEP . 5518)
 
227
   (DELIVER . 4937) (DELIVER . 7809) (DELIVER . 4283) (STEP . 3460)
 
228
   (STEP . 5613) (DELIVER . 7930) (STEP . 7872) (DELIVER . 7326)
 
229
   (STEP . 6265) (DELIVER . 4308) (DELIVER . 9783) (STEP . 6137)
 
230
   (DELIVER . 2433) (STEP . 5497) (DELIVER . 3809) (DELIVER . 4715)
 
231
   (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379)
 
232
   (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157)
 
233
   (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482)
 
234
   (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398)
 
235
   (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265)
 
236
   (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958)
 
237
   (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573)
 
238
   (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629)
 
239
   (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772)
 
240
   (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976)
 
241
   (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251)
 
242
   (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840)
 
243
   (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336)
 
244
   (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028)
 
245
   (DELIVER . 4620) (STEP . 4009) (DELIVER . 2804) (STEP . 4379)
 
246
   (STEP . 5861) (DELIVER . 5774) (DELIVER . 5009) (DELIVER . 1157)
 
247
   (DELIVER . 6810) (DELIVER . 7092) (STEP . 7881) (DELIVER . 1482)
 
248
   (DELIVER . 8311) (DELIVER . 9081) (DELIVER . 9421) (DELIVER . 5398)
 
249
   (STEP . 1479) (STEP . 9636) (STEP . 7004) (STEP . 7265)
 
250
   (DELIVER . 5280) (DELIVER . 2882) (STEP . 3706) (DELIVER . 3958)
 
251
   (DELIVER . 1606) (STEP . 6121) (DELIVER . 2129) (STEP . 573)
 
252
   (STEP . 7854) (DELIVER . 4293) (STEP . 5735) (STEP . 3629)
 
253
   (DELIVER . 7005) (STEP . 1922) (STEP . 7669) (DELIVER . 1772)
 
254
   (STEP . 5202) (STEP . 2576) (STEP . 7091) (DELIVER . 3976)
 
255
   (STEP . 6828) (DELIVER . 5815) (DELIVER . 3000) (DELIVER . 5251)
 
256
   (DELIVER . 7082) (DELIVER . 1645) (DELIVER . 5567) (STEP . 9840)
 
257
   (STEP . 2061) (STEP . 2473) (STEP . 4960) (STEP . 1926) (STEP . 6336)
 
258
   (STEP . 2559) (STEP . 7669) (DELIVER . 3834) (DELIVER . 8028)
 
259
   (DELIVER . 4968) (STEP . 344) (STEP . 1733) (DELIVER . 1392)
 
260
   (STEP . 6026) (DELIVER . 1112) (DELIVER . 8843) (STEP . 6888)
 
261
   (STEP . 7271) (STEP . 8412) (STEP . 6133) (STEP . 8764) (STEP . 4904)
 
262
   (DELIVER . 7828)
 
263
   )
 
264
 
 
265
 0;; step counter
 
266
 
 
267
 nil;; trace
 
268
 
 
269
 (list                                  ; mstate = multiprocess state with connections
 
270
 
 
271
   ;; This program simulates a barrier algorithm implemented by the managers
 
272
   ;; for the clients.  (There are no daemons or consoles.)  The three clients
 
273
   ;; each must call the barrier (send fence-in message) before they can
 
274
   ;; continue (receive fence-out message).  All connections are
 
275
   ;; pre-established in the initial mstate.
 
276
   
 
277
 
 
278
  (list                                 ; list of pstates, one for each process
 
279
 
 
280
   ;;------------------------------------------------------------- manager 0
 
281
 
 
282
   ;; Each manager is connected to its neighbors in the ring and to a client
 
283
   ;; process.  The managers must collectively wait for all the clients to
 
284
   ;; enter the barrier (send their managers fence-in messages) before they
 
285
   ;; are allowed to leave (they wait for fence-out messages from their managers.)
 
286
 
 
287
   (list                                ; first manager pstate
 
288
 
 
289
    '(host1 1)                          ; process id for manager 0
 
290
 
 
291
    (compile-list                       ; main manager program
 
292
     '(
 
293
       (asgn select-set (lhs-fd cli-fd))
 
294
       (while 'true
 
295
         (select select-set selected-set)
 
296
         (if (member lhs-fd selected-set)
 
297
             (call lhs-handler)
 
298
           )
 
299
         (if (member cli-fd selected-set)
 
300
             (call cli-handler)
 
301
           )
 
302
         )
 
303
       (return)                         ; end of main manager program
 
304
 
 
305
 
 
306
       (procedure lhs-handler)          ; lhs-handler
 
307
       (receive lhs-fd lhs-message)
 
308
       (asgn cmd (cdr (assoc 'cmd lhs-message)))
 
309
 
 
310
       (if (equal cmd 'man-fence-in)
 
311
           (call man-fence-in-handler)
 
312
         )
 
313
       (if (equal cmd 'man-fence-out)
 
314
           (call man-fence-out-handler)
 
315
         )
 
316
       (return)                         ; end of lhs-handler
 
317
 
 
318
 
 
319
       (procedure cli-handler)          ; client handler in manager
 
320
       (receive cli-fd cli-message)
 
321
       (asgn cmd (cdr (assoc 'cmd cli-message)))
 
322
       (if (equal cmd 'cli-fence-in)
 
323
           (call cli-fence-in-handler)
 
324
         )
 
325
       (if (not (equal cmd 'cli-fence-in))
 
326
           (asgn status 'ERROR-unxpected-message-not-fence-in)
 
327
         )
 
328
       (return)                         ; end of cli-handler
 
329
 
 
330
 
 
331
                                        ; beginning of specific message handlers
 
332
      
 
333
 
 
334
       (procedure cli-fence-in-handler) ; manager gets fence-in message from client
 
335
       (asgn client-fenced-in 1)
 
336
       (if (equal man-id 0)
 
337
           (send rhs-fd (('cmd . 'man-fence-in)))
 
338
         )
 
339
       (if (not (equal man-id 0))
 
340
           (if (equal fence-in-msg-here 1)
 
341
               (send rhs-fd (('cmd . 'man-fence-in)))
 
342
             )
 
343
         )
 
344
       (return)                         ; end of cli-fence-in handler
 
345
 
 
346
       (procedure man-fence-in-handler) ; manager gets fence-in message from lhs
 
347
       (asgn fence-in-msg-here 1)
 
348
       (if (equal man-id 0)
 
349
           (send rhs-fd (('cmd . 'man-fence-out)))
 
350
         )
 
351
       (if (not (equal man-id 0))
 
352
           (if (equal client-fenced-in 1)
 
353
               (send rhs-fd (('cmd . 'man-fence-in)))
 
354
             )
 
355
         )
 
356
       (return)                         ; end of man-fence-in-handler
 
357
 
 
358
       (procedure man-fence-out-handler) ; manager gets fence out message from lhs
 
359
       (send cli-fd (('cmd . 'cli-fence-out)))
 
360
       (if (not (equal man-id 0))
 
361
           (send rhs-fd (('cmd . 'man-fence-out)))
 
362
         )              
 
363
       (return)                         ; end of man-fence-out-handler
 
364
 
 
365
       )                                ; uncompiled program
 
366
     nil
 
367
     )                                  ; compiled program
 
368
    1                                   ; program counter
 
369
    nil                                 ; xstack
 
370
    '((man-id . 0)                      ; initial memory
 
371
      (fence-in-msg-here . 0)
 
372
      (client-fenced-in  . 0) 
 
373
      (lhs-fd            . 3)
 
374
      (rhs-fd            . 4)
 
375
      (mpd-fd            . 5)
 
376
      (cli-fd            . 6)
 
377
      )
 
378
    )                                   ; end of pstate
 
379
 
 
380
   ;;------------------------------------------------------------- manager 1
 
381
 
 
382
   ;; Same as for manager 0
 
383
 
 
384
   (list                                ; first manager pstate
 
385
 
 
386
    '(host2 1)                          ; process id for manager 0
 
387
 
 
388
    (compile-list                       ; main manager program
 
389
     '(
 
390
       (asgn select-set (lhs-fd cli-fd))
 
391
       (while 'true
 
392
         (select select-set selected-set)
 
393
         (if (member lhs-fd selected-set)
 
394
             (call lhs-handler)
 
395
           )
 
396
         (if (member cli-fd selected-set)
 
397
             (call cli-handler)
 
398
           )
 
399
         )
 
400
       (return)                         ; end of main manager program
 
401
 
 
402
 
 
403
       (procedure lhs-handler)          ; lhs-handler
 
404
       (receive lhs-fd lhs-message)
 
405
       (asgn cmd (cdr (assoc 'cmd lhs-message)))
 
406
 
 
407
       (if (equal cmd 'man-fence-in)
 
408
           (call man-fence-in-handler)
 
409
         )
 
410
       (if (equal cmd 'man-fence-out)
 
411
           (call man-fence-out-handler)
 
412
         )
 
413
       (return)                         ; end of lhs-handler
 
414
 
 
415
 
 
416
       (procedure cli-handler)          ; client handler in manager
 
417
       (receive cli-fd cli-message)
 
418
       (asgn cmd (cdr (assoc 'cmd cli-message)))
 
419
       (if (equal cmd 'cli-fence-in)
 
420
           (call cli-fence-in-handler)
 
421
         )
 
422
       (if (not (equal cmd 'cli-fence-in))
 
423
           (asgn status 'ERROR-unxpected-message-not-fence-in)
 
424
         )
 
425
       (return)                         ; end of cli-handler
 
426
 
 
427
 
 
428
                                        ; beginning of specific message handlers
 
429
      
 
430
 
 
431
       (procedure cli-fence-in-handler) ; manager gets fence-in message from client
 
432
       (asgn client-fenced-in 1)
 
433
       (if (equal man-id 0)
 
434
           (send rhs-fd (('cmd . 'man-fence-in)))
 
435
         )
 
436
       (if (not (equal man-id 0))
 
437
           (if (equal fence-in-msg-here 1)
 
438
               (send rhs-fd (('cmd . 'man-fence-in)))
 
439
             )
 
440
         )
 
441
       (return)                         ; end of cli-fence-in handler
 
442
 
 
443
       (procedure man-fence-in-handler) ; manager gets fence-in message from lhs
 
444
       (asgn fence-in-msg-here 1)
 
445
       (if (equal man-id 0)
 
446
           (send rhs-fd (('cmd . 'man-fence-out)))
 
447
         )
 
448
       (if (not (equal man-id 0))
 
449
           (if (equal client-fenced-in 1)
 
450
               (send rhs-fd (('cmd . 'man-fence-in)))
 
451
             )
 
452
         )
 
453
       (return)                         ; end of man-fence-in-handler
 
454
 
 
455
       (procedure man-fence-out-handler) ; manager gets fence out message from lhs
 
456
       (send cli-fd (('cmd . 'cli-fence-out)))
 
457
       (if (not (equal man-id 0))
 
458
           (send rhs-fd (('cmd . 'man-fence-out)))
 
459
         )              
 
460
       (return)                         ; end of man-fence-out-handler
 
461
 
 
462
       )                                ; uncompiled program
 
463
     nil
 
464
     )                                  ; compiled program
 
465
    1                                   ; program counter
 
466
    nil                                 ; xstack
 
467
    '((man-id . 1)                      ; initial memory
 
468
      (fence-in-msg-here . 0)
 
469
      (client-fenced-in  . 0) 
 
470
      (lhs-fd            . 3)
 
471
      (rhs-fd            . 4)
 
472
      (mpd-fd            . 5)
 
473
      (cli-fd            . 6)
 
474
      )
 
475
    )                                   ; end of pstate
 
476
 
 
477
   ;;------------------------------------------------------------- manager 2
 
478
 
 
479
   (list                                ; first manager pstate
 
480
 
 
481
   ;; same as for managers 0 and 1
 
482
 
 
483
    '(host3 1)                          ; process id for manager 0
 
484
 
 
485
    (compile-list                       ; main manager program
 
486
     '(
 
487
       (asgn select-set (lhs-fd cli-fd))
 
488
       (while 'true
 
489
         (select select-set selected-set)
 
490
         (if (member lhs-fd selected-set)
 
491
             (call lhs-handler)
 
492
           )
 
493
         (if (member cli-fd selected-set)
 
494
             (call cli-handler)
 
495
           )
 
496
         )
 
497
       (return)                         ; end of main manager program
 
498
 
 
499
 
 
500
       (procedure lhs-handler)          ; lhs-handler
 
501
       (receive lhs-fd lhs-message)
 
502
       (asgn cmd (cdr (assoc 'cmd lhs-message)))
 
503
 
 
504
       (if (equal cmd 'man-fence-in)
 
505
           (call man-fence-in-handler)
 
506
         )
 
507
       (if (equal cmd 'man-fence-out)
 
508
           (call man-fence-out-handler)
 
509
         )
 
510
       (return)                         ; end of lhs-handler
 
511
 
 
512
 
 
513
       (procedure cli-handler)          ; client handler in manager
 
514
       (receive cli-fd cli-message)
 
515
       (asgn cmd (cdr (assoc 'cmd cli-message)))
 
516
       (if (equal cmd 'cli-fence-in)
 
517
           (call cli-fence-in-handler)
 
518
         )
 
519
       (if (not (equal cmd 'cli-fence-in))
 
520
           (asgn status 'ERROR-unxpected-message-not-fence-in)
 
521
         )
 
522
       (return)                         ; end of cli-handler
 
523
 
 
524
 
 
525
                                        ; beginning of specific message handlers
 
526
      
 
527
 
 
528
       (procedure cli-fence-in-handler) ; manager gets fence-in message from client
 
529
       (asgn client-fenced-in 1)
 
530
       (if (equal man-id 0)
 
531
           (send rhs-fd (('cmd . 'man-fence-in)))
 
532
         )
 
533
       (if (not (equal man-id 0))
 
534
           (if (equal fence-in-msg-here 1)
 
535
               (send rhs-fd (('cmd . 'man-fence-in)))
 
536
             )
 
537
         )
 
538
       (return)                         ; end of cli-fence-in handler
 
539
 
 
540
       (procedure man-fence-in-handler) ; manager gets fence-in message from lhs
 
541
       (asgn fence-in-msg-here 1)
 
542
       (if (equal man-id 0)
 
543
           (send rhs-fd (('cmd . 'man-fence-out)))
 
544
         )
 
545
       (if (not (equal man-id 0))
 
546
           (if (equal client-fenced-in 1)
 
547
               (send rhs-fd (('cmd . 'man-fence-in)))
 
548
             )
 
549
         )
 
550
       (return)                         ; end of man-fence-in-handler
 
551
 
 
552
       (procedure man-fence-out-handler) ; manager gets fence out message from lhs
 
553
       (send cli-fd (('cmd . 'cli-fence-out)))
 
554
       (if (not (equal man-id 0))
 
555
           (send rhs-fd (('cmd . 'man-fence-out)))
 
556
         )              
 
557
       (return)                         ; end of man-fence-out-handler
 
558
 
 
559
       )                                ; uncompiled program
 
560
     nil
 
561
     )                                  ; compiled program
 
562
    1                                   ; program counter
 
563
    nil                                 ; xstack
 
564
    '((man-id . 2)                      ; initial memory
 
565
      (fence-in-msg-here . 0)
 
566
      (client-fenced-in  . 0) 
 
567
      (lhs-fd            . 3)
 
568
      (rhs-fd            . 4)
 
569
      (mpd-fd            . 5)
 
570
      (cli-fd            . 6)
 
571
      )
 
572
    )                                   ; end of pstate
 
573
 
 
574
   ;;-------------------------------------------------------- client 0
 
575
 
 
576
   ;; Each client sends its manager a fence-in message and waits for a
 
577
   ;; fence-out message.
 
578
 
 
579
   (list                                ; client on first host
 
580
 
 
581
    '(host1 2)                          ; process id for first client
 
582
 
 
583
    (compile-list                       ; client doing fence
 
584
     '(
 
585
       (send man-fd (('cmd . 'cli-fence-in)))
 
586
       (receive man-fd man-message)
 
587
       (asgn cmd (cdr (assoc 'cmd man-message)))
 
588
       (if (not (equal cmd 'cli-fence-out))
 
589
           (asgn status 'ERROR-unexpected-message-not-cli-fence-out)
 
590
         )
 
591
       (return)                         ; end of client
 
592
 
 
593
       )                                ; uncompiled program
 
594
     nil
 
595
     )                                  ; compiled program
 
596
    1                                   ; program counter
 
597
    nil                                 ; xstack
 
598
    '((man-fd . 1))                     ; initial memory
 
599
    )                                   ; end of pstate
 
600
 
 
601
   ;;-------------------------------------------------------- client 1
 
602
 
 
603
   ;; Same as for client 0
 
604
 
 
605
   (list                                ; client on first host
 
606
 
 
607
    '(host2 2)                          ; process id for first client
 
608
 
 
609
    (compile-list                       ; client doing fence
 
610
     '(
 
611
       (send man-fd (('cmd . 'cli-fence-in)))
 
612
       (receive man-fd man-message)
 
613
       (asgn cmd (cdr (assoc 'cmd man-message)))
 
614
       (if (not (equal cmd 'cli-fence-out))
 
615
           (asgn status 'ERROR-unexpected-message-not-cli-fence-out)
 
616
         )
 
617
       (return)                         ; end of client
 
618
 
 
619
       )                                ; uncompiled program
 
620
     nil
 
621
     )                                  ; compiled program
 
622
    1                                   ; program counter
 
623
    nil                                 ; xstack
 
624
    '((man-fd . 1))                     ; initial memory
 
625
    )                                   ; end of pstate
 
626
 
 
627
   ;;-------------------------------------------------------- client 2
 
628
 
 
629
   ;; Same as for clients 0 and 1
 
630
 
 
631
   (list                                ; client on first host
 
632
 
 
633
    '(host3 2)                          ; process id for first client
 
634
 
 
635
    (compile-list                       ; client doing fence
 
636
     '(
 
637
       (send man-fd (('cmd . 'cli-fence-in)))
 
638
       (receive man-fd man-message)
 
639
       (asgn cmd (cdr (assoc 'cmd man-message)))
 
640
       (if (not (equal cmd 'cli-fence-out))
 
641
           (asgn status 'ERROR-unexpected-message-not-cli-fence-out)
 
642
         )
 
643
       (return)                         ; end of client
 
644
 
 
645
       )                                ; uncompiled program
 
646
     nil
 
647
     )                                  ; compiled program
 
648
    1                                   ; program counter
 
649
    nil                                 ; xstack
 
650
    '((man-fd . 1))                     ; initial memory
 
651
    )                                   ; end of pstate
 
652
 
 
653
   ;;------------------------------------------------------------
 
654
 
 
655
   )                                    ; end of pstate list
 
656
 
 
657
  (list                                 ; connection list
 
658
 
 
659
   ;; The managers are connected in a ring and each client is connected to one
 
660
   ;; manager. 
 
661
 
 
662
   '(((host1 1) 4 (host2 1) 3) nil nil)
 
663
   '(((host2 1) 4 (host3 1) 3) nil nil)
 
664
   '(((host3 1) 4 (host1 1) 3) nil nil)
 
665
 
 
666
   '(((host1 1) 6 (host1 2) 1) nil nil)
 
667
   '(((host2 1) 6 (host2 2) 1) nil nil)
 
668
   '(((host3 1) 6 (host3 2) 1) nil nil)
 
669
 
 
670
   '(((host2 1) 3 (host1 1) 4) nil nil)
 
671
   '(((host3 1) 3 (host2 1) 4) nil nil)
 
672
   '(((host1 1) 3 (host3 1) 4) nil nil)
 
673
                            
 
674
   '(((host1 2) 1 (host1 1) 6) nil nil)
 
675
   '(((host2 2) 1 (host2 1) 6) nil nil)
 
676
   '(((host3 2) 1 (host3 1) 6) nil nil)
 
677
 
 
678
   )                                    ; end of connections
 
679
 
 
680
  (list                                 ; list of sockets being listened on
 
681
 
 
682
   )                                    ; end of listening list
 
683
 
 
684
  nil                                   ; program-list
 
685
 
 
686
  )                                     ; End of multiprocess-state
 
687
 
 
688
 )