projects / lttv.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
convert from svn repository: remove tags directory
[lttv.git] / trunk / verif / Spin / Test / examples
CommitLineData
0b55f123 1# To unbundle, sh this file
2echo ex.readme 1>&2
3sed '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
9echo ex.1a 1>&2
10sed '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
18echo ex.1b 1>&2
19sed '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
28echo ex.1c 1>&2
29sed '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
46echo ex.2 1>&2
47sed '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
104echo ex.3 1>&2
105sed '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
331echo ex.4b 1>&2
332sed '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
347echo ex.4c 1>&2
348sed '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
375echo ex.5a 1>&2
376sed '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
397echo ex.5b 1>&2
398sed '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
430echo ex.6 1>&2
431sed '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
671echo ex.7 1>&2
672sed '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
724echo ex.8 1>&2
725sed '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
838echo ex.9 1>&2
839sed '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
891echo ex.9b 1>&2
892sed '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
957echo ex.9c 1>&2
958sed '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.063897 seconds and 4 git commands to generate.