0b55f123 |
1 | # To unbundle, sh this file |
2 | echo ex.readme 1>&2 |
3 | sed 's/.//' >ex.readme <<'//GO.SYSIN DD ex.readme' |
4 | -The 12 files in this bundle are the PROMELA |
5 | -files of all exercises and examples discussed |
6 | -in the document Doc/Exercises.ps from the |
7 | -SPIN distribution. |
8 | //GO.SYSIN DD ex.readme |
9 | echo ex.1a 1>&2 |
10 | sed 's/.//' >ex.1a <<'//GO.SYSIN DD ex.1a' |
11 | -init { |
12 | - byte i = 0; |
13 | - do |
14 | - :: i = i+1 |
15 | - od |
16 | -} |
17 | //GO.SYSIN DD ex.1a |
18 | echo ex.1b 1>&2 |
19 | sed 's/.//' >ex.1b <<'//GO.SYSIN DD ex.1b' |
20 | -init { |
21 | - chan dummy = [20] of { byte }; |
22 | - do |
23 | - :: dummy!85 |
24 | - :: dummy!170 |
25 | - od |
26 | -} |
27 | //GO.SYSIN DD ex.1b |
28 | echo ex.1c 1>&2 |
29 | sed 's/.//' >ex.1c <<'//GO.SYSIN DD ex.1c' |
30 | -#define N 26 |
31 | - |
32 | -int a; |
33 | -byte b; |
34 | - |
35 | -init { |
36 | - do |
37 | - :: atomic { (b < N) -> |
38 | - if |
39 | - :: a = a + (1<<b) |
40 | - :: skip |
41 | - fi; |
42 | - b=b+1 } |
43 | - od |
44 | -} |
45 | //GO.SYSIN DD ex.1c |
46 | echo ex.2 1>&2 |
47 | sed 's/.//' >ex.2 <<'//GO.SYSIN DD ex.2' |
48 | -#define MAX 8 |
49 | -proctype A(chan in, out) |
50 | -{ byte mt; /* message data */ |
51 | - bit vr; |
52 | -S1: mt = (mt+1)%MAX; |
53 | - out!mt,1; |
54 | - goto S2; |
55 | -S2: in?vr; |
56 | - if |
57 | - :: (vr == 1) -> goto S1 |
58 | - :: (vr == 0) -> goto S3 |
59 | - :: printf("AERROR1\n") -> goto S5 |
60 | - fi; |
61 | -S3: out!mt,1; |
62 | - goto S4; |
63 | -S4: in?vr; |
64 | - if |
65 | - :: goto S1 |
66 | - :: printf("AERROR2\n"); goto S5 |
67 | - fi; |
68 | -S5: out!mt,0; |
69 | - goto S4 |
70 | -} |
71 | -proctype B(chan in, out) |
72 | -{ byte mr, lmr; |
73 | - bit ar; |
74 | - goto S2; /* initial state */ |
75 | -S1: assert(mr == (lmr+1)%MAX); |
76 | - lmr = mr; |
77 | - out!1; |
78 | - goto S2; |
79 | -S2: in?mr,ar; |
80 | - if |
81 | - :: (ar == 1) -> goto S1 |
82 | - :: (ar == 0) -> goto S3 |
83 | - :: printf("ERROR1\n"); goto S5 |
84 | - fi; |
85 | -S3: out!1; |
86 | - goto S2; |
87 | -S4: in?mr,ar; |
88 | - if |
89 | - :: goto S1 |
90 | - :: printf("ERROR2\n"); goto S5 |
91 | - fi; |
92 | -S5: out!0; |
93 | - goto S4 |
94 | -} |
95 | -init { |
96 | - chan a2b = [2] of { bit }; |
97 | - chan b2a = [2] of { byte, bit }; |
98 | - atomic { |
99 | - run A(a2b, b2a); |
100 | - run B(b2a, a2b) |
101 | - } |
102 | -} |
103 | //GO.SYSIN DD ex.2 |
104 | echo ex.3 1>&2 |
105 | sed 's/.//' >ex.3 <<'//GO.SYSIN DD ex.3' |
106 | -mtype = { a, b, c, d, e, i, l, m, n, q, r, u, v }; |
107 | - |
108 | -chan dce = [0] of { mtype }; |
109 | -chan dte = [0] of { mtype }; |
110 | - |
111 | -active proctype dte_proc() |
112 | -{ |
113 | -state01: |
114 | - do |
115 | - :: dce!b -> /* state21 */ dce!a |
116 | - :: dce!i -> /* state14 */ |
117 | - if |
118 | - :: dte?m -> goto state19 |
119 | - :: dce!a |
120 | - fi |
121 | - :: dte?m -> goto state18 |
122 | - :: dte?u -> goto state08 |
123 | - :: dce!d -> break |
124 | - od; |
125 | - |
126 | - /* state02: */ |
127 | - if |
128 | - :: dte?v |
129 | - :: dte?u -> goto state15 |
130 | - :: dte?m -> goto state19 |
131 | - fi; |
132 | -state03: |
133 | - dce!e; |
134 | - /* state04: */ |
135 | - if |
136 | - :: dte?m -> goto state19 |
137 | - :: dce!c |
138 | - fi; |
139 | - /* state05: */ |
140 | - if |
141 | - :: dte?m -> goto state19 |
142 | - :: dte?r |
143 | - fi; |
144 | - /* state6A: */ |
145 | - if |
146 | - :: dte?m -> goto state19 |
147 | - :: dte?q |
148 | - fi; |
149 | -state07: |
150 | - if |
151 | - :: dte?m -> goto state19 |
152 | - :: dte?r |
153 | - fi; |
154 | - /* state6B: */ |
155 | - if /* non-deterministic select */ |
156 | - :: dte?q -> goto state07 |
157 | - :: dte?q |
158 | - :: dte?m -> goto state19 |
159 | - fi; |
160 | - /* state10: */ |
161 | - if |
162 | - :: dte?m -> goto state19 |
163 | - :: dte?r |
164 | - fi; |
165 | -state6C: |
166 | - if |
167 | - :: dte?m -> goto state19 |
168 | - :: dte?l |
169 | - fi; |
170 | - /* state11: */ |
171 | - if |
172 | - :: dte?m -> goto state19 |
173 | - :: dte?n |
174 | - fi; |
175 | - /* state12: */ |
176 | - if |
177 | - :: dte?m -> goto state19 |
178 | - :: dce!b -> goto state16 |
179 | - fi; |
180 | - |
181 | -state15: |
182 | - if |
183 | - :: dte?v -> goto state03 |
184 | - :: dte?m -> goto state19 |
185 | - fi; |
186 | -state08: |
187 | - if |
188 | - :: dce!c |
189 | - :: dce!d -> goto state15 |
190 | - :: dte?m -> goto state19 |
191 | - fi; |
192 | - /* state09: */ |
193 | - if |
194 | - :: dte?m -> goto state19 |
195 | - :: dte?q |
196 | - fi; |
197 | - /* state10B: */ |
198 | - if |
199 | - :: dte?r -> goto state6C |
200 | - :: dte?m -> goto state19 |
201 | - fi; |
202 | -state18: |
203 | - if |
204 | - :: dte?l -> goto state01 |
205 | - :: dte?m -> goto state19 |
206 | - fi; |
207 | -state16: |
208 | - dte?m; |
209 | - /* state17: */ |
210 | - dte?l; |
211 | - /* state21: */ |
212 | - dce!a; goto state01; |
213 | -state19: |
214 | - dce!b; |
215 | - /* state20: */ |
216 | - dte?l; |
217 | - /* state21: */ |
218 | - dce!a; goto state01 |
219 | -} |
220 | - |
221 | -active proctype dce_proc() |
222 | -{ |
223 | -state01: |
224 | - do |
225 | - :: dce?b -> /* state21 */ dce?a |
226 | - :: dce?i -> /* state14 */ |
227 | - if |
228 | - :: dce?b -> goto state16 |
229 | - :: dce?a |
230 | - fi |
231 | - :: dte!m -> goto state18 |
232 | - :: dte!u -> goto state08 |
233 | - :: dce?d -> break |
234 | - od; |
235 | - |
236 | - /* state02: */ |
237 | - if |
238 | - :: dte!v |
239 | - :: dte!u -> goto state15 |
240 | - :: dce?b -> goto state16 |
241 | - fi; |
242 | -state03: |
243 | - dce?e; |
244 | - /* state04: */ |
245 | - if |
246 | - :: dce?b -> goto state16 |
247 | - :: dce?c |
248 | - fi; |
249 | - /* state05: */ |
250 | - if |
251 | - :: dce?b -> goto state16 |
252 | - :: dte!r |
253 | - fi; |
254 | - /* state6A: */ |
255 | - if |
256 | - :: dce?b -> goto state16 |
257 | - :: dte!q |
258 | - fi; |
259 | -state07: |
260 | - if |
261 | - :: dce?b -> goto state16 |
262 | - :: dte!r |
263 | - fi; |
264 | - /* state6B: */ |
265 | - if /* non-deterministic select */ |
266 | - :: dte!q -> goto state07 |
267 | - :: dte!q |
268 | - :: dce?b -> goto state16 |
269 | - fi; |
270 | - /* state10: */ |
271 | - if |
272 | - :: dce?b -> goto state16 |
273 | - :: dte!r |
274 | - fi; |
275 | -state6C: |
276 | - if |
277 | - :: dce?b -> goto state16 |
278 | - :: dte!l |
279 | - fi; |
280 | - /* state11: */ |
281 | - if |
282 | - :: dce?b -> goto state16 |
283 | - :: dte!n |
284 | - fi; |
285 | - /* state12: */ |
286 | - if |
287 | - :: dce?b -> goto state16 |
288 | - :: dte!m -> goto state19 |
289 | - fi; |
290 | - |
291 | -state15: |
292 | - if |
293 | - :: dte!v -> goto state03 |
294 | - :: dce?b -> goto state16 |
295 | - fi; |
296 | -state08: |
297 | - if |
298 | - :: dce?c |
299 | - :: dce?d -> goto state15 |
300 | - :: dce?b -> goto state16 |
301 | - fi; |
302 | - /* state09: */ |
303 | - if |
304 | - :: dce?b -> goto state16 |
305 | - :: dte!q |
306 | - fi; |
307 | - /* state10B: */ |
308 | - if |
309 | - :: dte!r -> goto state6C |
310 | - :: dce?b -> goto state16 |
311 | - fi; |
312 | -state18: |
313 | - if |
314 | - :: dte!l -> goto state01 |
315 | - :: dce?b -> goto state16 |
316 | - fi; |
317 | -state16: |
318 | - dte!m; |
319 | - /* state17: */ |
320 | - dte!l; |
321 | - /* state21: */ |
322 | - dce?a; goto state01; |
323 | -state19: |
324 | - dce?b; |
325 | - /* state20: */ |
326 | - dte!l; |
327 | - /* state21: */ |
328 | - dce?a; goto state01 |
329 | -} |
330 | //GO.SYSIN DD ex.3 |
331 | echo ex.4b 1>&2 |
332 | sed 's/.//' >ex.4b <<'//GO.SYSIN DD ex.4b' |
333 | -#define true 1 |
334 | -#define false 0 |
335 | - |
336 | -bool flag[2]; |
337 | -bool turn; |
338 | - |
339 | -active [2] proctype user() |
340 | -{ flag[_pid] = true; |
341 | - turn = _pid; |
342 | - (flag[1-_pid] == false || turn == 1-_pid); |
343 | -crit: skip; /* critical section */ |
344 | - flag[_pid] = false |
345 | -} |
346 | //GO.SYSIN DD ex.4b |
347 | echo ex.4c 1>&2 |
348 | sed 's/.//' >ex.4c <<'//GO.SYSIN DD ex.4c' |
349 | -byte in; |
350 | -byte x, y, z; |
351 | -active [2] proctype user() /* file ex.4c */ |
352 | -{ byte me = _pid+1; /* me is 1 or 2 */ |
353 | -L1: x = me; |
354 | -L2: if |
355 | - :: (y != 0 && y != me) -> goto L1 /* try again */ |
356 | - :: (y == 0 || y == me) |
357 | - fi; |
358 | -L3: z = me; |
359 | -L4: if |
360 | - :: (x != me) -> goto L1 /* try again */ |
361 | - :: (x == me) |
362 | - fi; |
363 | -L5: y = me; |
364 | -L6: if |
365 | - :: (z != me) -> goto L1 /* try again */ |
366 | - :: (z == me) |
367 | - fi; |
368 | -L7: /* success */ |
369 | - in = in+1; |
370 | - assert(in == 1); |
371 | - in = in - 1; |
372 | - goto L1 |
373 | -} |
374 | //GO.SYSIN DD ex.4c |
375 | echo ex.5a 1>&2 |
376 | sed 's/.//' >ex.5a <<'//GO.SYSIN DD ex.5a' |
377 | -#define Place byte /* assume < 256 tokens per place */ |
378 | - |
379 | -Place p1, p2, p3; |
380 | -Place p4, p5, p6; |
381 | -#define inp1(x) (x>0) -> x=x-1 |
382 | -#define inp2(x,y) (x>0&&y>0) -> x = x-1; y=y-1 |
383 | -#define out1(x) x=x+1 |
384 | -#define out2(x,y) x=x+1; y=y+1 |
385 | -init |
386 | -{ p1 = 1; p4 = 1; /* initial marking */ |
387 | - do |
388 | -/*t1*/ :: atomic { inp1(p1) -> out1(p2) } |
389 | -/*t2*/ :: atomic { inp2(p2,p4) -> out1(p3) } |
390 | -/*t3*/ :: atomic { inp1(p3) -> out2(p1,p4) } |
391 | -/*t4*/ :: atomic { inp1(p4) -> out1(p5) } |
392 | -/*t5*/ :: atomic { inp2(p1,p5) -> out1(p6) } |
393 | -/*t6*/ :: atomic { inp1(p6) -> out2(p4,p1) } |
394 | - od |
395 | -} |
396 | //GO.SYSIN DD ex.5a |
397 | echo ex.5b 1>&2 |
398 | sed 's/.//' >ex.5b <<'//GO.SYSIN DD ex.5b' |
399 | -#define Place byte /* assume < 256 tokens per place */ |
400 | - |
401 | -Place P1, P2, P4, P5, RC, CC, RD, CD; |
402 | -Place p1, p2, p4, p5, rc, cc, rd, cd; |
403 | - |
404 | -#define inp1(x) (x>0) -> x=x-1 |
405 | -#define inp2(x,y) (x>0&&y>0) -> x = x-1; y=y-1 |
406 | -#define out1(x) x=x+1 |
407 | -#define out2(x,y) x=x+1; y=y+1 |
408 | - |
409 | -init /* file ex.5b */ |
410 | -{ P1 = 1; p1 = 1; /* initial marking */ |
411 | - do |
412 | - :: atomic { inp1(P1) -> out2(rc,P2) } /* DC */ |
413 | - :: atomic { inp2(P2,CC) -> out1(P4) } /* CA */ |
414 | - :: atomic { inp1(P4) -> out2(P5,rd) } /* DD */ |
415 | - :: atomic { inp2(P5,CD) -> out1(P1) } /* FD */ |
416 | - :: atomic { inp2(P1,RC) -> out2(P4,cc) } /* AC */ |
417 | - :: atomic { inp2(P4,RD) -> out2(P1,cd) } /* AD */ |
418 | - :: atomic { inp2(P5,RD) -> out1(P1) } /* DA */ |
419 | - |
420 | - :: atomic { inp1(p1) -> out2(RC,p2) } /* dc */ |
421 | - :: atomic { inp2(p2,cc) -> out1(p4) } /* ca */ |
422 | - :: atomic { inp1(p4) -> out2(p5,RD) } /* dd */ |
423 | - :: atomic { inp2(p5,cd) -> out1(p1) } /* fd */ |
424 | - :: atomic { inp2(p1,rc) -> out2(p4,CC) } /* ac */ |
425 | - :: atomic { inp2(p4,rd) -> out2(p1,CD) } /* ad */ |
426 | - :: atomic { inp2(p5,rd) -> out1(p1) } /* da */ |
427 | - od |
428 | -} |
429 | //GO.SYSIN DD ex.5b |
430 | echo ex.6 1>&2 |
431 | sed 's/.//' >ex.6 <<'//GO.SYSIN DD ex.6' |
432 | -#if 0 |
433 | - Cambridge Ring Protocol [Needham'82] |
434 | - basic protocol - no LTL properties |
435 | -#endif |
436 | - |
437 | -#define LOSS 1 |
438 | -#define RELAXED 1 |
439 | - |
440 | -#if RELAXED==1 |
441 | -#define stimeout empty(sender) |
442 | -#define rtimeout empty(recv) |
443 | -#else |
444 | -#define stimeout timeout |
445 | -#define rtimeout timeout |
446 | -#endif |
447 | - |
448 | -#define QSZ 6 /* length of message queues */ |
449 | - |
450 | - mtype = { |
451 | - RDY, NOTRDY, DATA, NODATA, RESET |
452 | - }; |
453 | - chan sender = [QSZ] of { mtype, byte }; |
454 | - chan recv = [QSZ] of { mtype, byte }; |
455 | - |
456 | -active proctype Sender() |
457 | -{ short n = -1; byte t,m; |
458 | - |
459 | - xr sender; |
460 | - xs recv; |
461 | - |
462 | -I: /* Idle State */ |
463 | - do |
464 | -#if LOSS==1 |
465 | - :: sender?_,_ -> progress2: skip |
466 | -#endif |
467 | - :: sender?RESET,0 -> |
468 | -ackreset: recv!RESET,0; /* stay in idle */ |
469 | - n = -1; |
470 | - goto I |
471 | - |
472 | - /* E-rep: protocol error */ |
473 | - |
474 | - :: sender?RDY,m -> /* E-exp */ |
475 | - assert(m == (n+1)%4); |
476 | -advance: n = (n+1)%4; |
477 | - if |
478 | -/* buffer */ :: atomic { |
479 | - printf("MSC: NEW\n"); |
480 | - recv!DATA,n; |
481 | - goto E |
482 | - } |
483 | -/* no buffer */ :: recv!NODATA,n; |
484 | - goto N |
485 | - fi |
486 | - |
487 | - :: sender?NOTRDY,m -> /* N-exp */ |
488 | -expected: assert(m == (n+1)%4); |
489 | - goto I |
490 | - |
491 | - /* Timeout */ |
492 | - /* ignored (p.154, in [Needham'82]) */ |
493 | - |
494 | - :: goto reset |
495 | - |
496 | - od; |
497 | - |
498 | -E: /* Essential element sent, ack expected */ |
499 | - do |
500 | -#if LOSS==1 |
501 | - :: sender?_,_ -> progress0: skip |
502 | -#endif |
503 | - :: sender?RESET,0 -> |
504 | - goto ackreset |
505 | - |
506 | - :: sender?RDY,m -> |
507 | - if |
508 | - :: (m == n) -> /* E-rep */ |
509 | - goto retrans |
510 | - :: (m == (n+1)%4) -> /* E-exp */ |
511 | - goto advance |
512 | - fi |
513 | - |
514 | - :: sender?NOTRDY,m -> /* N-exp */ |
515 | - goto expected |
516 | - |
517 | - /* Timeout */ |
518 | - :: stimeout -> |
519 | - printf("MSC: STO\n"); |
520 | -retrans: recv!DATA,n /* retransmit */ |
521 | - |
522 | - :: goto reset |
523 | - |
524 | - od; |
525 | - |
526 | - |
527 | -N: /* Non-essential element sent */ |
528 | - do |
529 | -#if LOSS==1 |
530 | - :: sender?_,_ -> progress1: skip |
531 | -#endif |
532 | - :: sender?RESET,0 -> |
533 | - goto ackreset |
534 | - |
535 | - :: sender?RDY,m -> /* E-rep */ |
536 | - assert(m == n) /* E-exp: protocol error */ |
537 | - -> recv!NODATA,n /* retransmit and stay in N */ |
538 | - |
539 | - :: recv!DATA,n; /* buffer ready event */ |
540 | - goto E |
541 | - |
542 | - :: goto reset |
543 | - |
544 | - /* Timeout */ |
545 | - /* ignored (p.154, in [Needham'82]) */ |
546 | - od; |
547 | - |
548 | -reset: recv!RESET,0; |
549 | - do |
550 | -#if LOSS==1 |
551 | - :: sender?_,_ -> progress3: skip |
552 | -#endif |
553 | - :: sender?t,m -> |
554 | - if |
555 | - :: t == RESET -> n = -1; goto I |
556 | - :: else /* ignored, p. 152 */ |
557 | - fi |
558 | - :: timeout -> /* a real timeout */ |
559 | - goto reset |
560 | - od |
561 | -} |
562 | - |
563 | -active proctype Receiver() |
564 | -{ byte t, n, m, Nexp; |
565 | - |
566 | - xr recv; |
567 | - xs sender; |
568 | - |
569 | -I: /* Idle State */ |
570 | - do |
571 | -#if LOSS==1 |
572 | - :: recv?_,_ -> progress2: skip |
573 | -#endif |
574 | - :: recv?RESET,0 -> |
575 | -ackreset: sender!RESET,0; /* stay in idle */ |
576 | - n = 0; Nexp = 0; |
577 | - goto I |
578 | - |
579 | - :: atomic { recv?DATA(m) -> /* E-exp */ |
580 | - assert(m == n); |
581 | -advance: printf("MSC: EXP\n"); |
582 | - n = (n+1)%4; |
583 | - assert(m == Nexp); |
584 | - Nexp = (m+1)%4; |
585 | - if |
586 | - :: sender!RDY,n; goto E |
587 | - :: sender!NOTRDY,n; goto N |
588 | - fi |
589 | - } |
590 | - |
591 | - :: recv?NODATA(m) -> /* N-exp */ |
592 | - assert(m == n) |
593 | - |
594 | - /* Timeout: ignored */ |
595 | - |
596 | - /* only receiver can initiate transfer; p. 156 */ |
597 | - :: empty(recv) -> sender!RDY,n; goto E |
598 | - |
599 | - :: goto reset |
600 | - od; |
601 | - |
602 | -E: |
603 | - do |
604 | -#if LOSS==1 |
605 | - :: recv?_,_ -> progress1: skip |
606 | -#endif |
607 | - :: recv?RESET,0 -> |
608 | - goto ackreset |
609 | - |
610 | - :: atomic { recv?DATA(m) -> |
611 | - if |
612 | - :: ((m+1)%4 == n) -> /* E-rep */ |
613 | - printf("MSC: REP\n"); |
614 | - goto retrans |
615 | - :: (m == n) -> /* E-exp */ |
616 | - goto advance |
617 | - fi |
618 | - } |
619 | - |
620 | - :: recv?NODATA(m) -> /* N-exp */ |
621 | - assert(m == n); |
622 | - goto I |
623 | - |
624 | - :: rtimeout -> |
625 | - printf("MSC: RTO\n"); |
626 | -retrans: sender!RDY,n; |
627 | - goto E |
628 | - |
629 | - :: goto reset |
630 | - |
631 | - od; |
632 | - |
633 | -N: |
634 | - do |
635 | -#if LOSS==1 |
636 | - :: recv?_,_ -> progress0: skip |
637 | -#endif |
638 | - :: recv?RESET,0 -> |
639 | - goto ackreset |
640 | - |
641 | - :: recv?DATA(m) -> /* E-rep */ |
642 | - assert((m+1)%4 == n); /* E-exp and N-exp: protocol error */ |
643 | - printf("MSC: REP\n"); |
644 | - sender!NOTRDY,n /* retransmit and stay in N */ |
645 | - |
646 | - :: sender!RDY,n -> /* buffer ready event */ |
647 | - goto E |
648 | - |
649 | - /* Timeout: ignored */ |
650 | - |
651 | - :: goto reset |
652 | - |
653 | - od; |
654 | - |
655 | -progress: |
656 | -reset: sender!RESET,0; |
657 | - do |
658 | -#if LOSS==1 |
659 | - :: recv?_,_ -> progress3: skip |
660 | -#endif |
661 | - :: recv?t,m -> |
662 | - if |
663 | - :: t == RESET -> n = 0; Nexp = 0; goto I |
664 | - :: else /* ignored, p. 152 */ |
665 | - fi |
666 | - :: timeout -> /* a real timeout */ |
667 | - goto reset |
668 | - od |
669 | -} |
670 | //GO.SYSIN DD ex.6 |
671 | echo ex.7 1>&2 |
672 | sed 's/.//' >ex.7 <<'//GO.SYSIN DD ex.7' |
673 | -mtype = { Wakeme, Running }; |
674 | - |
675 | -bit lk, sleep_q; |
676 | -bit r_lock, r_want; |
677 | -mtype State = Running; |
678 | - |
679 | -active proctype client() |
680 | -{ |
681 | -sleep: /* sleep routine */ |
682 | - atomic { (lk == 0) -> lk = 1 }; /* spinlock(&lk) */ |
683 | - do /* while r->lock */ |
684 | - :: (r_lock == 1) -> /* r->lock == 1 */ |
685 | - r_want = 1; |
686 | - State = Wakeme; |
687 | - lk = 0; /* freelock(&lk) */ |
688 | - (State == Running); /* wait for wakeup */ |
689 | - :: else -> /* r->lock == 0 */ |
690 | - break |
691 | - od; |
692 | -progress: |
693 | - assert(r_lock == 0); /* should still be true */ |
694 | - r_lock = 1; /* consumed resource */ |
695 | - lk = 0; /* freelock(&lk) */ |
696 | - goto sleep |
697 | -} |
698 | - |
699 | -active proctype server() /* interrupt routine */ |
700 | -{ |
701 | -wakeup: /* wakeup routine */ |
702 | - r_lock = 0; /* r->lock = 0 */ |
703 | - (lk == 0); /* waitlock(&lk) */ |
704 | - if |
705 | - :: r_want -> /* someone is sleeping */ |
706 | - atomic { /* spinlock on sleep queue */ |
707 | - (sleep_q == 0) -> sleep_q = 1 |
708 | - }; |
709 | - r_want = 0; |
710 | -#ifdef PROPOSED_FIX |
711 | - (lk == 0); /* waitlock(&lk) */ |
712 | -#endif |
713 | - if |
714 | - :: (State == Wakeme) -> |
715 | - State = Running; |
716 | - :: else -> |
717 | - fi; |
718 | - sleep_q = 0 |
719 | - :: else -> |
720 | - fi; |
721 | - goto wakeup |
722 | -} |
723 | //GO.SYSIN DD ex.7 |
724 | echo ex.8 1>&2 |
725 | sed 's/.//' >ex.8 <<'//GO.SYSIN DD ex.8' |
726 | -/* Dolev, Klawe & Rodeh for leader election in unidirectional ring |
727 | - * `An O(n log n) unidirectional distributed algorithm for extrema |
728 | - * finding in a circle,' J. of Algs, Vol 3. (1982), pp. 245-260 |
729 | - */ |
730 | - |
731 | -#define elected (nr_leaders > 0) |
732 | -#define noLeader (nr_leaders == 0) |
733 | -#define oneLeader (nr_leaders == 1) |
734 | - |
735 | -/* properties: |
736 | - * ![] noLeader |
737 | - * <> elected |
738 | - * <>[]oneLeader |
739 | - * [] (noLeader U oneLeader) |
740 | - */ |
741 | - |
742 | -#define N 7 /* nr of processes (use 5 for demos) */ |
743 | -#define I 3 /* node given the smallest number */ |
744 | -#define L 14 /* size of buffer (>= 2*N) */ |
745 | - |
746 | -mtype = { one, two, winner }; |
747 | -chan q[N] = [L] of { mtype, byte}; |
748 | - |
749 | -byte nr_leaders = 0; |
750 | - |
751 | -proctype node (chan in, out; byte mynumber) |
752 | -{ bit Active = 1, know_winner = 0; |
753 | - byte nr, maximum = mynumber, neighbourR; |
754 | - |
755 | - xr in; |
756 | - xs out; |
757 | - |
758 | - printf("MSC: %d\n", mynumber); |
759 | - out!one(mynumber); |
760 | -end: do |
761 | - :: in?one(nr) -> |
762 | - if |
763 | - :: Active -> |
764 | - if |
765 | - :: nr != maximum -> |
766 | - out!two(nr); |
767 | - neighbourR = nr |
768 | - :: else -> |
769 | - /* Raynal p.39: max is greatest number */ |
770 | - assert(nr == N); |
771 | - know_winner = 1; |
772 | - out!winner,nr; |
773 | - fi |
774 | - :: else -> |
775 | - out!one(nr) |
776 | - fi |
777 | - |
778 | - :: in?two(nr) -> |
779 | - if |
780 | - :: Active -> |
781 | - if |
782 | - :: neighbourR > nr && neighbourR > maximum -> |
783 | - maximum = neighbourR; |
784 | - out!one(neighbourR) |
785 | - :: else -> |
786 | - Active = 0 |
787 | - fi |
788 | - :: else -> |
789 | - out!two(nr) |
790 | - fi |
791 | - :: in?winner,nr -> |
792 | - if |
793 | - :: nr != mynumber -> |
794 | - printf("MSC: LOST\n"); |
795 | - :: else -> |
796 | - printf("MSC: LEADER\n"); |
797 | - nr_leaders++; |
798 | - assert(nr_leaders == 1) |
799 | - fi; |
800 | - if |
801 | - :: know_winner |
802 | - :: else -> out!winner,nr |
803 | - fi; |
804 | - break |
805 | - od |
806 | -} |
807 | - |
808 | -init { |
809 | - byte proc; |
810 | - atomic { |
811 | - proc = 1; |
812 | - do |
813 | - :: proc <= N -> |
814 | - run node (q[proc-1], q[proc%N], (N+I-proc)%N+1); |
815 | - proc++ |
816 | - :: proc > N -> |
817 | - break |
818 | - od |
819 | - } |
820 | -} |
821 | - |
822 | -#if 0 |
823 | -/* !(<>[]oneLeader) */ |
824 | - |
825 | -never { |
826 | -T0: |
827 | - if |
828 | - :: skip -> goto T0 |
829 | - :: !oneLeader -> goto accept |
830 | - fi; |
831 | -accept: |
832 | - if |
833 | - :: skip -> goto T0 |
834 | - fi |
835 | -} |
836 | -#endif |
837 | //GO.SYSIN DD ex.8 |
838 | echo ex.9 1>&2 |
839 | sed 's/.//' >ex.9 <<'//GO.SYSIN DD ex.9' |
840 | -#define MaxSeq 3 |
841 | -#define MaxSeq_plus_1 4 |
842 | -#define inc(x) x = (x + 1) % (MaxSeq_plus_1) |
843 | - |
844 | -chan q[2] = [MaxSeq] of { byte, byte }; |
845 | - |
846 | -active [2] proctype p5() |
847 | -{ byte NextFrame, AckExp, FrameExp, |
848 | - r, s, nbuf, i; |
849 | - chan in, out; |
850 | - |
851 | - in = q[_pid]; |
852 | - out = q[1-_pid]; |
853 | - |
854 | - xr in; |
855 | - xs out; |
856 | - |
857 | - do |
858 | - :: nbuf < MaxSeq -> |
859 | - nbuf++; |
860 | - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq_plus_1); |
861 | - inc(NextFrame) |
862 | - :: in?r,s -> |
863 | - if |
864 | - :: r == FrameExp -> |
865 | - inc(FrameExp) |
866 | - :: else |
867 | - fi; |
868 | - do |
869 | - :: ((AckExp <= s) && (s < NextFrame)) |
870 | - || ((AckExp <= s) && (NextFrame < AckExp)) |
871 | - || ((s < NextFrame) && (NextFrame < AckExp)) -> |
872 | - nbuf--; |
873 | - inc(AckExp) |
874 | - :: else -> |
875 | - break |
876 | - od |
877 | - :: timeout -> |
878 | - NextFrame = AckExp; |
879 | - i = 1; |
880 | - do |
881 | - :: i <= nbuf -> |
882 | - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq_plus_1); |
883 | - inc(NextFrame); |
884 | - i++ |
885 | - :: else -> |
886 | - break |
887 | - od |
888 | - od |
889 | -} |
890 | //GO.SYSIN DD ex.9 |
891 | echo ex.9b 1>&2 |
892 | sed 's/.//' >ex.9b <<'//GO.SYSIN DD ex.9b' |
893 | -#define MaxSeq 3 |
894 | -#define MaxSeq_plus_1 4 |
895 | -#define inc(x) x = (x + 1) % (MaxSeq + 1) |
896 | - |
897 | -chan q[2] = [MaxSeq] of { byte, byte }; |
898 | - |
899 | -active [2] proctype p5() |
900 | -{ byte NextFrame, AckExp, FrameExp, |
901 | - r, s, nbuf, i; |
902 | - chan in, out; |
903 | - |
904 | - d_step { |
905 | - in = q[_pid]; |
906 | - out = q[1-_pid] |
907 | - }; |
908 | - xr in; |
909 | - xs out; |
910 | - |
911 | - do |
912 | - :: atomic { nbuf < MaxSeq -> |
913 | - nbuf++; |
914 | - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); |
915 | - printf("MSC: nbuf: %d\n", nbuf); |
916 | - inc(NextFrame) |
917 | - } |
918 | - :: atomic { in?r,s -> |
919 | - if |
920 | - :: r == FrameExp -> |
921 | - printf("MSC: accept %d\n", r); |
922 | - inc(FrameExp) |
923 | - :: else |
924 | - -> printf("MSC: reject\n") |
925 | - fi |
926 | - }; |
927 | - d_step { |
928 | - do |
929 | - :: ((AckExp <= s) && (s < NextFrame)) |
930 | - || ((AckExp <= s) && (NextFrame < AckExp)) |
931 | - || ((s < NextFrame) && (NextFrame < AckExp)) -> |
932 | - nbuf--; |
933 | - printf("MSC: nbuf: %d\n", nbuf); |
934 | - inc(AckExp) |
935 | - :: else -> |
936 | - printf("MSC: %d %d %d\n", AckExp, s, NextFrame); |
937 | - break |
938 | - od; skip |
939 | - } |
940 | - :: timeout -> |
941 | - d_step { |
942 | - NextFrame = AckExp; |
943 | - printf("MSC: timeout\n"); |
944 | - i = 1; |
945 | - do |
946 | - :: i <= nbuf -> |
947 | - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); |
948 | - inc(NextFrame); |
949 | - i++ |
950 | - :: else -> |
951 | - break |
952 | - od; i = 0 |
953 | - } |
954 | - od |
955 | -} |
956 | //GO.SYSIN DD ex.9b |
957 | echo ex.9c 1>&2 |
958 | sed 's/.//' >ex.9c <<'//GO.SYSIN DD ex.9c' |
959 | -#define MaxSeq 3 |
960 | -#define MaxSeq_plus_1 4 |
961 | -#define inc(x) x = (x + 1) % (MaxSeq + 1) |
962 | - |
963 | -#define CHECKIT |
964 | - |
965 | -#ifdef CHECKIT |
966 | - mtype = { red, white, blue }; /* Wolper's test */ |
967 | - chan source = [0] of { mtype }; |
968 | - chan q[2] = [MaxSeq] of { mtype, byte, byte }; |
969 | - mtype rcvd = white; |
970 | - mtype sent = white; |
971 | -#else |
972 | - chan q[2] = [MaxSeq] of { byte, byte }; |
973 | -#endif |
974 | - |
975 | -active [2] proctype p5() |
976 | -{ byte NextFrame, AckExp, FrameExp, |
977 | - r, s, nbuf, i; |
978 | - chan in, out; |
979 | -#ifdef CHECKIT |
980 | - mtype ball; |
981 | - byte frames[MaxSeq_plus_1]; |
982 | -#endif |
983 | - |
984 | - d_step { |
985 | - in = q[_pid]; |
986 | - out = q[1-_pid] |
987 | - }; |
988 | - |
989 | - xr in; |
990 | - xs out; |
991 | - |
992 | - do |
993 | - :: atomic { |
994 | - nbuf < MaxSeq -> |
995 | - nbuf++; |
996 | -#ifdef CHECKIT |
997 | - if |
998 | - :: _pid%2 -> source?ball |
999 | - :: else |
1000 | - fi; |
1001 | - frames[NextFrame] = ball; |
1002 | - out!ball, NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); |
1003 | - if |
1004 | - :: _pid%2 -> sent = ball; |
1005 | - :: else |
1006 | - fi; |
1007 | -#else |
1008 | - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); |
1009 | -#endif |
1010 | -#ifdef VERBOSE |
1011 | - printf("MSC: nbuf: %d\n", nbuf); |
1012 | -#endif |
1013 | - inc(NextFrame) |
1014 | - } |
1015 | -#ifdef CHECKIT |
1016 | - :: atomic { in?ball,r,s -> |
1017 | -#else |
1018 | - :: atomic { in?r,s -> |
1019 | -#endif |
1020 | - if |
1021 | - :: r == FrameExp -> |
1022 | -#ifdef VERBOSE |
1023 | - printf("MSC: accept %d\n", r); |
1024 | -#endif |
1025 | -#ifdef CHECKIT |
1026 | - if |
1027 | - :: _pid%2 |
1028 | - :: else -> rcvd = ball |
1029 | - fi; |
1030 | -#endif |
1031 | - inc(FrameExp) |
1032 | - :: else |
1033 | -#ifdef VERBOSE |
1034 | - -> printf("MSC: reject\n") |
1035 | -#endif |
1036 | - fi |
1037 | - }; |
1038 | - d_step { |
1039 | - do |
1040 | - :: ((AckExp <= s) && (s < NextFrame)) |
1041 | - || ((AckExp <= s) && (NextFrame < AckExp)) |
1042 | - || ((s < NextFrame) && (NextFrame < AckExp)) -> |
1043 | - nbuf--; |
1044 | -#ifdef VERBOSE |
1045 | - printf("MSC: nbuf: %d\n", nbuf); |
1046 | -#endif |
1047 | - inc(AckExp) |
1048 | - :: else -> |
1049 | -#ifdef VERBOSE |
1050 | - printf("MSC: %d %d %d\n", AckExp, s, NextFrame); |
1051 | -#endif |
1052 | - break |
1053 | - od; |
1054 | - skip |
1055 | - } |
1056 | - :: timeout -> |
1057 | - d_step { |
1058 | - NextFrame = AckExp; |
1059 | -#ifdef VERBOSE |
1060 | - printf("MSC: timeout\n"); |
1061 | -#endif |
1062 | - i = 1; |
1063 | - do |
1064 | - :: i <= nbuf -> |
1065 | -#ifdef CHECKIT |
1066 | - if |
1067 | - :: _pid%2 -> ball = frames[NextFrame] |
1068 | - :: else |
1069 | - fi; |
1070 | - out!ball, NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); |
1071 | -#else |
1072 | - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); |
1073 | -#endif |
1074 | - inc(NextFrame); |
1075 | - i++ |
1076 | - :: else -> |
1077 | - break |
1078 | - od; |
1079 | - i = 0 |
1080 | - } |
1081 | - od |
1082 | -} |
1083 | -#ifdef CHECKIT |
1084 | -active proctype Source() |
1085 | -{ |
1086 | - do |
1087 | - :: source!white |
1088 | - :: source!red -> break |
1089 | - od; |
1090 | - do |
1091 | - :: source!white |
1092 | - :: source!blue -> break |
1093 | - od; |
1094 | -end: do |
1095 | - :: source!white |
1096 | - od |
1097 | -} |
1098 | - |
1099 | -#define sw (sent == white) |
1100 | -#define sr (sent == red) |
1101 | -#define sb (sent == blue) |
1102 | - |
1103 | -#define rw (rcvd == white) |
1104 | -#define rr (rcvd == red) |
1105 | -#define rb (rcvd == blue) |
1106 | - |
1107 | -#define LTL 3 |
1108 | -#if LTL==1 |
1109 | - |
1110 | -never { /* ![](sr -> <> rr) */ |
1111 | - /* the never claim is generated by |
1112 | - spin -f "![](sr -> <> rr)" |
1113 | - and then edited a little for readability |
1114 | - the same is true for all others below |
1115 | - */ |
1116 | - do |
1117 | - :: 1 |
1118 | - :: !rr && sr -> goto accept |
1119 | - od; |
1120 | -accept: |
1121 | - if |
1122 | - :: !rr -> goto accept |
1123 | - fi |
1124 | -} |
1125 | - |
1126 | -#endif |
1127 | -#if LTL==2 |
1128 | - |
1129 | -never { /* !rr U rb */ |
1130 | - do |
1131 | - :: !rr |
1132 | - :: rb -> break /* move to implicit 2nd state */ |
1133 | - od |
1134 | -} |
1135 | - |
1136 | -#endif |
1137 | -#if LTL==3 |
1138 | - |
1139 | -never { /* (![](sr -> <> rr)) || (!rr U rb) */ |
1140 | - |
1141 | - if |
1142 | - :: 1 -> goto T0_S5 |
1143 | - :: !rr && sr -> goto accept_S8 |
1144 | - :: !rr -> goto T0_S2 |
1145 | - :: rb -> goto accept_all |
1146 | - fi; |
1147 | -accept_S8: |
1148 | - if |
1149 | - :: !rr -> goto T0_S8 |
1150 | - fi; |
1151 | -T0_S2: |
1152 | - if |
1153 | - :: !rr -> goto T0_S2 |
1154 | - :: rb -> goto accept_all |
1155 | - fi; |
1156 | -T0_S8: |
1157 | - if |
1158 | - :: !rr -> goto accept_S8 |
1159 | - fi; |
1160 | -T0_S5: |
1161 | - if |
1162 | - :: 1 -> goto T0_S5 |
1163 | - :: !rr && sr -> goto accept_S8 |
1164 | - fi; |
1165 | -accept_all: |
1166 | - skip |
1167 | -} |
1168 | -#endif |
1169 | - |
1170 | -#endif |
1171 | //GO.SYSIN DD ex.9c |