sys/src/cmd/spin/pangen3.h

   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         "void",
 658         "run(void)",
 659         "{      /* int i; */",
 660         "       memset((char *)&now, 0, sizeof(State));",
 661         "       vsize = (ulong) (sizeof(State) - VECTORSZ);",
 662         "#ifndef NOVSZ",
 663         "       now._vsz = vsize;",
 664         "#endif",
 665         "#ifdef TRIX",
 666         "       if (VECTORSZ != sizeof(now._ids_))",
 667         "       {       printf(\"VECTORSZ is %%d, but should be %%d in this mode\\n\",",
 668         "                       VECTORSZ, (int) sizeof(now._ids_));",
 669         "               Uerror(\"VECTORSZ set incorrectly, recompile Spin (not pan.c)\");",
 670         "       }",
 671         "#endif",
 672         "/* optional provisioning statements, e.g. to */",
 673         "/* set hidden variables, used as constants */",
 674         "#ifdef PROV",
 675         "#include PROV",
 676         "#endif",
 677         "       settable();",
 678         0,
 679 };
 680
 681 static const char *R0[] = {
 682         "       Maxbody = max(Maxbody, ((int) sizeof(P%d)));",
 683         "       reached[%d] = reached%d;",
 684         "       accpstate[%d] = (uchar *) emalloc(_nstates%d);",
 685         "       progstate[%d] = (uchar *) emalloc(_nstates%d);",
 686         "       loopstate%d = loopstate[%d] = (uchar *) emalloc(_nstates%d);",
 687         "       stopstate[%d] = (uchar *) emalloc(_nstates%d);",
 688         "       visstate[%d] = (uchar *) emalloc(_nstates%d);",
 689         "       mapstate[%d] = (short *) emalloc(_nstates%d * sizeof(short));",
 690         "       stopstate[%d][_endstate%d] = 1;",
 691         0,
 692 };
 693
 694 static const char *R00[] = {
 695         "       NrStates[%d] = _nstates%d;",
 696         0,
 697 };
 698
 699 static const char *R0a[] = {
 700         "       retrans(%d, _nstates%d, _start%d, src_ln%d, reached%d, loopstate%d);",
 701         0,
 702 };
 703
 704 static const char *Code1[] = {
 705         "#ifdef NP",
 706         "       #define ACCEPT_LAB      1 /* at least 1 in np_ */",
 707         "#else",
 708         "       #define ACCEPT_LAB      %d /* user-defined accept labels */",
 709         "#endif",
 710         "#ifdef MEMCNT",
 711         "       #ifdef MEMLIM",
 712         "               #warning -DMEMLIM takes precedence over -DMEMCNT",
 713         "               #undef MEMCNT",
 714         "       #else",
 715         "               #if MEMCNT<20",
 716         "                       #warning using minimal value -DMEMCNT=20 (=1MB)",
 717         "                       #define MEMLIM  (1)",
 718         "                       #undef MEMCNT",
 719         "               #else",
 720         "                       #if MEMCNT==20",
 721         "                               #define MEMLIM  (1)",
 722         "                               #undef MEMCNT",
 723         "                       #else",
 724         "                        #if MEMCNT>=50",
 725         "                               #error excessive value for MEMCNT",
 726         "                        #else",
 727         "                               #define MEMLIM  (1<<(MEMCNT-20))",
 728         "                        #endif",
 729         "                       #endif",
 730         "               #endif",
 731         "       #endif",
 732         "#endif",
 733
 734         "#if NCORE>1 && !defined(MEMLIM)",
 735         "       #define MEMLIM  (2048)  /* need a default, using 2 GB */",
 736         "#endif",
 737         0,
 738 };
 739
 740 static const char *Code3[] = {
 741         "#define PROG_LAB       %d /* progress labels */",
 742         0,
 743 };
 744
 745 static const char *R2[] = {
 746         "uchar *accpstate[%d];",
 747         "uchar *progstate[%d];",
 748         "uchar *loopstate[%d];",
 749         "uchar *reached[%d];",
 750         "uchar *stopstate[%d];",
 751         "uchar *visstate[%d];",
 752         "short *mapstate[%d];",
 753         "#ifdef HAS_CODE",
 754         "       int NrStates[%d];",
 755         "#endif",
 756         0,
 757 };
 758 static const char *R3[] = {
 759         "       Maxbody = max(Maxbody, ((int) sizeof(Q%d)));",
 760         0,
 761 };
 762 static const char *R4[] = {
 763         "       r_ck(reached%d, _nstates%d, %d, src_ln%d, src_file%d);",
 764         0,
 765 };
 766 static const char *R5[] = {
 767         "       case %d: j = sizeof(P%d); break;",
 768         0,
 769 };
 770 static const char *R6[] = {
 771         "       }",
 772         "       this = o_this;",
 773         "#ifdef TRIX",
 774         "       re_mark_all(1); /* addproc */",
 775         "#endif",
 776         "       return h-BASE;",
 777         "#ifndef NOBOUNDCHECK",
 778         "       #undef Index",
 779         "       #define Index(x, y)     Boundcheck(x, y, II, tt, t)",
 780         "#endif",
 781         "}\n",
 782         "#if defined(BITSTATE) && defined(COLLAPSE)",
 783         "       /* just to allow compilation, to generate the error */",
 784         "       long col_p(int i, char *z) { return 0; }",
 785         "       long col_q(int i, char *z) { return 0; }",
 786         "#endif",
 787         "#ifndef BITSTATE",
 788         "       #ifdef COLLAPSE",
 789         "long",
 790         "col_p(int i, char *z)",
 791         "{      int j, k; ulong ordinal(char *, long, short);",
 792         "       char *x, *y;",
 793         "       P0 *ptr = (P0 *) pptr(i);",
 794         "       switch (ptr->_t) {",
 795         "       case 0: j = sizeof(P0); break;",
 796         0,
 797 };
 798 static const char *R7a[] = {
 799         "void\nre_mark_all(int whichway)",
 800         "{      int j;",
 801         "       #ifdef V_TRIX",
 802         "               printf(\"%%d: re_mark_all channels %%d\\n\", depth, whichway);",
 803         "       #endif",
 804         "       #ifndef BFS",
 805         "       for (j = 0; j < now._nr_qs; j++)",
 806         "               channels[j]->modified = 1; /* channel index moved */",
 807         "       #endif",
 808         "       #ifndef TRIX_ORIG",
 809         "       if (whichway > 0)",
 810         "       {       for (j = now._nr_pr + now._nr_qs - 1; j >= now._nr_pr; j--)",
 811         "                       now._ids_[j] = now._ids_[j-1];",
 812         "       } else",
 813         "       {       for (j = now._nr_pr; j < now._nr_pr + now._nr_qs; j++)",
 814         "                       now._ids_[j] = now._ids_[j+1];",
 815         "       }",
 816         "       #endif",
 817         "}",
 818         0,
 819 };
 820
 821 static const char *R7b[] = {
 822         "#ifdef BFS_PAR",
 823         "inline void",
 824         "bfs_prepmask(int caller)",
 825         "{",
 826         "#if !defined(NOCOMP) && !defined(HC)",
 827         "       memcpy((char *) &tmp_msk, (const char *) Mask, sizeof(State));",
 828         "       Mask = (uchar *) &tmp_msk;",
 829         "#endif",
 830         "       switch (caller) {",
 831         "       case 1: /* addproc */",
 832         "#if VECTORSZ>32000",
 833         "               memcpy((char *) P_o_tmp, (const char *) proc_offset, MAXPROC*sizeof(int));",
 834         "#else",
 835         "               memcpy((char *) P_o_tmp, (const char *) proc_offset, MAXPROC*sizeof(short));",
 836         "#endif",
 837         "               memcpy((char *) P_s_tmp, (const char *) proc_skip, MAXPROC*sizeof(uchar));",
 838         "               proc_offset = P_o_tmp;",
 839         "               proc_skip   = (uchar *) &P_s_tmp[0];",
 840         "               break;",
 841         "       case 2: /* addqueue */",
 842         "#if VECTORSZ>32000",
 843         "               memcpy((char *) Q_o_tmp, (const char *) q_offset, MAXQ*sizeof(int));",
 844         "#else",
 845         "               memcpy((char *) Q_o_tmp, (const char *) q_offset, MAXQ*sizeof(short));",
 846         "#endif",
 847         "               memcpy((char *) Q_s_tmp, (const char *) q_skip, MAXQ*sizeof(uchar));",
 848         "               q_offset = Q_o_tmp;",
 849         "               q_skip   = (uchar *) &Q_s_tmp[0];",
 850         "               break;",
 851         "       case 3: /* no nothing */",
 852         "               break;",
 853         "       default: /* cannot happen */",
 854         "               Uerror(\"no good\");",
 855         "               break;",
 856         "       }",
 857         "}",
 858         "",
 859         "typedef struct BFS_saves BFS_saves;",
 860         "struct BFS_saves {",
 861         "       char *m;",
 862         "       BFS_saves *nxt;",
 863         "} *bfs_save_po,",
 864         "  *bfs_save_ps,",
 865         "#if !defined(NOCOMP) && !defined(HC)",
 866         "  *bfs_save_mask,",
 867         "#endif",
 868         "  *bfs_save_qo,",
 869         "  *bfs_save_qs;",
 870         "",
 871         "extern volatile uchar *sh_malloc(ulong);",
 872         "static int bfs_runs; /* 0 before local heaps are initialized */",
 873         "",
 874         "void",
 875         "bfs_swoosh(BFS_saves **where, char **what, int howmuch)",
 876         "{      BFS_saves *m;",
 877         "       for (m = *where; m; m = m->nxt)",
 878         "       {       if (memcmp(m->m, *what, howmuch) == 0)",
 879         "               {       *what = m->m;",
 880         "                       return;",
 881         "       }       }",
 882         "       m = (BFS_saves *) emalloc(sizeof(BFS_saves));",
 883         "       if (bfs_runs)",
 884         "       {       m->m = (char *) sh_malloc(howmuch);",
 885         "       } else",
 886         "       {       m->m = (char *) sh_pre_malloc(howmuch);",
 887         "       }",
 888         "       memcpy(m->m, *what, howmuch);",
 889         "       m->nxt = *where;",
 890         "       *where = m;",
 891         "       *what = m->m;",
 892         "}",
 893         "",
 894         "void",
 895         "bfs_fixmask(int caller)",      /* 1=addproc, 2=addqueue */
 896         "{",
 897         "#if !defined(NOCOMP) && !defined(HC)",
 898         "       bfs_swoosh(&bfs_save_mask, (char **) &Mask, sizeof(State));",
 899         "#endif",
 900         "#ifndef TRIX",
 901         "       switch (caller) {",
 902         "       case 1: /* addproc */",
 903         "       #if VECTORSZ>32000",
 904         "               bfs_swoosh(&bfs_save_po, (char **) &proc_offset, MAXPROC*sizeof(int));",
 905         "       #else",
 906         "               bfs_swoosh(&bfs_save_po, (char **) &proc_offset, MAXPROC*sizeof(short));",
 907         "       #endif",
 908         "               bfs_swoosh(&bfs_save_ps, (char **) &proc_skip, MAXPROC*sizeof(uchar));",
 909         "               break;",
 910         "       case 2: /* addqueue */",
 911         "       #if VECTORSZ>32000",
 912         "               bfs_swoosh(&bfs_save_qo, (char **) &q_offset, MAXQ*sizeof(int));",
 913         "       #else",
 914         "               bfs_swoosh(&bfs_save_qo, (char **) &q_offset, MAXQ*sizeof(short));",
 915         "       #endif",
 916         "               bfs_swoosh(&bfs_save_qs, (char **) &q_skip, MAXQ*sizeof(uchar));",
 917         "               break;",
 918         "       case 3: /* do nothing */",
 919         "               break;",
 920         "       default:",
 921         "               Uerror(\"double plus ungood\");",
 922         "               break;",
 923         "       }",
 924         "#endif",
 925         "}",
 926         "#endif",
 927         0,
 928 };
 929 static const char *R8a[] = {
 930         "       default: Uerror(\"bad proctype - collapse\");",
 931         "       }",
 932         "       if (z) x = z; else x = scratch;",
 933         "       y = (char *) ptr; k = proc_offset[i];",
 934         "",
 935         "#if !defined(NOCOMP) && !defined(HC)",
 936         "       for ( ; j > 0; j--, y++)",
 937         "               if (!Mask[k++]) *x++ = *y;",
 938         "#else",
 939         "       memcpy(x, y, j);",
 940         "       x += j;",
 941         "#endif",
 942         "       for (j = 0; j < WS-1; j++)",
 943         "               *x++ = 0;",
 944         "       x -= j;",
 945         "       if (z) return (long) (x - z);",
 946         "       return ordinal(scratch, x-scratch, (short) (2+ptr->_t));",
 947         "}",
 948         "       #endif",
 949         "#endif",
 950         0,
 951 };
 952 static const char *R8b[] = {
 953         "       default: Uerror(\"bad qtype - collapse\");",
 954         "       }",
 955         "       if (z) x = z; else x = scratch;",
 956         "       y = (char *) ptr; k = q_offset[i];",
 957
 958         "#if NQS > 0",
 959         "       /* no need to store the empty slots at the end */",
 960         "       j -= (q_max[ptr->_t] - ptr->Qlen) * ((j - 2)/q_max[ptr->_t]);",
 961         "#endif",
 962         "",
 963         "#if !defined(NOCOMP) && !defined(HC)",
 964         "       for ( ; j > 0; j--, y++)",
 965         "               if (!Mask[k++]) *x++ = *y;",
 966         "#else",
 967         "       memcpy(x, y, j);",
 968         "       x += j;",
 969         "#endif",
 970         "       for (j = 0; j < WS-1; j++)",
 971         "               *x++ = 0;",
 972         "       x -= j;",
 973         "       if (z) return (long) (x - z);",
 974         "       return ordinal(scratch, x-scratch, 1); /* chan */",
 975         "}",
 976         "       #endif",
 977         "#endif",
 978         0,
 979 };
 980
 981 static const char *R12[] = {
 982         "\t\tcase %d: r = ((Q%d *)z)->contents[slot].fld%d; break;",
 983         0,
 984 };
 985 const char *R13[] = {
 986         "int ",
 987         "unsend(int into)",
 988         "{      int _m=0, j; uchar *z;\n",
 989         "#ifdef HAS_SORTED",
 990         "       int k;",
 991         "#endif",
 992         "       if (!into--)",
 993         "               uerror(\"ref to uninitialized chan (unsend)\");",
 994         "#if defined(TRIX) && !defined(BFS)",
 995         "       #ifndef TRIX_ORIG",
 996         "               now._ids_[now._nr_pr+into] = trpt->q_bup;",
 997         "               #ifdef V_TRIX",
 998         "                       printf(\"%%4d: channel %%d s restore %%p into %%d\\n\",",
 999         "                               depth, into, trpt->q_bup, now._nr_pr+into);",
1000         "               #endif",
1001         "       #else",
1002         "               channels[into]->modified = 1;   /* unsend */",
1003         "               #ifdef V_TRIX",
1004         "                       printf(\"%%4d: channel %%d unmodify\\n\", depth, into);",
1005         "               #endif",
1006         "       #endif",
1007         "#endif",
1008         "       z = qptr(into);",
1009         "       j = ((Q0 *)z)->Qlen;",
1010         "       ((Q0 *)z)->Qlen = --j;",
1011         "       switch (((Q0 *)qptr(into))->_t) {",
1012         0,
1013 };
1014 const char *R14[] = {
1015         "       default: Uerror(\"bad queue - unsend\");",
1016         "       }",
1017         "       return _m;",
1018         "}\n",
1019         "void",
1020         "unrecv(int from, int slot, int fld, int fldvar, int strt)",
1021         "{      int j; uchar *z;\n",
1022         "       if (!from--)",
1023         "               uerror(\"ref to uninitialized chan (unrecv)\");",
1024         "#if defined(TRIX) && !defined(BFS)",
1025         "       #ifndef TRIX_ORIG",
1026         "               now._ids_[now._nr_pr+from] = trpt->q_bup;",
1027         "               #ifdef V_TRIX",
1028         "                       printf(\"%%4d: channel %%d r restore %%p into %%d\\n\",",
1029         "                               depth, from, trpt->q_bup, now._nr_pr+from);",
1030         "               #endif",
1031         "       #else",
1032         "               channels[from]->modified = 1;   /* unrecv */",
1033         "               #ifdef V_TRIX",
1034         "                       printf(\"%%4d: channel %%d unmodify\\n\", depth, from);",
1035         "               #endif",
1036         "       #endif",
1037         "#endif",
1038         "       z = qptr(from);",
1039         "       j = ((Q0 *)z)->Qlen;",
1040         "       if (strt) ((Q0 *)z)->Qlen = j+1;",
1041         "       switch (((Q0 *)qptr(from))->_t) {",
1042         0,
1043 };
1044 const char *R15[] = {
1045         "       default: Uerror(\"bad queue - qrecv\");",
1046         "       }",
1047         "}",
1048         0,
1049 };
1050 static const char *Proto[] = {
1051         "",
1052         "/** function prototypes **/",
1053         "char *emalloc(ulong);",
1054         "char *Malloc(ulong);",
1055         "int Boundcheck(int, int, int, int, Trans *);",
1056         "int addqueue(int, int, int);",
1057         "/* int atoi(char *); */",
1058         "/* int abort(void); */",
1059         "int close(int);",      /* should probably remove this */
1060 #if 0
1061         "#ifndef SC",
1062         "       int creat(char *, unsigned short);",
1063         "       int write(int, void *, unsigned);",
1064         "#endif",
1065 #endif
1066         "int delproc(int, int);",
1067         "int endstate(void);",
1068         "int find_claim(char *);",
1069         "int h_store(char *, int);",
1070         "int pan_rand(void);",
1071         "int q_cond(short, Trans *);",
1072         "int q_full(int);",
1073         "int q_len(int);",
1074         "int q_zero(int);",
1075         "int qrecv(int, int, int, int);",
1076         "int unsend(int);",
1077         "/* void *sbrk(int); */",
1078         "void spin_assert(int, char *, int, int, Trans *);",
1079         "#ifdef BFS_PAR",
1080         "void bfs_printf(const char *, ...);",
1081         "volatile uchar *sh_pre_malloc(ulong);",
1082         "#endif",
1083         "void c_chandump(int);",
1084         "void c_globals(void);",
1085         "void c_locals(int, int);",
1086         "void checkcycles(void);",
1087         "void crack(int, int, Trans *, short *);",
1088         "void d_sfh(uchar *, int);",
1089         "void d_hash(uchar *, int);",
1090         "void m_hash(uchar *, int);",
1091         "void s_hash(uchar *, int);",
1092         "void delq(int);",
1093         "void dot_crack(int, int, Trans *);",
1094         "void do_reach(void);",
1095         "void pan_exit(int);",
1096         "void exit(int);",
1097         "#ifdef BFS_PAR",
1098         "       void bfs_setup_mem(void);",
1099         "#endif",
1100         "#ifdef BITSTATE",
1101         "       void sinit(void);",
1102         "#else",
1103         "       void hinit(void);",
1104         "#endif",
1105         "void imed(Trans *, int, int, int);",
1106         "void new_state(void);",
1107         "void p_restor(int);",
1108         "void putpeg(int, int);",
1109         "void putrail(void);",
1110         "void q_restor(void);",
1111         "void retrans(int, int, int, short *, uchar *, uchar *);",
1112         "void select_claim(int);",
1113         "void settable(void);",
1114         "void setq_claim(int, int, char *, int, char *);",
1115         "void sv_restor(void);",
1116         "void sv_save(void);",
1117         "void tagtable(int, int, int, short *, uchar *);",
1118         "void do_dfs(int, int, int, short *, uchar *, uchar *);",
1119         "void unrecv(int, int, int, int, int);",
1120         "void usage(FILE *);",
1121         "void wrap_stats(void);\n",
1122         "#ifdef MA",
1123         "       int g_store(char *, int, uchar);",
1124         "#endif",
1125         "#if defined(FULLSTACK) && defined(BITSTATE)",
1126         "       int  onstack_now(void);",
1127         "       void onstack_init(void);",
1128         "       void onstack_put(void);",
1129         "       void onstack_zap(void);",
1130         "#endif",
1131         "#ifndef XUSAFE",
1132         "       int q_S_check(int, int);",
1133         "       int q_R_check(int, int);",
1134         "       uchar q_claim[MAXQ+1];",
1135         "       char *q_name[MAXQ+1];",
1136         "       char *p_name[MAXPROC+1];",
1137         "#endif",
1138         "",
1139         "#ifndef NO_V_PROVISO",
1140         "       #define V_PROVISO",
1141         "#endif",
1142         "#if !defined(NO_RESIZE) && !defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(SPACE) && !defined(USE_TDH) && NCORE==1",
1143         "       #define AUTO_RESIZE",
1144         "#endif",
1145         "",
1146         "typedef struct Trail Trail;",
1147         "typedef struct H_el  H_el;",
1148         "",
1149         "struct H_el {",
1150         "       H_el *nxt;",
1151         "       #ifdef FULLSTACK",
1152         "               unsigned int tagged;",
1153         "               #if defined(BITSTATE) && !defined(NOREDUCE) && !defined(SAFETY)",
1154         "                       unsigned int proviso;", /* uses just 1 bit 0/1 */
1155         "               #endif",
1156         "       #endif",
1157         "       #if defined(CHECK) || (defined(COLLAPSE) && !defined(FULLSTACK))",
1158         "               ulong st_id;",
1159         "       #endif",
1160         "       #if !defined(SAFETY) || defined(REACH)",
1161         "               uint D;",
1162         "       #endif",
1163         "       #ifdef BCS",
1164         "               #ifndef CONSERVATIVE",
1165         "                       #define CONSERVATIVE    1 /* good for up to 8 processes */",
1166         "               #endif",
1167         "               #ifdef CONSERVATIVE",
1168         "                       #if CONSERVATIVE <= 0 || CONSERVATIVE>32",
1169         "                       #error sensible values for CONSERVATIVE are 1..32 (256/8 = 32)",
1170         "                       #endif",
1171         "                       uchar ctx_pid[CONSERVATIVE];", /* pids setting lowest value */
1172         "               #endif",
1173         "               uchar ctx_low;", /* lowest nr of context switches seen so far */
1174         "       #endif",
1175         "       #if NCORE>1",
1176         "               /* could cost 1 extra word: 4 bytes if 32-bit and 8 bytes if 64-bit */",
1177         "               #ifdef V_PROVISO",
1178         "                       uchar   cpu_id;         /* id of cpu that created the state */",
1179         "               #endif",
1180         "       #endif",
1181         "       #ifdef COLLAPSE",
1182         "               #if VECTORSZ<65536",
1183         "                       ushort ln;",    /* length of vector */
1184         "               #else",
1185         "                       ulong ln;",     /* length of vector */
1186         "               #endif",
1187         "       #endif",
1188         "       #if defined(AUTO_RESIZE) && !defined(BITSTATE)",
1189         "               ulong m_K1;",
1190         "       #endif",
1191         "       ulong state;",
1192         "};",
1193         "",
1194         "#ifdef BFS_PAR",
1195         "typedef struct BFS_Trail BFS_Trail;",
1196         "struct BFS_Trail {",
1197         "       H_el *ostate;",
1198         "       int   st;",
1199         "       int   o_tt;",
1200         "       T_ID  t_id;", /* could be uint, ushort, or uchar */
1201         "       uchar pr;",
1202         "       uchar o_pm;",
1203         "       uchar tau;",
1204         "};",
1205         "       #if SYNC>0",
1206         "               #undef BFS_NOTRAIL", /* just in case it was used */
1207         "       #endif",
1208         "#endif",
1209         "",
1210         "#ifdef RHASH",
1211         "       #ifndef PERMUTED",
1212         "       #define PERMUTED",
1213         "       #endif",
1214         "#endif",
1215         "",
1216         "struct Trail {",
1217         "       int   st;       /* current state */",
1218         "       int   o_tt;",
1219         "#ifdef PERMUTED",
1220         "       uint  seed;",
1221         "       uchar oII;",
1222         "#endif",
1223         "       uchar pr;       /* process id */",
1224         "       uchar tau;      /* 8 bit-flags */",
1225         "       uchar o_pm;     /* 8 more bit-flags */",
1226         "",
1227         "       #if 0",
1228         "       Meaning of bit-flags on tau and o_pm:",
1229         "       tau&1   -> timeout enabled",
1230         "       tau&2   -> request to enable timeout 1 level up (in claim)",
1231         "       tau&4   -> current transition is a  claim move",
1232         "       tau&8   -> current transition is an atomic move",
1233         "       tau&16  -> last move was truncated on stack",
1234         "       tau&32  -> current transition is a preselected move",
1235         "       tau&64  -> at least one next state is not on the stack",
1236         "       tau&128 -> current transition is a stutter move",
1237
1238         "       o_pm&1  -> the current pid moved -- implements else",
1239         "       o_pm&2  -> this is an acceptance state",
1240         "       o_pm&4  -> this is a  progress state",
1241         "       o_pm&8  -> fairness alg rule 1 undo mark",
1242         "       o_pm&16 -> fairness alg rule 3 undo mark",
1243         "       o_pm&32 -> fairness alg rule 2 undo mark",
1244         "       o_pm&64 -> the current proc applied rule2",
1245         "       o_pm&128 -> a fairness, dummy move - all procs blocked",
1246         "       #endif",
1247         "",
1248         "       #ifdef NSUCC",
1249         "        uchar n_succ;  /* nr of successor states */",
1250         "       #endif",
1251         "       #if defined(FULLSTACK) && defined(MA) && !defined(BFS)",
1252         "        uchar proviso;",
1253         "       #endif",
1254         "       #ifndef BFS",
1255         "        uchar  o_n, o_ot;      /* to save locals */",
1256         "       #endif",
1257         "       uchar  o_m;",
1258         "       #ifdef EVENT_TRACE",
1259         "               #if nstates_event<256",
1260         "                uchar o_event;",
1261         "               #else",
1262         "                unsigned short o_event;",
1263         "               #endif",
1264         "       #endif",
1265         "       #ifndef BFS",
1266         "               short o_To;",
1267         "               #if defined(T_RAND) || defined(RANDOMIZE)",
1268         "                short oo_i;",
1269         "               #endif",
1270         "       #endif",
1271         "       #if defined(HAS_UNLESS) && !defined(BFS)",
1272         "        int e_state;   /* if escape trans - state of origin */",
1273         "       #endif",
1274         "       #if (defined(FULLSTACK) && !defined(MA)) || defined(BFS) || (NCORE>1)",
1275         "        H_el *ostate;  /* pointer to stored state */",
1276         "       #endif",
1277         /* CNTRSTACK when !NOREDUCE && BITSTATE && SAFETY && WS<=4, uses LL[] */
1278         "       #if defined(CNTRSTACK) && !defined(BFS)",
1279         "        long   j6, j7;",
1280         "       #endif",
1281         "       Trans *o_t;",   /* transition fct, next state   */
1282
1283         "       #if !defined(BFS) && !defined(TRIX_ORIG)",
1284         "        char *p_bup;",
1285         "        char *q_bup;",
1286         "       #endif",
1287
1288         "       #ifdef BCS",
1289         "        unsigned short sched_limit;",
1290         "        unsigned char  bcs; /* phase 1 or 2, or forced 4 */",
1291         "        unsigned char  b_pno; /* preferred pid */",
1292         "       #endif",
1293
1294         "       #ifdef P_RAND", /* process scheduling randomization */
1295         "        unsigned char p_left;  /* nr of procs left to explore */",
1296         "        short p_skip;  /* to find starting point in list */",
1297         "       #endif",
1298
1299         "       #ifdef HAS_SORTED",
1300         "        short ipt;",   /* insertion slot in q */
1301         "       #endif",
1302         "       #ifdef HAS_PRIORITY",
1303         "        short o_priority;",
1304         "       #endif",
1305         "       union {",
1306         "        int oval;",    /* single backup value of variable */
1307         "        int *ovals;",  /* ptr to multiple values */
1308         "       } bup;",
1309         "}; /* end of struct Trail */",
1310         "",
1311         "#ifdef BFS",   /* breadth-first search */
1312         "       #define Q_PROVISO",
1313         "       #ifndef INLINE_REV",
1314         "               #define INLINE_REV",
1315         "       #endif",
1316         "",
1317         "typedef struct SV_Hold {",
1318         "       State *sv;",
1319         " #ifndef BFS_PAR",
1320         "       int  sz;",
1321         " #endif",
1322         "       struct SV_Hold *nxt;",
1323         "} SV_Hold;",
1324         "#if !defined(BFS_PAR) || NRUNS>0",
1325         "       typedef struct EV_Hold {",
1326         "        #if !defined(BFS_PAR) || (!defined(NOCOMP) && !defined(HC) && NRUNS>0)",
1327         "               char *sv;       /* Mask */",
1328         "        #endif",
1329         "        #if VECTORSZ<65536",
1330         "               ushort sz;      /* vsize */",
1331         "        #else",
1332         "               ulong  sz;",
1333         "        #endif",
1334         "        #ifdef BFS_PAR",
1335         "               uchar owner;",
1336         "        #endif",
1337         "               uchar nrpr;",
1338         "               uchar nrqs;",
1339         "               #if !defined(BFS_PAR) || (!defined(TRIX) && NRUNS>0)",
1340         "                       char *po, *qo;",
1341         "                       char *ps, *qs;",
1342         "               #endif",
1343         "               struct EV_Hold *nxt;",
1344         "       } EV_Hold;",
1345         "#endif",
1346         "typedef struct BFS_State {",
1347         " #ifdef BFS_PAR",
1348         "       BFS_Trail *t_info;",
1349         "       State   *osv;",
1350         " #else",
1351         "       Trail   *frame;",
1352         "       SV_Hold *onow;",
1353         " #endif",
1354         " #if !defined(BFS_PAR) || NRUNS>0",
1355         "       EV_Hold *omask;",
1356         " #endif",
1357         " #if defined(Q_PROVISO) && !defined(NOREDUCE)",
1358         "       H_el *lstate;",
1359         " #endif",
1360         " #if !defined(BFS_PAR) || SYNC>0",
1361         "       short boq;",
1362         " #endif",
1363         " #ifdef VERBOSE",
1364         "       ulong nr;",
1365         " #endif",
1366         " #ifndef BFS_PAR",     /* new 6.2.4, 3 dec 2012 */
1367         "       struct BFS_State *nxt;",
1368         " #endif",
1369         "} BFS_State;",
1370         "#endif\n",
1371         0,
1372 };
1373
1374 static const char *SvMap[] = {
1375         "void",
1376         "to_compile(void)",
1377         "{      char ctd[2048], carg[128];",
1378         "#ifdef BITSTATE",
1379         "       strcpy(ctd, \"-DBITSTATE \");",
1380         "#else",
1381         "       strcpy(ctd, \"\");",
1382         "#endif",
1383         "#ifdef BFS_PAR",
1384         "       strcat(ctd, \"-DBFS_PAR \");",
1385         "#endif",
1386         "#ifdef NOVSZ",
1387         "       strcat(ctd, \"-DNOVSZ \");",
1388         "#endif",
1389         "#ifdef RHASH",
1390         "       strcat(ctd, \"-DRHASH \");",
1391         "#else",
1392         "       #ifdef PERMUTED",
1393         "               strcat(ctd, \"-DPERMUTED \");",
1394         "       #endif",
1395         "#endif",
1396         "#ifdef P_REVERSE",
1397         "       strcat(ctd, \"-DP_REVERSE \");",
1398         "#endif",
1399         "#ifdef T_REVERSE",
1400         "       strcat(ctd, \"-DT_REVERSE \");",
1401         "#endif",
1402         "#ifdef T_RAND",
1403         "       #if T_RAND>0",
1404         "       sprintf(carg, \"-DT_RAND=%%d \", T_RAND);",
1405         "       strcat(ctd, carg);",
1406         "       #else",
1407         "       strcat(ctd, \"-DT_RAND \");",
1408         "       #endif",
1409         "#endif",
1410         "#ifdef P_RAND",
1411         "       #if P_RAND>0",
1412         "       sprintf(carg, \"-DP_RAND=%%d \", P_RAND);",
1413         "       strcat(ctd, carg);",
1414         "       #else",
1415         "       strcat(ctd, \"-DP_RAND \");",
1416         "       #endif",
1417         "#endif",
1418         "#ifdef BCS",
1419         "       sprintf(carg, \"-DBCS=%%d \", BCS);",
1420         "       strcat(ctd, carg);",
1421         "#endif",
1422         "#ifdef BFS",
1423         "       strcat(ctd, \"-DBFS \");",
1424         "#endif",
1425         "#ifdef MEMLIM",
1426         "       sprintf(carg, \"-DMEMLIM=%%d \", MEMLIM);",
1427         "       strcat(ctd, carg);",
1428         "#else",
1429         "#ifdef MEMCNT",
1430         "       sprintf(carg, \"-DMEMCNT=%%d \", MEMCNT);",
1431         "       strcat(ctd, carg);",
1432         "#endif",
1433         "#endif",
1434         "#ifdef NOCLAIM",
1435         "       strcat(ctd, \"-DNOCLAIM \");",
1436         "#endif",
1437         "#ifdef SAFETY",
1438         "       strcat(ctd, \"-DSAFETY \");",
1439         "#else",
1440                 "#ifdef NOFAIR",
1441                 "       strcat(ctd, \"-DNOFAIR \");",
1442                 "#else",
1443                         "#ifdef NFAIR",
1444                 "       if (NFAIR != 2)",
1445                 "       {       sprintf(carg, \"-DNFAIR=%%d \", NFAIR);",
1446                 "               strcat(ctd, carg);",
1447                 "       }",
1448                         "#endif",
1449                 "#endif",
1450         "#endif",
1451         "#ifdef NOREDUCE",
1452         "       strcat(ctd, \"-DNOREDUCE \");",
1453         "#else",
1454                 "#ifdef XUSAFE",
1455                 "       strcat(ctd, \"-DXUSAFE \");",
1456                 "#endif",
1457         "#endif",
1458         "#ifdef NP",
1459         "       strcat(ctd, \"-DNP \");",
1460         "#endif",
1461         "#ifdef PEG",
1462         "       strcat(ctd, \"-DPEG \");",
1463         "#endif",
1464         "#ifdef VAR_RANGES",
1465         "       strcat(ctd, \"-DVAR_RANGES \");",
1466         "#endif",
1467         "#ifdef HC",
1468         "       strcat(ctd, \"-DHC \");",
1469         "#endif",
1470         "#ifdef CHECK",
1471         "       strcat(ctd, \"-DCHECK \");",
1472         "#endif",
1473         "#ifdef CTL",
1474         "       strcat(ctd, \"-DCTL \");",
1475         "#endif",
1476         "#ifdef TRIX",
1477         "       strcat(ctd, \"-DTRIX \");",
1478         "#endif",
1479         "#ifdef NIBIS",
1480         "       strcat(ctd, \"-DNIBIS \");",
1481         "#endif",
1482         "#ifdef NOBOUNDCHECK",
1483         "       strcat(ctd, \"-DNOBOUNDCHECK \");",
1484         "#endif",
1485         "#ifdef NOSTUTTER",
1486         "       strcat(ctd, \"-DNOSTUTTER \");",
1487         "#endif",
1488         "#ifdef REACH",
1489         "       strcat(ctd, \"-DREACH \");",
1490         "#endif",
1491         "#ifdef PRINTF",
1492         "       strcat(ctd, \"-DPRINTF \");",
1493         "#endif",
1494         "#ifdef COLLAPSE",
1495         "       strcat(ctd, \"-DCOLLAPSE \");",
1496         "#endif",
1497         "#ifdef MA",
1498         "       sprintf(carg, \"-DMA=%%d \", MA);",
1499         "       strcat(ctd, carg);",
1500         "#endif",
1501         "#ifdef SVDUMP",
1502         "       strcat(ctd, \"-DSVDUMP \");",
1503         "#endif",
1504         "#if defined(VECTORSZ) && !defined(TRIX)",
1505         "       if (VECTORSZ != 1024)",
1506         "       {       sprintf(carg, \"-DVECTORSZ=%%d \", VECTORSZ);",
1507         "               strcat(ctd, carg);",
1508         "       }",
1509         "#endif",
1510         "#ifdef VERBOSE",
1511         "       strcat(ctd, \"-DVERBOSE \");",
1512         "#endif",
1513         "#ifdef CHECK",
1514         "       strcat(ctd, \"-DCHECK \");",
1515         "#endif",
1516         "#ifdef SDUMP",
1517         "       strcat(ctd, \"-DSDUMP \");",
1518         "#endif",
1519         "#if NCORE>1",
1520         "       sprintf(carg, \"-DNCORE=%%d \", NCORE);",
1521         "       strcat(ctd, carg);",
1522         "#endif",
1523         "#ifdef VMAX",
1524         "       if (VMAX != 256)",
1525         "       {       sprintf(carg, \"-DVMAX=%%d \", VMAX);",
1526         "               strcat(ctd, carg);",
1527         "       }",
1528         "#endif",
1529         "#ifdef PMAX",
1530         "       if (PMAX != 16)",
1531         "       {       sprintf(carg, \"-DPMAX=%%d \", PMAX);",
1532         "               strcat(ctd, carg);",
1533         "       }",
1534         "#endif",
1535         "#ifdef QMAX",
1536         "       if (QMAX != 16)",
1537         "       {       sprintf(carg, \"-DQMAX=%%d \", QMAX);",
1538         "               strcat(ctd, carg);",
1539         "       }",
1540         "#endif",
1541         "#ifdef SET_WQ_SIZE",
1542         "       sprintf(carg, \"-DSET_WQ_SIZE=%%d \", SET_WQ_SIZE);",
1543         "       strcat(ctd, carg);",
1544         "#endif",
1545         "       printf(\"Compiled as: cc -o pan %%span.c\\n\", ctd);",
1546         "}",
1547         0,
1548 };