1 # To unbundle, sh this file
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
8 //GO.SYSIN DD ex.readme
10 sed 's/.//' >ex.1a <<'//GO.SYSIN DD ex.1a'
19 sed 's/.//' >ex.1b <<'//GO.SYSIN DD ex.1b'
21 - chan dummy = [20] of { byte };
29 sed 's/.//' >ex.1c <<'//GO.SYSIN DD ex.1c'
37 - :: atomic { (b < N) ->
47 sed 's/.//' >ex.2 <<'//GO.SYSIN DD ex.2'
49 -proctype A(chan in, out)
50 -{ byte mt; /* message data */
57 - :: (vr == 1) -> goto S1
58 - :: (vr == 0) -> goto S3
59 - :: printf("AERROR1\n") -> goto S5
66 - :: printf("AERROR2\n"); goto S5
71 -proctype B(chan in, out)
74 - goto S2; /* initial state */
75 -S1: assert(mr == (lmr+1)%MAX);
81 - :: (ar == 1) -> goto S1
82 - :: (ar == 0) -> goto S3
83 - :: printf("ERROR1\n"); goto S5
90 - :: printf("ERROR2\n"); goto S5
96 - chan a2b = [2] of { bit };
97 - chan b2a = [2] of { byte, bit };
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 };
108 -chan dce = [0] of { mtype };
109 -chan dte = [0] of { mtype };
111 -active proctype dte_proc()
115 - :: dce!b -> /* state21 */ dce!a
116 - :: dce!i -> /* state14 */
118 - :: dte?m -> goto state19
121 - :: dte?m -> goto state18
122 - :: dte?u -> goto state08
129 - :: dte?u -> goto state15
130 - :: dte?m -> goto state19
136 - :: dte?m -> goto state19
141 - :: dte?m -> goto state19
146 - :: dte?m -> goto state19
151 - :: dte?m -> goto state19
155 - if /* non-deterministic select */
156 - :: dte?q -> goto state07
158 - :: dte?m -> goto state19
162 - :: dte?m -> goto state19
167 - :: dte?m -> goto state19
172 - :: dte?m -> goto state19
177 - :: dte?m -> goto state19
178 - :: dce!b -> goto state16
183 - :: dte?v -> goto state03
184 - :: dte?m -> goto state19
189 - :: dce!d -> goto state15
190 - :: dte?m -> goto state19
194 - :: dte?m -> goto state19
199 - :: dte?r -> goto state6C
200 - :: dte?m -> goto state19
204 - :: dte?l -> goto state01
205 - :: dte?m -> goto state19
212 - dce!a; goto state01;
218 - dce!a; goto state01
221 -active proctype dce_proc()
225 - :: dce?b -> /* state21 */ dce?a
226 - :: dce?i -> /* state14 */
228 - :: dce?b -> goto state16
231 - :: dte!m -> goto state18
232 - :: dte!u -> goto state08
239 - :: dte!u -> goto state15
240 - :: dce?b -> goto state16
246 - :: dce?b -> goto state16
251 - :: dce?b -> goto state16
256 - :: dce?b -> goto state16
261 - :: dce?b -> goto state16
265 - if /* non-deterministic select */
266 - :: dte!q -> goto state07
268 - :: dce?b -> goto state16
272 - :: dce?b -> goto state16
277 - :: dce?b -> goto state16
282 - :: dce?b -> goto state16
287 - :: dce?b -> goto state16
288 - :: dte!m -> goto state19
293 - :: dte!v -> goto state03
294 - :: dce?b -> goto state16
299 - :: dce?d -> goto state15
300 - :: dce?b -> goto state16
304 - :: dce?b -> goto state16
309 - :: dte!r -> goto state6C
310 - :: dce?b -> goto state16
314 - :: dte!l -> goto state01
315 - :: dce?b -> goto state16
322 - dce?a; goto state01;
328 - dce?a; goto state01
332 sed 's/.//' >ex.4b <<'//GO.SYSIN DD ex.4b'
339 -active [2] proctype user()
340 -{ flag[_pid] = true;
342 - (flag[1-_pid] == false || turn == 1-_pid);
343 -crit: skip; /* critical section */
348 sed 's/.//' >ex.4c <<'//GO.SYSIN DD ex.4c'
351 -active [2] proctype user() /* file ex.4c */
352 -{ byte me = _pid+1; /* me is 1 or 2 */
355 - :: (y != 0 && y != me) -> goto L1 /* try again */
356 - :: (y == 0 || y == me)
360 - :: (x != me) -> goto L1 /* try again */
365 - :: (z != me) -> goto L1 /* try again */
376 sed 's/.//' >ex.5a <<'//GO.SYSIN DD ex.5a'
377 -#define Place byte /* assume < 256 tokens per place */
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
386 -{ p1 = 1; p4 = 1; /* initial marking */
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) }
398 sed 's/.//' >ex.5b <<'//GO.SYSIN DD ex.5b'
399 -#define Place byte /* assume < 256 tokens per place */
401 -Place P1, P2, P4, P5, RC, CC, RD, CD;
402 -Place p1, p2, p4, p5, rc, cc, rd, cd;
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
409 -init /* file ex.5b */
410 -{ P1 = 1; p1 = 1; /* initial marking */
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 */
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 */
431 sed 's/.//' >ex.6 <<'//GO.SYSIN DD ex.6'
433 - Cambridge Ring Protocol [Needham'82]
434 - basic protocol - no LTL properties
441 -#define stimeout empty(sender)
442 -#define rtimeout empty(recv)
444 -#define stimeout timeout
445 -#define rtimeout timeout
448 -#define QSZ 6 /* length of message queues */
451 - RDY, NOTRDY, DATA, NODATA, RESET
453 - chan sender = [QSZ] of { mtype, byte };
454 - chan recv = [QSZ] of { mtype, byte };
456 -active proctype Sender()
457 -{ short n = -1; byte t,m;
465 - :: sender?_,_ -> progress2: skip
467 - :: sender?RESET,0 ->
468 -ackreset: recv!RESET,0; /* stay in idle */
472 - /* E-rep: protocol error */
474 - :: sender?RDY,m -> /* E-exp */
475 - assert(m == (n+1)%4);
476 -advance: n = (n+1)%4;
478 -/* buffer */ :: atomic {
479 - printf("MSC: NEW\n");
483 -/* no buffer */ :: recv!NODATA,n;
487 - :: sender?NOTRDY,m -> /* N-exp */
488 -expected: assert(m == (n+1)%4);
492 - /* ignored (p.154, in [Needham'82]) */
498 -E: /* Essential element sent, ack expected */
501 - :: sender?_,_ -> progress0: skip
503 - :: sender?RESET,0 ->
508 - :: (m == n) -> /* E-rep */
510 - :: (m == (n+1)%4) -> /* E-exp */
514 - :: sender?NOTRDY,m -> /* N-exp */
519 - printf("MSC: STO\n");
520 -retrans: recv!DATA,n /* retransmit */
527 -N: /* Non-essential element sent */
530 - :: sender?_,_ -> progress1: skip
532 - :: sender?RESET,0 ->
535 - :: sender?RDY,m -> /* E-rep */
536 - assert(m == n) /* E-exp: protocol error */
537 - -> recv!NODATA,n /* retransmit and stay in N */
539 - :: recv!DATA,n; /* buffer ready event */
545 - /* ignored (p.154, in [Needham'82]) */
548 -reset: recv!RESET,0;
551 - :: sender?_,_ -> progress3: skip
555 - :: t == RESET -> n = -1; goto I
556 - :: else /* ignored, p. 152 */
558 - :: timeout -> /* a real timeout */
563 -active proctype Receiver()
564 -{ byte t, n, m, Nexp;
572 - :: recv?_,_ -> progress2: skip
575 -ackreset: sender!RESET,0; /* stay in idle */
579 - :: atomic { recv?DATA(m) -> /* E-exp */
581 -advance: printf("MSC: EXP\n");
586 - :: sender!RDY,n; goto E
587 - :: sender!NOTRDY,n; goto N
591 - :: recv?NODATA(m) -> /* N-exp */
594 - /* Timeout: ignored */
596 - /* only receiver can initiate transfer; p. 156 */
597 - :: empty(recv) -> sender!RDY,n; goto E
605 - :: recv?_,_ -> progress1: skip
610 - :: atomic { recv?DATA(m) ->
612 - :: ((m+1)%4 == n) -> /* E-rep */
613 - printf("MSC: REP\n");
615 - :: (m == n) -> /* E-exp */
620 - :: recv?NODATA(m) -> /* N-exp */
625 - printf("MSC: RTO\n");
626 -retrans: sender!RDY,n;
636 - :: recv?_,_ -> progress0: skip
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 */
646 - :: sender!RDY,n -> /* buffer ready event */
649 - /* Timeout: ignored */
656 -reset: sender!RESET,0;
659 - :: recv?_,_ -> progress3: skip
663 - :: t == RESET -> n = 0; Nexp = 0; goto I
664 - :: else /* ignored, p. 152 */
666 - :: timeout -> /* a real timeout */
672 sed 's/.//' >ex.7 <<'//GO.SYSIN DD ex.7'
673 -mtype = { Wakeme, Running };
677 -mtype State = Running;
679 -active proctype client()
681 -sleep: /* sleep routine */
682 - atomic { (lk == 0) -> lk = 1 }; /* spinlock(&lk) */
683 - do /* while r->lock */
684 - :: (r_lock == 1) -> /* r->lock == 1 */
687 - lk = 0; /* freelock(&lk) */
688 - (State == Running); /* wait for wakeup */
689 - :: else -> /* r->lock == 0 */
693 - assert(r_lock == 0); /* should still be true */
694 - r_lock = 1; /* consumed resource */
695 - lk = 0; /* freelock(&lk) */
699 -active proctype server() /* interrupt routine */
701 -wakeup: /* wakeup routine */
702 - r_lock = 0; /* r->lock = 0 */
703 - (lk == 0); /* waitlock(&lk) */
705 - :: r_want -> /* someone is sleeping */
706 - atomic { /* spinlock on sleep queue */
707 - (sleep_q == 0) -> sleep_q = 1
711 - (lk == 0); /* waitlock(&lk) */
714 - :: (State == Wakeme) ->
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
731 -#define elected (nr_leaders > 0)
732 -#define noLeader (nr_leaders == 0)
733 -#define oneLeader (nr_leaders == 1)
739 - * [] (noLeader U oneLeader)
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) */
746 -mtype = { one, two, winner };
747 -chan q[N] = [L] of { mtype, byte};
749 -byte nr_leaders = 0;
751 -proctype node (chan in, out; byte mynumber)
752 -{ bit Active = 1, know_winner = 0;
753 - byte nr, maximum = mynumber, neighbourR;
758 - printf("MSC: %d\n", mynumber);
765 - :: nr != maximum ->
769 - /* Raynal p.39: max is greatest number */
782 - :: neighbourR > nr && neighbourR > maximum ->
783 - maximum = neighbourR;
784 - out!one(neighbourR)
793 - :: nr != mynumber ->
794 - printf("MSC: LOST\n");
796 - printf("MSC: LEADER\n");
798 - assert(nr_leaders == 1)
802 - :: else -> out!winner,nr
814 - run node (q[proc-1], q[proc%N], (N+I-proc)%N+1);
823 -/* !(<>[]oneLeader) */
829 - :: !oneLeader -> goto accept
839 sed 's/.//' >ex.9 <<'//GO.SYSIN DD ex.9'
841 -#define MaxSeq_plus_1 4
842 -#define inc(x) x = (x + 1) % (MaxSeq_plus_1)
844 -chan q[2] = [MaxSeq] of { byte, byte };
846 -active [2] proctype p5()
847 -{ byte NextFrame, AckExp, FrameExp,
858 - :: nbuf < MaxSeq ->
860 - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq_plus_1);
864 - :: r == FrameExp ->
869 - :: ((AckExp <= s) && (s < NextFrame))
870 - || ((AckExp <= s) && (NextFrame < AckExp))
871 - || ((s < NextFrame) && (NextFrame < AckExp)) ->
878 - NextFrame = AckExp;
882 - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq_plus_1);
892 sed 's/.//' >ex.9b <<'//GO.SYSIN DD ex.9b'
894 -#define MaxSeq_plus_1 4
895 -#define inc(x) x = (x + 1) % (MaxSeq + 1)
897 -chan q[2] = [MaxSeq] of { byte, byte };
899 -active [2] proctype p5()
900 -{ byte NextFrame, AckExp, FrameExp,
912 - :: atomic { nbuf < MaxSeq ->
914 - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
915 - printf("MSC: nbuf: %d\n", nbuf);
918 - :: atomic { in?r,s ->
920 - :: r == FrameExp ->
921 - printf("MSC: accept %d\n", r);
924 - -> printf("MSC: reject\n")
929 - :: ((AckExp <= s) && (s < NextFrame))
930 - || ((AckExp <= s) && (NextFrame < AckExp))
931 - || ((s < NextFrame) && (NextFrame < AckExp)) ->
933 - printf("MSC: nbuf: %d\n", nbuf);
936 - printf("MSC: %d %d %d\n", AckExp, s, NextFrame);
942 - NextFrame = AckExp;
943 - printf("MSC: timeout\n");
947 - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
958 sed 's/.//' >ex.9c <<'//GO.SYSIN DD ex.9c'
960 -#define MaxSeq_plus_1 4
961 -#define inc(x) x = (x + 1) % (MaxSeq + 1)
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;
972 - chan q[2] = [MaxSeq] of { byte, byte };
975 -active [2] proctype p5()
976 -{ byte NextFrame, AckExp, FrameExp,
981 - byte frames[MaxSeq_plus_1];
998 - :: _pid%2 -> source?ball
1001 - frames[NextFrame] = ball;
1002 - out!ball, NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
1004 - :: _pid%2 -> sent = ball;
1008 - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
1011 - printf("MSC: nbuf: %d\n", nbuf);
1016 - :: atomic { in?ball,r,s ->
1018 - :: atomic { in?r,s ->
1021 - :: r == FrameExp ->
1023 - printf("MSC: accept %d\n", r);
1028 - :: else -> rcvd = ball
1034 - -> printf("MSC: reject\n")
1040 - :: ((AckExp <= s) && (s < NextFrame))
1041 - || ((AckExp <= s) && (NextFrame < AckExp))
1042 - || ((s < NextFrame) && (NextFrame < AckExp)) ->
1045 - printf("MSC: nbuf: %d\n", nbuf);
1050 - printf("MSC: %d %d %d\n", AckExp, s, NextFrame);
1058 - NextFrame = AckExp;
1060 - printf("MSC: timeout\n");
1067 - :: _pid%2 -> ball = frames[NextFrame]
1070 - out!ball, NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
1072 - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
1084 -active proctype Source()
1088 - :: source!red -> break
1092 - :: source!blue -> break
1099 -#define sw (sent == white)
1100 -#define sr (sent == red)
1101 -#define sb (sent == blue)
1103 -#define rw (rcvd == white)
1104 -#define rr (rcvd == red)
1105 -#define rb (rcvd == blue)
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
1118 - :: !rr && sr -> goto accept
1122 - :: !rr -> goto accept
1129 -never { /* !rr U rb */
1132 - :: rb -> break /* move to implicit 2nd state */
1139 -never { /* (![](sr -> <> rr)) || (!rr U rb) */
1142 - :: 1 -> goto T0_S5
1143 - :: !rr && sr -> goto accept_S8
1144 - :: !rr -> goto T0_S2
1145 - :: rb -> goto accept_all
1149 - :: !rr -> goto T0_S8
1153 - :: !rr -> goto T0_S2
1154 - :: rb -> goto accept_all
1158 - :: !rr -> goto accept_S8
1162 - :: 1 -> goto T0_S5
1163 - :: !rr && sr -> goto accept_S8