1 /***** spin: pangen3.h *****/ 2 3 /* 4 * This file is part of the public release of Spin. It is subject to the 5 * terms in the LICENSE file that is included in this source directory. 6 * Tool documentation is available at http://spinroot.com 7 */ 8 9 static const char *Head0[] = { 10 "#if defined(BFS) && defined(REACH)", 11 " #undef REACH", /* redundant with bfs */ 12 "#endif", 13 "#ifdef VERI", 14 " #define BASE 1", 15 "#else", 16 " #define BASE 0", 17 "#endif", 18 "typedef struct Trans {", 19 " short atom; /* if &2 = atomic trans; if &8 local */", 20 "#ifdef HAS_UNLESS", 21 " short escp[HAS_UNLESS]; /* lists the escape states */", 22 " short e_trans; /* if set, this is an escp-trans */", 23 "#endif", 24 " short tpe[2]; /* class of operation (for reduction) */", 25 " short qu[6]; /* for conditional selections: qid's */", 26 " uchar ty[6]; /* ditto: type's */", 27 "#ifdef NIBIS", 28 " short om; /* completion status of preselects */", 29 "#endif", 30 " char *tp; /* src txt of statement */", 31 " int st; /* the nextstate */", 32 " int t_id; /* transition id, unique within proc */", 33 " int forw; /* index forward transition */", 34 " int back; /* index return transition */", 35 " struct Trans *nxt;", 36 "} Trans;\n", 37 38 "#ifdef TRIX", 39 " #define qptr(x) (channels[x]->body)", 40 " #define pptr(x) (processes[x]->body)", 41 "#else", 42 " #define qptr(x) (((uchar *)&now)+(int)q_offset[x])", 43 " #define pptr(x) (((uchar *)&now)+(int)proc_offset[x])", 44 /* " #define Pptr(x) ((proc_offset[x])?pptr(x):noptr)", */ 45 "#endif", 46 "extern uchar *Pptr(int);", 47 "extern uchar *Qptr(int);", 48 49 "#define q_sz(x) (((Q0 *)qptr(x))->Qlen)", 50 "", 51 "#ifdef TRIX", 52 " #ifdef VECTORSZ", 53 " #undef VECTORSZ", /* backward compatibility */ 54 " #endif", 55 " #if WS==4", 56 " #define VECTORSZ 2056 /* ((MAXPROC+MAXQ+4)*sizeof(uchar *)) */", 57 " #else", 58 " #define VECTORSZ 4112 /* the formula causes probs in preprocessing */", 59 " #endif", 60 "#else", 61 " #ifndef VECTORSZ", 62 " #define VECTORSZ 1024 /* sv size in bytes */", 63 " #endif", 64 "#endif\n", 65 "#define MAXQ 255", 66 "#define MAXPROC 255", 67 "", 68 0, 69 }; 70 71 static const char *Header[] = { 72 "#ifdef VERBOSE", 73 " #ifndef CHECK", 74 " #define CHECK", 75 " #endif", 76 " #ifndef DEBUG", 77 " #define DEBUG", 78 " #endif", 79 "#endif", 80 "#ifdef SAFETY", 81 " #ifndef NOFAIR", 82 " #define NOFAIR", 83 " #endif", 84 "#endif", 85 #if 0 86 NOREDUCE BITSTATE SAFETY MA WS>4 87 CNTRSTACK: - + + d - 88 FULLSTACK: + d - - d 89 - + d d d 90 - + + d + 91 - - d d d 92 Neither: + d + d d 93 + d d + d 94 #endif 95 "#ifdef NOREDUCE", 96 " #ifndef XUSAFE", 97 " #define XUSAFE", 98 " #endif", 99 " #if !defined(SAFETY) && !defined(MA)", 100 " #define FULLSTACK", /* => NOREDUCE && !SAFETY && !MA */ 101 " #endif", 102 "#else", 103 " #ifdef BITSTATE", 104 " #if defined(SAFETY) && WS<=4", 105 " #define CNTRSTACK", /* => !NOREDUCE && BITSTATE && SAFETY && WS<=4 */ 106 " #else", 107 " #define FULLSTACK", /* => !NOREDUCE && BITSTATE && (!SAFETY || WS>4) */ 108 " #endif", 109 " #else", 110 " #define FULLSTACK", /* => !NOREDUCE && !BITSTATE */ 111 " #endif", 112 "#endif", 113 "#ifdef BITSTATE", 114 " #ifndef NOCOMP", 115 " #define NOCOMP", 116 " #endif", 117 " #if !defined(LC) && defined(SC)", 118 " #define LC", 119 " #endif", 120 "#endif", 121 "#if defined(COLLAPSE2) || defined(COLLAPSE3) || defined(COLLAPSE4)", 122 " /* accept the above for backward compatibility */", 123 " #define COLLAPSE", 124 "#endif", 125 "#ifdef HC", 126 " #undef HC", 127 " #define HC4", 128 "#endif", 129 "#if defined(HC0) || defined(HC1) || defined(HC2) || defined(HC3) || defined(HC4)", 130 " #define HC 4", /* 2x32 bits */ 131 "#endif", /* really only one hashcompact mode, not 5 */ 132 "", 133 "typedef struct _Stack { /* for queues and processes */", 134 "#if VECTORSZ>32000", 135 " int o_delta;", 136 " #ifndef TRIX", 137 " int o_offset;", 138 " int o_skip;", 139 " #endif", 140 " int o_delqs;", 141 "#else", 142 " short o_delta;", 143 " #ifndef TRIX", 144 " short o_offset;", 145 " short o_skip;", 146 " #endif", 147 " short o_delqs;", 148 "#endif", 149 " short o_boq;", 150 "#ifdef TRIX", 151 " short parent;", 152 " char *b_ptr;", /* used in delq/q_restor and delproc/p_restor */ 153 "#else", 154 " char *body;", /* full copy of state vector in non-trix mode */ 155 "#endif", 156 "#ifndef XUSAFE", 157 " char *o_name;", 158 "#endif", 159 " struct _Stack *nxt;", 160 " struct _Stack *lst;", 161 "} _Stack;\n", 162 "typedef struct Svtack { /* for complete state vector */", 163 "#if VECTORSZ>32000", 164 " int o_delta;", 165 " int m_delta;", 166 "#else", 167 " short o_delta; /* current size of frame */", 168 " short m_delta; /* maximum size of frame */", 169 "#endif", 170 "#if SYNC", 171 " short o_boq;", 172 "#endif", 173 0, 174 }; 175 176 static const char *Header0[] = { 177 " char *body;", 178 " struct Svtack *nxt;", 179 " struct Svtack *lst;", 180 "} Svtack;\n", 181 0, 182 }; 183 184 static const char *Head1[] = { 185 "typedef struct State {", 186 " uchar _nr_pr;", 187 " uchar _nr_qs;", 188 " uchar _a_t; /* cycle detection */", 189 #if 0 190 in _a_t: bits 0,4, and 5 =(1|16|32) are set during a 2nd dfs 191 bit 1 is used as the A-bit for fairness 192 bit 7 (128) is the proviso bit, for reduced 2nd dfs (acceptance) 193 #endif 194 "#ifndef NOFAIR", 195 " uchar _cnt[NFAIR]; /* counters, weak fairness */", 196 "#endif", 197 198 "#ifndef NOVSZ", 199 #ifdef SOLARIS 200 "#if 0", 201 /* v3.4 202 * noticed alignment problems with some Solaris 203 * compilers, if widest field isn't wordsized 204 */ 205 #else 206 "#if VECTORSZ<65536", 207 #endif 208 " unsigned short _vsz;", 209 "#else", 210 " ulong _vsz;", 211 "#endif", 212 "#endif", 213 214 "#ifdef HAS_LAST", /* cannot go before _cnt - see h_store() */ 215 " uchar _last; /* pid executed in last step */", 216 "#endif", 217 218 "#if defined(BITSTATE) && defined(BCS) && defined(STORE_CTX)", 219 " uchar _ctx; /* nr of context switches so far */", 220 "#endif", 221 "#if defined(BFS_PAR) && defined(L_BOUND)", 222 " uchar _l_bnd; /* bounded liveness */", 223 " uchar *_l_sds; /* seed state */", 224 "#endif", 225 "#ifdef EVENT_TRACE", 226 " #if nstates_event<256", 227 " uchar _event;", 228 " #else", 229 " unsigned short _event;", 230 " #endif", 231 "#endif", 232 0, 233 }; 234 235 static const char *Addp0[] = { 236 /* addproc(....parlist... */ ")", 237 "{ int j, h = now._nr_pr;", 238 "#ifndef NOCOMP", 239 " int k;", 240 "#endif", 241 " uchar *o_this = _this;\n", 242 "#ifndef INLINE", 243 " if (TstOnly) return (h < MAXPROC);", 244 "#endif", 245 "#ifndef NOBOUNDCHECK", 246 " /* redefine Index only within this procedure */", 247 " #undef Index", 248 " #define Index(x, y) Boundcheck(x, y, 0, 0, 0)", 249 "#endif", 250 " if (h >= MAXPROC)", 251 " Uerror(\"too many processes\");", 252 "#ifdef V_TRIX", 253 " printf(\"%%4d: add process %%d\\n\", depth, h);", 254 "#endif", 255 " switch (n) {", 256 " case 0: j = sizeof(P0); break;", 257 0, 258 }; 259 260 static const char *Addp1[] = { 261 " default: Uerror(\"bad proc - addproc\");", 262 " }", 263 " #ifdef BFS_PAR", 264 " bfs_prepmask(1); /* addproc */", 265 " #endif", 266 267 "#ifdef TRIX", 268 " vsize += sizeof(H_el *);", 269 "#else", 270 " if (vsize%%WS)", 271 " proc_skip[h] = WS-(vsize%%WS);", 272 " else", 273 " proc_skip[h] = 0;", 274 " #if !defined(NOCOMP) && !defined(HC)", 275 " for (k = vsize + (int) proc_skip[h]; k > vsize; k--)", 276 " Mask[k-1] = 1; /* align */", 277 " #endif", 278 " vsize += (int) proc_skip[h];", 279 " proc_offset[h] = vsize;", 280 " vsize += j;", 281 " #if defined(SVDUMP) && defined(VERBOSE)", 282 " if (vprefix > 0)", 283 " { int dummy = 0;", 284 " write(svfd, (uchar *) &dummy, sizeof(int)); /* mark */", 285 " write(svfd, (uchar *) &h, sizeof(int));", 286 " write(svfd, (uchar *) &n, sizeof(int));", 287 " #if VECTORSZ>32000", 288 " write(svfd, (uchar *) &proc_offset[h], sizeof(int));", 289 " write(svfd, (uchar *) &now, vprefix-4*sizeof(int)); /* padd */", 290 " #else", 291 " write(svfd, (uchar *) &proc_offset[h], sizeof(short));", 292 " write(svfd, (uchar *) &now, vprefix-3*sizeof(int)-sizeof(short)); /* padd */", 293 " #endif", 294 " }", 295 " #endif", 296 "#endif", 297 298 " now._nr_pr += 1;", 299 "#if defined(BCS) && defined(CONSERVATIVE)", 300 " if (now._nr_pr >= CONSERVATIVE*8)", 301 " { printf(\"pan: error: too many processes -- recompile with \");", 302 " printf(\"-DCONSERVATIVE=%%d\\n\", CONSERVATIVE+1);", 303 " pan_exit(1);", 304 " }", 305 "#endif", 306 " if (fairness && ((int) now._nr_pr + 1 >= (8*NFAIR)/2))", 307 " { printf(\"pan: error: too many processes -- current\");", 308 " printf(\" max is %%d procs (-DNFAIR=%%d)\\n\",", 309 " (8*NFAIR)/2 - 2, NFAIR);", 310 " printf(\"\\trecompile with -DNFAIR=%%d\\n\",", 311 " NFAIR+1);", 312 " pan_exit(1);", 313 " }", 314 "#ifndef NOVSZ", 315 " now._vsz = vsize;", 316 "#endif", 317 " hmax = max(hmax, vsize);", 318 319 "#ifdef TRIX", 320 " #ifndef BFS", 321 " if (freebodies)", 322 " { processes[h] = freebodies;", 323 " freebodies = freebodies->nxt;", 324 " } else", 325 " { processes[h] = (TRIX_v6 *) emalloc(sizeof(TRIX_v6));", 326 " processes[h]->body = (uchar *) emalloc(Maxbody * sizeof(char));", 327 " }", 328 " processes[h]->modified = 1; /* addproc */", 329 " #endif", 330 " processes[h]->psize = j;", 331 " processes[h]->parent_pid = calling_pid;", 332 " processes[h]->nxt = (TRIX_v6 *) 0;", 333 "#else", 334 " #if !defined(NOCOMP) && !defined(HC)", 335 " for (k = 1; k <= Air[n]; k++)", 336 " Mask[vsize - k] = 1; /* pad */", 337 " Mask[vsize-j] = 1; /* _pid */", 338 " #endif", 339 " #ifdef BFS_PAR", 340 " bfs_fixmask(1); /* addproc */", 341 " #endif", 342 " if (vsize >= VECTORSZ)", 343 " { printf(\"pan: error, VECTORSZ too small, recompile pan.c\");", 344 " printf(\" with -DVECTORSZ=N with N>%%d\\n\", (int) vsize);", 345 " Uerror(\"aborting\");", 346 " }", 347 "#endif", 348 349 " memset((char *)pptr(h), 0, j);", 350 " _this = pptr(h);", 351 " if (BASE > 0 && h > 0)", 352 " { ((P0 *)_this)->_pid = h-BASE;", 353 " } else", 354 " { ((P0 *)_this)->_pid = h;", 355 " }", 356 " switch (n) {", 357 0, 358 }; 359 360 static const char *Addq0[] = { 361 "", 362 "int", 363 "addqueue(int calling_pid, int n, int is_rv)", 364 "{ int j=0, i = now._nr_qs;", 365 "#if !defined(NOCOMP) && !defined(TRIX)", 366 " int k;", 367 "#endif", 368 " if (i >= MAXQ)", 369 " Uerror(\"too many queues\");", 370 "#ifdef V_TRIX", 371 " printf(\"%%4d: add queue %%d\\n\", depth, i);", 372 "#endif", 373 " switch (n) {", 374 0, 375 }; 376 377 static const char *Addq1[] = { 378 " default: Uerror(\"bad queue - addqueue\");", 379 " }", 380 " #ifdef BFS_PAR", 381 " bfs_prepmask(2); /* addqueue */", 382 " #endif", 383 384 "#ifdef TRIX", 385 " vsize += sizeof(H_el *);", 386 "#else", 387 " if (vsize%%WS)", 388 " q_skip[i] = WS-(vsize%%WS);", 389 " else", 390 " q_skip[i] = 0;", 391 " #if !defined(NOCOMP) && !defined(HC)", 392 " k = vsize;", 393 " #ifndef BFS", 394 " if (is_rv) k += j;", 395 " #endif", 396 " for (k += (int) q_skip[i]; k > vsize; k--)", 397 " Mask[k-1] = 1;", 398 " #endif", 399 " vsize += (int) q_skip[i];", 400 " q_offset[i] = vsize;", 401 " vsize += j;", 402 " #ifdef BFS_PAR", 403 " bfs_fixmask(2); /* addqueue */", 404 " #endif", 405 "#endif", 406 407 " now._nr_qs += 1;", 408 "#ifndef NOVSZ", 409 " now._vsz = vsize;", 410 "#endif", 411 " hmax = max(hmax, vsize);", 412 413 "#ifdef TRIX", 414 " #ifndef BFS", 415 " if (freebodies)", 416 " { channels[i] = freebodies;", 417 " freebodies = freebodies->nxt;", 418 " } else", 419 " { channels[i] = (TRIX_v6 *) emalloc(sizeof(TRIX_v6));", 420 " channels[i]->body = (uchar *) emalloc(Maxbody * sizeof(char));", 421 " }", 422 " channels[i]->modified = 1; /* addq */", 423 " #endif", 424 " channels[i]->psize = j;", 425 " channels[i]->parent_pid = calling_pid;", 426 " channels[i]->nxt = (TRIX_v6 *) 0;", 427 "#else", 428 " if (vsize >= VECTORSZ)", 429 " Uerror(\"VECTORSZ is too small, edit pan.h\");", 430 "#endif", 431 432 " if (j > 0)", /* zero if there are no queues */ 433 " { memset((char *)qptr(i), 0, j);", 434 " }", 435 " ((Q0 *)qptr(i))->_t = n;", 436 " return i+1;", 437 "}\n", 438 0, 439 }; 440 441 static const char *Addq11[] = { 442 "{ int j; uchar *z;\n", 443 "#ifdef HAS_SORTED", 444 " int k;", 445 "#endif", 446 " if (!into--)", 447 " uerror(\"ref to uninitialized chan name (sending)\");", 448 " if (into >= (int) now._nr_qs || into < 0)", 449 " Uerror(\"qsend bad queue#\");", 450 "#if defined(TRIX) && !defined(BFS)", 451 " #ifndef TRIX_ORIG", 452 " (trpt+1)->q_bup = now._ids_[now._nr_pr+into];", 453 " #ifdef V_TRIX", 454 " printf(\"%%4d: channel %%d s save %%p from %%d\\n\",", 455 " depth, into, (trpt+1)->q_bup, now._nr_pr+into);", 456 " #endif", 457 " #endif", 458 " channels[into]->modified = 1; /* qsend */", 459 " #ifdef V_TRIX", 460 " printf(\"%%4d: channel %%d modified\\n\", depth, into);", 461 " #endif", 462 "#endif", 463 " z = qptr(into);", 464 " j = ((Q0 *)qptr(into))->Qlen;", 465 " switch (((Q0 *)qptr(into))->_t) {", 466 0, 467 }; 468 469 static const char *Addq2[] = { 470 " case 0: printf(\"queue %%d was deleted\\n\", into+1);", 471 " default: Uerror(\"bad queue - qsend\");", 472 " }", 473 "#ifdef EVENT_TRACE", 474 " if (in_s_scope(into+1))", 475 " require('s', into);", 476 "#endif", 477 "}", 478 "#endif\n", 479 "#if SYNC", 480 "int", 481 "q_zero(int from)", 482 "{ if (!from--)", 483 " { uerror(\"ref to uninitialized chan name (q_zero)\");", 484 " return 0;", 485 " }", 486 " switch(((Q0 *)qptr(from))->_t) {", 487 0, 488 }; 489 490 static const char *Addq3[] = { 491 " case 0: printf(\"queue %%d was deleted\\n\", from+1);", 492 " }", 493 " Uerror(\"bad queue q-zero\");", 494 " return -1;", 495 "}", 496 "int", 497 "not_RV(int from)", 498 "{ if (q_zero(from))", 499 " { printf(\"==>> a test of the contents of a rv \");", 500 " printf(\"channel always returns FALSE\\n\");", 501 " uerror(\"error to poll rendezvous channel\");", 502 " }", 503 " return 1;", 504 "}", 505 "#endif", 506 "#ifndef XUSAFE", 507 "void", 508 "setq_claim(int x, int m, char *s, int y, char *p)", 509 "{ if (x == 0)", 510 " uerror(\"x[rs] claim on uninitialized channel\");", 511 " if (x < 0 || x > MAXQ)", 512 " Uerror(\"cannot happen setq_claim\");", 513 " q_claim[x] |= m;", 514 " p_name[y] = p;", 515 " q_name[x] = s;", 516 " if (m&2) q_S_check(x, y);", 517 " if (m&1) q_R_check(x, y);", 518 "}", 519 "short q_sender[MAXQ+1];", 520 "int", 521 "q_S_check(int x, int who)", 522 "{ if (!q_sender[x])", 523 " { q_sender[x] = who+1;", 524 "#if SYNC", 525 " if (q_zero(x))", 526 " { printf(\"chan %%s (%%d), \",", 527 " q_name[x], x-1);", 528 " printf(\"sndr proc %%s (%%d)\\n\",", 529 " p_name[who], who);", 530 " uerror(\"xs chans cannot be used for rv\");", 531 " }", 532 "#endif", 533 " } else", 534 " if (q_sender[x] != who+1)", 535 " { printf(\"pan: xs assertion violated: \");", 536 " printf(\"access to chan <%%s> (%%d)\\npan: by \",", 537 " q_name[x], x-1);", 538 " if (q_sender[x] > 0 && p_name[q_sender[x]-1])", 539 " printf(\"%%s (proc %%d) and by \",", 540 " p_name[q_sender[x]-1], q_sender[x]-1);", 541 " printf(\"%%s (proc %%d)\\n\",", 542 " p_name[who], who);", 543 " uerror(\"error, partial order reduction invalid\");", 544 " }", 545 " return 1;", 546 "}", 547 "short q_recver[MAXQ+1];", 548 "int", 549 "q_R_check(int x, int who)", 550 "{", 551 "#ifdef VERBOSE", 552 " printf(\"q_R_check x=%%d who=%%d\\n\", x, who);", 553 "#endif", 554 " if (!q_recver[x])", 555 " { q_recver[x] = who+1;", 556 "#if SYNC", 557 " if (q_zero(x))", 558 " { printf(\"chan %%s (%%d), \",", 559 " q_name[x], x-1);", 560 " printf(\"recv proc %%s (%%d)\\n\",", 561 " p_name[who], who);", 562 " uerror(\"xr chans cannot be used for rv\");", 563 " }", 564 "#endif", 565 " } else", 566 " if (q_recver[x] != who+1)", 567 " { printf(\"pan: xr assertion violated: \");", 568 " printf(\"access to chan %%s (%%d)\\npan: \",", 569 " q_name[x], x-1);", 570 " if (q_recver[x] > 0 && p_name[q_recver[x]-1])", 571 " printf(\"by %%s (proc %%d) and \",", 572 " p_name[q_recver[x]-1], q_recver[x]-1);", 573 " printf(\"by %%s (proc %%d)\\n\",", 574 " p_name[who], who);", 575 " uerror(\"error, partial order reduction invalid\");", 576 " }", 577 " return 1;", 578 "}", 579 "#endif", 580 "int", 581 "q_len(int x)", 582 "{ if (!x--)", 583 " uerror(\"ref to uninitialized chan name (len)\");", 584 " return ((Q0 *)qptr(x))->Qlen;", 585 "}\n", 586 "int", 587 "q_full(int from)", 588 "{ if (!from--)", 589 " uerror(\"ref to uninitialized chan name (qfull)\");", 590 " switch(((Q0 *)qptr(from))->_t) {", 591 0, 592 }; 593 594 static const char *Addq4[] = { 595 " case 0: printf(\"queue %%d was deleted\\n\", from+1);", 596 " }", 597 " Uerror(\"bad queue - q_full\");", 598 " return 0;", 599 "}\n", 600 "#ifdef HAS_UNLESS", 601 "int", 602 "q_e_f(int from)", 603 "{ /* empty or full */", 604 " return !q_len(from) || q_full(from);", 605 "}", 606 "#endif", 607 "#if NQS>0", 608 "int", 609 "qrecv(int from, int slot, int fld, int done)", 610 "{ uchar *z;", 611 " int j, k, r=0;\n", 612 " if (!from--)", 613 " uerror(\"ref to uninitialized chan name (receiving)\");", 614 "#if defined(TRIX) && !defined(BFS)", 615 " #ifndef TRIX_ORIG", 616 " (trpt+1)->q_bup = now._ids_[now._nr_pr+from];", 617 " #ifdef V_TRIX", 618 " printf(\"%%4d: channel %%d r save %%p from %%d\\n\",", 619 " depth, from, (trpt+1)->q_bup, now._nr_pr+from);", 620 " #endif", 621 " #endif", 622 " channels[from]->modified = 1; /* qrecv */", 623 " #ifdef V_TRIX", 624 " printf(\"%%4d: channel %%d modified\\n\", depth, from);", 625 " #endif", 626 "#endif", 627 " if (from >= (int) now._nr_qs || from < 0)", 628 " Uerror(\"qrecv bad queue#\");", 629 " z = qptr(from);", 630 "#ifdef EVENT_TRACE", 631 " if (done && (in_r_scope(from+1)))", 632 " require('r', from);", 633 "#endif", 634 " switch (((Q0 *)qptr(from))->_t) {", 635 0, 636 }; 637 638 static const char *Addq5[] = { 639 " case 0: printf(\"queue %%d was deleted\\n\", from+1);", 640 " default: Uerror(\"bad queue - qrecv\");", 641 " }", 642 " return r;", 643 "}", 644 "#endif\n", 645 "#ifndef BITSTATE", 646 " #ifdef COLLAPSE", 647 "long", 648 "col_q(int i, char *z)", 649 "{ int j=0, k;", 650 " char *x, *y;", 651 " Q0 *ptr = (Q0 *) qptr(i);", 652 " switch (ptr->_t) {", 653 0, 654 }; 655 656 static const char *Code0[] = { 657 "#ifdef INIT_STATE", 658 "void", /* Bocchino */ 659 "init_state(State state)" 660 "{ state._nr_pr = 0;", 661 " state._nr_qs = 0;", 662 " state._a_t = 0;", 663 "#ifndef NOFAIR", 664 " memset(&state._cnt, 0, sizeof(state._cnt));", 665 "#endif", 666 "#ifndef NOVSZ", 667 " state._vsz = 0;", 668 "#endif", 669 "#ifdef HAS_LAST", 670 " state._last = 0;", 671 "#endif", 672 "#if defined(BITSTATE) && defined(BCS) && defined(STORE_CTX)", 673 " state._ctx = 0;", 674 "#endif", 675 "#if defined(BFS_PAR) && defined(L_BOUND)", 676 " state._l_bnd = 0;", 677 " state._l_sds = 0;", 678 "#endif", 679 "#ifdef EVENT_TRACE", 680 " state_event = 0;", 681 "#endif", 682 "#ifdef TRIX", 683 " memset(&state._ids_, 0, sizeof(state._ids_));", 684 "#else", 685 " memset(&state.sv, 0, sizeof(state.sv));", 686 "#endif", 687 "}", 688 "#endif", 689 "", 690 "void", 691 "run(void)", 692 "{ /* int i; */", 693 "#ifdef INIT_STATE", 694 " init_state(now);", 695 "#else", 696 " memset((char *)&now, 0, sizeof(State));", 697 "#endif", 698 " vsize = (ulong) (sizeof(State) - VECTORSZ);", 699 "#ifndef NOVSZ", 700 " now._vsz = vsize;", 701 "#endif", 702 "#ifdef TRIX", 703 " if (VECTORSZ != sizeof(now._ids_))", 704 " { printf(\"VECTORSZ is %%d, but should be %%d in this mode\\n\",", 705 " VECTORSZ, (int) sizeof(now._ids_));", 706 " Uerror(\"VECTORSZ set incorrectly, recompile Spin (not pan.c)\");", 707 " }", 708 "#endif", 709 "/* optional provisioning statements, e.g. to */", 710 "/* set hidden variables, used as constants */", 711 "#ifdef PROV", 712 "#include PROV", 713 "#endif", 714 " settable();", 715 0, 716 }; 717 718 static const char *R0[] = { 719 " Maxbody = max(Maxbody, ((int) sizeof(P%d)));", 720 " reached[%d] = reached%d;", 721 " accpstate[%d] = (uchar *) emalloc(_nstates%d);", 722 " progstate[%d] = (uchar *) emalloc(_nstates%d);", 723 " loopstate%d = loopstate[%d] = (uchar *) emalloc(_nstates%d);", 724 " stopstate[%d] = (uchar *) emalloc(_nstates%d);", 725 " visstate[%d] = (uchar *) emalloc(_nstates%d);", 726 " mapstate[%d] = (short *) emalloc(_nstates%d * sizeof(short));", 727 " stopstate[%d][_endstate%d] = 1;", 728 0, 729 }; 730 731 static const char *R00[] = { 732 " NrStates[%d] = _nstates%d;", 733 0, 734 }; 735 736 static const char *R0a[] = { 737 " retrans(%d, _nstates%d, _start%d, src_ln%d, reached%d, loopstate%d);", 738 0, 739 }; 740 741 static const char *Code1[] = { 742 "#ifdef NP", 743 " #define ACCEPT_LAB 1 /* at least 1 in np_ */", 744 "#else", 745 " #define ACCEPT_LAB %d /* user-defined accept labels */", 746 "#endif", 747 "#ifdef MEMCNT", 748 " #ifdef MEMLIM", 749 " #warning -DMEMLIM takes precedence over -DMEMCNT", 750 " #undef MEMCNT", 751 " #else", 752 " #if MEMCNT<20", 753 " #warning using minimal value -DMEMCNT=20 (=1MB)", 754 " #define MEMLIM (1)", 755 " #undef MEMCNT", 756 " #else", 757 " #if MEMCNT==20", 758 " #define MEMLIM (1)", 759 " #undef MEMCNT", 760 " #else", 761 " #if MEMCNT>=50", 762 " #error excessive value for MEMCNT", 763 " #else", 764 " #define MEMLIM (1<<(MEMCNT-20))", 765 " #endif", 766 " #endif", 767 " #endif", 768 " #endif", 769 "#endif", 770 771 "#if NCORE>1 && !defined(MEMLIM)", 772 " #define MEMLIM (2048) /* need a default, using 2 GB */", 773 "#endif", 774 0, 775 }; 776 777 static const char *Code3[] = { 778 "#define PROG_LAB %d /* progress labels */", 779 0, 780 }; 781 782 static const char *R2[] = { 783 "uchar *accpstate[%d];", 784 "uchar *progstate[%d];", 785 "uchar *loopstate[%d];", 786 "uchar *reached[%d];", 787 "uchar *stopstate[%d];", 788 "uchar *visstate[%d];", 789 "short *mapstate[%d];", 790 "#ifdef HAS_CODE", 791 " int NrStates[%d];", 792 "#endif", 793 0, 794 }; 795 static const char *R3[] = { 796 " Maxbody = max(Maxbody, ((int) sizeof(Q%d)));", 797 0, 798 }; 799 static const char *R4[] = { 800 " r_ck(reached%d, _nstates%d, %d, src_ln%d, src_file%d);", 801 0, 802 }; 803 static const char *R5[] = { 804 " case %d: j = sizeof(P%d); break;", 805 0, 806 }; 807 static const char *R6[] = { 808 " }", 809 " _this = o_this;", 810 "#ifdef TRIX", 811 " re_mark_all(1); /* addproc */", 812 "#endif", 813 " return h-BASE;", 814 "#ifndef NOBOUNDCHECK", 815 " #undef Index", 816 " #define Index(x, y) Boundcheck(x, y, II, tt, t)", 817 "#endif", 818 "}\n", 819 "#if defined(BITSTATE) && defined(COLLAPSE)", 820 " /* just to allow compilation, to generate the error */", 821 " long col_p(int i, char *z) { return 0; }", 822 " long col_q(int i, char *z) { return 0; }", 823 "#endif", 824 "#ifndef BITSTATE", 825 " #ifdef COLLAPSE", 826 "long", 827 "col_p(int i, char *z)", 828 "{ int j, k; ulong ordinal(char *, long, short);", 829 " char *x, *y;", 830 " P0 *ptr = (P0 *) pptr(i);", 831 " switch (ptr->_t) {", 832 " case 0: j = sizeof(P0); break;", 833 0, 834 }; 835 static const char *R7a[] = { 836 "void\nre_mark_all(int whichway)", 837 "{ int j;", 838 " #ifdef V_TRIX", 839 " printf(\"%%d: re_mark_all channels %%d\\n\", depth, whichway);", 840 " #endif", 841 " #ifndef BFS", 842 " for (j = 0; j < now._nr_qs; j++)", 843 " channels[j]->modified = 1; /* channel index moved */", 844 " #endif", 845 " #ifndef TRIX_ORIG", 846 " if (whichway > 0)", 847 " { for (j = now._nr_pr + now._nr_qs - 1; j >= now._nr_pr; j--)", 848 " now._ids_[j] = now._ids_[j-1];", 849 " } else", 850 " { for (j = now._nr_pr; j < now._nr_pr + now._nr_qs; j++)", 851 " now._ids_[j] = now._ids_[j+1];", 852 " }", 853 " #endif", 854 "}", 855 0, 856 }; 857 858 static const char *R7b[] = { 859 "#ifdef BFS_PAR", 860 "void", 861 "bfs_prepmask(int caller)", 862 "{", 863 "#if !defined(NOCOMP) && !defined(HC)", 864 " memcpy((char *) &tmp_msk, (const char *) Mask, sizeof(State));", 865 " Mask = (uchar *) &tmp_msk;", 866 "#endif", 867 " switch (caller) {", 868 " case 1: /* addproc */", 869 "#if VECTORSZ>32000", 870 " memcpy((char *) P_o_tmp, (const char *) proc_offset, MAXPROC*sizeof(int));", 871 "#else", 872 " memcpy((char *) P_o_tmp, (const char *) proc_offset, MAXPROC*sizeof(short));", 873 "#endif", 874 " memcpy((char *) P_s_tmp, (const char *) proc_skip, MAXPROC*sizeof(uchar));", 875 " proc_offset = P_o_tmp;", 876 " proc_skip = (uchar *) &P_s_tmp[0];", 877 " break;", 878 " case 2: /* addqueue */", 879 "#if VECTORSZ>32000", 880 " memcpy((char *) Q_o_tmp, (const char *) q_offset, MAXQ*sizeof(int));", 881 "#else", 882 " memcpy((char *) Q_o_tmp, (const char *) q_offset, MAXQ*sizeof(short));", 883 "#endif", 884 " memcpy((char *) Q_s_tmp, (const char *) q_skip, MAXQ*sizeof(uchar));", 885 " q_offset = Q_o_tmp;", 886 " q_skip = (uchar *) &Q_s_tmp[0];", 887 " break;", 888 " case 3: /* no nothing */", 889 " break;", 890 " default: /* cannot happen */", 891 " Uerror(\"no good\");", 892 " break;", 893 " }", 894 "}", 895 "", 896 "typedef struct BFS_saves BFS_saves;", 897 "struct BFS_saves {", 898 " char *m;", 899 " BFS_saves *nxt;", 900 "} *bfs_save_po,", 901 " *bfs_save_ps,", 902 "#if !defined(NOCOMP) && !defined(HC)", 903 " *bfs_save_mask,", 904 "#endif", 905 " *bfs_save_qo,", 906 " *bfs_save_qs;", 907 "", 908 "extern volatile uchar *sh_malloc(ulong);", 909 "static int bfs_runs; /* 0 before local heaps are initialized */", 910 "", 911 "void", 912 "bfs_swoosh(BFS_saves **where, char **what, int howmuch)", 913 "{ BFS_saves *m;", 914 " for (m = *where; m; m = m->nxt)", 915 " { if (memcmp(m->m, *what, howmuch) == 0)", 916 " { *what = m->m;", 917 " return;", 918 " } }", 919 " m = (BFS_saves *) emalloc(sizeof(BFS_saves));", 920 " if (bfs_runs)", 921 " { m->m = (char *) sh_malloc(howmuch);", 922 " } else", 923 " { m->m = (char *) sh_pre_malloc(howmuch);", 924 " }", 925 " memcpy(m->m, *what, howmuch);", 926 " m->nxt = *where;", 927 " *where = m;", 928 " *what = m->m;", 929 "}", 930 "", 931 "void", 932 "bfs_fixmask(int caller)", /* 1=addproc, 2=addqueue */ 933 "{", 934 "#if !defined(NOCOMP) && !defined(HC)", 935 " bfs_swoosh(&bfs_save_mask, (char **) &Mask, sizeof(State));", 936 "#endif", 937 "#ifndef TRIX", 938 " switch (caller) {", 939 " case 1: /* addproc */", 940 " #if VECTORSZ>32000", 941 " bfs_swoosh(&bfs_save_po, (char **) &proc_offset, MAXPROC*sizeof(int));", 942 " #else", 943 " bfs_swoosh(&bfs_save_po, (char **) &proc_offset, MAXPROC*sizeof(short));", 944 " #endif", 945 " bfs_swoosh(&bfs_save_ps, (char **) &proc_skip, MAXPROC*sizeof(uchar));", 946 " break;", 947 " case 2: /* addqueue */", 948 " #if VECTORSZ>32000", 949 " bfs_swoosh(&bfs_save_qo, (char **) &q_offset, MAXQ*sizeof(int));", 950 " #else", 951 " bfs_swoosh(&bfs_save_qo, (char **) &q_offset, MAXQ*sizeof(short));", 952 " #endif", 953 " bfs_swoosh(&bfs_save_qs, (char **) &q_skip, MAXQ*sizeof(uchar));", 954 " break;", 955 " case 3: /* do nothing */", 956 " break;", 957 " default:", 958 " Uerror(\"double plus ungood\");", 959 " break;", 960 " }", 961 "#endif", 962 "}", 963 "#endif", 964 0, 965 }; 966 static const char *R8a[] = { 967 " default: Uerror(\"bad proctype - collapse\");", 968 " }", 969 " if (z) x = z; else x = scratch;", 970 " y = (char *) ptr; k = proc_offset[i];", 971 "", 972 "#if !defined(NOCOMP) && !defined(HC)", 973 " for ( ; j > 0; j--, y++)", 974 " if (!Mask[k++]) *x++ = *y;", 975 "#else", 976 " memcpy(x, y, j);", 977 " x += j;", 978 "#endif", 979 " for (j = 0; j < WS-1; j++)", 980 " *x++ = 0;", 981 " x -= j;", 982 " if (z) return (long) (x - z);", 983 " return ordinal(scratch, x-scratch, (short) (2+ptr->_t));", 984 "}", 985 " #endif", 986 "#endif", 987 0, 988 }; 989 static const char *R8b[] = { 990 " default: Uerror(\"bad qtype - collapse\");", 991 " }", 992 " if (z) x = z; else x = scratch;", 993 " y = (char *) ptr; k = q_offset[i];", 994 995 "#if NQS > 0", 996 " /* no need to store the empty slots at the end */", 997 " j -= (q_max[ptr->_t] - ptr->Qlen) * ((j - 2)/q_max[ptr->_t]);", 998 "#endif", 999 "", 1000 "#if !defined(NOCOMP) && !defined(HC)", 1001 " for ( ; j > 0; j--, y++)", 1002 " if (!Mask[k++]) *x++ = *y;", 1003 "#else", 1004 " memcpy(x, y, j);", 1005 " x += j;", 1006 "#endif", 1007 " for (j = 0; j < WS-1; j++)", 1008 " *x++ = 0;", 1009 " x -= j;", 1010 " if (z) return (long) (x - z);", 1011 " return ordinal(scratch, x-scratch, 1); /* chan */", 1012 "}", 1013 " #endif", 1014 "#endif", 1015 0, 1016 }; 1017 1018 static const char *R12[] = { 1019 "\t\tcase %d: r = ((Q%d *)z)->contents[slot].fld%d; break;", 1020 0, 1021 }; 1022 1023 const char *R13_[] = { 1024 "int ", 1025 "unsend(int into)", 1026 "{ int _m=0, j; uchar *z;\n", 1027 "#ifdef HAS_SORTED", 1028 " int k;", 1029 "#endif", 1030 " if (!into--)", 1031 " uerror(\"ref to uninitialized chan (unsend)\");", 1032 "#if defined(TRIX) && !defined(BFS)", 1033 " #ifndef TRIX_ORIG", 1034 " now._ids_[now._nr_pr+into] = trpt->q_bup;", 1035 " #ifdef V_TRIX", 1036 " printf(\"%%4d: channel %%d s restore %%p into %%d\\n\",", 1037 " depth, into, trpt->q_bup, now._nr_pr+into);", 1038 " #endif", 1039 " #else", 1040 " channels[into]->modified = 1; /* unsend */", 1041 " #ifdef V_TRIX", 1042 " printf(\"%%4d: channel %%d unmodify\\n\", depth, into);", 1043 " #endif", 1044 " #endif", 1045 "#endif", 1046 " z = qptr(into);", 1047 " j = ((Q0 *)z)->Qlen;", 1048 " ((Q0 *)z)->Qlen = --j;", 1049 " switch (((Q0 *)qptr(into))->_t) {", 1050 0, 1051 }; 1052 const char *R14_[] = { 1053 " default: Uerror(\"bad queue - unsend\");", 1054 " }", 1055 " return _m;", 1056 "}\n", 1057 "void", 1058 "unrecv(int from, int slot, int fld, int fldvar, int strt)", 1059 "{ int j; uchar *z;\n", 1060 " if (!from--)", 1061 " uerror(\"ref to uninitialized chan (unrecv)\");", 1062 "#if defined(TRIX) && !defined(BFS)", 1063 " #ifndef TRIX_ORIG", 1064 " now._ids_[now._nr_pr+from] = trpt->q_bup;", 1065 " #ifdef V_TRIX", 1066 " printf(\"%%4d: channel %%d r restore %%p into %%d\\n\",", 1067 " depth, from, trpt->q_bup, now._nr_pr+from);", 1068 " #endif", 1069 " #else", 1070 " channels[from]->modified = 1; /* unrecv */", 1071 " #ifdef V_TRIX", 1072 " printf(\"%%4d: channel %%d unmodify\\n\", depth, from);", 1073 " #endif", 1074 " #endif", 1075 "#endif", 1076 " z = qptr(from);", 1077 " j = ((Q0 *)z)->Qlen;", 1078 " if (strt) ((Q0 *)z)->Qlen = j+1;", 1079 " switch (((Q0 *)qptr(from))->_t) {", 1080 0, 1081 }; 1082 const char *R15_[] = { 1083 " default: Uerror(\"bad queue - qrecv\");", 1084 " }", 1085 "}", 1086 0, 1087 }; 1088 static const char *Proto[] = { 1089 "", 1090 "/** function prototypes **/", 1091 "char *emalloc(ulong);", 1092 "char *Malloc(ulong);", 1093 "int Boundcheck(int, int, int, int, Trans *);", 1094 "int addqueue(int, int, int);", 1095 "/* int atoi(char *); */", 1096 "/* int abort(void); */", 1097 "int close(int);", /* should probably remove this */ 1098 #if 0 1099 "#ifndef SC", 1100 " int creat(char *, unsigned short);", 1101 " int write(int, void *, unsigned);", 1102 "#endif", 1103 #endif 1104 "int delproc(int, int);", 1105 "int endstate(void);", 1106 "int find_claim(char *);", 1107 "int h_store(char *, int);", 1108 "int pan_rand(void);", 1109 "int q_cond(short, Trans *);", 1110 "int q_full(int);", 1111 "int q_len(int);", 1112 "int q_zero(int);", 1113 "int qrecv(int, int, int, int);", 1114 "int unsend(int);", 1115 "/* void *sbrk(int); */", 1116 "void spin_assert(int, char *, int, int, Trans *);", 1117 "#ifdef BFS_PAR", 1118 "void bfs_printf(const char *, ...);", 1119 "volatile uchar *sh_pre_malloc(ulong);", 1120 "#endif", 1121 "void c_chandump(int);", 1122 "void c_globals(void);", 1123 "void c_locals(int, int);", 1124 "void checkcycles(void);", 1125 "void crack(int, int, Trans *, short *);", 1126 "void d_sfh(uchar *, int);", 1127 "void d_hash(uchar *, int);", 1128 "void m_hash(uchar *, int);", 1129 "void s_hash(uchar *, int);", 1130 "void delq(int);", 1131 "void dot_crack(int, int, Trans *);", 1132 "void do_reach(void);", 1133 "void pan_exit(int);", 1134 "void exit(int);", 1135 "#ifdef BFS_PAR", 1136 " void bfs_setup_mem(void);", 1137 "#endif", 1138 "#ifdef BITSTATE", 1139 " void sinit(void);", 1140 "#else", 1141 " void hinit(void);", 1142 "#endif", 1143 "void imed(Trans *, int, int, int);", 1144 "void new_state(void);", 1145 "void p_restor(int);", 1146 "void putpeg(int, int);", 1147 "void putrail(void);", 1148 "void q_restor(void);", 1149 "void retrans(int, int, int, short *, uchar *, uchar *);", 1150 "void select_claim(int);", 1151 "void settable(void);", 1152 "void setq_claim(int, int, char *, int, char *);", 1153 "void sv_restor(void);", 1154 "void sv_save(void);", 1155 "void tagtable(int, int, int, short *, uchar *);", 1156 "void do_dfs(int, int, int, short *, uchar *, uchar *);", 1157 "void unrecv(int, int, int, int, int);", 1158 "void usage(FILE *);", 1159 "void wrap_stats(void);\n", 1160 "#ifdef MA", 1161 " int g_store(char *, int, uchar);", 1162 "#endif", 1163 "#if defined(FULLSTACK) && defined(BITSTATE)", 1164 " int onstack_now(void);", 1165 " void onstack_init(void);", 1166 " void onstack_put(void);", 1167 " void onstack_zap(void);", 1168 "#endif", 1169 "#ifndef XUSAFE", 1170 " int q_S_check(int, int);", 1171 " int q_R_check(int, int);", 1172 " uchar q_claim[MAXQ+1];", 1173 " char *q_name[MAXQ+1];", 1174 " char *p_name[MAXPROC+1];", 1175 "#endif", 1176 "", 1177 "#ifndef NO_V_PROVISO", 1178 " #define V_PROVISO", 1179 "#endif", 1180 "#if !defined(NO_RESIZE) && !defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(SPACE) && !defined(USE_TDH) && NCORE==1", 1181 " #define AUTO_RESIZE", 1182 "#endif", 1183 "", 1184 "typedef struct Trail Trail;", 1185 "typedef struct H_el H_el;", 1186 "", 1187 "struct H_el {", 1188 " H_el *nxt;", 1189 " #ifdef FULLSTACK", 1190 " unsigned int tagged;", 1191 " #if defined(BITSTATE) && !defined(NOREDUCE) && !defined(SAFETY)", 1192 " unsigned int proviso;", /* uses just 1 bit 0/1 */ 1193 " #endif", 1194 " #endif", 1195 " #if defined(CHECK) || (defined(COLLAPSE) && !defined(FULLSTACK))", 1196 " ulong st_id;", 1197 " #endif", 1198 " #if !defined(SAFETY) || defined(REACH)", 1199 " uint D;", 1200 " #endif", 1201 " #ifdef BCS", 1202 " #ifndef CONSERVATIVE", 1203 " #define CONSERVATIVE 1 /* good for up to 8 processes */", 1204 " #endif", 1205 " #ifdef CONSERVATIVE", 1206 " #if CONSERVATIVE <= 0 || CONSERVATIVE>32", 1207 " #error sensible values for CONSERVATIVE are 1..32 (256/8 = 32)", 1208 " #endif", 1209 " uchar ctx_pid[CONSERVATIVE];", /* pids setting lowest value */ 1210 " #endif", 1211 " uchar ctx_low;", /* lowest nr of context switches seen so far */ 1212 " #endif", 1213 " #if NCORE>1", 1214 " /* could cost 1 extra word: 4 bytes if 32-bit and 8 bytes if 64-bit */", 1215 " #ifdef V_PROVISO", 1216 " uchar cpu_id; /* id of cpu that created the state */", 1217 " #endif", 1218 " #endif", 1219 " #ifdef COLLAPSE", 1220 " #if VECTORSZ<65536", 1221 " ushort ln;", /* length of vector */ 1222 " #else", 1223 " ulong ln;", /* length of vector */ 1224 " #endif", 1225 " #endif", 1226 " #if defined(AUTO_RESIZE) && !defined(BITSTATE)", 1227 " ulong m_K1;", 1228 " #endif", 1229 " ulong state;", 1230 "};", 1231 "", 1232 "#ifdef BFS_PAR", 1233 "typedef struct BFS_Trail BFS_Trail;", 1234 "struct BFS_Trail {", 1235 " H_el *ostate;", 1236 " int st;", 1237 " int o_tt;", 1238 " T_ID t_id;", /* could be uint, ushort, or uchar */ 1239 " uchar pr;", 1240 " uchar o_pm;", 1241 " uchar tau;", 1242 "};", 1243 " #if SYNC>0", 1244 " #undef BFS_NOTRAIL", /* just in case it was used */ 1245 " #endif", 1246 "#endif", 1247 "", 1248 "#ifdef RHASH", 1249 " #ifndef PERMUTED", 1250 " #define PERMUTED", 1251 " #endif", 1252 "#endif", 1253 "", 1254 "struct Trail {", 1255 " int st; /* current state */", 1256 " int o_tt;", 1257 "#ifdef PERMUTED", 1258 " uint seed;", 1259 " uchar oII;", 1260 "#endif", 1261 " uchar pr; /* process id */", 1262 " uchar tau; /* 8 bit-flags */", 1263 " uchar o_pm; /* 8 more bit-flags */", 1264 "", 1265 " #if 0", 1266 " Meaning of bit-flags on tau and o_pm:", 1267 " tau&1 -> timeout enabled", 1268 " tau&2 -> request to enable timeout 1 level up (in claim)", 1269 " tau&4 -> current transition is a claim move", 1270 " tau&8 -> current transition is an atomic move", 1271 " tau&16 -> last move was truncated on stack", 1272 " tau&32 -> current transition is a preselected move", 1273 " tau&64 -> at least one next state is not on the stack", 1274 " tau&128 -> current transition is a stutter move", 1275 1276 " o_pm&1 -> the current pid moved -- implements else", 1277 " o_pm&2 -> this is an acceptance state", 1278 " o_pm&4 -> this is a progress state", 1279 " o_pm&8 -> fairness alg rule 1 undo mark", 1280 " o_pm&16 -> fairness alg rule 3 undo mark", 1281 " o_pm&32 -> fairness alg rule 2 undo mark", 1282 " o_pm&64 -> the current proc applied rule2", 1283 " o_pm&128 -> a fairness, dummy move - all procs blocked", 1284 " #endif", 1285 "", 1286 " #ifdef NSUCC", 1287 " uchar n_succ; /* nr of successor states */", 1288 " #endif", 1289 " #if defined(FULLSTACK) && defined(MA) && !defined(BFS)", 1290 " uchar proviso;", 1291 " #endif", 1292 " #ifndef BFS", 1293 " uchar o_n, o_ot; /* to save locals */", 1294 " #endif", 1295 " uchar o_m;", 1296 " #ifdef EVENT_TRACE", 1297 " #if nstates_event<256", 1298 " uchar o_event;", 1299 " #else", 1300 " unsigned short o_event;", 1301 " #endif", 1302 " #endif", 1303 " #ifndef BFS", 1304 " short o_To;", 1305 " #if defined(T_RAND) || defined(RANDOMIZE)", 1306 " short oo_i;", 1307 " #endif", 1308 " #endif", 1309 " #if defined(HAS_UNLESS) && !defined(BFS)", 1310 " int e_state; /* if escape trans - state of origin */", 1311 " #endif", 1312 " #if (defined(FULLSTACK) && !defined(MA)) || defined(BFS) || (NCORE>1)", 1313 " H_el *ostate; /* pointer to stored state */", 1314 " #endif", 1315 /* CNTRSTACK when !NOREDUCE && BITSTATE && SAFETY && WS<=4, uses LL[] */ 1316 " #if defined(CNTRSTACK) && !defined(BFS)", 1317 " long j6, j7;", 1318 " #endif", 1319 " Trans *o_t;", /* transition fct, next state */ 1320 1321 " #if !defined(BFS) && !defined(TRIX_ORIG)", 1322 " char *p_bup;", 1323 " char *q_bup;", 1324 " #endif", 1325 1326 " #ifdef BCS", 1327 " unsigned short sched_limit;", 1328 " unsigned char bcs; /* phase 1 or 2, or forced 4 */", 1329 " unsigned char b_pno; /* preferred pid */", 1330 " #endif", 1331 1332 " #ifdef P_RAND", /* process scheduling randomization */ 1333 " unsigned char p_left; /* nr of procs left to explore */", 1334 " short p_skip; /* to find starting point in list */", 1335 " #endif", 1336 1337 " #ifdef HAS_SORTED", 1338 " short ipt;", /* insertion slot in q */ 1339 " #endif", 1340 " #ifdef HAS_PRIORITY", 1341 " short o_priority;", 1342 " #endif", 1343 " union {", 1344 " int oval;", /* single backup value of variable */ 1345 " int *ovals;", /* ptr to multiple values */ 1346 " } bup;", 1347 "}; /* end of struct Trail */", 1348 "", 1349 "#ifdef BFS", /* breadth-first search */ 1350 " #define Q_PROVISO", 1351 " #ifndef INLINE_REV", 1352 " #define INLINE_REV", 1353 " #endif", 1354 "", 1355 "typedef struct SV_Hold {", 1356 " State *sv;", 1357 " #ifndef BFS_PAR", 1358 " int sz;", 1359 " #endif", 1360 " struct SV_Hold *nxt;", 1361 "} SV_Hold;", 1362 "#if !defined(BFS_PAR) || NRUNS>0", 1363 " typedef struct EV_Hold {", 1364 " #if !defined(BFS_PAR) || (!defined(NOCOMP) && !defined(HC) && NRUNS>0)", 1365 " char *sv; /* Mask */", 1366 " #endif", 1367 " #if VECTORSZ<65536", 1368 " ushort sz; /* vsize */", 1369 " #else", 1370 " ulong sz;", 1371 " #endif", 1372 " #ifdef BFS_PAR", 1373 " uchar owner;", 1374 " #endif", 1375 " uchar nrpr;", 1376 " uchar nrqs;", 1377 " #if !defined(BFS_PAR) || (!defined(TRIX) && NRUNS>0)", 1378 " char *po, *qo;", 1379 " char *ps, *qs;", 1380 " #endif", 1381 " struct EV_Hold *nxt;", 1382 " } EV_Hold;", 1383 "#endif", 1384 "typedef struct BFS_State {", 1385 " #ifdef BFS_PAR", 1386 " BFS_Trail *t_info;", 1387 " State *osv;", 1388 " #else", 1389 " Trail *frame;", 1390 " SV_Hold *onow;", 1391 " #endif", 1392 " #if !defined(BFS_PAR) || NRUNS>0", 1393 " EV_Hold *omask;", 1394 " #endif", 1395 " #if defined(Q_PROVISO) && !defined(NOREDUCE)", 1396 " H_el *lstate;", 1397 " #endif", 1398 " #if !defined(BFS_PAR) || SYNC>0", 1399 " short boq;", 1400 " #endif", 1401 " #ifdef VERBOSE", 1402 " ulong nr;", 1403 " #endif", 1404 " #ifndef BFS_PAR", /* new 6.2.4, 3 dec 2012 */ 1405 " struct BFS_State *nxt;", 1406 " #endif", 1407 "} BFS_State;", 1408 "#endif\n", 1409 0, 1410 }; 1411 1412 static const char *SvMap[] = { 1413 "void", 1414 "to_compile(void)", 1415 "{ char ctd[2048], carg[128];", 1416 "#ifdef BITSTATE", 1417 " strcpy(ctd, \"-DBITSTATE \");", 1418 "#else", 1419 " strcpy(ctd, \"\");", 1420 "#endif", 1421 "#ifdef BFS_PAR", 1422 " strcat(ctd, \"-DBFS_PAR \");", 1423 "#endif", 1424 "#ifdef NOVSZ", 1425 " strcat(ctd, \"-DNOVSZ \");", 1426 "#endif", 1427 "#ifdef RHASH", 1428 " strcat(ctd, \"-DRHASH \");", 1429 "#else", 1430 " #ifdef PERMUTED", 1431 " strcat(ctd, \"-DPERMUTED \");", 1432 " #endif", 1433 "#endif", 1434 "#ifdef P_REVERSE", 1435 " strcat(ctd, \"-DP_REVERSE \");", 1436 "#endif", 1437 "#ifdef T_REVERSE", 1438 " strcat(ctd, \"-DT_REVERSE \");", 1439 "#endif", 1440 "#ifdef T_RAND", 1441 " #if T_RAND>0", 1442 " sprintf(carg, \"-DT_RAND=%%d \", T_RAND);", 1443 " strcat(ctd, carg);", 1444 " #else", 1445 " strcat(ctd, \"-DT_RAND \");", 1446 " #endif", 1447 "#endif", 1448 "#ifdef P_RAND", 1449 " #if P_RAND>0", 1450 " sprintf(carg, \"-DP_RAND=%%d \", P_RAND);", 1451 " strcat(ctd, carg);", 1452 " #else", 1453 " strcat(ctd, \"-DP_RAND \");", 1454 " #endif", 1455 "#endif", 1456 "#ifdef BCS", 1457 " sprintf(carg, \"-DBCS=%%d \", BCS);", 1458 " strcat(ctd, carg);", 1459 "#endif", 1460 "#ifdef BFS", 1461 " strcat(ctd, \"-DBFS \");", 1462 "#endif", 1463 "#ifdef MEMLIM", 1464 " sprintf(carg, \"-DMEMLIM=%%d \", MEMLIM);", 1465 " strcat(ctd, carg);", 1466 "#else", 1467 "#ifdef MEMCNT", 1468 " sprintf(carg, \"-DMEMCNT=%%d \", MEMCNT);", 1469 " strcat(ctd, carg);", 1470 "#endif", 1471 "#endif", 1472 "#ifdef NOCLAIM", 1473 " strcat(ctd, \"-DNOCLAIM \");", 1474 "#endif", 1475 "#ifdef SAFETY", 1476 " strcat(ctd, \"-DSAFETY \");", 1477 "#else", 1478 "#ifdef NOFAIR", 1479 " strcat(ctd, \"-DNOFAIR \");", 1480 "#else", 1481 "#ifdef NFAIR", 1482 " if (NFAIR != 2)", 1483 " { sprintf(carg, \"-DNFAIR=%%d \", NFAIR);", 1484 " strcat(ctd, carg);", 1485 " }", 1486 "#endif", 1487 "#endif", 1488 "#endif", 1489 "#ifdef NOREDUCE", 1490 " strcat(ctd, \"-DNOREDUCE \");", 1491 "#else", 1492 "#ifdef XUSAFE", 1493 " strcat(ctd, \"-DXUSAFE \");", 1494 "#endif", 1495 "#endif", 1496 "#ifdef NP", 1497 " strcat(ctd, \"-DNP \");", 1498 "#endif", 1499 "#ifdef PEG", 1500 " strcat(ctd, \"-DPEG \");", 1501 "#endif", 1502 "#ifdef VAR_RANGES", 1503 " strcat(ctd, \"-DVAR_RANGES \");", 1504 "#endif", 1505 "#ifdef HC", 1506 " strcat(ctd, \"-DHC \");", 1507 "#endif", 1508 "#ifdef CHECK", 1509 " strcat(ctd, \"-DCHECK \");", 1510 "#endif", 1511 "#ifdef CTL", 1512 " strcat(ctd, \"-DCTL \");", 1513 "#endif", 1514 "#ifdef TRIX", 1515 " strcat(ctd, \"-DTRIX \");", 1516 "#endif", 1517 "#ifdef NIBIS", 1518 " strcat(ctd, \"-DNIBIS \");", 1519 "#endif", 1520 "#ifdef NOBOUNDCHECK", 1521 " strcat(ctd, \"-DNOBOUNDCHECK \");", 1522 "#endif", 1523 "#ifdef NOSTUTTER", 1524 " strcat(ctd, \"-DNOSTUTTER \");", 1525 "#endif", 1526 "#ifdef REACH", 1527 " strcat(ctd, \"-DREACH \");", 1528 "#endif", 1529 "#ifdef PRINTF", 1530 " strcat(ctd, \"-DPRINTF \");", 1531 "#endif", 1532 "#ifdef COLLAPSE", 1533 " strcat(ctd, \"-DCOLLAPSE \");", 1534 "#endif", 1535 "#ifdef MA", 1536 " sprintf(carg, \"-DMA=%%d \", MA);", 1537 " strcat(ctd, carg);", 1538 "#endif", 1539 "#ifdef SVDUMP", 1540 " strcat(ctd, \"-DSVDUMP \");", 1541 "#endif", 1542 "#if defined(VECTORSZ) && !defined(TRIX)", 1543 " if (VECTORSZ != 1024)", 1544 " { sprintf(carg, \"-DVECTORSZ=%%d \", VECTORSZ);", 1545 " strcat(ctd, carg);", 1546 " }", 1547 "#endif", 1548 "#ifdef VERBOSE", 1549 " strcat(ctd, \"-DVERBOSE \");", 1550 "#endif", 1551 "#ifdef CHECK", 1552 " strcat(ctd, \"-DCHECK \");", 1553 "#endif", 1554 "#ifdef SDUMP", 1555 " strcat(ctd, \"-DSDUMP \");", 1556 "#endif", 1557 "#if NCORE>1", 1558 " sprintf(carg, \"-DNCORE=%%d \", NCORE);", 1559 " strcat(ctd, carg);", 1560 "#endif", 1561 "#ifdef VMAX", 1562 " if (VMAX != 256)", 1563 " { sprintf(carg, \"-DVMAX=%%d \", VMAX);", 1564 " strcat(ctd, carg);", 1565 " }", 1566 "#endif", 1567 "#ifdef PMAX", 1568 " if (PMAX != 16)", 1569 " { sprintf(carg, \"-DPMAX=%%d \", PMAX);", 1570 " strcat(ctd, carg);", 1571 " }", 1572 "#endif", 1573 "#ifdef QMAX", 1574 " if (QMAX != 16)", 1575 " { sprintf(carg, \"-DQMAX=%%d \", QMAX);", 1576 " strcat(ctd, carg);", 1577 " }", 1578 "#endif", 1579 "#ifdef SET_WQ_SIZE", 1580 " sprintf(carg, \"-DSET_WQ_SIZE=%%d \", SET_WQ_SIZE);", 1581 " strcat(ctd, carg);", 1582 "#endif", 1583 " printf(\"Compiled as: cc -o pan %%span.c\\n\", ctd);", 1584 "}", 1585 0, 1586 }; 1587