--- /dev/null
+# To unbundle, sh this file
+echo ex.readme 1>&2
+sed 's/.//' >ex.readme <<'//GO.SYSIN DD ex.readme'
+-The 12 files in this bundle are the PROMELA
+-files of all exercises and examples discussed
+-in the document Doc/Exercises.ps from the
+-SPIN distribution.
+//GO.SYSIN DD ex.readme
+echo ex.1a 1>&2
+sed 's/.//' >ex.1a <<'//GO.SYSIN DD ex.1a'
+-init {
+- byte i = 0;
+- do
+- :: i = i+1
+- od
+-}
+//GO.SYSIN DD ex.1a
+echo ex.1b 1>&2
+sed 's/.//' >ex.1b <<'//GO.SYSIN DD ex.1b'
+-init {
+- chan dummy = [20] of { byte };
+- do
+- :: dummy!85
+- :: dummy!170
+- od
+-}
+//GO.SYSIN DD ex.1b
+echo ex.1c 1>&2
+sed 's/.//' >ex.1c <<'//GO.SYSIN DD ex.1c'
+-#define N 26
+-
+-int a;
+-byte b;
+-
+-init {
+- do
+- :: atomic { (b < N) ->
+- if
+- :: a = a + (1<<b)
+- :: skip
+- fi;
+- b=b+1 }
+- od
+-}
+//GO.SYSIN DD ex.1c
+echo ex.2 1>&2
+sed 's/.//' >ex.2 <<'//GO.SYSIN DD ex.2'
+-#define MAX 8
+-proctype A(chan in, out)
+-{ byte mt; /* message data */
+- bit vr;
+-S1: mt = (mt+1)%MAX;
+- out!mt,1;
+- goto S2;
+-S2: in?vr;
+- if
+- :: (vr == 1) -> goto S1
+- :: (vr == 0) -> goto S3
+- :: printf("AERROR1\n") -> goto S5
+- fi;
+-S3: out!mt,1;
+- goto S4;
+-S4: in?vr;
+- if
+- :: goto S1
+- :: printf("AERROR2\n"); goto S5
+- fi;
+-S5: out!mt,0;
+- goto S4
+-}
+-proctype B(chan in, out)
+-{ byte mr, lmr;
+- bit ar;
+- goto S2; /* initial state */
+-S1: assert(mr == (lmr+1)%MAX);
+- lmr = mr;
+- out!1;
+- goto S2;
+-S2: in?mr,ar;
+- if
+- :: (ar == 1) -> goto S1
+- :: (ar == 0) -> goto S3
+- :: printf("ERROR1\n"); goto S5
+- fi;
+-S3: out!1;
+- goto S2;
+-S4: in?mr,ar;
+- if
+- :: goto S1
+- :: printf("ERROR2\n"); goto S5
+- fi;
+-S5: out!0;
+- goto S4
+-}
+-init {
+- chan a2b = [2] of { bit };
+- chan b2a = [2] of { byte, bit };
+- atomic {
+- run A(a2b, b2a);
+- run B(b2a, a2b)
+- }
+-}
+//GO.SYSIN DD ex.2
+echo ex.3 1>&2
+sed 's/.//' >ex.3 <<'//GO.SYSIN DD ex.3'
+-mtype = { a, b, c, d, e, i, l, m, n, q, r, u, v };
+-
+-chan dce = [0] of { mtype };
+-chan dte = [0] of { mtype };
+-
+-active proctype dte_proc()
+-{
+-state01:
+- do
+- :: dce!b -> /* state21 */ dce!a
+- :: dce!i -> /* state14 */
+- if
+- :: dte?m -> goto state19
+- :: dce!a
+- fi
+- :: dte?m -> goto state18
+- :: dte?u -> goto state08
+- :: dce!d -> break
+- od;
+-
+- /* state02: */
+- if
+- :: dte?v
+- :: dte?u -> goto state15
+- :: dte?m -> goto state19
+- fi;
+-state03:
+- dce!e;
+- /* state04: */
+- if
+- :: dte?m -> goto state19
+- :: dce!c
+- fi;
+- /* state05: */
+- if
+- :: dte?m -> goto state19
+- :: dte?r
+- fi;
+- /* state6A: */
+- if
+- :: dte?m -> goto state19
+- :: dte?q
+- fi;
+-state07:
+- if
+- :: dte?m -> goto state19
+- :: dte?r
+- fi;
+- /* state6B: */
+- if /* non-deterministic select */
+- :: dte?q -> goto state07
+- :: dte?q
+- :: dte?m -> goto state19
+- fi;
+- /* state10: */
+- if
+- :: dte?m -> goto state19
+- :: dte?r
+- fi;
+-state6C:
+- if
+- :: dte?m -> goto state19
+- :: dte?l
+- fi;
+- /* state11: */
+- if
+- :: dte?m -> goto state19
+- :: dte?n
+- fi;
+- /* state12: */
+- if
+- :: dte?m -> goto state19
+- :: dce!b -> goto state16
+- fi;
+-
+-state15:
+- if
+- :: dte?v -> goto state03
+- :: dte?m -> goto state19
+- fi;
+-state08:
+- if
+- :: dce!c
+- :: dce!d -> goto state15
+- :: dte?m -> goto state19
+- fi;
+- /* state09: */
+- if
+- :: dte?m -> goto state19
+- :: dte?q
+- fi;
+- /* state10B: */
+- if
+- :: dte?r -> goto state6C
+- :: dte?m -> goto state19
+- fi;
+-state18:
+- if
+- :: dte?l -> goto state01
+- :: dte?m -> goto state19
+- fi;
+-state16:
+- dte?m;
+- /* state17: */
+- dte?l;
+- /* state21: */
+- dce!a; goto state01;
+-state19:
+- dce!b;
+- /* state20: */
+- dte?l;
+- /* state21: */
+- dce!a; goto state01
+-}
+-
+-active proctype dce_proc()
+-{
+-state01:
+- do
+- :: dce?b -> /* state21 */ dce?a
+- :: dce?i -> /* state14 */
+- if
+- :: dce?b -> goto state16
+- :: dce?a
+- fi
+- :: dte!m -> goto state18
+- :: dte!u -> goto state08
+- :: dce?d -> break
+- od;
+-
+- /* state02: */
+- if
+- :: dte!v
+- :: dte!u -> goto state15
+- :: dce?b -> goto state16
+- fi;
+-state03:
+- dce?e;
+- /* state04: */
+- if
+- :: dce?b -> goto state16
+- :: dce?c
+- fi;
+- /* state05: */
+- if
+- :: dce?b -> goto state16
+- :: dte!r
+- fi;
+- /* state6A: */
+- if
+- :: dce?b -> goto state16
+- :: dte!q
+- fi;
+-state07:
+- if
+- :: dce?b -> goto state16
+- :: dte!r
+- fi;
+- /* state6B: */
+- if /* non-deterministic select */
+- :: dte!q -> goto state07
+- :: dte!q
+- :: dce?b -> goto state16
+- fi;
+- /* state10: */
+- if
+- :: dce?b -> goto state16
+- :: dte!r
+- fi;
+-state6C:
+- if
+- :: dce?b -> goto state16
+- :: dte!l
+- fi;
+- /* state11: */
+- if
+- :: dce?b -> goto state16
+- :: dte!n
+- fi;
+- /* state12: */
+- if
+- :: dce?b -> goto state16
+- :: dte!m -> goto state19
+- fi;
+-
+-state15:
+- if
+- :: dte!v -> goto state03
+- :: dce?b -> goto state16
+- fi;
+-state08:
+- if
+- :: dce?c
+- :: dce?d -> goto state15
+- :: dce?b -> goto state16
+- fi;
+- /* state09: */
+- if
+- :: dce?b -> goto state16
+- :: dte!q
+- fi;
+- /* state10B: */
+- if
+- :: dte!r -> goto state6C
+- :: dce?b -> goto state16
+- fi;
+-state18:
+- if
+- :: dte!l -> goto state01
+- :: dce?b -> goto state16
+- fi;
+-state16:
+- dte!m;
+- /* state17: */
+- dte!l;
+- /* state21: */
+- dce?a; goto state01;
+-state19:
+- dce?b;
+- /* state20: */
+- dte!l;
+- /* state21: */
+- dce?a; goto state01
+-}
+//GO.SYSIN DD ex.3
+echo ex.4b 1>&2
+sed 's/.//' >ex.4b <<'//GO.SYSIN DD ex.4b'
+-#define true 1
+-#define false 0
+-
+-bool flag[2];
+-bool turn;
+-
+-active [2] proctype user()
+-{ flag[_pid] = true;
+- turn = _pid;
+- (flag[1-_pid] == false || turn == 1-_pid);
+-crit: skip; /* critical section */
+- flag[_pid] = false
+-}
+//GO.SYSIN DD ex.4b
+echo ex.4c 1>&2
+sed 's/.//' >ex.4c <<'//GO.SYSIN DD ex.4c'
+-byte in;
+-byte x, y, z;
+-active [2] proctype user() /* file ex.4c */
+-{ byte me = _pid+1; /* me is 1 or 2 */
+-L1: x = me;
+-L2: if
+- :: (y != 0 && y != me) -> goto L1 /* try again */
+- :: (y == 0 || y == me)
+- fi;
+-L3: z = me;
+-L4: if
+- :: (x != me) -> goto L1 /* try again */
+- :: (x == me)
+- fi;
+-L5: y = me;
+-L6: if
+- :: (z != me) -> goto L1 /* try again */
+- :: (z == me)
+- fi;
+-L7: /* success */
+- in = in+1;
+- assert(in == 1);
+- in = in - 1;
+- goto L1
+-}
+//GO.SYSIN DD ex.4c
+echo ex.5a 1>&2
+sed 's/.//' >ex.5a <<'//GO.SYSIN DD ex.5a'
+-#define Place byte /* assume < 256 tokens per place */
+-
+-Place p1, p2, p3;
+-Place p4, p5, p6;
+-#define inp1(x) (x>0) -> x=x-1
+-#define inp2(x,y) (x>0&&y>0) -> x = x-1; y=y-1
+-#define out1(x) x=x+1
+-#define out2(x,y) x=x+1; y=y+1
+-init
+-{ p1 = 1; p4 = 1; /* initial marking */
+- do
+-/*t1*/ :: atomic { inp1(p1) -> out1(p2) }
+-/*t2*/ :: atomic { inp2(p2,p4) -> out1(p3) }
+-/*t3*/ :: atomic { inp1(p3) -> out2(p1,p4) }
+-/*t4*/ :: atomic { inp1(p4) -> out1(p5) }
+-/*t5*/ :: atomic { inp2(p1,p5) -> out1(p6) }
+-/*t6*/ :: atomic { inp1(p6) -> out2(p4,p1) }
+- od
+-}
+//GO.SYSIN DD ex.5a
+echo ex.5b 1>&2
+sed 's/.//' >ex.5b <<'//GO.SYSIN DD ex.5b'
+-#define Place byte /* assume < 256 tokens per place */
+-
+-Place P1, P2, P4, P5, RC, CC, RD, CD;
+-Place p1, p2, p4, p5, rc, cc, rd, cd;
+-
+-#define inp1(x) (x>0) -> x=x-1
+-#define inp2(x,y) (x>0&&y>0) -> x = x-1; y=y-1
+-#define out1(x) x=x+1
+-#define out2(x,y) x=x+1; y=y+1
+-
+-init /* file ex.5b */
+-{ P1 = 1; p1 = 1; /* initial marking */
+- do
+- :: atomic { inp1(P1) -> out2(rc,P2) } /* DC */
+- :: atomic { inp2(P2,CC) -> out1(P4) } /* CA */
+- :: atomic { inp1(P4) -> out2(P5,rd) } /* DD */
+- :: atomic { inp2(P5,CD) -> out1(P1) } /* FD */
+- :: atomic { inp2(P1,RC) -> out2(P4,cc) } /* AC */
+- :: atomic { inp2(P4,RD) -> out2(P1,cd) } /* AD */
+- :: atomic { inp2(P5,RD) -> out1(P1) } /* DA */
+-
+- :: atomic { inp1(p1) -> out2(RC,p2) } /* dc */
+- :: atomic { inp2(p2,cc) -> out1(p4) } /* ca */
+- :: atomic { inp1(p4) -> out2(p5,RD) } /* dd */
+- :: atomic { inp2(p5,cd) -> out1(p1) } /* fd */
+- :: atomic { inp2(p1,rc) -> out2(p4,CC) } /* ac */
+- :: atomic { inp2(p4,rd) -> out2(p1,CD) } /* ad */
+- :: atomic { inp2(p5,rd) -> out1(p1) } /* da */
+- od
+-}
+//GO.SYSIN DD ex.5b
+echo ex.6 1>&2
+sed 's/.//' >ex.6 <<'//GO.SYSIN DD ex.6'
+-#if 0
+- Cambridge Ring Protocol [Needham'82]
+- basic protocol - no LTL properties
+-#endif
+-
+-#define LOSS 1
+-#define RELAXED 1
+-
+-#if RELAXED==1
+-#define stimeout empty(sender)
+-#define rtimeout empty(recv)
+-#else
+-#define stimeout timeout
+-#define rtimeout timeout
+-#endif
+-
+-#define QSZ 6 /* length of message queues */
+-
+- mtype = {
+- RDY, NOTRDY, DATA, NODATA, RESET
+- };
+- chan sender = [QSZ] of { mtype, byte };
+- chan recv = [QSZ] of { mtype, byte };
+-
+-active proctype Sender()
+-{ short n = -1; byte t,m;
+-
+- xr sender;
+- xs recv;
+-
+-I: /* Idle State */
+- do
+-#if LOSS==1
+- :: sender?_,_ -> progress2: skip
+-#endif
+- :: sender?RESET,0 ->
+-ackreset: recv!RESET,0; /* stay in idle */
+- n = -1;
+- goto I
+-
+- /* E-rep: protocol error */
+-
+- :: sender?RDY,m -> /* E-exp */
+- assert(m == (n+1)%4);
+-advance: n = (n+1)%4;
+- if
+-/* buffer */ :: atomic {
+- printf("MSC: NEW\n");
+- recv!DATA,n;
+- goto E
+- }
+-/* no buffer */ :: recv!NODATA,n;
+- goto N
+- fi
+-
+- :: sender?NOTRDY,m -> /* N-exp */
+-expected: assert(m == (n+1)%4);
+- goto I
+-
+- /* Timeout */
+- /* ignored (p.154, in [Needham'82]) */
+-
+- :: goto reset
+-
+- od;
+-
+-E: /* Essential element sent, ack expected */
+- do
+-#if LOSS==1
+- :: sender?_,_ -> progress0: skip
+-#endif
+- :: sender?RESET,0 ->
+- goto ackreset
+-
+- :: sender?RDY,m ->
+- if
+- :: (m == n) -> /* E-rep */
+- goto retrans
+- :: (m == (n+1)%4) -> /* E-exp */
+- goto advance
+- fi
+-
+- :: sender?NOTRDY,m -> /* N-exp */
+- goto expected
+-
+- /* Timeout */
+- :: stimeout ->
+- printf("MSC: STO\n");
+-retrans: recv!DATA,n /* retransmit */
+-
+- :: goto reset
+-
+- od;
+-
+-
+-N: /* Non-essential element sent */
+- do
+-#if LOSS==1
+- :: sender?_,_ -> progress1: skip
+-#endif
+- :: sender?RESET,0 ->
+- goto ackreset
+-
+- :: sender?RDY,m -> /* E-rep */
+- assert(m == n) /* E-exp: protocol error */
+- -> recv!NODATA,n /* retransmit and stay in N */
+-
+- :: recv!DATA,n; /* buffer ready event */
+- goto E
+-
+- :: goto reset
+-
+- /* Timeout */
+- /* ignored (p.154, in [Needham'82]) */
+- od;
+-
+-reset: recv!RESET,0;
+- do
+-#if LOSS==1
+- :: sender?_,_ -> progress3: skip
+-#endif
+- :: sender?t,m ->
+- if
+- :: t == RESET -> n = -1; goto I
+- :: else /* ignored, p. 152 */
+- fi
+- :: timeout -> /* a real timeout */
+- goto reset
+- od
+-}
+-
+-active proctype Receiver()
+-{ byte t, n, m, Nexp;
+-
+- xr recv;
+- xs sender;
+-
+-I: /* Idle State */
+- do
+-#if LOSS==1
+- :: recv?_,_ -> progress2: skip
+-#endif
+- :: recv?RESET,0 ->
+-ackreset: sender!RESET,0; /* stay in idle */
+- n = 0; Nexp = 0;
+- goto I
+-
+- :: atomic { recv?DATA(m) -> /* E-exp */
+- assert(m == n);
+-advance: printf("MSC: EXP\n");
+- n = (n+1)%4;
+- assert(m == Nexp);
+- Nexp = (m+1)%4;
+- if
+- :: sender!RDY,n; goto E
+- :: sender!NOTRDY,n; goto N
+- fi
+- }
+-
+- :: recv?NODATA(m) -> /* N-exp */
+- assert(m == n)
+-
+- /* Timeout: ignored */
+-
+- /* only receiver can initiate transfer; p. 156 */
+- :: empty(recv) -> sender!RDY,n; goto E
+-
+- :: goto reset
+- od;
+-
+-E:
+- do
+-#if LOSS==1
+- :: recv?_,_ -> progress1: skip
+-#endif
+- :: recv?RESET,0 ->
+- goto ackreset
+-
+- :: atomic { recv?DATA(m) ->
+- if
+- :: ((m+1)%4 == n) -> /* E-rep */
+- printf("MSC: REP\n");
+- goto retrans
+- :: (m == n) -> /* E-exp */
+- goto advance
+- fi
+- }
+-
+- :: recv?NODATA(m) -> /* N-exp */
+- assert(m == n);
+- goto I
+-
+- :: rtimeout ->
+- printf("MSC: RTO\n");
+-retrans: sender!RDY,n;
+- goto E
+-
+- :: goto reset
+-
+- od;
+-
+-N:
+- do
+-#if LOSS==1
+- :: recv?_,_ -> progress0: skip
+-#endif
+- :: recv?RESET,0 ->
+- goto ackreset
+-
+- :: recv?DATA(m) -> /* E-rep */
+- assert((m+1)%4 == n); /* E-exp and N-exp: protocol error */
+- printf("MSC: REP\n");
+- sender!NOTRDY,n /* retransmit and stay in N */
+-
+- :: sender!RDY,n -> /* buffer ready event */
+- goto E
+-
+- /* Timeout: ignored */
+-
+- :: goto reset
+-
+- od;
+-
+-progress:
+-reset: sender!RESET,0;
+- do
+-#if LOSS==1
+- :: recv?_,_ -> progress3: skip
+-#endif
+- :: recv?t,m ->
+- if
+- :: t == RESET -> n = 0; Nexp = 0; goto I
+- :: else /* ignored, p. 152 */
+- fi
+- :: timeout -> /* a real timeout */
+- goto reset
+- od
+-}
+//GO.SYSIN DD ex.6
+echo ex.7 1>&2
+sed 's/.//' >ex.7 <<'//GO.SYSIN DD ex.7'
+-mtype = { Wakeme, Running };
+-
+-bit lk, sleep_q;
+-bit r_lock, r_want;
+-mtype State = Running;
+-
+-active proctype client()
+-{
+-sleep: /* sleep routine */
+- atomic { (lk == 0) -> lk = 1 }; /* spinlock(&lk) */
+- do /* while r->lock */
+- :: (r_lock == 1) -> /* r->lock == 1 */
+- r_want = 1;
+- State = Wakeme;
+- lk = 0; /* freelock(&lk) */
+- (State == Running); /* wait for wakeup */
+- :: else -> /* r->lock == 0 */
+- break
+- od;
+-progress:
+- assert(r_lock == 0); /* should still be true */
+- r_lock = 1; /* consumed resource */
+- lk = 0; /* freelock(&lk) */
+- goto sleep
+-}
+-
+-active proctype server() /* interrupt routine */
+-{
+-wakeup: /* wakeup routine */
+- r_lock = 0; /* r->lock = 0 */
+- (lk == 0); /* waitlock(&lk) */
+- if
+- :: r_want -> /* someone is sleeping */
+- atomic { /* spinlock on sleep queue */
+- (sleep_q == 0) -> sleep_q = 1
+- };
+- r_want = 0;
+-#ifdef PROPOSED_FIX
+- (lk == 0); /* waitlock(&lk) */
+-#endif
+- if
+- :: (State == Wakeme) ->
+- State = Running;
+- :: else ->
+- fi;
+- sleep_q = 0
+- :: else ->
+- fi;
+- goto wakeup
+-}
+//GO.SYSIN DD ex.7
+echo ex.8 1>&2
+sed 's/.//' >ex.8 <<'//GO.SYSIN DD ex.8'
+-/* Dolev, Klawe & Rodeh for leader election in unidirectional ring
+- * `An O(n log n) unidirectional distributed algorithm for extrema
+- * finding in a circle,' J. of Algs, Vol 3. (1982), pp. 245-260
+- */
+-
+-#define elected (nr_leaders > 0)
+-#define noLeader (nr_leaders == 0)
+-#define oneLeader (nr_leaders == 1)
+-
+-/* properties:
+- * ![] noLeader
+- * <> elected
+- * <>[]oneLeader
+- * [] (noLeader U oneLeader)
+- */
+-
+-#define N 7 /* nr of processes (use 5 for demos) */
+-#define I 3 /* node given the smallest number */
+-#define L 14 /* size of buffer (>= 2*N) */
+-
+-mtype = { one, two, winner };
+-chan q[N] = [L] of { mtype, byte};
+-
+-byte nr_leaders = 0;
+-
+-proctype node (chan in, out; byte mynumber)
+-{ bit Active = 1, know_winner = 0;
+- byte nr, maximum = mynumber, neighbourR;
+-
+- xr in;
+- xs out;
+-
+- printf("MSC: %d\n", mynumber);
+- out!one(mynumber);
+-end: do
+- :: in?one(nr) ->
+- if
+- :: Active ->
+- if
+- :: nr != maximum ->
+- out!two(nr);
+- neighbourR = nr
+- :: else ->
+- /* Raynal p.39: max is greatest number */
+- assert(nr == N);
+- know_winner = 1;
+- out!winner,nr;
+- fi
+- :: else ->
+- out!one(nr)
+- fi
+-
+- :: in?two(nr) ->
+- if
+- :: Active ->
+- if
+- :: neighbourR > nr && neighbourR > maximum ->
+- maximum = neighbourR;
+- out!one(neighbourR)
+- :: else ->
+- Active = 0
+- fi
+- :: else ->
+- out!two(nr)
+- fi
+- :: in?winner,nr ->
+- if
+- :: nr != mynumber ->
+- printf("MSC: LOST\n");
+- :: else ->
+- printf("MSC: LEADER\n");
+- nr_leaders++;
+- assert(nr_leaders == 1)
+- fi;
+- if
+- :: know_winner
+- :: else -> out!winner,nr
+- fi;
+- break
+- od
+-}
+-
+-init {
+- byte proc;
+- atomic {
+- proc = 1;
+- do
+- :: proc <= N ->
+- run node (q[proc-1], q[proc%N], (N+I-proc)%N+1);
+- proc++
+- :: proc > N ->
+- break
+- od
+- }
+-}
+-
+-#if 0
+-/* !(<>[]oneLeader) */
+-
+-never {
+-T0:
+- if
+- :: skip -> goto T0
+- :: !oneLeader -> goto accept
+- fi;
+-accept:
+- if
+- :: skip -> goto T0
+- fi
+-}
+-#endif
+//GO.SYSIN DD ex.8
+echo ex.9 1>&2
+sed 's/.//' >ex.9 <<'//GO.SYSIN DD ex.9'
+-#define MaxSeq 3
+-#define MaxSeq_plus_1 4
+-#define inc(x) x = (x + 1) % (MaxSeq_plus_1)
+-
+-chan q[2] = [MaxSeq] of { byte, byte };
+-
+-active [2] proctype p5()
+-{ byte NextFrame, AckExp, FrameExp,
+- r, s, nbuf, i;
+- chan in, out;
+-
+- in = q[_pid];
+- out = q[1-_pid];
+-
+- xr in;
+- xs out;
+-
+- do
+- :: nbuf < MaxSeq ->
+- nbuf++;
+- out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq_plus_1);
+- inc(NextFrame)
+- :: in?r,s ->
+- if
+- :: r == FrameExp ->
+- inc(FrameExp)
+- :: else
+- fi;
+- do
+- :: ((AckExp <= s) && (s < NextFrame))
+- || ((AckExp <= s) && (NextFrame < AckExp))
+- || ((s < NextFrame) && (NextFrame < AckExp)) ->
+- nbuf--;
+- inc(AckExp)
+- :: else ->
+- break
+- od
+- :: timeout ->
+- NextFrame = AckExp;
+- i = 1;
+- do
+- :: i <= nbuf ->
+- out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq_plus_1);
+- inc(NextFrame);
+- i++
+- :: else ->
+- break
+- od
+- od
+-}
+//GO.SYSIN DD ex.9
+echo ex.9b 1>&2
+sed 's/.//' >ex.9b <<'//GO.SYSIN DD ex.9b'
+-#define MaxSeq 3
+-#define MaxSeq_plus_1 4
+-#define inc(x) x = (x + 1) % (MaxSeq + 1)
+-
+-chan q[2] = [MaxSeq] of { byte, byte };
+-
+-active [2] proctype p5()
+-{ byte NextFrame, AckExp, FrameExp,
+- r, s, nbuf, i;
+- chan in, out;
+-
+- d_step {
+- in = q[_pid];
+- out = q[1-_pid]
+- };
+- xr in;
+- xs out;
+-
+- do
+- :: atomic { nbuf < MaxSeq ->
+- nbuf++;
+- out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
+- printf("MSC: nbuf: %d\n", nbuf);
+- inc(NextFrame)
+- }
+- :: atomic { in?r,s ->
+- if
+- :: r == FrameExp ->
+- printf("MSC: accept %d\n", r);
+- inc(FrameExp)
+- :: else
+- -> printf("MSC: reject\n")
+- fi
+- };
+- d_step {
+- do
+- :: ((AckExp <= s) && (s < NextFrame))
+- || ((AckExp <= s) && (NextFrame < AckExp))
+- || ((s < NextFrame) && (NextFrame < AckExp)) ->
+- nbuf--;
+- printf("MSC: nbuf: %d\n", nbuf);
+- inc(AckExp)
+- :: else ->
+- printf("MSC: %d %d %d\n", AckExp, s, NextFrame);
+- break
+- od; skip
+- }
+- :: timeout ->
+- d_step {
+- NextFrame = AckExp;
+- printf("MSC: timeout\n");
+- i = 1;
+- do
+- :: i <= nbuf ->
+- out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
+- inc(NextFrame);
+- i++
+- :: else ->
+- break
+- od; i = 0
+- }
+- od
+-}
+//GO.SYSIN DD ex.9b
+echo ex.9c 1>&2
+sed 's/.//' >ex.9c <<'//GO.SYSIN DD ex.9c'
+-#define MaxSeq 3
+-#define MaxSeq_plus_1 4
+-#define inc(x) x = (x + 1) % (MaxSeq + 1)
+-
+-#define CHECKIT
+-
+-#ifdef CHECKIT
+- mtype = { red, white, blue }; /* Wolper's test */
+- chan source = [0] of { mtype };
+- chan q[2] = [MaxSeq] of { mtype, byte, byte };
+- mtype rcvd = white;
+- mtype sent = white;
+-#else
+- chan q[2] = [MaxSeq] of { byte, byte };
+-#endif
+-
+-active [2] proctype p5()
+-{ byte NextFrame, AckExp, FrameExp,
+- r, s, nbuf, i;
+- chan in, out;
+-#ifdef CHECKIT
+- mtype ball;
+- byte frames[MaxSeq_plus_1];
+-#endif
+-
+- d_step {
+- in = q[_pid];
+- out = q[1-_pid]
+- };
+-
+- xr in;
+- xs out;
+-
+- do
+- :: atomic {
+- nbuf < MaxSeq ->
+- nbuf++;
+-#ifdef CHECKIT
+- if
+- :: _pid%2 -> source?ball
+- :: else
+- fi;
+- frames[NextFrame] = ball;
+- out!ball, NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
+- if
+- :: _pid%2 -> sent = ball;
+- :: else
+- fi;
+-#else
+- out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
+-#endif
+-#ifdef VERBOSE
+- printf("MSC: nbuf: %d\n", nbuf);
+-#endif
+- inc(NextFrame)
+- }
+-#ifdef CHECKIT
+- :: atomic { in?ball,r,s ->
+-#else
+- :: atomic { in?r,s ->
+-#endif
+- if
+- :: r == FrameExp ->
+-#ifdef VERBOSE
+- printf("MSC: accept %d\n", r);
+-#endif
+-#ifdef CHECKIT
+- if
+- :: _pid%2
+- :: else -> rcvd = ball
+- fi;
+-#endif
+- inc(FrameExp)
+- :: else
+-#ifdef VERBOSE
+- -> printf("MSC: reject\n")
+-#endif
+- fi
+- };
+- d_step {
+- do
+- :: ((AckExp <= s) && (s < NextFrame))
+- || ((AckExp <= s) && (NextFrame < AckExp))
+- || ((s < NextFrame) && (NextFrame < AckExp)) ->
+- nbuf--;
+-#ifdef VERBOSE
+- printf("MSC: nbuf: %d\n", nbuf);
+-#endif
+- inc(AckExp)
+- :: else ->
+-#ifdef VERBOSE
+- printf("MSC: %d %d %d\n", AckExp, s, NextFrame);
+-#endif
+- break
+- od;
+- skip
+- }
+- :: timeout ->
+- d_step {
+- NextFrame = AckExp;
+-#ifdef VERBOSE
+- printf("MSC: timeout\n");
+-#endif
+- i = 1;
+- do
+- :: i <= nbuf ->
+-#ifdef CHECKIT
+- if
+- :: _pid%2 -> ball = frames[NextFrame]
+- :: else
+- fi;
+- out!ball, NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
+-#else
+- out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
+-#endif
+- inc(NextFrame);
+- i++
+- :: else ->
+- break
+- od;
+- i = 0
+- }
+- od
+-}
+-#ifdef CHECKIT
+-active proctype Source()
+-{
+- do
+- :: source!white
+- :: source!red -> break
+- od;
+- do
+- :: source!white
+- :: source!blue -> break
+- od;
+-end: do
+- :: source!white
+- od
+-}
+-
+-#define sw (sent == white)
+-#define sr (sent == red)
+-#define sb (sent == blue)
+-
+-#define rw (rcvd == white)
+-#define rr (rcvd == red)
+-#define rb (rcvd == blue)
+-
+-#define LTL 3
+-#if LTL==1
+-
+-never { /*  */
+- /* the never claim is generated by
+- spin -f ""
+- and then edited a little for readability
+- the same is true for all others below
+- */
+- do
+- :: 1
+- :: !rr && sr -> goto accept
+- od;
+-accept:
+- if
+- :: !rr -> goto accept
+- fi
+-}
+-
+-#endif
+-#if LTL==2
+-
+-never { /* !rr U rb */
+- do
+- :: !rr
+- :: rb -> break /* move to implicit 2nd state */
+- od
+-}
+-
+-#endif
+-#if LTL==3
+-
+-never { /* () || (!rr U rb) */
+-
+- if
+- :: 1 -> goto T0_S5
+- :: !rr && sr -> goto accept_S8
+- :: !rr -> goto T0_S2
+- :: rb -> goto accept_all
+- fi;
+-accept_S8:
+- if
+- :: !rr -> goto T0_S8
+- fi;
+-T0_S2:
+- if
+- :: !rr -> goto T0_S2
+- :: rb -> goto accept_all
+- fi;
+-T0_S8:
+- if
+- :: !rr -> goto accept_S8
+- fi;
+-T0_S5:
+- if
+- :: 1 -> goto T0_S5
+- :: !rr && sr -> goto accept_S8
+- fi;
+-accept_all:
+- skip
+-}
+-#endif
+-
+-#endif
+//GO.SYSIN DD ex.9c
projects / lttv.git / blobdiff