1 # To unbundle, sh this file
3 sed 's/.//' >README <<'//GO.SYSIN DD README'
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.
13 -Description Page Nr = Filename
14 ------------ ------------------
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
25 -ackerman's fct = p108 # read info at start of the file
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
34 -See also the single file version of pftp in: Test/pftp
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.
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)
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.
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.
69 -Some Small Experiments
70 ------------------------
72 - spin p95.1 # small simulation run
74 - spin -s p108 # bigger simulation run, track send stmnts
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
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.
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
91 -for more intuitive use of all the above options: try using the
92 -graphical interface xspin, and repeat the experiments.
94 echo App.F.datalink 1>&2
95 sed 's/.//' >App.F.datalink <<'//GO.SYSIN DD App.F.datalink'
97 - * Datalink Layer Validation Model
100 -proctype data_link()
104 - :: flow_to_dll[0]?type,seq ->
106 - :: dll_to_flow[1]!type,seq
107 - :: skip /* lose message */
109 - :: flow_to_dll[1]?type,seq ->
111 - :: dll_to_flow[0]!type,seq
112 - :: skip /* lose message */
116 //GO.SYSIN DD App.F.datalink
117 echo App.F.defines 1>&2
118 sed 's/.//' >App.F.defines <<'//GO.SYSIN DD App.F.defines'
120 - * Global Definitions
123 -#define LOSS 0 /* message loss */
124 -#define DUPS 0 /* duplicate msgs */
125 -#define QSZ 2 /* queue size */
129 - abort, accept, ack, sync_ack, close, connect,
130 - create, data, eof, open, reject, sync, transfer,
131 - FATAL, NON_FATAL, COMPLETE
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
145 echo App.F.flow_cl 1>&2
146 sed 's/.//' >App.F.flow_cl <<'//GO.SYSIN DD App.F.flow_cl'
148 - * Flow Control Layer Validation Model
154 -#define M 4 /* range sequence numbers */
155 -#define W 2 /* window size: M/2 */
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 */
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;
178 - flow_to_dll[n]!type,s;
180 - :: (type != sync) ->
182 - :: (type == sync) ->
195 - (window > 0 && busy[q] == false) ->
196 - window = window - 1;
201 - (len(flow_to_dll[n]) < QSZ
202 - && window > 0 && busy[q] == true) ->
203 - flow_to_dll[n]! O_buf[q],q
207 - (timeout && len(flow_to_dll[n]) < QSZ
208 - && window > 0 && busy[q] == true) ->
209 - flow_to_dll[n]! O_buf[q],q
212 - /* receiver part */
214 - :: dll_to_flow[n]?type,m /* lose any message */
216 - :: dll_to_flow[n]?type,m ->
224 - flow_to_dll[n]!sync_ack,m;
234 - :: (type == sync_ack) ->
235 - flow_to_ses[n]!sync_ack,m
236 - :: (type != ack && type != sync && type != sync_ack)->
239 - (received[m] == true) ->
240 - x = ((0<p-m && p-m<=W)
241 - || (0<p-m+M && p-m+M<=W)) };
243 - :: (x) -> flow_to_dll[n]!ack,m
244 - :: (!x) /* else skip */
247 - (received[m] == false) ->
249 - received[m] = true;
250 - received[(m-W+M)%M] = false
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;
261 //GO.SYSIN DD App.F.flow_cl
262 echo App.F.fserver 1>&2
263 sed 's/.//' >App.F.fserver <<'//GO.SYSIN DD App.F.fserver'
265 - * File Server Validation Model
268 -proctype fserver(bit n)
271 - :: ses_to_fsrv[n]?create -> /* incoming */
273 - :: fsrv_to_ses[n]!reject
274 - :: fsrv_to_ses[n]!accept ->
276 - :: ses_to_fsrv[n]?data
277 - :: ses_to_fsrv[n]?eof -> break
278 - :: ses_to_fsrv[n]?close -> break
281 - :: ses_to_fsrv[n]?open -> /* outgoing */
283 - :: fsrv_to_ses[n]!reject
284 - :: fsrv_to_ses[n]!accept ->
286 - :: fsrv_to_ses[n]!data -> progress: skip
287 - :: ses_to_fsrv[n]?close -> break
288 - :: fsrv_to_ses[n]!eof -> break
293 //GO.SYSIN DD App.F.fserver
295 sed 's/.//' >App.F.pftp <<'//GO.SYSIN DD App.F.pftp'
297 - * PROMELA Validation Model - startup script
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"
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);
318 //GO.SYSIN DD App.F.pftp
319 echo App.F.present 1>&2
320 sed 's/.//' >App.F.present <<'//GO.SYSIN DD App.F.present'
322 - * Presentation Layer Validation Model
325 -proctype present(bit n)
326 -{ byte status, uabort;
330 - :: use_to_pres[n]?transfer ->
333 - :: use_to_pres[n]?abort ->
338 - pres_to_ses[n]!transfer;
340 - :: use_to_pres[n]?abort ->
344 - pres_to_ses[n]!abort
348 - :: ses_to_pres[n]?accept,0 ->
350 - :: ses_to_pres[n]?reject(status) ->
352 - :: (status == FATAL || uabort) ->
354 - :: (status == NON_FATAL && !uabort) ->
355 -progress: goto TRANSFER
359 - pres_to_use[n]!accept;
362 - pres_to_use[n]!reject;
365 //GO.SYSIN DD App.F.present
366 echo App.F.session 1>&2
367 sed 's/.//' >App.F.session <<'//GO.SYSIN DD App.F.session'
369 - * Session Layer Validation Model
372 -proctype session(bit n)
378 - :: pres_to_ses[n]?type ->
380 - :: (type == transfer) ->
382 - :: (type != transfer) /* ignore */
384 - :: flow_to_ses[n]?type,0 ->
386 - :: (type == connect) ->
388 - :: (type != connect) /* ignore */
392 -DATA_IN: /* 1. prepare local file fsrver */
393 - ses_to_fsrv[n]!create;
395 - :: fsrv_to_ses[n]?reject ->
396 - ses_to_flow[n]!reject,0;
398 - :: fsrv_to_ses[n]?accept ->
399 - ses_to_flow[n]!accept,0;
402 - /* 2. Receive the data, upto eof */
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;
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;
414 - :: timeout -> /* got disconnected */
415 - ses_to_fsrv[n]!close;
418 - /* 3. Close the connection */
419 - ses_to_flow[n]!close,0;
422 -DATA_OUT: /* 1. prepare local file fsrver */
423 - ses_to_fsrv[n]!open;
425 - :: fsrv_to_ses[n]?reject ->
426 - ses_to_pres[n]!reject(FATAL);
428 - :: fsrv_to_ses[n]?accept ->
431 - /* 2. initialize flow control */
432 - ses_to_flow[n]!sync,toggle;
435 - flow_to_ses[n]?sync_ack,type ->
437 - :: (type != toggle)
438 - :: (type == toggle) -> break
442 - ses_to_fsrv[n]!close;
443 - ses_to_pres[n]!reject(FATAL);
446 - toggle = 1 - toggle;
447 - /* 3. prepare remote file fsrver */
448 - ses_to_flow[n]!connect,0;
450 - :: flow_to_ses[n]?reject,0 ->
451 - ses_to_fsrv[n]!close;
452 - ses_to_pres[n]!reject(FATAL);
454 - :: flow_to_ses[n]?connect,0 ->
455 - ses_to_fsrv[n]!close;
456 - ses_to_pres[n]!reject(NON_FATAL);
458 - :: flow_to_ses[n]?accept,0 ->
461 - ses_to_fsrv[n]!close;
462 - ses_to_pres[n]!reject(FATAL);
465 - /* 4. Transmit the data, upto eof */
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;
473 - :: pres_to_ses[n]?abort -> /* local user aborted */
474 - ses_to_fsrv[n]!close;
475 - ses_to_flow[n]!close,0;
479 - /* 5. Close the connection */
481 - :: pres_to_ses[n]?abort /* ignore */
482 - :: flow_to_ses[n]?close,0 ->
484 - :: (status == COMPLETE) ->
485 - ses_to_pres[n]!accept,0
486 - :: (status != COMPLETE) ->
487 - ses_to_pres[n]!reject(status)
491 - ses_to_pres[n]!reject(FATAL);
496 //GO.SYSIN DD App.F.session
498 sed 's/.//' >App.F.user <<'//GO.SYSIN DD App.F.user'
500 - * User Layer Validation Model
503 -proctype userprc(bit n)
505 - use_to_pres[n]!transfer;
507 - :: pres_to_use[n]?accept -> goto Done
508 - :: pres_to_use[n]?reject -> goto Done
509 - :: use_to_pres[n]!abort -> goto Aborted
513 - :: pres_to_use[n]?accept -> goto Done
514 - :: pres_to_use[n]?reject -> goto Done
519 //GO.SYSIN DD App.F.user
521 sed 's/.//' >p101 <<'//GO.SYSIN DD p101'
524 -chan name = [0] of { byte, byte };
526 -/* byte name; typo - this line shouldn't have been here */
529 -{ name!msgtype(124);
534 - name?msgtype(state)
537 -{ atomic { run A(); run B() }
541 sed 's/.//' >p102 <<'//GO.SYSIN DD p102'
545 -chan ch = [1] of { byte };
547 -proctype A() { ch!a }
548 -proctype B() { ch!b }
555 -init { atomic { run A(); run B(); run C() } }
558 sed 's/.//' >p104.1 <<'//GO.SYSIN DD p104.1'
562 -chan in = [size] of { short };
563 -chan large = [size] of { short };
564 -chan small = [size] of { short };
572 - :: (cargo >= N) -> large!cargo
573 - :: (cargo < N) -> small!cargo
577 -init { run split() }
580 sed 's/.//' >p104.2 <<'//GO.SYSIN DD p104.2'
584 -chan in = [size] of { short };
585 -chan large = [size] of { short };
586 -chan small = [size] of { short };
594 - :: (cargo >= N) -> large!cargo
595 - :: (cargo < N) -> small!cargo
611 -{ in!345; in!12; in!6777; in!32; in!0;
612 - run split(); run merge()
616 sed 's/.//' >p105.1 <<'//GO.SYSIN DD p105.1'
620 -chan sema = [0] of { bit };
624 - :: sema!p -> sema?v
629 - /* critical section */
631 - /* non-critical section */
636 - run user(); run user(); run user()
641 sed 's/.//' >p105.2 <<'//GO.SYSIN DD p105.2'
642 -proctype fact(int n; chan p)
648 - chan child = [1] of { int };
649 - run fact(n-1, child);
656 - chan child = [1] of { int };
658 - run fact(7, child);
660 - printf("result: %d\n", result)
664 sed 's/.//' >p107 <<'//GO.SYSIN DD p107'
665 -mtype = { ack, nak, err, next, accept }
667 -proctype transfer(chan in, out, chin, chout)
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)
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 };
686 - run transfer(Ain, Aout, AtoB, BtoA);
687 - run transfer(Bin, Bout, BtoA, AtoB)
693 sed 's/.//' >p108 <<'//GO.SYSIN DD p108'
694 -/***** Ackermann's function *****/
696 -/* a good example where a simulation run is the
697 - better choice - and verification is overkill.
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
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:
717 - -> cc -DVECTORSZ=2048 -o pan pan.c
719 - -> which completes in about 5 sec
722 -proctype ack(short a, b; chan ch1)
723 -{ chan ch2 = [1] of { short };
732 - run ack(a-1, 1, ch2)
734 - run ack(a, b-1, ch2);
736 - run ack(a-1, ans, ch2)
743 -{ chan ch = [1] of { short };
748 - printf("ack(3,3) = %d\n", ans);
749 - assert(0) /* a forced stop, (Chapter 6) */
753 sed 's/.//' >p116 <<'//GO.SYSIN DD p116'
757 -{ (state == 1) -> state = state + 1;
761 -{ (state == 1) -> state = state - 1;
764 -init { run A(); run B() }
767 sed 's/.//' >p117 <<'//GO.SYSIN DD p117'
771 -chan sema = [0] of { bit }; /* typo in original `=' was missing */
775 - :: sema!p -> sema?v
783 - skip; /* critical section */
786 - skip /* non-critical section */
788 -proctype monitor() { assert(count == 0 || count == 1) }
791 - run dijkstra(); run monitor();
792 - run user(); run user(); run user()
797 sed 's/.//' >p123 <<'//GO.SYSIN DD p123'
798 -/* alternating bit - version with message loss */
802 -mtype = { msg0, msg1, ack0, ack1 };
804 -chan sender =[1] of { byte };
805 -chan receiver=[1] of { byte };
813 - :: sender?ack1 -> break
814 - :: sender?any /* lost */
815 - :: timeout /* retransmit */
821 - :: sender?ack0 -> break
822 - :: sender?any /* lost */
823 - :: timeout /* retransmit */
833 - :: receiver?msg1 -> sender!ack1; break
834 - :: receiver?msg0 -> sender!ack0
835 - :: receiver?any /* lost */
839 - :: receiver?msg0 -> sender!ack0; break
840 - :: receiver?msg1 -> sender!ack1
841 - :: receiver?any /* lost */
847 -init { atomic { run Sender(); run Receiver() } }
851 - :: skip /* allow any time delay */
852 - :: receiver?[msg0] -> goto accept0
853 - :: receiver?[msg1] -> goto accept1
857 - :: !Receiver[2]@P0 /* n.b. new syntax of remote reference */
866 sed 's/.//' >p248 <<'//GO.SYSIN DD p248'
867 -proctype fact(int n; chan p)
873 - chan child = [1] of { int };
874 - run fact(n-1, child);
881 - chan child = [1] of { int };
883 - run fact(12, child);
885 - printf("result: %d\n", result)
889 sed '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 */
894 -mtype = { ack, nak, err }
896 -proctype transfer(chan chin, chout)
897 -{ byte o, i, last_i=MIN;
902 - assert(i == last_i+1);
906 - :: (o < MAX) -> o = o+1 /* next */
907 - :: (o >= MAX) -> o = FILL /* done */
915 -proctype channel(chan in, out)
927 -{ chan AtoB = [1] of { byte, byte };
928 - chan BtoC = [1] of { byte, byte };
929 - chan CtoA = [1] of { byte, byte };
931 - run transfer(AtoB, BtoC);
932 - run channel(BtoC, CtoA);
933 - run transfer(CtoA, AtoB)
935 - AtoB!err,0 /* start */
939 sed 's/.//' >p319 <<'//GO.SYSIN DD p319'
945 -chan up[3] = [1] of { byte };
946 -chan down[3] = [1] of { byte };
948 -mtype = { start, attention, data, stop }
950 -proctype station(byte id; chan in, out)
953 - atomic { !busy[id] -> busy[id] = true };
956 - :: in?data -> out!data
957 - :: in?stop -> break
961 - :: atomic { !busy[id] -> busy[id] = true };
965 - :: out!data -> in?data
966 - :: out!stop -> break
975 - run station(0, up[2], down[2]);
976 - run station(1, up[0], down[0]);
977 - run station(2, up[1], down[1]);
979 - run station(0, down[0], up[0]);
980 - run station(1, down[1], up[1]);
981 - run station(2, down[2], up[2])
986 sed 's/.//' >p320 <<'//GO.SYSIN DD p320'
998 - (y == false || t == Aturn);
1000 - assert(bin == false); /* critical section */
1008 - (x == false || t == Bturn);
1010 - assert(ain == false); /* critical section */
1020 sed 's/.//' >p325.test <<'//GO.SYSIN DD p325.test'
1021 -proctype test_sender(bit n)
1022 -{ byte type, toggle;
1024 - ses_to_flow[n]!sync,toggle;
1026 - :: flow_to_ses[n]?sync_ack,type ->
1028 - :: (type != toggle)
1029 - :: (type == toggle) -> break
1032 - ses_to_flow[n]!sync,toggle
1034 - toggle = 1 - toggle;
1037 - :: ses_to_flow[n]!data,white
1038 - :: ses_to_flow[n]!data,red -> break
1041 - :: ses_to_flow[n]!data,white
1042 - :: ses_to_flow[n]!data,blue -> break
1045 - :: ses_to_flow[n]!data,white
1049 -proctype test_receiver(bit n)
1052 - :: flow_to_ses[n]?data,white
1053 - :: flow_to_ses[n]?data,red -> break
1056 - :: flow_to_ses[n]?data,white
1057 - :: flow_to_ses[n]?data,blue -> break
1060 - :: flow_to_ses[n]?data,white
1063 //GO.SYSIN DD p325.test
1064 echo p327.upper 1>&2
1065 sed 's/.//' >p327.upper <<'//GO.SYSIN DD p327.upper'
1067 -{ byte s_state, r_state;
1068 - byte type, toggle;
1070 - ses_to_flow[0]!sync,toggle;
1072 - :: flow_to_ses[0]?sync_ack,type ->
1074 - :: (type != toggle)
1075 - :: (type == toggle) -> break
1078 - ses_to_flow[0]!sync,toggle
1080 - toggle = 1 - toggle;
1084 - :: ses_to_flow[0]!white,0
1086 - (s_state == 0 && len (ses_to_flow[0]) < QSZ) ->
1087 - ses_to_flow[0]!red,0 ->
1091 - (s_state == 1 && len (ses_to_flow[0]) < QSZ) ->
1092 - ses_to_flow[0]!blue,0 ->
1096 - :: flow_to_ses[1]?white,0
1098 - (r_state == 0 && flow_to_ses[1]?[red]) ->
1099 - flow_to_ses[1]?red,0 ->
1103 - (r_state == 0 && flow_to_ses[1]?[blue]) ->
1107 - (r_state == 1 && flow_to_ses[1]?[blue]) ->
1108 - flow_to_ses[1]?blue,0;
1112 - (r_state == 1 && flow_to_ses[1]?[red]) ->
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)
1123 //GO.SYSIN DD p327.upper
1125 sed 's/.//' >p329 <<'//GO.SYSIN DD p329'
1127 - * PROMELA Validation Model
1128 - * FLOW CONTROL LAYER VALIDATION
1131 -#define LOSS 0 /* message loss */
1132 -#define DUPS 0 /* duplicate msgs */
1133 -#define QSZ 2 /* queue size */
1137 - abort, accept, ack, sync_ack, close, connect,
1138 - create, data, eof, open, reject, sync, transfer,
1139 - FATAL, NON_FATAL, COMPLETE
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];
1147 -#include "App.F.flow_cl"
1148 -#include "p327.upper"
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);
1161 sed 's/.//' >p330 <<'//GO.SYSIN DD p330'
1163 - * PROMELA Validation Model
1164 - * FLOW CONTROL LAYER VALIDATION
1167 -#define LOSS 0 /* message loss */
1168 -#define DUPS 0 /* duplicate msgs */
1169 -#define QSZ 2 /* queue size */
1173 - abort, accept, ack, sync_ack, close, connect,
1174 - create, data, eof, open, reject, sync, transfer,
1175 - FATAL, NON_FATAL, COMPLETE
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];
1183 -#include "App.F.flow_cl"
1184 -#include "p327.upper"
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);
1196 echo p337.defines2 1>&2
1197 sed 's/.//' >p337.defines2 <<'//GO.SYSIN DD p337.defines2'
1199 - * PROMELA Validation Model
1200 - * global definitions
1203 -#define QSZ 2 /* queue size */
1207 - abort, accept, ack, sync_ack, close, connect,
1208 - create, data, eof, open, reject, sync, transfer,
1209 - FATAL, NON_FATAL, COMPLETE
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
1221 echo p337.fserver 1>&2
1222 sed 's/.//' >p337.fserver <<'//GO.SYSIN DD p337.fserver'
1224 - * File Server Validation Model
1227 -proctype fserver(bit n)
1230 - :: ses_to_fsrv[n]?create -> /* incoming */
1232 - :: fsrv_to_ses[n]!reject
1233 - :: fsrv_to_ses[n]!accept ->
1235 - :: ses_to_fsrv[n]?data
1236 - :: ses_to_fsrv[n]?eof -> break
1237 - :: ses_to_fsrv[n]?close -> break
1240 - :: ses_to_fsrv[n]?open -> /* outgoing */
1242 - :: fsrv_to_ses[n]!reject
1243 - :: fsrv_to_ses[n]!accept ->
1245 - :: fsrv_to_ses[n]!data -> progress: skip
1246 - :: ses_to_fsrv[n]?close -> break
1247 - :: fsrv_to_ses[n]!eof -> break
1252 //GO.SYSIN DD p337.fserver
1253 echo p337.pftp.ses 1>&2
1254 sed 's/.//' >p337.pftp.ses <<'//GO.SYSIN DD p337.pftp.ses'
1256 - * PROMELA Validation Model
1260 -#include "p337.defines2"
1261 -#include "p337.user"
1262 -#include "App.F.present"
1263 -#include "p337.session"
1264 -#include "p337.fserver"
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]
1276 //GO.SYSIN DD p337.pftp.ses
1277 echo p337.session 1>&2
1278 sed 's/.//' >p337.session <<'//GO.SYSIN DD p337.session'
1280 - * Session Layer Validation Model
1283 -proctype session(bit n)
1285 - byte type, status;
1289 - :: pres_to_ses[n]?type ->
1291 - :: (type == transfer) ->
1293 - :: (type != transfer) /* ignore */
1295 - :: flow_to_ses[n]?type,0 ->
1297 - :: (type == connect) ->
1299 - :: (type != connect) /* ignore */
1303 -DATA_IN: /* 1. prepare local file fsrver */
1304 - ses_to_fsrv[n]!create;
1306 - :: fsrv_to_ses[n]?reject ->
1307 - ses_to_flow[n]!reject,0;
1309 - :: fsrv_to_ses[n]?accept ->
1310 - ses_to_flow[n]!accept,0;
1313 - /* 2. Receive the data, upto eof */
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;
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;
1325 - :: timeout -> /* got disconnected */
1326 - ses_to_fsrv[n]!close;
1329 - /* 3. Close the connection */
1330 - ses_to_flow[n]!close,0;
1333 -DATA_OUT: /* 1. prepare local file fsrver */
1334 - ses_to_fsrv[n]!open;
1336 - :: fsrv_to_ses[n]?reject ->
1337 - ses_to_pres[n]!reject(FATAL);
1339 - :: fsrv_to_ses[n]?accept ->
1342 - /* 2. initialize flow control *** disabled
1343 - ses_to_flow[n]!sync,toggle;
1346 - flow_to_ses[n]?sync_ack,type ->
1348 - :: (type != toggle)
1349 - :: (type == toggle) -> break
1353 - ses_to_fsrv[n]!close;
1354 - ses_to_pres[n]!reject(FATAL);
1357 - toggle = 1 - toggle;
1358 - /* 3. prepare remote file fsrver */
1359 - ses_to_flow[n]!connect,0;
1361 - :: flow_to_ses[n]?reject,0 ->
1362 - ses_to_fsrv[n]!close;
1363 - ses_to_pres[n]!reject(FATAL);
1365 - :: flow_to_ses[n]?connect,0 ->
1366 - ses_to_fsrv[n]!close;
1367 - ses_to_pres[n]!reject(NON_FATAL);
1369 - :: flow_to_ses[n]?accept,0 ->
1372 - ses_to_fsrv[n]!close;
1373 - ses_to_pres[n]!reject(FATAL);
1376 - /* 4. Transmit the data, upto eof */
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;
1384 - :: pres_to_ses[n]?abort -> /* local user aborted */
1385 - ses_to_fsrv[n]!close;
1386 - ses_to_flow[n]!close,0;
1390 - /* 5. Close the connection */
1392 - :: pres_to_ses[n]?abort /* ignore */
1393 - :: flow_to_ses[n]?close,0 ->
1395 - :: (status == COMPLETE) ->
1396 - ses_to_pres[n]!accept,0
1397 - :: (status != COMPLETE) ->
1398 - ses_to_pres[n]!reject(status)
1402 - ses_to_pres[n]!reject(FATAL);
1407 //GO.SYSIN DD p337.session
1409 sed 's/.//' >p337.user <<'//GO.SYSIN DD p337.user'
1411 - * User Layer Validation Model
1414 -proctype userprc(bit n)
1416 - use_to_pres[n]!transfer;
1418 - :: pres_to_use[n]?accept -> goto Done
1419 - :: pres_to_use[n]?reject -> goto Done
1420 - :: use_to_pres[n]!abort -> goto Aborted
1424 - :: pres_to_use[n]?accept -> goto Done
1425 - :: pres_to_use[n]?reject -> goto Done
1430 //GO.SYSIN DD p337.user
1431 echo p342.pftp.ses1 1>&2
1432 sed 's/.//' >p342.pftp.ses1 <<'//GO.SYSIN DD p342.pftp.ses1'
1434 - * PROMELA Validation Model
1438 -#include "p337.defines2"
1439 -#include "p337.user"
1440 -#include "App.F.present"
1441 -#include "p337.session"
1442 -#include "p337.fserver"
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]
1456 - chan foo = [1] of { byte, byte };
1457 - ses_to_flow[0] = foo;
1458 - ses_to_flow[1] = foo
1464 //GO.SYSIN DD p342.pftp.ses1
1465 echo p343.claim 1>&2
1466 sed 's/.//' >p343.claim <<'//GO.SYSIN DD p343.claim'
1468 - skip; /* match first step of init (spin version 2.0) */
1470 - :: !pres_to_ses[0]?[transfer]
1471 - && !flow_to_ses[0]?[connect]
1472 - :: pres_to_ses[0]?[transfer] ->
1474 - :: flow_to_ses[0]?[connect] ->
1479 - :: !ses_to_pres[0]?[accept]
1480 - && !ses_to_pres[0]?[reject]
1484 - :: !ses_to_pres[1]?[accept]
1485 - && !ses_to_pres[1]?[reject]
1488 //GO.SYSIN DD p343.claim
1489 echo p347.pftp.ses5 1>&2
1490 sed 's/.//' >p347.pftp.ses5 <<'//GO.SYSIN DD p347.pftp.ses5'
1492 - * PROMELA Validation Model
1496 -#include "p337.defines2"
1497 -#include "p347.pres.sim"
1498 -#include "p347.session.prog"
1499 -#include "p337.fserver"
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]
1510 //GO.SYSIN DD p347.pftp.ses5
1511 echo p347.pres.sim 1>&2
1512 sed 's/.//' >p347.pres.sim <<'//GO.SYSIN DD p347.pres.sim'
1514 - * PROMELA Validation Model
1515 - * Presentation & User Layer - combined and reduced
1518 -proctype present(bit n)
1521 - pres_to_ses[n]!transfer ->
1523 - :: pres_to_ses[n]!abort;
1525 - :: ses_to_pres[n]?accept,status ->
1527 - :: ses_to_pres[n]?reject,status ->
1529 - :: (status == NON_FATAL) ->
1531 - :: (status != NON_FATAL) ->
1536 //GO.SYSIN DD p347.pres.sim
1537 echo p347.session.prog 1>&2
1538 sed 's/.//' >p347.session.prog <<'//GO.SYSIN DD p347.session.prog'
1540 - * Session Layer Validation Model
1543 -proctype session(bit n)
1545 - byte type, status;
1549 - :: pres_to_ses[n]?type ->
1551 - :: (type == transfer) ->
1552 - goto progressDATA_OUT
1553 - :: (type != transfer) /* ignore */
1555 - :: flow_to_ses[n]?type,0 ->
1557 - :: (type == connect) ->
1558 - goto progressDATA_IN
1559 - :: (type != connect) /* ignore */
1563 -progressDATA_IN: /* 1. prepare local file fsrver */
1564 - ses_to_fsrv[n]!create;
1566 - :: fsrv_to_ses[n]?reject ->
1567 - ses_to_flow[n]!reject,0;
1569 - :: fsrv_to_ses[n]?accept ->
1570 - ses_to_flow[n]!accept,0;
1573 - /* 2. Receive the data, upto eof */
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;
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;
1585 - :: timeout -> /* got disconnected */
1586 - ses_to_fsrv[n]!close;
1589 - /* 3. Close the connection */
1590 - ses_to_flow[n]!close,0;
1593 -progressDATA_OUT: /* 1. prepare local file fsrver */
1594 - ses_to_fsrv[n]!open;
1596 - :: fsrv_to_ses[n]?reject ->
1597 - ses_to_pres[n]!reject(FATAL);
1599 - :: fsrv_to_ses[n]?accept ->
1602 - /* 2. initialize flow control *** disabled
1603 - ses_to_flow[n]!sync,toggle;
1606 - flow_to_ses[n]?sync_ack,type ->
1608 - :: (type != toggle)
1609 - :: (type == toggle) -> break
1613 - ses_to_fsrv[n]!close;
1614 - ses_to_pres[n]!reject(FATAL);
1617 - toggle = 1 - toggle;
1618 - /* 3. prepare remote file fsrver */
1619 - ses_to_flow[n]!connect,0;
1621 - :: flow_to_ses[n]?reject,status ->
1622 - ses_to_fsrv[n]!close;
1623 - ses_to_pres[n]!reject(FATAL);
1625 - :: flow_to_ses[n]?connect,0 ->
1626 - ses_to_fsrv[n]!close;
1627 - ses_to_pres[n]!reject(NON_FATAL);
1629 - :: flow_to_ses[n]?accept,0 ->
1632 - ses_to_fsrv[n]!close;
1633 - ses_to_pres[n]!reject(FATAL);
1636 - /* 4. Transmit the data, upto eof */
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;
1644 - :: pres_to_ses[n]?abort -> /* local user aborted */
1645 - ses_to_fsrv[n]!close;
1646 - ses_to_flow[n]!close,0;
1650 - /* 5. Close the connection */
1652 - :: pres_to_ses[n]?abort /* ignore */
1653 - :: flow_to_ses[n]?close,0 ->
1655 - :: (status == COMPLETE) ->
1656 - ses_to_pres[n]!accept,0
1657 - :: (status != COMPLETE) ->
1658 - ses_to_pres[n]!reject(status)
1662 - ses_to_pres[n]!reject(FATAL);
1667 //GO.SYSIN DD p347.session.prog
1669 sed 's/.//' >p94 <<'//GO.SYSIN DD p94'
1672 -proctype A() { (state == 1) -> state = 3 }
1674 -proctype B() { state = state - 1 }
1677 -init { run A(); run B() }
1680 sed 's/.//' >p95.1 <<'//GO.SYSIN DD p95.1'
1681 -init { printf("hello world\n") }
1684 sed 's/.//' >p95.2 <<'//GO.SYSIN DD p95.2'
1685 -proctype A(byte state; short set)
1686 -{ (state == 1) -> state = set
1689 -init { run A(1, 3) }
1692 sed 's/.//' >p96.1 <<'//GO.SYSIN DD p96.1'
1695 -proctype A() { (state == 1) -> state = state + 1 }
1697 -proctype B() { (state == 1) -> state = state - 1 }
1699 -init { run A(); run B() }
1702 sed 's/.//' >p96.2 <<'//GO.SYSIN DD p96.2'
1713 - (y == false || t == Aturn);
1714 - /* critical section */
1720 - (x == false || t == Bturn);
1721 - /* critical section */
1724 -init { run A(); run B() }
1727 sed 's/.//' >p97.1 <<'//GO.SYSIN DD p97.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() }
1734 sed 's/.//' >p97.2 <<'//GO.SYSIN DD p97.2'
1735 -proctype nr(short pid, a, b)
1738 -atomic { res = (a*a+b)/2*a;
1739 - printf("result %d: %d\n", pid, res)
1742 -init { run nr(1,1,1); run nr(1,2,2); run nr(1,3,2) }
1745 sed 's/.//' >p99 <<'//GO.SYSIN DD p99'
1746 -proctype A(chan q1)
1753 -proctype B(chan qforb)
1757 - printf("x = %d\n", x)
1761 -{ chan qname[2] = [1] of { chan };
1762 - chan qforb = [1] of { int };