| 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 |