0b55f123 |
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\16 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 |