sys/src/cmd/spin/pangen1.h

   1 /***** spin: pangen1.h *****/
   2
   3 /* Copyright (c) 1989-2005 by Lucent Technologies, Bell Laboratories.     */
   4 /* All Rights Reserved.  This software is for educational purposes only.  */
   5 /* No guarantee whatsoever is expressed or implied by the distribution of */
   6 /* this code.  Permission is given to distribute this code provided that  */
   7 /* this introductory message is not removed and no monies are exchanged.  */
   8 /* Software written by Gerard J. Holzmann.  For tool documentation see:   */
   9 /*             http://spinroot.com/                                       */
  10 /* Send all bug-reports and/or questions to: bugs@spinroot.com            */
  11
  12 static char *Code2a[] = { /* the tail of procedure run() */
  13         "#if defined(VERI) && !defined(NOREDUCE) && !defined(NP)",
  14         "       if (!state_tables",
  15         "#ifdef HAS_CODE",
  16         "       && !readtrail",
  17         "#endif",
  18         "       )",
  19         "       { printf(\"warning: for p.o. reduction to be valid \");",
  20         "         printf(\"the never claim must be stutter-invariant\\n\");",
  21         "         printf(\"(never claims generated from LTL \");",
  22         "         printf(\"formulae are stutter-invariant)\\n\");",
  23         "       }",
  24         "#endif",
  25         "       UnBlock;        /* disable rendez-vous */",
  26         "#ifdef BITSTATE",
  27 #ifndef POWOW
  28         "       if (udmem)",
  29         "       {       udmem *= 1024L*1024L;",
  30         "               SS = (uchar *) emalloc(udmem);",
  31         "               bstore = bstore_mod;",
  32         "       } else",
  33 #endif
  34         "       SS = (uchar *) emalloc(1L<<(ssize-3));",
  35         "#else",
  36         "       hinit();",
  37         "#endif",
  38         "#if defined(FULLSTACK) && defined(BITSTATE)",
  39         "       onstack_init();",
  40         "#endif",
  41         "#if defined(CNTRSTACK) && !defined(BFS)",
  42         "       LL = (uchar *) emalloc(1L<<(ssize-3));",
  43         "#endif",
  44         "       stack   = ( Stack *) emalloc(sizeof(Stack));",
  45         "       svtack  = (Svtack *) emalloc(sizeof(Svtack));",
  46         "       /* a place to point for Pptr of non-running procs: */",
  47         "       noptr   = (uchar *) emalloc(Maxbody * sizeof(char));",
  48         "#ifdef SVDUMP",
  49         "       if (vprefix > 0)",
  50         "               write(svfd, (uchar *) &vprefix, sizeof(int));",
  51         "#endif",
  52         "#ifdef VERI",
  53         "       Addproc(VERI);  /* never - pid = 0 */",
  54         "#endif",
  55         "       active_procs(); /* started after never */",
  56         "#ifdef EVENT_TRACE",
  57         "       now._event = start_event;",
  58         "       reached[EVENT_TRACE][start_event] = 1;",
  59         "#endif",
  60
  61         "#ifdef HAS_CODE",
  62         "       globinit();",
  63         "#endif",
  64         "#ifdef BITSTATE",
  65         "go_again:",
  66         "#endif",
  67         "       do_the_search();",
  68         "#ifdef BITSTATE",
  69         "       if (--Nrun > 0 && HASH_CONST[++HASH_NR])",
  70         "       {       printf(\"Run %%d:\\n\", HASH_NR);",
  71         "               wrap_stats();",
  72         "               printf(\"\\n\");",
  73         "               memset(SS, 0, 1L<<(ssize-3));",
  74                 "#if defined(CNTRSTACK)",
  75         "               memset(LL, 0, 1L<<(ssize-3));",
  76                 "#endif",
  77                 "#if defined(FULLSTACK)",
  78         "               memset((uchar *) S_Tab, 0, ",
  79         "               maxdepth*sizeof(struct H_el *));",
  80                 "#endif",
  81         "               nstates=nlinks=truncs=truncs2=ngrabs = 0;",
  82         "               nlost=nShadow=hcmp = 0;",
  83         "               Fa=Fh=Zh=Zn = 0;",
  84         "               PUT=PROBE=ZAPS=Ccheck=Cholds = 0;",
  85         "               goto go_again;",
  86         "       }",
  87         "#endif",
  88         "}",
  89         "#ifdef HAS_PROVIDED",
  90         "int provided(int, uchar, int, Trans *);",
  91         "#endif",
  92
  93 #ifndef PRINTF
  94         "int",
  95         "Printf(const char *fmt, ...)",
  96         "{      /* Make sure the args to Printf",
  97         "        * are always evaluated (e.g., they",
  98         "        * could contain a run stmnt)",
  99         "        * but do not generate the output",
 100         "        * during verification runs",
 101         "        * unless explicitly wanted",
 102         "        * If this fails on your system",
 103         "        * compile SPIN itself -DPRINTF",
 104         "        * and this code is not generated",
 105         "        */",
 106         "#ifdef HAS_CODE",
 107         "       if (readtrail)",
 108         "       {       va_list args;",
 109         "               va_start(args, fmt);",
 110         "               vprintf(fmt, args);",
 111         "               va_end(args);",
 112         "               return 1;",
 113         "       }",
 114         "#endif",
 115         "#ifdef PRINTF",
 116         "       va_list args;",
 117         "       va_start(args, fmt);",
 118         "       vprintf(fmt, args);",
 119         "       va_end(args);",
 120         "#endif",
 121         "       return 1;",
 122         "}",
 123 #endif
 124         "extern void printm(int);",
 125
 126         "#ifndef SC",
 127         "#define getframe(i)    &trail[i];",
 128         "#else",
 129         "static long HHH, DDD, hiwater;",
 130         "static long CNT1, CNT2;",
 131         "static int stackwrite;",
 132         "static int stackread;",
 133         "static Trail frameptr;",
 134         "Trail *",
 135         "getframe(int d)",
 136         "{",
 137         "       if (CNT1 == CNT2)",
 138         "               return &trail[d];",
 139         "",
 140         "       if (d >= (CNT1-CNT2)*DDD)",
 141         "               return &trail[d - (CNT1-CNT2)*DDD];",
 142         "",
 143         "       if (!stackread",
 144         "       &&  (stackread = open(stackfile, 0)) < 0)",
 145         "       {       printf(\"getframe: cannot open %%s\\n\", stackfile);",
 146         "               wrapup();",
 147         "       }",
 148         "       if (lseek(stackread, d* (off_t) sizeof(Trail), SEEK_SET) == -1",
 149         "       || read(stackread, &frameptr, sizeof(Trail)) != sizeof(Trail))",
 150         "       {       printf(\"getframe: frame read error\\n\");",
 151         "               wrapup();",
 152         "       }",
 153         "       return &frameptr;",
 154         "}",
 155         "#endif",
 156
 157         "#if !defined(SAFETY) && !defined(BITSTATE)",
 158         "#if !defined(FULLSTACK) || defined(MA)",
 159         "#define depth_of(x)    A_depth /* an estimate */",
 160         "#else",
 161         "int",
 162         "depth_of(struct H_el *s)",
 163         "{      Trail *t; int d;",
 164         "       for (d = 0; d <= A_depth; d++)",
 165         "       {       t = getframe(d);",
 166         "               if (s == t->ostate)",
 167         "                       return d;",
 168         "       }",
 169         "       printf(\"pan: cannot happen, depth_of\\n\");",
 170         "       return depthfound;",
 171         "}",
 172         "#endif",
 173         "#endif",
 174
 175         "void",
 176         "pan_exit(int val)",
 177         "{      if (signoff) printf(\"--end of output--\\n\");",
 178         "       exit(val);",
 179         "}",
 180
 181         "#ifdef HAS_CODE",
 182         "char *",
 183         "transmognify(char *s)",
 184         "{      char *v, *w;",
 185         "       static char buf[2][2048];",
 186         "       int i, toggle = 0;",
 187
 188         "       if (!s || strlen(s) > 2047) return s;",
 189         "       memset(buf[0], 0, 2048);",
 190         "       memset(buf[1], 0, 2048);",
 191         "       strcpy(buf[toggle], s);",
 192         "       while ((v = strstr(buf[toggle], \"{c_code\")))",        /* assign v */
 193         "       {       *v = '\\0'; v++;",
 194         "               strcpy(buf[1-toggle], buf[toggle]);",
 195         "               for (w = v; *w != '}' && *w != '\\0'; w++) /* skip */;",
 196         "               if (*w != '}') return s;",
 197         "               *w = '\\0'; w++;",
 198         "               for (i = 0; code_lookup[i].c; i++)",
 199         "                       if (strcmp(v, code_lookup[i].c) == 0",
 200         "                       &&  strlen(v) == strlen(code_lookup[i].c))",
 201         "                       {       if (strlen(buf[1-toggle])",
 202         "                                +  strlen(code_lookup[i].t)",
 203         "                                +  strlen(w) > 2047)",
 204         "                                       return s;",
 205         "                               strcat(buf[1-toggle], code_lookup[i].t);",
 206         "                               break;",
 207         "                       }",
 208         "               strcat(buf[1-toggle], w);",
 209         "               toggle = 1 - toggle;",
 210         "       }",
 211         "       buf[toggle][2047] = '\\0';",
 212         "       return buf[toggle];",
 213         "}",
 214         "#else",
 215         "char * transmognify(char *s) { return s; }",
 216         "#endif",
 217
 218         "#ifdef HAS_CODE",
 219         "void",
 220         "add_src_txt(int ot, int tt)",
 221         "{      Trans *t;",
 222         "       char *q;",
 223         "",
 224         "       for (t = trans[ot][tt]; t; t = t->nxt)",
 225         "       {       printf(\"\\t\\t\");",
 226
 227         "               q = transmognify(t->tp);",
 228         "               for ( ; q && *q; q++)",
 229         "                       if (*q == '\\n')",
 230         "                               printf(\"\\\\n\");",
 231         "                       else",
 232         "                               putchar(*q);",
 233         "               printf(\"\\n\");",
 234         "       }",
 235         "}",
 236         "void",
 237         "wrap_trail(void)",
 238         "{      static int wrap_in_progress = 0;",
 239         "       int i; short II;",
 240         "       P0 *z;",
 241         "",
 242         "       if (wrap_in_progress++) return;",
 243         "",
 244         "       printf(\"spin: trail ends after %%ld steps\\n\", depth);",
 245         "       if (onlyproc >= 0)",
 246         "       {       if (onlyproc >= now._nr_pr) pan_exit(0);",
 247         "               II = onlyproc;",
 248         "               z = (P0 *)pptr(II);",
 249         "               printf(\"%%3ld:\tproc %%d (%%s) \",",
 250         "                       depth, II, procname[z->_t]);",
 251         "               for (i = 0; src_all[i].src; i++)",
 252         "                       if (src_all[i].tp == (int) z->_t)",
 253         "                       {       printf(\" line %%3d\",",
 254         "                                       src_all[i].src[z->_p]);",
 255         "                               break;",
 256         "                       }",
 257         "               printf(\" (state %%2d)\", z->_p);",
 258         "               if (!stopstate[z->_t][z->_p])",
 259         "                       printf(\" (invalid end state)\");",
 260         "               printf(\"\\n\");",
 261         "               add_src_txt(z->_t, z->_p);",
 262         "               pan_exit(0);",
 263         "       }",
 264         "       printf(\"#processes %%d:\\n\", now._nr_pr);",
 265         "       if (depth < 0) depth = 0;",
 266         "       for (II = 0; II < now._nr_pr; II++)",
 267         "       {       z = (P0 *)pptr(II);",
 268         "               printf(\"%%3ld:\tproc %%d (%%s) \",",
 269         "                       depth, II, procname[z->_t]);",
 270         "               for (i = 0; src_all[i].src; i++)",
 271         "                       if (src_all[i].tp == (int) z->_t)",
 272         "                       {       printf(\" line %%3d\",",
 273         "                                       src_all[i].src[z->_p]);",
 274         "                               break;",
 275         "                       }",
 276         "               printf(\" (state %%2d)\", z->_p);",
 277         "               if (!stopstate[z->_t][z->_p])",
 278         "                       printf(\" (invalid end state)\");",
 279         "               printf(\"\\n\");",
 280         "               add_src_txt(z->_t, z->_p);",
 281         "       }",
 282         "       c_globals();",
 283         "       for (II = 0; II < now._nr_pr; II++)",
 284         "       {       z = (P0 *)pptr(II);",
 285         "               c_locals(II, z->_t);",
 286         "       }",
 287         "#ifdef ON_EXIT",
 288         "       ON_EXIT;",
 289         "#endif",
 290         "       pan_exit(0);",
 291         "}",
 292         "FILE *",
 293         "findtrail(void)",
 294         "{      FILE *fd;",
 295         "       char fnm[512], *q;",
 296         "       char MyFile[512];",
 297         "",
 298         "       strcpy(MyFile, TrailFile);",    /* avoid problem with non-writable strings */
 299         "",
 300         "       if (whichtrail)",
 301         "       {       sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);",
 302         "               fd = fopen(fnm, \"r\");",
 303         "               if (fd == NULL && (q = strchr(MyFile, \'.\')))",
 304         "               {       *q = \'\\0\';", /* e.g., strip .pml on original file */
 305         "                       sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);",
 306         "                       *q = \'.\';",
 307         "                       fd = fopen(fnm, \"r\");",
 308         "                       if (fd == NULL)",
 309         "                       {       printf(\"pan: cannot find %%s%%d.%%s or %%s\\n\", ",
 310         "                                       MyFile, whichtrail, tprefix, fnm);",
 311         "                               pan_exit(1);",
 312         "               }       }",
 313         "       } else",
 314         "       {       sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
 315         "               fd = fopen(fnm, \"r\");",
 316         "               if (fd == NULL && (q = strchr(MyFile, \'.\')))",
 317         "               {       *q = \'\\0\';", /* e.g., strip .pml on original file */
 318         "                       sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
 319         "                       *q = \'.\';",
 320         "                       fd = fopen(fnm, \"r\");",
 321         "                       if (fd == NULL)",
 322         "                       {       printf(\"pan: cannot find %%s.%%s or %%s\\n\", ",
 323         "                                       MyFile, tprefix, fnm);",
 324         "                               pan_exit(1);",
 325         "       }       }       }",
 326         "       if (fd == NULL)",
 327         "       {       printf(\"pan: cannot find trailfile %%s\\n\", fnm);",
 328         "               pan_exit(1);",
 329         "       }",
 330         "       return fd;",
 331         "}",
 332         "",
 333         "uchar do_transit(Trans *, short);",
 334         "",
 335         "void",
 336         "getrail(void)",
 337         "{      FILE *fd;",
 338         "       char *q;",
 339         "       int i, t_id, lastnever=-1; short II;",
 340         "       Trans *t;",
 341         "       P0 *z;",
 342         "",
 343         "       fd = findtrail();       /* exits if unsuccessful */",
 344         "       while (fscanf(fd, \"%%ld:%%d:%%d\\n\", &depth, &i, &t_id) == 3)",
 345         "       {       if (depth == -1)",
 346         "                       printf(\"<<<<<START OF CYCLE>>>>>\\n\");",
 347         "               if (depth < 0)",
 348         "                       continue;",
 349         "               if (i > now._nr_pr)",
 350         "               {       printf(\"pan: Error, proc %%d invalid pid \", i);",
 351         "                       printf(\"transition %%d\\n\", t_id);",
 352         "                       break;",
 353         "               }",
 354         "               II = i;",
 355         "",
 356         "               z = (P0 *)pptr(II);",
 357         "               for (t = trans[z->_t][z->_p]; t; t = t->nxt)",
 358         "                       if (t->t_id == t_id)",
 359         "                               break;",
 360         "               if (!t)",
 361         "               {       for (i = 0; i < NrStates[z->_t]; i++)",
 362         "                       {       t = trans[z->_t][i];",
 363         "                               if (t && t->t_id == t_id)",
 364         "                               {       printf(\"       Recovered at state %%d\\n\", i);",
 365         "                                       z->_p = i;",
 366         "                                       goto recovered;",
 367         "                       }       }",
 368         "                       printf(\"pan: Error, proc %%d type %%d state %%d: \",",
 369         "                               II, z->_t, z->_p);",
 370         "                       printf(\"transition %%d not found\\n\", t_id);",
 371         "                       for (t = trans[z->_t][z->_p]; t; t = t->nxt)",
 372         "                               printf(\"       t_id %%d -- case %%d, [%%s]\\n\",",
 373         "                                       t->t_id, t->forw, t->tp);",
 374         "                       break; /* pan_exit(1); */",
 375         "               }",
 376         "recovered:",
 377         "               q = transmognify(t->tp);",
 378         "               if (gui) simvals[0] = \'\\0\';",
 379
 380         "               this = pptr(II);",
 381         "               trpt->tau |= 1;",       /* timeout always possible */
 382         "               if (!do_transit(t, II))",
 383         "               {       if (onlyproc >= 0 && II != onlyproc)",
 384         "                               goto moveon;",
 385         "                       printf(\"pan: error, next transition UNEXECUTABLE on replay\\n\");",
 386         "                       printf(\"     most likely causes: missing c_track statements\\n\");",
 387         "                       printf(\"       or illegal side-effects in c_expr statements\\n\");",
 388         "               }",
 389
 390         "               if (onlyproc >= 0 && II != onlyproc)",
 391         "                       goto moveon;",
 392
 393         "               if (verbose)",
 394         "               {       printf(\"depth: %%3ld proc: %%3d trans: %%3d (%%d procs)  \",",
 395         "                               depth, II, t_id, now._nr_pr);",
 396         "                       printf(\"forw=%%3d [%%s]\\n\", t->forw, q);",
 397         "",
 398         "                       c_globals();",
 399         "                       for (i = 0; i < now._nr_pr; i++)",
 400         "                       {       c_locals(i, ((P0 *)pptr(i))->_t);",
 401         "                       }",
 402         "               } else",
 403         "               if (strcmp(procname[z->_t], \":never:\") == 0)",
 404         "               {       if (lastnever != (int) z->_p)",
 405         "                       {       for (i = 0; src_all[i].src; i++)",
 406         "                                       if (src_all[i].tp == (int) z->_t)",
 407         "                                       {       printf(\"MSC: ~G %%d\\n\",",
 408         "                                                       src_all[i].src[z->_p]);",
 409         "                                               break;",
 410         "                                       }",
 411         "                               if (!src_all[i].src)",
 412         "                                       printf(\"MSC: ~R %%d\\n\", z->_p);",
 413         "                       }",
 414         "                       lastnever = z->_p;",
 415         "                       goto sameas;",
 416         "               } else",
 417         "               if (strcmp(procname[z->_t], \":np_:\") != 0)",
 418         "               {",
 419         "sameas:                if (no_rck) goto moveon;",
 420         "                       if (coltrace)",
 421         "                       {       printf(\"%%ld: \", depth);",
 422         "                               for (i = 0; i < II; i++)",
 423         "                                       printf(\"\\t\\t\");",
 424         "                               printf(\"%%s(%%d):\", procname[z->_t], II);",
 425         "                               printf(\"[%%s]\\n\", q?q:\"\");",
 426         "                       } else if (!silent)",
 427         "                       {       if (strlen(simvals) > 0) {",
 428         "                               printf(\"%%3ld: proc %%2d (%%s)\", ",
 429         "                                       depth, II, procname[z->_t]);",
 430         "                               for (i = 0; src_all[i].src; i++)",
 431         "                                       if (src_all[i].tp == (int) z->_t)",
 432         "                                       {       printf(\" line %%3d \\\"pan_in\\\" \",",
 433         "                                                       src_all[i].src[z->_p]);",
 434         "                                               break;",
 435         "                                       }",
 436         "                               printf(\"(state %%d)\t[values: %%s]\\n\", z->_p, simvals);",
 437         "                               }",
 438         "                               printf(\"%%3ld: proc %%2d (%%s)\", ",
 439         "                                       depth, II, procname[z->_t]);",
 440         "                               for (i = 0; src_all[i].src; i++)",
 441         "                                       if (src_all[i].tp == (int) z->_t)",
 442         "                                       {       printf(\" line %%3d \\\"pan_in\\\" \",",
 443         "                                                       src_all[i].src[z->_p]);",
 444         "                                               break;",
 445         "                                       }",
 446         "                               printf(\"(state %%d)\t[%%s]\\n\", z->_p, q?q:\"\");",
 447         "                               printf(\"\\n\");",
 448         "               }       }",
 449         "moveon:        z->_p = t->st;",
 450         "       }",
 451         "       wrap_trail();",
 452         "}",
 453         "#endif",
 454         "int",
 455         "f_pid(int pt)",
 456         "{      int i;",
 457         "       P0 *z;",
 458         "       for (i = 0; i < now._nr_pr; i++)",
 459         "       {       z = (P0 *)pptr(i);",
 460         "               if (z->_t == (unsigned) pt)",
 461         "                       return BASE+z->_pid;",
 462         "       }",
 463         "       return -1;",
 464         "}",
 465         "#ifdef VERI",
 466         "void check_claim(int);",
 467         "#endif",
 468         "",
 469         "#ifdef BITSTATE",
 470 #ifndef POWOW
 471         "int",
 472         "bstore_mod(char *v, int n)     /* hasharray size not a power of two */",
 473         "{      unsigned long x, y;",
 474         "       unsigned int i = 1;",
 475         "",
 476         "       d_hash((uchar *) v, n); /* sets j3, j4, K1, K2 */",
 477         "       x = K2; y = j3;",
 478         "       for (;;)",
 479         "       {       if (!(SS[x%%udmem]&(1<<y))) break;",    /* take the hit in speed */
 480         "               if (i == hfns) {",
 481                                 "#ifdef DEBUG",
 482         "                       printf(\"Old bitstate\\n\");",
 483                                 "#endif",
 484         "                       return 1;",
 485         "               }",
 486         "               x = (x + K1 + i);",     /* no mask, using mod */
 487         "               y = (y + j4) & 7;",
 488         "               i++;",
 489         "       }",
 490                 "#ifdef RANDSTOR",
 491         "       if (rand()%%100 > RANDSTOR) return 0;",
 492                 "#endif",
 493         "       for (;;)",
 494         "       {       SS[x%%udmem] |= (1<<y);",
 495         "               if (i == hfns) break;", /* done */
 496         "               x = (x + K1 + i);",     /* no mask */
 497         "               y = (y + j4) & 7;",
 498         "               i++;",
 499         "       }",
 500                 "#ifdef DEBUG",
 501         "       printf(\"New bitstate\\n\");",
 502                 "#endif",
 503         "       if (now._a_t&1)",
 504         "       {       nShadow++;",
 505         "       }",
 506         "       return 0;",
 507         "}",
 508 #endif
 509         "int",
 510         "bstore_reg(char *v, int n)     /* extended hashing, Peter Dillinger, 2004 */",
 511         "{      unsigned long x, y;",
 512         "       unsigned int i = 1;",
 513         "",
 514         "       d_hash((uchar *) v, n); /* sets j1-j4 */",
 515         "       x = j2; y = j3;",
 516         "       for (;;)",
 517         "       {       if (!(SS[x]&(1<<y))) break;",   /* at least one bit not set */
 518         "               if (i == hfns) {",
 519                                 "#ifdef DEBUG",
 520         "                       printf(\"Old bitstate\\n\");",
 521                                 "#endif",
 522         "                       return 1;",
 523         "               }",
 524         "               x = (x + j1 + i) & nmask;",
 525         "               y = (y + j4) & 7;",
 526         "               i++;",
 527         "       }",
 528                 "#ifdef RANDSTOR",
 529         "       if (rand()%%100 > RANDSTOR) return 0;",
 530                 "#endif",
 531         "       for (;;)",
 532         "       {       SS[x] |= (1<<y);",
 533         "               if (i == hfns) break;",         /* done */
 534         "               x = (x + j1 + i) & nmask;",
 535         "               y = (y + j4) & 7;",
 536         "               i++;",
 537         "       }",
 538                 "#ifdef DEBUG",
 539         "       printf(\"New bitstate\\n\");",
 540                 "#endif",
 541         "       if (now._a_t&1)",
 542         "       {       nShadow++;",
 543         "       }",
 544         "       return 0;",
 545         "}",
 546         "#endif",
 547         "unsigned long TMODE = 0666; /* file permission bits for trail files */",
 548         "",
 549         "int trcnt=1;",
 550         "char snap[64], fnm[512];",
 551         "",
 552         "int",
 553         "make_trail(void)",
 554         "{      int fd;",
 555         "       char *q;",
 556         "       char MyFile[512];",
 557         "",
 558         "       q = strrchr(TrailFile, \'/\');",
 559         "       if (q == NULL) q = TrailFile; else q++;",
 560         "       strcpy(MyFile, q); /* TrailFile is not a writable string */",
 561         "",
 562         "       if (iterative == 0 && Nr_Trails++ > 0)",
 563         "               sprintf(fnm, \"%%s%%d.%%s\",",
 564         "                       MyFile, Nr_Trails-1, tprefix);",
 565         "       else",
 566         "               sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
 567         "",
 568         "       if ((fd = creat(fnm, TMODE)) < 0)",
 569         "       {       if ((q = strchr(MyFile, \'.\')))",
 570         "               {       *q = \'\\0\';",         /* strip .pml */
 571         "                       if (iterative == 0 && Nr_Trails-1 > 0)",
 572         "                               sprintf(fnm, \"%%s%%d.%%s\",",
 573         "                                       MyFile, Nr_Trails-1, tprefix);",
 574         "                       else",
 575         "                               sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
 576         "                       *q = \'.\';",
 577         "                       fd = creat(fnm, TMODE);",
 578         "       }       }",
 579         "       if (fd < 0)",
 580         "       {       printf(\"pan: cannot create %%s\\n\", fnm);",
 581         "               perror(\"cause\");",
 582         "       } else",
 583         "       {       printf(\"pan: wrote %%s\\n\", fnm);",
 584         "       }",
 585         "       return fd;",
 586         "}",
 587         0
 588 };
 589
 590 static char *Code2b[] = {       /* breadth-first search option */
 591         "#ifdef BFS",
 592         "#define Q_PROVISO",
 593         "#ifndef INLINE_REV",
 594         "#define INLINE_REV",
 595         "#endif",
 596         "",
 597         "typedef struct SV_Hold {",
 598         "       State *sv;",
 599         "       int  sz;",
 600         "       struct SV_Hold *nxt;",
 601         "} SV_Hold;",
 602         "",
 603         "typedef struct EV_Hold {",
 604         "       char *sv;",     /* Mask */
 605         "       int  sz;",      /* vsize */
 606         "       int nrpr;",
 607         "       int nrqs;",
 608         "#if VECTORSZ>32000",
 609         "       int *po;",
 610         "#else",
 611         "       short *po;",
 612         "#endif",
 613         "       int *qo;",
 614         "       uchar *ps, *qs;",
 615         "       struct EV_Hold *nxt;",
 616         "} EV_Hold;",
 617         "",
 618         "typedef struct BFS_Trail {",
 619         "       Trail   *frame;",
 620         "       SV_Hold *onow;",
 621         "       EV_Hold *omask;",
 622         "#ifdef Q_PROVISO",
 623         "       struct H_el *lstate;",
 624         "#endif",
 625         "       short boq;",
 626         "       struct BFS_Trail *nxt;",
 627         "} BFS_Trail;",
 628         "",
 629         "BFS_Trail *bfs_trail, *bfs_bot, *bfs_free;",
 630         "",
 631         "SV_Hold *svhold, *svfree;",
 632         "",
 633         "uchar do_reverse(Trans *, short, uchar);",
 634         "void snapshot(void);",
 635         "",
 636         "SV_Hold *",
 637         "getsv(int n)",
 638         "{      SV_Hold *h = (SV_Hold *) 0, *oh;",
 639         "",
 640         "       oh = (SV_Hold *) 0;",
 641         "       for (h = svfree; h; oh = h, h = h->nxt)",
 642         "       {       if (n == h->sz)",
 643         "               {       if (!oh)",
 644         "                               svfree = h->nxt;",
 645         "                       else",
 646         "                               oh->nxt = h->nxt;",
 647         "                       h->nxt = (SV_Hold *) 0;",
 648         "                       break;",
 649         "               }",
 650         "               if (n < h->sz)",
 651         "               {       h = (SV_Hold *) 0;",
 652         "                       break;",
 653         "               }",
 654         "               /* else continue */",
 655         "       }",
 656         "",
 657         "       if (!h)",
 658         "       {       h = (SV_Hold *) emalloc(sizeof(SV_Hold));",
 659         "               h->sz = n;",
 660         "               h->sv = (State *) emalloc(sizeof(State) - VECTORSZ + n);",
 661         "       }",
 662         "       return h;",
 663         "}",
 664         "",
 665         "EV_Hold *",
 666         "getsv_mask(int n)",
 667         "{      EV_Hold *h;",
 668         "       static EV_Hold *kept = (EV_Hold *) 0;",
 669         "",
 670         "       for (h = kept; h; h = h->nxt)",
 671         "               if (n == h->sz",
 672         "               &&  (memcmp((char *) Mask, (char *) h->sv, n) == 0)",
 673         "               &&  (now._nr_pr == h->nrpr)",
 674         "               &&  (now._nr_qs == h->nrqs)",
 675         "#if VECTORSZ>32000",
 676         "               &&  (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(int)) == 0)",
 677         "               &&  (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(int)) == 0)",
 678         "#else",
 679         "               &&  (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(short)) == 0)",
 680         "               &&  (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(short)) == 0)",
 681         "#endif",
 682         "               &&  (memcmp((char *) proc_skip,   (char *) h->ps, now._nr_pr * sizeof(uchar)) == 0)",
 683         "               &&  (memcmp((char *) q_skip,   (char *) h->qs, now._nr_qs * sizeof(uchar)) == 0))",
 684         "                       break;",
 685         "       if (!h)",
 686         "       {       h = (EV_Hold *) emalloc(sizeof(EV_Hold));",
 687         "               h->sz = n;",
 688         "               h->nrpr = now._nr_pr;",
 689         "               h->nrqs = now._nr_qs;",
 690         "",
 691         "               h->sv = (char *) emalloc(n * sizeof(char));",
 692         "               memcpy((char *) h->sv, (char *) Mask, n);",
 693         "",
 694         "               if (now._nr_pr > 0)",
 695         "               {       h->po = (int *) emalloc(now._nr_pr * sizeof(int));",
 696         "                       h->ps = (int *) emalloc(now._nr_pr * sizeof(int));",
 697         "#if VECTORSZ>32000",
 698         "                       memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(int));",
 699         "#else",
 700         "                       memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(short));",
 701         "#endif",
 702         "                       memcpy((char *) h->ps, (char *) proc_skip,   now._nr_pr * sizeof(uchar));",
 703         "               }",
 704         "               if (now._nr_qs > 0)",
 705         "               {       h->qo = (int *) emalloc(now._nr_qs * sizeof(int));",
 706         "                       h->qs = (int *) emalloc(now._nr_qs * sizeof(int));",
 707         "#if VECTORSZ>32000",
 708         "                       memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(int));",
 709         "#else",
 710         "                       memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(short));",
 711         "#endif",
 712         "                       memcpy((char *) h->qs, (char *) q_skip,   now._nr_qs * sizeof(uchar));",
 713         "               }",
 714         "",
 715         "               h->nxt = kept;",
 716         "               kept = h;",
 717         "       }",
 718         "       return h;",
 719         "}",
 720         "",
 721         "void",
 722         "freesv(SV_Hold *p)",
 723         "{      SV_Hold *h, *oh;",
 724         "",
 725         "       oh = (SV_Hold *) 0;",
 726         "       for (h = svfree; h; oh = h, h = h->nxt)",
 727         "               if (h->sz >= p->sz)",
 728         "                       break;",
 729         "",
 730         "       if (!oh)",
 731         "       {       p->nxt = svfree;",
 732         "               svfree = p;",
 733         "       } else",
 734         "       {       p->nxt = h;",
 735         "               oh->nxt = p;",
 736         "       }",
 737         "}",
 738         "",
 739         "BFS_Trail *",
 740         "get_bfs_frame(void)",
 741         "{      BFS_Trail *t;",
 742         "",
 743         "       if (bfs_free)",
 744         "       {       t = bfs_free;",
 745         "               bfs_free = bfs_free->nxt;",
 746         "               t->nxt = (BFS_Trail *) 0;",
 747         "       } else",
 748         "       {       t = (BFS_Trail *) emalloc(sizeof(BFS_Trail));",
 749         "       }",
 750         "       t->frame = (Trail *) emalloc(sizeof(Trail));", /* always new */
 751         "       return t;",
 752         "}",
 753         "",
 754         "void",
 755         "push_bfs(Trail *f, int d)",
 756         "{      BFS_Trail *t;",
 757         "",
 758         "       t = get_bfs_frame();",
 759         "       memcpy((char *)t->frame, (char *)f, sizeof(Trail));",
 760         "       t->frame->o_tt = d;     /* depth */",
 761         "",
 762         "       t->boq = boq;",
 763         "       t->onow = getsv(vsize);",
 764         "       memcpy((char *)t->onow->sv, (char *)&now, vsize);",
 765         "       t->omask = getsv_mask(vsize);",
 766         "#if defined(FULLSTACK) && defined(Q_PROVISO)",
 767         "       t->lstate = Lstate;",
 768         "#endif",
 769         "       if (!bfs_bot)",
 770         "       {       bfs_bot = bfs_trail = t;",
 771         "       } else",
 772         "       {       bfs_bot->nxt = t;",
 773         "               bfs_bot = t;",
 774         "       }",
 775         "#ifdef CHECK",
 776         "       printf(\"PUSH %%u (%%d)\\n\", t->frame, d);",
 777         "#endif",
 778         "}",
 779         "",
 780         "Trail *",
 781         "pop_bfs(void)",
 782         "{      BFS_Trail *t;",
 783         "",
 784         "       if (!bfs_trail)",
 785         "               return (Trail *) 0;",
 786         "",
 787         "       t = bfs_trail;",
 788         "       bfs_trail = t->nxt;",
 789         "       if (!bfs_trail)",
 790         "               bfs_bot = (BFS_Trail *) 0;",
 791         "#if defined(Q_PROVISO) && !defined(BITSTATE) && !defined(NOREDUCE)",
 792         "       if (t->lstate) t->lstate->tagged = 0;",
 793         "#endif",
 794         "",
 795         "       t->nxt = bfs_free;",
 796         "       bfs_free = t;",
 797         "",
 798         "       vsize = t->onow->sz;",
 799         "       boq = t->boq;",
 800         "",
 801         "       memcpy((uchar *) &now, (uchar *) t->onow->sv, vsize);",
 802         "       memcpy((uchar *) Mask, (uchar *) t->omask->sv, vsize);",
 803
 804         "       if (now._nr_pr > 0)",
 805         "#if VECTORSZ>32000",
 806         "       {       memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(int));",
 807         "#else",
 808         "       {       memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(short));",
 809         "#endif",
 810         "               memcpy((char *)proc_skip,   (char *)t->omask->ps, now._nr_pr * sizeof(uchar));",
 811         "       }",
 812         "       if (now._nr_qs > 0)",
 813         "#if VECTORSZ>32000",
 814         "       {       memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(int));",
 815         "#else",
 816         "       {       memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(short));",
 817         "#endif",
 818         "               memcpy((uchar *)q_skip,   (uchar *)t->omask->qs, now._nr_qs * sizeof(uchar));",
 819         "       }",
 820
 821         "       freesv(t->onow);        /* omask not freed */",
 822         "#ifdef CHECK",
 823         "       printf(\"POP %%u (%%d)\\n\", t->frame, t->frame->o_tt);",
 824         "#endif",
 825         "       return t->frame;",
 826         "}",
 827         "",
 828         "void",
 829         "store_state(Trail *ntrpt, int shortcut, short oboq)",
 830         "{",
 831         "#ifdef VERI",
 832         "       Trans *t2 = (Trans *) 0;",
 833         "       uchar ot; int tt, E_state;",
 834         "       uchar o_opm = trpt->o_pm, *othis = this;",
 835         "",
 836         "       if (shortcut)",
 837         "       {",
 838         "#ifdef VERBOSE",
 839         "               printf(\"claim: shortcut\\n\");",
 840         "#endif",
 841         "               goto store_it;  /* no claim move */",
 842         "       }",
 843         "",
 844         "       this  = (((uchar *)&now)+proc_offset[0]); /* 0 = never claim */",
 845         "       trpt->o_pm = 0;",       /* to interpret else in never claim */
 846         "",
 847         "       tt    = (int)   ((P0 *)this)->_p;",
 848         "       ot    = (uchar) ((P0 *)this)->_t;",
 849         "",
 850                 "#ifdef HAS_UNLESS",
 851         "       E_state = 0;",
 852                 "#endif",
 853         "       for (t2 = trans[ot][tt]; t2; t2 = t2?t2->nxt:(Trans *)0)",
 854         "       {",
 855                 "#ifdef HAS_UNLESS",
 856         "               if (E_state > 0",
 857         "               &&  E_state != t2->e_trans)",
 858         "                       break;",
 859                 "#endif",
 860         "               if (do_transit(t2, 0))",
 861         "               {",
 862                 "#ifdef VERBOSE",
 863         "                       if (!reached[ot][t2->st])",
 864         "                       printf(\"depth: %%d -- claim move from %%d -> %%d\\n\",",
 865         "                               trpt->o_tt, ((P0 *)this)->_p, t2->st);",
 866                 "#endif",
 867                 "#ifdef HAS_UNLESS",
 868         "                       E_state = t2->e_trans;",
 869                 "#endif",
 870         "                       if (t2->st > 0)",
 871         "                       {       ((P0 *)this)->_p = t2->st;",
 872         "                               reached[ot][t2->st] = 1;",
 873                 "#ifndef NOCLAIM",
 874         "                               check_claim(t2->st);",
 875                 "#endif",
 876         "                       }",
 877         "                       if (now._nr_pr == 0)    /* claim terminated */",
 878         "                               uerror(\"end state in claim reached\");",
 879         "",
 880                 "#ifdef PEG",
 881         "                       peg[t2->forw]++;",
 882                 "#endif",
 883         "                       trpt->o_pm |= 1;",
 884         "                       if (t2->atom&2)",       /* atomic in claim */
 885         "                       Uerror(\"atomic in claim not supported in BFS mode\");",
 886         "store_it:",
 887         "",
 888         "#endif",       /* VERI */
 889         "",
 890         "#ifdef BITSTATE",
 891         "                       if (!bstore((char *)&now, vsize))",
 892         "#else",
 893                 "#ifdef MA",
 894         "                       if (!gstore((char *)&now, vsize, 0))",
 895                 "#else",
 896         "                       if (!hstore((char *)&now, vsize))",
 897                 "#endif",
 898         "#endif",
 899         "                       {       nstates++;",
 900         "#ifndef NOREDUCE",
 901         "                               trpt->tau |= 64;", /* succ definitely outside stack */
 902         "#endif",
 903         "#if SYNC",
 904         "                               if (boq != -1)",
 905         "                                       midrv++;",
 906         "                               else if (oboq != -1)",
 907         "                               {       Trail *x;",
 908         "                                       x = (Trail *) trpt->ostate; /* pre-rv state */",
 909         "                                       if (x) x->o_pm |= 4; /* mark success */",
 910         "                               }",
 911         "#endif",
 912         "                               push_bfs(ntrpt, trpt->o_tt+1);",
 913         "                       } else",
 914         "                       {       truncs++;",
 915
 916         "#if !defined(NOREDUCE) && defined(FULLSTACK) && defined(Q_PROVISO)",
 917                 "#if !defined(QLIST) && !defined(BITSTATE)",
 918         "                               if (Lstate && Lstate->tagged) trpt->tau |= 64;",
 919                 "#else",
 920         "                               if (trpt->tau&32)",
 921         "                               {  BFS_Trail *tprov;",
 922         "                                  for (tprov = bfs_trail; tprov; tprov = tprov->nxt)",
 923         "                                       if (!memcmp((uchar *)&now, (uchar *)tprov->onow->sv, vsize))",
 924         "                                       {       trpt->tau |= 64;",
 925         "                                               break;  /* state is in queue */",
 926         "                               }       }",
 927                 "#endif",
 928         "#endif",
 929         "                       }",
 930         "#ifdef VERI",
 931         "                       ((P0 *)this)->_p = tt;  /* reset claim */",
 932         "                       if (t2)",
 933         "                               do_reverse(t2, 0, 0);",
 934         "                       else",
 935         "                               break;",
 936         "       }       }",
 937         "       this = othis;",
 938         "       trpt->o_pm = o_opm;",
 939         "#endif",
 940         "}",
 941         "",
 942         "Trail *ntrpt;",        /* 4.2.8 */
 943         "",
 944         "void",
 945         "bfs(void)",
 946         "{      Trans *t; Trail *otrpt, *x;",
 947         "       uchar _n, _m, ot, nps = 0;",
 948         "       int tt, E_state;",
 949         "       short II, From = (short) (now._nr_pr-1), To = BASE;",
 950         "       short oboq = boq;",
 951         "",
 952         "       ntrpt = (Trail *) emalloc(sizeof(Trail));",
 953         "       trpt->ostate = (struct H_el *) 0;",
 954         "       trpt->tau = 0;",
 955         "",
 956         "       trpt->o_tt = -1;",
 957         "       store_state(ntrpt, 0, oboq);    /* initial state */",
 958         "",
 959         "       while ((otrpt = pop_bfs()))     /* also restores now */",
 960         "       {       memcpy((char *) trpt, (char *) otrpt, sizeof(Trail));",
 961         "#if defined(C_States) && (HAS_TRACK==1)",
 962         "               c_revert((uchar *) &(now.c_state[0]));",
 963         "#endif",
 964         "               if (trpt->o_pm & 4)",
 965         "               {",
 966         "#ifdef VERBOSE",
 967         "                       printf(\"Revisit of atomic not needed (%%d)\\n\",",
 968         "                               trpt->o_pm);",  /* at least 1 rv succeeded */
 969         "#endif",
 970         "                       continue;",
 971         "               }",
 972         "#ifndef NOREDUCE",
 973         "               nps = 0;",
 974         "#endif",
 975         "               if (trpt->o_pm == 8)",
 976         "               {       revrv++;",
 977         "                       if (trpt->tau&8)",
 978         "                       {",
 979                 "#ifdef VERBOSE",
 980         "                               printf(\"Break atomic (pm:%%d,tau:%%d)\\n\",",
 981         "                                       trpt->o_pm, trpt->tau);",
 982                 "#endif",
 983         "                               trpt->tau &= ~8;",
 984         "                       }",
 985         "#ifndef NOREDUCE",
 986         "                       else if (trpt->tau&32)",        /* was a preselected move */
 987         "                       {",
 988                 "#ifdef VERBOSE",
 989         "                               printf(\"Void preselection (pm:%%d,tau:%%d)\\n\",",
 990         "                                       trpt->o_pm, trpt->tau);",
 991                 "#endif",
 992         "                               trpt->tau &= ~32;",
 993         "                               nps = 1; /* no preselection in repeat */",
 994         "                       }",
 995         "#endif",
 996         "               }",
 997         "               trpt->o_pm &= ~(4|8);",
 998         "               if (trpt->o_tt > mreached)",
 999         "               {       mreached = trpt->o_tt;",
1000         "                       if (mreached%%10 == 0)",
1001         "                       {       printf(\"Depth= %%7d States= %%7g \", mreached, nstates);",
1002         "                               printf(\"Transitions= %%7g \", nstates+truncs);",
1003         "#ifdef MA",
1004         "                               printf(\"Nodes= %%7d \", nr_states);",
1005         "#endif",
1006         "                               printf(\"Memory= %%-6.3f\\n\", memcnt/1000000.);",
1007         "                               fflush(stdout);",
1008         "               }       }",
1009         "               depth = trpt->o_tt;",
1010
1011         "               if (depth >= maxdepth)",
1012         "               {",
1013         "#if SYNC",
1014         "                       Trail *x;",
1015         "                       if (boq != -1)",
1016         "                       {       x = (Trail *) trpt->ostate;",
1017         "                               if (x) x->o_pm |= 4; /* not failing */",
1018         "                       }",
1019         "#endif",
1020         "                       truncs++;",
1021         "                       if (!warned)",
1022         "                       {       warned = 1;",
1023         "                               printf(\"error: max search depth too small\\n\");",
1024         "                       }",
1025         "                       if (bounded)",
1026         "                               uerror(\"depth limit reached\");",
1027         "                       continue;",
1028         "               }",
1029
1030 /* PO */
1031         "#ifndef NOREDUCE",
1032         "               if (boq == -1 && !(trpt->tau&8) && nps == 0)",
1033         "               for (II = now._nr_pr-1; II >= BASE; II -= 1)",
1034         "               {",
1035         "Pickup:                        this = pptr(II);",
1036         "                       tt = (int) ((P0 *)this)->_p;",
1037         "                       ot = (uchar) ((P0 *)this)->_t;",
1038         "                       if (trans[ot][tt]->atom & 8)",  /* safe */
1039         "                       {       t = trans[ot][tt];",
1040         "                               if (t->qu[0] != 0)",
1041         "                               {       Ccheck++;",
1042         "                                       if (!q_cond(II, t))",
1043         "                                               continue;",
1044         "                                       Cholds++;",
1045         "                               }",
1046         "                               From = To = II;",
1047         "                               trpt->tau |= 32; /* preselect marker */",
1048                 "#ifdef DEBUG",
1049         "                               printf(\"%%3d: proc %%d PreSelected (tau=%%d)\\n\", ",
1050         "                                       depth, II, trpt->tau);",
1051                 "#endif",
1052         "                               goto MainLoop;",
1053         "               }       }",
1054         "               trpt->tau &= ~32;",     /* not preselected */
1055         "#endif",
1056 /* PO */
1057         "Repeat:",
1058         "               if (trpt->tau&8)                /* atomic */",
1059         "               {       From = To = (short ) trpt->pr;",
1060         "                       nlinks++;",
1061         "               } else",
1062         "               {       From = now._nr_pr-1;",
1063         "                       To = BASE;",
1064         "               }",
1065         "MainLoop:",
1066         "               _n = _m = 0;",
1067         "               for (II = From; II >= To; II -= 1)",
1068         "               {",
1069         "                       this = (((uchar *)&now)+proc_offset[II]);",
1070         "                       tt = (int) ((P0 *)this)->_p;",
1071         "                       ot = (uchar) ((P0 *)this)->_t;",
1072         "#if SYNC",
1073         "                       /* no rendezvous with same proc */",
1074         "                       if (boq != -1 && trpt->pr == II) continue;",
1075         "#endif",
1076         "                       ntrpt->pr = (uchar) II;",
1077         "                       ntrpt->st = tt; ",
1078         "                       trpt->o_pm &= ~1;               /* no move yet */",
1079         "#ifdef EVENT_TRACE",
1080         "                       trpt->o_event = now._event;",
1081         "#endif",
1082         "#ifdef HAS_PROVIDED",
1083         "                       if (!provided(II, ot, tt, t)) continue;",
1084         "#endif",
1085         "#ifdef HAS_UNLESS",
1086         "                       E_state = 0;",
1087         "#endif",
1088         "                       for (t = trans[ot][tt]; t; t = t->nxt)",
1089         "                       {",
1090         "#ifdef HAS_UNLESS",
1091         "                               if (E_state > 0",
1092         "                               &&  E_state != t->e_trans)",
1093         "                                       break;",
1094         "#endif",
1095         "                               ntrpt->o_t = t;",
1096         "",
1097         "                               oboq = boq;",
1098         "",
1099         "                               if (!(_m = do_transit(t, II)))",
1100         "                                       continue;",
1101         "",
1102         "                               trpt->o_pm |= 1;        /* we moved */",
1103         "                               (trpt+1)->o_m = _m;     /* for unsend */",
1104                 "#ifdef PEG",
1105         "                               peg[t->forw]++;",
1106                 "#endif",
1107         "#ifdef CHECK",
1108         "                               printf(\"%%3d: proc %%d exec %%d, \",",
1109         "                                       depth, II, t->forw);",
1110         "                               printf(\"%%d to %%d, %%s %%s %%s\",",
1111         "                                       tt, t->st, t->tp,",
1112         "                                       (t->atom&2)?\"atomic\":\"\",",
1113         "                                       (boq != -1)?\"rendez-vous\":\"\");",
1114                 "#ifdef HAS_UNLESS",
1115         "                               if (t->e_trans)",
1116         "                                       printf(\" (escapes to state %%d)\", t->st);",
1117                 "#endif",
1118         "                               printf(\" %%saccepting [tau=%%d]\\n\",",
1119         "                                       (trpt->o_pm&2)?\"\":\"non-\", trpt->tau);",
1120         "#endif",
1121         "#ifdef HAS_UNLESS",
1122         "                               E_state = t->e_trans;",
1123                 "#if SYNC>0",
1124         "                               if (t->e_trans > 0 && (boq != -1 /* || oboq != -1 */))",
1125         "                               { fprintf(efd, \"error:\tthe use of rendezvous stmnt in the escape clause\\n\");",
1126         "                                 fprintf(efd, \"\tof an unless stmnt is not compatible with -DBFS\\n\");",
1127         "                                 pan_exit(1);",
1128         "                               }",
1129                 "#endif",
1130         "#endif",
1131         "                               if (t->st > 0) ((P0 *)this)->_p = t->st;",
1132         "",
1133         "       /* ptr to pred: */      ntrpt->ostate = (struct H_el *) otrpt;",
1134         "                               ntrpt->st = tt;",
1135         "                               if (boq == -1 && (t->atom&2))   /* atomic */",
1136         "                                       ntrpt->tau = 8; /* record for next move */",
1137         "                               else",
1138         "                                       ntrpt->tau = 0;",
1139         "",
1140         "                               store_state(ntrpt, (boq != -1 || (t->atom&2)), oboq);",
1141         "#ifdef EVENT_TRACE",
1142         "                               now._event = trpt->o_event;",
1143         "#endif",
1144         "",
1145         "                               /* undo move and continue */",
1146         "                               trpt++; /* this is where ovals and ipt are set */",
1147         "                               do_reverse(t, II, _m);  /* restore now. */",
1148         "                               trpt--;",
1149         "#ifdef CHECK",
1150         "                               printf(\"%%3d: proc %%d \", depth, II);",
1151         "                               printf(\"reverses %%d, %%d to %%d,\",",
1152         "                                       t->forw, tt, t->st);",
1153         "                               printf(\" %%s [abit=%%d,adepth=%%d,\",",
1154         "                                       t->tp, now._a_t, A_depth);",
1155         "                               printf(\"tau=%%d,%%d]\\n\",",
1156         "                                       trpt->tau, (trpt-1)->tau);",
1157         "#endif",
1158         "                               reached[ot][t->st] = 1;",
1159         "                               reached[ot][tt] = 1;",
1160         "",
1161         "                               ((P0 *)this)->_p = tt;",
1162         "                               _n |= _m;",
1163         "               }       }",
1164 /* PO */
1165         "#ifndef NOREDUCE",
1166         "               /* preselected - no succ definitely outside stack */",
1167         "               if ((trpt->tau&32) && !(trpt->tau&64))",
1168         "               {       From = now._nr_pr-1; To = BASE;",
1169         "#ifdef DEBUG",
1170         "                       printf(\"%%3d: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
1171         "                               depth, II+1, (int) _n, trpt->tau);",
1172         "#endif",
1173         "                       _n = 0; trpt->tau &= ~32;",
1174         "                       if (II >= BASE)",
1175         "                               goto Pickup;",
1176         "                       goto MainLoop;",
1177         "               }",
1178         "               trpt->tau &= ~(32|64);",
1179         "#endif",
1180 /* PO */
1181         "               if (_n != 0)",
1182         "                       continue;",
1183         "#ifdef DEBUG",
1184         "               printf(\"%%3d: no move [II=%%d, tau=%%d, boq=%%d, _nr_pr=%%d]\\n\",",
1185         "                       depth, II, trpt->tau, boq, now._nr_pr);",
1186         "#endif",
1187         "               if (boq != -1)",
1188         "               {       failedrv++;",
1189         "                       x = (Trail *) trpt->ostate; /* pre-rv state */",
1190         "                       if (!x) continue; /* root state */",
1191         "                       if ((x->tau&8) || (x->tau&32)) /* break atomic or preselect at parent */",
1192         "                       {       x->o_pm |= 8; /* mark failure */",
1193         "                               this = (((uchar *)&now)+proc_offset[otrpt->pr]);",
1194         "#ifdef VERBOSE",
1195         "                               printf(\"\\treset state of %%d from %%d to %%d\\n\",",
1196         "                                       otrpt->pr, ((P0 *)this)->_p, otrpt->st);",
1197         "#endif",
1198         "                               ((P0 *)this)->_p = otrpt->st;",
1199         "                               unsend(boq);    /* retract rv offer */",
1200         "                               boq = -1;",
1201
1202         "                               push_bfs(x, x->o_tt);",
1203         "#ifdef VERBOSE",
1204         "                               printf(\"failed rv, repush with %%d\\n\", x->o_pm);",
1205         "#endif",
1206         "                       }",
1207         "#ifdef VERBOSE",
1208         "                       else printf(\"failed rv, tau at parent: %%d\\n\", x->tau);",
1209         "#endif",
1210         "               } else if (now._nr_pr > 0)",
1211         "               {",
1212         "                       if ((trpt->tau&8))              /* atomic */",
1213         "                       {       trpt->tau &= ~(1|8);    /* 1=timeout, 8=atomic */",
1214         "#ifdef DEBUG",
1215         "                               printf(\"%%3d: atomic step proc %%d blocks\\n\",",
1216         "                                       depth, II+1);",
1217         "#endif",
1218         "                               goto Repeat;",
1219         "                       }",
1220         "",
1221         "                       if (!(trpt->tau&1)) /* didn't try timeout yet */",
1222         "                       {       trpt->tau |=  1;",
1223         "#ifdef DEBUG",
1224         "                               printf(\"%%d: timeout\\n\", depth);",
1225         "#endif",
1226         "                               goto MainLoop;",
1227         "                       }",
1228         "#ifndef VERI",
1229         "                       if (!noends && !a_cycles && !endstate())",
1230         "                               uerror(\"invalid end state\");",
1231         "#endif",
1232         "       }       }",
1233         "}",
1234         "",
1235         "void",
1236         "putter(Trail *trpt, int fd)",
1237         "{      long j;",
1238         "",
1239         "       if (!trpt) return;",
1240         "",
1241         "       if (trpt != (Trail *) trpt->ostate)",
1242         "               putter((Trail *) trpt->ostate, fd);",
1243         "",
1244         "       if (trpt->o_t)",
1245         "       {       sprintf(snap, \"%%d:%%d:%%d\\n\",",
1246         "                       trcnt++, trpt->pr, trpt->o_t->t_id);",
1247         "               j = strlen(snap);",
1248         "               if (write(fd, snap, j) != j)",
1249         "               {       printf(\"pan: error writing %%s\\n\", fnm);",
1250         "                       pan_exit(1);",
1251         "       }       }",
1252         "}",
1253         "",
1254         "void",
1255         "nuerror(char *str)",
1256         "{      int fd = make_trail();",
1257         "       int j;",
1258         "",
1259         "       if (fd < 0) return;",
1260         "#ifdef VERI",
1261         "       sprintf(snap, \"-2:%%d:-2\\n\", VERI);",
1262         "       write(fd, snap, strlen(snap));",
1263         "#endif",
1264         "#ifdef MERGED",
1265         "       sprintf(snap, \"-4:-4:-4\\n\");",
1266         "       write(fd, snap, strlen(snap));",
1267         "#endif",
1268         "       trcnt = 1;",
1269         "       putter(trpt, fd);",
1270         "       if (ntrpt->o_t)",       /* 4.2.8 -- Alex example, missing last transition */
1271         "       {       sprintf(snap, \"%%d:%%d:%%d\\n\",",
1272         "                       trcnt++, ntrpt->pr, ntrpt->o_t->t_id);",
1273         "               j = strlen(snap);",
1274         "               if (write(fd, snap, j) != j)",
1275         "               {       printf(\"pan: error writing %%s\\n\", fnm);",
1276         "                       pan_exit(1);",
1277         "       }       }",
1278         "       close(fd);",
1279         "       if (errors >= upto && upto != 0)",
1280         "       {",
1281         "               wrapup();",
1282         "       }",
1283         "}",
1284         "#endif",       /* BFS */
1285         0,
1286 };
1287
1288 static char *Code2c[] = {
1289         "void",
1290         "do_the_search(void)",
1291         "{      int i;",
1292         "       depth = mreached = 0;",
1293         "       trpt = &trail[0];",
1294         "#ifdef VERI",
1295         "       trpt->tau |= 4; /* the claim moves first */",
1296         "#endif",
1297         "       for (i = 0; i < (int) now._nr_pr; i++)",
1298         "       {       P0 *ptr = (P0 *) pptr(i);",
1299         "#ifndef NP",
1300         "               if (!(trpt->o_pm&2)",
1301         "               &&  accpstate[ptr->_t][ptr->_p])",
1302         "               {       trpt->o_pm |= 2;",
1303         "               }",
1304         "#else",
1305         "               if (!(trpt->o_pm&4)",
1306         "               &&  progstate[ptr->_t][ptr->_p])",
1307         "               {       trpt->o_pm |= 4;",
1308         "               }",
1309         "#endif",
1310         "       }",
1311         "#ifdef EVENT_TRACE",
1312         "#ifndef NP",
1313         "       if (accpstate[EVENT_TRACE][now._event])",
1314         "       {       trpt->o_pm |= 2;",
1315         "       }",
1316         "#else",
1317         "       if (progstate[EVENT_TRACE][now._event])",
1318         "       {       trpt->o_pm |= 4;",
1319         "       }",
1320         "#endif",
1321         "#endif",
1322         "#ifndef NOCOMP",
1323         "       Mask[0] = Mask[1] = 1;  /* _nr_pr, _nr_qs */",
1324         "       if (!a_cycles)",
1325         "       {       i = &(now._a_t) - (uchar *) &now;",
1326         "               Mask[i] = 1; /* _a_t */",
1327         "       }",
1328         "#ifndef NOFAIR",
1329         "       if (!fairness)",
1330         "       {       int j = 0;",
1331         "               i = &(now._cnt[0]) - (uchar *) &now;",
1332         "               while (j++ < NFAIR)",
1333         "                       Mask[i++] = 1; /* _cnt[] */",
1334         "       }",
1335         "#endif",
1336         "#endif",
1337         "#ifndef NOFAIR",
1338         "       if (fairness",
1339         "       &&  (a_cycles && (trpt->o_pm&2)))",
1340         "       {       now._a_t = 2;   /* set the A-bit */",
1341         "               now._cnt[0] = now._nr_pr + 1;", /* NEW: +1 */
1342                 "#ifdef VERBOSE",
1343         "       printf(\"%%3d: fairness Rule 1, cnt=%%d, _a_t=%%d\\n\",",
1344         "               depth, now._cnt[now._a_t&1], now._a_t);",
1345                 "#endif",
1346         "       }",
1347         "#endif",
1348
1349         "#if defined(C_States) && (HAS_TRACK==1)",
1350         "       /* capture initial state of tracked C objects */",
1351         "       c_update((uchar *) &(now.c_state[0]));",
1352         "#endif",
1353
1354         "#ifdef HAS_CODE",
1355         "       if (readtrail) getrail(); /* no return */",
1356         "#endif",
1357         "#ifdef BFS",
1358         "       bfs();",
1359         "#else",
1360                 "#if defined(C_States) && defined(HAS_STACK) && (HAS_TRACK==1)",
1361                 "       /* initial state of tracked & unmatched objects */",
1362                 "       c_stack((uchar *) &(svtack->c_stack[0]));",
1363                 "#endif",
1364                 "#ifdef RANDOMIZE",
1365         "       srand(123);",
1366                 "#endif",
1367         "       new_state();    /* start 1st DFS */",
1368         "#endif",
1369         "}",
1370
1371         "#ifdef INLINE_REV",
1372         "uchar",
1373         "do_reverse(Trans *t, short II, uchar M)",
1374         "{      uchar _m = M;",
1375         "       int  tt = (int) ((P0 *)this)->_p;",
1376         "#include REVERSE_MOVES",
1377         "R999:  return _m;",
1378         "}",
1379         "#endif",
1380
1381         "#ifndef INLINE",
1382         "#ifdef EVENT_TRACE",
1383         "static char _tp = 'n'; static int _qid = 0;",
1384         "#endif",
1385         "uchar",
1386         "do_transit(Trans *t, short II)",
1387         "{      uchar _m = 0;",
1388         "       int  tt = (int) ((P0 *)this)->_p;",
1389         "#ifdef M_LOSS",
1390         "       uchar delta_m = 0;",
1391         "#endif",
1392         "#ifdef EVENT_TRACE",
1393         "       short oboq = boq;",
1394         "       uchar ot = (uchar)  ((P0 *)this)->_t;",
1395         "       if (ot == EVENT_TRACE) boq = -1;",
1396                 "#define continue       { boq = oboq; return 0; }",
1397         "#else",
1398                 "#define continue       return 0",
1399                 "#ifdef SEPARATE",
1400         "       uchar ot = (uchar)  ((P0 *)this)->_t;",
1401                 "#endif",
1402         "#endif",
1403         "#include FORWARD_MOVES",
1404         "P999:",
1405         "#ifdef EVENT_TRACE",
1406         "       if (ot == EVENT_TRACE) boq = oboq;",
1407         "#endif",
1408         "       return _m;",
1409         "#undef continue",
1410         "}",
1411
1412         "#ifdef EVENT_TRACE",
1413         "void",
1414         "require(char tp, int qid)",
1415         "{      Trans *t;",
1416         "       _tp = tp; _qid = qid;",
1417         "",
1418         "       if (now._event != endevent)",
1419         "       for (t = trans[EVENT_TRACE][now._event]; t; t = t->nxt)",
1420         "       {       if (do_transit(t, EVENT_TRACE))",
1421         "               {       now._event = t->st;",
1422         "                       reached[EVENT_TRACE][t->st] = 1;",
1423         "#ifdef VERBOSE",
1424         "       printf(\"       event_trace move to -> %%d\\n\", t->st);",
1425         "#endif",
1426         "#ifndef BFS",
1427                 "#ifndef NP",
1428         "                       if (accpstate[EVENT_TRACE][now._event])",
1429         "                               (trpt+1)->o_pm |= 2;",
1430                 "#else",
1431         "                       if (progstate[EVENT_TRACE][now._event])",
1432         "                               (trpt+1)->o_pm |= 4;",
1433                 "#endif",
1434         "#endif",
1435         "#ifdef NEGATED_TRACE",
1436         "                       if (now._event == endevent)",
1437         "                       {",
1438                 "#ifndef BFS",
1439         "                               depth++; trpt++;",
1440                 "#endif",
1441         "                               uerror(\"event_trace error (all events matched)\");",
1442                 "#ifndef BFS",
1443         "                               trpt--; depth--;",
1444                 "#endif",
1445         "                               break;",
1446         "                       }",
1447         "#endif",
1448         "                       for (t = t->nxt; t; t = t->nxt)",
1449         "                       {       if (do_transit(t, EVENT_TRACE))",
1450         "                                Uerror(\"non-determinism in event-trace\");",
1451         "                       }",
1452         "                       return;",
1453         "               }",
1454         "#ifdef VERBOSE",
1455         "                else",
1456         "       printf(\"       event_trace miss '%%c' -- %%d, %%d, %%d\\n\",",
1457         "                       tp, qid, now._event, t->forw);",
1458         "#endif",
1459         "       }",
1460         "#ifdef NEGATED_TRACE",
1461         "       now._event = endevent; /* only 1st try will count -- fixed 4.2.6 */",
1462         "#else",
1463                 "#ifndef BFS",
1464         "       depth++; trpt++;",
1465                 "#endif",
1466         "       uerror(\"event_trace error (no matching event)\");",
1467                 "#ifndef BFS",
1468         "       trpt--; depth--;",
1469                 "#endif",
1470         "#endif",
1471         "}",
1472         "#endif",
1473
1474         "int",
1475         "enabled(int iam, int pid)",
1476         "{      Trans *t; uchar *othis = this;",
1477         "       int res = 0; int tt; uchar ot;",
1478         "#ifdef VERI",
1479         "       /* if (pid > 0) */ pid++;",
1480         "#endif",
1481         "       if (pid == iam)",
1482         "               Uerror(\"used: enabled(pid=thisproc)\");",
1483         "       if (pid < 0 || pid >= (int) now._nr_pr)",
1484         "               return 0;",
1485         "       this = pptr(pid);",
1486         "       TstOnly = 1;",
1487         "       tt = (int) ((P0 *)this)->_p;",
1488         "       ot = (uchar) ((P0 *)this)->_t;",
1489         "       for (t = trans[ot][tt]; t; t = t->nxt)",
1490         "               if (do_transit(t, (short) pid))",
1491         "               {       res = 1;",
1492         "                       break;",
1493         "               }",
1494         "       TstOnly = 0;",
1495         "       this = othis;",
1496         "       return res;",
1497         "}",
1498         "#endif",
1499         "void",
1500         "snapshot(void)",
1501         "{      static long sdone = (long) 0;",
1502         "       long ndone = (unsigned long) nstates/1000000;",
1503         "       if (ndone == sdone) return;",
1504         "       sdone = ndone;",
1505         "       printf(\"Depth= %%7d States= %%7g \", mreached, nstates);",
1506         "       printf(\"Transitions= %%7g \", nstates+truncs);",
1507         "#ifdef MA",
1508         "       printf(\"Nodes= %%7d \", nr_states);",
1509         "#endif",
1510         "       printf(\"Memory= %%-6.3f\\n\", memcnt/1000000.);",
1511         "       fflush(stdout);",
1512         "}",
1513
1514         "#ifdef SC",
1515         "void",
1516         "stack2disk(void)",
1517         "{",
1518         "       if (!stackwrite",
1519         "       &&  (stackwrite = creat(stackfile, TMODE)) < 0)",
1520         "               Uerror(\"cannot create stackfile\");",
1521         "",
1522         "       if (write(stackwrite, trail, DDD*sizeof(Trail))",
1523         "       !=  DDD*sizeof(Trail))",
1524         "               Uerror(\"stackfile write error -- disk is full?\");",
1525         "",
1526         "       memmove(trail, &trail[DDD], (HHH-DDD+2)*sizeof(Trail));",
1527         "       memset(&trail[HHH-DDD+2], 0, (omaxdepth - HHH + DDD - 2)*sizeof(Trail));",
1528         "       CNT1++;",
1529         "}",
1530         "void",
1531         "disk2stack(void)",
1532         "{      long have;",
1533         "",
1534         "       CNT2++;",
1535         "       memmove(&trail[DDD], trail, (HHH-DDD+2)*sizeof(Trail));",
1536         "",
1537         "       if (!stackwrite",
1538         "       ||  lseek(stackwrite, -DDD* (off_t) sizeof(Trail), SEEK_CUR) == -1)",
1539         "               Uerror(\"disk2stack lseek error\");",
1540         "",
1541         "       if (!stackread",
1542         "       &&  (stackread = open(stackfile, 0)) < 0)",
1543         "               Uerror(\"cannot open stackfile\");",
1544         "",
1545         "       if (lseek(stackread, (CNT1-CNT2)*DDD* (off_t) sizeof(Trail), SEEK_SET) == -1)",
1546         "               Uerror(\"disk2stack lseek error\");",
1547         "",
1548         "       have = read(stackread, trail, DDD*sizeof(Trail));",
1549         "       if (have !=  DDD*sizeof(Trail))",
1550         "               Uerror(\"stackfile read error\");",
1551         "}",
1552         "#endif",
1553
1554         "uchar *",
1555         "Pptr(int x)",  /* as a fct, to avoid a problem with the p9 compiler */
1556         "{      if (x < 0 || x >= MAXPROC || !proc_offset[x])", /* does not exist */
1557         "               return noptr;",
1558         "       else",
1559         "               return (uchar *) pptr(x);",
1560         "}",
1561         "int qs_empty(void);",
1562
1563         "/*",
1564         " * new_state() is the main DFS search routine in the verifier",
1565         " * it has a lot of code ifdef-ed together to support",
1566         " * different search modes, which makes it quite unreadable.",
1567         " * if you are studying the code, first use the C preprocessor",
1568         " * to generate a specific version from the pan.c source,",
1569         " * e.g. by saying:",
1570         " *     gcc -E -DNOREDUCE -DBITSTATE pan.c > ppan.c",
1571         " * and then study the resulting file, rather than this one",
1572         " */",
1573         "#if !defined(BFS) && (!defined(BITSTATE) || !defined(MA))",
1574         "void",
1575         "new_state(void)",
1576         "{      Trans *t;",
1577         "       uchar _n, _m, ot;",
1578         "#ifdef RANDOMIZE",
1579         "       short ooi, eoi;",
1580         "#endif",
1581         "#ifdef M_LOSS",
1582         "       uchar delta_m = 0;",
1583         "#endif",
1584         "       short II, JJ = 0, kk;",
1585         "       int tt;",
1586         "       short From = now._nr_pr-1, To = BASE;",
1587         "Down:",
1588         "#ifdef CHECK",
1589         "       printf(\"%%d: Down - %%s\",",
1590         "               depth, (trpt->tau&4)?\"claim\":\"program\");",
1591         "       printf(\" %%saccepting [pids %%d-%%d]\\n\",",
1592         "               (trpt->o_pm&2)?\"\":\"non-\", From, To);",
1593         "#endif",
1594
1595         "#ifdef SC",
1596         "       if (depth > hiwater)",
1597         "       {       stack2disk();",
1598         "               maxdepth += DDD;",
1599         "               hiwater += DDD;",
1600         "               trpt -= DDD;",
1601         "               if(verbose)",
1602         "               printf(\"zap %%d: %%d (maxdepth now %%d)\\n\",",
1603         "                       CNT1, hiwater, maxdepth);",
1604         "       }",
1605         "#endif",
1606
1607         "       trpt->tau &= ~(16|32|64); /* make sure these are off */",
1608         "#if defined(FULLSTACK) && defined(MA)",
1609         "       trpt->proviso = 0;",
1610         "#endif",
1611         "       if (depth >= maxdepth)",
1612         "       {       truncs++;",
1613         "#if SYNC",
1614         "               (trpt+1)->o_n = 1; /* not a deadlock */",
1615         "#endif",
1616         "               if (!warned)",
1617         "               { warned = 1;",
1618         "                 printf(\"error: max search depth too small\\n\");",
1619         "               }",
1620         "               if (bounded) uerror(\"depth limit reached\");",
1621         "               (trpt-1)->tau |= 16; /* worstcase guess */",
1622         "               goto Up;",
1623         "       }",
1624         "AllOver:",
1625         "#if defined(FULLSTACK) && !defined(MA)",
1626         "       /* if atomic or rv move, carry forward previous state */",
1627         "       trpt->ostate = (trpt-1)->ostate;",      /* was: = (struct H_el *) 0;*/
1628         "#endif",
1629         "#ifdef VERI",
1630         "       if ((trpt->tau&4) || ((trpt-1)->tau&128))",
1631         "#endif",
1632         "       if (boq == -1) {        /* if not mid-rv */",
1633         "#ifndef SAFETY",
1634         "               /* this check should now be redundant",
1635         "                * because the seed state also appears",
1636         "                * on the 1st dfs stack and would be",
1637         "                * matched in hstore below",
1638         "                */",
1639         "               if ((now._a_t&1) && depth > A_depth)",
1640         "               {       if (!memcmp((char *)&A_Root, ",
1641         "                               (char *)&now, vsize))",
1642         "                       {",
1643         "                               depthfound = A_depth;",
1644                 "#ifdef CHECK",
1645         "                         printf(\"matches seed\\n\");",
1646                 "#endif",
1647                 "#ifdef NP",
1648         "                         uerror(\"non-progress cycle\");",
1649                 "#else",
1650         "                         uerror(\"acceptance cycle\");",
1651                 "#endif",
1652         "                         goto Up;",
1653         "                       }",
1654                 "#ifdef CHECK",
1655         "                       printf(\"not seed\\n\");",
1656                 "#endif",
1657         "               }",
1658         "#endif",
1659         "               if (!(trpt->tau&8)) /* if no atomic move */",
1660         "               {",
1661         "#ifdef BITSTATE",
1662                 "#ifdef CNTRSTACK",     /* -> bitstate, reduced, safety */
1663         "                       II = bstore((char *)&now, vsize);",
1664         "                       trpt->j6 = j1; trpt->j7 = j2;",
1665         "                       JJ = LL[j1] && LL[j2];",
1666                 "#else",
1667                         "#ifdef FULLSTACK",
1668         "                       JJ = onstack_now();",               /* sets j1 */
1669                         "#else",
1670                                 "#ifndef NOREDUCE",
1671         "                       JJ = II; /* worstcase guess for p.o. */",
1672                                 "#endif",
1673                         "#endif",
1674         "                       II = bstore((char *)&now, vsize);", /* sets j1-j4 */
1675                 "#endif",
1676         "#else",
1677                 "#ifdef MA",
1678         "                       II = gstore((char *)&now, vsize, 0);",
1679                         "#ifndef FULLSTACK",
1680         "                       JJ = II;",
1681                         "#else",
1682         "                       JJ = (II == 2)?1:0;",
1683                         "#endif",
1684                 "#else",
1685         "                       II = hstore((char *)&now, vsize);",
1686                         "#ifdef FULLSTACK",
1687         "                       JJ = (II == 2)?1:0;",
1688                         "#endif",
1689                 "#endif",
1690         "#endif",
1691         "                       kk = (II == 1 || II == 2);",
1692                                 /* II==0 new state */
1693                                 /* II==1 old state */
1694                                 /* II==2 on current dfs stack */
1695                                 /* II==3 on 1st dfs stack */
1696         "#ifndef SAFETY",
1697
1698         "                       if (!fairness && a_cycles)",
1699         "                       if (II == 2 && ((trpt->o_pm&2) || ((trpt-1)->o_pm&2)))",
1700         "                       {       II = 3; /* Schwoon & Esparza 2005, Gastin&Moro 2004 */",
1701                 "#ifdef VERBOSE",
1702         "                               printf(\"state match on dfs stack\\n\");",
1703                 "#endif",
1704         "                               goto same_case;",
1705         "                       }",
1706
1707
1708                 "#if defined(FULLSTACK) && defined(BITSTATE)",
1709         "                       if (!JJ && (now._a_t&1) && depth > A_depth)",
1710         "                       {       int oj1 = j1;",
1711         "                               uchar o_a_t = now._a_t;",
1712         "                               now._a_t &= ~(1|16|32);", /* 1st stack  */
1713         "                               if (onstack_now())",      /* changes j1 */
1714         "                               {       II = 3;",
1715                 "#ifdef VERBOSE",
1716         "                                       printf(\"state match on 1st dfs stack\\n\");",
1717                 "#endif",
1718         "                               }",
1719         "                               now._a_t = o_a_t;",     /* restore */
1720         "                               j1 = oj1;",
1721         "                       }",
1722                 "#endif",
1723         "                       if (II == 3 && a_cycles && (now._a_t&1))",
1724         "                       {",
1725                 "#ifndef NOFAIR",
1726         "                          if (fairness && now._cnt[1] > 1)     /* was != 0 */",
1727         "                          {",
1728                 "#ifdef VERBOSE",
1729         "                               printf(\"\tfairness count non-zero\\n\");",
1730                 "#endif",
1731         "                               II = 0;", /* treat as new state */
1732         "                          } else",
1733                 "#endif",
1734         "                          {",
1735                 "#ifndef BITSTATE",
1736         "                               nShadow--;",
1737                 "#endif",
1738         "same_case:                     if (Lstate) depthfound = Lstate->D;",
1739                 "#ifdef NP",
1740         "                               uerror(\"non-progress cycle\");",
1741                 "#else",
1742         "                               uerror(\"acceptance cycle\");",
1743                 "#endif",
1744         "                               goto Up;",
1745         "                          }",
1746         "                       }",
1747         "#endif",
1748
1749         "#ifndef NOREDUCE",
1750                 "#ifndef SAFETY",
1751         "                       if ((II && JJ) || (II == 3))",
1752         "                       {       /* marker for liveness proviso */",
1753         "                               (trpt-1)->tau |= 16;",
1754         "                               truncs2++;",
1755         "                       }",
1756                 "#else",
1757         "                       if (!II || !JJ)",
1758         "                       {       /* successor outside stack */",
1759         "                               (trpt-1)->tau |= 64;",
1760         "                       }",
1761                 "#endif",
1762         "#endif",
1763         "                       if (II)",
1764         "                       {       truncs++;",
1765         "                               goto Up;",
1766         "                       }",
1767         "                       if (!kk)",
1768         "                       {       nstates++;",
1769         "                               if ((unsigned long) nstates%%1000000 == 0)",
1770         "                                       snapshot();",
1771         "#ifdef SVDUMP",
1772         "                               if (vprefix > 0)",
1773         "                               if (write(svfd, (uchar *) &now, vprefix) != vprefix)",
1774         "                               {       fprintf(efd, \"writing %%s.svd failed\\n\", Source);",
1775         "                                       wrapup();",
1776         "                               }",
1777         "#endif",
1778         "#if defined(MA) && defined(W_XPT)",
1779         "                               if ((unsigned long) nstates%%W_XPT == 0)",
1780         "                               {       void w_xpoint(void);",
1781         "                                       w_xpoint();",
1782         "                               }",
1783         "#endif",
1784         "                       }",
1785         "#if defined(FULLSTACK) || defined(CNTRSTACK)",
1786         "                       onstack_put();",
1787                 "#ifdef DEBUG2",
1788                 "#if defined(FULLSTACK) && !defined(MA)",
1789         "                       printf(\"%%d: putting %%u (%%d)\\n\", depth,",
1790         "                               trpt->ostate, ",
1791         "                               (trpt->ostate)?trpt->ostate->tagged:0);",
1792                 "#else",
1793         "                       printf(\"%%d: putting\\n\", depth);",
1794                 "#endif",
1795                 "#endif",
1796         "#endif",
1797         "       }       }",
1798
1799
1800         "       if (depth > mreached)",
1801         "               mreached = depth;",
1802         "#ifdef VERI",
1803         "       if (trpt->tau&4)",
1804         "#endif",
1805         "       trpt->tau &= ~(1|2);    /* timeout and -request off */",
1806         "       _n = 0;",
1807         "#if SYNC",
1808         "       (trpt+1)->o_n = 0;",
1809         "#endif",
1810         "#ifdef VERI",
1811         "       if (now._nr_pr == 0)    /* claim terminated */",
1812         "               uerror(\"end state in claim reached\");",
1813         "       check_claim(((P0 *)pptr(0))->_p);",
1814         "Stutter:",
1815         "       if (trpt->tau&4)        /* must make a claimmove */",
1816         "       {",
1817
1818         "#ifndef NOFAIR",
1819         "               if ((now._a_t&2)        /* A-bit set */",
1820         "               &&   now._cnt[now._a_t&1] == 1)",
1821         "               {       now._a_t &= ~2;",
1822         "                       now._cnt[now._a_t&1] = 0;",
1823         "                       trpt->o_pm |= 16;",
1824                 "#ifdef DEBUG",
1825         "       printf(\"%%3d: fairness Rule 3.: _a_t = %%d\\n\",",
1826         "               depth, now._a_t);",
1827                 "#endif",
1828         "               }",
1829         "#endif",
1830
1831         "               II = 0;         /* never */",
1832         "               goto Veri0;",
1833         "       }",
1834         "#endif",
1835         "#ifndef NOREDUCE",
1836         "       /* Look for a process with only safe transitions */",
1837         "       /* (special rules apply in the 2nd dfs) */",
1838 "#ifdef SAFETY",
1839         "       if (boq == -1 && From != To)",
1840 "#else",
1841         "/* implied: #ifdef FULLSTACK */",
1842         "       if (boq == -1 && From != To",
1843         "       &&  (!(now._a_t&1)",
1844         "           ||  (a_cycles &&",
1845         "#ifndef BITSTATE",
1846                 "#ifdef MA",
1847                         "#ifdef VERI",
1848         "                !((trpt-1)->proviso))",
1849                         "#else",
1850         "               !(trpt->proviso))",
1851                         "#endif",
1852                 "#else",
1853                         "#ifdef VERI",
1854         "                (trpt-1)->ostate &&",
1855         "               !(((char *)&((trpt-1)->ostate->state))[0] & 128))",
1856                         "#else",
1857         "               !(((char *)&(trpt->ostate->state))[0] & 128))",
1858                         "#endif",
1859                 "#endif",
1860         "#else",
1861                 "#ifdef VERI",
1862         "               (trpt-1)->ostate &&",
1863         "               (trpt-1)->ostate->proviso == 0)",
1864                 "#else",
1865         "               trpt->ostate->proviso == 0)",
1866                 "#endif",
1867         "#endif",
1868         "          ))",
1869         "/* #endif */",
1870 "#endif",
1871         "       for (II = From; II >= To; II -= 1)",
1872         "       {",
1873         "Resume:        /* pick up here if preselect fails */",
1874         "               this = pptr(II);",
1875         "               tt = (int) ((P0 *)this)->_p;",
1876         "               ot = (uchar) ((P0 *)this)->_t;",
1877         "               if (trans[ot][tt]->atom & 8)",
1878         "               {       t = trans[ot][tt];",
1879         "                       if (t->qu[0] != 0)",
1880         "                       {       Ccheck++;",
1881         "                               if (!q_cond(II, t))",
1882         "                                       continue;",
1883         "                               Cholds++;",
1884         "                       }",
1885         "                       From = To = II;",
1886         "#ifdef NIBIS",
1887         "                       t->om = 0;",
1888         "#endif",
1889         "                       trpt->tau |= 32; /* preselect marker */",
1890                 "#ifdef DEBUG",
1891                 "#ifdef NIBIS",
1892         "                       printf(\"%%3d: proc %%d Pre\", depth, II);",
1893         "                       printf(\"Selected (om=%%d, tau=%%d)\\n\", ",
1894         "                               t->om, trpt->tau);",
1895                 "#else",
1896         "       printf(\"%%3d: proc %%d PreSelected (tau=%%d)\\n\", ",
1897         "               depth, II, trpt->tau);",
1898                 "#endif",
1899                 "#endif",
1900         "                       goto Again;",
1901         "               }",
1902         "       }",
1903         "       trpt->tau &= ~32;",
1904         "#endif",
1905         "#if !defined(NOREDUCE) || (defined(ETIM) && !defined(VERI))",
1906         "Again:",
1907         "#endif",
1908         "       /* The Main Expansion Loop over Processes */",
1909
1910         "       trpt->o_pm &= ~(8|16|32|64); /* fairness-marks */",
1911
1912         "#ifndef NOFAIR",
1913         "       if (fairness && boq == -1",
1914                 "#ifdef VERI",
1915         "       && (!(trpt->tau&4) && !((trpt-1)->tau&128))",
1916                 "#endif",
1917         "       && !(trpt->tau&8))",
1918         "       {       /* A_bit = 1; Cnt = N in acc states with A_bit 0 */",
1919         "               if (!(now._a_t&2))",    /* A-bit not set */
1920         "               {",
1921         "                       if (a_cycles && (trpt->o_pm&2))",
1922         "                       {       /* Accepting state */",
1923         "                               now._a_t |= 2;",
1924         "                               now._cnt[now._a_t&1] = now._nr_pr + 1;", /* NEW +1 */
1925         "                               trpt->o_pm |= 8;",
1926                 "#ifdef DEBUG",
1927         "       printf(\"%%3d: fairness Rule 1: cnt=%%d, _a_t=%%d\\n\",",
1928         "                       depth, now._cnt[now._a_t&1], now._a_t);",
1929                 "#endif",
1930         "                       }",
1931         "               } else",                /* A-bit set */
1932         "               {       /* A_bit = 0 when Cnt 0 */",
1933         "                       if (now._cnt[now._a_t&1] == 1)",        /* NEW: 1 iso 0 */
1934         "                       {       now._a_t &= ~2;",               /* reset a-bit */
1935         "                               now._cnt[now._a_t&1] = 0;",     /* NEW: reset cnt */
1936         "                               trpt->o_pm |= 16;",
1937                 "#ifdef DEBUG",
1938         "       printf(\"%%3d: fairness Rule 3: _a_t = %%d\\n\",",
1939         "               depth, now._a_t);",
1940                 "#endif",
1941         "       }       }       }",
1942         "#endif",
1943
1944         "       for (II = From; II >= To; II -= 1)",
1945         "       {",
1946         "#if SYNC",
1947         "               /* no rendezvous with same proc */",
1948         "               if (boq != -1 && trpt->pr == II) continue;",
1949         "#endif",
1950         "#ifdef VERI",
1951         "Veri0:",
1952         "#endif",
1953         "               this = pptr(II);",
1954         "               tt = (int) ((P0 *)this)->_p;",
1955         "               ot = (uchar) ((P0 *)this)->_t;",
1956
1957         "#ifdef NIBIS",
1958         "               /* don't repeat a previous preselected expansion */",
1959         "               /* could hit this if reduction proviso was false */",
1960         "               t = trans[ot][tt];",
1961         "               if (!(trpt->tau&4)",    /* not claim */
1962         "               && !(trpt->tau&1)",     /* not timeout */
1963         "               && !(trpt->tau&32)",    /* not preselected */
1964         "               && (t->atom & 8)",      /* local */
1965         "               && boq == -1",          /* not inside rendezvous */
1966         "               && From != To)",        /* not inside atomic seq */
1967         "               {       if (t->qu[0] == 0",     /* unconditional */
1968         "                       ||  q_cond(II, t))",    /* true condition */
1969         "                       {       _m = t->om;",
1970         "                               if (_m>_n||(_n>3&&_m!=0)) _n=_m;",
1971         "                               continue; /* did it before */",
1972         "               }       }",
1973         "#endif",
1974         "               trpt->o_pm &=  ~1; /* no move in this pid yet */",
1975         "#ifdef EVENT_TRACE",
1976         "               (trpt+1)->o_event = now._event;",
1977         "#endif",
1978         "               /* Fairness: Cnt++ when Cnt == II */",
1979         "#ifndef NOFAIR",
1980         "               trpt->o_pm &= ~64; /* didn't apply rule 2 */",
1981         "               if (fairness",
1982         "               && boq == -1",  /* not mid rv - except rcv - NEW 3.0.8 */
1983         "               && !(trpt->o_pm&32)",   /* Rule 2 not in effect */
1984         "               && (now._a_t&2)",       /* A-bit is set */
1985         "               &&  now._cnt[now._a_t&1] == II+2)",
1986         "               {       now._cnt[now._a_t&1] -= 1;",
1987                 "#ifdef VERI",
1988         "                       /* claim need not participate */",
1989         "                       if (II == 1)",
1990         "                               now._cnt[now._a_t&1] = 1;",
1991                 "#endif",
1992                 "#ifdef DEBUG",
1993         "               printf(\"%%3d: proc %%d fairness \", depth, II);",
1994         "               printf(\"Rule 2: --cnt to %%d (%%d)\\n\",",
1995         "                       now._cnt[now._a_t&1], now._a_t);",
1996                 "#endif",
1997         "                       trpt->o_pm |= (32|64);",
1998         "               }",
1999         "#endif",
2000         "#ifdef HAS_PROVIDED",
2001         "               if (!provided(II, ot, tt, t)) continue;",
2002         "#endif",
2003         "               /* check all trans of proc II - escapes first */",
2004         "#ifdef HAS_UNLESS",
2005         "               trpt->e_state = 0;",
2006         "#endif",
2007         "               (trpt+1)->pr = (uchar) II;",    /* for uerror */
2008         "               (trpt+1)->st = tt;",
2009
2010         "#ifdef RANDOMIZE",
2011         "               for (ooi = eoi = 0, t = trans[ot][tt]; t; t = t->nxt, ooi++)",
2012         "                       if (strcmp(t->tp, \"else\") == 0)",
2013         "                               eoi++;",
2014         "",
2015         "               if (eoi)",
2016         "               {       t = trans[ot][tt];",
2017         "#ifdef VERBOSE",
2018         "                       printf(\"randomizer: suppressed, saw else\\n\");",
2019         "#endif",
2020         "               } else",
2021         "               {       eoi = rand()%%ooi;",
2022         "#ifdef VERBOSE",
2023         "                       printf(\"randomizer: skip %%d in %%d\\n\", eoi, ooi);",
2024         "#endif",
2025         "                       for (t = trans[ot][tt]; t; t = t->nxt)",
2026         "                               if (eoi-- <= 0) break;",
2027         "               }",
2028         "DOMORE:",
2029         "               for ( ; t && ooi > 0; t = t->nxt, ooi--)",
2030         "#else",
2031         "               for (t = trans[ot][tt]; t; t = t->nxt)",
2032         "#endif",
2033         "               {",
2034         "#ifdef HAS_UNLESS",
2035         "                       /* exploring all transitions from",
2036         "                        * a single escape state suffices",
2037         "                        */",
2038         "                       if (trpt->e_state > 0",
2039         "                       &&  trpt->e_state != t->e_trans)",
2040         "                       {",
2041                 "#ifdef DEBUG",
2042         "               printf(\"skip 2nd escape %%d (did %%d before)\\n\",",
2043         "                       t->e_trans, trpt->e_state);",
2044                 "#endif",
2045         "                               break;",
2046         "                       }",
2047         "#endif",
2048         "                       (trpt+1)->o_t = t;",    /* for uerror */
2049         "#ifdef INLINE",
2050         "#include FORWARD_MOVES",
2051         "P999:                  /* jumps here when move succeeds */",
2052         "#else",
2053         "                       if (!(_m = do_transit(t, II))) continue;",
2054         "#endif",
2055         "                       if (boq == -1)",
2056 "#ifdef CTL",
2057         "       /* for branching-time, can accept reduction only if */",
2058         "       /* the persistent set contains just 1 transition */",
2059         "                       {       if ((trpt->tau&32) && (trpt->o_pm&1))",
2060         "                                       trpt->tau |= 16;",
2061         "                               trpt->o_pm |= 1; /* we moved */",
2062         "                       }",
2063 "#else",
2064         "                               trpt->o_pm |= 1; /* we moved */",
2065 "#endif",
2066         "#ifdef PEG",
2067         "                       peg[t->forw]++;",
2068         "#endif",
2069
2070         "#if defined(VERBOSE) || defined(CHECK)",
2071                 "#if defined(SVDUMP)",
2072         "                       printf(\"%%3d: proc %%d exec %%d \\n\", ",
2073         "                               depth, II, t->t_id);",
2074                 "#else",
2075         "                       printf(\"%%3d: proc %%d exec %%d, \", ",
2076         "                               depth, II, t->forw);",
2077         "                       printf(\"%%d to %%d, %%s %%s %%s\", ",
2078         "                               tt, t->st, t->tp,",
2079         "                               (t->atom&2)?\"atomic\":\"\",",
2080         "                               (boq != -1)?\"rendez-vous\":\"\");",
2081                         "#ifdef HAS_UNLESS",
2082         "                       if (t->e_trans)",
2083         "                               printf(\" (escapes to state %%d)\",",
2084         "                                       t->st);",
2085                         "#endif",
2086         "                       printf(\" %%saccepting [tau=%%d]\\n\",",
2087         "                               (trpt->o_pm&2)?\"\":\"non-\", trpt->tau);",
2088                 "#endif",
2089                 "#ifdef RANDOMIZE",
2090         "                       printf(\"       randomizer %%d\\n\", ooi);",
2091                 "#endif",
2092         "#endif",
2093
2094         "#ifdef HAS_LAST",
2095         "#ifdef VERI",
2096         "                       if (II != 0)",
2097         "#endif",
2098         "                               now._last = II - BASE;",
2099         "#endif",
2100         "#ifdef HAS_UNLESS",
2101         "                       trpt->e_state = t->e_trans;",
2102         "#endif",
2103
2104         "                       depth++; trpt++;",
2105         "                       trpt->pr = (uchar) II;",
2106         "                       trpt->st = tt;",
2107         "                       trpt->o_pm &= ~(2|4);",
2108         "                       if (t->st > 0)",
2109         "                       {       ((P0 *)this)->_p = t->st;",
2110         "/*     moved down              reached[ot][t->st] = 1; */",
2111         "                       }",
2112         "#ifndef SAFETY",
2113         "                       if (a_cycles)",
2114         "                       {",
2115                 "#if (ACCEPT_LAB>0 && !defined(NP)) || (PROG_LAB>0 && defined(HAS_NP))",
2116         "                               int ii;",
2117                 "#endif",
2118                 "#define P__Q   ((P0 *)pptr(ii))",
2119                 "#if ACCEPT_LAB>0",
2120                         "#ifdef NP",
2121         "                               /* state 1 of np_ claim is accepting */",
2122         "                               if (((P0 *)pptr(0))->_p == 1)",
2123         "                                       trpt->o_pm |= 2;",
2124                         "#else",
2125         "                               for (ii = 0; ii < (int) now._nr_pr; ii++)",
2126         "                               { if (accpstate[P__Q->_t][P__Q->_p])",
2127         "                                 {     trpt->o_pm |= 2;",
2128         "                                       break;",
2129         "                               } }",
2130                         "#endif",
2131                 "#endif",
2132                 "#if defined(HAS_NP) && PROG_LAB>0",
2133         "                               for (ii = 0; ii < (int) now._nr_pr; ii++)",
2134         "                               { if (progstate[P__Q->_t][P__Q->_p])",
2135         "                                 {     trpt->o_pm |= 4;",
2136         "                                       break;",
2137         "                               } }",
2138                 "#endif",
2139                 "#undef P__Q",
2140         "                       }",
2141         "#endif",
2142         "                       trpt->o_t  =  t; trpt->o_n  = _n;",
2143         "                       trpt->o_ot = ot; trpt->o_tt = tt;",
2144         "                       trpt->o_To = To; trpt->o_m  = _m;",
2145         "                       trpt->tau = 0;",
2146 "#ifdef RANDOMIZE",
2147         "                       trpt->oo_i = ooi;",
2148 "#endif",
2149         "                       if (boq != -1 || (t->atom&2))",
2150         "                       {       trpt->tau |= 8;",
2151         "#ifdef VERI",
2152         "                               /* atomic sequence in claim */",
2153         "                               if((trpt-1)->tau&4)",
2154         "                                       trpt->tau |= 4;",
2155         "                               else",
2156         "                                       trpt->tau &= ~4;",
2157         "                       } else",
2158         "                       {       if ((trpt-1)->tau&4)",
2159         "                                       trpt->tau &= ~4;",
2160         "                               else",
2161         "                                       trpt->tau |= 4;",
2162         "                       }",
2163         "                       /* if claim allowed timeout, so */",
2164         "                       /* does the next program-step: */",
2165         "                       if (((trpt-1)->tau&1) && !(trpt->tau&4))",
2166         "                               trpt->tau |= 1;",
2167         "#else",
2168         "                       } else",
2169         "                               trpt->tau &= ~8;",
2170         "#endif",
2171         "                       if (boq == -1 && (t->atom&2))",
2172         "                       {       From = To = II; nlinks++;",
2173         "                       } else",
2174         "                       {       From = now._nr_pr-1; To = BASE;",
2175         "                       }",
2176         "                       goto Down;      /* pseudo-recursion */",
2177         "Up:",
2178         "#ifdef CHECK",
2179         "       printf(\"%%d: Up - %%s\\n\", depth,",
2180         "               (trpt->tau&4)?\"claim\":\"program\");",
2181         "#endif",
2182         "#ifdef MA",
2183         "       if (depth <= 0) return;",
2184         "       /* e.g., if first state is old, after a restart */",
2185         "#endif",
2186
2187         "#ifdef SC",
2188         "       if (CNT1 > CNT2",
2189         "               && depth < hiwater - (HHH-DDD) + 2)",
2190         "       {",
2191         "               trpt += DDD;",
2192         "               disk2stack();",
2193         "               maxdepth -= DDD;",
2194         "               hiwater -= DDD;",
2195         "if(verbose)",
2196         "printf(\"unzap %%d: %%d\\n\", CNT2, hiwater);",
2197         "       }",
2198         "#endif",
2199
2200         "#ifndef NOFAIR",
2201         "                       if (trpt->o_pm&128)     /* fairness alg */",
2202         "                       {       now._cnt[now._a_t&1] = trpt->bup.oval;",
2203         "                               _n = 1; trpt->o_pm &= ~128;",
2204         "                               depth--; trpt--;",
2205                 "#if defined(VERBOSE) || defined(CHECK)",
2206         "       printf(\"%%3d: reversed fairness default move\\n\", depth);",
2207                 "#endif",
2208         "                               goto Q999;",
2209         "                       }",
2210         "#endif",
2211
2212         "#ifdef HAS_LAST",
2213         "#ifdef VERI",
2214         "                       { int d; Trail *trl;",
2215         "                         now._last = 0;",
2216         "                         for (d = 1; d < depth; d++)",
2217         "                         {     trl = getframe(depth-d); /* was (trpt-d) */",
2218         "                               if (trl->pr != 0)",
2219         "                               { now._last = trl->pr - BASE;",
2220         "                                 break;",
2221         "                       } }     }",
2222         "#else",
2223         "                       now._last = (depth<1)?0:(trpt-1)->pr;",
2224         "#endif",
2225         "#endif",
2226         "#ifdef EVENT_TRACE",
2227         "                       now._event = trpt->o_event;",
2228         "#endif",
2229         "#ifndef SAFETY",
2230         "                       if ((now._a_t&1) && depth <= A_depth)",
2231         "                               return; /* to checkcycles() */",
2232         "#endif",
2233         "                       t  = trpt->o_t;  _n = trpt->o_n;",
2234         "                       ot = trpt->o_ot; II = trpt->pr;",
2235         "                       tt = trpt->o_tt; this = pptr(II);",
2236         "                       To = trpt->o_To; _m  = trpt->o_m;",
2237 "#ifdef RANDOMIZE",
2238         "                       ooi = trpt->oo_i;",
2239 "#endif",
2240         "#ifdef INLINE_REV",
2241         "                       _m = do_reverse(t, II, _m);",
2242         "#else",
2243         "#include REVERSE_MOVES",
2244         "R999:                  /* jumps here when done */",
2245         "#endif",
2246
2247         "#ifdef VERBOSE",
2248         "                       printf(\"%%3d: proc %%d \", depth, II);",
2249         "                       printf(\"reverses %%d, %%d to %%d,\",",
2250         "                               t->forw, tt, t->st);",
2251         "                       printf(\" %%s [abit=%%d,adepth=%%d,\", ",
2252         "                               t->tp, now._a_t, A_depth);",
2253         "                       printf(\"tau=%%d,%%d]\\n\", ",
2254         "                               trpt->tau, (trpt-1)->tau);",
2255         "#endif",
2256         "#ifndef NOREDUCE",
2257         "                       /* pass the proviso tags */",
2258         "                       if ((trpt->tau&8)       /* rv or atomic */",
2259         "                       &&  (trpt->tau&16))",
2260         "                               (trpt-1)->tau |= 16;",
2261         "#ifdef SAFETY",
2262         "                       if ((trpt->tau&8)       /* rv or atomic */",
2263         "                       &&  (trpt->tau&64))",
2264         "                               (trpt-1)->tau |= 64;",
2265         "#endif",
2266         "#endif",
2267         "                       depth--; trpt--;",
2268         "#ifdef NIBIS",
2269         "                       (trans[ot][tt])->om = _m; /* head of list */",
2270         "#endif",
2271
2272         "                       /* i.e., not set if rv fails */",
2273         "                       if (_m)",
2274         "                       {",
2275         "#if defined(VERI) && !defined(NP)",
2276         "                               if (II == 0 && verbose && !reached[ot][t->st])",
2277         "                               {",
2278         "                       printf(\"depth %%d: Claim reached state %%d (line %%d)\\n\",",
2279         "                                       depth, t->st, src_claim [t->st]);",
2280         "                                       fflush(stdout);",
2281         "                               }",
2282         "#endif",
2283         "                               reached[ot][t->st] = 1;",
2284         "                               reached[ot][tt] = 1;",
2285         "                       }",
2286         "#ifdef HAS_UNLESS",
2287         "                       else trpt->e_state = 0; /* undo */",
2288         "#endif",
2289
2290         "                       if (_m>_n||(_n>3&&_m!=0)) _n=_m;",
2291         "                       ((P0 *)this)->_p = tt;",
2292         "               } /* all options */",
2293
2294         "#ifdef RANDOMIZE",
2295         "               if (!t && ooi > 0)",    /* means we skipped some initial options */
2296         "               {       t = trans[ot][tt];",
2297         "#ifdef VERBOSE",
2298         "                       printf(\"randomizer: continue for %%d more\\n\", ooi);",
2299         "#endif",
2300         "                       goto DOMORE;",
2301         "               }",
2302         "#ifdef VERBOSE",
2303         "                 else",
2304         "                       printf(\"randomizer: done\\n\");",
2305         "#endif",
2306         "#endif",
2307
2308         "#ifndef NOFAIR",
2309         "               /* Fairness: undo Rule 2 */",
2310         "               if ((trpt->o_pm&32)",/* rule 2 was applied */
2311         "               &&  (trpt->o_pm&64))",/* by this process II */
2312         "               {       if (trpt->o_pm&1)",/* it didn't block */
2313         "                       {",
2314                 "#ifdef VERI",
2315         "                               if (now._cnt[now._a_t&1] == 1)",        /* NEW: 1 iso 0 */
2316         "                                       now._cnt[now._a_t&1] = 2;",     /* NEW: 2 iso 1*/
2317                 "#endif",
2318         "                               now._cnt[now._a_t&1] += 1;",
2319                 "#ifdef VERBOSE",
2320         "               printf(\"%%3d: proc %%d fairness \", depth, II);",
2321         "               printf(\"undo Rule 2, cnt=%%d, _a_t=%%d\\n\",",
2322         "                       now._cnt[now._a_t&1], now._a_t);",
2323                 "#endif",
2324         "                               trpt->o_pm &= ~(32|64);",
2325         "                       } else",        /* process blocked  */
2326         "                       {       if (_n > 0)", /* a prev proc didn't */
2327         "                               {",     /* start over */
2328         "                                       trpt->o_pm &= ~64;",
2329         "                                       II = From+1;",
2330         "               }       }       }",
2331         "#endif",
2332
2333         "#ifdef VERI",
2334         "               if (II == 0) break;     /* never claim */",
2335         "#endif",
2336         "       } /* all processes */",
2337
2338         "#ifndef NOFAIR",
2339         "       /* Fairness: undo Rule 2 */",
2340         "       if (trpt->o_pm&32)      /* remains if proc blocked */",
2341         "       {",
2342                 "#ifdef VERI",
2343         "               if (now._cnt[now._a_t&1] == 1)",        /* NEW: 1 iso 0 */
2344         "                       now._cnt[now._a_t&1] = 2;",     /* NEW: 2 iso 1 */
2345                 "#endif",
2346         "               now._cnt[now._a_t&1] += 1;",
2347                 "#ifdef VERBOSE",
2348         "               printf(\"%%3d: proc -- fairness \", depth);",
2349         "               printf(\"undo Rule 2, cnt=%%d, _a_t=%%d\\n\",",
2350         "                       now._cnt[now._a_t&1], now._a_t);",
2351                 "#endif",
2352         "               trpt->o_pm &= ~32;",
2353         "       }",
2354 "#ifndef NP",
2355         /* 12/97 non-progress cycles cannot be created
2356          * by stuttering extension, here or elsewhere
2357          */
2358         "       if (fairness",
2359         "       &&  _n == 0             /* nobody moved */",
2360                 "#ifdef VERI",
2361                 "       && !(trpt->tau&4)       /* in program move */",
2362                 "#endif",
2363         "       && !(trpt->tau&8)       /* not an atomic one */",
2364                 "#ifdef OTIM",
2365                 "       && ((trpt->tau&1) || endstate())",
2366                 "#else",
2367                         "#ifdef ETIM",
2368                         "       &&  (trpt->tau&1)       /* already tried timeout */",
2369                         "#endif",
2370                 "#endif",
2371                 "#ifndef NOREDUCE",
2372                 "       /* see below  */",
2373                 "       && !((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
2374                 "#endif",
2375         "       && now._cnt[now._a_t&1] > 0)    /* needed more procs */",
2376         "       {       depth++; trpt++;",
2377         "               trpt->o_pm |= 128 | ((trpt-1)->o_pm&(2|4));",
2378         "               trpt->bup.oval = now._cnt[now._a_t&1];",
2379         "               now._cnt[now._a_t&1] = 1;",
2380                 "#ifdef VERI",
2381         "               trpt->tau = 4;",
2382                 "#else",
2383         "               trpt->tau = 0;",
2384                 "#endif",
2385         "               From = now._nr_pr-1; To = BASE;",
2386                 "#if defined(VERBOSE) || defined(CHECK)",
2387         "               printf(\"%%3d: fairness default move \", depth);",
2388         "               printf(\"(all procs block)\\n\");",
2389                 "#endif",
2390         "               goto Down;",
2391         "       }",
2392 "#endif",
2393         "Q999:  /* returns here with _n>0 when done */;",
2394
2395         "       if (trpt->o_pm&8)",
2396         "       {       now._a_t &= ~2;",
2397         "               now._cnt[now._a_t&1] = 0;",
2398         "               trpt->o_pm &= ~8;",
2399                 "#ifdef VERBOSE",
2400         "               printf(\"%%3d: fairness undo Rule 1, _a_t=%%d\\n\",",
2401         "                       depth, now._a_t);",
2402                 "#endif",
2403         "       }",
2404         "       if (trpt->o_pm&16)",
2405         "       {       now._a_t |= 2;",                /* restore a-bit */
2406         "               now._cnt[now._a_t&1] = 1;",     /* NEW: restore cnt */
2407         "               trpt->o_pm &= ~16;",
2408                 "#ifdef VERBOSE",
2409         "               printf(\"%%3d: fairness undo Rule 3, _a_t=%%d\\n\",",
2410         "                       depth, now._a_t);",
2411                 "#endif",
2412         "       }",
2413         "#endif",
2414
2415         "#ifndef NOREDUCE",
2416 "#ifdef SAFETY",
2417         "       /* preselected move - no successors outside stack */",
2418         "       if ((trpt->tau&32) && !(trpt->tau&64))",
2419         "       {       From = now._nr_pr-1; To = BASE;",
2420                 "#ifdef DEBUG",
2421         "       printf(\"%%3d: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
2422         "       depth, II+1, _n, trpt->tau);",
2423                 "#endif",
2424         "               _n = 0; trpt->tau &= ~(16|32|64);",
2425         "               if (II >= BASE) /* II already decremented */",
2426         "                       goto Resume;",
2427         "               else",
2428         "                       goto Again;",
2429         "       }",
2430 "#else",
2431         "       /* at least one move that was preselected at this */",
2432         "       /* level, blocked or truncated at the next level  */",
2433         "/* implied: #ifdef FULLSTACK */",
2434         "       if ((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
2435         "       {",
2436                 "#ifdef DEBUG",
2437         "       printf(\"%%3d: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
2438         "       depth, II+1, (int) _n, trpt->tau);",
2439                 "#endif",
2440         "               if (a_cycles && (trpt->tau&16))",
2441         "               {       if (!(now._a_t&1))",
2442         "                       {",
2443                 "#ifdef DEBUG",
2444         "       printf(\"%%3d: setting proviso bit\\n\", depth);",
2445                 "#endif",
2446         "#ifndef BITSTATE",
2447                 "#ifdef MA",
2448                         "#ifdef VERI",
2449         "                       (trpt-1)->proviso = 1;",
2450                         "#else",
2451         "                       trpt->proviso = 1;",
2452                         "#endif",
2453                 "#else",
2454                         "#ifdef VERI",
2455         "                       if ((trpt-1)->ostate)",
2456         "                       ((char *)&((trpt-1)->ostate->state))[0] |= 128;",
2457                         "#else",
2458         "                       ((char *)&(trpt->ostate->state))[0] |= 128;",
2459                         "#endif",
2460                 "#endif",
2461         "#else",
2462                 "#ifdef VERI",
2463         "                       if ((trpt-1)->ostate)",
2464         "                       (trpt-1)->ostate->proviso = 1;",
2465                 "#else",
2466         "                       trpt->ostate->proviso = 1;",
2467                 "#endif",
2468         "#endif",
2469         "                               From = now._nr_pr-1; To = BASE;",
2470         "                               _n = 0; trpt->tau &= ~(16|32|64);",
2471         "                               goto Again; /* do full search */",
2472         "                       } /* else accept reduction */",
2473         "               } else",
2474         "               {       From = now._nr_pr-1; To = BASE;",
2475         "                       _n = 0; trpt->tau &= ~(16|32|64);",
2476         "                       if (II >= BASE) /* already decremented */",
2477         "                               goto Resume;",
2478         "                       else",
2479         "                               goto Again;",
2480         "       }       }",
2481         "/* #endif */",
2482 "#endif",
2483         "#endif",
2484
2485         "       if (_n == 0 || ((trpt->tau&4) && (trpt->tau&2)))",
2486         "       {",
2487                 "#ifdef DEBUG",
2488         "       printf(\"%%3d: no move [II=%%d, tau=%%d, boq=%%d]\\n\",",
2489         "                depth, II, trpt->tau, boq);",
2490                 "#endif",
2491         "#if SYNC",
2492         "               /* ok if a rendez-vous fails: */",
2493         "               if (boq != -1) goto Done;",
2494         "#endif",
2495         "               /* ok if no procs or we're at maxdepth */",
2496         "               if ((now._nr_pr == 0 && (!strict || qs_empty()))",
2497         "#ifdef OTIM",
2498         "               ||  endstate()",
2499         "#endif",
2500         "               ||  depth >= maxdepth-1) goto Done;",
2501
2502         "               if ((trpt->tau&8) && !(trpt->tau&4))",
2503         "               {       trpt->tau &= ~(1|8);",
2504         "                       /* 1=timeout, 8=atomic */",
2505         "                       From = now._nr_pr-1; To = BASE;",
2506                 "#ifdef DEBUG",
2507         "               printf(\"%%3d: atomic step proc %%d \", depth, II+1);",
2508         "               printf(\"unexecutable\\n\");",
2509                 "#endif",
2510         "#ifdef VERI",
2511         "                       trpt->tau |= 4; /* switch to claim */",
2512         "#endif",
2513         "                       goto AllOver;",
2514         "               }",
2515
2516         "#ifdef ETIM",
2517         "               if (!(trpt->tau&1)) /* didn't try timeout yet */",
2518         "               {",
2519         "#ifdef VERI",
2520         "                       if (trpt->tau&4)",
2521         "                       {",
2522                 "#ifndef NTIM",
2523         "                               if (trpt->tau&2) /* requested */",
2524                 "#endif",
2525         "                               {       trpt->tau |=  1;",
2526         "                                       trpt->tau &= ~2;",
2527                                 "#ifdef DEBUG",
2528         "                               printf(\"%%d: timeout\\n\", depth);",
2529                                 "#endif",
2530         "                                       goto Stutter;",
2531         "                       }       }",
2532         "                       else",
2533         "                       {       /* only claim can enable timeout */",
2534         "                               if ((trpt->tau&8)",
2535         "                               &&  !((trpt-1)->tau&4))",
2536         "/* blocks inside an atomic */          goto BreakOut;",
2537                                 "#ifdef DEBUG",
2538         "                               printf(\"%%d: req timeout\\n\",",
2539         "                                       depth);",
2540                                 "#endif",
2541         "                               (trpt-1)->tau |= 2; /* request */",
2542         "                               goto Up;",
2543         "                       }",
2544         "#else",
2545
2546                                 "#ifdef DEBUG",
2547         "                       printf(\"%%d: timeout\\n\", depth);",
2548                                 "#endif",
2549         "                       trpt->tau |=  1;",
2550         "                       goto Again;",
2551         "#endif",
2552         "               }",
2553         "#endif",
2554
2555         /* old location of atomic block code */
2556         "#ifdef VERI",
2557         "BreakOut:",
2558                 "#ifndef NOSTUTTER",
2559         "               if (!(trpt->tau&4))",
2560         "               {       trpt->tau |= 4;   /* claim stuttering */",
2561         "                       trpt->tau |= 128; /* stutter mark */",
2562                                 "#ifdef DEBUG",
2563         "                       printf(\"%%d: claim stutter\\n\", depth);",
2564                                 "#endif",
2565         "                       goto Stutter;",
2566         "               }",
2567                 "#else",
2568         "               ;",
2569                 "#endif",
2570         "#else",
2571         "               if (!noends && !a_cycles && !endstate())",
2572         "               {       depth--; trpt--;        /* new 4.2.3 */",
2573         "                       uerror(\"invalid end state\");",
2574         "                       depth++; trpt++;",
2575         "               }",
2576                 "#ifndef NOSTUTTER",
2577         "               else if (a_cycles && (trpt->o_pm&2)) /* new 4.2.4 */",
2578         "               {       depth--; trpt--;",
2579         "                       uerror(\"accept stutter\");",
2580         "                       depth++; trpt++;",
2581         "               }",
2582                 "#endif",
2583         "#endif",
2584         "       }",
2585         "Done:",
2586         "       if (!(trpt->tau&8))     /* not in atomic seqs */",
2587         "       {",
2588         "#ifndef SAFETY",
2589         "               if (_n != 0",           /* we made a move */
2590                 "#ifdef VERI",
2591         "               /* --after-- a program-step, i.e., */",
2592         "               /* after backtracking a claim-step */",
2593         "               && (trpt->tau&4)",
2594         "               /* with at least one running process */",
2595         "               /* unless in a stuttered accept state */",
2596         "               && ((now._nr_pr > 1) || (trpt->o_pm&2))",
2597                 "#endif",
2598         "               && !(now._a_t&1))",     /* not in 2nd DFS */
2599         "               {",
2600                 "#ifndef NOFAIR",
2601         "                       if (fairness)", /* implies a_cycles */
2602         "                       {",
2603                         "#ifdef VERBOSE",
2604         "                       printf(\"Consider check %%d %%d...\\n\",",
2605         "                               now._a_t, now._cnt[0]);",
2606                         "#endif",
2607 #if 0
2608                 the a-bit is set, which means that the fairness
2609                 counter is running -- it was started in an accepting state.
2610                 we check that the counter reached 1, which means that all
2611                 processes moved least once.
2612                 this means we can start the search for cycles -
2613                 to be able to return to this state, we should be able to
2614                 run down the counter to 1 again -- which implies a visit to
2615                 the accepting state -- even though the Seed state for this
2616                 search is itself not necessarily accepting
2617 #endif
2618         "                               if ((now._a_t&2) /* A-bit */",
2619         "                               &&  (now._cnt[0] == 1))",
2620         "                                       checkcycles();",
2621         "                       } else",
2622                 "#endif",
2623         "                       if (a_cycles && (trpt->o_pm&2))",
2624         "                               checkcycles();",
2625         "               }",
2626         "#endif",
2627 "#ifndef MA",
2628         "#if defined(FULLSTACK) || defined(CNTRSTACK)",
2629         "#ifdef VERI",
2630         "               if (boq == -1",
2631         "               &&  (((trpt->tau&4) && !(trpt->tau&128))",
2632         "               ||  ( (trpt-1)->tau&128)))",
2633         "#else",
2634         "               if (boq == -1)",
2635         "#endif",
2636         "               {",
2637                 "#ifdef DEBUG2",
2638                 "#if defined(FULLSTACK)",
2639         "                       printf(\"%%d: zapping %%u (%%d)\\n\",",
2640         "                               depth, trpt->ostate,",
2641         "                       (trpt->ostate)?trpt->ostate->tagged:0);",
2642                 "#endif",
2643                 "#endif",
2644         "                       onstack_zap();",
2645         "               }",
2646         "#endif",
2647 "#else",
2648         "#ifdef VERI",
2649         "               if (boq == -1",
2650         "               &&  (((trpt->tau&4) && !(trpt->tau&128))",
2651         "               ||  ( (trpt-1)->tau&128)))",
2652         "#else",
2653         "               if (boq == -1)",
2654         "#endif",
2655         "               {",
2656                 "#ifdef DEBUG",
2657         "                       printf(\"%%d: zapping\\n\", depth);",
2658                 "#endif",
2659         "                       onstack_zap();",
2660                 "#ifndef NOREDUCE",
2661         "                       if (trpt->proviso)",
2662         "                       gstore((char *) &now, vsize, 1);",
2663                 "#endif",
2664         "               }",
2665 "#endif",
2666         "       }",
2667         "       if (depth > 0) goto Up;",
2668         "}\n",
2669         "#else",
2670         "void new_state(void) { /* place holder */ }",
2671         "#endif",       /* BFS */
2672         "",
2673         "void",
2674         "assert(int a, char *s, int ii, int tt, Trans *t)",
2675         "{",
2676         "       if (!a && !noasserts)",
2677         "       {       char bad[1024];",
2678         "               strcpy(bad, \"assertion violated \");",
2679         "               if (strlen(s) > 1000)",
2680         "               {       strncpy(&bad[19], (const char *) s, 1000);",
2681         "                       bad[1019] = '\\0';",
2682         "               } else",
2683         "                       strcpy(&bad[19], s);",
2684         "               uerror(bad);",
2685         "       }",
2686         "}",
2687         "#ifndef NOBOUNDCHECK",
2688         "int",
2689         "Boundcheck(int x, int y, int a1, int a2, Trans *a3)",
2690         "{",
2691         "       assert((x >= 0 && x < y), \"- invalid array index\",",
2692         "               a1, a2, a3);",
2693         "       return x;",
2694         "}",
2695         "#endif",
2696         "void",
2697         "wrap_stats(void)",
2698         "{",
2699         "       if (nShadow>0)",
2700         "         printf(\"%%8g states, stored (%%g visited)\\n\",",
2701         "                       nstates - nShadow, nstates);",
2702         "       else",
2703         "         printf(\"%%8g states, stored\\n\", nstates);",
2704         "#ifdef BFS",
2705         "#if SYNC",
2706         "       printf(\"       %%8g nominal states (- rv and atomic)\\n\", nstates-midrv-nlinks+revrv);",
2707         "       printf(\"       %%8g rvs succeeded\\n\", midrv-failedrv);",
2708         "#else",
2709         "       printf(\"       %%8g nominal states (stored-atomic)\\n\", nstates-nlinks);",
2710         "#endif",
2711         "#ifdef DEBUG",
2712         "       printf(\"       %%8g midrv\\n\", midrv);",
2713         "       printf(\"       %%8g failedrv\\n\", failedrv);",
2714         "       printf(\"       %%8g revrv\\n\", revrv);",
2715         "#endif",
2716         "#endif",
2717         "       printf(\"%%8g states, matched\\n\", truncs);",
2718         "#ifdef CHECK",
2719         "       printf(\"%%8g matches within stack\\n\",truncs2);",
2720         "#endif",
2721         "       if (nShadow>0)",
2722         "       printf(\"%%8g transitions (= visited+matched)\\n\",",
2723         "               nstates+truncs);",
2724         "       else",
2725         "       printf(\"%%8g transitions (= stored+matched)\\n\",",
2726         "               nstates+truncs);",
2727         "       printf(\"%%8g atomic steps\\n\", nlinks);",
2728         "       if (nlost) printf(\"%%g lost messages\\n\", (double) nlost);",
2729         "",
2730         "#ifndef BITSTATE",
2731         "       printf(\"hash conflicts: %%g (resolved)\\n\", hcmp);",
2732         "#else",
2733                 "#ifdef CHECK",
2734                 "       printf(\"%%8g states allocated for dfs stack\\n\", ngrabs);",
2735                 "#endif",
2736         "       printf(\"\\nhash factor: %%4g (best if > 100.)\\n\\n\",",
2737         "               (double)(1<<(ssize-8)) / (double) nstates * 256.0);",
2738         "       printf(\"bits set per state: %%u (-k%%u)\\n\", hfns, hfns);",
2739         "#if 0",
2740 #ifndef POWOW
2741         "       if (udmem)",
2742         "       printf(\"total bits available: %%8g (-M%%ld)\\n\",",
2743         "               ((double) udmem) * 8.0, udmem/(1024L*1024L));",
2744         "       else",
2745 #endif
2746         "       printf(\"total bits available: %%8g (-w%%d)\\n\",",
2747         "               ((double) (1L << (ssize-4)) * 16.0), ssize);",
2748         "#endif",
2749 "#ifdef COVEST",
2750         "       /* this code requires compilation with -lm on some systems */",
2751         "       {       double pow(double, double);",
2752         "               double log(double);",
2753         "               unsigned int best_k;",
2754         "               double i, n = 30000.0L;",
2755         "               double f, p, q, m, c, est = 0.0L, k = (double)hfns;",
2756         "               c = (double) nstates / n;",
2757         "               m = (double) (1<<(ssize-8)) * 256.0L / c;",
2758         "               p = 1.0L - (k / m);  q = 1.0L;",
2759         "               for (i = 0.0L; i - est < n; i += 1.0L)",
2760         "               {       q *= p;",
2761         "                       est += pow(1.0L - q, k);",
2762         "               }",
2763         "               f = m/i;",
2764         "               est *= c;",
2765         "               i *= c;",
2766         "               /* account for loss from enhanced double hashing */",
2767         "               if (hfns > 2) est += i * pow(0.5, (double) ssize * 2.0);",
2768         "",
2769         "               if (f < 1.134) best_k = 1;",
2770         "               else if (f < 2.348) best_k = 2;",
2771         "               else if (f < 3.644) best_k = 3;",
2772         "               else best_k = (unsigned int) (pow(3.8L,1.0L/(f+4.2L))*f*.69315L + 0.99999999L);",
2773         "",
2774         "               if (best_k != hfns && best_k > ssize)",
2775         "                       best_k = (unsigned int) 1.0 + ssize/log((double)best_k / (double)ssize + 3.0);",
2776         "",
2777         "               if (best_k > 32)",
2778         "                       best_k = 1 + (unsigned int) (32.0/log((double)best_k/35.0));",
2779         "",
2780         "               if (est * (double) nstates < 1.0)",
2781         "               {       printf(\"prob. of omissions: negligible\\n\");",
2782         "                       return; /* no hints needed */",
2783         "               }",
2784         "",
2785         "               if (best_k != hfns)",
2786         "               {       printf(\"hint: repeating the search with -k%%u \", best_k);",
2787         "                       printf(\"may increase accuracy\\n\");",
2788         "               } else",
2789         "               {       printf(\"hint: the current setting for -k (-k%%d) \", hfns);",
2790         "                       printf(\"is likely to be optimal for -w%%d\\n\", ssize);",
2791         "               }",
2792         "               if (ssize < 32)",
2793         "               {       printf(\"hint: increasing -w above -w%%d \", ssize);",
2794         "                       printf(\"will increase accuracy (max is -w34)\\n\");",
2795         "                       printf(\"(in xspin, increase Estimated State Space Size)\\n\");",
2796         "       }       }",
2797 "#endif",
2798         "#endif",
2799         "}",
2800         "void",
2801         "wrapup(void)",
2802         "{",
2803         "#if defined(BITSTATE) || !defined(NOCOMP)",
2804         "       double nr1, nr2, nr3 = 0.0, nr4, nr5 = 0.0;",
2805         "#if !defined(MA) && (defined(MEMCNT) || defined(MEMLIM))",
2806         "       int mverbose = 1;",
2807         "#else",
2808         "       int mverbose = verbose;",
2809         "#endif",
2810         "#endif",
2811
2812         "       signal(SIGINT, SIG_DFL);",
2813         "       printf(\"(%%s)\\n\", Version);",
2814         "       if (!done) printf(\"Warning: Search not completed\\n\");",
2815         "#ifdef SC",
2816         "       (void) unlink((const char *)stackfile);",
2817         "#endif",
2818         "#ifdef BFS",
2819         "       printf(\"       + Using Breadth-First Search\\n\");",
2820         "#endif",
2821         "#ifndef NOREDUCE",
2822         "       printf(\"       + Partial Order Reduction\\n\");",
2823         "#endif",
2824 #if 0
2825         "#ifdef Q_PROVISO",
2826         "       printf(\"       + Queue Proviso\\n\");",
2827         "#endif",
2828 #endif
2829         "#ifdef COLLAPSE",
2830         "       printf(\"       + Compression\\n\");",
2831         "#endif",
2832         "#ifdef MA",
2833         "       printf(\"       + Graph Encoding (-DMA=%%d)\\n\", MA);",
2834         "#ifdef R_XPT",
2835         "       printf(\"         Restarted from checkpoint %%s.xpt\\n\", Source);",
2836         "#endif",
2837         "#endif",
2838         "#ifdef CHECK",
2839                 "#ifdef FULLSTACK",
2840         "       printf(\"       + FullStack Matching\\n\");",
2841                 "#endif",
2842                 "#ifdef CNTRSTACK",
2843         "       printf(\"       + CntrStack Matching\\n\");",
2844                 "#endif",
2845         "#endif",
2846         "#ifdef BITSTATE",
2847         "       printf(\"\\nBit statespace search for:\\n\");",
2848         "#else",
2849                 "#ifdef HC",
2850         "       printf(\"\\nHash-Compact %%d search for:\\n\", HC);",
2851                 "#else",
2852         "       printf(\"\\nFull statespace search for:\\n\");",
2853                 "#endif",
2854         "#endif",
2855         "#ifdef EVENT_TRACE",
2856         "#ifdef NEGATED_TRACE",
2857         "       printf(\"\tnotrace assertion  \t+\\n\");",
2858         "#else",
2859         "       printf(\"\ttrace assertion    \t+\\n\");",
2860         "#endif",
2861         "#endif",
2862         "#ifdef VERI",
2863         "       printf(\"\tnever claim         \t+\\n\");",
2864         "       printf(\"\tassertion violations\t\");",
2865         "       if (noasserts)",
2866         "               printf(\"- (disabled by -A flag)\\n\");",
2867         "       else",
2868         "               printf(\"+ (if within scope of claim)\\n\");",
2869         "#else",
2870                 "#ifdef NOCLAIM",
2871         "       printf(\"\tnever claim         \t- (not selected)\\n\");",
2872                 "#else",
2873         "       printf(\"\tnever claim         \t- (none specified)\\n\");",
2874                 "#endif",
2875         "       printf(\"\tassertion violations\t\");",
2876         "       if (noasserts)",
2877         "               printf(\"- (disabled by -A flag)\\n\");",
2878         "       else",
2879         "               printf(\"+\\n\");",
2880         "#endif",
2881         "#ifndef SAFETY",
2882                 "#ifdef NP",
2883         "       printf(\"\tnon-progress cycles \t\");",
2884                 "#else",
2885         "       printf(\"\tacceptance   cycles \t\");",
2886                 "#endif",
2887         "       if (a_cycles)",
2888         "               printf(\"+ (fairness %%sabled)\\n\",",
2889         "                       fairness?\"en\":\"dis\");",
2890         "       else printf(\"- (not selected)\\n\");",
2891         "#else",
2892         "       printf(\"\tcycle checks       \t- (disabled by -DSAFETY)\\n\");",
2893         "#endif",
2894         "#ifdef VERI",
2895         "       printf(\"\tinvalid end states\t- \");",
2896         "       printf(\"(disabled by \");",
2897         "       if (noends)",
2898         "               printf(\"-E flag)\\n\\n\");",
2899         "       else",
2900         "               printf(\"never claim)\\n\\n\");",
2901         "#else",
2902         "       printf(\"\tinvalid end states\t\");",
2903         "       if (noends)",
2904         "               printf(\"- (disabled by -E flag)\\n\\n\");",
2905         "       else",
2906         "               printf(\"+\\n\\n\");",
2907         "#endif",
2908         "       printf(\"State-vector %%d byte, depth reached %%d\", ",
2909         "                                       hmax, mreached);",
2910         "       printf(\", errors: %%d\\n\", errors);",
2911         "#ifdef MA",
2912         "       if (done)",
2913         "       {       extern void dfa_stats(void);",
2914         "               if (maxgs+a_cycles+2 < MA)",
2915         "               printf(\"MA stats: -DMA=%%d is sufficient\\n\",",
2916         "                       maxgs+a_cycles+2);",
2917         "               dfa_stats();",
2918         "       }",
2919         "#endif",
2920         "       wrap_stats();",
2921         "#ifdef CHECK",
2922         "       printf(\"stackframes: %%d/%%d\\n\\n\", smax, svmax);",
2923         "       printf(\"stats: fa %%d, fh %%d, zh %%d, zn %%d - \",",
2924         "               Fa, Fh, Zh, Zn);",
2925         "       printf(\"check %%d holds %%d\\n\", Ccheck, Cholds);",
2926         "       printf(\"stack stats: puts %%d, probes %%d, zaps %%d\\n\",",
2927         "               PUT, PROBE, ZAPS);",
2928         "#else",
2929         "       printf(\"\\n\");",
2930         "#endif",
2931         "",
2932         "#if defined(BITSTATE) || !defined(NOCOMP)",
2933         "       nr1 = (nstates-nShadow)*",
2934         "             (double)(hmax+sizeof(struct H_el)-sizeof(unsigned));",
2935                 "#ifdef BFS",
2936         "       nr2 = 0.0;",
2937                 "#else",
2938         "       nr2 = (double) ((maxdepth+3)*sizeof(Trail));",
2939                 "#endif",
2940
2941                 "#ifndef BITSTATE",
2942                         "#if !defined(MA) || defined(COLLAPSE)",
2943         "       nr3 = (double) (1L<<ssize)*sizeof(struct H_el *);",
2944                         "#endif",
2945                 "#else",
2946 #ifndef POWOW
2947         "       if (udmem)",
2948         "               nr3 = (double) (udmem);",
2949         "       else",
2950 #endif
2951         "       nr3 = (double) (1L<<(ssize-3));",
2952                         "#ifdef CNTRSTACK",
2953         "       nr3 += (double) (1L<<(ssize-3));",
2954                         "#endif",
2955                         "#ifdef FULLSTACK",
2956         "       nr5 = (double) (maxdepth*sizeof(struct H_el *));",
2957                         "#endif",
2958                 "#endif",
2959         "       nr4 = (double) (svmax * (sizeof(Svtack) + hmax))",
2960         "           + (double) (smax * (sizeof(Stack) + Maxbody));",
2961                 "#ifndef MA",
2962         "       if (mverbose || memcnt < nr1+nr2+nr3+nr4+nr5)",
2963                 "#endif",
2964         "       { double remainder = memcnt;",
2965         "         double tmp_nr = memcnt-nr3-nr4-(nr2-fragment)-nr5;",
2966         "               if (tmp_nr < 0.0) tmp_nr = 0.;",
2967         "               printf(\"Stats on memory usage (in Megabytes):\\n\");",
2968         "               printf(\"%%-6.3f\tequivalent memory usage for states\",",
2969         "                       nr1/1000000.);",
2970         "               printf(\" (stored*(State-vector + overhead))\\n\");",
2971                 "#ifdef BITSTATE",
2972 #ifndef POWOW
2973         "               if (udmem)",
2974         "               printf(\"%%-6.3f\tmemory used for hash array (-M%%ld)\\n\",",
2975         "                       nr3/1000000., udmem/(1024L*1024L));",
2976         "               else",
2977 #endif
2978         "               printf(\"%%-6.3f\tmemory used for hash array (-w%%d)\\n\",",
2979         "                       nr3/1000000., ssize);",
2980         "               if (nr5 > 0.0)",
2981         "               printf(\"%%-6.3f\tmemory used for bit stack\\n\",",
2982         "                       nr5/1000000.);",
2983         "               remainder = remainder - nr3 - nr5;",
2984                 "#else",
2985         "               printf(\"%%-6.3f\tactual memory usage for states\",",
2986         "                       tmp_nr/1000000.);",
2987         "               remainder = remainder - tmp_nr;",
2988         "               printf(\" (\");",
2989         "               if (tmp_nr > 0.)",
2990         "               {       if (tmp_nr > nr1) printf(\"unsuccessful \");",
2991         "                       printf(\"compression: %%.2f%%%%)\\n\",",
2992         "                               (100.0*tmp_nr)/nr1);",
2993         "               } else",
2994         "                       printf(\"less than 1k)\\n\");",
2995                         "#ifndef MA",
2996         "               if (tmp_nr > 0.)",
2997         "               {       printf(\"\tState-vector as stored = %%.0f byte\",",
2998         "                       (tmp_nr)/(nstates-nShadow) -",
2999         "                       (double) (sizeof(struct H_el) - sizeof(unsigned)));",
3000         "                       printf(\" + %%ld byte overhead\\n\",",
3001         "                       sizeof(struct H_el)-sizeof(unsigned));",
3002         "               }",
3003                         "#endif",
3004                         "#if !defined(MA) || defined(COLLAPSE)",
3005         "               printf(\"%%-6.3f\tmemory used for hash table (-w%%d)\\n\",",
3006         "                       nr3/1000000., ssize);",
3007         "               remainder = remainder - nr3;",
3008                         "#endif",
3009                 "#endif",
3010                 "#ifndef BFS",
3011         "               printf(\"%%-6.3f\tmemory used for DFS stack (-m%%ld)\\n\",",
3012         "                       nr2/1000000., maxdepth);",
3013         "               remainder = remainder - nr2;",
3014                 "#endif",
3015         "               if (remainder - fragment > 0.0)",
3016         "               printf(\"%%-6.3f\tother (proc and chan stacks)\\n\",",
3017         "                       (remainder-fragment)/1000000.);",
3018         "               if (fragment > 0.0)",
3019         "               printf(\"%%-6.3f\tmemory lost to fragmentation\\n\",",
3020         "                       fragment/1000000.);",
3021         "               printf(\"%%-6.3f\ttotal actual memory usage\\n\\n\",",
3022         "                       memcnt/1000000.);",
3023         "       }",
3024                 "#ifndef MA",
3025         "       else",
3026                 "#endif",
3027         "#endif",
3028                 "#ifndef MA",
3029         "               printf(\"%%-6.3f\tmemory usage (Mbyte)\\n\\n\",",
3030         "                       memcnt/1000000.);",
3031                 "#endif",
3032         "#ifdef COLLAPSE",
3033         "       printf(\"nr of templates: [ globals chans procs ]\\n\");",
3034         "       printf(\"collapse counts: [ \");",
3035         "       { int i; for (i = 0; i < 256+2; i++)",
3036         "               if (ncomps[i] != 0)",
3037         "                       printf(\"%%d \", ncomps[i]);",
3038         "               printf(\"]\\n\");",
3039         "       }",
3040         "#endif",
3041
3042         "       if ((done || verbose) && !no_rck) do_reach();",
3043         "#ifdef PEG",
3044         "       { int i;",
3045         "         printf(\"\\nPeg Counts (transitions executed):\\n\");",
3046         "         for (i = 1; i < NTRANS; i++)",
3047         "         {     if (peg[i]) putpeg(i, peg[i]);",
3048         "       } }",
3049         "#endif",
3050         "#ifdef VAR_RANGES",
3051         "       dumpranges();",
3052         "#endif",
3053         "#ifdef SVDUMP",
3054         "       if (vprefix > 0) close(svfd);",
3055         "#endif",
3056         "       pan_exit(0);",
3057         "}\n",
3058         "void",
3059         "stopped(int arg)",
3060         "{      printf(\"Interrupted\\n\");",
3061         "       wrapup();",
3062         "       pan_exit(0);",
3063         "}",
3064         "/*",
3065         " * based on Bob Jenkins hash-function from 1996",
3066         " * see: http://www.burtleburtle.net/bob/",
3067         " */",
3068         "",
3069 "#if defined(HASH64) || defined(WIN64)",
3070         /* 64-bit Jenkins hash: http://burtleburtle.net/bob/c/lookup8.c */
3071         "#define mix(a,b,c) \\",
3072         "{ a -= b; a -= c; a ^= (c>>43); \\",
3073         "  b -= c; b -= a; b ^= (a<<9);  \\",
3074         "  c -= a; c -= b; c ^= (b>>8);  \\",
3075         "  a -= b; a -= c; a ^= (c>>38); \\",
3076         "  b -= c; b -= a; b ^= (a<<23); \\",
3077         "  c -= a; c -= b; c ^= (b>>5);  \\",
3078         "  a -= b; a -= c; a ^= (c>>35); \\",
3079         "  b -= c; b -= a; b ^= (a<<49); \\",
3080         "  c -= a; c -= b; c ^= (b>>11); \\",
3081         "  a -= b; a -= c; a ^= (c>>12); \\",
3082         "  b -= c; b -= a; b ^= (a<<18); \\",
3083         "  c -= a; c -= b; c ^= (b>>22); \\",
3084         "}",
3085 "#else",
3086         "#define mix(a,b,c) \\",
3087         "{ a -= b; a -= c; a ^= (c>>13); \\",
3088         "  b -= c; b -= a; b ^= (a<<8);  \\",
3089         "  c -= a; c -= b; c ^= (b>>13); \\",
3090         "  a -= b; a -= c; a ^= (c>>12); \\",
3091         "  b -= c; b -= a; b ^= (a<<16); \\",
3092         "  c -= a; c -= b; c ^= (b>>5);  \\",
3093         "  a -= b; a -= c; a ^= (c>>3);  \\",
3094         "  b -= c; b -= a; b ^= (a<<10); \\",
3095         "  c -= a; c -= b; c ^= (b>>15); \\",
3096         "}",
3097 "#endif",
3098         "void",
3099         "d_hash(uchar *Cp, int Om)      /* double bit hash - Jenkins */",
3100         "{      unsigned long a = 0x9e3779b9, b, c = 0, len, length;",
3101         "       unsigned long *k = (unsigned long *) Cp;",
3102         "",
3103         "       length = len = (unsigned long) ((unsigned long) Om + WS-1)/WS;",
3104         "",
3105         "       b = HASH_CONST[HASH_NR];",
3106         "       while (len >= 3)",
3107         "       {       a += k[0];",
3108         "               b += k[1];",
3109         "               c += k[2];",
3110         "               mix(a,b,c);",
3111         "               k += 3; len -= 3;",
3112         "       }",
3113         "       c += length;",
3114         "       switch (len) {",
3115         "       case 2: b += k[1];",
3116         "       case 1: a += k[0];",
3117         "       }",
3118         "       mix(a,b,c);",
3119         "       j1 = c&nmask; j3 = a&7;",       /* 1st bit */
3120         "       j2 = b&nmask; j4 = (a>>3)&7;",  /* 2nd bit */
3121         "       K1 = c; K2 = b;",               /* no nmask */
3122         "}",
3123         "void",
3124         "s_hash(uchar *cp, int om)",
3125         "{      d_hash(cp, om); /* sets K1 and K2 */",
3126         "#ifdef BITSTATE",
3127         "       if (S_Tab == H_tab)",   /* state stack in bitstate search */
3128         "               j1 = K1 %% omaxdepth;",
3129         "       else",
3130         "#endif", /* if (S_Tab != H_Tab) */
3131         "               if (ssize < 8*WS)",
3132         "                       j1 = K1&mask;",
3133         "               else",
3134         "                       j1 = K1;",
3135         "}",
3136         "#ifndef RANDSTOR",
3137         "int *prerand;",
3138         "void",
3139         "inirand(void)",
3140         "{      int i;",
3141         "       srand(123);     /* fixed startpoint */",
3142         "       prerand = (int *) emalloc((omaxdepth+3)*sizeof(int));",
3143         "       for (i = 0; i < omaxdepth+3; i++)",
3144         "               prerand[i] = rand();",
3145         "}",
3146         "int",
3147         "pan_rand(void)",
3148         "{      if (!prerand) inirand();",
3149         "       return prerand[depth];",
3150         "}",
3151         "#endif",
3152         "",
3153         "int",
3154         "main(int argc, char *argv[])",
3155         "{      void to_compile(void);\n",
3156         "       efd = stderr;   /* default */",
3157         "#ifdef BITSTATE",
3158         "       bstore = bstore_reg; /* default */",
3159         "#endif",
3160         "       while (argc > 1 && argv[1][0] == '-')",
3161         "       {       switch (argv[1][1]) {",
3162         "#ifndef SAFETY",
3163                 "#ifdef NP",
3164         "               case 'a': fprintf(efd, \"error: -a disabled\");",
3165         "                         usage(efd); break;",
3166                 "#else",
3167         "               case 'a': a_cycles = 1; break;",
3168                 "#endif",
3169         "#endif",
3170         "               case 'A': noasserts = 1; break;",
3171         "               case 'b': bounded = 1; break;",
3172         "               case 'c': upto  = atoi(&argv[1][2]); break;",
3173         "               case 'd': state_tables++; break;",
3174         "               case 'e': every_error = 1; Nr_Trails = 1; break;",
3175         "               case 'E': noends = 1; break;",
3176         "#ifdef SC",
3177         "               case 'F': if (strlen(argv[1]) > 2)",
3178         "                               stackfile = &argv[1][2];",
3179         "                         break;",
3180         "#endif",
3181         "#if !defined(SAFETY) && !defined(NOFAIR)",
3182         "               case 'f': fairness = 1; break;",
3183         "#endif",
3184         "               case 'h': if (!argv[1][2]) usage(efd); else",
3185         "                         HASH_NR = atoi(&argv[1][2])%%33; break;",
3186         "               case 'I': iterative = 2; every_error = 1; break;",
3187         "               case 'i': iterative = 1; every_error = 1; break;",
3188         "               case 'J': like_java = 1; break; /* Klaus Havelund */",
3189         "#ifdef BITSTATE",
3190         "               case 'k': hfns = atoi(&argv[1][2]); break;",
3191         "#endif",
3192         "#ifndef SAFETY",
3193                 "#ifdef NP",
3194         "               case 'l': a_cycles = 1; break;",
3195                 "#else",
3196         "               case 'l': fprintf(efd, \"error: -l disabled\");",
3197         "                         usage(efd); break;",
3198                 "#endif",
3199         "#endif",
3200 #ifndef POWOW
3201         "#ifdef BITSTATE",
3202         "               case 'M': udmem = atoi(&argv[1][2]); break;",
3203         "               case 'G': udmem = atoi(&argv[1][2]); udmem *= 1024; break;",
3204         "#else",
3205         "               case 'M': case 'G':",
3206         "                         fprintf(stderr, \"-M and -G affect only -DBITSTATE\\n\");",
3207         "                         break;",
3208         "#endif",
3209 #endif
3210         "               case 'm': maxdepth = atoi(&argv[1][2]); break;",
3211         "               case 'n': no_rck = 1; break;",
3212         "#ifdef SVDUMP",
3213         "               case 'p': vprefix = atoi(&argv[1][2]); break;",
3214         "#endif",
3215         "               case 'q': strict = 1; break;",
3216         "#ifdef HAS_CODE",
3217         "               case 'r':",
3218         "samething:               readtrail = 1;",
3219         "                         if (isdigit(argv[1][2]))",
3220         "                               whichtrail = atoi(&argv[1][2]);",
3221         "                         break;",
3222         "               case 'P': readtrail = 1; onlyproc = atoi(&argv[1][2]); break;",
3223         "               case 'C': coltrace = 1; goto samething;",
3224         "               case 'g': gui = 1; goto samething;",
3225         "               case 'S': silent = 1; break;",
3226         "#endif",
3227         "               case 'R': Nrun = atoi(&argv[1][2]); break;",
3228         "#ifdef BITSTATE",
3229         "               case 's': hfns = 1; break;",
3230         "#endif",
3231         "               case 'T': TMODE = 0444; break;",
3232         "               case 't': if (argv[1][2]) tprefix = &argv[1][2]; break;",
3233         "               case 'V': printf(\"Generated by %%s\\n\", Version);",
3234         "                         to_compile(); pan_exit(0); break;",
3235         "               case 'v': verbose = 1; break;",
3236         "               case 'w': ssize = atoi(&argv[1][2]); break;",
3237         "               case 'Y': signoff = 1; break;",
3238         "               case 'X': efd = stdout; break;",
3239         "               default : fprintf(efd, \"saw option -%%c\\n\", argv[1][1]); usage(efd); break;",
3240         "               }",
3241         "               argc--; argv++;",
3242         "       }",
3243         "       if (iterative && TMODE != 0666)",
3244         "       {       TMODE = 0666;",
3245         "               fprintf(efd, \"warning: -T ignored when -i or -I is used\\n\");",
3246         "       }",
3247         "#if defined(WIN32) || defined(WIN64)",
3248         "       if (TMODE == 0666)",
3249         "               TMODE = _S_IWRITE | _S_IREAD;",
3250         "       else",
3251         "               TMODE = _S_IREAD;",
3252         "#endif",
3253         "#ifdef OHASH",
3254         "       fprintf(efd, \"warning: -DOHASH no longer supported (directive ignored)\\n\");",
3255         "#endif",
3256         "#ifdef JHASH",
3257         "       fprintf(efd, \"warning: -DJHASH no longer supported (directive ignored)\\n\");",
3258         "#endif",
3259         "#ifdef HYBRID_HASH",
3260         "       fprintf(efd, \"warning: -DHYBRID_HASH no longer supported (directive ignored)\\n\");",
3261         "#endif",
3262         "#ifdef NOCOVEST",
3263         "       fprintf(efd, \"warning: -DNOCOVEST no longer supported (directive ignored)\\n\");",
3264         "#endif",
3265         "#ifdef BITSTATE",
3266         "#ifdef BCOMP",
3267         "       fprintf(efd, \"warning: -DBCOMP no longer supported (directive ignored)\\n\");",
3268         "#endif",
3269         "       if (hfns <= 0)",
3270         "       {       hfns = 1;",
3271         "               fprintf(efd, \"warning: using -k%%d as minimal usable value\\n\", hfns);",
3272         "       }",
3273         "#endif",
3274         "       omaxdepth = maxdepth;",
3275         "#ifdef BITSTATE",
3276         "       if (WS == 4 && ssize > 34)",    /* 32-bit word size */
3277         "       {       ssize = 34;",
3278         "               fprintf(efd, \"warning: using -w%%d as max usable value\\n\", ssize);",
3279         "/*",
3280         " *     -w35 would not work: 35-3 = 32 but 1^31 is the largest",
3281         " *     power of 2 that can be represented in an unsigned long",
3282         " */",
3283         "       }",
3284         "#else",
3285         "       if (WS == 4 && ssize > 27)",
3286         "       {       ssize = 27;",
3287         "               fprintf(efd, \"warning: using -w%%d as max usable value\\n\", ssize);",
3288         "/*",
3289         " *     for emalloc, the lookup table size multiplies by 4 for the pointers",
3290         " *     the largest power of 2 that can be represented in a ulong is 1^31",
3291         " *     hence the largest number of lookup table slots is 31-4 = 27",
3292         " */",
3293         "       }",
3294
3295         "#endif",
3296         "#ifdef SC",
3297         "       hiwater = HHH = maxdepth-10;",
3298         "       DDD = HHH/2;",
3299         "       if (!stackfile)",
3300         "       {       stackfile = (char *) emalloc(strlen(Source)+4+1);",
3301         "               sprintf(stackfile, \"%%s._s_\", Source);",
3302         "       }",
3303         "       if (iterative)",
3304         "       {       fprintf(efd, \"error: cannot use -i or -I with -DSC\\n\");",
3305         "               pan_exit(1);",
3306         "       }",
3307         "#endif",
3308
3309         "#if (defined(R_XPT) || defined(W_XPT)) && !defined(MA)",
3310         "       fprintf(efd, \"error: -D?_XPT requires -DMA\\n\");",
3311         "       exit(1);",
3312         "#endif",
3313
3314         "       if (iterative && a_cycles)",
3315         "       fprintf(efd, \"warning: -i or -I work for safety properties only\\n\");",
3316
3317         "#ifdef BFS",
3318         "#if defined(SC)",
3319         "       fprintf(efd, \"error: -DBFS not compatible with -DSC\\n\");",
3320         "       exit(1);",
3321         "#endif",
3322         "#if defined(HAS_LAST)",
3323         "       fprintf(efd, \"error: -DBFS not compatible with _last\\n\");",
3324         "       exit(1);",
3325         "#endif",
3326         "#if defined(REACH)",
3327         "       fprintf(efd, \"warning: -DREACH redundant when -DBFS is used\\n\");",
3328         "#endif",
3329         "#if defined(HAS_STACK)",
3330         "       fprintf(efd, \"error: cannot use UnMatched qualifier on c_track with BFS\\n\");",
3331         "       exit(1);",
3332         "#endif",
3333         "#endif",
3334
3335         "#if defined(MERGED) && defined(PEG)",
3336         "       fprintf(efd, \"error: to allow -DPEG use: spin -o3 -a %%s\\n\", Source);",
3337         "       fprintf(efd, \"       to turn off transition merge optimization\\n\");",
3338         "       pan_exit(1);",
3339         "#endif",
3340         "#ifdef HC",
3341                 "#ifdef NOCOMP",
3342         "       fprintf(efd, \"error: cannot combine -DHC and -DNOCOMP\\n\");",
3343         "       pan_exit(1);",
3344                 "#endif",
3345                 "#ifdef BITSTATE",
3346         "       fprintf(efd, \"error: cannot combine -DHC and -DBITSTATE\\n\");",
3347         "       pan_exit(1);",
3348                 "#endif",
3349         "#endif",
3350         "#if defined(SAFETY) && defined(NP)",
3351         "       fprintf(efd, \"error: cannot combine -DNP and -DSAFETY\\n\");",
3352         "       pan_exit(1);",
3353         "#endif",
3354         "#ifdef MA",
3355         "#ifdef BITSTATE",
3356         "       fprintf(efd, \"error: cannot combine -DMA and -DBITSTATE\\n\");",
3357         "       pan_exit(1);",
3358         "#endif",
3359         "       if (MA <= 0)",
3360         "       {       fprintf(efd, \"usage: -DMA=N with N > 0 and < VECTORSZ\\n\");",
3361         "               pan_exit(1);",
3362         "       }",
3363         "#endif",
3364         "#ifdef COLLAPSE",
3365                 "#if defined(BITSTATE)",
3366         "       fprintf(efd, \"error: cannot combine -DBITSTATE and -DCOLLAPSE\\n\");",
3367         "       pan_exit(1);",
3368                 "#endif",
3369                 "#if defined(NOCOMP)",
3370         "       fprintf(efd, \"error: cannot combine -DNOCOMP and -DCOLLAPSE\\n\");",
3371         "       pan_exit(1);",
3372                 "#endif",
3373         "#endif",
3374         "       if (maxdepth <= 0 || ssize <= 1) usage(efd);",
3375         "#if SYNC>0 && !defined(NOREDUCE)",
3376         "       if (a_cycles && fairness)",
3377         "       { fprintf(efd, \"error: p.o. reduction not compatible with \");",
3378         "         fprintf(efd, \"fairness (-f) in models\\n\");",
3379         "         fprintf(efd, \"       with rendezvous operations: \");",
3380         "         fprintf(efd, \"recompile with -DNOREDUCE\\n\");",
3381         "         pan_exit(1);",
3382         "       }",
3383         "#endif",
3384         "#if defined(REM_VARS) && !defined(NOREDUCE)",
3385         "       { fprintf(efd, \"warning: p.o. reduction not compatible with \");",
3386         "         fprintf(efd, \"remote varrefs (use -DNOREDUCE)\\n\");",
3387         "       }",
3388         "#endif",
3389         "#if defined(NOCOMP) && !defined(BITSTATE)",
3390         "       if (a_cycles)",
3391         "       { fprintf(efd, \"error: -DNOCOMP voids -l and -a\\n\");",
3392         "         pan_exit(1);",
3393         "       }",
3394         "#endif",
3395
3396         "#ifdef MEMLIM",        /* MEMLIM setting takes precedence */
3397                 "       memlim = (double) MEMLIM * (double) (1<<20);    /* size in Mbyte */",
3398         "#else",
3399                 "#ifdef MEMCNT",
3400                 "#if MEMCNT<31",
3401                 "       memlim  = (double) (1<<MEMCNT);",
3402                 "#else",
3403                 "       memlim  = (double) (1<<30);",
3404                 "       memlim *= (double) (1<<(MEMCNT-30));",
3405                 "#endif",
3406                 "#endif",
3407         "#endif",
3408
3409         "#ifndef BITSTATE",
3410         "       if (Nrun > 1) HASH_NR = Nrun - 1;",
3411         "#endif",
3412         "       if (Nrun < 1 || Nrun > 32)",
3413         "       {       fprintf(efd, \"error: invalid arg for -R\\n\");",
3414         "               usage(efd);",
3415         "       }",
3416         "#ifndef SAFETY",
3417         "       if (fairness && !a_cycles)",
3418         "       {       fprintf(efd, \"error: -f requires -a or -l\\n\");",
3419         "               usage(efd);",
3420         "       }",
3421                 "#if ACCEPT_LAB==0",
3422         "       if (a_cycles)",
3423                 "#ifndef VERI",
3424         "       {       fprintf(efd, \"error: no accept labels defined \");",
3425         "               fprintf(efd, \"in model (for option -a)\\n\");",
3426         "               usage(efd);",
3427         "       }",
3428                 "#else",
3429         "       {       fprintf(efd, \"warning: no explicit accept labels \");",
3430         "               fprintf(efd, \"defined in model (for -a)\\n\");",
3431         "       }",
3432                 "#endif",
3433                 "#endif",
3434         "#endif",
3435         "#if !defined(NOREDUCE)",
3436                 "#if defined(HAS_ENABLED)",
3437         "       fprintf(efd, \"error: reduced search precludes \");",
3438         "       fprintf(efd, \"use of 'enabled()'\\n\");",
3439         "       pan_exit(1);",
3440                 "#endif",
3441                 "#if defined(HAS_PCVALUE)",
3442         "       fprintf(efd, \"error: reduced search precludes \");",
3443         "       fprintf(efd, \"use of 'pcvalue()'\\n\");",
3444         "       pan_exit(1);",
3445                 "#endif",
3446                 "#if defined(HAS_BADELSE)",
3447         "       fprintf(efd, \"error: reduced search precludes \");",
3448         "       fprintf(efd, \"using 'else' combined with i/o stmnts\\n\");",
3449         "       pan_exit(1);",
3450                 "#endif",
3451                 "#if defined(HAS_LAST)",
3452         "       fprintf(efd, \"error: reduced search precludes \");",
3453         "       fprintf(efd, \"use of _last\\n\");",
3454         "       pan_exit(1);",
3455                 "#endif",
3456         "#endif",
3457
3458         "#if SYNC>0 && !defined(NOREDUCE)",
3459                 "#ifdef HAS_UNLESS",
3460         "       fprintf(efd, \"warning: use of a rendezvous stmnts in the escape\\n\");",
3461         "       fprintf(efd, \"\tof an unless clause, if present, could make p.o. reduction\\n\");",
3462         "       fprintf(efd, \"\tinvalid (use -DNOREDUCE to avoid this)\\n\");",
3463                         "#ifdef BFS",
3464         "       fprintf(efd, \"\t(this type of rv is also not compatible with -DBFS)\\n\");",
3465                         "#endif",
3466                 "#endif",
3467         "#endif",
3468         "#if SYNC>0 && defined(BFS)",
3469         "       fprintf(efd, \"warning: use of rendezvous in BFS mode \");",
3470         "       fprintf(efd, \"does not preserve all invalid endstates\\n\");",
3471         "#endif",
3472         "#if !defined(REACH) && !defined(BITSTATE)",
3473         "       if (iterative != 0 && a_cycles == 0)",
3474         "       fprintf(efd, \"warning: -i and -I need -DREACH to work accurately\\n\");",
3475         "#endif",
3476         "#if defined(BITSTATE) && defined(REACH)",
3477         "       fprintf(efd, \"warning: -DREACH voided by -DBITSTATE\\n\");",
3478         "#endif",
3479         "#if defined(MA) && defined(REACH)",
3480         "       fprintf(efd, \"warning: -DREACH voided by -DMA\\n\");",
3481         "#endif",
3482         "#if defined(FULLSTACK) && defined(CNTRSTACK)",
3483         "       fprintf(efd, \"error: cannot combine\");",
3484         "       fprintf(efd, \" -DFULLSTACK and -DCNTRSTACK\\n\");",
3485         "       pan_exit(1);",
3486         "#endif",
3487         "#if defined(VERI)",
3488                 "#if ACCEPT_LAB>0",
3489         "#ifndef BFS",
3490         "       if (!a_cycles",
3491                 "#ifdef HAS_CODE",
3492         "       && !readtrail",
3493                 "#endif",
3494         "       && !state_tables)",
3495         "       { fprintf(efd, \"warning: never claim + accept labels \");",
3496         "         fprintf(efd, \"requires -a flag to fully verify\\n\");",
3497         "       }",
3498         "#else",
3499         "       if (",
3500                 "#ifdef HAS_CODE",
3501         "       !readtrail",
3502                 "#endif",
3503         "       && !state_tables)",
3504         "       { fprintf(efd, \"warning: verification in BFS mode \");",
3505         "         fprintf(efd, \"is restricted to safety properties\\n\");",
3506         "       }",
3507         "#endif",
3508                 "#endif",
3509         "#endif",
3510         "#ifndef SAFETY",
3511         "       if (!a_cycles",
3512         "#ifdef HAS_CODE",
3513         "       && !readtrail",
3514         "#endif",
3515         "       &&  !state_tables)",
3516         "       { fprintf(efd, \"hint: this search is more efficient \");",
3517         "         fprintf(efd, \"if pan.c is compiled -DSAFETY\\n\");",
3518         "       }",
3519                 "#ifndef NOCOMP",
3520         "       if (!a_cycles)",
3521         "               S_A = 0;",
3522         "       else",
3523         "       {       if (!fairness)",
3524         "                       S_A = 1; /* _a_t */",
3525                 "#ifndef NOFAIR",
3526         "               else /* _a_t and _cnt[NFAIR] */",
3527         "                 S_A = (&(now._cnt[0]) - (uchar *) &now) + NFAIR - 2;",
3528         "               /* -2 because first two uchars in now are masked */",
3529                 "#endif",
3530         "       }",
3531                 "#endif",
3532         "#endif",
3533         "       signal(SIGINT, stopped);",
3534
3535         /******************* 4.2.5 ********************/
3536         "       if (WS == 4 && ssize >= 32)",
3537         "       {       mask = 0xffffffff;",
3538         "#ifdef BITSTATE",
3539         "               switch (ssize) {",
3540         "               case 34: nmask = (mask>>1); break;",
3541         "               case 33: nmask = (mask>>2); break;",
3542         "               default: nmask = (mask>>3); break;",
3543         "               }",
3544         "#else",
3545         "               nmask = mask;",
3546         "#endif",
3547         "       } else if (WS == 8)",
3548         "       {       mask = ((1L<<ssize)-1); /* hash init */",
3549         "#ifdef BITSTATE",
3550         "               nmask = mask>>3;",
3551         "#else",
3552         "               nmask = mask;",
3553         "#endif",
3554         "       } else if (WS != 4)",
3555         "       {       fprintf(stderr, \"pan: wordsize %%ld not supported\\n\", WS);",
3556         "               exit(1);",
3557         "       } else  /* WS == 4 and ssize < 32 */",
3558         "       {       mask = ((1L<<ssize)-1); /* hash init */",
3559         "               nmask = (mask>>3);",
3560         "       }",
3561         /****************** end **********************/
3562
3563         "#ifdef BFS",
3564         "       trail = (Trail *) emalloc(6*sizeof(Trail));",
3565         "       trail += 3;",
3566         "#else",
3567         "       trail = (Trail *) emalloc((maxdepth+3)*sizeof(Trail));",
3568         "       trail++;        /* protect trpt-1 refs at depth 0 */",
3569         "#endif",
3570         "#ifdef SVDUMP",
3571         "       if (vprefix > 0)",
3572         "       {       char nm[64];",
3573         "               sprintf(nm, \"%%s.svd\", Source);",
3574         "               if ((svfd = creat(nm, 0666)) < 0)",
3575         "               {       fprintf(efd, \"couldn't create %%s\\n\", nm);",
3576         "                       vprefix = 0;",
3577         "       }       }",
3578         "#endif",
3579         "#ifdef RANDSTOR",
3580         "       srand(123);",
3581         "#endif",
3582         "#if SYNC>0 && ASYNC==0",
3583         "       set_recvs();",
3584         "#endif",
3585         "       run();",
3586         "       done = 1;",
3587         "       wrapup();",
3588         "       return 0;",
3589         "}",    /* end of main() */
3590         "",
3591         "void",
3592         "usage(FILE *fd)",
3593         "{",
3594         "       fprintf(fd, \"Valid Options are:\\n\");",
3595         "#ifndef SAFETY",
3596                 "#ifdef NP",
3597         "       fprintf(fd, \"\t-a  -> is disabled by -DNP \");",
3598         "       fprintf(fd, \"(-DNP compiles for -l only)\\n\");",
3599                 "#else",
3600         "       fprintf(fd, \"\t-a  find acceptance cycles\\n\");",
3601                 "#endif",
3602         "#else",
3603         "       fprintf(fd, \"\t-a,-l,-f  -> are disabled by -DSAFETY\\n\");",
3604         "#endif",
3605         "       fprintf(fd, \"\t-A  ignore assert() violations\\n\");",
3606         "       fprintf(fd, \"\t-b  consider it an error to exceed the depth-limit\\n\");",
3607         "       fprintf(fd, \"\t-cN stop at Nth error \");",
3608         "       fprintf(fd, \"(defaults to -c1)\\n\");",
3609         "       fprintf(fd, \"\t-d  print state tables and stop\\n\");",
3610         "       fprintf(fd, \"\t-e  create trails for all errors\\n\");",
3611         "       fprintf(fd, \"\t-E  ignore invalid end states\\n\");",
3612         "#ifdef SC",
3613         "       fprintf(fd, \"\t-Ffile  use 'file' to store disk-stack\\n\");",
3614         "#endif",
3615         "#ifndef NOFAIR",
3616         "       fprintf(fd, \"\t-f  add weak fairness (to -a or -l)\\n\");",
3617         "#endif",
3618         "       fprintf(fd, \"\t-hN use different hash-seed N:1..32\\n\");",
3619         "       fprintf(fd, \"\t-i  search for shortest path to error\\n\");",
3620         "       fprintf(fd, \"\t-I  like -i, but approximate and faster\\n\");",
3621         "       fprintf(fd, \"\t-J  reverse eval order of nested unlesses\\n\");",
3622         "#ifdef BITSTATE",
3623         "       fprintf(fd, \"\t-kN set N bits per state (defaults to 3)\\n\");",
3624         "#endif",
3625         "#ifndef SAFETY",
3626                 "#ifdef NP",
3627         "       fprintf(fd, \"\t-l  find non-progress cycles\\n\");",
3628                 "#else",
3629         "       fprintf(fd, \"\t-l  find non-progress cycles -> \");",
3630         "       fprintf(fd, \"disabled, requires \");",
3631         "       fprintf(fd, \"compilation with -DNP\\n\");",
3632                 "#endif",
3633         "#endif",
3634 #ifndef POWOW
3635         "#ifdef BITSTATE",
3636         "       fprintf(fd, \"\t-MN use N Megabytes for bitstate hash array\\n\");",
3637         "       fprintf(fd, \"\t-GN use N Gigabytes for bitstate hash array\\n\");",
3638         "#endif",
3639 #endif
3640         "       fprintf(fd, \"\t-mN max depth N steps (default=10k)\\n\");",
3641         "       fprintf(fd, \"\t-n  no listing of unreached states\\n\");",
3642         "#ifdef SVDUMP",
3643         "       fprintf(fd, \"\t-pN create svfile (save N bytes per state)\\n\");",
3644         "#endif",
3645         "       fprintf(fd, \"\t-q  require empty chans in valid end states\\n\");",
3646         "#ifdef HAS_CODE",
3647         "       fprintf(fd, \"\t-r  read and execute trail - can add -v,-n,-PN,-g,-C\\n\");",
3648         "       fprintf(fd, \"\t-rN read and execute N-th error trail\\n\");",
3649         "       fprintf(fd, \"\t-C  read and execute trail - columnated output (can add -v,-n)\\n\");",
3650         "       fprintf(fd, \"\t-PN read and execute trail - restrict trail output to proc N\\n\");",
3651         "       fprintf(fd, \"\t-g  read and execute trail + msc gui support\\n\");",
3652         "       fprintf(fd, \"\t-S  silent replay: only user defined printfs show\\n\");",
3653         "#endif",
3654         "#ifdef BITSTATE",
3655         "       fprintf(fd, \"\t-RN repeat run Nx with N \");",
3656         "       fprintf(fd, \"[1..32] independent hash functions\\n\");",
3657         "       fprintf(fd, \"\t-s  same as -k1 (single bit per state)\\n\");",
3658         "#endif",
3659         "       fprintf(fd, \"\t-T  create trail files in read-only mode\\n\");",
3660         "       fprintf(fd, \"\t-tsuf replace .trail with .suf on trailfiles\\n\");",
3661         "       fprintf(fd, \"\t-V  print SPIN version number\\n\");",
3662         "       fprintf(fd, \"\t-v  verbose -- filenames in unreached state listing\\n\");",
3663         "       fprintf(fd, \"\t-wN hashtable of 2^N entries \");",
3664         "       fprintf(fd, \"(defaults to -w%%d)\\n\", ssize);",
3665         "       exit(1);",
3666         "}",
3667         "",
3668         "char *",
3669         "Malloc(unsigned long n)",
3670         "{      char *tmp;",
3671         "#if defined(MEMCNT) || defined(MEMLIM)",
3672         "       if (memcnt+ (double) n > memlim) goto err;",
3673         "#endif",
3674 "#if 1",
3675         "       tmp = (char *) malloc(n);",
3676         "       if (!tmp)",
3677 "#else",
3678         /* on linux machines, a large amount of memory is set aside
3679          * for malloc, whether it is used or not
3680          * using sbrk would make this memory arena inaccessible
3681          * the reason for using sbrk was originally to provide a
3682          * small additional speedup (since this memory is never released)
3683          */
3684         "       tmp = (char *) sbrk(n);",
3685         "       if (tmp == (char *) -1L)",
3686 "#endif",
3687         "       {",
3688         "#if defined(MEMCNT) || defined(MEMLIM)",
3689         "err:",
3690         "#endif",
3691         "               printf(\"pan: out of memory\\n\");",
3692         "#if defined(MEMCNT) || defined(MEMLIM)",
3693         "               printf(\"\t%%g bytes used\\n\", memcnt);",
3694         "               printf(\"\t%%g bytes more needed\\n\", (double) n);",
3695         "               printf(\"\t%%g bytes limit\\n\",",
3696         "                       memlim);",
3697         "#endif",
3698         "#ifdef COLLAPSE",
3699         "               printf(\"hint: to reduce memory, recompile with\\n\");",
3700                 "#ifndef MA",
3701         "               printf(\"  -DMA=%%d   # better/slower compression, or\\n\", hmax);",
3702                 "#endif",
3703         "               printf(\"  -DBITSTATE # supertrace, approximation\\n\");",
3704         "#else",
3705         "#ifndef BITSTATE",
3706         "               printf(\"hint: to reduce memory, recompile with\\n\");",
3707                 "#ifndef HC",
3708         "               printf(\"  -DCOLLAPSE # good, fast compression, or\\n\");",
3709                         "#ifndef MA",
3710         "               printf(\"  -DMA=%%d   # better/slower compression, or\\n\", hmax);",
3711                         "#endif",
3712         "               printf(\"  -DHC # hash-compaction, approximation\\n\");",
3713                 "#endif",
3714         "               printf(\"  -DBITSTATE # supertrace, approximation\\n\");",
3715         "#endif",
3716         "#endif",
3717         "               wrapup();",
3718         "       }",
3719         "       memcnt += (double) n;",
3720         "       return tmp;",
3721         "}",
3722         "",
3723         "#define CHUNK  (100*VECTORSZ)",
3724         "",
3725         "char *",
3726         "emalloc(unsigned long n) /* never released or reallocated */",
3727         "{      char *tmp;",
3728         "       if (n == 0)",
3729         "               return (char *) NULL;",
3730         "       if (n&(sizeof(void *)-1)) /* for proper alignment */",
3731         "               n += sizeof(void *)-(n&(sizeof(void *)-1));",
3732         "       if ((unsigned long) left < n)", /* was: (left < (long)n) */
3733         "       {       grow = (n < CHUNK) ? CHUNK : n;",
3734 #if 1
3735         "               have = Malloc(grow);",
3736 #else
3737         "               /* gcc's sbrk can give non-aligned result */",
3738         "               grow += sizeof(void *); /* allow realignment */",
3739         "               have = Malloc(grow);",
3740         "               if (((unsigned) have)&(sizeof(void *)-1))",
3741         "               {       have += (long) (sizeof(void *) ",
3742         "                               - (((unsigned) have)&(sizeof(void *)-1)));",
3743         "                       grow -= sizeof(void *);",
3744         "               }",
3745 #endif
3746         "               fragment += (double) left;",
3747         "               left = grow;",
3748         "       }",
3749         "       tmp = have;",
3750         "       have += (long) n;",
3751         "       left -= (long) n;",
3752         "       memset(tmp, 0, n);",
3753         "       return tmp;",
3754         "}",
3755
3756         "void",
3757         "Uerror(char *str)",
3758         "{      /* always fatal */",
3759         "       uerror(str);",
3760         "       wrapup();",
3761         "}\n",
3762         "#if defined(MA) && !defined(SAFETY)",
3763         "int",
3764         "Unwind(void)",
3765         "{      Trans *t; uchar ot, _m; int tt; short II;",
3766         "#ifdef VERBOSE",
3767         "       int i;",
3768         "#endif",
3769         "       uchar oat = now._a_t;",
3770         "       now._a_t &= ~(1|16|32);",
3771         "       memcpy((char *) &comp_now, (char *) &now, vsize);",
3772         "       now._a_t = oat;",
3773         "Up:",
3774         "#ifdef SC",
3775         "       trpt = getframe(depth);",
3776         "#endif",
3777         "#ifdef VERBOSE",
3778         "       printf(\"%%d     State: \", depth);",
3779         "       for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",",
3780         "               ((char *)&now)[i], Mask[i]?\"*\":\"\");",
3781         "       printf(\"\\n\");",
3782         "#endif",
3783         "#ifndef NOFAIR",
3784         "       if (trpt->o_pm&128)     /* fairness alg */",
3785         "       {       now._cnt[now._a_t&1] = trpt->bup.oval;",
3786         "               depth--;",
3787         "#ifdef SC",
3788         "               trpt = getframe(depth);",
3789         "#else",
3790         "               trpt--;",
3791         "#endif",
3792         "               goto Q999;",
3793         "       }",
3794         "#endif",
3795         "#ifdef HAS_LAST",
3796         "#ifdef VERI",
3797         "       { int d; Trail *trl;",
3798         "         now._last = 0;",
3799         "         for (d = 1; d < depth; d++)",
3800         "         {     trl = getframe(depth-d); /* was trl = (trpt-d); */",
3801         "               if (trl->pr != 0)",
3802         "               { now._last = trl->pr - BASE;",
3803         "                 break;",
3804         "       } }     }",
3805         "#else",
3806         "       now._last = (depth<1)?0:(trpt-1)->pr;",
3807         "#endif",
3808         "#endif",
3809         "#ifdef EVENT_TRACE",
3810         "       now._event = trpt->o_event;",
3811         "#endif",
3812         "       if ((now._a_t&1) && depth <= A_depth)",
3813         "       {       now._a_t &= ~(1|16|32);",
3814         "               if (fairness) now._a_t |= 2;    /* ? */",
3815         "               A_depth = 0;",
3816         "               goto CameFromHere;      /* checkcycles() */",
3817         "       }",
3818         "       t  = trpt->o_t;",
3819         "       ot = trpt->o_ot; II = trpt->pr;",
3820         "       tt = trpt->o_tt; this = pptr(II);",
3821         "       _m = do_reverse(t, II, trpt->o_m);",
3822         "#ifdef VERBOSE",
3823         "       printf(\"%%3d: proc %%d \", depth, II);",
3824         "       printf(\"reverses %%d, %%d to %%d,\",",
3825         "               t->forw, tt, t->st);",
3826         "       printf(\" %%s [abit=%%d,adepth=%%d,\", ",
3827         "               t->tp, now._a_t, A_depth);",
3828         "       printf(\"tau=%%d,%%d] <unwind>\\n\", ",
3829         "               trpt->tau, (trpt-1)->tau);",
3830         "#endif",
3831         "       depth--;",
3832         "#ifdef SC",
3833         "       trpt = getframe(depth);",
3834         "#else",
3835         "       trpt--;",
3836         "#endif",
3837         "       /* reached[ot][t->st] = 1;      3.4.13 */",
3838         "       ((P0 *)this)->_p = tt;",
3839         "#ifndef NOFAIR",
3840         "       if ((trpt->o_pm&32))",
3841         "       {",
3842                 "#ifdef VERI",
3843         "               if (now._cnt[now._a_t&1] == 0)",
3844         "                       now._cnt[now._a_t&1] = 1;",
3845                 "#endif",
3846         "               now._cnt[now._a_t&1] += 1;",
3847         "       }",
3848         "Q999:",
3849         "       if (trpt->o_pm&8)",
3850         "       {       now._a_t &= ~2;",
3851         "               now._cnt[now._a_t&1] = 0;",
3852         "       }",
3853         "       if (trpt->o_pm&16)",
3854         "               now._a_t |= 2;",
3855         "#endif",
3856         "CameFromHere:",
3857         "       if (memcmp((char *) &now, (char *) &comp_now, vsize) == 0)",
3858         "               return depth;",
3859         "       if (depth > 0) goto Up;",
3860         "       return 0;",
3861         "}",
3862         "#endif",
3863         "static char unwinding;",
3864         "void",
3865         "uerror(char *str)",
3866         "{      static char laststr[256];",
3867         "       int is_cycle;",
3868         "",
3869         "       if (unwinding) return; /* 1.4.2 */",
3870         "       if (strncmp(str, laststr, 254))",
3871         "       printf(\"pan: %%s (at depth %%ld)\\n\", str,",
3872         "               (depthfound==-1)?depth:depthfound);",
3873         "       strncpy(laststr, str, 254);",
3874         "       errors++;",
3875         "#ifdef HAS_CODE",
3876         "       if (readtrail) { wrap_trail(); return; }",
3877         "#endif",
3878         "       is_cycle = (strstr(str, \" cycle\") != (char *) 0);",
3879         "       if (!is_cycle)",
3880         "       {       depth++; trpt++;",      /* include failed step */
3881         "       }",
3882         "       if ((every_error != 0)",
3883         "       ||  errors == upto)",
3884         "       {",
3885         "#if defined(MA) && !defined(SAFETY)",
3886         "               if (is_cycle)",
3887         "               {       int od = depth;",
3888         "                       unwinding = 1;",
3889         "                       depthfound = Unwind();",
3890         "                       unwinding = 0;",
3891         "                       depth = od;",
3892         "               }",
3893         "#endif",
3894 "#ifdef BFS",
3895         "               if (depth > 1) trpt--;",
3896         "               nuerror(str);",
3897         "               if (depth > 1) trpt++;",
3898 "#else",
3899         "               putrail();",
3900 "#endif",
3901         "#if defined(MA) && !defined(SAFETY)",
3902         "               if (strstr(str, \" cycle\"))",
3903         "               {       if (every_error)",
3904         "                       printf(\"sorry: MA writes 1 trail max\\n\");",
3905         "                       wrapup(); /* no recovery from unwind */",
3906         "               }",
3907         "#endif",
3908         "       }",
3909         "       if (!is_cycle)",
3910         "       {       depth--; trpt--;        /* undo */",
3911         "       }",
3912 "#ifndef BFS",
3913         "       if (iterative != 0 && maxdepth > 0)",
3914         "       {       maxdepth = (iterative == 1)?(depth-1):(depth/2);",
3915         "               warned = 1;",
3916         "               printf(\"pan: reducing search depth to %%ld\\n\",",
3917         "                       maxdepth);",
3918         "       } else",
3919 "#endif",
3920         "       if (errors >= upto && upto != 0)",
3921         "               wrapup();",
3922         "       depthfound = -1;",
3923         "}\n",
3924         "int",
3925         "xrefsrc(int lno, S_F_MAP *mp, int M, int i)",
3926         "{      Trans *T; int j, retval=1;",
3927         "       for (T = trans[M][i]; T; T = T->nxt)",
3928         "       if (T && T->tp)",
3929         "       {       if (strcmp(T->tp, \".(goto)\") == 0",
3930         "               ||  strncmp(T->tp, \"goto :\", 6) == 0)",
3931         "                       return 1; /* not reported */",
3932         "",
3933         "               printf(\"\\tline %%d\", lno);",
3934         "               if (verbose)",
3935         "               for (j = 0; j < sizeof(mp); j++)",
3936         "                       if (i >= mp[j].from && i <= mp[j].upto)",
3937         "                       {       printf(\", \\\"%%s\\\"\", mp[j].fnm);",
3938         "                               break;",
3939         "                       }",
3940         "               printf(\", state %%d\", i);",
3941         "               if (strcmp(T->tp, \"\") != 0)",
3942         "               {       char *q;",
3943         "                       q = transmognify(T->tp);",
3944         "                       printf(\", \\\"%%s\\\"\", q?q:\"\");",
3945         "               } else if (stopstate[M][i])",
3946         "                       printf(\", -end state-\");",
3947         "               printf(\"\\n\");",
3948         "               retval = 0; /* reported */",
3949         "       }",
3950         "       return retval;",
3951         "}\n",
3952         "void",
3953         "r_ck(uchar *which, int N, int M, short *src, S_F_MAP *mp)",
3954         "{      int i, m=0;\n",
3955         "#ifdef VERI",
3956         "       if (M == VERI && !verbose) return;",
3957         "#endif",
3958         "       printf(\"unreached in proctype %%s\\n\", procname[M]);",
3959         "       for (i = 1; i < N; i++)",
3960 #if 0
3961         "         if (which[i] == 0 /* && trans[M][i] */)",
3962 #else
3963         "         if (which[i] == 0",
3964         "         &&  (mapstate[M][i] == 0",
3965         "         ||   which[mapstate[M][i]] == 0))",
3966 #endif
3967         "               m += xrefsrc((int) src[i], mp, M, i);",
3968         "         else",
3969         "               m++;",
3970         "       printf(\"\t(%%d of %%d states)\\n\", N-1-m, N-1);",
3971         "}\n",
3972         "void",
3973         "putrail(void)",
3974         "{      int fd; long i, j;",
3975         "       Trail *trl;",
3976         "#if defined VERI || defined(MERGED)",
3977         "       char snap[64];",
3978         "#endif",
3979         "",
3980         "       fd = make_trail();",
3981         "       if (fd < 0) return;",
3982         "#ifdef VERI",
3983         "       sprintf(snap, \"-2:%%d:-2\\n\", VERI);",
3984         "       write(fd, snap, strlen(snap));",
3985         "#endif",
3986         "#ifdef MERGED",
3987         "       sprintf(snap, \"-4:-4:-4\\n\");",
3988         "       write(fd, snap, strlen(snap));",
3989         "#endif",
3990         "       for (i = 1; i <= depth; i++)",
3991         "       {       if (i == depthfound+1)",
3992         "                       write(fd, \"-1:-1:-1\\n\", 9);",
3993         "               trl = getframe(i);",
3994         "               if (!trl->o_t) continue;",
3995         "               if (trl->o_pm&128) continue;",
3996         "               sprintf(snap, \"%%ld:%%d:%%d\\n\", ",
3997         "                       i, trl->pr, trl->o_t->t_id);",
3998         "               j = strlen(snap);",
3999         "               if (write(fd, snap, j) != j)",
4000         "               {       printf(\"pan: error writing trailfile\\n\");",
4001         "                       close(fd);",
4002         "                       wrapup();",
4003         "               }",
4004         "       }",
4005         "       close(fd);",
4006         "}\n",
4007         "void",
4008         "sv_save(void)  /* push state vector onto save stack */",
4009         "{      if (!svtack->nxt)",
4010         "       {  svtack->nxt = (Svtack *) emalloc(sizeof(Svtack));",
4011         "          svtack->nxt->body = emalloc(vsize*sizeof(char));",
4012         "          svtack->nxt->lst = svtack;",
4013         "          svtack->nxt->m_delta = vsize;",
4014         "          svmax++;",
4015         "       } else if (vsize > svtack->nxt->m_delta)",
4016         "       {  svtack->nxt->body = emalloc(vsize*sizeof(char));",
4017         "          svtack->nxt->lst = svtack;",
4018         "          svtack->nxt->m_delta = vsize;",
4019         "          svmax++;",
4020         "       }",
4021         "       svtack = svtack->nxt;",
4022         "#if SYNC",
4023         "       svtack->o_boq = boq;",
4024         "#endif",
4025         "       svtack->o_delta = vsize; /* don't compress */",
4026         "       memcpy((char *)(svtack->body), (char *) &now, vsize);",
4027         "#if defined(C_States) && defined(HAS_STACK) && (HAS_TRACK==1)",
4028         "       c_stack((uchar *) &(svtack->c_stack[0]));",
4029         "#endif",
4030         "#ifdef DEBUG",
4031         "       printf(\"%%d:   sv_save\\n\", depth);",
4032         "#endif",
4033         "}\n",
4034         "void",
4035         "sv_restor(void)        /* pop state vector from save stack */",
4036         "{",
4037         "       memcpy((char *)&now, svtack->body, svtack->o_delta);",
4038         "#if SYNC",
4039         "       boq = svtack->o_boq;",
4040         "#endif",
4041
4042         "#if defined(C_States) && (HAS_TRACK==1)",
4043         "#ifdef HAS_STACK",
4044         "       c_unstack((uchar *) &(svtack->c_stack[0]));",
4045         "#endif",
4046         "       c_revert((uchar *) &(now.c_state[0]));",
4047         "#endif",
4048
4049         "       if (vsize != svtack->o_delta)",
4050         "               Uerror(\"sv_restor\");",
4051         "       if (!svtack->lst)",
4052         "               Uerror(\"error: v_restor\");",
4053         "       svtack  = svtack->lst;",
4054         "#ifdef DEBUG",
4055         "       printf(\"       sv_restor\\n\");",
4056         "#endif",
4057         "}\n",
4058         "void",
4059         "p_restor(int h)",
4060         "{      int i; char *z = (char *) &now;\n",
4061         "       proc_offset[h] = stack->o_offset;",
4062         "       proc_skip[h]   = (uchar) stack->o_skip;",
4063         "#ifndef XUSAFE",
4064         "       p_name[h] = stack->o_name;",
4065         "#endif",
4066         "#ifndef NOCOMP",
4067         "       for (i = vsize + stack->o_skip; i > vsize; i--)",
4068         "               Mask[i-1] = 1; /* align */",
4069         "#endif",
4070         "       vsize += stack->o_skip;",
4071         "       memcpy(z+vsize, stack->body, stack->o_delta);",
4072         "       vsize += stack->o_delta;",
4073         "#ifndef NOVSZ",
4074         "       now._vsz = vsize;",
4075         "#endif",
4076         "#ifndef NOCOMP",
4077         "       for (i = 1; i <= Air[((P0 *)pptr(h))->_t]; i++)",
4078         "               Mask[vsize - i] = 1; /* pad */",
4079         "       Mask[proc_offset[h]] = 1;       /* _pid */",
4080         "#endif",
4081         "       if (BASE > 0 && h > 0)",
4082         "               ((P0 *)pptr(h))->_pid = h-BASE;",
4083         "       else",
4084         "               ((P0 *)pptr(h))->_pid = h;",
4085         "       i = stack->o_delqs;",
4086         "       now._nr_pr += 1;",
4087         "       if (!stack->lst)        /* debugging */",
4088         "               Uerror(\"error: p_restor\");",
4089         "       stack = stack->lst;",
4090         "       this = pptr(h);",
4091         "       while (i-- > 0)",
4092         "               q_restor();",
4093         "}\n",
4094         "void",
4095         "q_restor(void)",
4096         "{      char *z = (char *) &now;",
4097         "#ifndef NOCOMP",
4098         "       int k, k_end;",
4099         "#endif",
4100         "       q_offset[now._nr_qs] = stack->o_offset;",
4101         "       q_skip[now._nr_qs]   = (uchar) stack->o_skip;",
4102         "#ifndef XUSAFE",
4103         "       q_name[now._nr_qs]   = stack->o_name;",
4104         "#endif",
4105         "       vsize += stack->o_skip;",
4106         "       memcpy(z+vsize, stack->body, stack->o_delta);",
4107         "       vsize += stack->o_delta;",
4108         "#ifndef NOVSZ",
4109         "       now._vsz = vsize;",
4110         "#endif",
4111         "       now._nr_qs += 1;",
4112         "#ifndef NOCOMP",
4113         "       k_end = stack->o_offset;",
4114         "       k = k_end - stack->o_skip;",
4115         "#if SYNC",
4116         "#ifndef BFS",
4117         "       if (q_zero(now._nr_qs)) k_end += stack->o_delta;",
4118         "#endif",
4119         "#endif",
4120         "       for ( ; k < k_end; k++)",
4121         "               Mask[k] = 1;",
4122         "#endif",
4123         "       if (!stack->lst)        /* debugging */",
4124         "               Uerror(\"error: q_restor\");",
4125         "       stack = stack->lst;",
4126         "}",
4127
4128         "typedef struct IntChunks {",
4129         "       int     *ptr;",
4130         "       struct  IntChunks *nxt;",
4131         "} IntChunks;",
4132         "IntChunks *filled_chunks[512];",
4133         "IntChunks *empty_chunks[512];",
4134
4135         "int *",
4136         "grab_ints(int nr)",
4137         "{      IntChunks *z;",
4138         "       if (nr >= 512) Uerror(\"cannot happen grab_int\");",
4139         "       if (filled_chunks[nr])",
4140         "       {       z = filled_chunks[nr];",
4141         "               filled_chunks[nr] = filled_chunks[nr]->nxt;",
4142         "       } else ",
4143         "       {       z = (IntChunks *) emalloc(sizeof(IntChunks));",
4144         "               z->ptr = (int *) emalloc(nr * sizeof(int));",
4145         "       }",
4146         "       z->nxt = empty_chunks[nr];",
4147         "       empty_chunks[nr] = z;",
4148         "       return z->ptr;",
4149         "}",
4150         "void",
4151         "ungrab_ints(int *p, int nr)",
4152         "{      IntChunks *z;",
4153         "       if (!empty_chunks[nr]) Uerror(\"cannot happen ungrab_int\");",
4154         "       z = empty_chunks[nr];",
4155         "       empty_chunks[nr] = empty_chunks[nr]->nxt;",
4156         "       z->ptr = p;",
4157         "       z->nxt = filled_chunks[nr];",
4158         "       filled_chunks[nr] = z;",
4159         "}",
4160         "int",
4161         "delproc(int sav, int h)",
4162         "{      int d, i=0;",
4163         "#ifndef NOCOMP",
4164         "       int o_vsize = vsize;",
4165         "#endif",
4166         "       if (h+1 != (int) now._nr_pr) return 0;\n",
4167         "       while (now._nr_qs",
4168         "       &&     q_offset[now._nr_qs-1] > proc_offset[h])",
4169         "       {       delq(sav);",
4170         "               i++;",
4171         "       }",
4172         "       d = vsize - proc_offset[h];",
4173         "       if (sav)",
4174         "       {       if (!stack->nxt)",
4175         "               {       stack->nxt = (Stack *)",
4176         "                               emalloc(sizeof(Stack));",
4177         "                       stack->nxt->body = ",
4178         "                               emalloc(Maxbody*sizeof(char));",
4179         "                       stack->nxt->lst = stack;",
4180         "                       smax++;",
4181         "               }",
4182         "               stack = stack->nxt;",
4183         "               stack->o_offset = proc_offset[h];",
4184         "#if VECTORSZ>32000",
4185         "               stack->o_skip   = (int) proc_skip[h];",
4186         "#else",
4187         "               stack->o_skip   = (short) proc_skip[h];",
4188         "#endif",
4189         "#ifndef XUSAFE",
4190         "               stack->o_name   = p_name[h];",
4191         "#endif",
4192         "               stack->o_delta  = d;",
4193         "               stack->o_delqs  = i;",
4194         "               memcpy(stack->body, (char *)pptr(h), d);",
4195         "       }",
4196         "       vsize = proc_offset[h];",
4197         "       now._nr_pr = now._nr_pr - 1;",
4198         "       memset((char *)pptr(h), 0, d);",
4199         "       vsize -= (int) proc_skip[h];",
4200         "#ifndef NOVSZ",
4201         "       now._vsz = vsize;",
4202         "#endif",
4203         "#ifndef NOCOMP",
4204         "       for (i = vsize; i < o_vsize; i++)",
4205         "               Mask[i] = 0; /* reset */",
4206         "#endif",
4207         "       return 1;",
4208         "}\n",
4209         "void",
4210         "delq(int sav)",
4211         "{      int h = now._nr_qs - 1;",
4212         "       int d = vsize - q_offset[now._nr_qs - 1];",
4213         "#ifndef NOCOMP",
4214         "       int k, o_vsize = vsize;",
4215         "#endif",
4216         "       if (sav)",
4217         "       {       if (!stack->nxt)",
4218         "               {       stack->nxt = (Stack *)",
4219         "                               emalloc(sizeof(Stack));",
4220         "                       stack->nxt->body = ",
4221         "                               emalloc(Maxbody*sizeof(char));",
4222         "                       stack->nxt->lst = stack;",
4223         "                       smax++;",
4224         "               }",
4225         "               stack = stack->nxt;",
4226         "               stack->o_offset = q_offset[h];",
4227         "#if VECTORSZ>32000",
4228         "               stack->o_skip   = (int) q_skip[h];",
4229         "#else",
4230         "               stack->o_skip   = (short) q_skip[h];",
4231         "#endif",
4232         "#ifndef XUSAFE",
4233         "               stack->o_name   = q_name[h];",
4234         "#endif",
4235         "               stack->o_delta  = d;",
4236         "               memcpy(stack->body, (char *)qptr(h), d);",
4237         "       }",
4238         "       vsize = q_offset[h];",
4239         "       now._nr_qs = now._nr_qs - 1;",
4240         "       memset((char *)qptr(h), 0, d);",
4241         "       vsize -= (int) q_skip[h];",
4242         "#ifndef NOVSZ",
4243         "       now._vsz = vsize;",
4244         "#endif",
4245         "#ifndef NOCOMP",
4246         "       for (k = vsize; k < o_vsize; k++)",
4247         "               Mask[k] = 0; /* reset */",
4248         "#endif",
4249         "}\n",
4250         "int",
4251         "qs_empty(void)",
4252         "{      int i;",
4253         "       for (i = 0; i < (int) now._nr_qs; i++)",
4254         "       {       if (q_sz(i) > 0)",
4255         "                       return 0;",
4256         "       }",
4257         "       return 1;",
4258         "}\n",
4259         "int",
4260         "endstate(void)",
4261         "{      int i; P0 *ptr;",
4262         "       for (i = BASE; i < (int) now._nr_pr; i++)",
4263         "       {       ptr = (P0 *) pptr(i);",
4264         "               if (!stopstate[ptr->_t][ptr->_p])",
4265         "                       return 0;",
4266         "       }",
4267         "       if (strict) return qs_empty();",
4268         "#if defined(EVENT_TRACE) && !defined(OTIM)",
4269         "       if (!stopstate[EVENT_TRACE][now._event] && !a_cycles)",
4270         "       {       printf(\"pan: event_trace not completed\\n\");",
4271         "               return 0;",
4272         "       }",
4273         "#endif",
4274         "       return 1;",
4275         "}\n",
4276         "#ifndef SAFETY",
4277         "void",
4278         "checkcycles(void)",
4279         "{      uchar o_a_t = now._a_t;",
4280         "#ifndef NOFAIR",
4281         "       uchar o_cnt = now._cnt[1];",
4282         "#endif",
4283                 "#ifdef FULLSTACK",
4284                 "#ifndef MA",
4285         "       struct H_el *sv = trpt->ostate; /* save */",
4286                 "#else",
4287         "       uchar prov = trpt->proviso; /* save */",
4288                 "#endif",
4289                 "#endif",
4290                 "#ifdef DEBUG",
4291         "       { int i; uchar *v = (uchar *) &now;",
4292         "         printf(\"     set Seed state \");",
4293         "#ifndef NOFAIR",
4294         "         if (fairness) printf(\"(cnt = %%d:%%d, nrpr=%%d) \",",
4295         "               now._cnt[0], now._cnt[1], now._nr_pr);",
4296         "#endif",
4297         "       /* for (i = 0; i < n; i++) printf(\"%%d,\", v[i]);      */",
4298         "         printf(\"\\n\");",
4299         "       }",
4300         "       printf(\"%%d: cycle check starts\\n\", depth);",
4301                 "#endif",
4302         "       now._a_t |= (1|16|32);",
4303         "       /* 1 = 2nd DFS; (16|32) to help hasher */",
4304                 "#ifndef NOFAIR",
4305 #if 0
4306         "       if (fairness)",
4307         "       {       now._a_t &= ~2;   /* pre-apply Rule 3 */",
4308         "               now._cnt[1] = 0;", /* reset both a-bit and cnt=0 */
4309         "       /* avoid matching seed on claim stutter on this state */",
4310         "       }",
4311 #else
4312         "       now._cnt[1] = now._cnt[0];",
4313 #endif
4314                 "#endif",
4315         "       memcpy((char *)&A_Root, (char *)&now, vsize);",
4316         "       A_depth = depthfound = depth;",
4317         "       new_state();    /* start 2nd DFS */",
4318         "       now._a_t = o_a_t;",
4319         "#ifndef NOFAIR",
4320         "       now._cnt[1] = o_cnt;",
4321         "#endif",
4322         "       A_depth = 0; depthfound = -1;",
4323                 "#ifdef DEBUG",
4324         "       printf(\"%%d: cycle check returns\\n\", depth);",
4325                 "#endif",
4326                 "#ifdef FULLSTACK",
4327                 "#ifndef MA",
4328         "       trpt->ostate = sv;      /* restore */",
4329                 "#else",
4330         "       trpt->proviso = prov;",
4331                 "#endif",
4332                 "#endif",
4333         "}",
4334         "#endif\n",
4335         "#if defined(FULLSTACK) && defined(BITSTATE)",
4336         "struct H_el *Free_list = (struct H_el *) 0;",
4337         "void",
4338         "onstack_init(void)     /* to store stack states in a bitstate search */",
4339         "{      S_Tab = (struct H_el **) emalloc(maxdepth*sizeof(struct H_el *));",
4340         "}",
4341         "struct H_el *",
4342         "grab_state(int n)",
4343         "{      struct H_el *v, *last = 0;",
4344         "       if (H_tab == S_Tab)",
4345         "       {       for (v = Free_list; v && ((int) v->tagged >= n); v=v->nxt)",
4346         "               {       if ((int) v->tagged == n)",
4347         "                       {       if (last)",
4348         "                                       last->nxt = v->nxt;",
4349         "                               else",
4350         "gotcha:                                Free_list = v->nxt;",
4351         "                               v->tagged = 0;",
4352         "                               v->nxt = 0;",
4353                 "#ifdef COLLAPSE",
4354         "                               v->ln = 0;",
4355                 "#endif",
4356         "                               return v;",
4357         "                       }",
4358         "                       Fh++; last=v;",
4359         "               }",
4360         "               /* new: second try */",
4361         "               v = Free_list;", /* try to avoid emalloc */
4362         "               if (v && ((int) v->tagged >= n))",
4363         "                       goto gotcha;",
4364         "               ngrabs++;",
4365         "       }",
4366         "       return (struct H_el *)",
4367         "             emalloc(sizeof(struct H_el)+n-sizeof(unsigned));",
4368         "}\n",
4369         "#else",
4370         "#define grab_state(n) (struct H_el *) \\",
4371         "               emalloc(sizeof(struct H_el)+n-sizeof(unsigned));",
4372         "#endif",
4373 "#ifdef COLLAPSE",
4374         "unsigned long",
4375         "ordinal(char *v, long n, short tp)",
4376         "{      struct H_el *tmp, *ntmp; long m;",
4377         "       struct H_el *olst = (struct H_el *) 0;",
4378         "       s_hash((uchar *)v, n);",
4379         "       tmp = H_tab[j1];",
4380         "       if (!tmp)",
4381         "       {       tmp = grab_state(n);",
4382         "               H_tab[j1] = tmp;",
4383         "       } else",
4384         "       for ( ;; olst = tmp, tmp = tmp->nxt)",
4385         "       {       m = memcmp(((char *)&(tmp->state)), v, n);",
4386         "               if (n == tmp->ln)",
4387         "               {",
4388         "                       if (m == 0)",
4389         "                               goto done;",
4390         "                       if (m < 0)",
4391         "                       {",
4392         "Insert:                        ntmp = grab_state(n);",
4393         "                               ntmp->nxt = tmp;",
4394         "                               if (!olst)",
4395         "                                       H_tab[j1] = ntmp;",
4396         "                               else",
4397         "                                       olst->nxt = ntmp;",
4398         "                               tmp = ntmp;",
4399         "                               break;",
4400         "                       } else if (!tmp->nxt)",
4401         "                       {",
4402         "Append:                        tmp->nxt = grab_state(n);",
4403         "                               tmp = tmp->nxt;",
4404         "                               break;",
4405         "                       }",
4406         "                       continue;",
4407         "               }",
4408         "               if (n < tmp->ln)",
4409         "                       goto Insert;",
4410         "               else if (!tmp->nxt)",
4411         "                       goto Append;",
4412         "       }",
4413         "       m = ++ncomps[tp];",
4414         "#ifdef FULLSTACK",
4415         "       tmp->tagged = m;",
4416         "#else",
4417         "       tmp->st_id  = m;",
4418         "#endif",
4419         "       memcpy(((char *)&(tmp->state)), v, n);",
4420         "       tmp->ln = n;",
4421         "done:",
4422         "#ifdef FULLSTACK",
4423         "       return tmp->tagged;",
4424         "#else",
4425         "       return tmp->st_id;",
4426         "#endif",
4427         "}",
4428         "",
4429         "int",
4430         "compress(char *vin, int nin)   /* collapse compression */",
4431         "{      char    *w, *v = (char *) &comp_now;",
4432         "       int     i, j;",
4433         "       unsigned long   n;",
4434         "       static char     *x;",
4435         "       static uchar    nbytes[513]; /* 1 + 256 + 256 */",
4436         "       static unsigned short nbytelen;",
4437         "       long col_q(int, char *);",
4438         "       long col_p(int, char *);",
4439         "#ifndef SAFETY",
4440         "       if (a_cycles)",
4441         "               *v++ = now._a_t;",
4442                 "#ifndef NOFAIR",
4443         "       if (fairness)",
4444         "       for (i = 0; i < NFAIR; i++)",
4445         "               *v++ = now._cnt[i];",
4446                 "#endif",
4447         "#endif",
4448         "       nbytelen = 0;",
4449
4450         "#ifndef JOINPROCS",
4451         "       for (i = 0; i < (int) now._nr_pr; i++)",
4452         "       {       n = col_p(i, (char *) 0);",
4453         "#ifdef NOFIX",
4454         "               nbytes[nbytelen] = 0;",
4455         "#else",
4456         "               nbytes[nbytelen] = 1;",
4457         "               *v++ = ((P0 *) pptr(i))->_t;",
4458         "#endif",
4459         "               *v++ = n&255;",
4460         "               if (n >= (1<<8))",
4461         "               {       nbytes[nbytelen]++;",
4462         "                       *v++ = (n>>8)&255;",
4463         "               }",
4464         "               if (n >= (1<<16))",
4465         "               {       nbytes[nbytelen]++;",
4466         "                       *v++ = (n>>16)&255;",
4467         "               }",
4468         "               if (n >= (1<<24))",
4469         "               {       nbytes[nbytelen]++;",
4470         "                       *v++ = (n>>24)&255;",
4471         "               }",
4472         "               nbytelen++;",
4473         "       }",
4474         "#else",
4475         "       x = scratch;",
4476         "       for (i = 0; i < (int) now._nr_pr; i++)",
4477         "               x += col_p(i, x);",
4478         "       n = ordinal(scratch, x-scratch, 2); /* procs */",
4479         "       *v++ = n&255;",
4480         "       nbytes[nbytelen] = 0;",
4481         "       if (n >= (1<<8))",
4482         "       {       nbytes[nbytelen]++;",
4483         "               *v++ = (n>>8)&255;",
4484         "       }",
4485         "       if (n >= (1<<16))",
4486         "       {       nbytes[nbytelen]++;",
4487         "               *v++ = (n>>16)&255;",
4488         "       }",
4489         "       if (n >= (1<<24))",
4490         "       {       nbytes[nbytelen]++;",
4491         "               *v++ = (n>>24)&255;",
4492         "       }",
4493         "       nbytelen++;",
4494         "#endif",
4495         "#ifdef SEPQS",
4496         "       for (i = 0; i < (int) now._nr_qs; i++)",
4497         "       {       n = col_q(i, (char *) 0);",
4498         "               nbytes[nbytelen] = 0;",
4499         "               *v++ = n&255;",
4500         "               if (n >= (1<<8))",
4501         "               {       nbytes[nbytelen]++;",
4502         "                       *v++ = (n>>8)&255;",
4503         "               }",
4504         "               if (n >= (1<<16))",
4505         "               {       nbytes[nbytelen]++;",
4506         "                       *v++ = (n>>16)&255;",
4507         "               }",
4508         "               if (n >= (1<<24))",
4509         "               {       nbytes[nbytelen]++;",
4510         "                       *v++ = (n>>24)&255;",
4511         "               }",
4512         "               nbytelen++;",
4513         "       }",
4514         "#endif",
4515
4516         "#ifdef NOVSZ",
4517         "       /* 3 = _a_t, _nr_pr, _nr_qs */",
4518         "       w = (char *) &now + 3 * sizeof(uchar);",
4519                 "#ifndef NOFAIR",
4520                 "       w += NFAIR;",
4521                 "#endif",
4522         "#else",
4523                 "#if VECTORSZ<65536",
4524                 "       w = (char *) &(now._vsz) + sizeof(unsigned short);",
4525                 "#else",
4526                 "       w = (char *) &(now._vsz) + sizeof(unsigned long);",
4527                 "#endif",
4528         "#endif",
4529         "       x = scratch;",
4530         "       *x++ = now._nr_pr;",
4531         "       *x++ = now._nr_qs;",
4532
4533         "       if (now._nr_qs > 0 && qptr(0) < pptr(0))",
4534         "               n = qptr(0) - (uchar *) w;",
4535         "       else",
4536         "               n = pptr(0) - (uchar *) w;",
4537         "       j = w - (char *) &now;",
4538         "       for (i = 0; i < (int) n; i++, w++)",
4539         "               if (!Mask[j++]) *x++ = *w;",
4540         "#ifndef SEPQS",
4541         "       for (i = 0; i < (int) now._nr_qs; i++)",
4542         "               x += col_q(i, x);",
4543         "#endif",
4544
4545         "       x--;",
4546         "       for (i = 0, j = 6; i < nbytelen; i++)",
4547         "       {       if (j == 6)",
4548         "               {       j = 0;",
4549         "                       *(++x) = 0;",
4550         "               } else",
4551         "                       j += 2;",
4552         "               *x |= (nbytes[i] << j);",
4553         "       }",
4554         "       x++;",
4555         "       for (j = 0; j < WS-1; j++)",
4556         "               *x++ = 0;",
4557         "       x -= j; j = 0;",
4558         "       n = ordinal(scratch, x-scratch, 0); /* globals */",
4559         "       *v++ = n&255;",
4560         "       if (n >= (1<< 8)) { *v++ = (n>> 8)&255; j++; }",
4561         "       if (n >= (1<<16)) { *v++ = (n>>16)&255; j++; }",
4562         "       if (n >= (1<<24)) { *v++ = (n>>24)&255; j++; }",
4563         "       *v++ = j;       /* add last count as a byte */",
4564
4565         "       for (i = 0; i < WS-1; i++)",
4566         "               *v++ = 0;",
4567         "       v -= i;",
4568         "#if 0",
4569         "       printf(\"collapse %%d -> %%d\\n\",",
4570         "               vsize, v - (char *)&comp_now);",
4571         "#endif",
4572         "       return v - (char *)&comp_now;",
4573         "}",
4574
4575 "#else",
4576 "#if !defined(NOCOMP)",
4577         "int",
4578         "compress(char *vin, int n)     /* default compression */",
4579         "{",
4580         "#ifdef HC",
4581         "       int delta = 0;",
4582         "       s_hash((uchar *)vin, n); /* sets K1 and K2 */",
4583                 "#ifndef SAFETY",
4584         "       if (S_A)",
4585         "       {       delta++;        /* _a_t  */",
4586                         "#ifndef NOFAIR",
4587         "               if (S_A > NFAIR)",
4588         "                       delta += NFAIR; /* _cnt[] */",
4589                         "#endif",
4590         "       }",
4591                 "#endif",
4592         "       memcpy((char *) &comp_now + delta, (char *) &K1, WS);",
4593         "       delta += WS;",
4594                 "#if HC>0",
4595         "       memcpy((char *) &comp_now + delta, (char *) &K2, HC);",
4596         "       delta += HC;",
4597                 "#endif",
4598         "       return delta;",
4599         "#else",
4600         "       char *vv = vin;",
4601         "       char *v = (char *) &comp_now;",
4602         "       int i;",
4603         "       for (i = 0; i < n; i++, vv++)",
4604         "               if (!Mask[i]) *v++ = *vv;",
4605         "       for (i = 0; i < WS-1; i++)",
4606         "               *v++ = 0;",
4607         "       v -= i;",
4608                 "#if 0",
4609         "       printf(\"compress %%d -> %%d\\n\",",
4610         "               n, v - (char *)&comp_now);",
4611                 "#endif",
4612         "       return v - (char *)&comp_now;",
4613         "#endif",
4614         "}",
4615 "#endif",
4616 "#endif",
4617         "#if defined(FULLSTACK) && defined(BITSTATE)",
4618 "#if defined(MA)",
4619         "#if !defined(onstack_now)",
4620         "int  onstack_now(void) {}", /* to suppress compiler errors */
4621         "#endif",
4622         "#if !defined(onstack_put)",
4623         "void onstack_put(void) {}", /* for this invalid combination */
4624         "#endif",
4625         "#if !defined(onstack_zap)",
4626         "void onstack_zap(void) {}", /* of directives */
4627         "#endif",
4628 "#else",
4629         "void",
4630         "onstack_zap(void)",
4631         "{      struct H_el *v, *w, *last = 0;",
4632         "       struct H_el **tmp = H_tab;",
4633         "       char *nv; int n, m;\n",
4634         "       H_tab = S_Tab;",
4635         "#ifndef NOCOMP",
4636         "       nv = (char *) &comp_now;",
4637         "       n = compress((char *)&now, vsize);",
4638         "#else",
4639                 "#if defined(BITSTATE) && defined(LC)",
4640         "       nv = (char *) &comp_now;",
4641         "       n = compact_stack((char *)&now, vsize);",
4642                 "#else",
4643         "       nv = (char *) &now;",
4644         "       n = vsize;",
4645                 "#endif",
4646         "#endif",
4647         "#if !defined(HC) && !(defined(BITSTATE) && defined(LC))",
4648         "       s_hash((uchar *)nv, n);",
4649         "#endif",
4650         "       H_tab = tmp;",
4651         "       for (v = S_Tab[j1]; v; Zh++, last=v, v=v->nxt)",
4652         "       {       m = memcmp(&(v->state), nv, n);",
4653         "               if (m == 0)",
4654         "                       goto Found;",
4655         "               if (m < 0)",
4656         "                       break;",
4657         "       }",
4658         "/* NotFound: */",
4659         "       Uerror(\"stack out of wack - zap\");",
4660         "       return;",
4661         "Found:",
4662         "       ZAPS++;",
4663         "       if (last)",
4664         "               last->nxt = v->nxt;",
4665         "       else",
4666         "               S_Tab[j1] = v->nxt;",
4667         "       v->tagged = (unsigned) n;",
4668         "#if !defined(NOREDUCE) && !defined(SAFETY)",
4669         "       v->proviso = 0;",
4670         "#endif",
4671         "       v->nxt = last = (struct H_el *) 0;",
4672         "       for (w = Free_list; w; Fa++, last=w, w = w->nxt)",
4673         "       {       if ((int) w->tagged <= n)",
4674         "               {       if (last)",
4675         "                       {       v->nxt = w; /* was: v->nxt = w->nxt; */",
4676         "                               last->nxt = v;",
4677         "                       } else",
4678         "                       {       v->nxt = Free_list;",
4679         "                               Free_list = v;",
4680         "                       }",
4681         "                       return;",
4682         "               }",
4683         "               if (!w->nxt)",
4684         "               {       w->nxt = v;",
4685         "                       return;",
4686         "       }       }",
4687         "       Free_list = v;",
4688         "}",
4689         "void",
4690         "onstack_put(void)",
4691         "{      struct H_el **tmp = H_tab;",
4692         "       H_tab = S_Tab;",
4693         "       if (hstore((char *)&now, vsize) != 0)",
4694         "#if defined(BITSTATE) && defined(LC)",
4695         "               printf(\"pan: warning, double stack entry\\n\");",
4696         "#else",
4697         "               Uerror(\"cannot happen - unstack_put\");",
4698         "#endif",
4699         "       H_tab = tmp;",
4700         "       trpt->ostate = Lstate;",
4701         "       PUT++;",
4702         "}",
4703         "int",
4704         "onstack_now(void)",
4705         "{      struct H_el *tmp;",
4706         "       struct H_el **tmp2 = H_tab;",
4707         "       char *v; int n, m = 1;\n",
4708         "       H_tab = S_Tab;",
4709         "#ifdef NOCOMP",
4710                 "#if defined(BITSTATE) && defined(LC)",
4711         "       v = (char *) &comp_now;",
4712         "       n = compact_stack((char *)&now, vsize);",
4713                 "#else",
4714         "       v = (char *) &now;",
4715         "       n = vsize;",
4716                 "#endif",
4717         "#else",
4718         "       v = (char *) &comp_now;",
4719         "       n = compress((char *)&now, vsize);",
4720         "#endif",
4721         "#if !defined(HC) && !(defined(BITSTATE) && defined(LC))",
4722         "       s_hash((uchar *)v, n);",
4723         "#endif",
4724         "       H_tab = tmp2;",
4725         "       for (tmp = S_Tab[j1]; tmp; Zn++, tmp = tmp->nxt)",
4726         "       {       m = memcmp(((char *)&(tmp->state)),v,n);",
4727         "               if (m <= 0)",
4728         "               {       Lstate = (struct H_el *) tmp;",
4729         "                       break;",
4730         "       }       }",
4731         "       PROBE++;",
4732         "       return (m == 0);",
4733         "}",
4734         "#endif",
4735 "#endif",
4736
4737         "#ifndef BITSTATE",
4738         "void",
4739         "hinit(void)",
4740         "{",
4741 "#ifdef MA",
4742         "#ifdef R_XPT",
4743         "       {       void r_xpoint(void);",
4744         "               r_xpoint();",
4745         "       }",
4746         "#else",
4747         "       dfa_init((unsigned short) (MA+a_cycles));",
4748         "#endif",
4749 "#endif",
4750 "#if !defined(MA) || defined(COLLAPSE)",
4751         "       H_tab = (struct H_el **)",
4752         "               emalloc((1L<<ssize)*sizeof(struct H_el *));",
4753 "#endif",
4754         "}",
4755         "#endif\n",
4756
4757         "#if !defined(BITSTATE) || defined(FULLSTACK)",
4758
4759         "#ifdef DEBUG",
4760         "void",
4761         "dumpstate(int wasnew, char *v, int n, int tag)",
4762         "{      int i;",
4763         "#ifndef SAFETY",
4764         "       if (S_A)",
4765         "       {       printf(\"\tstate tags %%d (%%d::%%d): \",",
4766         "                       V_A, wasnew, v[0]);",
4767                 "#ifdef FULLSTACK",
4768         "               printf(\" %%d \", tag);",
4769                 "#endif",
4770         "               printf(\"\\n\");",
4771         "       }",
4772         "#endif",
4773         "#ifdef SDUMP",
4774         "#ifndef NOCOMP",
4775         "       printf(\"\t State: \");",
4776         "       for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",",
4777         "               ((char *)&now)[i], Mask[i]?\"*\":\"\");",
4778         "#endif",
4779         "       printf(\"\\n\tVector: \");",
4780         "       for (i = 0; i < n; i++) printf(\"%%d,\", v[i]);",
4781         "       printf(\"\\n\");",
4782         "#endif",
4783         "}",
4784         "#endif",
4785
4786 "#ifdef MA",
4787         "int",
4788         "gstore(char *vin, int nin, uchar pbit)",
4789         "{      int n, i;",
4790         "       uchar *v;",
4791         "       static uchar Info[MA+1];",
4792         "#ifndef NOCOMP",
4793         "       n = compress(vin, nin);",
4794         "       v = (uchar *) &comp_now;",
4795         "#else",
4796         "       n = nin;",
4797         "       v = vin;",
4798         "#endif",
4799         "       if (n >= MA)",
4800         "       {       printf(\"pan: error, MA too small, recompile pan.c\");",
4801         "               printf(\" with -DMA=N with N>%%d\\n\", n);",
4802         "               Uerror(\"aborting\");",
4803         "       }",
4804         "       if (n > (int) maxgs) maxgs = (unsigned int) n;",
4805
4806         "       for (i = 0; i < n; i++)",
4807         "               Info[i] = v[i];",
4808         "       for ( ; i < MA-1; i++)",
4809         "               Info[i] = 0;",
4810         "       Info[MA-1] = pbit;",
4811         "       if (a_cycles)   /* place _a_t at the end */",
4812         "       {       Info[MA] = Info[0]; Info[0] = 0;  }",
4813         "       if (!dfa_store(Info))",
4814         "       {       if (pbit == 0",
4815         "               && (now._a_t&1)",
4816         "               &&  depth > A_depth)",
4817         "               {       Info[MA] &= ~(1|16|32); /* _a_t */",
4818         "                       if (dfa_member(MA))",   /* was !dfa_member(MA) */
4819         "                       {       Info[MA-1] = 4; /* off-stack bit */",
4820         "                               nShadow++;",
4821         "                               if (!dfa_member(MA-1))",
4822         "                               {",
4823         "#ifdef VERBOSE",
4824         "               printf(\"intersected 1st dfs stack\\n\");",
4825         "#endif",
4826         "                                       return 3;",
4827         "               }       }       }",
4828         "#ifdef VERBOSE",
4829         "               printf(\"new state\\n\");",
4830         "#endif",
4831         "               return 0;       /* new state */",
4832         "       }",
4833         "#ifdef FULLSTACK",
4834         "       if (pbit == 0)",
4835         "       {       Info[MA-1] = 1; /* proviso bit */",
4836         "#ifndef BFS",
4837         "               trpt->proviso = dfa_member(MA-1);",
4838         "#endif",
4839         "               Info[MA-1] = 4; /* off-stack bit */",
4840         "               if (dfa_member(MA-1)) {",
4841         "#ifdef VERBOSE",
4842         "                       printf(\"old state\\n\");",
4843         "#endif",
4844         "                       return 1; /* off-stack */",
4845         "               } else {",
4846         "#ifdef VERBOSE",
4847         "                       printf(\"on-stack\\n\");",
4848         "#endif",
4849         "                       return 2; /* on-stack */",
4850         "               }",
4851         "       }",
4852         "#endif",
4853         "#ifdef VERBOSE",
4854         "               printf(\"old state\\n\");",
4855         "#endif",
4856         "       return 1;       /* old state */",
4857         "}",
4858 "#endif",
4859
4860         "#if defined(BITSTATE) && defined(LC)",
4861         "int",
4862         "compact_stack(char *vin, int n)",      /* special case of HC4 */
4863         "{      int delta = 0;",
4864         "       s_hash((uchar *)vin, n); /* sets K1 and K2 */",
4865                 "#ifndef SAFETY",
4866         "       delta++;        /* room for state[0] |= 128 */",
4867                 "#endif",
4868         "       memcpy((char *) &comp_now + delta, (char *) &K1, WS);",
4869         "       delta += WS;",
4870         "       memcpy((char *) &comp_now + delta, (char *) &K2, WS);",
4871         "       delta += WS; /* use all available bits */",
4872         "       return delta;",
4873         "}",
4874         "#endif",
4875
4876         "int",
4877         "hstore(char *vin, int nin)     /* hash table storage */",
4878         "{      struct H_el *tmp, *ntmp, *olst = (struct H_el *) 0;",
4879         "       char *v; int n, m=0;",
4880         "#ifdef HC",
4881         "       uchar rem_a;",
4882         "#endif",
4883         "#ifdef NOCOMP",        /* defined by BITSTATE */
4884                 "#if defined(BITSTATE) && defined(LC)",
4885         "       if (S_Tab == H_tab)",
4886         "       {       v = (char *) &comp_now;",
4887         "               n = compact_stack(vin, nin);",
4888         "       } else",
4889         "       {       v = vin; n = nin;",
4890         "       }",
4891                 "#else",
4892         "       v = vin; n = nin;",
4893                 "#endif",
4894         "#else",
4895         "       v = (char *) &comp_now;",
4896         "       #ifdef HC",
4897         "       rem_a = now._a_t;",     /* 4.3.0 */
4898         "       now._a_t = 0;", /* for hashing/state matching to work right */
4899         "       #endif",
4900         "       n = compress(vin, nin);", /* with HC, this calls s_hash */
4901         "       #ifdef HC",
4902         "       now._a_t = rem_a;",     /* 4.3.0 */
4903         "       #endif",
4904                 "#ifndef SAFETY",
4905         "       if (S_A)",
4906         "       {       v[0] = 0;       /* _a_t  */",
4907                         "#ifndef NOFAIR",
4908         "               if (S_A > NFAIR)",
4909         "               for (m = 0; m < NFAIR; m++)",
4910         "                       v[m+1] = 0;     /* _cnt[] */",
4911                         "#endif",
4912         "               m = 0;",
4913         "       }",
4914                 "#endif",
4915         "#endif",
4916         "#if !defined(HC) && !(defined(BITSTATE) && defined(LC))",
4917         "       s_hash((uchar *)v, n);",
4918         "#endif",
4919         "       tmp = H_tab[j1];",
4920         "       if (!tmp)",
4921         "       {  tmp = grab_state(n);",
4922         "          H_tab[j1] = tmp;",
4923         "       } else",
4924         "       {  for (;; hcmp++, olst = tmp, tmp = tmp->nxt)",
4925         "          {   /* skip the _a_t and the _cnt bytes */",
4926         "#ifdef COLLAPSE",
4927         "               if (tmp->ln != 0)",
4928         "               {       if (!tmp->nxt) goto Append;",
4929         "                       continue;",
4930         "               }",
4931         "#endif",
4932         "               m = memcmp(((char *)&(tmp->state)) + S_A, ",
4933         "                       v + S_A, n - S_A);",
4934         "               if (m == 0) {",
4935         "#ifdef SAFETY",
4936                         "#define wasnew 0",
4937         "#else",
4938         "               int wasnew = 0;",
4939         "#endif",
4940
4941         "#ifndef SAFETY",
4942         "#ifndef NOCOMP",
4943         "               if (S_A)",
4944         "               { if ((((char *)&(tmp->state))[0] & V_A) != V_A)",
4945         "                 {     wasnew = 1; nShadow++;",
4946         "                       ((char *)&(tmp->state))[0] |= V_A;",
4947         "                 }",
4948                 "#ifndef NOFAIR",
4949         "                 if (S_A > NFAIR)",
4950         "                 {     /* 0 <= now._cnt[now._a_t&1] < MAXPROC */",
4951         "                       unsigned ci, bp; /* index, bit pos */",
4952         "                       ci = (now._cnt[now._a_t&1] / 8);",
4953         "                       bp = (now._cnt[now._a_t&1] - 8*ci);",
4954         "                       if (now._a_t&1) /* use tail-bits in _cnt */",
4955         "                       {       ci = (NFAIR - 1) - ci;",
4956         "                               bp = 7 - bp; /* bp = 0..7 */",
4957         "                       }",
4958         "                       ci++;   /* skip over _a_t */",
4959         "                       bp = 1 << bp;   /* the bit mask */",
4960         "                       if ((((char *)&(tmp->state))[ci] & bp)==0)",
4961         "                       {       if (!wasnew)",
4962         "                               {       wasnew = 1;",
4963         "                                       nShadow++;",
4964         "                               }",
4965         "                               ((char *)&(tmp->state))[ci] |= bp;",
4966         "                       }",
4967         "                  }",
4968         "                  /* else: wasnew == 0, i.e., old state */",
4969                 "#endif",
4970         "               }",
4971         "#endif",
4972         "#endif",
4973
4974         "#ifdef FULLSTACK",
4975                 "#ifndef SAFETY",       /* or else wasnew == 0 */
4976         "               if (wasnew)",
4977         "               {       Lstate = (struct H_el *) tmp;",
4978         "                       tmp->tagged |= V_A;",
4979         "                       if ((now._a_t&1)",
4980         "                       && (tmp->tagged&A_V)",
4981         "                       && depth > A_depth)",
4982         "                       {",
4983         "intersect:",
4984                 "#ifdef CHECK",
4985         "       printf(\"1st dfs-stack intersected on state %%d+\\n\",",
4986         "               (int) tmp->st_id);",
4987                 "#endif",
4988         "                               return 3;",
4989         "                       }",
4990                 "#ifdef CHECK",
4991         "       printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);",
4992                 "#endif",
4993                 "#ifdef DEBUG",
4994         "       dumpstate(1, (char *)&(tmp->state),n,tmp->tagged);",
4995                 "#endif",
4996         "                       return 0;",
4997         "               } else",
4998                 "#endif",
4999         "               if ((S_A)?(tmp->tagged&V_A):tmp->tagged)",
5000         "               {       Lstate = (struct H_el *) tmp;",
5001                 "#ifndef SAFETY",
5002         "                       /* already on current dfs stack */",
5003         "                       /* but may also be on 1st dfs stack */",
5004         "                       if ((now._a_t&1)",
5005         "                       && (tmp->tagged&A_V)",
5006
5007         "                       && depth > A_depth",
5008                 /* new (Zhang's example) */
5009                 "#ifndef NOFAIR",
5010         "                       && (!fairness || now._cnt[1] <= 1)",
5011                 "#endif",
5012         "                       )",
5013
5014         "                               goto intersect;",
5015                 "#endif",
5016                 "#ifdef CHECK",
5017         "       printf(\"\tStack state %%d\\n\", (int) tmp->st_id);",
5018                 "#endif",
5019                 "#ifdef DEBUG",
5020         "       dumpstate(0, (char *)&(tmp->state),n,tmp->tagged);",
5021                 "#endif",
5022         "                       return 2; /* match on stack */",
5023         "               }",
5024         "#else",
5025         "               if (wasnew)",
5026         "               {",
5027                 "#ifdef CHECK",
5028         "       printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);",
5029                 "#endif",
5030                 "#ifdef DEBUG",
5031         "       dumpstate(1, (char *)&(tmp->state), n, 0);",
5032                 "#endif",
5033         "                       return 0;",
5034         "               }",
5035         "#endif",
5036                 "#ifdef CHECK",
5037         "       printf(\"\tOld state %%d\\n\", (int) tmp->st_id);",
5038                 "#endif",
5039                 "#ifdef DEBUG",
5040         "       dumpstate(0, (char *)&(tmp->state), n, 0);",
5041                 "#endif",
5042         "#ifdef REACH",
5043         "               if (tmp->D > depth)",
5044         "               {       tmp->D = depth;",
5045                 "#ifdef CHECK",
5046         "       printf(\"\t\tReVisiting (from smaller depth)\\n\");",
5047                 "#endif",
5048         "                       nstates--;",
5049 #if 0
5050   possible variation of iterative search for shortest counter-example (pan -i
5051   and pan -I) suggested by Pierre Moro (for safety properties):
5052   state revisits on shorter depths do not start until after
5053   the first counter-example is found.  this assumes that the max search
5054   depth is set large enough that a first (possibly long) counter-example
5055   can be found
5056   if set too short, this variant can miss the counter-example, even if
5057   it would otherwise be shorter than the depth-limit.
5058   (p.m. unsure if this preserves the guarantee of finding the
5059    shortest counter-example - so not enabled yet)
5060         "                       if (errors > 0 && iterative)", /* Moro */
5061 #endif
5062         "                       return 0;",
5063         "               }",
5064         "#endif",
5065         "#if defined(BFS) && defined(Q_PROVISO)",
5066         "               Lstate = (struct H_el *) tmp;",
5067         "#endif",
5068         "               return 1; /* match outside stack */",
5069         "              } else if (m < 0)",
5070         "              {        /* insert state before tmp */",
5071         "                       ntmp = grab_state(n);",
5072         "                       ntmp->nxt = tmp;",
5073         "                       if (!olst)",
5074         "                               H_tab[j1] = ntmp;",
5075         "                       else",
5076         "                               olst->nxt = ntmp;",
5077         "                       tmp = ntmp;",
5078         "                       break;",
5079         "              } else if (!tmp->nxt)",
5080         "              {        /* append after tmp */",
5081         "#ifdef COLLAPSE",
5082         "Append:",
5083         "#endif",
5084         "                       tmp->nxt = grab_state(n);",
5085         "                       tmp = tmp->nxt;",
5086         "                       break;",
5087         "          }   }",
5088         "       }",
5089         "#ifdef CHECK",
5090         "       tmp->st_id = (unsigned) nstates;",
5091                 "#ifdef BITSTATE",
5092         "       printf(\"       Push state %%d\\n\", ((int) nstates) - 1);",
5093                 "#else",
5094         "       printf(\"       New state %%d\\n\", (int) nstates);",
5095                 "#endif",
5096         "#endif",
5097         "#if !defined(SAFETY) || defined(REACH)",
5098         "       tmp->D = depth;",
5099         "#endif",
5100         "#ifndef SAFETY",
5101         "#ifndef NOCOMP",
5102         "       if (S_A)",
5103         "       {       v[0] = V_A;",
5104                 "#ifndef NOFAIR",
5105         "               if (S_A > NFAIR)",
5106         "               {       unsigned ci, bp; /* as above */",
5107         "                       ci = (now._cnt[now._a_t&1] / 8);",
5108         "                       bp = (now._cnt[now._a_t&1] - 8*ci);",
5109         "                       if (now._a_t&1)",
5110         "                       {       ci = (NFAIR - 1) - ci;",
5111         "                               bp = 7 - bp; /* bp = 0..7 */",
5112         "                       }",
5113         "                       v[1+ci] = 1 << bp;",
5114         "               }",
5115                 "#endif",
5116         "       }",
5117         "#endif",
5118         "#endif",
5119         "       memcpy(((char *)&(tmp->state)), v, n);",
5120         "#ifdef FULLSTACK",
5121         "       tmp->tagged = (S_A)?V_A:(depth+1);",
5122                 "#ifdef DEBUG",
5123         "       dumpstate(-1, v, n, tmp->tagged);",
5124                 "#endif",
5125         "       Lstate = (struct H_el *) tmp;",
5126         "#else",
5127                 "#ifdef DEBUG",
5128         "       dumpstate(-1, v, n, 0);",
5129                 "#endif",
5130         "#endif",
5131         "       return 0;",
5132         "}",
5133         "#endif",
5134         "#include TRANSITIONS",
5135         "void",
5136         "do_reach(void)",
5137         "{",
5138         0,
5139 };