BD20.net 15.4 KB
Newer Older
Jaime Arias's avatar
Jaime Arias committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
#place Mutex  mk(<..>)
#place Idle0 mk(<..>)
#place Wait0
#place Update0
#place Mess0
#place Ack0
#place Idle1 mk(<..>)
#place Wait1
#place Update1
#place Mess1
#place Ack1
#place Idle2 mk(<..>)
#place Wait2
#place Update2
#place Mess2
#place Ack2
#place Idle3 mk(<..>)
#place Wait3
#place Update3
#place Mess3
#place Ack3
#place Idle4 mk(<..>)
#place Wait4
#place Update4
#place Mess4
#place Ack4
#place Idle5 mk(<..>)
#place Wait5
#place Update5
#place Mess5
#place Ack5
#place Idle6 mk(<..>)
#place Wait6
#place Update6
#place Mess6
#place Ack6
#place Idle7 mk(<..>)
#place Wait7
#place Update7
#place Mess7
#place Ack7
#place Idle8 mk(<..>)
#place Wait8
#place Update8
#place Mess8
#place Ack8
#place Idle9 mk(<..>)
#place Wait9
#place Update9
#place Mess9
#place Ack9
#place Idle10 mk(<..>)
#place Wait10
#place Update10
#place Mess10
#place Ack10
#place Idle11 mk(<..>)
#place Wait11
#place Update11
#place Mess11
#place Ack11
#place Idle12 mk(<..>)
#place Wait12
#place Update12
#place Mess12
#place Ack12
#place Idle13 mk(<..>)
#place Wait13
#place Update13
#place Mess13
#place Ack13
#place Idle14 mk(<..>)
#place Wait14
#place Update14
#place Mess14
#place Ack14
#place Idle15 mk(<..>)
#place Wait15
#place Update15
#place Mess15
#place Ack15
#place Idle16 mk(<..>)
#place Wait16
#place Update16
#place Mess16
#place Ack16
#place Idle17 mk(<..>)
#place Wait17
#place Update17
#place Mess17
#place Ack17
#place Idle18 mk(<..>)
#place Wait18
#place Update18
#place Mess18
#place Ack18
#place Idle19 mk(<..>)
#place Wait19
#place Update19
#place Mess19
#place Ack19
#trans T1_0
in {Idle0:<..>;Mutex:<..>;}
out {Wait0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_0
in {Wait0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle0:<..>;Mutex:<..>;}
#endtr
#trans T3_0
in {Idle0:<..>;Mess0:<..>;}
out {Update0:<..>;}
#endtr
#trans T4_0
in {Update0:<..>;}
out {Idle0:<..>;Ack0:<..>;}
#endtr
#trans T1_1
in {Idle1:<..>;Mutex:<..>;}
out {Wait1:<..>;Mess0:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_1
in {Wait1:<..>;Ack0:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle1:<..>;Mutex:<..>;}
#endtr
#trans T3_1
in {Idle1:<..>;Mess1:<..>;}
out {Update1:<..>;}
#endtr
#trans T4_1
in {Update1:<..>;}
out {Idle1:<..>;Ack1:<..>;}
#endtr
#trans T1_2
in {Idle2:<..>;Mutex:<..>;}
out {Wait2:<..>;Mess0:<..>;Mess1:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_2
in {Wait2:<..>;Ack0:<..>;Ack1:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle2:<..>;Mutex:<..>;}
#endtr
#trans T3_2
in {Idle2:<..>;Mess2:<..>;}
out {Update2:<..>;}
#endtr
#trans T4_2
in {Update2:<..>;}
out {Idle2:<..>;Ack2:<..>;}
#endtr
#trans T1_3
in {Idle3:<..>;Mutex:<..>;}
out {Wait3:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_3
in {Wait3:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle3:<..>;Mutex:<..>;}
#endtr
#trans T3_3
in {Idle3:<..>;Mess3:<..>;}
out {Update3:<..>;}
#endtr
#trans T4_3
in {Update3:<..>;}
out {Idle3:<..>;Ack3:<..>;}
#endtr
#trans T1_4
in {Idle4:<..>;Mutex:<..>;}
out {Wait4:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_4
in {Wait4:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle4:<..>;Mutex:<..>;}
#endtr
#trans T3_4
in {Idle4:<..>;Mess4:<..>;}
out {Update4:<..>;}
#endtr
#trans T4_4
in {Update4:<..>;}
out {Idle4:<..>;Ack4:<..>;}
#endtr
#trans T1_5
in {Idle5:<..>;Mutex:<..>;}
out {Wait5:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_5
in {Wait5:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle5:<..>;Mutex:<..>;}
#endtr
#trans T3_5
in {Idle5:<..>;Mess5:<..>;}
out {Update5:<..>;}
#endtr
#trans T4_5
in {Update5:<..>;}
out {Idle5:<..>;Ack5:<..>;}
#endtr
#trans T1_6
in {Idle6:<..>;Mutex:<..>;}
out {Wait6:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_6
in {Wait6:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle6:<..>;Mutex:<..>;}
#endtr
#trans T3_6
in {Idle6:<..>;Mess6:<..>;}
out {Update6:<..>;}
#endtr
#trans T4_6
in {Update6:<..>;}
out {Idle6:<..>;Ack6:<..>;}
#endtr
#trans T1_7
in {Idle7:<..>;Mutex:<..>;}
out {Wait7:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_7
in {Wait7:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle7:<..>;Mutex:<..>;}
#endtr
#trans T3_7
in {Idle7:<..>;Mess7:<..>;}
out {Update7:<..>;}
#endtr
#trans T4_7
in {Update7:<..>;}
out {Idle7:<..>;Ack7:<..>;}
#endtr
#trans T1_8
in {Idle8:<..>;Mutex:<..>;}
out {Wait8:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_8
in {Wait8:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle8:<..>;Mutex:<..>;}
#endtr
#trans T3_8
in {Idle8:<..>;Mess8:<..>;}
out {Update8:<..>;}
#endtr
#trans T4_8
in {Update8:<..>;}
out {Idle8:<..>;Ack8:<..>;}
#endtr
#trans T1_9
in {Idle9:<..>;Mutex:<..>;}
out {Wait9:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_9
in {Wait9:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle9:<..>;Mutex:<..>;}
#endtr
#trans T3_9
in {Idle9:<..>;Mess9:<..>;}
out {Update9:<..>;}
#endtr
#trans T4_9
in {Update9:<..>;}
out {Idle9:<..>;Ack9:<..>;}
#endtr
#trans T1_10
in {Idle10:<..>;Mutex:<..>;}
out {Wait10:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_10
in {Wait10:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle10:<..>;Mutex:<..>;}
#endtr
#trans T3_10
in {Idle10:<..>;Mess10:<..>;}
out {Update10:<..>;}
#endtr
#trans T4_10
in {Update10:<..>;}
out {Idle10:<..>;Ack10:<..>;}
#endtr
#trans T1_11
in {Idle11:<..>;Mutex:<..>;}
out {Wait11:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_11
in {Wait11:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle11:<..>;Mutex:<..>;}
#endtr
#trans T3_11
in {Idle11:<..>;Mess11:<..>;}
out {Update11:<..>;}
#endtr
#trans T4_11
in {Update11:<..>;}
out {Idle11:<..>;Ack11:<..>;}
#endtr
#trans T1_12
in {Idle12:<..>;Mutex:<..>;}
out {Wait12:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_12
in {Wait12:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle12:<..>;Mutex:<..>;}
#endtr
#trans T3_12
in {Idle12:<..>;Mess12:<..>;}
out {Update12:<..>;}
#endtr
#trans T4_12
in {Update12:<..>;}
out {Idle12:<..>;Ack12:<..>;}
#endtr
#trans T1_13
in {Idle13:<..>;Mutex:<..>;}
out {Wait13:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_13
in {Wait13:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle13:<..>;Mutex:<..>;}
#endtr
#trans T3_13
in {Idle13:<..>;Mess13:<..>;}
out {Update13:<..>;}
#endtr
#trans T4_13
in {Update13:<..>;}
out {Idle13:<..>;Ack13:<..>;}
#endtr
#trans T1_14
in {Idle14:<..>;Mutex:<..>;}
out {Wait14:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_14
in {Wait14:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle14:<..>;Mutex:<..>;}
#endtr
#trans T3_14
in {Idle14:<..>;Mess14:<..>;}
out {Update14:<..>;}
#endtr
#trans T4_14
in {Update14:<..>;}
out {Idle14:<..>;Ack14:<..>;}
#endtr
#trans T1_15
in {Idle15:<..>;Mutex:<..>;}
out {Wait15:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_15
in {Wait15:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle15:<..>;Mutex:<..>;}
#endtr
#trans T3_15
in {Idle15:<..>;Mess15:<..>;}
out {Update15:<..>;}
#endtr
#trans T4_15
in {Update15:<..>;}
out {Idle15:<..>;Ack15:<..>;}
#endtr
#trans T1_16
in {Idle16:<..>;Mutex:<..>;}
out {Wait16:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_16
in {Wait16:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle16:<..>;Mutex:<..>;}
#endtr
#trans T3_16
in {Idle16:<..>;Mess16:<..>;}
out {Update16:<..>;}
#endtr
#trans T4_16
in {Update16:<..>;}
out {Idle16:<..>;Ack16:<..>;}
#endtr
#trans T1_17
in {Idle17:<..>;Mutex:<..>;}
out {Wait17:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_17
in {Wait17:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle17:<..>;Mutex:<..>;}
#endtr
#trans T3_17
in {Idle17:<..>;Mess17:<..>;}
out {Update17:<..>;}
#endtr
#trans T4_17
in {Update17:<..>;}
out {Idle17:<..>;Ack17:<..>;}
#endtr
#trans T1_18
in {Idle18:<..>;Mutex:<..>;}
out {Wait18:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess19:<..>;}
#endtr
#trans T2_18
in {Wait18:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack19:<..>;}
out {Idle18:<..>;Mutex:<..>;}
#endtr
#trans T3_18
in {Idle18:<..>;Mess18:<..>;}
out {Update18:<..>;}
#endtr
#trans T4_18
in {Update18:<..>;}
out {Idle18:<..>;Ack18:<..>;}
#endtr
#trans T1_19
in {Idle19:<..>;Mutex:<..>;}
out {Wait19:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;}
#endtr
#trans T2_19
in {Wait19:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;}
out {Idle19:<..>;Mutex:<..>;}
#endtr
#trans T3_19
in {Idle19:<..>;Mess19:<..>;}
out {Update19:<..>;}
#endtr
#trans T4_19
in {Update19:<..>;}
out {Idle19:<..>;Ack19:<..>;}
#endtr