| 1 | # To unbundle, sh this file |
| 2 | echo ex.readme 1>&2 |
| 3 | sed 's/.//' >ex.readme <<'//GO.SYSIN DD ex.readme' |
| 4 | -The 12 files in this bundle are the PROMELA |
| 5 | -files of all exercises and examples discussed |
| 6 | -in the document Doc/Exercises.ps from the |
| 7 | -SPIN distribution. |
| 8 | //GO.SYSIN DD ex.readme |
| 9 | echo ex.1a 1>&2 |
| 10 | sed 's/.//' >ex.1a <<'//GO.SYSIN DD ex.1a' |
| 11 | -init { |
| 12 | - byte i = 0; |
| 13 | - do |
| 14 | - :: i = i+1 |
| 15 | - od |
| 16 | -} |
| 17 | //GO.SYSIN DD ex.1a |
| 18 | echo ex.1b 1>&2 |
| 19 | sed 's/.//' >ex.1b <<'//GO.SYSIN DD ex.1b' |
| 20 | -init { |
| 21 | - chan dummy = [20] of { byte }; |
| 22 | - do |
| 23 | - :: dummy!85 |
| 24 | - :: dummy!170 |
| 25 | - od |
| 26 | -} |
| 27 | //GO.SYSIN DD ex.1b |
| 28 | echo ex.1c 1>&2 |
| 29 | sed 's/.//' >ex.1c <<'//GO.SYSIN DD ex.1c' |
| 30 | -#define N 26 |
| 31 | - |
| 32 | -int a; |
| 33 | -byte b; |
| 34 | - |
| 35 | -init { |
| 36 | - do |
| 37 | - :: atomic { (b < N) -> |
| 38 | - if |
| 39 | - :: a = a + (1<<b) |
| 40 | - :: skip |
| 41 | - fi; |
| 42 | - b=b+1 } |
| 43 | - od |
| 44 | -} |
| 45 | //GO.SYSIN DD ex.1c |
| 46 | echo ex.2 1>&2 |
| 47 | sed 's/.//' >ex.2 <<'//GO.SYSIN DD ex.2' |
| 48 | -#define MAX 8 |
| 49 | -proctype A(chan in, out) |
| 50 | -{ byte mt; /* message data */ |
| 51 | - bit vr; |
| 52 | -S1: mt = (mt+1)%MAX; |
| 53 | - out!mt,1; |
| 54 | - goto S2; |
| 55 | -S2: in?vr; |
| 56 | - if |
| 57 | - :: (vr == 1) -> goto S1 |
| 58 | - :: (vr == 0) -> goto S3 |
| 59 | - :: printf("AERROR1\n") -> goto S5 |
| 60 | - fi; |
| 61 | -S3: out!mt,1; |
| 62 | - goto S4; |
| 63 | -S4: in?vr; |
| 64 | - if |
| 65 | - :: goto S1 |
| 66 | - :: printf("AERROR2\n"); goto S5 |
| 67 | - fi; |
| 68 | -S5: out!mt,0; |
| 69 | - goto S4 |
| 70 | -} |
| 71 | -proctype B(chan in, out) |
| 72 | -{ byte mr, lmr; |
| 73 | - bit ar; |
| 74 | - goto S2; /* initial state */ |
| 75 | -S1: assert(mr == (lmr+1)%MAX); |
| 76 | - lmr = mr; |
| 77 | - out!1; |
| 78 | - goto S2; |
| 79 | -S2: in?mr,ar; |
| 80 | - if |
| 81 | - :: (ar == 1) -> goto S1 |
| 82 | - :: (ar == 0) -> goto S3 |
| 83 | - :: printf("ERROR1\n"); goto S5 |
| 84 | - fi; |
| 85 | -S3: out!1; |
| 86 | - goto S2; |
| 87 | -S4: in?mr,ar; |
| 88 | - if |
| 89 | - :: goto S1 |
| 90 | - :: printf("ERROR2\n"); goto S5 |
| 91 | - fi; |
| 92 | -S5: out!0; |
| 93 | - goto S4 |
| 94 | -} |
| 95 | -init { |
| 96 | - chan a2b = [2] of { bit }; |
| 97 | - chan b2a = [2] of { byte, bit }; |
| 98 | - atomic { |
| 99 | - run A(a2b, b2a); |
| 100 | - run B(b2a, a2b) |
| 101 | - } |
| 102 | -} |
| 103 | //GO.SYSIN DD ex.2 |
| 104 | echo ex.3 1>&2 |
| 105 | sed 's/.//' >ex.3 <<'//GO.SYSIN DD ex.3' |
| 106 | -mtype = { a, b, c, d, e, i, l, m, n, q, r, u, v }; |
| 107 | - |
| 108 | -chan dce = [0] of { mtype }; |
| 109 | -chan dte = [0] of { mtype }; |
| 110 | - |
| 111 | -active proctype dte_proc() |
| 112 | -{ |
| 113 | -state01: |
| 114 | - do |
| 115 | - :: dce!b -> /* state21 */ dce!a |
| 116 | - :: dce!i -> /* state14 */ |
| 117 | - if |
| 118 | - :: dte?m -> goto state19 |
| 119 | - :: dce!a |
| 120 | - fi |
| 121 | - :: dte?m -> goto state18 |
| 122 | - :: dte?u -> goto state08 |
| 123 | - :: dce!d -> break |
| 124 | - od; |
| 125 | - |
| 126 | - /* state02: */ |
| 127 | - if |
| 128 | - :: dte?v |
| 129 | - :: dte?u -> goto state15 |
| 130 | - :: dte?m -> goto state19 |
| 131 | - fi; |
| 132 | -state03: |
| 133 | - dce!e; |
| 134 | - /* state04: */ |
| 135 | - if |
| 136 | - :: dte?m -> goto state19 |
| 137 | - :: dce!c |
| 138 | - fi; |
| 139 | - /* state05: */ |
| 140 | - if |
| 141 | - :: dte?m -> goto state19 |
| 142 | - :: dte?r |
| 143 | - fi; |
| 144 | - /* state6A: */ |
| 145 | - if |
| 146 | - :: dte?m -> goto state19 |
| 147 | - :: dte?q |
| 148 | - fi; |
| 149 | -state07: |
| 150 | - if |
| 151 | - :: dte?m -> goto state19 |
| 152 | - :: dte?r |
| 153 | - fi; |
| 154 | - /* state6B: */ |
| 155 | - if /* non-deterministic select */ |
| 156 | - :: dte?q -> goto state07 |
| 157 | - :: dte?q |
| 158 | - :: dte?m -> goto state19 |
| 159 | - fi; |
| 160 | - /* state10: */ |
| 161 | - if |
| 162 | - :: dte?m -> goto state19 |
| 163 | - :: dte?r |
| 164 | - fi; |
| 165 | -state6C: |
| 166 | - if |
| 167 | - :: dte?m -> goto state19 |
| 168 | - :: dte?l |
| 169 | - fi; |
| 170 | - /* state11: */ |
| 171 | - if |
| 172 | - :: dte?m -> goto state19 |
| 173 | - :: dte?n |
| 174 | - fi; |
| 175 | - /* state12: */ |
| 176 | - if |
| 177 | - :: dte?m -> goto state19 |
| 178 | - :: dce!b -> goto state16 |
| 179 | - fi; |
| 180 | - |
| 181 | -state15: |
| 182 | - if |
| 183 | - :: dte?v -> goto state03 |
| 184 | - :: dte?m -> goto state19 |
| 185 | - fi; |
| 186 | -state08: |
| 187 | - if |
| 188 | - :: dce!c |
| 189 | - :: dce!d -> goto state15 |
| 190 | - :: dte?m -> goto state19 |
| 191 | - fi; |
| 192 | - /* state09: */ |
| 193 | - if |
| 194 | - :: dte?m -> goto state19 |
| 195 | - :: dte?q |
| 196 | - fi; |
| 197 | - /* state10B: */ |
| 198 | - if |
| 199 | - :: dte?r -> goto state6C |
| 200 | - :: dte?m -> goto state19 |
| 201 | - fi; |
| 202 | -state18: |
| 203 | - if |
| 204 | - :: dte?l -> goto state01 |
| 205 | - :: dte?m -> goto state19 |
| 206 | - fi; |
| 207 | -state16: |
| 208 | - dte?m; |
| 209 | - /* state17: */ |
| 210 | - dte?l; |
| 211 | - /* state21: */ |
| 212 | - dce!a; goto state01; |
| 213 | -state19: |
| 214 | - dce!b; |
| 215 | - /* state20: */ |
| 216 | - dte?l; |
| 217 | - /* state21: */ |
| 218 | - dce!a; goto state01 |
| 219 | -} |
| 220 | - |
| 221 | -active proctype dce_proc() |
| 222 | -{ |
| 223 | -state01: |
| 224 | - do |
| 225 | - :: dce?b -> /* state21 */ dce?a |
| 226 | - :: dce?i -> /* state14 */ |
| 227 | - if |
| 228 | - :: dce?b -> goto state16 |
| 229 | - :: dce?a |
| 230 | - fi |
| 231 | - :: dte!m -> goto state18 |
| 232 | - :: dte!u -> goto state08 |
| 233 | - :: dce?d -> break |
| 234 | - od; |
| 235 | - |
| 236 | - /* state02: */ |
| 237 | - if |
| 238 | - :: dte!v |
| 239 | - :: dte!u -> goto state15 |
| 240 | - :: dce?b -> goto state16 |
| 241 | - fi; |
| 242 | -state03: |
| 243 | - dce?e; |
| 244 | - /* state04: */ |
| 245 | - if |
| 246 | - :: dce?b -> goto state16 |
| 247 | - :: dce?c |
| 248 | - fi; |
| 249 | - /* state05: */ |
| 250 | - if |
| 251 | - :: dce?b -> goto state16 |
| 252 | - :: dte!r |
| 253 | - fi; |
| 254 | - /* state6A: */ |
| 255 | - if |
| 256 | - :: dce?b -> goto state16 |
| 257 | - :: dte!q |
| 258 | - fi; |
| 259 | -state07: |
| 260 | - if |
| 261 | - :: dce?b -> goto state16 |
| 262 | - :: dte!r |
| 263 | - fi; |
| 264 | - /* state6B: */ |
| 265 | - if /* non-deterministic select */ |
| 266 | - :: dte!q -> goto state07 |
| 267 | - :: dte!q |
| 268 | - :: dce?b -> goto state16 |
| 269 | - fi; |
| 270 | - /* state10: */ |
| 271 | - if |
| 272 | - :: dce?b -> goto state16 |
| 273 | - :: dte!r |
| 274 | - fi; |
| 275 | -state6C: |
| 276 | - if |
| 277 | - :: dce?b -> goto state16 |
| 278 | - :: dte!l |
| 279 | - fi; |
| 280 | - /* state11: */ |
| 281 | - if |
| 282 | - :: dce?b -> goto state16 |
| 283 | - :: dte!n |
| 284 | - fi; |
| 285 | - /* state12: */ |
| 286 | - if |
| 287 | - :: dce?b -> goto state16 |
| 288 | - :: dte!m -> goto state19 |
| 289 | - fi; |
| 290 | - |
| 291 | -state15: |
| 292 | - if |
| 293 | - :: dte!v -> goto state03 |
| 294 | - :: dce?b -> goto state16 |
| 295 | - fi; |
| 296 | -state08: |
| 297 | - if |
| 298 | - :: dce?c |
| 299 | - :: dce?d -> goto state15 |
| 300 | - :: dce?b -> goto state16 |
| 301 | - fi; |
| 302 | - /* state09: */ |
| 303 | - if |
| 304 | - :: dce?b -> goto state16 |
| 305 | - :: dte!q |
| 306 | - fi; |
| 307 | - /* state10B: */ |
| 308 | - if |
| 309 | - :: dte!r -> goto state6C |
| 310 | - :: dce?b -> goto state16 |
| 311 | - fi; |
| 312 | -state18: |
| 313 | - if |
| 314 | - :: dte!l -> goto state01 |
| 315 | - :: dce?b -> goto state16 |
| 316 | - fi; |
| 317 | -state16: |
| 318 | - dte!m; |
| 319 | - /* state17: */ |
| 320 | - dte!l; |
| 321 | - /* state21: */ |
| 322 | - dce?a; goto state01; |
| 323 | -state19: |
| 324 | - dce?b; |
| 325 | - /* state20: */ |
| 326 | - dte!l; |
| 327 | - /* state21: */ |
| 328 | - dce?a; goto state01 |
| 329 | -} |
| 330 | //GO.SYSIN DD ex.3 |
| 331 | echo ex.4b 1>&2 |
| 332 | sed 's/.//' >ex.4b <<'//GO.SYSIN DD ex.4b' |
| 333 | -#define true 1 |
| 334 | -#define false 0 |
| 335 | - |
| 336 | -bool flag[2]; |
| 337 | -bool turn; |
| 338 | - |
| 339 | -active [2] proctype user() |
| 340 | -{ flag[_pid] = true; |
| 341 | - turn = _pid; |
| 342 | - (flag[1-_pid] == false || turn == 1-_pid); |
| 343 | -crit: skip; /* critical section */ |
| 344 | - flag[_pid] = false |
| 345 | -} |
| 346 | //GO.SYSIN DD ex.4b |
| 347 | echo ex.4c 1>&2 |
| 348 | sed 's/.//' >ex.4c <<'//GO.SYSIN DD ex.4c' |
| 349 | -byte in; |
| 350 | -byte x, y, z; |
| 351 | -active [2] proctype user() /* file ex.4c */ |
| 352 | -{ byte me = _pid+1; /* me is 1 or 2 */ |
| 353 | -L1: x = me; |
| 354 | -L2: if |
| 355 | - :: (y != 0 && y != me) -> goto L1 /* try again */ |
| 356 | - :: (y == 0 || y == me) |
| 357 | - fi; |
| 358 | -L3: z = me; |
| 359 | -L4: if |
| 360 | - :: (x != me) -> goto L1 /* try again */ |
| 361 | - :: (x == me) |
| 362 | - fi; |
| 363 | -L5: y = me; |
| 364 | -L6: if |
| 365 | - :: (z != me) -> goto L1 /* try again */ |
| 366 | - :: (z == me) |
| 367 | - fi; |
| 368 | -L7: /* success */ |
| 369 | - in = in+1; |
| 370 | - assert(in == 1); |
| 371 | - in = in - 1; |
| 372 | - goto L1 |
| 373 | -} |
| 374 | //GO.SYSIN DD ex.4c |
| 375 | echo ex.5a 1>&2 |
| 376 | sed 's/.//' >ex.5a <<'//GO.SYSIN DD ex.5a' |
| 377 | -#define Place byte /* assume < 256 tokens per place */ |
| 378 | - |
| 379 | -Place p1, p2, p3; |
| 380 | -Place p4, p5, p6; |
| 381 | -#define inp1(x) (x>0) -> x=x-1 |
| 382 | -#define inp2(x,y) (x>0&&y>0) -> x = x-1; y=y-1 |
| 383 | -#define out1(x) x=x+1 |
| 384 | -#define out2(x,y) x=x+1; y=y+1 |
| 385 | -init |
| 386 | -{ p1 = 1; p4 = 1; /* initial marking */ |
| 387 | - do |
| 388 | -/*t1*/ :: atomic { inp1(p1) -> out1(p2) } |
| 389 | -/*t2*/ :: atomic { inp2(p2,p4) -> out1(p3) } |
| 390 | -/*t3*/ :: atomic { inp1(p3) -> out2(p1,p4) } |
| 391 | -/*t4*/ :: atomic { inp1(p4) -> out1(p5) } |
| 392 | -/*t5*/ :: atomic { inp2(p1,p5) -> out1(p6) } |
| 393 | -/*t6*/ :: atomic { inp1(p6) -> out2(p4,p1) } |
| 394 | - od |
| 395 | -} |
| 396 | //GO.SYSIN DD ex.5a |
| 397 | echo ex.5b 1>&2 |
| 398 | sed 's/.//' >ex.5b <<'//GO.SYSIN DD ex.5b' |
| 399 | -#define Place byte /* assume < 256 tokens per place */ |
| 400 | - |
| 401 | -Place P1, P2, P4, P5, RC, CC, RD, CD; |
| 402 | -Place p1, p2, p4, p5, rc, cc, rd, cd; |
| 403 | - |
| 404 | -#define inp1(x) (x>0) -> x=x-1 |
| 405 | -#define inp2(x,y) (x>0&&y>0) -> x = x-1; y=y-1 |
| 406 | -#define out1(x) x=x+1 |
| 407 | -#define out2(x,y) x=x+1; y=y+1 |
| 408 | - |
| 409 | -init /* file ex.5b */ |
| 410 | -{ P1 = 1; p1 = 1; /* initial marking */ |
| 411 | - do |
| 412 | - :: atomic { inp1(P1) -> out2(rc,P2) } /* DC */ |
| 413 | - :: atomic { inp2(P2,CC) -> out1(P4) } /* CA */ |
| 414 | - :: atomic { inp1(P4) -> out2(P5,rd) } /* DD */ |
| 415 | - :: atomic { inp2(P5,CD) -> out1(P1) } /* FD */ |
| 416 | - :: atomic { inp2(P1,RC) -> out2(P4,cc) } /* AC */ |
| 417 | - :: atomic { inp2(P4,RD) -> out2(P1,cd) } /* AD */ |
| 418 | - :: atomic { inp2(P5,RD) -> out1(P1) } /* DA */ |
| 419 | - |
| 420 | - :: atomic { inp1(p1) -> out2(RC,p2) } /* dc */ |
| 421 | - :: atomic { inp2(p2,cc) -> out1(p4) } /* ca */ |
| 422 | - :: atomic { inp1(p4) -> out2(p5,RD) } /* dd */ |
| 423 | - :: atomic { inp2(p5,cd) -> out1(p1) } /* fd */ |
| 424 | - :: atomic { inp2(p1,rc) -> out2(p4,CC) } /* ac */ |
| 425 | - :: atomic { inp2(p4,rd) -> out2(p1,CD) } /* ad */ |
| 426 | - :: atomic { inp2(p5,rd) -> out1(p1) } /* da */ |
| 427 | - od |
| 428 | -} |
| 429 | //GO.SYSIN DD ex.5b |
| 430 | echo ex.6 1>&2 |
| 431 | sed 's/.//' >ex.6 <<'//GO.SYSIN DD ex.6' |
| 432 | -#if 0 |
| 433 | - Cambridge Ring Protocol [Needham'82] |
| 434 | - basic protocol - no LTL properties |
| 435 | -#endif |
| 436 | - |
| 437 | -#define LOSS 1 |
| 438 | -#define RELAXED 1 |
| 439 | - |
| 440 | -#if RELAXED==1 |
| 441 | -#define stimeout empty(sender) |
| 442 | -#define rtimeout empty(recv) |
| 443 | -#else |
| 444 | -#define stimeout timeout |
| 445 | -#define rtimeout timeout |
| 446 | -#endif |
| 447 | - |
| 448 | -#define QSZ 6 /* length of message queues */ |
| 449 | - |
| 450 | - mtype = { |
| 451 | - RDY, NOTRDY, DATA, NODATA, RESET |
| 452 | - }; |
| 453 | - chan sender = [QSZ] of { mtype, byte }; |
| 454 | - chan recv = [QSZ] of { mtype, byte }; |
| 455 | - |
| 456 | -active proctype Sender() |
| 457 | -{ short n = -1; byte t,m; |
| 458 | - |
| 459 | - xr sender; |
| 460 | - xs recv; |
| 461 | - |
| 462 | -I: /* Idle State */ |
| 463 | - do |
| 464 | -#if LOSS==1 |
| 465 | - :: sender?_,_ -> progress2: skip |
| 466 | -#endif |
| 467 | - :: sender?RESET,0 -> |
| 468 | -ackreset: recv!RESET,0; /* stay in idle */ |
| 469 | - n = -1; |
| 470 | - goto I |
| 471 | - |
| 472 | - /* E-rep: protocol error */ |
| 473 | - |
| 474 | - :: sender?RDY,m -> /* E-exp */ |
| 475 | - assert(m == (n+1)%4); |
| 476 | -advance: n = (n+1)%4; |
| 477 | - if |
| 478 | -/* buffer */ :: atomic { |
| 479 | - printf("MSC: NEW\n"); |
| 480 | - recv!DATA,n; |
| 481 | - goto E |
| 482 | - } |
| 483 | -/* no buffer */ :: recv!NODATA,n; |
| 484 | - goto N |
| 485 | - fi |
| 486 | - |
| 487 | - :: sender?NOTRDY,m -> /* N-exp */ |
| 488 | -expected: assert(m == (n+1)%4); |
| 489 | - goto I |
| 490 | - |
| 491 | - /* Timeout */ |
| 492 | - /* ignored (p.154, in [Needham'82]) */ |
| 493 | - |
| 494 | - :: goto reset |
| 495 | - |
| 496 | - od; |
| 497 | - |
| 498 | -E: /* Essential element sent, ack expected */ |
| 499 | - do |
| 500 | -#if LOSS==1 |
| 501 | - :: sender?_,_ -> progress0: skip |
| 502 | -#endif |
| 503 | - :: sender?RESET,0 -> |
| 504 | - goto ackreset |
| 505 | - |
| 506 | - :: sender?RDY,m -> |
| 507 | - if |
| 508 | - :: (m == n) -> /* E-rep */ |
| 509 | - goto retrans |
| 510 | - :: (m == (n+1)%4) -> /* E-exp */ |
| 511 | - goto advance |
| 512 | - fi |
| 513 | - |
| 514 | - :: sender?NOTRDY,m -> /* N-exp */ |
| 515 | - goto expected |
| 516 | - |
| 517 | - /* Timeout */ |
| 518 | - :: stimeout -> |
| 519 | - printf("MSC: STO\n"); |
| 520 | -retrans: recv!DATA,n /* retransmit */ |
| 521 | - |
| 522 | - :: goto reset |
| 523 | - |
| 524 | - od; |
| 525 | - |
| 526 | - |
| 527 | -N: /* Non-essential element sent */ |
| 528 | - do |
| 529 | -#if LOSS==1 |
| 530 | - :: sender?_,_ -> progress1: skip |
| 531 | -#endif |
| 532 | - :: sender?RESET,0 -> |
| 533 | - goto ackreset |
| 534 | - |
| 535 | - :: sender?RDY,m -> /* E-rep */ |
| 536 | - assert(m == n) /* E-exp: protocol error */ |
| 537 | - -> recv!NODATA,n /* retransmit and stay in N */ |
| 538 | - |
| 539 | - :: recv!DATA,n; /* buffer ready event */ |
| 540 | - goto E |
| 541 | - |
| 542 | - :: goto reset |
| 543 | - |
| 544 | - /* Timeout */ |
| 545 | - /* ignored (p.154, in [Needham'82]) */ |
| 546 | - od; |
| 547 | - |
| 548 | -reset: recv!RESET,0; |
| 549 | - do |
| 550 | -#if LOSS==1 |
| 551 | - :: sender?_,_ -> progress3: skip |
| 552 | -#endif |
| 553 | - :: sender?t,m -> |
| 554 | - if |
| 555 | - :: t == RESET -> n = -1; goto I |
| 556 | - :: else /* ignored, p. 152 */ |
| 557 | - fi |
| 558 | - :: timeout -> /* a real timeout */ |
| 559 | - goto reset |
| 560 | - od |
| 561 | -} |
| 562 | - |
| 563 | -active proctype Receiver() |
| 564 | -{ byte t, n, m, Nexp; |
| 565 | - |
| 566 | - xr recv; |
| 567 | - xs sender; |
| 568 | - |
| 569 | -I: /* Idle State */ |
| 570 | - do |
| 571 | -#if LOSS==1 |
| 572 | - :: recv?_,_ -> progress2: skip |
| 573 | -#endif |
| 574 | - :: recv?RESET,0 -> |
| 575 | -ackreset: sender!RESET,0; /* stay in idle */ |
| 576 | - n = 0; Nexp = 0; |
| 577 | - goto I |
| 578 | - |
| 579 | - :: atomic { recv?DATA(m) -> /* E-exp */ |
| 580 | - assert(m == n); |
| 581 | -advance: printf("MSC: EXP\n"); |
| 582 | - n = (n+1)%4; |
| 583 | - assert(m == Nexp); |
| 584 | - Nexp = (m+1)%4; |
| 585 | - if |
| 586 | - :: sender!RDY,n; goto E |
| 587 | - :: sender!NOTRDY,n; goto N |
| 588 | - fi |
| 589 | - } |
| 590 | - |
| 591 | - :: recv?NODATA(m) -> /* N-exp */ |
| 592 | - assert(m == n) |
| 593 | - |
| 594 | - /* Timeout: ignored */ |
| 595 | - |
| 596 | - /* only receiver can initiate transfer; p. 156 */ |
| 597 | - :: empty(recv) -> sender!RDY,n; goto E |
| 598 | - |
| 599 | - :: goto reset |
| 600 | - od; |
| 601 | - |
| 602 | -E: |
| 603 | - do |
| 604 | -#if LOSS==1 |
| 605 | - :: recv?_,_ -> progress1: skip |
| 606 | -#endif |
| 607 | - :: recv?RESET,0 -> |
| 608 | - goto ackreset |
| 609 | - |
| 610 | - :: atomic { recv?DATA(m) -> |
| 611 | - if |
| 612 | - :: ((m+1)%4 == n) -> /* E-rep */ |
| 613 | - printf("MSC: REP\n"); |
| 614 | - goto retrans |
| 615 | - :: (m == n) -> /* E-exp */ |
| 616 | - goto advance |
| 617 | - fi |
| 618 | - } |
| 619 | - |
| 620 | - :: recv?NODATA(m) -> /* N-exp */ |
| 621 | - assert(m == n); |
| 622 | - goto I |
| 623 | - |
| 624 | - :: rtimeout -> |
| 625 | - printf("MSC: RTO\n"); |
| 626 | -retrans: sender!RDY,n; |
| 627 | - goto E |
| 628 | - |
| 629 | - :: goto reset |
| 630 | - |
| 631 | - od; |
| 632 | - |
| 633 | -N: |
| 634 | - do |
| 635 | -#if LOSS==1 |
| 636 | - :: recv?_,_ -> progress0: skip |
| 637 | -#endif |
| 638 | - :: recv?RESET,0 -> |
| 639 | - goto ackreset |
| 640 | - |
| 641 | - :: recv?DATA(m) -> /* E-rep */ |
| 642 | - assert((m+1)%4 == n); /* E-exp and N-exp: protocol error */ |
| 643 | - printf("MSC: REP\n"); |
| 644 | - sender!NOTRDY,n /* retransmit and stay in N */ |
| 645 | - |
| 646 | - :: sender!RDY,n -> /* buffer ready event */ |
| 647 | - goto E |
| 648 | - |
| 649 | - /* Timeout: ignored */ |
| 650 | - |
| 651 | - :: goto reset |
| 652 | - |
| 653 | - od; |
| 654 | - |
| 655 | -progress: |
| 656 | -reset: sender!RESET,0; |
| 657 | - do |
| 658 | -#if LOSS==1 |
| 659 | - :: recv?_,_ -> progress3: skip |
| 660 | -#endif |
| 661 | - :: recv?t,m -> |
| 662 | - if |
| 663 | - :: t == RESET -> n = 0; Nexp = 0; goto I |
| 664 | - :: else /* ignored, p. 152 */ |
| 665 | - fi |
| 666 | - :: timeout -> /* a real timeout */ |
| 667 | - goto reset |
| 668 | - od |
| 669 | -} |
| 670 | //GO.SYSIN DD ex.6 |
| 671 | echo ex.7 1>&2 |
| 672 | sed 's/.//' >ex.7 <<'//GO.SYSIN DD ex.7' |
| 673 | -mtype = { Wakeme, Running }; |
| 674 | - |
| 675 | -bit lk, sleep_q; |
| 676 | -bit r_lock, r_want; |
| 677 | -mtype State = Running; |
| 678 | - |
| 679 | -active proctype client() |
| 680 | -{ |
| 681 | -sleep: /* sleep routine */ |
| 682 | - atomic { (lk == 0) -> lk = 1 }; /* spinlock(&lk) */ |
| 683 | - do /* while r->lock */ |
| 684 | - :: (r_lock == 1) -> /* r->lock == 1 */ |
| 685 | - r_want = 1; |
| 686 | - State = Wakeme; |
| 687 | - lk = 0; /* freelock(&lk) */ |
| 688 | - (State == Running); /* wait for wakeup */ |
| 689 | - :: else -> /* r->lock == 0 */ |
| 690 | - break |
| 691 | - od; |
| 692 | -progress: |
| 693 | - assert(r_lock == 0); /* should still be true */ |
| 694 | - r_lock = 1; /* consumed resource */ |
| 695 | - lk = 0; /* freelock(&lk) */ |
| 696 | - goto sleep |
| 697 | -} |
| 698 | - |
| 699 | -active proctype server() /* interrupt routine */ |
| 700 | -{ |
| 701 | -wakeup: /* wakeup routine */ |
| 702 | - r_lock = 0; /* r->lock = 0 */ |
| 703 | - (lk == 0); /* waitlock(&lk) */ |
| 704 | - if |
| 705 | - :: r_want -> /* someone is sleeping */ |
| 706 | - atomic { /* spinlock on sleep queue */ |
| 707 | - (sleep_q == 0) -> sleep_q = 1 |
| 708 | - }; |
| 709 | - r_want = 0; |
| 710 | -#ifdef PROPOSED_FIX |
| 711 | - (lk == 0); /* waitlock(&lk) */ |
| 712 | -#endif |
| 713 | - if |
| 714 | - :: (State == Wakeme) -> |
| 715 | - State = Running; |
| 716 | - :: else -> |
| 717 | - fi; |
| 718 | - sleep_q = 0 |
| 719 | - :: else -> |
| 720 | - fi; |
| 721 | - goto wakeup |
| 722 | -} |
| 723 | //GO.SYSIN DD ex.7 |
| 724 | echo ex.8 1>&2 |
| 725 | sed 's/.//' >ex.8 <<'//GO.SYSIN DD ex.8' |
| 726 | -/* Dolev, Klawe & Rodeh for leader election in unidirectional ring |
| 727 | - * `An O(n log n) unidirectional distributed algorithm for extrema |
| 728 | - * finding in a circle,' J. of Algs, Vol 3. (1982), pp. 245-260 |
| 729 | - */ |
| 730 | - |
| 731 | -#define elected (nr_leaders > 0) |
| 732 | -#define noLeader (nr_leaders == 0) |
| 733 | -#define oneLeader (nr_leaders == 1) |
| 734 | - |
| 735 | -/* properties: |
| 736 | - * ![] noLeader |
| 737 | - * <> elected |
| 738 | - * <>[]oneLeader |
| 739 | - * [] (noLeader U oneLeader) |
| 740 | - */ |
| 741 | - |
| 742 | -#define N 7 /* nr of processes (use 5 for demos) */ |
| 743 | -#define I 3 /* node given the smallest number */ |
| 744 | -#define L 14 /* size of buffer (>= 2*N) */ |
| 745 | - |
| 746 | -mtype = { one, two, winner }; |
| 747 | -chan q[N] = [L] of { mtype, byte}; |
| 748 | - |
| 749 | -byte nr_leaders = 0; |
| 750 | - |
| 751 | -proctype node (chan in, out; byte mynumber) |
| 752 | -{ bit Active = 1, know_winner = 0; |
| 753 | - byte nr, maximum = mynumber, neighbourR; |
| 754 | - |
| 755 | - xr in; |
| 756 | - xs out; |
| 757 | - |
| 758 | - printf("MSC: %d\n", mynumber); |
| 759 | - out!one(mynumber); |
| 760 | -end: do |
| 761 | - :: in?one(nr) -> |
| 762 | - if |
| 763 | - :: Active -> |
| 764 | - if |
| 765 | - :: nr != maximum -> |
| 766 | - out!two(nr); |
| 767 | - neighbourR = nr |
| 768 | - :: else -> |
| 769 | - /* Raynal p.39: max is greatest number */ |
| 770 | - assert(nr == N); |
| 771 | - know_winner = 1; |
| 772 | - out!winner,nr; |
| 773 | - fi |
| 774 | - :: else -> |
| 775 | - out!one(nr) |
| 776 | - fi |
| 777 | - |
| 778 | - :: in?two(nr) -> |
| 779 | - if |
| 780 | - :: Active -> |
| 781 | - if |
| 782 | - :: neighbourR > nr && neighbourR > maximum -> |
| 783 | - maximum = neighbourR; |
| 784 | - out!one(neighbourR) |
| 785 | - :: else -> |
| 786 | - Active = 0 |
| 787 | - fi |
| 788 | - :: else -> |
| 789 | - out!two(nr) |
| 790 | - fi |
| 791 | - :: in?winner,nr -> |
| 792 | - if |
| 793 | - :: nr != mynumber -> |
| 794 | - printf("MSC: LOST\n"); |
| 795 | - :: else -> |
| 796 | - printf("MSC: LEADER\n"); |
| 797 | - nr_leaders++; |
| 798 | - assert(nr_leaders == 1) |
| 799 | - fi; |
| 800 | - if |
| 801 | - :: know_winner |
| 802 | - :: else -> out!winner,nr |
| 803 | - fi; |
| 804 | - break |
| 805 | - od |
| 806 | -} |
| 807 | - |
| 808 | -init { |
| 809 | - byte proc; |
| 810 | - atomic { |
| 811 | - proc = 1; |
| 812 | - do |
| 813 | - :: proc <= N -> |
| 814 | - run node (q[proc-1], q[proc%N], (N+I-proc)%N+1); |
| 815 | - proc++ |
| 816 | - :: proc > N -> |
| 817 | - break |
| 818 | - od |
| 819 | - } |
| 820 | -} |
| 821 | - |
| 822 | -#if 0 |
| 823 | -/* !(<>[]oneLeader) */ |
| 824 | - |
| 825 | -never { |
| 826 | -T0: |
| 827 | - if |
| 828 | - :: skip -> goto T0 |
| 829 | - :: !oneLeader -> goto accept |
| 830 | - fi; |
| 831 | -accept: |
| 832 | - if |
| 833 | - :: skip -> goto T0 |
| 834 | - fi |
| 835 | -} |
| 836 | -#endif |
| 837 | //GO.SYSIN DD ex.8 |
| 838 | echo ex.9 1>&2 |
| 839 | sed 's/.//' >ex.9 <<'//GO.SYSIN DD ex.9' |
| 840 | -#define MaxSeq 3 |
| 841 | -#define MaxSeq_plus_1 4 |
| 842 | -#define inc(x) x = (x + 1) % (MaxSeq_plus_1) |
| 843 | - |
| 844 | -chan q[2] = [MaxSeq] of { byte, byte }; |
| 845 | - |
| 846 | -active [2] proctype p5() |
| 847 | -{ byte NextFrame, AckExp, FrameExp, |
| 848 | - r, s, nbuf, i; |
| 849 | - chan in, out; |
| 850 | - |
| 851 | - in = q[_pid]; |
| 852 | - out = q[1-_pid]; |
| 853 | - |
| 854 | - xr in; |
| 855 | - xs out; |
| 856 | - |
| 857 | - do |
| 858 | - :: nbuf < MaxSeq -> |
| 859 | - nbuf++; |
| 860 | - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq_plus_1); |
| 861 | - inc(NextFrame) |
| 862 | - :: in?r,s -> |
| 863 | - if |
| 864 | - :: r == FrameExp -> |
| 865 | - inc(FrameExp) |
| 866 | - :: else |
| 867 | - fi; |
| 868 | - do |
| 869 | - :: ((AckExp <= s) && (s < NextFrame)) |
| 870 | - || ((AckExp <= s) && (NextFrame < AckExp)) |
| 871 | - || ((s < NextFrame) && (NextFrame < AckExp)) -> |
| 872 | - nbuf--; |
| 873 | - inc(AckExp) |
| 874 | - :: else -> |
| 875 | - break |
| 876 | - od |
| 877 | - :: timeout -> |
| 878 | - NextFrame = AckExp; |
| 879 | - i = 1; |
| 880 | - do |
| 881 | - :: i <= nbuf -> |
| 882 | - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq_plus_1); |
| 883 | - inc(NextFrame); |
| 884 | - i++ |
| 885 | - :: else -> |
| 886 | - break |
| 887 | - od |
| 888 | - od |
| 889 | -} |
| 890 | //GO.SYSIN DD ex.9 |
| 891 | echo ex.9b 1>&2 |
| 892 | sed 's/.//' >ex.9b <<'//GO.SYSIN DD ex.9b' |
| 893 | -#define MaxSeq 3 |
| 894 | -#define MaxSeq_plus_1 4 |
| 895 | -#define inc(x) x = (x + 1) % (MaxSeq + 1) |
| 896 | - |
| 897 | -chan q[2] = [MaxSeq] of { byte, byte }; |
| 898 | - |
| 899 | -active [2] proctype p5() |
| 900 | -{ byte NextFrame, AckExp, FrameExp, |
| 901 | - r, s, nbuf, i; |
| 902 | - chan in, out; |
| 903 | - |
| 904 | - d_step { |
| 905 | - in = q[_pid]; |
| 906 | - out = q[1-_pid] |
| 907 | - }; |
| 908 | - xr in; |
| 909 | - xs out; |
| 910 | - |
| 911 | - do |
| 912 | - :: atomic { nbuf < MaxSeq -> |
| 913 | - nbuf++; |
| 914 | - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); |
| 915 | - printf("MSC: nbuf: %d\n", nbuf); |
| 916 | - inc(NextFrame) |
| 917 | - } |
| 918 | - :: atomic { in?r,s -> |
| 919 | - if |
| 920 | - :: r == FrameExp -> |
| 921 | - printf("MSC: accept %d\n", r); |
| 922 | - inc(FrameExp) |
| 923 | - :: else |
| 924 | - -> printf("MSC: reject\n") |
| 925 | - fi |
| 926 | - }; |
| 927 | - d_step { |
| 928 | - do |
| 929 | - :: ((AckExp <= s) && (s < NextFrame)) |
| 930 | - || ((AckExp <= s) && (NextFrame < AckExp)) |
| 931 | - || ((s < NextFrame) && (NextFrame < AckExp)) -> |
| 932 | - nbuf--; |
| 933 | - printf("MSC: nbuf: %d\n", nbuf); |
| 934 | - inc(AckExp) |
| 935 | - :: else -> |
| 936 | - printf("MSC: %d %d %d\n", AckExp, s, NextFrame); |
| 937 | - break |
| 938 | - od; skip |
| 939 | - } |
| 940 | - :: timeout -> |
| 941 | - d_step { |
| 942 | - NextFrame = AckExp; |
| 943 | - printf("MSC: timeout\n"); |
| 944 | - i = 1; |
| 945 | - do |
| 946 | - :: i <= nbuf -> |
| 947 | - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); |
| 948 | - inc(NextFrame); |
| 949 | - i++ |
| 950 | - :: else -> |
| 951 | - break |
| 952 | - od; i = 0 |
| 953 | - } |
| 954 | - od |
| 955 | -} |
| 956 | //GO.SYSIN DD ex.9b |
| 957 | echo ex.9c 1>&2 |
| 958 | sed 's/.//' >ex.9c <<'//GO.SYSIN DD ex.9c' |
| 959 | -#define MaxSeq 3 |
| 960 | -#define MaxSeq_plus_1 4 |
| 961 | -#define inc(x) x = (x + 1) % (MaxSeq + 1) |
| 962 | - |
| 963 | -#define CHECKIT |
| 964 | - |
| 965 | -#ifdef CHECKIT |
| 966 | - mtype = { red, white, blue }; /* Wolper's test */ |
| 967 | - chan source = [0] of { mtype }; |
| 968 | - chan q[2] = [MaxSeq] of { mtype, byte, byte }; |
| 969 | - mtype rcvd = white; |
| 970 | - mtype sent = white; |
| 971 | -#else |
| 972 | - chan q[2] = [MaxSeq] of { byte, byte }; |
| 973 | -#endif |
| 974 | - |
| 975 | -active [2] proctype p5() |
| 976 | -{ byte NextFrame, AckExp, FrameExp, |
| 977 | - r, s, nbuf, i; |
| 978 | - chan in, out; |
| 979 | -#ifdef CHECKIT |
| 980 | - mtype ball; |
| 981 | - byte frames[MaxSeq_plus_1]; |
| 982 | -#endif |
| 983 | - |
| 984 | - d_step { |
| 985 | - in = q[_pid]; |
| 986 | - out = q[1-_pid] |
| 987 | - }; |
| 988 | - |
| 989 | - xr in; |
| 990 | - xs out; |
| 991 | - |
| 992 | - do |
| 993 | - :: atomic { |
| 994 | - nbuf < MaxSeq -> |
| 995 | - nbuf++; |
| 996 | -#ifdef CHECKIT |
| 997 | - if |
| 998 | - :: _pid%2 -> source?ball |
| 999 | - :: else |
| 1000 | - fi; |
| 1001 | - frames[NextFrame] = ball; |
| 1002 | - out!ball, NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); |
| 1003 | - if |
| 1004 | - :: _pid%2 -> sent = ball; |
| 1005 | - :: else |
| 1006 | - fi; |
| 1007 | -#else |
| 1008 | - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); |
| 1009 | -#endif |
| 1010 | -#ifdef VERBOSE |
| 1011 | - printf("MSC: nbuf: %d\n", nbuf); |
| 1012 | -#endif |
| 1013 | - inc(NextFrame) |
| 1014 | - } |
| 1015 | -#ifdef CHECKIT |
| 1016 | - :: atomic { in?ball,r,s -> |
| 1017 | -#else |
| 1018 | - :: atomic { in?r,s -> |
| 1019 | -#endif |
| 1020 | - if |
| 1021 | - :: r == FrameExp -> |
| 1022 | -#ifdef VERBOSE |
| 1023 | - printf("MSC: accept %d\n", r); |
| 1024 | -#endif |
| 1025 | -#ifdef CHECKIT |
| 1026 | - if |
| 1027 | - :: _pid%2 |
| 1028 | - :: else -> rcvd = ball |
| 1029 | - fi; |
| 1030 | -#endif |
| 1031 | - inc(FrameExp) |
| 1032 | - :: else |
| 1033 | -#ifdef VERBOSE |
| 1034 | - -> printf("MSC: reject\n") |
| 1035 | -#endif |
| 1036 | - fi |
| 1037 | - }; |
| 1038 | - d_step { |
| 1039 | - do |
| 1040 | - :: ((AckExp <= s) && (s < NextFrame)) |
| 1041 | - || ((AckExp <= s) && (NextFrame < AckExp)) |
| 1042 | - || ((s < NextFrame) && (NextFrame < AckExp)) -> |
| 1043 | - nbuf--; |
| 1044 | -#ifdef VERBOSE |
| 1045 | - printf("MSC: nbuf: %d\n", nbuf); |
| 1046 | -#endif |
| 1047 | - inc(AckExp) |
| 1048 | - :: else -> |
| 1049 | -#ifdef VERBOSE |
| 1050 | - printf("MSC: %d %d %d\n", AckExp, s, NextFrame); |
| 1051 | -#endif |
| 1052 | - break |
| 1053 | - od; |
| 1054 | - skip |
| 1055 | - } |
| 1056 | - :: timeout -> |
| 1057 | - d_step { |
| 1058 | - NextFrame = AckExp; |
| 1059 | -#ifdef VERBOSE |
| 1060 | - printf("MSC: timeout\n"); |
| 1061 | -#endif |
| 1062 | - i = 1; |
| 1063 | - do |
| 1064 | - :: i <= nbuf -> |
| 1065 | -#ifdef CHECKIT |
| 1066 | - if |
| 1067 | - :: _pid%2 -> ball = frames[NextFrame] |
| 1068 | - :: else |
| 1069 | - fi; |
| 1070 | - out!ball, NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); |
| 1071 | -#else |
| 1072 | - out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); |
| 1073 | -#endif |
| 1074 | - inc(NextFrame); |
| 1075 | - i++ |
| 1076 | - :: else -> |
| 1077 | - break |
| 1078 | - od; |
| 1079 | - i = 0 |
| 1080 | - } |
| 1081 | - od |
| 1082 | -} |
| 1083 | -#ifdef CHECKIT |
| 1084 | -active proctype Source() |
| 1085 | -{ |
| 1086 | - do |
| 1087 | - :: source!white |
| 1088 | - :: source!red -> break |
| 1089 | - od; |
| 1090 | - do |
| 1091 | - :: source!white |
| 1092 | - :: source!blue -> break |
| 1093 | - od; |
| 1094 | -end: do |
| 1095 | - :: source!white |
| 1096 | - od |
| 1097 | -} |
| 1098 | - |
| 1099 | -#define sw (sent == white) |
| 1100 | -#define sr (sent == red) |
| 1101 | -#define sb (sent == blue) |
| 1102 | - |
| 1103 | -#define rw (rcvd == white) |
| 1104 | -#define rr (rcvd == red) |
| 1105 | -#define rb (rcvd == blue) |
| 1106 | - |
| 1107 | -#define LTL 3 |
| 1108 | -#if LTL==1 |
| 1109 | - |
| 1110 | -never { /* ![](sr -> <> rr) */ |
| 1111 | - /* the never claim is generated by |
| 1112 | - spin -f "![](sr -> <> rr)" |
| 1113 | - and then edited a little for readability |
| 1114 | - the same is true for all others below |
| 1115 | - */ |
| 1116 | - do |
| 1117 | - :: 1 |
| 1118 | - :: !rr && sr -> goto accept |
| 1119 | - od; |
| 1120 | -accept: |
| 1121 | - if |
| 1122 | - :: !rr -> goto accept |
| 1123 | - fi |
| 1124 | -} |
| 1125 | - |
| 1126 | -#endif |
| 1127 | -#if LTL==2 |
| 1128 | - |
| 1129 | -never { /* !rr U rb */ |
| 1130 | - do |
| 1131 | - :: !rr |
| 1132 | - :: rb -> break /* move to implicit 2nd state */ |
| 1133 | - od |
| 1134 | -} |
| 1135 | - |
| 1136 | -#endif |
| 1137 | -#if LTL==3 |
| 1138 | - |
| 1139 | -never { /* (![](sr -> <> rr)) || (!rr U rb) */ |
| 1140 | - |
| 1141 | - if |
| 1142 | - :: 1 -> goto T0_S5 |
| 1143 | - :: !rr && sr -> goto accept_S8 |
| 1144 | - :: !rr -> goto T0_S2 |
| 1145 | - :: rb -> goto accept_all |
| 1146 | - fi; |
| 1147 | -accept_S8: |
| 1148 | - if |
| 1149 | - :: !rr -> goto T0_S8 |
| 1150 | - fi; |
| 1151 | -T0_S2: |
| 1152 | - if |
| 1153 | - :: !rr -> goto T0_S2 |
| 1154 | - :: rb -> goto accept_all |
| 1155 | - fi; |
| 1156 | -T0_S8: |
| 1157 | - if |
| 1158 | - :: !rr -> goto accept_S8 |
| 1159 | - fi; |
| 1160 | -T0_S5: |
| 1161 | - if |
| 1162 | - :: 1 -> goto T0_S5 |
| 1163 | - :: !rr && sr -> goto accept_S8 |
| 1164 | - fi; |
| 1165 | -accept_all: |
| 1166 | - skip |
| 1167 | -} |
| 1168 | -#endif |
| 1169 | - |
| 1170 | -#endif |
| 1171 | //GO.SYSIN DD ex.9c |