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 / Doc / Book91_samples_bundle
CommitLineData
0b55f123 1# To unbundle, sh this file
2echo README 1>&2
3sed 's/.//' >README <<'//GO.SYSIN DD README'
4-Readme
5-------
6-The files in this set contain the text of examples
7-used in the Design and Validation of Computer
8-Protocols book. The name of each file corresponds to the
9-page number in the book where the example appears in its
10-most useful version. The overview below gives a short
11-descriptive phrase for each file.
12-
13-Description Page Nr = Filename
14------------ ------------------
15-hello world = p95.1
16-tiny examples = p94 p95.2 p96.1 p97.1 p97.2 p101 p102 p104.1
17-useful demos = p99 p104.2 p105.2 p116 p248
18-mutual excl. = p96.2 p105.1 p117 p320
19-Lynch's prot. = p107 p312
20-alternatin bit = p123
21-chappe's prot. = p319
22-
23-Large runs
24-----------
25-ackerman's fct = p108 # read info at start of the file
26-
27-Pftp Protocol
28--------------
29-upper tester = p325.test # not runnable
30-flow control l. = p329 p330
31-session layer = p337.pftp.ses p342.pftp.ses1 p347.pftp.ses5
32-all pftp = App.F.pftp - plus 8 include files
33-
34-See also the single file version of pftp in: Test/pftp
35-
36-General
37--------
38-Use these examples for inspiration, and to get quickly
39-acquainted with the language and the Spin software.
40-All examples - except p123 - can be used with both version
41-1 and version 2 of SPIN. (p123 was modifed for versoin 2.0
42-to use the new syntax for remote referencing).
43-If you repeat the runs that are listed in the book for
44-these examples, you should expect to get roughly the same
45-numbers in the result - although in some cases there may
46-be small differences that are due to changes in bookkeeping.
47-
48-For instance, for p329, the book (Spin V1.0) says
49-on pg. 332, using a BITSTATE run, that there are:
50- 90845 + 317134 + 182425 states (stored + linked + matched)
51-Spin V2.0 reports the numbers:
52- 90837 + 317122 + 182421 states (stored + atomic + matched)
53-and when compiled for partial order reduction (-DREDUCE):
54- 74016 + 203616 + 104008 states (stored + atomic + matched)
55-
56-If you repeat a BITSTATE run, of course, by the nature of the
57-machine dependent effect of hashing, you may get different
58-coverage and hash-factors for larger runs. The implementation
59-of the hash functions has also been improved in version 2.0,
60-so the numbers you see will likely differ. The numbers, though,
61-should still be in the same range as those reported in the book.
62-
63-The last set of file (prefixed App.F) is included for completeness.
64-As explained in the book: don't expect to be able to do an
65-exhaustive verification for this specification as listed.
66-In chapter 14 it is illustrated how the spec can be broken up
67-into smaller portions that are more easily verified.
68-
69-Some Small Experiments
70------------------------
71-Try:
72- spin p95.1 # small simulation run
73-
74- spin -s p108 # bigger simulation run, track send stmnts
75-
76- spin -a p312 # lynch's protocol - generate verifier
77- cc -o pan pan.c # compile it for exhaustive verification
78- pan # prove correctness of assertions etc.
79- spin -t -r -s p312 # display the error trace
80-
81-now edit p312 to change all three channel declarations in init
82-to look like: ``chan AtoB = [1] of { mtype byte }''
83-and repeat the above four steps.
84-note the improvement in the trace.
85-
86- spin -a p123 # alternating bit protocol - generate verifier
87- cc -o pan pan.c # compile it for exhaustive verification
88- pan -a # check violations of the never claim
89- spin -t -r -s p123 # display the error trace
90-
91-for more intuitive use of all the above options: try using the
92-graphical interface xspin, and repeat the experiments.
93//GO.SYSIN DD README
94echo App.F.datalink 1>&2
95sed 's/.//' >App.F.datalink <<'//GO.SYSIN DD App.F.datalink'
96-/*
97- * Datalink Layer Validation Model
98- */
99-
100-proctype data_link()
101-{ byte type, seq;
102-
103-end: do
104- :: flow_to_dll[0]?type,seq ->
105- if
106- :: dll_to_flow[1]!type,seq
107- :: skip /* lose message */
108- fi
109- :: flow_to_dll[1]?type,seq ->
110- if
111- :: dll_to_flow[0]!type,seq
112- :: skip /* lose message */
113- fi
114- od
115-}
116//GO.SYSIN DD App.F.datalink
117echo App.F.defines 1>&2
118sed 's/.//' >App.F.defines <<'//GO.SYSIN DD App.F.defines'
119-/*
120- * Global Definitions
121- */
122-
123-#define LOSS 0 /* message loss */
124-#define DUPS 0 /* duplicate msgs */
125-#define QSZ 2 /* queue size */
126-
127-mtype = {
128- red, white, blue,
129- abort, accept, ack, sync_ack, close, connect,
130- create, data, eof, open, reject, sync, transfer,
131- FATAL, NON_FATAL, COMPLETE
132- }
133-
134-chan use_to_pres[2] = [QSZ] of { byte };
135-chan pres_to_use[2] = [QSZ] of { byte };
136-chan pres_to_ses[2] = [QSZ] of { byte };
137-chan ses_to_pres[2] = [QSZ] of { byte, byte };
138-chan ses_to_flow[2] = [QSZ] of { byte, byte };
139-chan flow_to_ses[2] = [QSZ] of { byte, byte };
140-chan dll_to_flow[2] = [QSZ] of { byte, byte };
141-chan flow_to_dll[2] = [QSZ] of { byte, byte };
142-chan ses_to_fsrv[2] = [0] of { byte };
143-chan fsrv_to_ses[2] = [0] of { byte };
144//GO.SYSIN DD App.F.defines
145echo App.F.flow_cl 1>&2
146sed 's/.//' >App.F.flow_cl <<'//GO.SYSIN DD App.F.flow_cl'
147-/*
148- * Flow Control Layer Validation Model
149- */
150-
151-#define true 1
152-#define false 0
153-
154-#define M 4 /* range sequence numbers */
155-#define W 2 /* window size: M/2 */
156-
157-proctype fc(bit n)
158-{ bool busy[M]; /* outstanding messages */
159- byte q; /* seq# oldest unacked msg */
160- byte m; /* seq# last msg received */
161- byte s; /* seq# next msg to send */
162- byte window; /* nr of outstanding msgs */
163- byte type; /* msg type */
164- bit received[M]; /* receiver housekeeping */
165- bit x; /* scratch variable */
166- byte p; /* seq# of last msg acked */
167- byte I_buf[M], O_buf[M]; /* message buffers */
168-
169- /* sender part */
170-end: do
171- :: atomic {
172- (window < W && len(ses_to_flow[n]) > 0
173- && len(flow_to_dll[n]) < QSZ) ->
174- ses_to_flow[n]?type,x;
175- window = window + 1;
176- busy[s] = true;
177- O_buf[s] = type;
178- flow_to_dll[n]!type,s;
179- if
180- :: (type != sync) ->
181- s = (s+1)%M
182- :: (type == sync) ->
183- window = 0;
184- s = M;
185- do
186- :: (s > 0) ->
187- s = s-1;
188- busy[s] = false
189- :: (s == 0) ->
190- break
191- od
192- fi
193- }
194- :: atomic {
195- (window > 0 && busy[q] == false) ->
196- window = window - 1;
197- q = (q+1)%M
198- }
199-#if DUPS
200- :: atomic {
201- (len(flow_to_dll[n]) < QSZ
202- && window > 0 && busy[q] == true) ->
203- flow_to_dll[n]! O_buf[q],q
204- }
205-#endif
206- :: atomic {
207- (timeout && len(flow_to_dll[n]) < QSZ
208- && window > 0 && busy[q] == true) ->
209- flow_to_dll[n]! O_buf[q],q
210- }
211-
212- /* receiver part */
213-#if LOSS
214- :: dll_to_flow[n]?type,m /* lose any message */
215-#endif
216- :: dll_to_flow[n]?type,m ->
217- if
218- :: atomic {
219- (type == ack) ->
220- busy[m] = false
221- }
222- :: atomic {
223- (type == sync) ->
224- flow_to_dll[n]!sync_ack,m;
225- m = 0;
226- do
227- :: (m < M) ->
228- received[m] = 0;
229- m = m+1
230- :: (m == M) ->
231- break
232- od
233- }
234- :: (type == sync_ack) ->
235- flow_to_ses[n]!sync_ack,m
236- :: (type != ack && type != sync && type != sync_ack)->
237- if
238- :: atomic {
239- (received[m] == true) ->
240- x = ((0<p-m && p-m<=W)
241- || (0<p-m+M && p-m+M<=W)) };
242- if
243- :: (x) -> flow_to_dll[n]!ack,m
244- :: (!x) /* else skip */
245- fi
246- :: atomic {
247- (received[m] == false) ->
248- I_buf[m] = type;
249- received[m] = true;
250- received[(m-W+M)%M] = false
251- }
252- fi
253- fi
254- :: (received[p] == true && len(flow_to_ses[n])<QSZ
255- && len(flow_to_dll[n])<QSZ) ->
256- flow_to_ses[n]!I_buf[p],0;
257- flow_to_dll[n]!ack,p;
258- p = (p+1)%M
259- od
260-}
261//GO.SYSIN DD App.F.flow_cl
262echo App.F.fserver 1>&2
263sed 's/.//' >App.F.fserver <<'//GO.SYSIN DD App.F.fserver'
264-/*
265- * File Server Validation Model
266- */
267-
268-proctype fserver(bit n)
269-{
270-end: do
271- :: ses_to_fsrv[n]?create -> /* incoming */
272- if
273- :: fsrv_to_ses[n]!reject
274- :: fsrv_to_ses[n]!accept ->
275- do
276- :: ses_to_fsrv[n]?data
277- :: ses_to_fsrv[n]?eof -> break
278- :: ses_to_fsrv[n]?close -> break
279- od
280- fi
281- :: ses_to_fsrv[n]?open -> /* outgoing */
282- if
283- :: fsrv_to_ses[n]!reject
284- :: fsrv_to_ses[n]!accept ->
285- do
286- :: fsrv_to_ses[n]!data -> progress: skip
287- :: ses_to_fsrv[n]?close -> break
288- :: fsrv_to_ses[n]!eof -> break
289- od
290- fi
291- od
292-}
293//GO.SYSIN DD App.F.fserver
294echo App.F.pftp 1>&2
295sed 's/.//' >App.F.pftp <<'//GO.SYSIN DD App.F.pftp'
296-/*
297- * PROMELA Validation Model - startup script
298- */
299-
300-#include "App.F.defines"
301-#include "App.F.user"
302-#include "App.F.present"
303-#include "App.F.session"
304-#include "App.F.fserver"
305-#include "App.F.flow_cl"
306-#include "App.F.datalink"
307-
308-init
309-{ atomic {
310- run userprc(0); run userprc(1);
311- run present(0); run present(1);
312- run session(0); run session(1);
313- run fserver(0); run fserver(1);
314- run fc(0); run fc(1);
315- run data_link()
316- }
317-}
318//GO.SYSIN DD App.F.pftp
319echo App.F.present 1>&2
320sed 's/.//' >App.F.present <<'//GO.SYSIN DD App.F.present'
321-/*
322- * Presentation Layer Validation Model
323- */
324-
325-proctype present(bit n)
326-{ byte status, uabort;
327-
328-endIDLE:
329- do
330- :: use_to_pres[n]?transfer ->
331- uabort = 0;
332- break
333- :: use_to_pres[n]?abort ->
334- skip
335- od;
336-
337-TRANSFER:
338- pres_to_ses[n]!transfer;
339- do
340- :: use_to_pres[n]?abort ->
341- if
342- :: (!uabort) ->
343- uabort = 1;
344- pres_to_ses[n]!abort
345- :: (uabort) ->
346- assert(1+1!=2)
347- fi
348- :: ses_to_pres[n]?accept,0 ->
349- goto DONE
350- :: ses_to_pres[n]?reject(status) ->
351- if
352- :: (status == FATAL || uabort) ->
353- goto FAIL
354- :: (status == NON_FATAL && !uabort) ->
355-progress: goto TRANSFER
356- fi
357- od;
358-DONE:
359- pres_to_use[n]!accept;
360- goto endIDLE;
361-FAIL:
362- pres_to_use[n]!reject;
363- goto endIDLE
364-}
365//GO.SYSIN DD App.F.present
366echo App.F.session 1>&2
367sed 's/.//' >App.F.session <<'//GO.SYSIN DD App.F.session'
368-/*
369- * Session Layer Validation Model
370- */
371-
372-proctype session(bit n)
373-{ bit toggle;
374- byte type, status;
375-
376-endIDLE:
377- do
378- :: pres_to_ses[n]?type ->
379- if
380- :: (type == transfer) ->
381- goto DATA_OUT
382- :: (type != transfer) /* ignore */
383- fi
384- :: flow_to_ses[n]?type,0 ->
385- if
386- :: (type == connect) ->
387- goto DATA_IN
388- :: (type != connect) /* ignore */
389- fi
390- od;
391-
392-DATA_IN: /* 1. prepare local file fsrver */
393- ses_to_fsrv[n]!create;
394- do
395- :: fsrv_to_ses[n]?reject ->
396- ses_to_flow[n]!reject,0;
397- goto endIDLE
398- :: fsrv_to_ses[n]?accept ->
399- ses_to_flow[n]!accept,0;
400- break
401- od;
402- /* 2. Receive the data, upto eof */
403- do
404- :: flow_to_ses[n]?data,0 ->
405- ses_to_fsrv[n]!data
406- :: flow_to_ses[n]?eof,0 ->
407- ses_to_fsrv[n]!eof;
408- break
409- :: pres_to_ses[n]?transfer ->
410- ses_to_pres[n]!reject(NON_FATAL)
411- :: flow_to_ses[n]?close,0 -> /* remote user aborted */
412- ses_to_fsrv[n]!close;
413- break
414- :: timeout -> /* got disconnected */
415- ses_to_fsrv[n]!close;
416- goto endIDLE
417- od;
418- /* 3. Close the connection */
419- ses_to_flow[n]!close,0;
420- goto endIDLE;
421-
422-DATA_OUT: /* 1. prepare local file fsrver */
423- ses_to_fsrv[n]!open;
424- if
425- :: fsrv_to_ses[n]?reject ->
426- ses_to_pres[n]!reject(FATAL);
427- goto endIDLE
428- :: fsrv_to_ses[n]?accept ->
429- skip
430- fi;
431- /* 2. initialize flow control */
432- ses_to_flow[n]!sync,toggle;
433- do
434- :: atomic {
435- flow_to_ses[n]?sync_ack,type ->
436- if
437- :: (type != toggle)
438- :: (type == toggle) -> break
439- fi
440- }
441- :: timeout ->
442- ses_to_fsrv[n]!close;
443- ses_to_pres[n]!reject(FATAL);
444- goto endIDLE
445- od;
446- toggle = 1 - toggle;
447- /* 3. prepare remote file fsrver */
448- ses_to_flow[n]!connect,0;
449- if
450- :: flow_to_ses[n]?reject,0 ->
451- ses_to_fsrv[n]!close;
452- ses_to_pres[n]!reject(FATAL);
453- goto endIDLE
454- :: flow_to_ses[n]?connect,0 ->
455- ses_to_fsrv[n]!close;
456- ses_to_pres[n]!reject(NON_FATAL);
457- goto endIDLE
458- :: flow_to_ses[n]?accept,0 ->
459- skip
460- :: timeout ->
461- ses_to_fsrv[n]!close;
462- ses_to_pres[n]!reject(FATAL);
463- goto endIDLE
464- fi;
465- /* 4. Transmit the data, upto eof */
466- do
467- :: fsrv_to_ses[n]?data ->
468- ses_to_flow[n]!data,0
469- :: fsrv_to_ses[n]?eof ->
470- ses_to_flow[n]!eof,0;
471- status = COMPLETE;
472- break
473- :: pres_to_ses[n]?abort -> /* local user aborted */
474- ses_to_fsrv[n]!close;
475- ses_to_flow[n]!close,0;
476- status = FATAL;
477- break
478- od;
479- /* 5. Close the connection */
480- do
481- :: pres_to_ses[n]?abort /* ignore */
482- :: flow_to_ses[n]?close,0 ->
483- if
484- :: (status == COMPLETE) ->
485- ses_to_pres[n]!accept,0
486- :: (status != COMPLETE) ->
487- ses_to_pres[n]!reject(status)
488- fi;
489- break
490- :: timeout ->
491- ses_to_pres[n]!reject(FATAL);
492- break
493- od;
494- goto endIDLE
495-}
496//GO.SYSIN DD App.F.session
497echo App.F.user 1>&2
498sed 's/.//' >App.F.user <<'//GO.SYSIN DD App.F.user'
499-/*
500- * User Layer Validation Model
501- */
502-
503-proctype userprc(bit n)
504-{
505- use_to_pres[n]!transfer;
506- if
507- :: pres_to_use[n]?accept -> goto Done
508- :: pres_to_use[n]?reject -> goto Done
509- :: use_to_pres[n]!abort -> goto Aborted
510- fi;
511-Aborted:
512- if
513- :: pres_to_use[n]?accept -> goto Done
514- :: pres_to_use[n]?reject -> goto Done
515- fi;
516-Done:
517- skip
518-}
519//GO.SYSIN DD App.F.user
520echo p101 1>&2
521sed 's/.//' >p101 <<'//GO.SYSIN DD p101'
522-#define msgtype 33
523-
524-chan name = [0] of { byte, byte };
525-
526-/* byte name; typo - this line shouldn't have been here */
527-
528-proctype A()
529-{ name!msgtype(124);
530- name!msgtype(121)
531-}
532-proctype B()
533-{ byte state;
534- name?msgtype(state)
535-}
536-init
537-{ atomic { run A(); run B() }
538-}
539//GO.SYSIN DD p101
540echo p102 1>&2
541sed 's/.//' >p102 <<'//GO.SYSIN DD p102'
542-#define a 1
543-#define b 2
544-
545-chan ch = [1] of { byte };
546-
547-proctype A() { ch!a }
548-proctype B() { ch!b }
549-proctype C()
550-{ if
551- :: ch?a
552- :: ch?b
553- fi
554-}
555-init { atomic { run A(); run B(); run C() } }
556//GO.SYSIN DD p102
557echo p104.1 1>&2
558sed 's/.//' >p104.1 <<'//GO.SYSIN DD p104.1'
559-#define N 128
560-#define size 16
561-
562-chan in = [size] of { short };
563-chan large = [size] of { short };
564-chan small = [size] of { short };
565-
566-proctype split()
567-{ short cargo;
568-
569- do
570- :: in?cargo ->
571- if
572- :: (cargo >= N) -> large!cargo
573- :: (cargo < N) -> small!cargo
574- fi
575- od
576-}
577-init { run split() }
578//GO.SYSIN DD p104.1
579echo p104.2 1>&2
580sed 's/.//' >p104.2 <<'//GO.SYSIN DD p104.2'
581-#define N 128
582-#define size 16
583-
584-chan in = [size] of { short };
585-chan large = [size] of { short };
586-chan small = [size] of { short };
587-
588-proctype split()
589-{ short cargo;
590-
591- do
592- :: in?cargo ->
593- if
594- :: (cargo >= N) -> large!cargo
595- :: (cargo < N) -> small!cargo
596- fi
597- od
598-}
599-proctype merge()
600-{ short cargo;
601-
602- do
603- :: if
604- :: large?cargo
605- :: small?cargo
606- fi;
607- in!cargo
608- od
609-}
610-init
611-{ in!345; in!12; in!6777; in!32; in!0;
612- run split(); run merge()
613-}
614//GO.SYSIN DD p104.2
615echo p105.1 1>&2
616sed 's/.//' >p105.1 <<'//GO.SYSIN DD p105.1'
617-#define p 0
618-#define v 1
619-
620-chan sema = [0] of { bit };
621-
622-proctype dijkstra()
623-{ do
624- :: sema!p -> sema?v
625- od
626-}
627-proctype user()
628-{ sema?p;
629- /* critical section */
630- sema!v
631- /* non-critical section */
632-}
633-init
634-{ atomic {
635- run dijkstra();
636- run user(); run user(); run user()
637- }
638-}
639//GO.SYSIN DD p105.1
640echo p105.2 1>&2
641sed 's/.//' >p105.2 <<'//GO.SYSIN DD p105.2'
642-proctype fact(int n; chan p)
643-{ int result;
644-
645- if
646- :: (n <= 1) -> p!1
647- :: (n >= 2) ->
648- chan child = [1] of { int };
649- run fact(n-1, child);
650- child?result;
651- p!n*result
652- fi
653-}
654-init
655-{ int result;
656- chan child = [1] of { int };
657-
658- run fact(7, child);
659- child?result;
660- printf("result: %d\n", result)
661-}
662//GO.SYSIN DD p105.2
663echo p107 1>&2
664sed 's/.//' >p107 <<'//GO.SYSIN DD p107'
665-mtype = { ack, nak, err, next, accept }
666-
667-proctype transfer(chan in, out, chin, chout)
668-{ byte o, i;
669-
670- in?next(o);
671- do
672- :: chin?nak(i) -> out!accept(i); chout!ack(o)
673- :: chin?ack(i) -> out!accept(i); in?next(o); chout!ack(o)
674- :: chin?err(i) -> chout!nak(o)
675- od
676-}
677-init
678-{ chan AtoB = [1] of { byte, byte };
679- chan BtoA = [1] of { byte, byte };
680- chan Ain = [2] of { byte, byte };
681- chan Bin = [2] of { byte, byte };
682- chan Aout = [2] of { byte, byte };
683- chan Bout = [2] of { byte, byte };
684-
685- atomic {
686- run transfer(Ain, Aout, AtoB, BtoA);
687- run transfer(Bin, Bout, BtoA, AtoB)
688- };
689- AtoB!err(0)
690-}
691//GO.SYSIN DD p107
692echo p108 1>&2
693sed 's/.//' >p108 <<'//GO.SYSIN DD p108'
694-/***** Ackermann's function *****/
695-
696-/* a good example where a simulation run is the
697- better choice - and verification is overkill.
698-
699- 1. simulation
700- -> straight simulation (spin p108) takes
701- -> approx. 6.4 sec on an SGI R3000
702- -> prints the answer: ack(3,3) = 61
703- -> after creating 2433 processes
704-
705- note: all process invocations can, at least in one
706- feasible execution scenario, overlap - if each
707- process chooses to hang around indefinitely in
708- its dying state, at the closing curly brace.
709- this means that the maximum state vector `could' grow
710- to hold all 2433 processes or about 2433*12 bytes of data.
711- the assert(0) at the end makes sure though that the run
712- stops the first time we complete an execution sequence
713- that computes the answer, so the following suffices:
714-
715- 2. verification
716- -> spin -a p108
717- -> cc -DVECTORSZ=2048 -o pan pan.c
718- -> pan -m15000
719- -> which completes in about 5 sec
720- */
721-
722-proctype ack(short a, b; chan ch1)
723-{ chan ch2 = [1] of { short };
724- short ans;
725-
726- if
727- :: (a == 0) ->
728- ans = b+1
729- :: (a != 0) ->
730- if
731- :: (b == 0) ->
732- run ack(a-1, 1, ch2)
733- :: (b != 0) ->
734- run ack(a, b-1, ch2);
735- ch2?ans;
736- run ack(a-1, ans, ch2)
737- fi;
738- ch2?ans
739- fi;
740- ch1!ans
741-}
742-init
743-{ chan ch = [1] of { short };
744- short ans;
745-
746- run ack(3, 3, ch);
747- ch?ans;
748- printf("ack(3,3) = %d\n", ans);
749- assert(0) /* a forced stop, (Chapter 6) */
750-}
751//GO.SYSIN DD p108
752echo p116 1>&2
753sed 's/.//' >p116 <<'//GO.SYSIN DD p116'
754-byte state = 1;
755-
756-proctype A()
757-{ (state == 1) -> state = state + 1;
758- assert(state == 2)
759-}
760-proctype B()
761-{ (state == 1) -> state = state - 1;
762- assert(state == 0)
763-}
764-init { run A(); run B() }
765//GO.SYSIN DD p116
766echo p117 1>&2
767sed 's/.//' >p117 <<'//GO.SYSIN DD p117'
768-#define p 0
769-#define v 1
770-
771-chan sema = [0] of { bit }; /* typo in original `=' was missing */
772-
773-proctype dijkstra()
774-{ do
775- :: sema!p -> sema?v
776- od
777-}
778-byte count;
779-
780-proctype user()
781-{ sema?p;
782- count = count+1;
783- skip; /* critical section */
784- count = count-1;
785- sema!v;
786- skip /* non-critical section */
787-}
788-proctype monitor() { assert(count == 0 || count == 1) }
789-init
790-{ atomic {
791- run dijkstra(); run monitor();
792- run user(); run user(); run user()
793- }
794-}
795//GO.SYSIN DD p117
796echo p123 1>&2
797sed 's/.//' >p123 <<'//GO.SYSIN DD p123'
798-/* alternating bit - version with message loss */
799-
800-#define MAX 3
801-
802-mtype = { msg0, msg1, ack0, ack1 };
803-
804-chan sender =[1] of { byte };
805-chan receiver=[1] of { byte };
806-
807-proctype Sender()
808-{ byte any;
809-again:
810- do
811- :: receiver!msg1;
812- if
813- :: sender?ack1 -> break
814- :: sender?any /* lost */
815- :: timeout /* retransmit */
816- fi
817- od;
818- do
819- :: receiver!msg0;
820- if
821- :: sender?ack0 -> break
822- :: sender?any /* lost */
823- :: timeout /* retransmit */
824- fi
825- od;
826- goto again
827-}
828-
829-proctype Receiver()
830-{ byte any;
831-again:
832- do
833- :: receiver?msg1 -> sender!ack1; break
834- :: receiver?msg0 -> sender!ack0
835- :: receiver?any /* lost */
836- od;
837-P0:
838- do
839- :: receiver?msg0 -> sender!ack0; break
840- :: receiver?msg1 -> sender!ack1
841- :: receiver?any /* lost */
842- od;
843-P1:
844- goto again
845-}
846-
847-init { atomic { run Sender(); run Receiver() } }
848-
849-never {
850- do
851- :: skip /* allow any time delay */
852- :: receiver?[msg0] -> goto accept0
853- :: receiver?[msg1] -> goto accept1
854- od;
855-accept0:
856- do
857- :: !Receiver[2]@P0 /* n.b. new syntax of remote reference */
858- od;
859-accept1:
860- do
861- :: !Receiver[2]@P1
862- od
863-}
864//GO.SYSIN DD p123
865echo p248 1>&2
866sed 's/.//' >p248 <<'//GO.SYSIN DD p248'
867-proctype fact(int n; chan p)
868-{ int result;
869-
870- if
871- :: (n <= 1) -> p!1
872- :: (n >= 2) ->
873- chan child = [1] of { int };
874- run fact(n-1, child);
875- child?result;
876- p!n*result
877- fi
878-}
879-init
880-{ int result;
881- chan child = [1] of { int };
882-
883- run fact(12, child);
884- child?result;
885- printf("result: %d\n", result)
886-}
887//GO.SYSIN DD p248
888echo p312 1>&2
889sed 's/.//' >p312 <<'//GO.SYSIN DD p312'
890-#define MIN 9 /* first data message to send */
891-#define MAX 12 /* last data message to send */
892-#define FILL 99 /* filler message */
893-
894-mtype = { ack, nak, err }
895-
896-proctype transfer(chan chin, chout)
897-{ byte o, i, last_i=MIN;
898-
899- o = MIN+1;
900- do
901- :: chin?nak(i) ->
902- assert(i == last_i+1);
903- chout!ack(o)
904- :: chin?ack(i) ->
905- if
906- :: (o < MAX) -> o = o+1 /* next */
907- :: (o >= MAX) -> o = FILL /* done */
908- fi;
909- chout!ack(o)
910- :: chin?err(i) ->
911- chout!nak(o)
912- od
913-}
914-
915-proctype channel(chan in, out)
916-{ byte md, mt;
917- do
918- :: in?mt,md ->
919- if
920- :: out!mt,md
921- :: out!err,0
922- fi
923- od
924-}
925-
926-init
927-{ chan AtoB = [1] of { byte, byte };
928- chan BtoC = [1] of { byte, byte };
929- chan CtoA = [1] of { byte, byte };
930- atomic {
931- run transfer(AtoB, BtoC);
932- run channel(BtoC, CtoA);
933- run transfer(CtoA, AtoB)
934- };
935- AtoB!err,0 /* start */
936-}
937//GO.SYSIN DD p312
938echo p319 1>&2
939sed 's/.//' >p319 <<'//GO.SYSIN DD p319'
940-#define true 1
941-#define false 0
942-
943-bool busy[3];
944-
945-chan up[3] = [1] of { byte };
946-chan down[3] = [1] of { byte };
947-
948-mtype = { start, attention, data, stop }
949-
950-proctype station(byte id; chan in, out)
951-{ do
952- :: in?start ->
953- atomic { !busy[id] -> busy[id] = true };
954- out!attention;
955- do
956- :: in?data -> out!data
957- :: in?stop -> break
958- od;
959- out!stop;
960- busy[id] = false
961- :: atomic { !busy[id] -> busy[id] = true };
962- out!start;
963- in?attention;
964- do
965- :: out!data -> in?data
966- :: out!stop -> break
967- od;
968- in?stop;
969- busy[id] = false
970- od
971-}
972-
973-init {
974- atomic {
975- run station(0, up[2], down[2]);
976- run station(1, up[0], down[0]);
977- run station(2, up[1], down[1]);
978-
979- run station(0, down[0], up[0]);
980- run station(1, down[1], up[1]);
981- run station(2, down[2], up[2])
982- }
983-}
984//GO.SYSIN DD p319
985echo p320 1>&2
986sed 's/.//' >p320 <<'//GO.SYSIN DD p320'
987-#define true 1
988-#define false 0
989-#define Aturn false
990-#define Bturn true
991-
992-bool x, y, t;
993-bool ain, bin;
994-
995-proctype A()
996-{ x = true;
997- t = Bturn;
998- (y == false || t == Aturn);
999- ain = true;
1000- assert(bin == false); /* critical section */
1001- ain = false;
1002- x = false
1003-}
1004-
1005-proctype B()
1006-{ y = true;
1007- t = Aturn;
1008- (x == false || t == Bturn);
1009- bin = true;
1010- assert(ain == false); /* critical section */
1011- bin = false;
1012- y = false
1013-}
1014-
1015-init
1016-{ run A(); run B()
1017-}
1018//GO.SYSIN DD p320
1019echo p325.test 1>&2
1020sed 's/.//' >p325.test <<'//GO.SYSIN DD p325.test'
1021-proctype test_sender(bit n)
1022-{ byte type, toggle;
1023-
1024- ses_to_flow[n]!sync,toggle;
1025- do
1026- :: flow_to_ses[n]?sync_ack,type ->
1027- if
1028- :: (type != toggle)
1029- :: (type == toggle) -> break
1030- fi
1031- :: timeout ->
1032- ses_to_flow[n]!sync,toggle
1033- od;
1034- toggle = 1 - toggle;
1035-
1036- do
1037- :: ses_to_flow[n]!data,white
1038- :: ses_to_flow[n]!data,red -> break
1039- od;
1040- do
1041- :: ses_to_flow[n]!data,white
1042- :: ses_to_flow[n]!data,blue -> break
1043- od;
1044- do
1045- :: ses_to_flow[n]!data,white
1046- :: break
1047- od
1048-}
1049-proctype test_receiver(bit n)
1050-{
1051- do
1052- :: flow_to_ses[n]?data,white
1053- :: flow_to_ses[n]?data,red -> break
1054- od;
1055- do
1056- :: flow_to_ses[n]?data,white
1057- :: flow_to_ses[n]?data,blue -> break
1058- od;
1059-end: do
1060- :: flow_to_ses[n]?data,white
1061- od
1062-}
1063//GO.SYSIN DD p325.test
1064echo p327.upper 1>&2
1065sed 's/.//' >p327.upper <<'//GO.SYSIN DD p327.upper'
1066-proctype upper()
1067-{ byte s_state, r_state;
1068- byte type, toggle;
1069-
1070- ses_to_flow[0]!sync,toggle;
1071- do
1072- :: flow_to_ses[0]?sync_ack,type ->
1073- if
1074- :: (type != toggle)
1075- :: (type == toggle) -> break
1076- fi
1077- :: timeout ->
1078- ses_to_flow[0]!sync,toggle
1079- od;
1080- toggle = 1 - toggle;
1081-
1082- do
1083- /* sender */
1084- :: ses_to_flow[0]!white,0
1085- :: atomic {
1086- (s_state == 0 && len (ses_to_flow[0]) < QSZ) ->
1087- ses_to_flow[0]!red,0 ->
1088- s_state = 1
1089- }
1090- :: atomic {
1091- (s_state == 1 && len (ses_to_flow[0]) < QSZ) ->
1092- ses_to_flow[0]!blue,0 ->
1093- s_state = 2
1094- }
1095- /* receiver */
1096- :: flow_to_ses[1]?white,0
1097- :: atomic {
1098- (r_state == 0 && flow_to_ses[1]?[red]) ->
1099- flow_to_ses[1]?red,0 ->
1100- r_state = 1
1101- }
1102- :: atomic {
1103- (r_state == 0 && flow_to_ses[1]?[blue]) ->
1104- assert(0)
1105- }
1106- :: atomic {
1107- (r_state == 1 && flow_to_ses[1]?[blue]) ->
1108- flow_to_ses[1]?blue,0;
1109- break
1110- }
1111- :: atomic {
1112- (r_state == 1 && flow_to_ses[1]?[red]) ->
1113- assert(0)
1114- }
1115- od;
1116-end:
1117- do
1118- :: flow_to_ses[1]?white,0
1119- :: flow_to_ses[1]?red,0 -> assert(0)
1120- :: flow_to_ses[1]?blue,0 -> assert(0)
1121- od
1122-}
1123//GO.SYSIN DD p327.upper
1124echo p329 1>&2
1125sed 's/.//' >p329 <<'//GO.SYSIN DD p329'
1126-/*
1127- * PROMELA Validation Model
1128- * FLOW CONTROL LAYER VALIDATION
1129- */
1130-
1131-#define LOSS 0 /* message loss */
1132-#define DUPS 0 /* duplicate msgs */
1133-#define QSZ 2 /* queue size */
1134-
1135-mtype = {
1136- red, white, blue,
1137- abort, accept, ack, sync_ack, close, connect,
1138- create, data, eof, open, reject, sync, transfer,
1139- FATAL, NON_FATAL, COMPLETE
1140- }
1141-
1142-chan ses_to_flow[2] = [QSZ] of { byte, byte };
1143-chan flow_to_ses[2] = [QSZ] of { byte, byte };
1144-chan dll_to_flow[2] = [QSZ] of { byte, byte };
1145-chan flow_to_dll[2];
1146-
1147-#include "App.F.flow_cl"
1148-#include "p327.upper"
1149-
1150-init
1151-{
1152- atomic {
1153- flow_to_dll[0] = dll_to_flow[1];
1154- flow_to_dll[1] = dll_to_flow[0];
1155- run fc(0); run fc(1);
1156- run upper()
1157- }
1158-}
1159//GO.SYSIN DD p329
1160echo p330 1>&2
1161sed 's/.//' >p330 <<'//GO.SYSIN DD p330'
1162-/*
1163- * PROMELA Validation Model
1164- * FLOW CONTROL LAYER VALIDATION
1165- */
1166-
1167-#define LOSS 0 /* message loss */
1168-#define DUPS 0 /* duplicate msgs */
1169-#define QSZ 2 /* queue size */
1170-
1171-mtype = {
1172- red, white, blue,
1173- abort, accept, ack, sync_ack, close, connect,
1174- create, data, eof, open, reject, sync, transfer,
1175- FATAL, NON_FATAL, COMPLETE
1176- }
1177-
1178-chan ses_to_flow[2] = [QSZ] of { byte, byte };
1179-chan flow_to_ses[2] = [QSZ] of { byte, byte };
1180-chan dll_to_flow[2] = [QSZ] of { byte, byte };
1181-chan flow_to_dll[2];
1182-
1183-#include "App.F.flow_cl"
1184-#include "p327.upper"
1185-
1186-init
1187-{
1188- atomic {
1189- flow_to_dll[0] = dll_to_flow[1];
1190- flow_to_dll[1] = dll_to_flow[0];
1191- run fc(0); run fc(1);
1192- run upper()
1193- }
1194-}
1195//GO.SYSIN DD p330
1196echo p337.defines2 1>&2
1197sed 's/.//' >p337.defines2 <<'//GO.SYSIN DD p337.defines2'
1198-/*
1199- * PROMELA Validation Model
1200- * global definitions
1201- */
1202-
1203-#define QSZ 2 /* queue size */
1204-
1205-mtype = {
1206- red, white, blue,
1207- abort, accept, ack, sync_ack, close, connect,
1208- create, data, eof, open, reject, sync, transfer,
1209- FATAL, NON_FATAL, COMPLETE
1210- }
1211-
1212-chan use_to_pres[2] = [QSZ] of { mtype };
1213-chan pres_to_use[2] = [QSZ] of { mtype };
1214-chan pres_to_ses[2] = [QSZ] of { mtype };
1215-chan ses_to_pres[2] = [QSZ] of { mtype, byte };
1216-chan ses_to_flow[2] = [QSZ] of { mtype, byte };
1217-chan ses_to_fsrv[2] = [0] of { mtype };
1218-chan fsrv_to_ses[2] = [0] of { mtype };
1219-chan flow_to_ses[2];
1220//GO.SYSIN DD p337.defines2
1221echo p337.fserver 1>&2
1222sed 's/.//' >p337.fserver <<'//GO.SYSIN DD p337.fserver'
1223-/*
1224- * File Server Validation Model
1225- */
1226-
1227-proctype fserver(bit n)
1228-{
1229-end: do
1230- :: ses_to_fsrv[n]?create -> /* incoming */
1231- if
1232- :: fsrv_to_ses[n]!reject
1233- :: fsrv_to_ses[n]!accept ->
1234- do
1235- :: ses_to_fsrv[n]?data
1236- :: ses_to_fsrv[n]?eof -> break
1237- :: ses_to_fsrv[n]?close -> break
1238- od
1239- fi
1240- :: ses_to_fsrv[n]?open -> /* outgoing */
1241- if
1242- :: fsrv_to_ses[n]!reject
1243- :: fsrv_to_ses[n]!accept ->
1244- do
1245- :: fsrv_to_ses[n]!data -> progress: skip
1246- :: ses_to_fsrv[n]?close -> break
1247- :: fsrv_to_ses[n]!eof -> break
1248- od
1249- fi
1250- od
1251-}
1252//GO.SYSIN DD p337.fserver
1253echo p337.pftp.ses 1>&2
1254sed 's/.//' >p337.pftp.ses <<'//GO.SYSIN DD p337.pftp.ses'
1255-/*
1256- * PROMELA Validation Model
1257- * Session Layer
1258- */
1259-
1260-#include "p337.defines2"
1261-#include "p337.user"
1262-#include "App.F.present"
1263-#include "p337.session"
1264-#include "p337.fserver"
1265-
1266-init
1267-{ atomic {
1268- run userprc(0); run userprc(1);
1269- run present(0); run present(1);
1270- run session(0); run session(1);
1271- run fserver(0); run fserver(1);
1272- flow_to_ses[0] = ses_to_flow[1];
1273- flow_to_ses[1] = ses_to_flow[0]
1274- }
1275-}
1276//GO.SYSIN DD p337.pftp.ses
1277echo p337.session 1>&2
1278sed 's/.//' >p337.session <<'//GO.SYSIN DD p337.session'
1279-/*
1280- * Session Layer Validation Model
1281- */
1282-
1283-proctype session(bit n)
1284-{ bit toggle;
1285- byte type, status;
1286-
1287-endIDLE:
1288- do
1289- :: pres_to_ses[n]?type ->
1290- if
1291- :: (type == transfer) ->
1292- goto DATA_OUT
1293- :: (type != transfer) /* ignore */
1294- fi
1295- :: flow_to_ses[n]?type,0 ->
1296- if
1297- :: (type == connect) ->
1298- goto DATA_IN
1299- :: (type != connect) /* ignore */
1300- fi
1301- od;
1302-
1303-DATA_IN: /* 1. prepare local file fsrver */
1304- ses_to_fsrv[n]!create;
1305- do
1306- :: fsrv_to_ses[n]?reject ->
1307- ses_to_flow[n]!reject,0;
1308- goto endIDLE
1309- :: fsrv_to_ses[n]?accept ->
1310- ses_to_flow[n]!accept,0;
1311- break
1312- od;
1313- /* 2. Receive the data, upto eof */
1314- do
1315- :: flow_to_ses[n]?data,0 ->
1316- ses_to_fsrv[n]!data
1317- :: flow_to_ses[n]?eof,0 ->
1318- ses_to_fsrv[n]!eof;
1319- break
1320- :: pres_to_ses[n]?transfer ->
1321- ses_to_pres[n]!reject(NON_FATAL)
1322- :: flow_to_ses[n]?close,0 -> /* remote user aborted */
1323- ses_to_fsrv[n]!close;
1324- break
1325- :: timeout -> /* got disconnected */
1326- ses_to_fsrv[n]!close;
1327- goto endIDLE
1328- od;
1329- /* 3. Close the connection */
1330- ses_to_flow[n]!close,0;
1331- goto endIDLE;
1332-
1333-DATA_OUT: /* 1. prepare local file fsrver */
1334- ses_to_fsrv[n]!open;
1335- if
1336- :: fsrv_to_ses[n]?reject ->
1337- ses_to_pres[n]!reject(FATAL);
1338- goto endIDLE
1339- :: fsrv_to_ses[n]?accept ->
1340- skip
1341- fi;
1342- /* 2. initialize flow control *** disabled
1343- ses_to_flow[n]!sync,toggle;
1344- do
1345- :: atomic {
1346- flow_to_ses[n]?sync_ack,type ->
1347- if
1348- :: (type != toggle)
1349- :: (type == toggle) -> break
1350- fi
1351- }
1352- :: timeout ->
1353- ses_to_fsrv[n]!close;
1354- ses_to_pres[n]!reject(FATAL);
1355- goto endIDLE
1356- od;
1357- toggle = 1 - toggle;
1358- /* 3. prepare remote file fsrver */
1359- ses_to_flow[n]!connect,0;
1360- if
1361- :: flow_to_ses[n]?reject,0 ->
1362- ses_to_fsrv[n]!close;
1363- ses_to_pres[n]!reject(FATAL);
1364- goto endIDLE
1365- :: flow_to_ses[n]?connect,0 ->
1366- ses_to_fsrv[n]!close;
1367- ses_to_pres[n]!reject(NON_FATAL);
1368- goto endIDLE
1369- :: flow_to_ses[n]?accept,0 ->
1370- skip
1371- :: timeout ->
1372- ses_to_fsrv[n]!close;
1373- ses_to_pres[n]!reject(FATAL);
1374- goto endIDLE
1375- fi;
1376- /* 4. Transmit the data, upto eof */
1377- do
1378- :: fsrv_to_ses[n]?data ->
1379- ses_to_flow[n]!data,0
1380- :: fsrv_to_ses[n]?eof ->
1381- ses_to_flow[n]!eof,0;
1382- status = COMPLETE;
1383- break
1384- :: pres_to_ses[n]?abort -> /* local user aborted */
1385- ses_to_fsrv[n]!close;
1386- ses_to_flow[n]!close,0;
1387- status = FATAL;
1388- break
1389- od;
1390- /* 5. Close the connection */
1391- do
1392- :: pres_to_ses[n]?abort /* ignore */
1393- :: flow_to_ses[n]?close,0 ->
1394- if
1395- :: (status == COMPLETE) ->
1396- ses_to_pres[n]!accept,0
1397- :: (status != COMPLETE) ->
1398- ses_to_pres[n]!reject(status)
1399- fi;
1400- break
1401- :: timeout ->
1402- ses_to_pres[n]!reject(FATAL);
1403- break
1404- od;
1405- goto endIDLE
1406-}
1407//GO.SYSIN DD p337.session
1408echo p337.user 1>&2
1409sed 's/.//' >p337.user <<'//GO.SYSIN DD p337.user'
1410-/*
1411- * User Layer Validation Model
1412- */
1413-
1414-proctype userprc(bit n)
1415-{
1416- use_to_pres[n]!transfer;
1417- if
1418- :: pres_to_use[n]?accept -> goto Done
1419- :: pres_to_use[n]?reject -> goto Done
1420- :: use_to_pres[n]!abort -> goto Aborted
1421- fi;
1422-Aborted:
1423- if
1424- :: pres_to_use[n]?accept -> goto Done
1425- :: pres_to_use[n]?reject -> goto Done
1426- fi;
1427-Done:
1428- skip
1429-}
1430//GO.SYSIN DD p337.user
1431echo p342.pftp.ses1 1>&2
1432sed 's/.//' >p342.pftp.ses1 <<'//GO.SYSIN DD p342.pftp.ses1'
1433-/*
1434- * PROMELA Validation Model
1435- * Session Layer
1436- */
1437-
1438-#include "p337.defines2"
1439-#include "p337.user"
1440-#include "App.F.present"
1441-#include "p337.session"
1442-#include "p337.fserver"
1443-
1444-init
1445-{
1446- atomic {
1447- run userprc(0); run userprc(1);
1448- run present(0); run present(1);
1449- run session(0); run session(1);
1450- run fserver(0); run fserver(1);
1451- flow_to_ses[0] = ses_to_flow[1];
1452- flow_to_ses[1] = ses_to_flow[0]
1453- };
1454- atomic {
1455- byte any;
1456- chan foo = [1] of { byte, byte };
1457- ses_to_flow[0] = foo;
1458- ses_to_flow[1] = foo
1459- };
1460-end: do
1461- :: foo?any,any
1462- od
1463-}
1464//GO.SYSIN DD p342.pftp.ses1
1465echo p343.claim 1>&2
1466sed 's/.//' >p343.claim <<'//GO.SYSIN DD p343.claim'
1467-never {
1468- skip; /* match first step of init (spin version 2.0) */
1469- do
1470- :: !pres_to_ses[0]?[transfer]
1471- && !flow_to_ses[0]?[connect]
1472- :: pres_to_ses[0]?[transfer] ->
1473- goto accept0
1474- :: flow_to_ses[0]?[connect] ->
1475- goto accept1
1476- od;
1477-accept0:
1478- do
1479- :: !ses_to_pres[0]?[accept]
1480- && !ses_to_pres[0]?[reject]
1481- od;
1482-accept1:
1483- do
1484- :: !ses_to_pres[1]?[accept]
1485- && !ses_to_pres[1]?[reject]
1486- od
1487-}
1488//GO.SYSIN DD p343.claim
1489echo p347.pftp.ses5 1>&2
1490sed 's/.//' >p347.pftp.ses5 <<'//GO.SYSIN DD p347.pftp.ses5'
1491-/*
1492- * PROMELA Validation Model
1493- * Session Layer
1494- */
1495-
1496-#include "p337.defines2"
1497-#include "p347.pres.sim"
1498-#include "p347.session.prog"
1499-#include "p337.fserver"
1500-
1501-init
1502-{ atomic {
1503- run present(0); run present(1);
1504- run session(0); run session(1);
1505- run fserver(0); run fserver(1);
1506- flow_to_ses[0] = ses_to_flow[1];
1507- flow_to_ses[1] = ses_to_flow[0]
1508- }
1509-}
1510//GO.SYSIN DD p347.pftp.ses5
1511echo p347.pres.sim 1>&2
1512sed 's/.//' >p347.pres.sim <<'//GO.SYSIN DD p347.pres.sim'
1513-/*
1514- * PROMELA Validation Model
1515- * Presentation & User Layer - combined and reduced
1516- */
1517-
1518-proctype present(bit n)
1519-{ byte status;
1520-progress0:
1521- pres_to_ses[n]!transfer ->
1522- do
1523- :: pres_to_ses[n]!abort;
1524-progress1: skip
1525- :: ses_to_pres[n]?accept,status ->
1526- break
1527- :: ses_to_pres[n]?reject,status ->
1528- if
1529- :: (status == NON_FATAL) ->
1530- goto progress0
1531- :: (status != NON_FATAL) ->
1532- break
1533- fi
1534- od
1535-}
1536//GO.SYSIN DD p347.pres.sim
1537echo p347.session.prog 1>&2
1538sed 's/.//' >p347.session.prog <<'//GO.SYSIN DD p347.session.prog'
1539-/*
1540- * Session Layer Validation Model
1541- */
1542-
1543-proctype session(bit n)
1544-{ bit toggle;
1545- byte type, status;
1546-
1547-endIDLE:
1548- do
1549- :: pres_to_ses[n]?type ->
1550- if
1551- :: (type == transfer) ->
1552- goto progressDATA_OUT
1553- :: (type != transfer) /* ignore */
1554- fi
1555- :: flow_to_ses[n]?type,0 ->
1556- if
1557- :: (type == connect) ->
1558- goto progressDATA_IN
1559- :: (type != connect) /* ignore */
1560- fi
1561- od;
1562-
1563-progressDATA_IN: /* 1. prepare local file fsrver */
1564- ses_to_fsrv[n]!create;
1565- do
1566- :: fsrv_to_ses[n]?reject ->
1567- ses_to_flow[n]!reject,0;
1568- goto endIDLE
1569- :: fsrv_to_ses[n]?accept ->
1570- ses_to_flow[n]!accept,0;
1571- break
1572- od;
1573- /* 2. Receive the data, upto eof */
1574- do
1575- :: flow_to_ses[n]?data,0 ->
1576-progress: ses_to_fsrv[n]!data
1577- :: flow_to_ses[n]?eof,0 ->
1578- ses_to_fsrv[n]!eof;
1579- break
1580- :: pres_to_ses[n]?transfer ->
1581- ses_to_pres[n]!reject(NON_FATAL)
1582- :: flow_to_ses[n]?close,0 -> /* remote user aborted */
1583- ses_to_fsrv[n]!close;
1584- break
1585- :: timeout -> /* got disconnected */
1586- ses_to_fsrv[n]!close;
1587- goto endIDLE
1588- od;
1589- /* 3. Close the connection */
1590- ses_to_flow[n]!close,0;
1591- goto endIDLE;
1592-
1593-progressDATA_OUT: /* 1. prepare local file fsrver */
1594- ses_to_fsrv[n]!open;
1595- if
1596- :: fsrv_to_ses[n]?reject ->
1597- ses_to_pres[n]!reject(FATAL);
1598- goto endIDLE
1599- :: fsrv_to_ses[n]?accept ->
1600- skip
1601- fi;
1602- /* 2. initialize flow control *** disabled
1603- ses_to_flow[n]!sync,toggle;
1604- do
1605- :: atomic {
1606- flow_to_ses[n]?sync_ack,type ->
1607- if
1608- :: (type != toggle)
1609- :: (type == toggle) -> break
1610- fi
1611- }
1612- :: timeout ->
1613- ses_to_fsrv[n]!close;
1614- ses_to_pres[n]!reject(FATAL);
1615- goto endIDLE
1616- od;
1617- toggle = 1 - toggle;
1618- /* 3. prepare remote file fsrver */
1619- ses_to_flow[n]!connect,0;
1620- if
1621- :: flow_to_ses[n]?reject,status ->
1622- ses_to_fsrv[n]!close;
1623- ses_to_pres[n]!reject(FATAL);
1624- goto endIDLE
1625- :: flow_to_ses[n]?connect,0 ->
1626- ses_to_fsrv[n]!close;
1627- ses_to_pres[n]!reject(NON_FATAL);
1628- goto endIDLE
1629- :: flow_to_ses[n]?accept,0 ->
1630- skip
1631- :: timeout ->
1632- ses_to_fsrv[n]!close;
1633- ses_to_pres[n]!reject(FATAL);
1634- goto endIDLE
1635- fi;
1636- /* 4. Transmit the data, upto eof */
1637- do
1638- :: fsrv_to_ses[n]?data ->
1639- ses_to_flow[n]!data,0
1640- :: fsrv_to_ses[n]?eof ->
1641- ses_to_flow[n]!eof,0;
1642- status = COMPLETE;
1643- break
1644- :: pres_to_ses[n]?abort -> /* local user aborted */
1645- ses_to_fsrv[n]!close;
1646- ses_to_flow[n]!close,0;
1647- status = FATAL;
1648- break
1649- od;
1650- /* 5. Close the connection */
1651- do
1652- :: pres_to_ses[n]?abort /* ignore */
1653- :: flow_to_ses[n]?close,0 ->
1654- if
1655- :: (status == COMPLETE) ->
1656- ses_to_pres[n]!accept,0
1657- :: (status != COMPLETE) ->
1658- ses_to_pres[n]!reject(status)
1659- fi;
1660- break
1661- :: timeout ->
1662- ses_to_pres[n]!reject(FATAL);
1663- break
1664- od;
1665- goto endIDLE
1666-}
1667//GO.SYSIN DD p347.session.prog
1668echo p94 1>&2
1669sed 's/.//' >p94 <<'//GO.SYSIN DD p94'
1670-byte state = 2;
1671-
1672-proctype A() { (state == 1) -> state = 3 }
1673-
1674-proctype B() { state = state - 1 }
1675-
1676-/* added: */
1677-init { run A(); run B() }
1678//GO.SYSIN DD p94
1679echo p95.1 1>&2
1680sed 's/.//' >p95.1 <<'//GO.SYSIN DD p95.1'
1681-init { printf("hello world\n") }
1682//GO.SYSIN DD p95.1
1683echo p95.2 1>&2
1684sed 's/.//' >p95.2 <<'//GO.SYSIN DD p95.2'
1685-proctype A(byte state; short set)
1686-{ (state == 1) -> state = set
1687-}
1688-
1689-init { run A(1, 3) }
1690//GO.SYSIN DD p95.2
1691echo p96.1 1>&2
1692sed 's/.//' >p96.1 <<'//GO.SYSIN DD p96.1'
1693-byte state = 1;
1694-
1695-proctype A() { (state == 1) -> state = state + 1 }
1696-
1697-proctype B() { (state == 1) -> state = state - 1 }
1698-
1699-init { run A(); run B() }
1700//GO.SYSIN DD p96.1
1701echo p96.2 1>&2
1702sed 's/.//' >p96.2 <<'//GO.SYSIN DD p96.2'
1703-#define true 1
1704-#define false 0
1705-#define Aturn 1
1706-#define Bturn 0
1707-
1708-bool x, y, t;
1709-
1710-proctype A()
1711-{ x = true;
1712- t = Bturn;
1713- (y == false || t == Aturn);
1714- /* critical section */
1715- x = false
1716-}
1717-proctype B()
1718-{ y = true;
1719- t = Aturn;
1720- (x == false || t == Bturn);
1721- /* critical section */
1722- y = false
1723-}
1724-init { run A(); run B() }
1725//GO.SYSIN DD p96.2
1726echo p97.1 1>&2
1727sed 's/.//' >p97.1 <<'//GO.SYSIN DD p97.1'
1728-byte state = 1;
1729-proctype A() { atomic { (state == 1) -> state = state + 1 } }
1730-proctype B() { atomic { (state == 1) -> state = state - 1 } }
1731-init { run A(); run B() }
1732//GO.SYSIN DD p97.1
1733echo p97.2 1>&2
1734sed 's/.//' >p97.2 <<'//GO.SYSIN DD p97.2'
1735-proctype nr(short pid, a, b)
1736-{ int res;
1737-
1738-atomic { res = (a*a+b)/2*a;
1739- printf("result %d: %d\n", pid, res)
1740- }
1741-}
1742-init { run nr(1,1,1); run nr(1,2,2); run nr(1,3,2) }
1743//GO.SYSIN DD p97.2
1744echo p99 1>&2
1745sed 's/.//' >p99 <<'//GO.SYSIN DD p99'
1746-proctype A(chan q1)
1747-{ chan q2;
1748-
1749- q1?q2;
1750- q2!123
1751-}
1752-
1753-proctype B(chan qforb)
1754-{ int x;
1755-
1756- qforb?x;
1757- printf("x = %d\n", x)
1758-}
1759-
1760-init
1761-{ chan qname[2] = [1] of { chan };
1762- chan qforb = [1] of { int };
1763-
1764- run A(qname[0]);
1765- run B(qforb);
1766-
1767- qname[0]!qforb
1768-}
1769//GO.SYSIN DD p99
LTTng 2.x Viewer (LTTV)
This page took 0.085212 seconds and 4 git commands to generate.