projects / lttv.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
blame | history | raw | HEAD
move everything out of trunk
[lttv.git] / verif / Spin / Test / examples
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
LTTng 2.x Viewer (LTTV)
This page took 0.052968 seconds and 4 git commands to generate.