projects / lttv.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
blame | history | raw | HEAD
convert from svn repository: remove tags directory
[lttv.git] / trunk / verif / Spin / Doc / Book91_samples_bundle
1 # To unbundle, sh this file
2 echo README 1>&2
3 sed '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
94 echo App.F.datalink 1>&2
95 sed '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
117 echo App.F.defines 1>&2
118 sed '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
145 echo App.F.flow_cl 1>&2
146 sed '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
262 echo App.F.fserver 1>&2
263 sed '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
294 echo App.F.pftp 1>&2
295 sed '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
319 echo App.F.present 1>&2
320 sed '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
366 echo App.F.session 1>&2
367 sed '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
497 echo App.F.user 1>&2
498 sed '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
520 echo p101 1>&2
521 sed '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
540 echo p102 1>&2
541 sed '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
557 echo p104.1 1>&2
558 sed '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
579 echo p104.2 1>&2
580 sed '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
615 echo p105.1 1>&2
616 sed '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
640 echo p105.2 1>&2
641 sed '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
663 echo p107 1>&2
664 sed '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
692 echo p108 1>&2
693 sed '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
752 echo p116 1>&2
753 sed '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
766 echo p117 1>&2
767 sed '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
796 echo p123 1>&2
797 sed '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
865 echo p248 1>&2
866 sed '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
888 echo p312 1>&2
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 */
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
938 echo p319 1>&2
939 sed '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
985 echo p320 1>&2
986 sed '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
1019 echo p325.test 1>&2
1020 sed '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
1064 echo p327.upper 1>&2
1065 sed '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
1124 echo p329 1>&2
1125 sed '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
1160 echo p330 1>&2
1161 sed '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
1196 echo p337.defines2 1>&2
1197 sed '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
1221 echo p337.fserver 1>&2
1222 sed '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
1253 echo p337.pftp.ses 1>&2
1254 sed '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
1277 echo p337.session 1>&2
1278 sed '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
1408 echo p337.user 1>&2
1409 sed '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
1431 echo p342.pftp.ses1 1>&2
1432 sed '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
1465 echo p343.claim 1>&2
1466 sed '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
1489 echo p347.pftp.ses5 1>&2
1490 sed '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
1511 echo p347.pres.sim 1>&2
1512 sed '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
1537 echo p347.session.prog 1>&2
1538 sed '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
1668 echo p94 1>&2
1669 sed '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
1679 echo p95.1 1>&2
1680 sed 's/.//' >p95.1 <<'//GO.SYSIN DD p95.1'
1681 -init { printf("hello world\n") }
1682 //GO.SYSIN DD p95.1
1683 echo p95.2 1>&2
1684 sed '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
1691 echo p96.1 1>&2
1692 sed '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
1701 echo p96.2 1>&2
1702 sed '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
1726 echo p97.1 1>&2
1727 sed '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
1733 echo p97.2 1>&2
1734 sed '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
1744 echo p99 1>&2
1745 sed '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.065864 seconds and 4 git commands to generate.