5140 lines
134 KiB
C
Executable file
5140 lines
134 KiB
C
Executable file
/***** spin: pangen1.h *****/
|
|
|
|
/* Copyright (c) 1989-2005 by Lucent Technologies, Bell Laboratories. */
|
|
/* All Rights Reserved. This software is for educational purposes only. */
|
|
/* No guarantee whatsoever is expressed or implied by the distribution of */
|
|
/* this code. Permission is given to distribute this code provided that */
|
|
/* this introductory message is not removed and no monies are exchanged. */
|
|
/* Software written by Gerard J. Holzmann. For tool documentation see: */
|
|
/* http://spinroot.com/ */
|
|
/* Send all bug-reports and/or questions to: bugs@spinroot.com */
|
|
|
|
static char *Code2a[] = { /* the tail of procedure run() */
|
|
"#if defined(VERI) && !defined(NOREDUCE) && !defined(NP)",
|
|
" if (!state_tables",
|
|
"#ifdef HAS_CODE",
|
|
" && !readtrail",
|
|
"#endif",
|
|
" )",
|
|
" { printf(\"warning: for p.o. reduction to be valid \");",
|
|
" printf(\"the never claim must be stutter-invariant\\n\");",
|
|
" printf(\"(never claims generated from LTL \");",
|
|
" printf(\"formulae are stutter-invariant)\\n\");",
|
|
" }",
|
|
"#endif",
|
|
" UnBlock; /* disable rendez-vous */",
|
|
"#ifdef BITSTATE",
|
|
#ifndef POWOW
|
|
" if (udmem)",
|
|
" { udmem *= 1024L*1024L;",
|
|
" SS = (uchar *) emalloc(udmem);",
|
|
" bstore = bstore_mod;",
|
|
" } else",
|
|
#endif
|
|
" SS = (uchar *) emalloc(1L<<(ssize-3));",
|
|
"#else",
|
|
" hinit();",
|
|
"#endif",
|
|
"#if defined(FULLSTACK) && defined(BITSTATE)",
|
|
" onstack_init();",
|
|
"#endif",
|
|
"#if defined(CNTRSTACK) && !defined(BFS)",
|
|
" LL = (uchar *) emalloc(1L<<(ssize-3));",
|
|
"#endif",
|
|
" stack = ( Stack *) emalloc(sizeof(Stack));",
|
|
" svtack = (Svtack *) emalloc(sizeof(Svtack));",
|
|
" /* a place to point for Pptr of non-running procs: */",
|
|
" noptr = (uchar *) emalloc(Maxbody * sizeof(char));",
|
|
"#ifdef SVDUMP",
|
|
" if (vprefix > 0)",
|
|
" write(svfd, (uchar *) &vprefix, sizeof(int));",
|
|
"#endif",
|
|
"#ifdef VERI",
|
|
" Addproc(VERI); /* never - pid = 0 */",
|
|
"#endif",
|
|
" active_procs(); /* started after never */",
|
|
"#ifdef EVENT_TRACE",
|
|
" now._event = start_event;",
|
|
" reached[EVENT_TRACE][start_event] = 1;",
|
|
"#endif",
|
|
|
|
"#ifdef HAS_CODE",
|
|
" globinit();",
|
|
"#endif",
|
|
"#ifdef BITSTATE",
|
|
"go_again:",
|
|
"#endif",
|
|
" do_the_search();",
|
|
"#ifdef BITSTATE",
|
|
" if (--Nrun > 0 && HASH_CONST[++HASH_NR])",
|
|
" { printf(\"Run %%d:\\n\", HASH_NR);",
|
|
" wrap_stats();",
|
|
" printf(\"\\n\");",
|
|
" memset(SS, 0, 1L<<(ssize-3));",
|
|
"#if defined(CNTRSTACK)",
|
|
" memset(LL, 0, 1L<<(ssize-3));",
|
|
"#endif",
|
|
"#if defined(FULLSTACK)",
|
|
" memset((uchar *) S_Tab, 0, ",
|
|
" maxdepth*sizeof(struct H_el *));",
|
|
"#endif",
|
|
" nstates=nlinks=truncs=truncs2=ngrabs = 0;",
|
|
" nlost=nShadow=hcmp = 0;",
|
|
" Fa=Fh=Zh=Zn = 0;",
|
|
" PUT=PROBE=ZAPS=Ccheck=Cholds = 0;",
|
|
" goto go_again;",
|
|
" }",
|
|
"#endif",
|
|
"}",
|
|
"#ifdef HAS_PROVIDED",
|
|
"int provided(int, uchar, int, Trans *);",
|
|
"#endif",
|
|
|
|
#ifndef PRINTF
|
|
"int",
|
|
"Printf(const char *fmt, ...)",
|
|
"{ /* Make sure the args to Printf",
|
|
" * are always evaluated (e.g., they",
|
|
" * could contain a run stmnt)",
|
|
" * but do not generate the output",
|
|
" * during verification runs",
|
|
" * unless explicitly wanted",
|
|
" * If this fails on your system",
|
|
" * compile SPIN itself -DPRINTF",
|
|
" * and this code is not generated",
|
|
" */",
|
|
"#ifdef HAS_CODE",
|
|
" if (readtrail)",
|
|
" { va_list args;",
|
|
" va_start(args, fmt);",
|
|
" vprintf(fmt, args);",
|
|
" va_end(args);",
|
|
" return 1;",
|
|
" }",
|
|
"#endif",
|
|
"#ifdef PRINTF",
|
|
" va_list args;",
|
|
" va_start(args, fmt);",
|
|
" vprintf(fmt, args);",
|
|
" va_end(args);",
|
|
"#endif",
|
|
" return 1;",
|
|
"}",
|
|
#endif
|
|
"extern void printm(int);",
|
|
|
|
"#ifndef SC",
|
|
"#define getframe(i) &trail[i];",
|
|
"#else",
|
|
"static long HHH, DDD, hiwater;",
|
|
"static long CNT1, CNT2;",
|
|
"static int stackwrite;",
|
|
"static int stackread;",
|
|
"static Trail frameptr;",
|
|
"Trail *",
|
|
"getframe(int d)",
|
|
"{",
|
|
" if (CNT1 == CNT2)",
|
|
" return &trail[d];",
|
|
"",
|
|
" if (d >= (CNT1-CNT2)*DDD)",
|
|
" return &trail[d - (CNT1-CNT2)*DDD];",
|
|
"",
|
|
" if (!stackread",
|
|
" && (stackread = open(stackfile, 0)) < 0)",
|
|
" { printf(\"getframe: cannot open %%s\\n\", stackfile);",
|
|
" wrapup();",
|
|
" }",
|
|
" if (lseek(stackread, d* (off_t) sizeof(Trail), SEEK_SET) == -1",
|
|
" || read(stackread, &frameptr, sizeof(Trail)) != sizeof(Trail))",
|
|
" { printf(\"getframe: frame read error\\n\");",
|
|
" wrapup();",
|
|
" }",
|
|
" return &frameptr;",
|
|
"}",
|
|
"#endif",
|
|
|
|
"#if !defined(SAFETY) && !defined(BITSTATE)",
|
|
"#if !defined(FULLSTACK) || defined(MA)",
|
|
"#define depth_of(x) A_depth /* an estimate */",
|
|
"#else",
|
|
"int",
|
|
"depth_of(struct H_el *s)",
|
|
"{ Trail *t; int d;",
|
|
" for (d = 0; d <= A_depth; d++)",
|
|
" { t = getframe(d);",
|
|
" if (s == t->ostate)",
|
|
" return d;",
|
|
" }",
|
|
" printf(\"pan: cannot happen, depth_of\\n\");",
|
|
" return depthfound;",
|
|
"}",
|
|
"#endif",
|
|
"#endif",
|
|
|
|
"void",
|
|
"pan_exit(int val)",
|
|
"{ if (signoff) printf(\"--end of output--\\n\");",
|
|
" exit(val);",
|
|
"}",
|
|
|
|
"#ifdef HAS_CODE",
|
|
"char *",
|
|
"transmognify(char *s)",
|
|
"{ char *v, *w;",
|
|
" static char buf[2][2048];",
|
|
" int i, toggle = 0;",
|
|
|
|
" if (!s || strlen(s) > 2047) return s;",
|
|
" memset(buf[0], 0, 2048);",
|
|
" memset(buf[1], 0, 2048);",
|
|
" strcpy(buf[toggle], s);",
|
|
" while ((v = strstr(buf[toggle], \"{c_code\")))", /* assign v */
|
|
" { *v = '\\0'; v++;",
|
|
" strcpy(buf[1-toggle], buf[toggle]);",
|
|
" for (w = v; *w != '}' && *w != '\\0'; w++) /* skip */;",
|
|
" if (*w != '}') return s;",
|
|
" *w = '\\0'; w++;",
|
|
" for (i = 0; code_lookup[i].c; i++)",
|
|
" if (strcmp(v, code_lookup[i].c) == 0",
|
|
" && strlen(v) == strlen(code_lookup[i].c))",
|
|
" { if (strlen(buf[1-toggle])",
|
|
" + strlen(code_lookup[i].t)",
|
|
" + strlen(w) > 2047)",
|
|
" return s;",
|
|
" strcat(buf[1-toggle], code_lookup[i].t);",
|
|
" break;",
|
|
" }",
|
|
" strcat(buf[1-toggle], w);",
|
|
" toggle = 1 - toggle;",
|
|
" }",
|
|
" buf[toggle][2047] = '\\0';",
|
|
" return buf[toggle];",
|
|
"}",
|
|
"#else",
|
|
"char * transmognify(char *s) { return s; }",
|
|
"#endif",
|
|
|
|
"#ifdef HAS_CODE",
|
|
"void",
|
|
"add_src_txt(int ot, int tt)",
|
|
"{ Trans *t;",
|
|
" char *q;",
|
|
"",
|
|
" for (t = trans[ot][tt]; t; t = t->nxt)",
|
|
" { printf(\"\\t\\t\");",
|
|
|
|
" q = transmognify(t->tp);",
|
|
" for ( ; q && *q; q++)",
|
|
" if (*q == '\\n')",
|
|
" printf(\"\\\\n\");",
|
|
" else",
|
|
" putchar(*q);",
|
|
" printf(\"\\n\");",
|
|
" }",
|
|
"}",
|
|
"void",
|
|
"wrap_trail(void)",
|
|
"{ static int wrap_in_progress = 0;",
|
|
" int i; short II;",
|
|
" P0 *z;",
|
|
"",
|
|
" if (wrap_in_progress++) return;",
|
|
"",
|
|
" printf(\"spin: trail ends after %%ld steps\\n\", depth);",
|
|
" if (onlyproc >= 0)",
|
|
" { if (onlyproc >= now._nr_pr) pan_exit(0);",
|
|
" II = onlyproc;",
|
|
" z = (P0 *)pptr(II);",
|
|
" printf(\"%%3ld:\tproc %%d (%%s) \",",
|
|
" depth, II, procname[z->_t]);",
|
|
" for (i = 0; src_all[i].src; i++)",
|
|
" if (src_all[i].tp == (int) z->_t)",
|
|
" { printf(\" line %%3d\",",
|
|
" src_all[i].src[z->_p]);",
|
|
" break;",
|
|
" }",
|
|
" printf(\" (state %%2d)\", z->_p);",
|
|
" if (!stopstate[z->_t][z->_p])",
|
|
" printf(\" (invalid end state)\");",
|
|
" printf(\"\\n\");",
|
|
" add_src_txt(z->_t, z->_p);",
|
|
" pan_exit(0);",
|
|
" }",
|
|
" printf(\"#processes %%d:\\n\", now._nr_pr);",
|
|
" if (depth < 0) depth = 0;",
|
|
" for (II = 0; II < now._nr_pr; II++)",
|
|
" { z = (P0 *)pptr(II);",
|
|
" printf(\"%%3ld:\tproc %%d (%%s) \",",
|
|
" depth, II, procname[z->_t]);",
|
|
" for (i = 0; src_all[i].src; i++)",
|
|
" if (src_all[i].tp == (int) z->_t)",
|
|
" { printf(\" line %%3d\",",
|
|
" src_all[i].src[z->_p]);",
|
|
" break;",
|
|
" }",
|
|
" printf(\" (state %%2d)\", z->_p);",
|
|
" if (!stopstate[z->_t][z->_p])",
|
|
" printf(\" (invalid end state)\");",
|
|
" printf(\"\\n\");",
|
|
" add_src_txt(z->_t, z->_p);",
|
|
" }",
|
|
" c_globals();",
|
|
" for (II = 0; II < now._nr_pr; II++)",
|
|
" { z = (P0 *)pptr(II);",
|
|
" c_locals(II, z->_t);",
|
|
" }",
|
|
"#ifdef ON_EXIT",
|
|
" ON_EXIT;",
|
|
"#endif",
|
|
" pan_exit(0);",
|
|
"}",
|
|
"FILE *",
|
|
"findtrail(void)",
|
|
"{ FILE *fd;",
|
|
" char fnm[512], *q;",
|
|
" char MyFile[512];",
|
|
"",
|
|
" strcpy(MyFile, TrailFile);", /* avoid problem with non-writable strings */
|
|
"",
|
|
" if (whichtrail)",
|
|
" { sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);",
|
|
" fd = fopen(fnm, \"r\");",
|
|
" if (fd == NULL && (q = strchr(MyFile, \'.\')))",
|
|
" { *q = \'\\0\';", /* e.g., strip .pml on original file */
|
|
" sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);",
|
|
" *q = \'.\';",
|
|
" fd = fopen(fnm, \"r\");",
|
|
" if (fd == NULL)",
|
|
" { printf(\"pan: cannot find %%s%%d.%%s or %%s\\n\", ",
|
|
" MyFile, whichtrail, tprefix, fnm);",
|
|
" pan_exit(1);",
|
|
" } }",
|
|
" } else",
|
|
" { sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
|
|
" fd = fopen(fnm, \"r\");",
|
|
" if (fd == NULL && (q = strchr(MyFile, \'.\')))",
|
|
" { *q = \'\\0\';", /* e.g., strip .pml on original file */
|
|
" sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
|
|
" *q = \'.\';",
|
|
" fd = fopen(fnm, \"r\");",
|
|
" if (fd == NULL)",
|
|
" { printf(\"pan: cannot find %%s.%%s or %%s\\n\", ",
|
|
" MyFile, tprefix, fnm);",
|
|
" pan_exit(1);",
|
|
" } } }",
|
|
" if (fd == NULL)",
|
|
" { printf(\"pan: cannot find trailfile %%s\\n\", fnm);",
|
|
" pan_exit(1);",
|
|
" }",
|
|
" return fd;",
|
|
"}",
|
|
"",
|
|
"uchar do_transit(Trans *, short);",
|
|
"",
|
|
"void",
|
|
"getrail(void)",
|
|
"{ FILE *fd;",
|
|
" char *q;",
|
|
" int i, t_id, lastnever=-1; short II;",
|
|
" Trans *t;",
|
|
" P0 *z;",
|
|
"",
|
|
" fd = findtrail(); /* exits if unsuccessful */",
|
|
" while (fscanf(fd, \"%%ld:%%d:%%d\\n\", &depth, &i, &t_id) == 3)",
|
|
" { if (depth == -1)",
|
|
" printf(\"<<<<<START OF CYCLE>>>>>\\n\");",
|
|
" if (depth < 0)",
|
|
" continue;",
|
|
" if (i > now._nr_pr)",
|
|
" { printf(\"pan: Error, proc %%d invalid pid \", i);",
|
|
" printf(\"transition %%d\\n\", t_id);",
|
|
" break;",
|
|
" }",
|
|
" II = i;",
|
|
"",
|
|
" z = (P0 *)pptr(II);",
|
|
" for (t = trans[z->_t][z->_p]; t; t = t->nxt)",
|
|
" if (t->t_id == t_id)",
|
|
" break;",
|
|
" if (!t)",
|
|
" { for (i = 0; i < NrStates[z->_t]; i++)",
|
|
" { t = trans[z->_t][i];",
|
|
" if (t && t->t_id == t_id)",
|
|
" { printf(\" Recovered at state %%d\\n\", i);",
|
|
" z->_p = i;",
|
|
" goto recovered;",
|
|
" } }",
|
|
" printf(\"pan: Error, proc %%d type %%d state %%d: \",",
|
|
" II, z->_t, z->_p);",
|
|
" printf(\"transition %%d not found\\n\", t_id);",
|
|
" for (t = trans[z->_t][z->_p]; t; t = t->nxt)",
|
|
" printf(\" t_id %%d -- case %%d, [%%s]\\n\",",
|
|
" t->t_id, t->forw, t->tp);",
|
|
" break; /* pan_exit(1); */",
|
|
" }",
|
|
"recovered:",
|
|
" q = transmognify(t->tp);",
|
|
" if (gui) simvals[0] = \'\\0\';",
|
|
|
|
" this = pptr(II);",
|
|
" trpt->tau |= 1;", /* timeout always possible */
|
|
" if (!do_transit(t, II))",
|
|
" { if (onlyproc >= 0 && II != onlyproc)",
|
|
" goto moveon;",
|
|
" printf(\"pan: error, next transition UNEXECUTABLE on replay\\n\");",
|
|
" printf(\" most likely causes: missing c_track statements\\n\");",
|
|
" printf(\" or illegal side-effects in c_expr statements\\n\");",
|
|
" }",
|
|
|
|
" if (onlyproc >= 0 && II != onlyproc)",
|
|
" goto moveon;",
|
|
|
|
" if (verbose)",
|
|
" { printf(\"depth: %%3ld proc: %%3d trans: %%3d (%%d procs) \",",
|
|
" depth, II, t_id, now._nr_pr);",
|
|
" printf(\"forw=%%3d [%%s]\\n\", t->forw, q);",
|
|
"",
|
|
" c_globals();",
|
|
" for (i = 0; i < now._nr_pr; i++)",
|
|
" { c_locals(i, ((P0 *)pptr(i))->_t);",
|
|
" }",
|
|
" } else",
|
|
" if (strcmp(procname[z->_t], \":never:\") == 0)",
|
|
" { if (lastnever != (int) z->_p)",
|
|
" { for (i = 0; src_all[i].src; i++)",
|
|
" if (src_all[i].tp == (int) z->_t)",
|
|
" { printf(\"MSC: ~G %%d\\n\",",
|
|
" src_all[i].src[z->_p]);",
|
|
" break;",
|
|
" }",
|
|
" if (!src_all[i].src)",
|
|
" printf(\"MSC: ~R %%d\\n\", z->_p);",
|
|
" }",
|
|
" lastnever = z->_p;",
|
|
" goto sameas;",
|
|
" } else",
|
|
" if (strcmp(procname[z->_t], \":np_:\") != 0)",
|
|
" {",
|
|
"sameas: if (no_rck) goto moveon;",
|
|
" if (coltrace)",
|
|
" { printf(\"%%ld: \", depth);",
|
|
" for (i = 0; i < II; i++)",
|
|
" printf(\"\\t\\t\");",
|
|
" printf(\"%%s(%%d):\", procname[z->_t], II);",
|
|
" printf(\"[%%s]\\n\", q?q:\"\");",
|
|
" } else if (!silent)",
|
|
" { if (strlen(simvals) > 0) {",
|
|
" printf(\"%%3ld: proc %%2d (%%s)\", ",
|
|
" depth, II, procname[z->_t]);",
|
|
" for (i = 0; src_all[i].src; i++)",
|
|
" if (src_all[i].tp == (int) z->_t)",
|
|
" { printf(\" line %%3d \\\"pan_in\\\" \",",
|
|
" src_all[i].src[z->_p]);",
|
|
" break;",
|
|
" }",
|
|
" printf(\"(state %%d)\t[values: %%s]\\n\", z->_p, simvals);",
|
|
" }",
|
|
" printf(\"%%3ld: proc %%2d (%%s)\", ",
|
|
" depth, II, procname[z->_t]);",
|
|
" for (i = 0; src_all[i].src; i++)",
|
|
" if (src_all[i].tp == (int) z->_t)",
|
|
" { printf(\" line %%3d \\\"pan_in\\\" \",",
|
|
" src_all[i].src[z->_p]);",
|
|
" break;",
|
|
" }",
|
|
" printf(\"(state %%d)\t[%%s]\\n\", z->_p, q?q:\"\");",
|
|
" printf(\"\\n\");",
|
|
" } }",
|
|
"moveon: z->_p = t->st;",
|
|
" }",
|
|
" wrap_trail();",
|
|
"}",
|
|
"#endif",
|
|
"int",
|
|
"f_pid(int pt)",
|
|
"{ int i;",
|
|
" P0 *z;",
|
|
" for (i = 0; i < now._nr_pr; i++)",
|
|
" { z = (P0 *)pptr(i);",
|
|
" if (z->_t == (unsigned) pt)",
|
|
" return BASE+z->_pid;",
|
|
" }",
|
|
" return -1;",
|
|
"}",
|
|
"#ifdef VERI",
|
|
"void check_claim(int);",
|
|
"#endif",
|
|
"",
|
|
"#ifdef BITSTATE",
|
|
#ifndef POWOW
|
|
"int",
|
|
"bstore_mod(char *v, int n) /* hasharray size not a power of two */",
|
|
"{ unsigned long x, y;",
|
|
" unsigned int i = 1;",
|
|
"",
|
|
" d_hash((uchar *) v, n); /* sets j3, j4, K1, K2 */",
|
|
" x = K2; y = j3;",
|
|
" for (;;)",
|
|
" { if (!(SS[x%%udmem]&(1<<y))) break;", /* take the hit in speed */
|
|
" if (i == hfns) {",
|
|
"#ifdef DEBUG",
|
|
" printf(\"Old bitstate\\n\");",
|
|
"#endif",
|
|
" return 1;",
|
|
" }",
|
|
" x = (x + K1 + i);", /* no mask, using mod */
|
|
" y = (y + j4) & 7;",
|
|
" i++;",
|
|
" }",
|
|
"#ifdef RANDSTOR",
|
|
" if (rand()%%100 > RANDSTOR) return 0;",
|
|
"#endif",
|
|
" for (;;)",
|
|
" { SS[x%%udmem] |= (1<<y);",
|
|
" if (i == hfns) break;", /* done */
|
|
" x = (x + K1 + i);", /* no mask */
|
|
" y = (y + j4) & 7;",
|
|
" i++;",
|
|
" }",
|
|
"#ifdef DEBUG",
|
|
" printf(\"New bitstate\\n\");",
|
|
"#endif",
|
|
" if (now._a_t&1)",
|
|
" { nShadow++;",
|
|
" }",
|
|
" return 0;",
|
|
"}",
|
|
#endif
|
|
"int",
|
|
"bstore_reg(char *v, int n) /* extended hashing, Peter Dillinger, 2004 */",
|
|
"{ unsigned long x, y;",
|
|
" unsigned int i = 1;",
|
|
"",
|
|
" d_hash((uchar *) v, n); /* sets j1-j4 */",
|
|
" x = j2; y = j3;",
|
|
" for (;;)",
|
|
" { if (!(SS[x]&(1<<y))) break;", /* at least one bit not set */
|
|
" if (i == hfns) {",
|
|
"#ifdef DEBUG",
|
|
" printf(\"Old bitstate\\n\");",
|
|
"#endif",
|
|
" return 1;",
|
|
" }",
|
|
" x = (x + j1 + i) & nmask;",
|
|
" y = (y + j4) & 7;",
|
|
" i++;",
|
|
" }",
|
|
"#ifdef RANDSTOR",
|
|
" if (rand()%%100 > RANDSTOR) return 0;",
|
|
"#endif",
|
|
" for (;;)",
|
|
" { SS[x] |= (1<<y);",
|
|
" if (i == hfns) break;", /* done */
|
|
" x = (x + j1 + i) & nmask;",
|
|
" y = (y + j4) & 7;",
|
|
" i++;",
|
|
" }",
|
|
"#ifdef DEBUG",
|
|
" printf(\"New bitstate\\n\");",
|
|
"#endif",
|
|
" if (now._a_t&1)",
|
|
" { nShadow++;",
|
|
" }",
|
|
" return 0;",
|
|
"}",
|
|
"#endif",
|
|
"unsigned long TMODE = 0666; /* file permission bits for trail files */",
|
|
"",
|
|
"int trcnt=1;",
|
|
"char snap[64], fnm[512];",
|
|
"",
|
|
"int",
|
|
"make_trail(void)",
|
|
"{ int fd;",
|
|
" char *q;",
|
|
" char MyFile[512];",
|
|
"",
|
|
" q = strrchr(TrailFile, \'/\');",
|
|
" if (q == NULL) q = TrailFile; else q++;",
|
|
" strcpy(MyFile, q); /* TrailFile is not a writable string */",
|
|
"",
|
|
" if (iterative == 0 && Nr_Trails++ > 0)",
|
|
" sprintf(fnm, \"%%s%%d.%%s\",",
|
|
" MyFile, Nr_Trails-1, tprefix);",
|
|
" else",
|
|
" sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
|
|
"",
|
|
" if ((fd = creat(fnm, TMODE)) < 0)",
|
|
" { if ((q = strchr(MyFile, \'.\')))",
|
|
" { *q = \'\\0\';", /* strip .pml */
|
|
" if (iterative == 0 && Nr_Trails-1 > 0)",
|
|
" sprintf(fnm, \"%%s%%d.%%s\",",
|
|
" MyFile, Nr_Trails-1, tprefix);",
|
|
" else",
|
|
" sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
|
|
" *q = \'.\';",
|
|
" fd = creat(fnm, TMODE);",
|
|
" } }",
|
|
" if (fd < 0)",
|
|
" { printf(\"pan: cannot create %%s\\n\", fnm);",
|
|
" perror(\"cause\");",
|
|
" } else",
|
|
" { printf(\"pan: wrote %%s\\n\", fnm);",
|
|
" }",
|
|
" return fd;",
|
|
"}",
|
|
0
|
|
};
|
|
|
|
static char *Code2b[] = { /* breadth-first search option */
|
|
"#ifdef BFS",
|
|
"#define Q_PROVISO",
|
|
"#ifndef INLINE_REV",
|
|
"#define INLINE_REV",
|
|
"#endif",
|
|
"",
|
|
"typedef struct SV_Hold {",
|
|
" State *sv;",
|
|
" int sz;",
|
|
" struct SV_Hold *nxt;",
|
|
"} SV_Hold;",
|
|
"",
|
|
"typedef struct EV_Hold {",
|
|
" char *sv;", /* Mask */
|
|
" int sz;", /* vsize */
|
|
" int nrpr;",
|
|
" int nrqs;",
|
|
"#if VECTORSZ>32000",
|
|
" int *po;",
|
|
"#else",
|
|
" short *po;",
|
|
"#endif",
|
|
" int *qo;",
|
|
" uchar *ps, *qs;",
|
|
" struct EV_Hold *nxt;",
|
|
"} EV_Hold;",
|
|
"",
|
|
"typedef struct BFS_Trail {",
|
|
" Trail *frame;",
|
|
" SV_Hold *onow;",
|
|
" EV_Hold *omask;",
|
|
"#ifdef Q_PROVISO",
|
|
" struct H_el *lstate;",
|
|
"#endif",
|
|
" short boq;",
|
|
" struct BFS_Trail *nxt;",
|
|
"} BFS_Trail;",
|
|
"",
|
|
"BFS_Trail *bfs_trail, *bfs_bot, *bfs_free;",
|
|
"",
|
|
"SV_Hold *svhold, *svfree;",
|
|
"",
|
|
"uchar do_reverse(Trans *, short, uchar);",
|
|
"void snapshot(void);",
|
|
"",
|
|
"SV_Hold *",
|
|
"getsv(int n)",
|
|
"{ SV_Hold *h = (SV_Hold *) 0, *oh;",
|
|
"",
|
|
" oh = (SV_Hold *) 0;",
|
|
" for (h = svfree; h; oh = h, h = h->nxt)",
|
|
" { if (n == h->sz)",
|
|
" { if (!oh)",
|
|
" svfree = h->nxt;",
|
|
" else",
|
|
" oh->nxt = h->nxt;",
|
|
" h->nxt = (SV_Hold *) 0;",
|
|
" break;",
|
|
" }",
|
|
" if (n < h->sz)",
|
|
" { h = (SV_Hold *) 0;",
|
|
" break;",
|
|
" }",
|
|
" /* else continue */",
|
|
" }",
|
|
"",
|
|
" if (!h)",
|
|
" { h = (SV_Hold *) emalloc(sizeof(SV_Hold));",
|
|
" h->sz = n;",
|
|
" h->sv = (State *) emalloc(sizeof(State) - VECTORSZ + n);",
|
|
" }",
|
|
" return h;",
|
|
"}",
|
|
"",
|
|
"EV_Hold *",
|
|
"getsv_mask(int n)",
|
|
"{ EV_Hold *h;",
|
|
" static EV_Hold *kept = (EV_Hold *) 0;",
|
|
"",
|
|
" for (h = kept; h; h = h->nxt)",
|
|
" if (n == h->sz",
|
|
" && (memcmp((char *) Mask, (char *) h->sv, n) == 0)",
|
|
" && (now._nr_pr == h->nrpr)",
|
|
" && (now._nr_qs == h->nrqs)",
|
|
"#if VECTORSZ>32000",
|
|
" && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(int)) == 0)",
|
|
" && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(int)) == 0)",
|
|
"#else",
|
|
" && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(short)) == 0)",
|
|
" && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(short)) == 0)",
|
|
"#endif",
|
|
" && (memcmp((char *) proc_skip, (char *) h->ps, now._nr_pr * sizeof(uchar)) == 0)",
|
|
" && (memcmp((char *) q_skip, (char *) h->qs, now._nr_qs * sizeof(uchar)) == 0))",
|
|
" break;",
|
|
" if (!h)",
|
|
" { h = (EV_Hold *) emalloc(sizeof(EV_Hold));",
|
|
" h->sz = n;",
|
|
" h->nrpr = now._nr_pr;",
|
|
" h->nrqs = now._nr_qs;",
|
|
"",
|
|
" h->sv = (char *) emalloc(n * sizeof(char));",
|
|
" memcpy((char *) h->sv, (char *) Mask, n);",
|
|
"",
|
|
" if (now._nr_pr > 0)",
|
|
" { h->po = (int *) emalloc(now._nr_pr * sizeof(int));",
|
|
" h->ps = (int *) emalloc(now._nr_pr * sizeof(int));",
|
|
"#if VECTORSZ>32000",
|
|
" memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(int));",
|
|
"#else",
|
|
" memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(short));",
|
|
"#endif",
|
|
" memcpy((char *) h->ps, (char *) proc_skip, now._nr_pr * sizeof(uchar));",
|
|
" }",
|
|
" if (now._nr_qs > 0)",
|
|
" { h->qo = (int *) emalloc(now._nr_qs * sizeof(int));",
|
|
" h->qs = (int *) emalloc(now._nr_qs * sizeof(int));",
|
|
"#if VECTORSZ>32000",
|
|
" memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(int));",
|
|
"#else",
|
|
" memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(short));",
|
|
"#endif",
|
|
" memcpy((char *) h->qs, (char *) q_skip, now._nr_qs * sizeof(uchar));",
|
|
" }",
|
|
"",
|
|
" h->nxt = kept;",
|
|
" kept = h;",
|
|
" }",
|
|
" return h;",
|
|
"}",
|
|
"",
|
|
"void",
|
|
"freesv(SV_Hold *p)",
|
|
"{ SV_Hold *h, *oh;",
|
|
"",
|
|
" oh = (SV_Hold *) 0;",
|
|
" for (h = svfree; h; oh = h, h = h->nxt)",
|
|
" if (h->sz >= p->sz)",
|
|
" break;",
|
|
"",
|
|
" if (!oh)",
|
|
" { p->nxt = svfree;",
|
|
" svfree = p;",
|
|
" } else",
|
|
" { p->nxt = h;",
|
|
" oh->nxt = p;",
|
|
" }",
|
|
"}",
|
|
"",
|
|
"BFS_Trail *",
|
|
"get_bfs_frame(void)",
|
|
"{ BFS_Trail *t;",
|
|
"",
|
|
" if (bfs_free)",
|
|
" { t = bfs_free;",
|
|
" bfs_free = bfs_free->nxt;",
|
|
" t->nxt = (BFS_Trail *) 0;",
|
|
" } else",
|
|
" { t = (BFS_Trail *) emalloc(sizeof(BFS_Trail));",
|
|
" }",
|
|
" t->frame = (Trail *) emalloc(sizeof(Trail));", /* always new */
|
|
" return t;",
|
|
"}",
|
|
"",
|
|
"void",
|
|
"push_bfs(Trail *f, int d)",
|
|
"{ BFS_Trail *t;",
|
|
"",
|
|
" t = get_bfs_frame();",
|
|
" memcpy((char *)t->frame, (char *)f, sizeof(Trail));",
|
|
" t->frame->o_tt = d; /* depth */",
|
|
"",
|
|
" t->boq = boq;",
|
|
" t->onow = getsv(vsize);",
|
|
" memcpy((char *)t->onow->sv, (char *)&now, vsize);",
|
|
" t->omask = getsv_mask(vsize);",
|
|
"#if defined(FULLSTACK) && defined(Q_PROVISO)",
|
|
" t->lstate = Lstate;",
|
|
"#endif",
|
|
" if (!bfs_bot)",
|
|
" { bfs_bot = bfs_trail = t;",
|
|
" } else",
|
|
" { bfs_bot->nxt = t;",
|
|
" bfs_bot = t;",
|
|
" }",
|
|
"#ifdef CHECK",
|
|
" printf(\"PUSH %%u (%%d)\\n\", t->frame, d);",
|
|
"#endif",
|
|
"}",
|
|
"",
|
|
"Trail *",
|
|
"pop_bfs(void)",
|
|
"{ BFS_Trail *t;",
|
|
"",
|
|
" if (!bfs_trail)",
|
|
" return (Trail *) 0;",
|
|
"",
|
|
" t = bfs_trail;",
|
|
" bfs_trail = t->nxt;",
|
|
" if (!bfs_trail)",
|
|
" bfs_bot = (BFS_Trail *) 0;",
|
|
"#if defined(Q_PROVISO) && !defined(BITSTATE) && !defined(NOREDUCE)",
|
|
" if (t->lstate) t->lstate->tagged = 0;",
|
|
"#endif",
|
|
"",
|
|
" t->nxt = bfs_free;",
|
|
" bfs_free = t;",
|
|
"",
|
|
" vsize = t->onow->sz;",
|
|
" boq = t->boq;",
|
|
"",
|
|
" memcpy((uchar *) &now, (uchar *) t->onow->sv, vsize);",
|
|
" memcpy((uchar *) Mask, (uchar *) t->omask->sv, vsize);",
|
|
|
|
" if (now._nr_pr > 0)",
|
|
"#if VECTORSZ>32000",
|
|
" { memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(int));",
|
|
"#else",
|
|
" { memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(short));",
|
|
"#endif",
|
|
" memcpy((char *)proc_skip, (char *)t->omask->ps, now._nr_pr * sizeof(uchar));",
|
|
" }",
|
|
" if (now._nr_qs > 0)",
|
|
"#if VECTORSZ>32000",
|
|
" { memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(int));",
|
|
"#else",
|
|
" { memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(short));",
|
|
"#endif",
|
|
" memcpy((uchar *)q_skip, (uchar *)t->omask->qs, now._nr_qs * sizeof(uchar));",
|
|
" }",
|
|
|
|
" freesv(t->onow); /* omask not freed */",
|
|
"#ifdef CHECK",
|
|
" printf(\"POP %%u (%%d)\\n\", t->frame, t->frame->o_tt);",
|
|
"#endif",
|
|
" return t->frame;",
|
|
"}",
|
|
"",
|
|
"void",
|
|
"store_state(Trail *ntrpt, int shortcut, short oboq)",
|
|
"{",
|
|
"#ifdef VERI",
|
|
" Trans *t2 = (Trans *) 0;",
|
|
" uchar ot; int tt, E_state;",
|
|
" uchar o_opm = trpt->o_pm, *othis = this;",
|
|
"",
|
|
" if (shortcut)",
|
|
" {",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"claim: shortcut\\n\");",
|
|
"#endif",
|
|
" goto store_it; /* no claim move */",
|
|
" }",
|
|
"",
|
|
" this = (((uchar *)&now)+proc_offset[0]); /* 0 = never claim */",
|
|
" trpt->o_pm = 0;", /* to interpret else in never claim */
|
|
"",
|
|
" tt = (int) ((P0 *)this)->_p;",
|
|
" ot = (uchar) ((P0 *)this)->_t;",
|
|
"",
|
|
"#ifdef HAS_UNLESS",
|
|
" E_state = 0;",
|
|
"#endif",
|
|
" for (t2 = trans[ot][tt]; t2; t2 = t2?t2->nxt:(Trans *)0)",
|
|
" {",
|
|
"#ifdef HAS_UNLESS",
|
|
" if (E_state > 0",
|
|
" && E_state != t2->e_trans)",
|
|
" break;",
|
|
"#endif",
|
|
" if (do_transit(t2, 0))",
|
|
" {",
|
|
"#ifdef VERBOSE",
|
|
" if (!reached[ot][t2->st])",
|
|
" printf(\"depth: %%d -- claim move from %%d -> %%d\\n\",",
|
|
" trpt->o_tt, ((P0 *)this)->_p, t2->st);",
|
|
"#endif",
|
|
"#ifdef HAS_UNLESS",
|
|
" E_state = t2->e_trans;",
|
|
"#endif",
|
|
" if (t2->st > 0)",
|
|
" { ((P0 *)this)->_p = t2->st;",
|
|
" reached[ot][t2->st] = 1;",
|
|
"#ifndef NOCLAIM",
|
|
" check_claim(t2->st);",
|
|
"#endif",
|
|
" }",
|
|
" if (now._nr_pr == 0) /* claim terminated */",
|
|
" uerror(\"end state in claim reached\");",
|
|
"",
|
|
"#ifdef PEG",
|
|
" peg[t2->forw]++;",
|
|
"#endif",
|
|
" trpt->o_pm |= 1;",
|
|
" if (t2->atom&2)", /* atomic in claim */
|
|
" Uerror(\"atomic in claim not supported in BFS mode\");",
|
|
"store_it:",
|
|
"",
|
|
"#endif", /* VERI */
|
|
"",
|
|
"#ifdef BITSTATE",
|
|
" if (!bstore((char *)&now, vsize))",
|
|
"#else",
|
|
"#ifdef MA",
|
|
" if (!gstore((char *)&now, vsize, 0))",
|
|
"#else",
|
|
" if (!hstore((char *)&now, vsize))",
|
|
"#endif",
|
|
"#endif",
|
|
" { nstates++;",
|
|
"#ifndef NOREDUCE",
|
|
" trpt->tau |= 64;", /* succ definitely outside stack */
|
|
"#endif",
|
|
"#if SYNC",
|
|
" if (boq != -1)",
|
|
" midrv++;",
|
|
" else if (oboq != -1)",
|
|
" { Trail *x;",
|
|
" x = (Trail *) trpt->ostate; /* pre-rv state */",
|
|
" if (x) x->o_pm |= 4; /* mark success */",
|
|
" }",
|
|
"#endif",
|
|
" push_bfs(ntrpt, trpt->o_tt+1);",
|
|
" } else",
|
|
" { truncs++;",
|
|
|
|
"#if !defined(NOREDUCE) && defined(FULLSTACK) && defined(Q_PROVISO)",
|
|
"#if !defined(QLIST) && !defined(BITSTATE)",
|
|
" if (Lstate && Lstate->tagged) trpt->tau |= 64;",
|
|
"#else",
|
|
" if (trpt->tau&32)",
|
|
" { BFS_Trail *tprov;",
|
|
" for (tprov = bfs_trail; tprov; tprov = tprov->nxt)",
|
|
" if (!memcmp((uchar *)&now, (uchar *)tprov->onow->sv, vsize))",
|
|
" { trpt->tau |= 64;",
|
|
" break; /* state is in queue */",
|
|
" } }",
|
|
"#endif",
|
|
"#endif",
|
|
" }",
|
|
"#ifdef VERI",
|
|
" ((P0 *)this)->_p = tt; /* reset claim */",
|
|
" if (t2)",
|
|
" do_reverse(t2, 0, 0);",
|
|
" else",
|
|
" break;",
|
|
" } }",
|
|
" this = othis;",
|
|
" trpt->o_pm = o_opm;",
|
|
"#endif",
|
|
"}",
|
|
"",
|
|
"Trail *ntrpt;", /* 4.2.8 */
|
|
"",
|
|
"void",
|
|
"bfs(void)",
|
|
"{ Trans *t; Trail *otrpt, *x;",
|
|
" uchar _n, _m, ot, nps = 0;",
|
|
" int tt, E_state;",
|
|
" short II, From = (short) (now._nr_pr-1), To = BASE;",
|
|
" short oboq = boq;",
|
|
"",
|
|
" ntrpt = (Trail *) emalloc(sizeof(Trail));",
|
|
" trpt->ostate = (struct H_el *) 0;",
|
|
" trpt->tau = 0;",
|
|
"",
|
|
" trpt->o_tt = -1;",
|
|
" store_state(ntrpt, 0, oboq); /* initial state */",
|
|
"",
|
|
" while ((otrpt = pop_bfs())) /* also restores now */",
|
|
" { memcpy((char *) trpt, (char *) otrpt, sizeof(Trail));",
|
|
"#if defined(C_States) && (HAS_TRACK==1)",
|
|
" c_revert((uchar *) &(now.c_state[0]));",
|
|
"#endif",
|
|
" if (trpt->o_pm & 4)",
|
|
" {",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"Revisit of atomic not needed (%%d)\\n\",",
|
|
" trpt->o_pm);", /* at least 1 rv succeeded */
|
|
"#endif",
|
|
" continue;",
|
|
" }",
|
|
"#ifndef NOREDUCE",
|
|
" nps = 0;",
|
|
"#endif",
|
|
" if (trpt->o_pm == 8)",
|
|
" { revrv++;",
|
|
" if (trpt->tau&8)",
|
|
" {",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"Break atomic (pm:%%d,tau:%%d)\\n\",",
|
|
" trpt->o_pm, trpt->tau);",
|
|
"#endif",
|
|
" trpt->tau &= ~8;",
|
|
" }",
|
|
"#ifndef NOREDUCE",
|
|
" else if (trpt->tau&32)", /* was a preselected move */
|
|
" {",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"Void preselection (pm:%%d,tau:%%d)\\n\",",
|
|
" trpt->o_pm, trpt->tau);",
|
|
"#endif",
|
|
" trpt->tau &= ~32;",
|
|
" nps = 1; /* no preselection in repeat */",
|
|
" }",
|
|
"#endif",
|
|
" }",
|
|
" trpt->o_pm &= ~(4|8);",
|
|
" if (trpt->o_tt > mreached)",
|
|
" { mreached = trpt->o_tt;",
|
|
" if (mreached%%10 == 0)",
|
|
" { printf(\"Depth= %%7d States= %%7g \", mreached, nstates);",
|
|
" printf(\"Transitions= %%7g \", nstates+truncs);",
|
|
"#ifdef MA",
|
|
" printf(\"Nodes= %%7d \", nr_states);",
|
|
"#endif",
|
|
" printf(\"Memory= %%-6.3f\\n\", memcnt/1000000.);",
|
|
" fflush(stdout);",
|
|
" } }",
|
|
" depth = trpt->o_tt;",
|
|
|
|
" if (depth >= maxdepth)",
|
|
" {",
|
|
"#if SYNC",
|
|
" Trail *x;",
|
|
" if (boq != -1)",
|
|
" { x = (Trail *) trpt->ostate;",
|
|
" if (x) x->o_pm |= 4; /* not failing */",
|
|
" }",
|
|
"#endif",
|
|
" truncs++;",
|
|
" if (!warned)",
|
|
" { warned = 1;",
|
|
" printf(\"error: max search depth too small\\n\");",
|
|
" }",
|
|
" if (bounded)",
|
|
" uerror(\"depth limit reached\");",
|
|
" continue;",
|
|
" }",
|
|
|
|
/* PO */
|
|
"#ifndef NOREDUCE",
|
|
" if (boq == -1 && !(trpt->tau&8) && nps == 0)",
|
|
" for (II = now._nr_pr-1; II >= BASE; II -= 1)",
|
|
" {",
|
|
"Pickup: this = pptr(II);",
|
|
" tt = (int) ((P0 *)this)->_p;",
|
|
" ot = (uchar) ((P0 *)this)->_t;",
|
|
" if (trans[ot][tt]->atom & 8)", /* safe */
|
|
" { t = trans[ot][tt];",
|
|
" if (t->qu[0] != 0)",
|
|
" { Ccheck++;",
|
|
" if (!q_cond(II, t))",
|
|
" continue;",
|
|
" Cholds++;",
|
|
" }",
|
|
" From = To = II;",
|
|
" trpt->tau |= 32; /* preselect marker */",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%3d: proc %%d PreSelected (tau=%%d)\\n\", ",
|
|
" depth, II, trpt->tau);",
|
|
"#endif",
|
|
" goto MainLoop;",
|
|
" } }",
|
|
" trpt->tau &= ~32;", /* not preselected */
|
|
"#endif",
|
|
/* PO */
|
|
"Repeat:",
|
|
" if (trpt->tau&8) /* atomic */",
|
|
" { From = To = (short ) trpt->pr;",
|
|
" nlinks++;",
|
|
" } else",
|
|
" { From = now._nr_pr-1;",
|
|
" To = BASE;",
|
|
" }",
|
|
"MainLoop:",
|
|
" _n = _m = 0;",
|
|
" for (II = From; II >= To; II -= 1)",
|
|
" {",
|
|
" this = (((uchar *)&now)+proc_offset[II]);",
|
|
" tt = (int) ((P0 *)this)->_p;",
|
|
" ot = (uchar) ((P0 *)this)->_t;",
|
|
"#if SYNC",
|
|
" /* no rendezvous with same proc */",
|
|
" if (boq != -1 && trpt->pr == II) continue;",
|
|
"#endif",
|
|
" ntrpt->pr = (uchar) II;",
|
|
" ntrpt->st = tt; ",
|
|
" trpt->o_pm &= ~1; /* no move yet */",
|
|
"#ifdef EVENT_TRACE",
|
|
" trpt->o_event = now._event;",
|
|
"#endif",
|
|
"#ifdef HAS_PROVIDED",
|
|
" if (!provided(II, ot, tt, t)) continue;",
|
|
"#endif",
|
|
"#ifdef HAS_UNLESS",
|
|
" E_state = 0;",
|
|
"#endif",
|
|
" for (t = trans[ot][tt]; t; t = t->nxt)",
|
|
" {",
|
|
"#ifdef HAS_UNLESS",
|
|
" if (E_state > 0",
|
|
" && E_state != t->e_trans)",
|
|
" break;",
|
|
"#endif",
|
|
" ntrpt->o_t = t;",
|
|
"",
|
|
" oboq = boq;",
|
|
"",
|
|
" if (!(_m = do_transit(t, II)))",
|
|
" continue;",
|
|
"",
|
|
" trpt->o_pm |= 1; /* we moved */",
|
|
" (trpt+1)->o_m = _m; /* for unsend */",
|
|
"#ifdef PEG",
|
|
" peg[t->forw]++;",
|
|
"#endif",
|
|
"#ifdef CHECK",
|
|
" printf(\"%%3d: proc %%d exec %%d, \",",
|
|
" depth, II, t->forw);",
|
|
" printf(\"%%d to %%d, %%s %%s %%s\",",
|
|
" tt, t->st, t->tp,",
|
|
" (t->atom&2)?\"atomic\":\"\",",
|
|
" (boq != -1)?\"rendez-vous\":\"\");",
|
|
"#ifdef HAS_UNLESS",
|
|
" if (t->e_trans)",
|
|
" printf(\" (escapes to state %%d)\", t->st);",
|
|
"#endif",
|
|
" printf(\" %%saccepting [tau=%%d]\\n\",",
|
|
" (trpt->o_pm&2)?\"\":\"non-\", trpt->tau);",
|
|
"#endif",
|
|
"#ifdef HAS_UNLESS",
|
|
" E_state = t->e_trans;",
|
|
"#if SYNC>0",
|
|
" if (t->e_trans > 0 && (boq != -1 /* || oboq != -1 */))",
|
|
" { fprintf(efd, \"error:\tthe use of rendezvous stmnt in the escape clause\\n\");",
|
|
" fprintf(efd, \"\tof an unless stmnt is not compatible with -DBFS\\n\");",
|
|
" pan_exit(1);",
|
|
" }",
|
|
"#endif",
|
|
"#endif",
|
|
" if (t->st > 0) ((P0 *)this)->_p = t->st;",
|
|
"",
|
|
" /* ptr to pred: */ ntrpt->ostate = (struct H_el *) otrpt;",
|
|
" ntrpt->st = tt;",
|
|
" if (boq == -1 && (t->atom&2)) /* atomic */",
|
|
" ntrpt->tau = 8; /* record for next move */",
|
|
" else",
|
|
" ntrpt->tau = 0;",
|
|
"",
|
|
" store_state(ntrpt, (boq != -1 || (t->atom&2)), oboq);",
|
|
"#ifdef EVENT_TRACE",
|
|
" now._event = trpt->o_event;",
|
|
"#endif",
|
|
"",
|
|
" /* undo move and continue */",
|
|
" trpt++; /* this is where ovals and ipt are set */",
|
|
" do_reverse(t, II, _m); /* restore now. */",
|
|
" trpt--;",
|
|
"#ifdef CHECK",
|
|
" printf(\"%%3d: proc %%d \", depth, II);",
|
|
" printf(\"reverses %%d, %%d to %%d,\",",
|
|
" t->forw, tt, t->st);",
|
|
" printf(\" %%s [abit=%%d,adepth=%%d,\",",
|
|
" t->tp, now._a_t, A_depth);",
|
|
" printf(\"tau=%%d,%%d]\\n\",",
|
|
" trpt->tau, (trpt-1)->tau);",
|
|
"#endif",
|
|
" reached[ot][t->st] = 1;",
|
|
" reached[ot][tt] = 1;",
|
|
"",
|
|
" ((P0 *)this)->_p = tt;",
|
|
" _n |= _m;",
|
|
" } }",
|
|
/* PO */
|
|
"#ifndef NOREDUCE",
|
|
" /* preselected - no succ definitely outside stack */",
|
|
" if ((trpt->tau&32) && !(trpt->tau&64))",
|
|
" { From = now._nr_pr-1; To = BASE;",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%3d: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
|
|
" depth, II+1, (int) _n, trpt->tau);",
|
|
"#endif",
|
|
" _n = 0; trpt->tau &= ~32;",
|
|
" if (II >= BASE)",
|
|
" goto Pickup;",
|
|
" goto MainLoop;",
|
|
" }",
|
|
" trpt->tau &= ~(32|64);",
|
|
"#endif",
|
|
/* PO */
|
|
" if (_n != 0)",
|
|
" continue;",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%3d: no move [II=%%d, tau=%%d, boq=%%d, _nr_pr=%%d]\\n\",",
|
|
" depth, II, trpt->tau, boq, now._nr_pr);",
|
|
"#endif",
|
|
" if (boq != -1)",
|
|
" { failedrv++;",
|
|
" x = (Trail *) trpt->ostate; /* pre-rv state */",
|
|
" if (!x) continue; /* root state */",
|
|
" if ((x->tau&8) || (x->tau&32)) /* break atomic or preselect at parent */",
|
|
" { x->o_pm |= 8; /* mark failure */",
|
|
" this = (((uchar *)&now)+proc_offset[otrpt->pr]);",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"\\treset state of %%d from %%d to %%d\\n\",",
|
|
" otrpt->pr, ((P0 *)this)->_p, otrpt->st);",
|
|
"#endif",
|
|
" ((P0 *)this)->_p = otrpt->st;",
|
|
" unsend(boq); /* retract rv offer */",
|
|
" boq = -1;",
|
|
|
|
" push_bfs(x, x->o_tt);",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"failed rv, repush with %%d\\n\", x->o_pm);",
|
|
"#endif",
|
|
" }",
|
|
"#ifdef VERBOSE",
|
|
" else printf(\"failed rv, tau at parent: %%d\\n\", x->tau);",
|
|
"#endif",
|
|
" } else if (now._nr_pr > 0)",
|
|
" {",
|
|
" if ((trpt->tau&8)) /* atomic */",
|
|
" { trpt->tau &= ~(1|8); /* 1=timeout, 8=atomic */",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%3d: atomic step proc %%d blocks\\n\",",
|
|
" depth, II+1);",
|
|
"#endif",
|
|
" goto Repeat;",
|
|
" }",
|
|
"",
|
|
" if (!(trpt->tau&1)) /* didn't try timeout yet */",
|
|
" { trpt->tau |= 1;",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%d: timeout\\n\", depth);",
|
|
"#endif",
|
|
" goto MainLoop;",
|
|
" }",
|
|
"#ifndef VERI",
|
|
" if (!noends && !a_cycles && !endstate())",
|
|
" uerror(\"invalid end state\");",
|
|
"#endif",
|
|
" } }",
|
|
"}",
|
|
"",
|
|
"void",
|
|
"putter(Trail *trpt, int fd)",
|
|
"{ long j;",
|
|
"",
|
|
" if (!trpt) return;",
|
|
"",
|
|
" if (trpt != (Trail *) trpt->ostate)",
|
|
" putter((Trail *) trpt->ostate, fd);",
|
|
"",
|
|
" if (trpt->o_t)",
|
|
" { sprintf(snap, \"%%d:%%d:%%d\\n\",",
|
|
" trcnt++, trpt->pr, trpt->o_t->t_id);",
|
|
" j = strlen(snap);",
|
|
" if (write(fd, snap, j) != j)",
|
|
" { printf(\"pan: error writing %%s\\n\", fnm);",
|
|
" pan_exit(1);",
|
|
" } }",
|
|
"}",
|
|
"",
|
|
"void",
|
|
"nuerror(char *str)",
|
|
"{ int fd = make_trail();",
|
|
" int j;",
|
|
"",
|
|
" if (fd < 0) return;",
|
|
"#ifdef VERI",
|
|
" sprintf(snap, \"-2:%%d:-2\\n\", VERI);",
|
|
" write(fd, snap, strlen(snap));",
|
|
"#endif",
|
|
"#ifdef MERGED",
|
|
" sprintf(snap, \"-4:-4:-4\\n\");",
|
|
" write(fd, snap, strlen(snap));",
|
|
"#endif",
|
|
" trcnt = 1;",
|
|
" putter(trpt, fd);",
|
|
" if (ntrpt->o_t)", /* 4.2.8 -- Alex example, missing last transition */
|
|
" { sprintf(snap, \"%%d:%%d:%%d\\n\",",
|
|
" trcnt++, ntrpt->pr, ntrpt->o_t->t_id);",
|
|
" j = strlen(snap);",
|
|
" if (write(fd, snap, j) != j)",
|
|
" { printf(\"pan: error writing %%s\\n\", fnm);",
|
|
" pan_exit(1);",
|
|
" } }",
|
|
" close(fd);",
|
|
" if (errors >= upto && upto != 0)",
|
|
" {",
|
|
" wrapup();",
|
|
" }",
|
|
"}",
|
|
"#endif", /* BFS */
|
|
0,
|
|
};
|
|
|
|
static char *Code2c[] = {
|
|
"void",
|
|
"do_the_search(void)",
|
|
"{ int i;",
|
|
" depth = mreached = 0;",
|
|
" trpt = &trail[0];",
|
|
"#ifdef VERI",
|
|
" trpt->tau |= 4; /* the claim moves first */",
|
|
"#endif",
|
|
" for (i = 0; i < (int) now._nr_pr; i++)",
|
|
" { P0 *ptr = (P0 *) pptr(i);",
|
|
"#ifndef NP",
|
|
" if (!(trpt->o_pm&2)",
|
|
" && accpstate[ptr->_t][ptr->_p])",
|
|
" { trpt->o_pm |= 2;",
|
|
" }",
|
|
"#else",
|
|
" if (!(trpt->o_pm&4)",
|
|
" && progstate[ptr->_t][ptr->_p])",
|
|
" { trpt->o_pm |= 4;",
|
|
" }",
|
|
"#endif",
|
|
" }",
|
|
"#ifdef EVENT_TRACE",
|
|
"#ifndef NP",
|
|
" if (accpstate[EVENT_TRACE][now._event])",
|
|
" { trpt->o_pm |= 2;",
|
|
" }",
|
|
"#else",
|
|
" if (progstate[EVENT_TRACE][now._event])",
|
|
" { trpt->o_pm |= 4;",
|
|
" }",
|
|
"#endif",
|
|
"#endif",
|
|
"#ifndef NOCOMP",
|
|
" Mask[0] = Mask[1] = 1; /* _nr_pr, _nr_qs */",
|
|
" if (!a_cycles)",
|
|
" { i = &(now._a_t) - (uchar *) &now;",
|
|
" Mask[i] = 1; /* _a_t */",
|
|
" }",
|
|
"#ifndef NOFAIR",
|
|
" if (!fairness)",
|
|
" { int j = 0;",
|
|
" i = &(now._cnt[0]) - (uchar *) &now;",
|
|
" while (j++ < NFAIR)",
|
|
" Mask[i++] = 1; /* _cnt[] */",
|
|
" }",
|
|
"#endif",
|
|
"#endif",
|
|
"#ifndef NOFAIR",
|
|
" if (fairness",
|
|
" && (a_cycles && (trpt->o_pm&2)))",
|
|
" { now._a_t = 2; /* set the A-bit */",
|
|
" now._cnt[0] = now._nr_pr + 1;", /* NEW: +1 */
|
|
"#ifdef VERBOSE",
|
|
" printf(\"%%3d: fairness Rule 1, cnt=%%d, _a_t=%%d\\n\",",
|
|
" depth, now._cnt[now._a_t&1], now._a_t);",
|
|
"#endif",
|
|
" }",
|
|
"#endif",
|
|
|
|
"#if defined(C_States) && (HAS_TRACK==1)",
|
|
" /* capture initial state of tracked C objects */",
|
|
" c_update((uchar *) &(now.c_state[0]));",
|
|
"#endif",
|
|
|
|
"#ifdef HAS_CODE",
|
|
" if (readtrail) getrail(); /* no return */",
|
|
"#endif",
|
|
"#ifdef BFS",
|
|
" bfs();",
|
|
"#else",
|
|
"#if defined(C_States) && defined(HAS_STACK) && (HAS_TRACK==1)",
|
|
" /* initial state of tracked & unmatched objects */",
|
|
" c_stack((uchar *) &(svtack->c_stack[0]));",
|
|
"#endif",
|
|
"#ifdef RANDOMIZE",
|
|
" srand(123);",
|
|
"#endif",
|
|
" new_state(); /* start 1st DFS */",
|
|
"#endif",
|
|
"}",
|
|
|
|
"#ifdef INLINE_REV",
|
|
"uchar",
|
|
"do_reverse(Trans *t, short II, uchar M)",
|
|
"{ uchar _m = M;",
|
|
" int tt = (int) ((P0 *)this)->_p;",
|
|
"#include REVERSE_MOVES",
|
|
"R999: return _m;",
|
|
"}",
|
|
"#endif",
|
|
|
|
"#ifndef INLINE",
|
|
"#ifdef EVENT_TRACE",
|
|
"static char _tp = 'n'; static int _qid = 0;",
|
|
"#endif",
|
|
"uchar",
|
|
"do_transit(Trans *t, short II)",
|
|
"{ uchar _m = 0;",
|
|
" int tt = (int) ((P0 *)this)->_p;",
|
|
"#ifdef M_LOSS",
|
|
" uchar delta_m = 0;",
|
|
"#endif",
|
|
"#ifdef EVENT_TRACE",
|
|
" short oboq = boq;",
|
|
" uchar ot = (uchar) ((P0 *)this)->_t;",
|
|
" if (ot == EVENT_TRACE) boq = -1;",
|
|
"#define continue { boq = oboq; return 0; }",
|
|
"#else",
|
|
"#define continue return 0",
|
|
"#ifdef SEPARATE",
|
|
" uchar ot = (uchar) ((P0 *)this)->_t;",
|
|
"#endif",
|
|
"#endif",
|
|
"#include FORWARD_MOVES",
|
|
"P999:",
|
|
"#ifdef EVENT_TRACE",
|
|
" if (ot == EVENT_TRACE) boq = oboq;",
|
|
"#endif",
|
|
" return _m;",
|
|
"#undef continue",
|
|
"}",
|
|
|
|
"#ifdef EVENT_TRACE",
|
|
"void",
|
|
"require(char tp, int qid)",
|
|
"{ Trans *t;",
|
|
" _tp = tp; _qid = qid;",
|
|
"",
|
|
" if (now._event != endevent)",
|
|
" for (t = trans[EVENT_TRACE][now._event]; t; t = t->nxt)",
|
|
" { if (do_transit(t, EVENT_TRACE))",
|
|
" { now._event = t->st;",
|
|
" reached[EVENT_TRACE][t->st] = 1;",
|
|
"#ifdef VERBOSE",
|
|
" printf(\" event_trace move to -> %%d\\n\", t->st);",
|
|
"#endif",
|
|
"#ifndef BFS",
|
|
"#ifndef NP",
|
|
" if (accpstate[EVENT_TRACE][now._event])",
|
|
" (trpt+1)->o_pm |= 2;",
|
|
"#else",
|
|
" if (progstate[EVENT_TRACE][now._event])",
|
|
" (trpt+1)->o_pm |= 4;",
|
|
"#endif",
|
|
"#endif",
|
|
"#ifdef NEGATED_TRACE",
|
|
" if (now._event == endevent)",
|
|
" {",
|
|
"#ifndef BFS",
|
|
" depth++; trpt++;",
|
|
"#endif",
|
|
" uerror(\"event_trace error (all events matched)\");",
|
|
"#ifndef BFS",
|
|
" trpt--; depth--;",
|
|
"#endif",
|
|
" break;",
|
|
" }",
|
|
"#endif",
|
|
" for (t = t->nxt; t; t = t->nxt)",
|
|
" { if (do_transit(t, EVENT_TRACE))",
|
|
" Uerror(\"non-determinism in event-trace\");",
|
|
" }",
|
|
" return;",
|
|
" }",
|
|
"#ifdef VERBOSE",
|
|
" else",
|
|
" printf(\" event_trace miss '%%c' -- %%d, %%d, %%d\\n\",",
|
|
" tp, qid, now._event, t->forw);",
|
|
"#endif",
|
|
" }",
|
|
"#ifdef NEGATED_TRACE",
|
|
" now._event = endevent; /* only 1st try will count -- fixed 4.2.6 */",
|
|
"#else",
|
|
"#ifndef BFS",
|
|
" depth++; trpt++;",
|
|
"#endif",
|
|
" uerror(\"event_trace error (no matching event)\");",
|
|
"#ifndef BFS",
|
|
" trpt--; depth--;",
|
|
"#endif",
|
|
"#endif",
|
|
"}",
|
|
"#endif",
|
|
|
|
"int",
|
|
"enabled(int iam, int pid)",
|
|
"{ Trans *t; uchar *othis = this;",
|
|
" int res = 0; int tt; uchar ot;",
|
|
"#ifdef VERI",
|
|
" /* if (pid > 0) */ pid++;",
|
|
"#endif",
|
|
" if (pid == iam)",
|
|
" Uerror(\"used: enabled(pid=thisproc)\");",
|
|
" if (pid < 0 || pid >= (int) now._nr_pr)",
|
|
" return 0;",
|
|
" this = pptr(pid);",
|
|
" TstOnly = 1;",
|
|
" tt = (int) ((P0 *)this)->_p;",
|
|
" ot = (uchar) ((P0 *)this)->_t;",
|
|
" for (t = trans[ot][tt]; t; t = t->nxt)",
|
|
" if (do_transit(t, (short) pid))",
|
|
" { res = 1;",
|
|
" break;",
|
|
" }",
|
|
" TstOnly = 0;",
|
|
" this = othis;",
|
|
" return res;",
|
|
"}",
|
|
"#endif",
|
|
"void",
|
|
"snapshot(void)",
|
|
"{ static long sdone = (long) 0;",
|
|
" long ndone = (unsigned long) nstates/1000000;",
|
|
" if (ndone == sdone) return;",
|
|
" sdone = ndone;",
|
|
" printf(\"Depth= %%7d States= %%7g \", mreached, nstates);",
|
|
" printf(\"Transitions= %%7g \", nstates+truncs);",
|
|
"#ifdef MA",
|
|
" printf(\"Nodes= %%7d \", nr_states);",
|
|
"#endif",
|
|
" printf(\"Memory= %%-6.3f\\n\", memcnt/1000000.);",
|
|
" fflush(stdout);",
|
|
"}",
|
|
|
|
"#ifdef SC",
|
|
"void",
|
|
"stack2disk(void)",
|
|
"{",
|
|
" if (!stackwrite",
|
|
" && (stackwrite = creat(stackfile, TMODE)) < 0)",
|
|
" Uerror(\"cannot create stackfile\");",
|
|
"",
|
|
" if (write(stackwrite, trail, DDD*sizeof(Trail))",
|
|
" != DDD*sizeof(Trail))",
|
|
" Uerror(\"stackfile write error -- disk is full?\");",
|
|
"",
|
|
" memmove(trail, &trail[DDD], (HHH-DDD+2)*sizeof(Trail));",
|
|
" memset(&trail[HHH-DDD+2], 0, (omaxdepth - HHH + DDD - 2)*sizeof(Trail));",
|
|
" CNT1++;",
|
|
"}",
|
|
"void",
|
|
"disk2stack(void)",
|
|
"{ long have;",
|
|
"",
|
|
" CNT2++;",
|
|
" memmove(&trail[DDD], trail, (HHH-DDD+2)*sizeof(Trail));",
|
|
"",
|
|
" if (!stackwrite",
|
|
" || lseek(stackwrite, -DDD* (off_t) sizeof(Trail), SEEK_CUR) == -1)",
|
|
" Uerror(\"disk2stack lseek error\");",
|
|
"",
|
|
" if (!stackread",
|
|
" && (stackread = open(stackfile, 0)) < 0)",
|
|
" Uerror(\"cannot open stackfile\");",
|
|
"",
|
|
" if (lseek(stackread, (CNT1-CNT2)*DDD* (off_t) sizeof(Trail), SEEK_SET) == -1)",
|
|
" Uerror(\"disk2stack lseek error\");",
|
|
"",
|
|
" have = read(stackread, trail, DDD*sizeof(Trail));",
|
|
" if (have != DDD*sizeof(Trail))",
|
|
" Uerror(\"stackfile read error\");",
|
|
"}",
|
|
"#endif",
|
|
|
|
"uchar *",
|
|
"Pptr(int x)", /* as a fct, to avoid a problem with the p9 compiler */
|
|
"{ if (x < 0 || x >= MAXPROC || !proc_offset[x])", /* does not exist */
|
|
" return noptr;",
|
|
" else",
|
|
" return (uchar *) pptr(x);",
|
|
"}",
|
|
"int qs_empty(void);",
|
|
|
|
"/*",
|
|
" * new_state() is the main DFS search routine in the verifier",
|
|
" * it has a lot of code ifdef-ed together to support",
|
|
" * different search modes, which makes it quite unreadable.",
|
|
" * if you are studying the code, first use the C preprocessor",
|
|
" * to generate a specific version from the pan.c source,",
|
|
" * e.g. by saying:",
|
|
" * gcc -E -DNOREDUCE -DBITSTATE pan.c > ppan.c",
|
|
" * and then study the resulting file, rather than this one",
|
|
" */",
|
|
"#if !defined(BFS) && (!defined(BITSTATE) || !defined(MA))",
|
|
"void",
|
|
"new_state(void)",
|
|
"{ Trans *t;",
|
|
" uchar _n, _m, ot;",
|
|
"#ifdef RANDOMIZE",
|
|
" short ooi, eoi;",
|
|
"#endif",
|
|
"#ifdef M_LOSS",
|
|
" uchar delta_m = 0;",
|
|
"#endif",
|
|
" short II, JJ = 0, kk;",
|
|
" int tt;",
|
|
" short From = now._nr_pr-1, To = BASE;",
|
|
"Down:",
|
|
"#ifdef CHECK",
|
|
" printf(\"%%d: Down - %%s\",",
|
|
" depth, (trpt->tau&4)?\"claim\":\"program\");",
|
|
" printf(\" %%saccepting [pids %%d-%%d]\\n\",",
|
|
" (trpt->o_pm&2)?\"\":\"non-\", From, To);",
|
|
"#endif",
|
|
|
|
"#ifdef SC",
|
|
" if (depth > hiwater)",
|
|
" { stack2disk();",
|
|
" maxdepth += DDD;",
|
|
" hiwater += DDD;",
|
|
" trpt -= DDD;",
|
|
" if(verbose)",
|
|
" printf(\"zap %%d: %%d (maxdepth now %%d)\\n\",",
|
|
" CNT1, hiwater, maxdepth);",
|
|
" }",
|
|
"#endif",
|
|
|
|
" trpt->tau &= ~(16|32|64); /* make sure these are off */",
|
|
"#if defined(FULLSTACK) && defined(MA)",
|
|
" trpt->proviso = 0;",
|
|
"#endif",
|
|
" if (depth >= maxdepth)",
|
|
" { truncs++;",
|
|
"#if SYNC",
|
|
" (trpt+1)->o_n = 1; /* not a deadlock */",
|
|
"#endif",
|
|
" if (!warned)",
|
|
" { warned = 1;",
|
|
" printf(\"error: max search depth too small\\n\");",
|
|
" }",
|
|
" if (bounded) uerror(\"depth limit reached\");",
|
|
" (trpt-1)->tau |= 16; /* worstcase guess */",
|
|
" goto Up;",
|
|
" }",
|
|
"AllOver:",
|
|
"#if defined(FULLSTACK) && !defined(MA)",
|
|
" /* if atomic or rv move, carry forward previous state */",
|
|
" trpt->ostate = (trpt-1)->ostate;", /* was: = (struct H_el *) 0;*/
|
|
"#endif",
|
|
"#ifdef VERI",
|
|
" if ((trpt->tau&4) || ((trpt-1)->tau&128))",
|
|
"#endif",
|
|
" if (boq == -1) { /* if not mid-rv */",
|
|
"#ifndef SAFETY",
|
|
" /* this check should now be redundant",
|
|
" * because the seed state also appears",
|
|
" * on the 1st dfs stack and would be",
|
|
" * matched in hstore below",
|
|
" */",
|
|
" if ((now._a_t&1) && depth > A_depth)",
|
|
" { if (!memcmp((char *)&A_Root, ",
|
|
" (char *)&now, vsize))",
|
|
" {",
|
|
" depthfound = A_depth;",
|
|
"#ifdef CHECK",
|
|
" printf(\"matches seed\\n\");",
|
|
"#endif",
|
|
"#ifdef NP",
|
|
" uerror(\"non-progress cycle\");",
|
|
"#else",
|
|
" uerror(\"acceptance cycle\");",
|
|
"#endif",
|
|
" goto Up;",
|
|
" }",
|
|
"#ifdef CHECK",
|
|
" printf(\"not seed\\n\");",
|
|
"#endif",
|
|
" }",
|
|
"#endif",
|
|
" if (!(trpt->tau&8)) /* if no atomic move */",
|
|
" {",
|
|
"#ifdef BITSTATE",
|
|
"#ifdef CNTRSTACK", /* -> bitstate, reduced, safety */
|
|
" II = bstore((char *)&now, vsize);",
|
|
" trpt->j6 = j1; trpt->j7 = j2;",
|
|
" JJ = LL[j1] && LL[j2];",
|
|
"#else",
|
|
"#ifdef FULLSTACK",
|
|
" JJ = onstack_now();", /* sets j1 */
|
|
"#else",
|
|
"#ifndef NOREDUCE",
|
|
" JJ = II; /* worstcase guess for p.o. */",
|
|
"#endif",
|
|
"#endif",
|
|
" II = bstore((char *)&now, vsize);", /* sets j1-j4 */
|
|
"#endif",
|
|
"#else",
|
|
"#ifdef MA",
|
|
" II = gstore((char *)&now, vsize, 0);",
|
|
"#ifndef FULLSTACK",
|
|
" JJ = II;",
|
|
"#else",
|
|
" JJ = (II == 2)?1:0;",
|
|
"#endif",
|
|
"#else",
|
|
" II = hstore((char *)&now, vsize);",
|
|
"#ifdef FULLSTACK",
|
|
" JJ = (II == 2)?1:0;",
|
|
"#endif",
|
|
"#endif",
|
|
"#endif",
|
|
" kk = (II == 1 || II == 2);",
|
|
/* II==0 new state */
|
|
/* II==1 old state */
|
|
/* II==2 on current dfs stack */
|
|
/* II==3 on 1st dfs stack */
|
|
"#ifndef SAFETY",
|
|
|
|
" if (!fairness && a_cycles)",
|
|
" if (II == 2 && ((trpt->o_pm&2) || ((trpt-1)->o_pm&2)))",
|
|
" { II = 3; /* Schwoon & Esparza 2005, Gastin&Moro 2004 */",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"state match on dfs stack\\n\");",
|
|
"#endif",
|
|
" goto same_case;",
|
|
" }",
|
|
|
|
|
|
"#if defined(FULLSTACK) && defined(BITSTATE)",
|
|
" if (!JJ && (now._a_t&1) && depth > A_depth)",
|
|
" { int oj1 = j1;",
|
|
" uchar o_a_t = now._a_t;",
|
|
" now._a_t &= ~(1|16|32);", /* 1st stack */
|
|
" if (onstack_now())", /* changes j1 */
|
|
" { II = 3;",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"state match on 1st dfs stack\\n\");",
|
|
"#endif",
|
|
" }",
|
|
" now._a_t = o_a_t;", /* restore */
|
|
" j1 = oj1;",
|
|
" }",
|
|
"#endif",
|
|
" if (II == 3 && a_cycles && (now._a_t&1))",
|
|
" {",
|
|
"#ifndef NOFAIR",
|
|
" if (fairness && now._cnt[1] > 1) /* was != 0 */",
|
|
" {",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"\tfairness count non-zero\\n\");",
|
|
"#endif",
|
|
" II = 0;", /* treat as new state */
|
|
" } else",
|
|
"#endif",
|
|
" {",
|
|
"#ifndef BITSTATE",
|
|
" nShadow--;",
|
|
"#endif",
|
|
"same_case: if (Lstate) depthfound = Lstate->D;",
|
|
"#ifdef NP",
|
|
" uerror(\"non-progress cycle\");",
|
|
"#else",
|
|
" uerror(\"acceptance cycle\");",
|
|
"#endif",
|
|
" goto Up;",
|
|
" }",
|
|
" }",
|
|
"#endif",
|
|
|
|
"#ifndef NOREDUCE",
|
|
"#ifndef SAFETY",
|
|
" if ((II && JJ) || (II == 3))",
|
|
" { /* marker for liveness proviso */",
|
|
" (trpt-1)->tau |= 16;",
|
|
" truncs2++;",
|
|
" }",
|
|
"#else",
|
|
" if (!II || !JJ)",
|
|
" { /* successor outside stack */",
|
|
" (trpt-1)->tau |= 64;",
|
|
" }",
|
|
"#endif",
|
|
"#endif",
|
|
" if (II)",
|
|
" { truncs++;",
|
|
" goto Up;",
|
|
" }",
|
|
" if (!kk)",
|
|
" { nstates++;",
|
|
" if ((unsigned long) nstates%%1000000 == 0)",
|
|
" snapshot();",
|
|
"#ifdef SVDUMP",
|
|
" if (vprefix > 0)",
|
|
" if (write(svfd, (uchar *) &now, vprefix) != vprefix)",
|
|
" { fprintf(efd, \"writing %%s.svd failed\\n\", Source);",
|
|
" wrapup();",
|
|
" }",
|
|
"#endif",
|
|
"#if defined(MA) && defined(W_XPT)",
|
|
" if ((unsigned long) nstates%%W_XPT == 0)",
|
|
" { void w_xpoint(void);",
|
|
" w_xpoint();",
|
|
" }",
|
|
"#endif",
|
|
" }",
|
|
"#if defined(FULLSTACK) || defined(CNTRSTACK)",
|
|
" onstack_put();",
|
|
"#ifdef DEBUG2",
|
|
"#if defined(FULLSTACK) && !defined(MA)",
|
|
" printf(\"%%d: putting %%u (%%d)\\n\", depth,",
|
|
" trpt->ostate, ",
|
|
" (trpt->ostate)?trpt->ostate->tagged:0);",
|
|
"#else",
|
|
" printf(\"%%d: putting\\n\", depth);",
|
|
"#endif",
|
|
"#endif",
|
|
"#endif",
|
|
" } }",
|
|
|
|
|
|
" if (depth > mreached)",
|
|
" mreached = depth;",
|
|
"#ifdef VERI",
|
|
" if (trpt->tau&4)",
|
|
"#endif",
|
|
" trpt->tau &= ~(1|2); /* timeout and -request off */",
|
|
" _n = 0;",
|
|
"#if SYNC",
|
|
" (trpt+1)->o_n = 0;",
|
|
"#endif",
|
|
"#ifdef VERI",
|
|
" if (now._nr_pr == 0) /* claim terminated */",
|
|
" uerror(\"end state in claim reached\");",
|
|
" check_claim(((P0 *)pptr(0))->_p);",
|
|
"Stutter:",
|
|
" if (trpt->tau&4) /* must make a claimmove */",
|
|
" {",
|
|
|
|
"#ifndef NOFAIR",
|
|
" if ((now._a_t&2) /* A-bit set */",
|
|
" && now._cnt[now._a_t&1] == 1)",
|
|
" { now._a_t &= ~2;",
|
|
" now._cnt[now._a_t&1] = 0;",
|
|
" trpt->o_pm |= 16;",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%3d: fairness Rule 3.: _a_t = %%d\\n\",",
|
|
" depth, now._a_t);",
|
|
"#endif",
|
|
" }",
|
|
"#endif",
|
|
|
|
" II = 0; /* never */",
|
|
" goto Veri0;",
|
|
" }",
|
|
"#endif",
|
|
"#ifndef NOREDUCE",
|
|
" /* Look for a process with only safe transitions */",
|
|
" /* (special rules apply in the 2nd dfs) */",
|
|
"#ifdef SAFETY",
|
|
" if (boq == -1 && From != To)",
|
|
"#else",
|
|
"/* implied: #ifdef FULLSTACK */",
|
|
" if (boq == -1 && From != To",
|
|
" && (!(now._a_t&1)",
|
|
" || (a_cycles &&",
|
|
"#ifndef BITSTATE",
|
|
"#ifdef MA",
|
|
"#ifdef VERI",
|
|
" !((trpt-1)->proviso))",
|
|
"#else",
|
|
" !(trpt->proviso))",
|
|
"#endif",
|
|
"#else",
|
|
"#ifdef VERI",
|
|
" (trpt-1)->ostate &&",
|
|
" !(((char *)&((trpt-1)->ostate->state))[0] & 128))",
|
|
"#else",
|
|
" !(((char *)&(trpt->ostate->state))[0] & 128))",
|
|
"#endif",
|
|
"#endif",
|
|
"#else",
|
|
"#ifdef VERI",
|
|
" (trpt-1)->ostate &&",
|
|
" (trpt-1)->ostate->proviso == 0)",
|
|
"#else",
|
|
" trpt->ostate->proviso == 0)",
|
|
"#endif",
|
|
"#endif",
|
|
" ))",
|
|
"/* #endif */",
|
|
"#endif",
|
|
" for (II = From; II >= To; II -= 1)",
|
|
" {",
|
|
"Resume: /* pick up here if preselect fails */",
|
|
" this = pptr(II);",
|
|
" tt = (int) ((P0 *)this)->_p;",
|
|
" ot = (uchar) ((P0 *)this)->_t;",
|
|
" if (trans[ot][tt]->atom & 8)",
|
|
" { t = trans[ot][tt];",
|
|
" if (t->qu[0] != 0)",
|
|
" { Ccheck++;",
|
|
" if (!q_cond(II, t))",
|
|
" continue;",
|
|
" Cholds++;",
|
|
" }",
|
|
" From = To = II;",
|
|
"#ifdef NIBIS",
|
|
" t->om = 0;",
|
|
"#endif",
|
|
" trpt->tau |= 32; /* preselect marker */",
|
|
"#ifdef DEBUG",
|
|
"#ifdef NIBIS",
|
|
" printf(\"%%3d: proc %%d Pre\", depth, II);",
|
|
" printf(\"Selected (om=%%d, tau=%%d)\\n\", ",
|
|
" t->om, trpt->tau);",
|
|
"#else",
|
|
" printf(\"%%3d: proc %%d PreSelected (tau=%%d)\\n\", ",
|
|
" depth, II, trpt->tau);",
|
|
"#endif",
|
|
"#endif",
|
|
" goto Again;",
|
|
" }",
|
|
" }",
|
|
" trpt->tau &= ~32;",
|
|
"#endif",
|
|
"#if !defined(NOREDUCE) || (defined(ETIM) && !defined(VERI))",
|
|
"Again:",
|
|
"#endif",
|
|
" /* The Main Expansion Loop over Processes */",
|
|
|
|
" trpt->o_pm &= ~(8|16|32|64); /* fairness-marks */",
|
|
|
|
"#ifndef NOFAIR",
|
|
" if (fairness && boq == -1",
|
|
"#ifdef VERI",
|
|
" && (!(trpt->tau&4) && !((trpt-1)->tau&128))",
|
|
"#endif",
|
|
" && !(trpt->tau&8))",
|
|
" { /* A_bit = 1; Cnt = N in acc states with A_bit 0 */",
|
|
" if (!(now._a_t&2))", /* A-bit not set */
|
|
" {",
|
|
" if (a_cycles && (trpt->o_pm&2))",
|
|
" { /* Accepting state */",
|
|
" now._a_t |= 2;",
|
|
" now._cnt[now._a_t&1] = now._nr_pr + 1;", /* NEW +1 */
|
|
" trpt->o_pm |= 8;",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%3d: fairness Rule 1: cnt=%%d, _a_t=%%d\\n\",",
|
|
" depth, now._cnt[now._a_t&1], now._a_t);",
|
|
"#endif",
|
|
" }",
|
|
" } else", /* A-bit set */
|
|
" { /* A_bit = 0 when Cnt 0 */",
|
|
" if (now._cnt[now._a_t&1] == 1)", /* NEW: 1 iso 0 */
|
|
" { now._a_t &= ~2;", /* reset a-bit */
|
|
" now._cnt[now._a_t&1] = 0;", /* NEW: reset cnt */
|
|
" trpt->o_pm |= 16;",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%3d: fairness Rule 3: _a_t = %%d\\n\",",
|
|
" depth, now._a_t);",
|
|
"#endif",
|
|
" } } }",
|
|
"#endif",
|
|
|
|
" for (II = From; II >= To; II -= 1)",
|
|
" {",
|
|
"#if SYNC",
|
|
" /* no rendezvous with same proc */",
|
|
" if (boq != -1 && trpt->pr == II) continue;",
|
|
"#endif",
|
|
"#ifdef VERI",
|
|
"Veri0:",
|
|
"#endif",
|
|
" this = pptr(II);",
|
|
" tt = (int) ((P0 *)this)->_p;",
|
|
" ot = (uchar) ((P0 *)this)->_t;",
|
|
|
|
"#ifdef NIBIS",
|
|
" /* don't repeat a previous preselected expansion */",
|
|
" /* could hit this if reduction proviso was false */",
|
|
" t = trans[ot][tt];",
|
|
" if (!(trpt->tau&4)", /* not claim */
|
|
" && !(trpt->tau&1)", /* not timeout */
|
|
" && !(trpt->tau&32)", /* not preselected */
|
|
" && (t->atom & 8)", /* local */
|
|
" && boq == -1", /* not inside rendezvous */
|
|
" && From != To)", /* not inside atomic seq */
|
|
" { if (t->qu[0] == 0", /* unconditional */
|
|
" || q_cond(II, t))", /* true condition */
|
|
" { _m = t->om;",
|
|
" if (_m>_n||(_n>3&&_m!=0)) _n=_m;",
|
|
" continue; /* did it before */",
|
|
" } }",
|
|
"#endif",
|
|
" trpt->o_pm &= ~1; /* no move in this pid yet */",
|
|
"#ifdef EVENT_TRACE",
|
|
" (trpt+1)->o_event = now._event;",
|
|
"#endif",
|
|
" /* Fairness: Cnt++ when Cnt == II */",
|
|
"#ifndef NOFAIR",
|
|
" trpt->o_pm &= ~64; /* didn't apply rule 2 */",
|
|
" if (fairness",
|
|
" && boq == -1", /* not mid rv - except rcv - NEW 3.0.8 */
|
|
" && !(trpt->o_pm&32)", /* Rule 2 not in effect */
|
|
" && (now._a_t&2)", /* A-bit is set */
|
|
" && now._cnt[now._a_t&1] == II+2)",
|
|
" { now._cnt[now._a_t&1] -= 1;",
|
|
"#ifdef VERI",
|
|
" /* claim need not participate */",
|
|
" if (II == 1)",
|
|
" now._cnt[now._a_t&1] = 1;",
|
|
"#endif",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%3d: proc %%d fairness \", depth, II);",
|
|
" printf(\"Rule 2: --cnt to %%d (%%d)\\n\",",
|
|
" now._cnt[now._a_t&1], now._a_t);",
|
|
"#endif",
|
|
" trpt->o_pm |= (32|64);",
|
|
" }",
|
|
"#endif",
|
|
"#ifdef HAS_PROVIDED",
|
|
" if (!provided(II, ot, tt, t)) continue;",
|
|
"#endif",
|
|
" /* check all trans of proc II - escapes first */",
|
|
"#ifdef HAS_UNLESS",
|
|
" trpt->e_state = 0;",
|
|
"#endif",
|
|
" (trpt+1)->pr = (uchar) II;", /* for uerror */
|
|
" (trpt+1)->st = tt;",
|
|
|
|
"#ifdef RANDOMIZE",
|
|
" for (ooi = eoi = 0, t = trans[ot][tt]; t; t = t->nxt, ooi++)",
|
|
" if (strcmp(t->tp, \"else\") == 0)",
|
|
" eoi++;",
|
|
"",
|
|
" if (eoi)",
|
|
" { t = trans[ot][tt];",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"randomizer: suppressed, saw else\\n\");",
|
|
"#endif",
|
|
" } else",
|
|
" { eoi = rand()%%ooi;",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"randomizer: skip %%d in %%d\\n\", eoi, ooi);",
|
|
"#endif",
|
|
" for (t = trans[ot][tt]; t; t = t->nxt)",
|
|
" if (eoi-- <= 0) break;",
|
|
" }",
|
|
"DOMORE:",
|
|
" for ( ; t && ooi > 0; t = t->nxt, ooi--)",
|
|
"#else",
|
|
" for (t = trans[ot][tt]; t; t = t->nxt)",
|
|
"#endif",
|
|
" {",
|
|
"#ifdef HAS_UNLESS",
|
|
" /* exploring all transitions from",
|
|
" * a single escape state suffices",
|
|
" */",
|
|
" if (trpt->e_state > 0",
|
|
" && trpt->e_state != t->e_trans)",
|
|
" {",
|
|
"#ifdef DEBUG",
|
|
" printf(\"skip 2nd escape %%d (did %%d before)\\n\",",
|
|
" t->e_trans, trpt->e_state);",
|
|
"#endif",
|
|
" break;",
|
|
" }",
|
|
"#endif",
|
|
" (trpt+1)->o_t = t;", /* for uerror */
|
|
"#ifdef INLINE",
|
|
"#include FORWARD_MOVES",
|
|
"P999: /* jumps here when move succeeds */",
|
|
"#else",
|
|
" if (!(_m = do_transit(t, II))) continue;",
|
|
"#endif",
|
|
" if (boq == -1)",
|
|
"#ifdef CTL",
|
|
" /* for branching-time, can accept reduction only if */",
|
|
" /* the persistent set contains just 1 transition */",
|
|
" { if ((trpt->tau&32) && (trpt->o_pm&1))",
|
|
" trpt->tau |= 16;",
|
|
" trpt->o_pm |= 1; /* we moved */",
|
|
" }",
|
|
"#else",
|
|
" trpt->o_pm |= 1; /* we moved */",
|
|
"#endif",
|
|
"#ifdef PEG",
|
|
" peg[t->forw]++;",
|
|
"#endif",
|
|
|
|
"#if defined(VERBOSE) || defined(CHECK)",
|
|
"#if defined(SVDUMP)",
|
|
" printf(\"%%3d: proc %%d exec %%d \\n\", ",
|
|
" depth, II, t->t_id);",
|
|
"#else",
|
|
" printf(\"%%3d: proc %%d exec %%d, \", ",
|
|
" depth, II, t->forw);",
|
|
" printf(\"%%d to %%d, %%s %%s %%s\", ",
|
|
" tt, t->st, t->tp,",
|
|
" (t->atom&2)?\"atomic\":\"\",",
|
|
" (boq != -1)?\"rendez-vous\":\"\");",
|
|
"#ifdef HAS_UNLESS",
|
|
" if (t->e_trans)",
|
|
" printf(\" (escapes to state %%d)\",",
|
|
" t->st);",
|
|
"#endif",
|
|
" printf(\" %%saccepting [tau=%%d]\\n\",",
|
|
" (trpt->o_pm&2)?\"\":\"non-\", trpt->tau);",
|
|
"#endif",
|
|
"#ifdef RANDOMIZE",
|
|
" printf(\" randomizer %%d\\n\", ooi);",
|
|
"#endif",
|
|
"#endif",
|
|
|
|
"#ifdef HAS_LAST",
|
|
"#ifdef VERI",
|
|
" if (II != 0)",
|
|
"#endif",
|
|
" now._last = II - BASE;",
|
|
"#endif",
|
|
"#ifdef HAS_UNLESS",
|
|
" trpt->e_state = t->e_trans;",
|
|
"#endif",
|
|
|
|
" depth++; trpt++;",
|
|
" trpt->pr = (uchar) II;",
|
|
" trpt->st = tt;",
|
|
" trpt->o_pm &= ~(2|4);",
|
|
" if (t->st > 0)",
|
|
" { ((P0 *)this)->_p = t->st;",
|
|
"/* moved down reached[ot][t->st] = 1; */",
|
|
" }",
|
|
"#ifndef SAFETY",
|
|
" if (a_cycles)",
|
|
" {",
|
|
"#if (ACCEPT_LAB>0 && !defined(NP)) || (PROG_LAB>0 && defined(HAS_NP))",
|
|
" int ii;",
|
|
"#endif",
|
|
"#define P__Q ((P0 *)pptr(ii))",
|
|
"#if ACCEPT_LAB>0",
|
|
"#ifdef NP",
|
|
" /* state 1 of np_ claim is accepting */",
|
|
" if (((P0 *)pptr(0))->_p == 1)",
|
|
" trpt->o_pm |= 2;",
|
|
"#else",
|
|
" for (ii = 0; ii < (int) now._nr_pr; ii++)",
|
|
" { if (accpstate[P__Q->_t][P__Q->_p])",
|
|
" { trpt->o_pm |= 2;",
|
|
" break;",
|
|
" } }",
|
|
"#endif",
|
|
"#endif",
|
|
"#if defined(HAS_NP) && PROG_LAB>0",
|
|
" for (ii = 0; ii < (int) now._nr_pr; ii++)",
|
|
" { if (progstate[P__Q->_t][P__Q->_p])",
|
|
" { trpt->o_pm |= 4;",
|
|
" break;",
|
|
" } }",
|
|
"#endif",
|
|
"#undef P__Q",
|
|
" }",
|
|
"#endif",
|
|
" trpt->o_t = t; trpt->o_n = _n;",
|
|
" trpt->o_ot = ot; trpt->o_tt = tt;",
|
|
" trpt->o_To = To; trpt->o_m = _m;",
|
|
" trpt->tau = 0;",
|
|
"#ifdef RANDOMIZE",
|
|
" trpt->oo_i = ooi;",
|
|
"#endif",
|
|
" if (boq != -1 || (t->atom&2))",
|
|
" { trpt->tau |= 8;",
|
|
"#ifdef VERI",
|
|
" /* atomic sequence in claim */",
|
|
" if((trpt-1)->tau&4)",
|
|
" trpt->tau |= 4;",
|
|
" else",
|
|
" trpt->tau &= ~4;",
|
|
" } else",
|
|
" { if ((trpt-1)->tau&4)",
|
|
" trpt->tau &= ~4;",
|
|
" else",
|
|
" trpt->tau |= 4;",
|
|
" }",
|
|
" /* if claim allowed timeout, so */",
|
|
" /* does the next program-step: */",
|
|
" if (((trpt-1)->tau&1) && !(trpt->tau&4))",
|
|
" trpt->tau |= 1;",
|
|
"#else",
|
|
" } else",
|
|
" trpt->tau &= ~8;",
|
|
"#endif",
|
|
" if (boq == -1 && (t->atom&2))",
|
|
" { From = To = II; nlinks++;",
|
|
" } else",
|
|
" { From = now._nr_pr-1; To = BASE;",
|
|
" }",
|
|
" goto Down; /* pseudo-recursion */",
|
|
"Up:",
|
|
"#ifdef CHECK",
|
|
" printf(\"%%d: Up - %%s\\n\", depth,",
|
|
" (trpt->tau&4)?\"claim\":\"program\");",
|
|
"#endif",
|
|
"#ifdef MA",
|
|
" if (depth <= 0) return;",
|
|
" /* e.g., if first state is old, after a restart */",
|
|
"#endif",
|
|
|
|
"#ifdef SC",
|
|
" if (CNT1 > CNT2",
|
|
" && depth < hiwater - (HHH-DDD) + 2)",
|
|
" {",
|
|
" trpt += DDD;",
|
|
" disk2stack();",
|
|
" maxdepth -= DDD;",
|
|
" hiwater -= DDD;",
|
|
"if(verbose)",
|
|
"printf(\"unzap %%d: %%d\\n\", CNT2, hiwater);",
|
|
" }",
|
|
"#endif",
|
|
|
|
"#ifndef NOFAIR",
|
|
" if (trpt->o_pm&128) /* fairness alg */",
|
|
" { now._cnt[now._a_t&1] = trpt->bup.oval;",
|
|
" _n = 1; trpt->o_pm &= ~128;",
|
|
" depth--; trpt--;",
|
|
"#if defined(VERBOSE) || defined(CHECK)",
|
|
" printf(\"%%3d: reversed fairness default move\\n\", depth);",
|
|
"#endif",
|
|
" goto Q999;",
|
|
" }",
|
|
"#endif",
|
|
|
|
"#ifdef HAS_LAST",
|
|
"#ifdef VERI",
|
|
" { int d; Trail *trl;",
|
|
" now._last = 0;",
|
|
" for (d = 1; d < depth; d++)",
|
|
" { trl = getframe(depth-d); /* was (trpt-d) */",
|
|
" if (trl->pr != 0)",
|
|
" { now._last = trl->pr - BASE;",
|
|
" break;",
|
|
" } } }",
|
|
"#else",
|
|
" now._last = (depth<1)?0:(trpt-1)->pr;",
|
|
"#endif",
|
|
"#endif",
|
|
"#ifdef EVENT_TRACE",
|
|
" now._event = trpt->o_event;",
|
|
"#endif",
|
|
"#ifndef SAFETY",
|
|
" if ((now._a_t&1) && depth <= A_depth)",
|
|
" return; /* to checkcycles() */",
|
|
"#endif",
|
|
" t = trpt->o_t; _n = trpt->o_n;",
|
|
" ot = trpt->o_ot; II = trpt->pr;",
|
|
" tt = trpt->o_tt; this = pptr(II);",
|
|
" To = trpt->o_To; _m = trpt->o_m;",
|
|
"#ifdef RANDOMIZE",
|
|
" ooi = trpt->oo_i;",
|
|
"#endif",
|
|
"#ifdef INLINE_REV",
|
|
" _m = do_reverse(t, II, _m);",
|
|
"#else",
|
|
"#include REVERSE_MOVES",
|
|
"R999: /* jumps here when done */",
|
|
"#endif",
|
|
|
|
"#ifdef VERBOSE",
|
|
" printf(\"%%3d: proc %%d \", depth, II);",
|
|
" printf(\"reverses %%d, %%d to %%d,\",",
|
|
" t->forw, tt, t->st);",
|
|
" printf(\" %%s [abit=%%d,adepth=%%d,\", ",
|
|
" t->tp, now._a_t, A_depth);",
|
|
" printf(\"tau=%%d,%%d]\\n\", ",
|
|
" trpt->tau, (trpt-1)->tau);",
|
|
"#endif",
|
|
"#ifndef NOREDUCE",
|
|
" /* pass the proviso tags */",
|
|
" if ((trpt->tau&8) /* rv or atomic */",
|
|
" && (trpt->tau&16))",
|
|
" (trpt-1)->tau |= 16;",
|
|
"#ifdef SAFETY",
|
|
" if ((trpt->tau&8) /* rv or atomic */",
|
|
" && (trpt->tau&64))",
|
|
" (trpt-1)->tau |= 64;",
|
|
"#endif",
|
|
"#endif",
|
|
" depth--; trpt--;",
|
|
"#ifdef NIBIS",
|
|
" (trans[ot][tt])->om = _m; /* head of list */",
|
|
"#endif",
|
|
|
|
" /* i.e., not set if rv fails */",
|
|
" if (_m)",
|
|
" {",
|
|
"#if defined(VERI) && !defined(NP)",
|
|
" if (II == 0 && verbose && !reached[ot][t->st])",
|
|
" {",
|
|
" printf(\"depth %%d: Claim reached state %%d (line %%d)\\n\",",
|
|
" depth, t->st, src_claim [t->st]);",
|
|
" fflush(stdout);",
|
|
" }",
|
|
"#endif",
|
|
" reached[ot][t->st] = 1;",
|
|
" reached[ot][tt] = 1;",
|
|
" }",
|
|
"#ifdef HAS_UNLESS",
|
|
" else trpt->e_state = 0; /* undo */",
|
|
"#endif",
|
|
|
|
" if (_m>_n||(_n>3&&_m!=0)) _n=_m;",
|
|
" ((P0 *)this)->_p = tt;",
|
|
" } /* all options */",
|
|
|
|
"#ifdef RANDOMIZE",
|
|
" if (!t && ooi > 0)", /* means we skipped some initial options */
|
|
" { t = trans[ot][tt];",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"randomizer: continue for %%d more\\n\", ooi);",
|
|
"#endif",
|
|
" goto DOMORE;",
|
|
" }",
|
|
"#ifdef VERBOSE",
|
|
" else",
|
|
" printf(\"randomizer: done\\n\");",
|
|
"#endif",
|
|
"#endif",
|
|
|
|
"#ifndef NOFAIR",
|
|
" /* Fairness: undo Rule 2 */",
|
|
" if ((trpt->o_pm&32)",/* rule 2 was applied */
|
|
" && (trpt->o_pm&64))",/* by this process II */
|
|
" { if (trpt->o_pm&1)",/* it didn't block */
|
|
" {",
|
|
"#ifdef VERI",
|
|
" if (now._cnt[now._a_t&1] == 1)", /* NEW: 1 iso 0 */
|
|
" now._cnt[now._a_t&1] = 2;", /* NEW: 2 iso 1*/
|
|
"#endif",
|
|
" now._cnt[now._a_t&1] += 1;",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"%%3d: proc %%d fairness \", depth, II);",
|
|
" printf(\"undo Rule 2, cnt=%%d, _a_t=%%d\\n\",",
|
|
" now._cnt[now._a_t&1], now._a_t);",
|
|
"#endif",
|
|
" trpt->o_pm &= ~(32|64);",
|
|
" } else", /* process blocked */
|
|
" { if (_n > 0)", /* a prev proc didn't */
|
|
" {", /* start over */
|
|
" trpt->o_pm &= ~64;",
|
|
" II = From+1;",
|
|
" } } }",
|
|
"#endif",
|
|
|
|
"#ifdef VERI",
|
|
" if (II == 0) break; /* never claim */",
|
|
"#endif",
|
|
" } /* all processes */",
|
|
|
|
"#ifndef NOFAIR",
|
|
" /* Fairness: undo Rule 2 */",
|
|
" if (trpt->o_pm&32) /* remains if proc blocked */",
|
|
" {",
|
|
"#ifdef VERI",
|
|
" if (now._cnt[now._a_t&1] == 1)", /* NEW: 1 iso 0 */
|
|
" now._cnt[now._a_t&1] = 2;", /* NEW: 2 iso 1 */
|
|
"#endif",
|
|
" now._cnt[now._a_t&1] += 1;",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"%%3d: proc -- fairness \", depth);",
|
|
" printf(\"undo Rule 2, cnt=%%d, _a_t=%%d\\n\",",
|
|
" now._cnt[now._a_t&1], now._a_t);",
|
|
"#endif",
|
|
" trpt->o_pm &= ~32;",
|
|
" }",
|
|
"#ifndef NP",
|
|
/* 12/97 non-progress cycles cannot be created
|
|
* by stuttering extension, here or elsewhere
|
|
*/
|
|
" if (fairness",
|
|
" && _n == 0 /* nobody moved */",
|
|
"#ifdef VERI",
|
|
" && !(trpt->tau&4) /* in program move */",
|
|
"#endif",
|
|
" && !(trpt->tau&8) /* not an atomic one */",
|
|
"#ifdef OTIM",
|
|
" && ((trpt->tau&1) || endstate())",
|
|
"#else",
|
|
"#ifdef ETIM",
|
|
" && (trpt->tau&1) /* already tried timeout */",
|
|
"#endif",
|
|
"#endif",
|
|
"#ifndef NOREDUCE",
|
|
" /* see below */",
|
|
" && !((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
|
|
"#endif",
|
|
" && now._cnt[now._a_t&1] > 0) /* needed more procs */",
|
|
" { depth++; trpt++;",
|
|
" trpt->o_pm |= 128 | ((trpt-1)->o_pm&(2|4));",
|
|
" trpt->bup.oval = now._cnt[now._a_t&1];",
|
|
" now._cnt[now._a_t&1] = 1;",
|
|
"#ifdef VERI",
|
|
" trpt->tau = 4;",
|
|
"#else",
|
|
" trpt->tau = 0;",
|
|
"#endif",
|
|
" From = now._nr_pr-1; To = BASE;",
|
|
"#if defined(VERBOSE) || defined(CHECK)",
|
|
" printf(\"%%3d: fairness default move \", depth);",
|
|
" printf(\"(all procs block)\\n\");",
|
|
"#endif",
|
|
" goto Down;",
|
|
" }",
|
|
"#endif",
|
|
"Q999: /* returns here with _n>0 when done */;",
|
|
|
|
" if (trpt->o_pm&8)",
|
|
" { now._a_t &= ~2;",
|
|
" now._cnt[now._a_t&1] = 0;",
|
|
" trpt->o_pm &= ~8;",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"%%3d: fairness undo Rule 1, _a_t=%%d\\n\",",
|
|
" depth, now._a_t);",
|
|
"#endif",
|
|
" }",
|
|
" if (trpt->o_pm&16)",
|
|
" { now._a_t |= 2;", /* restore a-bit */
|
|
" now._cnt[now._a_t&1] = 1;", /* NEW: restore cnt */
|
|
" trpt->o_pm &= ~16;",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"%%3d: fairness undo Rule 3, _a_t=%%d\\n\",",
|
|
" depth, now._a_t);",
|
|
"#endif",
|
|
" }",
|
|
"#endif",
|
|
|
|
"#ifndef NOREDUCE",
|
|
"#ifdef SAFETY",
|
|
" /* preselected move - no successors outside stack */",
|
|
" if ((trpt->tau&32) && !(trpt->tau&64))",
|
|
" { From = now._nr_pr-1; To = BASE;",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%3d: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
|
|
" depth, II+1, _n, trpt->tau);",
|
|
"#endif",
|
|
" _n = 0; trpt->tau &= ~(16|32|64);",
|
|
" if (II >= BASE) /* II already decremented */",
|
|
" goto Resume;",
|
|
" else",
|
|
" goto Again;",
|
|
" }",
|
|
"#else",
|
|
" /* at least one move that was preselected at this */",
|
|
" /* level, blocked or truncated at the next level */",
|
|
"/* implied: #ifdef FULLSTACK */",
|
|
" if ((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
|
|
" {",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%3d: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
|
|
" depth, II+1, (int) _n, trpt->tau);",
|
|
"#endif",
|
|
" if (a_cycles && (trpt->tau&16))",
|
|
" { if (!(now._a_t&1))",
|
|
" {",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%3d: setting proviso bit\\n\", depth);",
|
|
"#endif",
|
|
"#ifndef BITSTATE",
|
|
"#ifdef MA",
|
|
"#ifdef VERI",
|
|
" (trpt-1)->proviso = 1;",
|
|
"#else",
|
|
" trpt->proviso = 1;",
|
|
"#endif",
|
|
"#else",
|
|
"#ifdef VERI",
|
|
" if ((trpt-1)->ostate)",
|
|
" ((char *)&((trpt-1)->ostate->state))[0] |= 128;",
|
|
"#else",
|
|
" ((char *)&(trpt->ostate->state))[0] |= 128;",
|
|
"#endif",
|
|
"#endif",
|
|
"#else",
|
|
"#ifdef VERI",
|
|
" if ((trpt-1)->ostate)",
|
|
" (trpt-1)->ostate->proviso = 1;",
|
|
"#else",
|
|
" trpt->ostate->proviso = 1;",
|
|
"#endif",
|
|
"#endif",
|
|
" From = now._nr_pr-1; To = BASE;",
|
|
" _n = 0; trpt->tau &= ~(16|32|64);",
|
|
" goto Again; /* do full search */",
|
|
" } /* else accept reduction */",
|
|
" } else",
|
|
" { From = now._nr_pr-1; To = BASE;",
|
|
" _n = 0; trpt->tau &= ~(16|32|64);",
|
|
" if (II >= BASE) /* already decremented */",
|
|
" goto Resume;",
|
|
" else",
|
|
" goto Again;",
|
|
" } }",
|
|
"/* #endif */",
|
|
"#endif",
|
|
"#endif",
|
|
|
|
" if (_n == 0 || ((trpt->tau&4) && (trpt->tau&2)))",
|
|
" {",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%3d: no move [II=%%d, tau=%%d, boq=%%d]\\n\",",
|
|
" depth, II, trpt->tau, boq);",
|
|
"#endif",
|
|
"#if SYNC",
|
|
" /* ok if a rendez-vous fails: */",
|
|
" if (boq != -1) goto Done;",
|
|
"#endif",
|
|
" /* ok if no procs or we're at maxdepth */",
|
|
" if ((now._nr_pr == 0 && (!strict || qs_empty()))",
|
|
"#ifdef OTIM",
|
|
" || endstate()",
|
|
"#endif",
|
|
" || depth >= maxdepth-1) goto Done;",
|
|
|
|
" if ((trpt->tau&8) && !(trpt->tau&4))",
|
|
" { trpt->tau &= ~(1|8);",
|
|
" /* 1=timeout, 8=atomic */",
|
|
" From = now._nr_pr-1; To = BASE;",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%3d: atomic step proc %%d \", depth, II+1);",
|
|
" printf(\"unexecutable\\n\");",
|
|
"#endif",
|
|
"#ifdef VERI",
|
|
" trpt->tau |= 4; /* switch to claim */",
|
|
"#endif",
|
|
" goto AllOver;",
|
|
" }",
|
|
|
|
"#ifdef ETIM",
|
|
" if (!(trpt->tau&1)) /* didn't try timeout yet */",
|
|
" {",
|
|
"#ifdef VERI",
|
|
" if (trpt->tau&4)",
|
|
" {",
|
|
"#ifndef NTIM",
|
|
" if (trpt->tau&2) /* requested */",
|
|
"#endif",
|
|
" { trpt->tau |= 1;",
|
|
" trpt->tau &= ~2;",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%d: timeout\\n\", depth);",
|
|
"#endif",
|
|
" goto Stutter;",
|
|
" } }",
|
|
" else",
|
|
" { /* only claim can enable timeout */",
|
|
" if ((trpt->tau&8)",
|
|
" && !((trpt-1)->tau&4))",
|
|
"/* blocks inside an atomic */ goto BreakOut;",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%d: req timeout\\n\",",
|
|
" depth);",
|
|
"#endif",
|
|
" (trpt-1)->tau |= 2; /* request */",
|
|
" goto Up;",
|
|
" }",
|
|
"#else",
|
|
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%d: timeout\\n\", depth);",
|
|
"#endif",
|
|
" trpt->tau |= 1;",
|
|
" goto Again;",
|
|
"#endif",
|
|
" }",
|
|
"#endif",
|
|
|
|
/* old location of atomic block code */
|
|
"#ifdef VERI",
|
|
"BreakOut:",
|
|
"#ifndef NOSTUTTER",
|
|
" if (!(trpt->tau&4))",
|
|
" { trpt->tau |= 4; /* claim stuttering */",
|
|
" trpt->tau |= 128; /* stutter mark */",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%d: claim stutter\\n\", depth);",
|
|
"#endif",
|
|
" goto Stutter;",
|
|
" }",
|
|
"#else",
|
|
" ;",
|
|
"#endif",
|
|
"#else",
|
|
" if (!noends && !a_cycles && !endstate())",
|
|
" { depth--; trpt--; /* new 4.2.3 */",
|
|
" uerror(\"invalid end state\");",
|
|
" depth++; trpt++;",
|
|
" }",
|
|
"#ifndef NOSTUTTER",
|
|
" else if (a_cycles && (trpt->o_pm&2)) /* new 4.2.4 */",
|
|
" { depth--; trpt--;",
|
|
" uerror(\"accept stutter\");",
|
|
" depth++; trpt++;",
|
|
" }",
|
|
"#endif",
|
|
"#endif",
|
|
" }",
|
|
"Done:",
|
|
" if (!(trpt->tau&8)) /* not in atomic seqs */",
|
|
" {",
|
|
"#ifndef SAFETY",
|
|
" if (_n != 0", /* we made a move */
|
|
"#ifdef VERI",
|
|
" /* --after-- a program-step, i.e., */",
|
|
" /* after backtracking a claim-step */",
|
|
" && (trpt->tau&4)",
|
|
" /* with at least one running process */",
|
|
" /* unless in a stuttered accept state */",
|
|
" && ((now._nr_pr > 1) || (trpt->o_pm&2))",
|
|
"#endif",
|
|
" && !(now._a_t&1))", /* not in 2nd DFS */
|
|
" {",
|
|
"#ifndef NOFAIR",
|
|
" if (fairness)", /* implies a_cycles */
|
|
" {",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"Consider check %%d %%d...\\n\",",
|
|
" now._a_t, now._cnt[0]);",
|
|
"#endif",
|
|
#if 0
|
|
the a-bit is set, which means that the fairness
|
|
counter is running -- it was started in an accepting state.
|
|
we check that the counter reached 1, which means that all
|
|
processes moved least once.
|
|
this means we can start the search for cycles -
|
|
to be able to return to this state, we should be able to
|
|
run down the counter to 1 again -- which implies a visit to
|
|
the accepting state -- even though the Seed state for this
|
|
search is itself not necessarily accepting
|
|
#endif
|
|
" if ((now._a_t&2) /* A-bit */",
|
|
" && (now._cnt[0] == 1))",
|
|
" checkcycles();",
|
|
" } else",
|
|
"#endif",
|
|
" if (a_cycles && (trpt->o_pm&2))",
|
|
" checkcycles();",
|
|
" }",
|
|
"#endif",
|
|
"#ifndef MA",
|
|
"#if defined(FULLSTACK) || defined(CNTRSTACK)",
|
|
"#ifdef VERI",
|
|
" if (boq == -1",
|
|
" && (((trpt->tau&4) && !(trpt->tau&128))",
|
|
" || ( (trpt-1)->tau&128)))",
|
|
"#else",
|
|
" if (boq == -1)",
|
|
"#endif",
|
|
" {",
|
|
"#ifdef DEBUG2",
|
|
"#if defined(FULLSTACK)",
|
|
" printf(\"%%d: zapping %%u (%%d)\\n\",",
|
|
" depth, trpt->ostate,",
|
|
" (trpt->ostate)?trpt->ostate->tagged:0);",
|
|
"#endif",
|
|
"#endif",
|
|
" onstack_zap();",
|
|
" }",
|
|
"#endif",
|
|
"#else",
|
|
"#ifdef VERI",
|
|
" if (boq == -1",
|
|
" && (((trpt->tau&4) && !(trpt->tau&128))",
|
|
" || ( (trpt-1)->tau&128)))",
|
|
"#else",
|
|
" if (boq == -1)",
|
|
"#endif",
|
|
" {",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%d: zapping\\n\", depth);",
|
|
"#endif",
|
|
" onstack_zap();",
|
|
"#ifndef NOREDUCE",
|
|
" if (trpt->proviso)",
|
|
" gstore((char *) &now, vsize, 1);",
|
|
"#endif",
|
|
" }",
|
|
"#endif",
|
|
" }",
|
|
" if (depth > 0) goto Up;",
|
|
"}\n",
|
|
"#else",
|
|
"void new_state(void) { /* place holder */ }",
|
|
"#endif", /* BFS */
|
|
"",
|
|
"void",
|
|
"assert(int a, char *s, int ii, int tt, Trans *t)",
|
|
"{",
|
|
" if (!a && !noasserts)",
|
|
" { char bad[1024];",
|
|
" strcpy(bad, \"assertion violated \");",
|
|
" if (strlen(s) > 1000)",
|
|
" { strncpy(&bad[19], (const char *) s, 1000);",
|
|
" bad[1019] = '\\0';",
|
|
" } else",
|
|
" strcpy(&bad[19], s);",
|
|
" uerror(bad);",
|
|
" }",
|
|
"}",
|
|
"#ifndef NOBOUNDCHECK",
|
|
"int",
|
|
"Boundcheck(int x, int y, int a1, int a2, Trans *a3)",
|
|
"{",
|
|
" assert((x >= 0 && x < y), \"- invalid array index\",",
|
|
" a1, a2, a3);",
|
|
" return x;",
|
|
"}",
|
|
"#endif",
|
|
"void",
|
|
"wrap_stats(void)",
|
|
"{",
|
|
" if (nShadow>0)",
|
|
" printf(\"%%8g states, stored (%%g visited)\\n\",",
|
|
" nstates - nShadow, nstates);",
|
|
" else",
|
|
" printf(\"%%8g states, stored\\n\", nstates);",
|
|
"#ifdef BFS",
|
|
"#if SYNC",
|
|
" printf(\" %%8g nominal states (- rv and atomic)\\n\", nstates-midrv-nlinks+revrv);",
|
|
" printf(\" %%8g rvs succeeded\\n\", midrv-failedrv);",
|
|
"#else",
|
|
" printf(\" %%8g nominal states (stored-atomic)\\n\", nstates-nlinks);",
|
|
"#endif",
|
|
"#ifdef DEBUG",
|
|
" printf(\" %%8g midrv\\n\", midrv);",
|
|
" printf(\" %%8g failedrv\\n\", failedrv);",
|
|
" printf(\" %%8g revrv\\n\", revrv);",
|
|
"#endif",
|
|
"#endif",
|
|
" printf(\"%%8g states, matched\\n\", truncs);",
|
|
"#ifdef CHECK",
|
|
" printf(\"%%8g matches within stack\\n\",truncs2);",
|
|
"#endif",
|
|
" if (nShadow>0)",
|
|
" printf(\"%%8g transitions (= visited+matched)\\n\",",
|
|
" nstates+truncs);",
|
|
" else",
|
|
" printf(\"%%8g transitions (= stored+matched)\\n\",",
|
|
" nstates+truncs);",
|
|
" printf(\"%%8g atomic steps\\n\", nlinks);",
|
|
" if (nlost) printf(\"%%g lost messages\\n\", (double) nlost);",
|
|
"",
|
|
"#ifndef BITSTATE",
|
|
" printf(\"hash conflicts: %%g (resolved)\\n\", hcmp);",
|
|
"#else",
|
|
"#ifdef CHECK",
|
|
" printf(\"%%8g states allocated for dfs stack\\n\", ngrabs);",
|
|
"#endif",
|
|
" printf(\"\\nhash factor: %%4g (best if > 100.)\\n\\n\",",
|
|
" (double)(1<<(ssize-8)) / (double) nstates * 256.0);",
|
|
" printf(\"bits set per state: %%u (-k%%u)\\n\", hfns, hfns);",
|
|
"#if 0",
|
|
#ifndef POWOW
|
|
" if (udmem)",
|
|
" printf(\"total bits available: %%8g (-M%%ld)\\n\",",
|
|
" ((double) udmem) * 8.0, udmem/(1024L*1024L));",
|
|
" else",
|
|
#endif
|
|
" printf(\"total bits available: %%8g (-w%%d)\\n\",",
|
|
" ((double) (1L << (ssize-4)) * 16.0), ssize);",
|
|
"#endif",
|
|
"#ifdef COVEST",
|
|
" /* this code requires compilation with -lm on some systems */",
|
|
" { double pow(double, double);",
|
|
" double log(double);",
|
|
" unsigned int best_k;",
|
|
" double i, n = 30000.0L;",
|
|
" double f, p, q, m, c, est = 0.0L, k = (double)hfns;",
|
|
" c = (double) nstates / n;",
|
|
" m = (double) (1<<(ssize-8)) * 256.0L / c;",
|
|
" p = 1.0L - (k / m); q = 1.0L;",
|
|
" for (i = 0.0L; i - est < n; i += 1.0L)",
|
|
" { q *= p;",
|
|
" est += pow(1.0L - q, k);",
|
|
" }",
|
|
" f = m/i;",
|
|
" est *= c;",
|
|
" i *= c;",
|
|
" /* account for loss from enhanced double hashing */",
|
|
" if (hfns > 2) est += i * pow(0.5, (double) ssize * 2.0);",
|
|
"",
|
|
" if (f < 1.134) best_k = 1;",
|
|
" else if (f < 2.348) best_k = 2;",
|
|
" else if (f < 3.644) best_k = 3;",
|
|
" else best_k = (unsigned int) (pow(3.8L,1.0L/(f+4.2L))*f*.69315L + 0.99999999L);",
|
|
"",
|
|
" if (best_k != hfns && best_k > ssize)",
|
|
" best_k = (unsigned int) 1.0 + ssize/log((double)best_k / (double)ssize + 3.0);",
|
|
"",
|
|
" if (best_k > 32)",
|
|
" best_k = 1 + (unsigned int) (32.0/log((double)best_k/35.0));",
|
|
"",
|
|
" if (est * (double) nstates < 1.0)",
|
|
" { printf(\"prob. of omissions: negligible\\n\");",
|
|
" return; /* no hints needed */",
|
|
" }",
|
|
"",
|
|
" if (best_k != hfns)",
|
|
" { printf(\"hint: repeating the search with -k%%u \", best_k);",
|
|
" printf(\"may increase accuracy\\n\");",
|
|
" } else",
|
|
" { printf(\"hint: the current setting for -k (-k%%d) \", hfns);",
|
|
" printf(\"is likely to be optimal for -w%%d\\n\", ssize);",
|
|
" }",
|
|
" if (ssize < 32)",
|
|
" { printf(\"hint: increasing -w above -w%%d \", ssize);",
|
|
" printf(\"will increase accuracy (max is -w34)\\n\");",
|
|
" printf(\"(in xspin, increase Estimated State Space Size)\\n\");",
|
|
" } }",
|
|
"#endif",
|
|
"#endif",
|
|
"}",
|
|
"void",
|
|
"wrapup(void)",
|
|
"{",
|
|
"#if defined(BITSTATE) || !defined(NOCOMP)",
|
|
" double nr1, nr2, nr3 = 0.0, nr4, nr5 = 0.0;",
|
|
"#if !defined(MA) && (defined(MEMCNT) || defined(MEMLIM))",
|
|
" int mverbose = 1;",
|
|
"#else",
|
|
" int mverbose = verbose;",
|
|
"#endif",
|
|
"#endif",
|
|
|
|
" signal(SIGINT, SIG_DFL);",
|
|
" printf(\"(%%s)\\n\", Version);",
|
|
" if (!done) printf(\"Warning: Search not completed\\n\");",
|
|
"#ifdef SC",
|
|
" (void) unlink((const char *)stackfile);",
|
|
"#endif",
|
|
"#ifdef BFS",
|
|
" printf(\" + Using Breadth-First Search\\n\");",
|
|
"#endif",
|
|
"#ifndef NOREDUCE",
|
|
" printf(\" + Partial Order Reduction\\n\");",
|
|
"#endif",
|
|
#if 0
|
|
"#ifdef Q_PROVISO",
|
|
" printf(\" + Queue Proviso\\n\");",
|
|
"#endif",
|
|
#endif
|
|
"#ifdef COLLAPSE",
|
|
" printf(\" + Compression\\n\");",
|
|
"#endif",
|
|
"#ifdef MA",
|
|
" printf(\" + Graph Encoding (-DMA=%%d)\\n\", MA);",
|
|
"#ifdef R_XPT",
|
|
" printf(\" Restarted from checkpoint %%s.xpt\\n\", Source);",
|
|
"#endif",
|
|
"#endif",
|
|
"#ifdef CHECK",
|
|
"#ifdef FULLSTACK",
|
|
" printf(\" + FullStack Matching\\n\");",
|
|
"#endif",
|
|
"#ifdef CNTRSTACK",
|
|
" printf(\" + CntrStack Matching\\n\");",
|
|
"#endif",
|
|
"#endif",
|
|
"#ifdef BITSTATE",
|
|
" printf(\"\\nBit statespace search for:\\n\");",
|
|
"#else",
|
|
"#ifdef HC",
|
|
" printf(\"\\nHash-Compact %%d search for:\\n\", HC);",
|
|
"#else",
|
|
" printf(\"\\nFull statespace search for:\\n\");",
|
|
"#endif",
|
|
"#endif",
|
|
"#ifdef EVENT_TRACE",
|
|
"#ifdef NEGATED_TRACE",
|
|
" printf(\"\tnotrace assertion \t+\\n\");",
|
|
"#else",
|
|
" printf(\"\ttrace assertion \t+\\n\");",
|
|
"#endif",
|
|
"#endif",
|
|
"#ifdef VERI",
|
|
" printf(\"\tnever claim \t+\\n\");",
|
|
" printf(\"\tassertion violations\t\");",
|
|
" if (noasserts)",
|
|
" printf(\"- (disabled by -A flag)\\n\");",
|
|
" else",
|
|
" printf(\"+ (if within scope of claim)\\n\");",
|
|
"#else",
|
|
"#ifdef NOCLAIM",
|
|
" printf(\"\tnever claim \t- (not selected)\\n\");",
|
|
"#else",
|
|
" printf(\"\tnever claim \t- (none specified)\\n\");",
|
|
"#endif",
|
|
" printf(\"\tassertion violations\t\");",
|
|
" if (noasserts)",
|
|
" printf(\"- (disabled by -A flag)\\n\");",
|
|
" else",
|
|
" printf(\"+\\n\");",
|
|
"#endif",
|
|
"#ifndef SAFETY",
|
|
"#ifdef NP",
|
|
" printf(\"\tnon-progress cycles \t\");",
|
|
"#else",
|
|
" printf(\"\tacceptance cycles \t\");",
|
|
"#endif",
|
|
" if (a_cycles)",
|
|
" printf(\"+ (fairness %%sabled)\\n\",",
|
|
" fairness?\"en\":\"dis\");",
|
|
" else printf(\"- (not selected)\\n\");",
|
|
"#else",
|
|
" printf(\"\tcycle checks \t- (disabled by -DSAFETY)\\n\");",
|
|
"#endif",
|
|
"#ifdef VERI",
|
|
" printf(\"\tinvalid end states\t- \");",
|
|
" printf(\"(disabled by \");",
|
|
" if (noends)",
|
|
" printf(\"-E flag)\\n\\n\");",
|
|
" else",
|
|
" printf(\"never claim)\\n\\n\");",
|
|
"#else",
|
|
" printf(\"\tinvalid end states\t\");",
|
|
" if (noends)",
|
|
" printf(\"- (disabled by -E flag)\\n\\n\");",
|
|
" else",
|
|
" printf(\"+\\n\\n\");",
|
|
"#endif",
|
|
" printf(\"State-vector %%d byte, depth reached %%d\", ",
|
|
" hmax, mreached);",
|
|
" printf(\", errors: %%d\\n\", errors);",
|
|
"#ifdef MA",
|
|
" if (done)",
|
|
" { extern void dfa_stats(void);",
|
|
" if (maxgs+a_cycles+2 < MA)",
|
|
" printf(\"MA stats: -DMA=%%d is sufficient\\n\",",
|
|
" maxgs+a_cycles+2);",
|
|
" dfa_stats();",
|
|
" }",
|
|
"#endif",
|
|
" wrap_stats();",
|
|
"#ifdef CHECK",
|
|
" printf(\"stackframes: %%d/%%d\\n\\n\", smax, svmax);",
|
|
" printf(\"stats: fa %%d, fh %%d, zh %%d, zn %%d - \",",
|
|
" Fa, Fh, Zh, Zn);",
|
|
" printf(\"check %%d holds %%d\\n\", Ccheck, Cholds);",
|
|
" printf(\"stack stats: puts %%d, probes %%d, zaps %%d\\n\",",
|
|
" PUT, PROBE, ZAPS);",
|
|
"#else",
|
|
" printf(\"\\n\");",
|
|
"#endif",
|
|
"",
|
|
"#if defined(BITSTATE) || !defined(NOCOMP)",
|
|
" nr1 = (nstates-nShadow)*",
|
|
" (double)(hmax+sizeof(struct H_el)-sizeof(unsigned));",
|
|
"#ifdef BFS",
|
|
" nr2 = 0.0;",
|
|
"#else",
|
|
" nr2 = (double) ((maxdepth+3)*sizeof(Trail));",
|
|
"#endif",
|
|
|
|
"#ifndef BITSTATE",
|
|
"#if !defined(MA) || defined(COLLAPSE)",
|
|
" nr3 = (double) (1L<<ssize)*sizeof(struct H_el *);",
|
|
"#endif",
|
|
"#else",
|
|
#ifndef POWOW
|
|
" if (udmem)",
|
|
" nr3 = (double) (udmem);",
|
|
" else",
|
|
#endif
|
|
" nr3 = (double) (1L<<(ssize-3));",
|
|
"#ifdef CNTRSTACK",
|
|
" nr3 += (double) (1L<<(ssize-3));",
|
|
"#endif",
|
|
"#ifdef FULLSTACK",
|
|
" nr5 = (double) (maxdepth*sizeof(struct H_el *));",
|
|
"#endif",
|
|
"#endif",
|
|
" nr4 = (double) (svmax * (sizeof(Svtack) + hmax))",
|
|
" + (double) (smax * (sizeof(Stack) + Maxbody));",
|
|
"#ifndef MA",
|
|
" if (mverbose || memcnt < nr1+nr2+nr3+nr4+nr5)",
|
|
"#endif",
|
|
" { double remainder = memcnt;",
|
|
" double tmp_nr = memcnt-nr3-nr4-(nr2-fragment)-nr5;",
|
|
" if (tmp_nr < 0.0) tmp_nr = 0.;",
|
|
" printf(\"Stats on memory usage (in Megabytes):\\n\");",
|
|
" printf(\"%%-6.3f\tequivalent memory usage for states\",",
|
|
" nr1/1000000.);",
|
|
" printf(\" (stored*(State-vector + overhead))\\n\");",
|
|
"#ifdef BITSTATE",
|
|
#ifndef POWOW
|
|
" if (udmem)",
|
|
" printf(\"%%-6.3f\tmemory used for hash array (-M%%ld)\\n\",",
|
|
" nr3/1000000., udmem/(1024L*1024L));",
|
|
" else",
|
|
#endif
|
|
" printf(\"%%-6.3f\tmemory used for hash array (-w%%d)\\n\",",
|
|
" nr3/1000000., ssize);",
|
|
" if (nr5 > 0.0)",
|
|
" printf(\"%%-6.3f\tmemory used for bit stack\\n\",",
|
|
" nr5/1000000.);",
|
|
" remainder = remainder - nr3 - nr5;",
|
|
"#else",
|
|
" printf(\"%%-6.3f\tactual memory usage for states\",",
|
|
" tmp_nr/1000000.);",
|
|
" remainder = remainder - tmp_nr;",
|
|
" printf(\" (\");",
|
|
" if (tmp_nr > 0.)",
|
|
" { if (tmp_nr > nr1) printf(\"unsuccessful \");",
|
|
" printf(\"compression: %%.2f%%%%)\\n\",",
|
|
" (100.0*tmp_nr)/nr1);",
|
|
" } else",
|
|
" printf(\"less than 1k)\\n\");",
|
|
"#ifndef MA",
|
|
" if (tmp_nr > 0.)",
|
|
" { printf(\"\tState-vector as stored = %%.0f byte\",",
|
|
" (tmp_nr)/(nstates-nShadow) -",
|
|
" (double) (sizeof(struct H_el) - sizeof(unsigned)));",
|
|
" printf(\" + %%ld byte overhead\\n\",",
|
|
" sizeof(struct H_el)-sizeof(unsigned));",
|
|
" }",
|
|
"#endif",
|
|
"#if !defined(MA) || defined(COLLAPSE)",
|
|
" printf(\"%%-6.3f\tmemory used for hash table (-w%%d)\\n\",",
|
|
" nr3/1000000., ssize);",
|
|
" remainder = remainder - nr3;",
|
|
"#endif",
|
|
"#endif",
|
|
"#ifndef BFS",
|
|
" printf(\"%%-6.3f\tmemory used for DFS stack (-m%%ld)\\n\",",
|
|
" nr2/1000000., maxdepth);",
|
|
" remainder = remainder - nr2;",
|
|
"#endif",
|
|
" if (remainder - fragment > 0.0)",
|
|
" printf(\"%%-6.3f\tother (proc and chan stacks)\\n\",",
|
|
" (remainder-fragment)/1000000.);",
|
|
" if (fragment > 0.0)",
|
|
" printf(\"%%-6.3f\tmemory lost to fragmentation\\n\",",
|
|
" fragment/1000000.);",
|
|
" printf(\"%%-6.3f\ttotal actual memory usage\\n\\n\",",
|
|
" memcnt/1000000.);",
|
|
" }",
|
|
"#ifndef MA",
|
|
" else",
|
|
"#endif",
|
|
"#endif",
|
|
"#ifndef MA",
|
|
" printf(\"%%-6.3f\tmemory usage (Mbyte)\\n\\n\",",
|
|
" memcnt/1000000.);",
|
|
"#endif",
|
|
"#ifdef COLLAPSE",
|
|
" printf(\"nr of templates: [ globals chans procs ]\\n\");",
|
|
" printf(\"collapse counts: [ \");",
|
|
" { int i; for (i = 0; i < 256+2; i++)",
|
|
" if (ncomps[i] != 0)",
|
|
" printf(\"%%d \", ncomps[i]);",
|
|
" printf(\"]\\n\");",
|
|
" }",
|
|
"#endif",
|
|
|
|
" if ((done || verbose) && !no_rck) do_reach();",
|
|
"#ifdef PEG",
|
|
" { int i;",
|
|
" printf(\"\\nPeg Counts (transitions executed):\\n\");",
|
|
" for (i = 1; i < NTRANS; i++)",
|
|
" { if (peg[i]) putpeg(i, peg[i]);",
|
|
" } }",
|
|
"#endif",
|
|
"#ifdef VAR_RANGES",
|
|
" dumpranges();",
|
|
"#endif",
|
|
"#ifdef SVDUMP",
|
|
" if (vprefix > 0) close(svfd);",
|
|
"#endif",
|
|
" pan_exit(0);",
|
|
"}\n",
|
|
"void",
|
|
"stopped(int arg)",
|
|
"{ printf(\"Interrupted\\n\");",
|
|
" wrapup();",
|
|
" pan_exit(0);",
|
|
"}",
|
|
"/*",
|
|
" * based on Bob Jenkins hash-function from 1996",
|
|
" * see: http://www.burtleburtle.net/bob/",
|
|
" */",
|
|
"",
|
|
"#if defined(HASH64) || defined(WIN64)",
|
|
/* 64-bit Jenkins hash: http://burtleburtle.net/bob/c/lookup8.c */
|
|
"#define mix(a,b,c) \\",
|
|
"{ a -= b; a -= c; a ^= (c>>43); \\",
|
|
" b -= c; b -= a; b ^= (a<<9); \\",
|
|
" c -= a; c -= b; c ^= (b>>8); \\",
|
|
" a -= b; a -= c; a ^= (c>>38); \\",
|
|
" b -= c; b -= a; b ^= (a<<23); \\",
|
|
" c -= a; c -= b; c ^= (b>>5); \\",
|
|
" a -= b; a -= c; a ^= (c>>35); \\",
|
|
" b -= c; b -= a; b ^= (a<<49); \\",
|
|
" c -= a; c -= b; c ^= (b>>11); \\",
|
|
" a -= b; a -= c; a ^= (c>>12); \\",
|
|
" b -= c; b -= a; b ^= (a<<18); \\",
|
|
" c -= a; c -= b; c ^= (b>>22); \\",
|
|
"}",
|
|
"#else",
|
|
"#define mix(a,b,c) \\",
|
|
"{ a -= b; a -= c; a ^= (c>>13); \\",
|
|
" b -= c; b -= a; b ^= (a<<8); \\",
|
|
" c -= a; c -= b; c ^= (b>>13); \\",
|
|
" a -= b; a -= c; a ^= (c>>12); \\",
|
|
" b -= c; b -= a; b ^= (a<<16); \\",
|
|
" c -= a; c -= b; c ^= (b>>5); \\",
|
|
" a -= b; a -= c; a ^= (c>>3); \\",
|
|
" b -= c; b -= a; b ^= (a<<10); \\",
|
|
" c -= a; c -= b; c ^= (b>>15); \\",
|
|
"}",
|
|
"#endif",
|
|
"void",
|
|
"d_hash(uchar *Cp, int Om) /* double bit hash - Jenkins */",
|
|
"{ unsigned long a = 0x9e3779b9, b, c = 0, len, length;",
|
|
" unsigned long *k = (unsigned long *) Cp;",
|
|
"",
|
|
" length = len = (unsigned long) ((unsigned long) Om + WS-1)/WS;",
|
|
"",
|
|
" b = HASH_CONST[HASH_NR];",
|
|
" while (len >= 3)",
|
|
" { a += k[0];",
|
|
" b += k[1];",
|
|
" c += k[2];",
|
|
" mix(a,b,c);",
|
|
" k += 3; len -= 3;",
|
|
" }",
|
|
" c += length;",
|
|
" switch (len) {",
|
|
" case 2: b += k[1];",
|
|
" case 1: a += k[0];",
|
|
" }",
|
|
" mix(a,b,c);",
|
|
" j1 = c&nmask; j3 = a&7;", /* 1st bit */
|
|
" j2 = b&nmask; j4 = (a>>3)&7;", /* 2nd bit */
|
|
" K1 = c; K2 = b;", /* no nmask */
|
|
"}",
|
|
"void",
|
|
"s_hash(uchar *cp, int om)",
|
|
"{ d_hash(cp, om); /* sets K1 and K2 */",
|
|
"#ifdef BITSTATE",
|
|
" if (S_Tab == H_tab)", /* state stack in bitstate search */
|
|
" j1 = K1 %% omaxdepth;",
|
|
" else",
|
|
"#endif", /* if (S_Tab != H_Tab) */
|
|
" if (ssize < 8*WS)",
|
|
" j1 = K1&mask;",
|
|
" else",
|
|
" j1 = K1;",
|
|
"}",
|
|
"#ifndef RANDSTOR",
|
|
"int *prerand;",
|
|
"void",
|
|
"inirand(void)",
|
|
"{ int i;",
|
|
" srand(123); /* fixed startpoint */",
|
|
" prerand = (int *) emalloc((omaxdepth+3)*sizeof(int));",
|
|
" for (i = 0; i < omaxdepth+3; i++)",
|
|
" prerand[i] = rand();",
|
|
"}",
|
|
"int",
|
|
"pan_rand(void)",
|
|
"{ if (!prerand) inirand();",
|
|
" return prerand[depth];",
|
|
"}",
|
|
"#endif",
|
|
"",
|
|
"int",
|
|
"main(int argc, char *argv[])",
|
|
"{ void to_compile(void);\n",
|
|
" efd = stderr; /* default */",
|
|
"#ifdef BITSTATE",
|
|
" bstore = bstore_reg; /* default */",
|
|
"#endif",
|
|
" while (argc > 1 && argv[1][0] == '-')",
|
|
" { switch (argv[1][1]) {",
|
|
"#ifndef SAFETY",
|
|
"#ifdef NP",
|
|
" case 'a': fprintf(efd, \"error: -a disabled\");",
|
|
" usage(efd); break;",
|
|
"#else",
|
|
" case 'a': a_cycles = 1; break;",
|
|
"#endif",
|
|
"#endif",
|
|
" case 'A': noasserts = 1; break;",
|
|
" case 'b': bounded = 1; break;",
|
|
" case 'c': upto = atoi(&argv[1][2]); break;",
|
|
" case 'd': state_tables++; break;",
|
|
" case 'e': every_error = 1; Nr_Trails = 1; break;",
|
|
" case 'E': noends = 1; break;",
|
|
"#ifdef SC",
|
|
" case 'F': if (strlen(argv[1]) > 2)",
|
|
" stackfile = &argv[1][2];",
|
|
" break;",
|
|
"#endif",
|
|
"#if !defined(SAFETY) && !defined(NOFAIR)",
|
|
" case 'f': fairness = 1; break;",
|
|
"#endif",
|
|
" case 'h': if (!argv[1][2]) usage(efd); else",
|
|
" HASH_NR = atoi(&argv[1][2])%%33; break;",
|
|
" case 'I': iterative = 2; every_error = 1; break;",
|
|
" case 'i': iterative = 1; every_error = 1; break;",
|
|
" case 'J': like_java = 1; break; /* Klaus Havelund */",
|
|
"#ifdef BITSTATE",
|
|
" case 'k': hfns = atoi(&argv[1][2]); break;",
|
|
"#endif",
|
|
"#ifndef SAFETY",
|
|
"#ifdef NP",
|
|
" case 'l': a_cycles = 1; break;",
|
|
"#else",
|
|
" case 'l': fprintf(efd, \"error: -l disabled\");",
|
|
" usage(efd); break;",
|
|
"#endif",
|
|
"#endif",
|
|
#ifndef POWOW
|
|
"#ifdef BITSTATE",
|
|
" case 'M': udmem = atoi(&argv[1][2]); break;",
|
|
" case 'G': udmem = atoi(&argv[1][2]); udmem *= 1024; break;",
|
|
"#else",
|
|
" case 'M': case 'G':",
|
|
" fprintf(stderr, \"-M and -G affect only -DBITSTATE\\n\");",
|
|
" break;",
|
|
"#endif",
|
|
#endif
|
|
" case 'm': maxdepth = atoi(&argv[1][2]); break;",
|
|
" case 'n': no_rck = 1; break;",
|
|
"#ifdef SVDUMP",
|
|
" case 'p': vprefix = atoi(&argv[1][2]); break;",
|
|
"#endif",
|
|
" case 'q': strict = 1; break;",
|
|
"#ifdef HAS_CODE",
|
|
" case 'r':",
|
|
"samething: readtrail = 1;",
|
|
" if (isdigit(argv[1][2]))",
|
|
" whichtrail = atoi(&argv[1][2]);",
|
|
" break;",
|
|
" case 'P': readtrail = 1; onlyproc = atoi(&argv[1][2]); break;",
|
|
" case 'C': coltrace = 1; goto samething;",
|
|
" case 'g': gui = 1; goto samething;",
|
|
" case 'S': silent = 1; break;",
|
|
"#endif",
|
|
" case 'R': Nrun = atoi(&argv[1][2]); break;",
|
|
"#ifdef BITSTATE",
|
|
" case 's': hfns = 1; break;",
|
|
"#endif",
|
|
" case 'T': TMODE = 0444; break;",
|
|
" case 't': if (argv[1][2]) tprefix = &argv[1][2]; break;",
|
|
" case 'V': printf(\"Generated by %%s\\n\", Version);",
|
|
" to_compile(); pan_exit(0); break;",
|
|
" case 'v': verbose = 1; break;",
|
|
" case 'w': ssize = atoi(&argv[1][2]); break;",
|
|
" case 'Y': signoff = 1; break;",
|
|
" case 'X': efd = stdout; break;",
|
|
" default : fprintf(efd, \"saw option -%%c\\n\", argv[1][1]); usage(efd); break;",
|
|
" }",
|
|
" argc--; argv++;",
|
|
" }",
|
|
" if (iterative && TMODE != 0666)",
|
|
" { TMODE = 0666;",
|
|
" fprintf(efd, \"warning: -T ignored when -i or -I is used\\n\");",
|
|
" }",
|
|
"#if defined(WIN32) || defined(WIN64)",
|
|
" if (TMODE == 0666)",
|
|
" TMODE = _S_IWRITE | _S_IREAD;",
|
|
" else",
|
|
" TMODE = _S_IREAD;",
|
|
"#endif",
|
|
"#ifdef OHASH",
|
|
" fprintf(efd, \"warning: -DOHASH no longer supported (directive ignored)\\n\");",
|
|
"#endif",
|
|
"#ifdef JHASH",
|
|
" fprintf(efd, \"warning: -DJHASH no longer supported (directive ignored)\\n\");",
|
|
"#endif",
|
|
"#ifdef HYBRID_HASH",
|
|
" fprintf(efd, \"warning: -DHYBRID_HASH no longer supported (directive ignored)\\n\");",
|
|
"#endif",
|
|
"#ifdef NOCOVEST",
|
|
" fprintf(efd, \"warning: -DNOCOVEST no longer supported (directive ignored)\\n\");",
|
|
"#endif",
|
|
"#ifdef BITSTATE",
|
|
"#ifdef BCOMP",
|
|
" fprintf(efd, \"warning: -DBCOMP no longer supported (directive ignored)\\n\");",
|
|
"#endif",
|
|
" if (hfns <= 0)",
|
|
" { hfns = 1;",
|
|
" fprintf(efd, \"warning: using -k%%d as minimal usable value\\n\", hfns);",
|
|
" }",
|
|
"#endif",
|
|
" omaxdepth = maxdepth;",
|
|
"#ifdef BITSTATE",
|
|
" if (WS == 4 && ssize > 34)", /* 32-bit word size */
|
|
" { ssize = 34;",
|
|
" fprintf(efd, \"warning: using -w%%d as max usable value\\n\", ssize);",
|
|
"/*",
|
|
" * -w35 would not work: 35-3 = 32 but 1^31 is the largest",
|
|
" * power of 2 that can be represented in an unsigned long",
|
|
" */",
|
|
" }",
|
|
"#else",
|
|
" if (WS == 4 && ssize > 27)",
|
|
" { ssize = 27;",
|
|
" fprintf(efd, \"warning: using -w%%d as max usable value\\n\", ssize);",
|
|
"/*",
|
|
" * for emalloc, the lookup table size multiplies by 4 for the pointers",
|
|
" * the largest power of 2 that can be represented in a ulong is 1^31",
|
|
" * hence the largest number of lookup table slots is 31-4 = 27",
|
|
" */",
|
|
" }",
|
|
|
|
"#endif",
|
|
"#ifdef SC",
|
|
" hiwater = HHH = maxdepth-10;",
|
|
" DDD = HHH/2;",
|
|
" if (!stackfile)",
|
|
" { stackfile = (char *) emalloc(strlen(Source)+4+1);",
|
|
" sprintf(stackfile, \"%%s._s_\", Source);",
|
|
" }",
|
|
" if (iterative)",
|
|
" { fprintf(efd, \"error: cannot use -i or -I with -DSC\\n\");",
|
|
" pan_exit(1);",
|
|
" }",
|
|
"#endif",
|
|
|
|
"#if (defined(R_XPT) || defined(W_XPT)) && !defined(MA)",
|
|
" fprintf(efd, \"error: -D?_XPT requires -DMA\\n\");",
|
|
" exit(1);",
|
|
"#endif",
|
|
|
|
" if (iterative && a_cycles)",
|
|
" fprintf(efd, \"warning: -i or -I work for safety properties only\\n\");",
|
|
|
|
"#ifdef BFS",
|
|
"#if defined(SC)",
|
|
" fprintf(efd, \"error: -DBFS not compatible with -DSC\\n\");",
|
|
" exit(1);",
|
|
"#endif",
|
|
"#if defined(HAS_LAST)",
|
|
" fprintf(efd, \"error: -DBFS not compatible with _last\\n\");",
|
|
" exit(1);",
|
|
"#endif",
|
|
"#if defined(REACH)",
|
|
" fprintf(efd, \"warning: -DREACH redundant when -DBFS is used\\n\");",
|
|
"#endif",
|
|
"#if defined(HAS_STACK)",
|
|
" fprintf(efd, \"error: cannot use UnMatched qualifier on c_track with BFS\\n\");",
|
|
" exit(1);",
|
|
"#endif",
|
|
"#endif",
|
|
|
|
"#if defined(MERGED) && defined(PEG)",
|
|
" fprintf(efd, \"error: to allow -DPEG use: spin -o3 -a %%s\\n\", Source);",
|
|
" fprintf(efd, \" to turn off transition merge optimization\\n\");",
|
|
" pan_exit(1);",
|
|
"#endif",
|
|
"#ifdef HC",
|
|
"#ifdef NOCOMP",
|
|
" fprintf(efd, \"error: cannot combine -DHC and -DNOCOMP\\n\");",
|
|
" pan_exit(1);",
|
|
"#endif",
|
|
"#ifdef BITSTATE",
|
|
" fprintf(efd, \"error: cannot combine -DHC and -DBITSTATE\\n\");",
|
|
" pan_exit(1);",
|
|
"#endif",
|
|
"#endif",
|
|
"#if defined(SAFETY) && defined(NP)",
|
|
" fprintf(efd, \"error: cannot combine -DNP and -DSAFETY\\n\");",
|
|
" pan_exit(1);",
|
|
"#endif",
|
|
"#ifdef MA",
|
|
"#ifdef BITSTATE",
|
|
" fprintf(efd, \"error: cannot combine -DMA and -DBITSTATE\\n\");",
|
|
" pan_exit(1);",
|
|
"#endif",
|
|
" if (MA <= 0)",
|
|
" { fprintf(efd, \"usage: -DMA=N with N > 0 and < VECTORSZ\\n\");",
|
|
" pan_exit(1);",
|
|
" }",
|
|
"#endif",
|
|
"#ifdef COLLAPSE",
|
|
"#if defined(BITSTATE)",
|
|
" fprintf(efd, \"error: cannot combine -DBITSTATE and -DCOLLAPSE\\n\");",
|
|
" pan_exit(1);",
|
|
"#endif",
|
|
"#if defined(NOCOMP)",
|
|
" fprintf(efd, \"error: cannot combine -DNOCOMP and -DCOLLAPSE\\n\");",
|
|
" pan_exit(1);",
|
|
"#endif",
|
|
"#endif",
|
|
" if (maxdepth <= 0 || ssize <= 1) usage(efd);",
|
|
"#if SYNC>0 && !defined(NOREDUCE)",
|
|
" if (a_cycles && fairness)",
|
|
" { fprintf(efd, \"error: p.o. reduction not compatible with \");",
|
|
" fprintf(efd, \"fairness (-f) in models\\n\");",
|
|
" fprintf(efd, \" with rendezvous operations: \");",
|
|
" fprintf(efd, \"recompile with -DNOREDUCE\\n\");",
|
|
" pan_exit(1);",
|
|
" }",
|
|
"#endif",
|
|
"#if defined(REM_VARS) && !defined(NOREDUCE)",
|
|
" { fprintf(efd, \"warning: p.o. reduction not compatible with \");",
|
|
" fprintf(efd, \"remote varrefs (use -DNOREDUCE)\\n\");",
|
|
" }",
|
|
"#endif",
|
|
"#if defined(NOCOMP) && !defined(BITSTATE)",
|
|
" if (a_cycles)",
|
|
" { fprintf(efd, \"error: -DNOCOMP voids -l and -a\\n\");",
|
|
" pan_exit(1);",
|
|
" }",
|
|
"#endif",
|
|
|
|
"#ifdef MEMLIM", /* MEMLIM setting takes precedence */
|
|
" memlim = (double) MEMLIM * (double) (1<<20); /* size in Mbyte */",
|
|
"#else",
|
|
"#ifdef MEMCNT",
|
|
"#if MEMCNT<31",
|
|
" memlim = (double) (1<<MEMCNT);",
|
|
"#else",
|
|
" memlim = (double) (1<<30);",
|
|
" memlim *= (double) (1<<(MEMCNT-30));",
|
|
"#endif",
|
|
"#endif",
|
|
"#endif",
|
|
|
|
"#ifndef BITSTATE",
|
|
" if (Nrun > 1) HASH_NR = Nrun - 1;",
|
|
"#endif",
|
|
" if (Nrun < 1 || Nrun > 32)",
|
|
" { fprintf(efd, \"error: invalid arg for -R\\n\");",
|
|
" usage(efd);",
|
|
" }",
|
|
"#ifndef SAFETY",
|
|
" if (fairness && !a_cycles)",
|
|
" { fprintf(efd, \"error: -f requires -a or -l\\n\");",
|
|
" usage(efd);",
|
|
" }",
|
|
"#if ACCEPT_LAB==0",
|
|
" if (a_cycles)",
|
|
"#ifndef VERI",
|
|
" { fprintf(efd, \"error: no accept labels defined \");",
|
|
" fprintf(efd, \"in model (for option -a)\\n\");",
|
|
" usage(efd);",
|
|
" }",
|
|
"#else",
|
|
" { fprintf(efd, \"warning: no explicit accept labels \");",
|
|
" fprintf(efd, \"defined in model (for -a)\\n\");",
|
|
" }",
|
|
"#endif",
|
|
"#endif",
|
|
"#endif",
|
|
"#if !defined(NOREDUCE)",
|
|
"#if defined(HAS_ENABLED)",
|
|
" fprintf(efd, \"error: reduced search precludes \");",
|
|
" fprintf(efd, \"use of 'enabled()'\\n\");",
|
|
" pan_exit(1);",
|
|
"#endif",
|
|
"#if defined(HAS_PCVALUE)",
|
|
" fprintf(efd, \"error: reduced search precludes \");",
|
|
" fprintf(efd, \"use of 'pcvalue()'\\n\");",
|
|
" pan_exit(1);",
|
|
"#endif",
|
|
"#if defined(HAS_BADELSE)",
|
|
" fprintf(efd, \"error: reduced search precludes \");",
|
|
" fprintf(efd, \"using 'else' combined with i/o stmnts\\n\");",
|
|
" pan_exit(1);",
|
|
"#endif",
|
|
"#if defined(HAS_LAST)",
|
|
" fprintf(efd, \"error: reduced search precludes \");",
|
|
" fprintf(efd, \"use of _last\\n\");",
|
|
" pan_exit(1);",
|
|
"#endif",
|
|
"#endif",
|
|
|
|
"#if SYNC>0 && !defined(NOREDUCE)",
|
|
"#ifdef HAS_UNLESS",
|
|
" fprintf(efd, \"warning: use of a rendezvous stmnts in the escape\\n\");",
|
|
" fprintf(efd, \"\tof an unless clause, if present, could make p.o. reduction\\n\");",
|
|
" fprintf(efd, \"\tinvalid (use -DNOREDUCE to avoid this)\\n\");",
|
|
"#ifdef BFS",
|
|
" fprintf(efd, \"\t(this type of rv is also not compatible with -DBFS)\\n\");",
|
|
"#endif",
|
|
"#endif",
|
|
"#endif",
|
|
"#if SYNC>0 && defined(BFS)",
|
|
" fprintf(efd, \"warning: use of rendezvous in BFS mode \");",
|
|
" fprintf(efd, \"does not preserve all invalid endstates\\n\");",
|
|
"#endif",
|
|
"#if !defined(REACH) && !defined(BITSTATE)",
|
|
" if (iterative != 0 && a_cycles == 0)",
|
|
" fprintf(efd, \"warning: -i and -I need -DREACH to work accurately\\n\");",
|
|
"#endif",
|
|
"#if defined(BITSTATE) && defined(REACH)",
|
|
" fprintf(efd, \"warning: -DREACH voided by -DBITSTATE\\n\");",
|
|
"#endif",
|
|
"#if defined(MA) && defined(REACH)",
|
|
" fprintf(efd, \"warning: -DREACH voided by -DMA\\n\");",
|
|
"#endif",
|
|
"#if defined(FULLSTACK) && defined(CNTRSTACK)",
|
|
" fprintf(efd, \"error: cannot combine\");",
|
|
" fprintf(efd, \" -DFULLSTACK and -DCNTRSTACK\\n\");",
|
|
" pan_exit(1);",
|
|
"#endif",
|
|
"#if defined(VERI)",
|
|
"#if ACCEPT_LAB>0",
|
|
"#ifndef BFS",
|
|
" if (!a_cycles",
|
|
"#ifdef HAS_CODE",
|
|
" && !readtrail",
|
|
"#endif",
|
|
" && !state_tables)",
|
|
" { fprintf(efd, \"warning: never claim + accept labels \");",
|
|
" fprintf(efd, \"requires -a flag to fully verify\\n\");",
|
|
" }",
|
|
"#else",
|
|
" if (",
|
|
"#ifdef HAS_CODE",
|
|
" !readtrail",
|
|
"#endif",
|
|
" && !state_tables)",
|
|
" { fprintf(efd, \"warning: verification in BFS mode \");",
|
|
" fprintf(efd, \"is restricted to safety properties\\n\");",
|
|
" }",
|
|
"#endif",
|
|
"#endif",
|
|
"#endif",
|
|
"#ifndef SAFETY",
|
|
" if (!a_cycles",
|
|
"#ifdef HAS_CODE",
|
|
" && !readtrail",
|
|
"#endif",
|
|
" && !state_tables)",
|
|
" { fprintf(efd, \"hint: this search is more efficient \");",
|
|
" fprintf(efd, \"if pan.c is compiled -DSAFETY\\n\");",
|
|
" }",
|
|
"#ifndef NOCOMP",
|
|
" if (!a_cycles)",
|
|
" S_A = 0;",
|
|
" else",
|
|
" { if (!fairness)",
|
|
" S_A = 1; /* _a_t */",
|
|
"#ifndef NOFAIR",
|
|
" else /* _a_t and _cnt[NFAIR] */",
|
|
" S_A = (&(now._cnt[0]) - (uchar *) &now) + NFAIR - 2;",
|
|
" /* -2 because first two uchars in now are masked */",
|
|
"#endif",
|
|
" }",
|
|
"#endif",
|
|
"#endif",
|
|
" signal(SIGINT, stopped);",
|
|
|
|
/******************* 4.2.5 ********************/
|
|
" if (WS == 4 && ssize >= 32)",
|
|
" { mask = 0xffffffff;",
|
|
"#ifdef BITSTATE",
|
|
" switch (ssize) {",
|
|
" case 34: nmask = (mask>>1); break;",
|
|
" case 33: nmask = (mask>>2); break;",
|
|
" default: nmask = (mask>>3); break;",
|
|
" }",
|
|
"#else",
|
|
" nmask = mask;",
|
|
"#endif",
|
|
" } else if (WS == 8)",
|
|
" { mask = ((1L<<ssize)-1); /* hash init */",
|
|
"#ifdef BITSTATE",
|
|
" nmask = mask>>3;",
|
|
"#else",
|
|
" nmask = mask;",
|
|
"#endif",
|
|
" } else if (WS != 4)",
|
|
" { fprintf(stderr, \"pan: wordsize %%ld not supported\\n\", WS);",
|
|
" exit(1);",
|
|
" } else /* WS == 4 and ssize < 32 */",
|
|
" { mask = ((1L<<ssize)-1); /* hash init */",
|
|
" nmask = (mask>>3);",
|
|
" }",
|
|
/****************** end **********************/
|
|
|
|
"#ifdef BFS",
|
|
" trail = (Trail *) emalloc(6*sizeof(Trail));",
|
|
" trail += 3;",
|
|
"#else",
|
|
" trail = (Trail *) emalloc((maxdepth+3)*sizeof(Trail));",
|
|
" trail++; /* protect trpt-1 refs at depth 0 */",
|
|
"#endif",
|
|
"#ifdef SVDUMP",
|
|
" if (vprefix > 0)",
|
|
" { char nm[64];",
|
|
" sprintf(nm, \"%%s.svd\", Source);",
|
|
" if ((svfd = creat(nm, 0666)) < 0)",
|
|
" { fprintf(efd, \"couldn't create %%s\\n\", nm);",
|
|
" vprefix = 0;",
|
|
" } }",
|
|
"#endif",
|
|
"#ifdef RANDSTOR",
|
|
" srand(123);",
|
|
"#endif",
|
|
"#if SYNC>0 && ASYNC==0",
|
|
" set_recvs();",
|
|
"#endif",
|
|
" run();",
|
|
" done = 1;",
|
|
" wrapup();",
|
|
" return 0;",
|
|
"}", /* end of main() */
|
|
"",
|
|
"void",
|
|
"usage(FILE *fd)",
|
|
"{",
|
|
" fprintf(fd, \"Valid Options are:\\n\");",
|
|
"#ifndef SAFETY",
|
|
"#ifdef NP",
|
|
" fprintf(fd, \"\t-a -> is disabled by -DNP \");",
|
|
" fprintf(fd, \"(-DNP compiles for -l only)\\n\");",
|
|
"#else",
|
|
" fprintf(fd, \"\t-a find acceptance cycles\\n\");",
|
|
"#endif",
|
|
"#else",
|
|
" fprintf(fd, \"\t-a,-l,-f -> are disabled by -DSAFETY\\n\");",
|
|
"#endif",
|
|
" fprintf(fd, \"\t-A ignore assert() violations\\n\");",
|
|
" fprintf(fd, \"\t-b consider it an error to exceed the depth-limit\\n\");",
|
|
" fprintf(fd, \"\t-cN stop at Nth error \");",
|
|
" fprintf(fd, \"(defaults to -c1)\\n\");",
|
|
" fprintf(fd, \"\t-d print state tables and stop\\n\");",
|
|
" fprintf(fd, \"\t-e create trails for all errors\\n\");",
|
|
" fprintf(fd, \"\t-E ignore invalid end states\\n\");",
|
|
"#ifdef SC",
|
|
" fprintf(fd, \"\t-Ffile use 'file' to store disk-stack\\n\");",
|
|
"#endif",
|
|
"#ifndef NOFAIR",
|
|
" fprintf(fd, \"\t-f add weak fairness (to -a or -l)\\n\");",
|
|
"#endif",
|
|
" fprintf(fd, \"\t-hN use different hash-seed N:1..32\\n\");",
|
|
" fprintf(fd, \"\t-i search for shortest path to error\\n\");",
|
|
" fprintf(fd, \"\t-I like -i, but approximate and faster\\n\");",
|
|
" fprintf(fd, \"\t-J reverse eval order of nested unlesses\\n\");",
|
|
"#ifdef BITSTATE",
|
|
" fprintf(fd, \"\t-kN set N bits per state (defaults to 3)\\n\");",
|
|
"#endif",
|
|
"#ifndef SAFETY",
|
|
"#ifdef NP",
|
|
" fprintf(fd, \"\t-l find non-progress cycles\\n\");",
|
|
"#else",
|
|
" fprintf(fd, \"\t-l find non-progress cycles -> \");",
|
|
" fprintf(fd, \"disabled, requires \");",
|
|
" fprintf(fd, \"compilation with -DNP\\n\");",
|
|
"#endif",
|
|
"#endif",
|
|
#ifndef POWOW
|
|
"#ifdef BITSTATE",
|
|
" fprintf(fd, \"\t-MN use N Megabytes for bitstate hash array\\n\");",
|
|
" fprintf(fd, \"\t-GN use N Gigabytes for bitstate hash array\\n\");",
|
|
"#endif",
|
|
#endif
|
|
" fprintf(fd, \"\t-mN max depth N steps (default=10k)\\n\");",
|
|
" fprintf(fd, \"\t-n no listing of unreached states\\n\");",
|
|
"#ifdef SVDUMP",
|
|
" fprintf(fd, \"\t-pN create svfile (save N bytes per state)\\n\");",
|
|
"#endif",
|
|
" fprintf(fd, \"\t-q require empty chans in valid end states\\n\");",
|
|
"#ifdef HAS_CODE",
|
|
" fprintf(fd, \"\t-r read and execute trail - can add -v,-n,-PN,-g,-C\\n\");",
|
|
" fprintf(fd, \"\t-rN read and execute N-th error trail\\n\");",
|
|
" fprintf(fd, \"\t-C read and execute trail - columnated output (can add -v,-n)\\n\");",
|
|
" fprintf(fd, \"\t-PN read and execute trail - restrict trail output to proc N\\n\");",
|
|
" fprintf(fd, \"\t-g read and execute trail + msc gui support\\n\");",
|
|
" fprintf(fd, \"\t-S silent replay: only user defined printfs show\\n\");",
|
|
"#endif",
|
|
"#ifdef BITSTATE",
|
|
" fprintf(fd, \"\t-RN repeat run Nx with N \");",
|
|
" fprintf(fd, \"[1..32] independent hash functions\\n\");",
|
|
" fprintf(fd, \"\t-s same as -k1 (single bit per state)\\n\");",
|
|
"#endif",
|
|
" fprintf(fd, \"\t-T create trail files in read-only mode\\n\");",
|
|
" fprintf(fd, \"\t-tsuf replace .trail with .suf on trailfiles\\n\");",
|
|
" fprintf(fd, \"\t-V print SPIN version number\\n\");",
|
|
" fprintf(fd, \"\t-v verbose -- filenames in unreached state listing\\n\");",
|
|
" fprintf(fd, \"\t-wN hashtable of 2^N entries \");",
|
|
" fprintf(fd, \"(defaults to -w%%d)\\n\", ssize);",
|
|
" exit(1);",
|
|
"}",
|
|
"",
|
|
"char *",
|
|
"Malloc(unsigned long n)",
|
|
"{ char *tmp;",
|
|
"#if defined(MEMCNT) || defined(MEMLIM)",
|
|
" if (memcnt+ (double) n > memlim) goto err;",
|
|
"#endif",
|
|
"#if 1",
|
|
" tmp = (char *) malloc(n);",
|
|
" if (!tmp)",
|
|
"#else",
|
|
/* on linux machines, a large amount of memory is set aside
|
|
* for malloc, whether it is used or not
|
|
* using sbrk would make this memory arena inaccessible
|
|
* the reason for using sbrk was originally to provide a
|
|
* small additional speedup (since this memory is never released)
|
|
*/
|
|
" tmp = (char *) sbrk(n);",
|
|
" if (tmp == (char *) -1L)",
|
|
"#endif",
|
|
" {",
|
|
"#if defined(MEMCNT) || defined(MEMLIM)",
|
|
"err:",
|
|
"#endif",
|
|
" printf(\"pan: out of memory\\n\");",
|
|
"#if defined(MEMCNT) || defined(MEMLIM)",
|
|
" printf(\"\t%%g bytes used\\n\", memcnt);",
|
|
" printf(\"\t%%g bytes more needed\\n\", (double) n);",
|
|
" printf(\"\t%%g bytes limit\\n\",",
|
|
" memlim);",
|
|
"#endif",
|
|
"#ifdef COLLAPSE",
|
|
" printf(\"hint: to reduce memory, recompile with\\n\");",
|
|
"#ifndef MA",
|
|
" printf(\" -DMA=%%d # better/slower compression, or\\n\", hmax);",
|
|
"#endif",
|
|
" printf(\" -DBITSTATE # supertrace, approximation\\n\");",
|
|
"#else",
|
|
"#ifndef BITSTATE",
|
|
" printf(\"hint: to reduce memory, recompile with\\n\");",
|
|
"#ifndef HC",
|
|
" printf(\" -DCOLLAPSE # good, fast compression, or\\n\");",
|
|
"#ifndef MA",
|
|
" printf(\" -DMA=%%d # better/slower compression, or\\n\", hmax);",
|
|
"#endif",
|
|
" printf(\" -DHC # hash-compaction, approximation\\n\");",
|
|
"#endif",
|
|
" printf(\" -DBITSTATE # supertrace, approximation\\n\");",
|
|
"#endif",
|
|
"#endif",
|
|
" wrapup();",
|
|
" }",
|
|
" memcnt += (double) n;",
|
|
" return tmp;",
|
|
"}",
|
|
"",
|
|
"#define CHUNK (100*VECTORSZ)",
|
|
"",
|
|
"char *",
|
|
"emalloc(unsigned long n) /* never released or reallocated */",
|
|
"{ char *tmp;",
|
|
" if (n == 0)",
|
|
" return (char *) NULL;",
|
|
" if (n&(sizeof(void *)-1)) /* for proper alignment */",
|
|
" n += sizeof(void *)-(n&(sizeof(void *)-1));",
|
|
" if ((unsigned long) left < n)", /* was: (left < (long)n) */
|
|
" { grow = (n < CHUNK) ? CHUNK : n;",
|
|
#if 1
|
|
" have = Malloc(grow);",
|
|
#else
|
|
" /* gcc's sbrk can give non-aligned result */",
|
|
" grow += sizeof(void *); /* allow realignment */",
|
|
" have = Malloc(grow);",
|
|
" if (((unsigned) have)&(sizeof(void *)-1))",
|
|
" { have += (long) (sizeof(void *) ",
|
|
" - (((unsigned) have)&(sizeof(void *)-1)));",
|
|
" grow -= sizeof(void *);",
|
|
" }",
|
|
#endif
|
|
" fragment += (double) left;",
|
|
" left = grow;",
|
|
" }",
|
|
" tmp = have;",
|
|
" have += (long) n;",
|
|
" left -= (long) n;",
|
|
" memset(tmp, 0, n);",
|
|
" return tmp;",
|
|
"}",
|
|
|
|
"void",
|
|
"Uerror(char *str)",
|
|
"{ /* always fatal */",
|
|
" uerror(str);",
|
|
" wrapup();",
|
|
"}\n",
|
|
"#if defined(MA) && !defined(SAFETY)",
|
|
"int",
|
|
"Unwind(void)",
|
|
"{ Trans *t; uchar ot, _m; int tt; short II;",
|
|
"#ifdef VERBOSE",
|
|
" int i;",
|
|
"#endif",
|
|
" uchar oat = now._a_t;",
|
|
" now._a_t &= ~(1|16|32);",
|
|
" memcpy((char *) &comp_now, (char *) &now, vsize);",
|
|
" now._a_t = oat;",
|
|
"Up:",
|
|
"#ifdef SC",
|
|
" trpt = getframe(depth);",
|
|
"#endif",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"%%d State: \", depth);",
|
|
" for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",",
|
|
" ((char *)&now)[i], Mask[i]?\"*\":\"\");",
|
|
" printf(\"\\n\");",
|
|
"#endif",
|
|
"#ifndef NOFAIR",
|
|
" if (trpt->o_pm&128) /* fairness alg */",
|
|
" { now._cnt[now._a_t&1] = trpt->bup.oval;",
|
|
" depth--;",
|
|
"#ifdef SC",
|
|
" trpt = getframe(depth);",
|
|
"#else",
|
|
" trpt--;",
|
|
"#endif",
|
|
" goto Q999;",
|
|
" }",
|
|
"#endif",
|
|
"#ifdef HAS_LAST",
|
|
"#ifdef VERI",
|
|
" { int d; Trail *trl;",
|
|
" now._last = 0;",
|
|
" for (d = 1; d < depth; d++)",
|
|
" { trl = getframe(depth-d); /* was trl = (trpt-d); */",
|
|
" if (trl->pr != 0)",
|
|
" { now._last = trl->pr - BASE;",
|
|
" break;",
|
|
" } } }",
|
|
"#else",
|
|
" now._last = (depth<1)?0:(trpt-1)->pr;",
|
|
"#endif",
|
|
"#endif",
|
|
"#ifdef EVENT_TRACE",
|
|
" now._event = trpt->o_event;",
|
|
"#endif",
|
|
" if ((now._a_t&1) && depth <= A_depth)",
|
|
" { now._a_t &= ~(1|16|32);",
|
|
" if (fairness) now._a_t |= 2; /* ? */",
|
|
" A_depth = 0;",
|
|
" goto CameFromHere; /* checkcycles() */",
|
|
" }",
|
|
" t = trpt->o_t;",
|
|
" ot = trpt->o_ot; II = trpt->pr;",
|
|
" tt = trpt->o_tt; this = pptr(II);",
|
|
" _m = do_reverse(t, II, trpt->o_m);",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"%%3d: proc %%d \", depth, II);",
|
|
" printf(\"reverses %%d, %%d to %%d,\",",
|
|
" t->forw, tt, t->st);",
|
|
" printf(\" %%s [abit=%%d,adepth=%%d,\", ",
|
|
" t->tp, now._a_t, A_depth);",
|
|
" printf(\"tau=%%d,%%d] <unwind>\\n\", ",
|
|
" trpt->tau, (trpt-1)->tau);",
|
|
"#endif",
|
|
" depth--;",
|
|
"#ifdef SC",
|
|
" trpt = getframe(depth);",
|
|
"#else",
|
|
" trpt--;",
|
|
"#endif",
|
|
" /* reached[ot][t->st] = 1; 3.4.13 */",
|
|
" ((P0 *)this)->_p = tt;",
|
|
"#ifndef NOFAIR",
|
|
" if ((trpt->o_pm&32))",
|
|
" {",
|
|
"#ifdef VERI",
|
|
" if (now._cnt[now._a_t&1] == 0)",
|
|
" now._cnt[now._a_t&1] = 1;",
|
|
"#endif",
|
|
" now._cnt[now._a_t&1] += 1;",
|
|
" }",
|
|
"Q999:",
|
|
" if (trpt->o_pm&8)",
|
|
" { now._a_t &= ~2;",
|
|
" now._cnt[now._a_t&1] = 0;",
|
|
" }",
|
|
" if (trpt->o_pm&16)",
|
|
" now._a_t |= 2;",
|
|
"#endif",
|
|
"CameFromHere:",
|
|
" if (memcmp((char *) &now, (char *) &comp_now, vsize) == 0)",
|
|
" return depth;",
|
|
" if (depth > 0) goto Up;",
|
|
" return 0;",
|
|
"}",
|
|
"#endif",
|
|
"static char unwinding;",
|
|
"void",
|
|
"uerror(char *str)",
|
|
"{ static char laststr[256];",
|
|
" int is_cycle;",
|
|
"",
|
|
" if (unwinding) return; /* 1.4.2 */",
|
|
" if (strncmp(str, laststr, 254))",
|
|
" printf(\"pan: %%s (at depth %%ld)\\n\", str,",
|
|
" (depthfound==-1)?depth:depthfound);",
|
|
" strncpy(laststr, str, 254);",
|
|
" errors++;",
|
|
"#ifdef HAS_CODE",
|
|
" if (readtrail) { wrap_trail(); return; }",
|
|
"#endif",
|
|
" is_cycle = (strstr(str, \" cycle\") != (char *) 0);",
|
|
" if (!is_cycle)",
|
|
" { depth++; trpt++;", /* include failed step */
|
|
" }",
|
|
" if ((every_error != 0)",
|
|
" || errors == upto)",
|
|
" {",
|
|
"#if defined(MA) && !defined(SAFETY)",
|
|
" if (is_cycle)",
|
|
" { int od = depth;",
|
|
" unwinding = 1;",
|
|
" depthfound = Unwind();",
|
|
" unwinding = 0;",
|
|
" depth = od;",
|
|
" }",
|
|
"#endif",
|
|
"#ifdef BFS",
|
|
" if (depth > 1) trpt--;",
|
|
" nuerror(str);",
|
|
" if (depth > 1) trpt++;",
|
|
"#else",
|
|
" putrail();",
|
|
"#endif",
|
|
"#if defined(MA) && !defined(SAFETY)",
|
|
" if (strstr(str, \" cycle\"))",
|
|
" { if (every_error)",
|
|
" printf(\"sorry: MA writes 1 trail max\\n\");",
|
|
" wrapup(); /* no recovery from unwind */",
|
|
" }",
|
|
"#endif",
|
|
" }",
|
|
" if (!is_cycle)",
|
|
" { depth--; trpt--; /* undo */",
|
|
" }",
|
|
"#ifndef BFS",
|
|
" if (iterative != 0 && maxdepth > 0)",
|
|
" { maxdepth = (iterative == 1)?(depth-1):(depth/2);",
|
|
" warned = 1;",
|
|
" printf(\"pan: reducing search depth to %%ld\\n\",",
|
|
" maxdepth);",
|
|
" } else",
|
|
"#endif",
|
|
" if (errors >= upto && upto != 0)",
|
|
" wrapup();",
|
|
" depthfound = -1;",
|
|
"}\n",
|
|
"int",
|
|
"xrefsrc(int lno, S_F_MAP *mp, int M, int i)",
|
|
"{ Trans *T; int j, retval=1;",
|
|
" for (T = trans[M][i]; T; T = T->nxt)",
|
|
" if (T && T->tp)",
|
|
" { if (strcmp(T->tp, \".(goto)\") == 0",
|
|
" || strncmp(T->tp, \"goto :\", 6) == 0)",
|
|
" return 1; /* not reported */",
|
|
"",
|
|
" printf(\"\\tline %%d\", lno);",
|
|
" if (verbose)",
|
|
" for (j = 0; j < sizeof(mp); j++)",
|
|
" if (i >= mp[j].from && i <= mp[j].upto)",
|
|
" { printf(\", \\\"%%s\\\"\", mp[j].fnm);",
|
|
" break;",
|
|
" }",
|
|
" printf(\", state %%d\", i);",
|
|
" if (strcmp(T->tp, \"\") != 0)",
|
|
" { char *q;",
|
|
" q = transmognify(T->tp);",
|
|
" printf(\", \\\"%%s\\\"\", q?q:\"\");",
|
|
" } else if (stopstate[M][i])",
|
|
" printf(\", -end state-\");",
|
|
" printf(\"\\n\");",
|
|
" retval = 0; /* reported */",
|
|
" }",
|
|
" return retval;",
|
|
"}\n",
|
|
"void",
|
|
"r_ck(uchar *which, int N, int M, short *src, S_F_MAP *mp)",
|
|
"{ int i, m=0;\n",
|
|
"#ifdef VERI",
|
|
" if (M == VERI && !verbose) return;",
|
|
"#endif",
|
|
" printf(\"unreached in proctype %%s\\n\", procname[M]);",
|
|
" for (i = 1; i < N; i++)",
|
|
#if 0
|
|
" if (which[i] == 0 /* && trans[M][i] */)",
|
|
#else
|
|
" if (which[i] == 0",
|
|
" && (mapstate[M][i] == 0",
|
|
" || which[mapstate[M][i]] == 0))",
|
|
#endif
|
|
" m += xrefsrc((int) src[i], mp, M, i);",
|
|
" else",
|
|
" m++;",
|
|
" printf(\"\t(%%d of %%d states)\\n\", N-1-m, N-1);",
|
|
"}\n",
|
|
"void",
|
|
"putrail(void)",
|
|
"{ int fd; long i, j;",
|
|
" Trail *trl;",
|
|
"#if defined VERI || defined(MERGED)",
|
|
" char snap[64];",
|
|
"#endif",
|
|
"",
|
|
" fd = make_trail();",
|
|
" if (fd < 0) return;",
|
|
"#ifdef VERI",
|
|
" sprintf(snap, \"-2:%%d:-2\\n\", VERI);",
|
|
" write(fd, snap, strlen(snap));",
|
|
"#endif",
|
|
"#ifdef MERGED",
|
|
" sprintf(snap, \"-4:-4:-4\\n\");",
|
|
" write(fd, snap, strlen(snap));",
|
|
"#endif",
|
|
" for (i = 1; i <= depth; i++)",
|
|
" { if (i == depthfound+1)",
|
|
" write(fd, \"-1:-1:-1\\n\", 9);",
|
|
" trl = getframe(i);",
|
|
" if (!trl->o_t) continue;",
|
|
" if (trl->o_pm&128) continue;",
|
|
" sprintf(snap, \"%%ld:%%d:%%d\\n\", ",
|
|
" i, trl->pr, trl->o_t->t_id);",
|
|
" j = strlen(snap);",
|
|
" if (write(fd, snap, j) != j)",
|
|
" { printf(\"pan: error writing trailfile\\n\");",
|
|
" close(fd);",
|
|
" wrapup();",
|
|
" }",
|
|
" }",
|
|
" close(fd);",
|
|
"}\n",
|
|
"void",
|
|
"sv_save(void) /* push state vector onto save stack */",
|
|
"{ if (!svtack->nxt)",
|
|
" { svtack->nxt = (Svtack *) emalloc(sizeof(Svtack));",
|
|
" svtack->nxt->body = emalloc(vsize*sizeof(char));",
|
|
" svtack->nxt->lst = svtack;",
|
|
" svtack->nxt->m_delta = vsize;",
|
|
" svmax++;",
|
|
" } else if (vsize > svtack->nxt->m_delta)",
|
|
" { svtack->nxt->body = emalloc(vsize*sizeof(char));",
|
|
" svtack->nxt->lst = svtack;",
|
|
" svtack->nxt->m_delta = vsize;",
|
|
" svmax++;",
|
|
" }",
|
|
" svtack = svtack->nxt;",
|
|
"#if SYNC",
|
|
" svtack->o_boq = boq;",
|
|
"#endif",
|
|
" svtack->o_delta = vsize; /* don't compress */",
|
|
" memcpy((char *)(svtack->body), (char *) &now, vsize);",
|
|
"#if defined(C_States) && defined(HAS_STACK) && (HAS_TRACK==1)",
|
|
" c_stack((uchar *) &(svtack->c_stack[0]));",
|
|
"#endif",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%d: sv_save\\n\", depth);",
|
|
"#endif",
|
|
"}\n",
|
|
"void",
|
|
"sv_restor(void) /* pop state vector from save stack */",
|
|
"{",
|
|
" memcpy((char *)&now, svtack->body, svtack->o_delta);",
|
|
"#if SYNC",
|
|
" boq = svtack->o_boq;",
|
|
"#endif",
|
|
|
|
"#if defined(C_States) && (HAS_TRACK==1)",
|
|
"#ifdef HAS_STACK",
|
|
" c_unstack((uchar *) &(svtack->c_stack[0]));",
|
|
"#endif",
|
|
" c_revert((uchar *) &(now.c_state[0]));",
|
|
"#endif",
|
|
|
|
" if (vsize != svtack->o_delta)",
|
|
" Uerror(\"sv_restor\");",
|
|
" if (!svtack->lst)",
|
|
" Uerror(\"error: v_restor\");",
|
|
" svtack = svtack->lst;",
|
|
"#ifdef DEBUG",
|
|
" printf(\" sv_restor\\n\");",
|
|
"#endif",
|
|
"}\n",
|
|
"void",
|
|
"p_restor(int h)",
|
|
"{ int i; char *z = (char *) &now;\n",
|
|
" proc_offset[h] = stack->o_offset;",
|
|
" proc_skip[h] = (uchar) stack->o_skip;",
|
|
"#ifndef XUSAFE",
|
|
" p_name[h] = stack->o_name;",
|
|
"#endif",
|
|
"#ifndef NOCOMP",
|
|
" for (i = vsize + stack->o_skip; i > vsize; i--)",
|
|
" Mask[i-1] = 1; /* align */",
|
|
"#endif",
|
|
" vsize += stack->o_skip;",
|
|
" memcpy(z+vsize, stack->body, stack->o_delta);",
|
|
" vsize += stack->o_delta;",
|
|
"#ifndef NOVSZ",
|
|
" now._vsz = vsize;",
|
|
"#endif",
|
|
"#ifndef NOCOMP",
|
|
" for (i = 1; i <= Air[((P0 *)pptr(h))->_t]; i++)",
|
|
" Mask[vsize - i] = 1; /* pad */",
|
|
" Mask[proc_offset[h]] = 1; /* _pid */",
|
|
"#endif",
|
|
" if (BASE > 0 && h > 0)",
|
|
" ((P0 *)pptr(h))->_pid = h-BASE;",
|
|
" else",
|
|
" ((P0 *)pptr(h))->_pid = h;",
|
|
" i = stack->o_delqs;",
|
|
" now._nr_pr += 1;",
|
|
" if (!stack->lst) /* debugging */",
|
|
" Uerror(\"error: p_restor\");",
|
|
" stack = stack->lst;",
|
|
" this = pptr(h);",
|
|
" while (i-- > 0)",
|
|
" q_restor();",
|
|
"}\n",
|
|
"void",
|
|
"q_restor(void)",
|
|
"{ char *z = (char *) &now;",
|
|
"#ifndef NOCOMP",
|
|
" int k, k_end;",
|
|
"#endif",
|
|
" q_offset[now._nr_qs] = stack->o_offset;",
|
|
" q_skip[now._nr_qs] = (uchar) stack->o_skip;",
|
|
"#ifndef XUSAFE",
|
|
" q_name[now._nr_qs] = stack->o_name;",
|
|
"#endif",
|
|
" vsize += stack->o_skip;",
|
|
" memcpy(z+vsize, stack->body, stack->o_delta);",
|
|
" vsize += stack->o_delta;",
|
|
"#ifndef NOVSZ",
|
|
" now._vsz = vsize;",
|
|
"#endif",
|
|
" now._nr_qs += 1;",
|
|
"#ifndef NOCOMP",
|
|
" k_end = stack->o_offset;",
|
|
" k = k_end - stack->o_skip;",
|
|
"#if SYNC",
|
|
"#ifndef BFS",
|
|
" if (q_zero(now._nr_qs)) k_end += stack->o_delta;",
|
|
"#endif",
|
|
"#endif",
|
|
" for ( ; k < k_end; k++)",
|
|
" Mask[k] = 1;",
|
|
"#endif",
|
|
" if (!stack->lst) /* debugging */",
|
|
" Uerror(\"error: q_restor\");",
|
|
" stack = stack->lst;",
|
|
"}",
|
|
|
|
"typedef struct IntChunks {",
|
|
" int *ptr;",
|
|
" struct IntChunks *nxt;",
|
|
"} IntChunks;",
|
|
"IntChunks *filled_chunks[512];",
|
|
"IntChunks *empty_chunks[512];",
|
|
|
|
"int *",
|
|
"grab_ints(int nr)",
|
|
"{ IntChunks *z;",
|
|
" if (nr >= 512) Uerror(\"cannot happen grab_int\");",
|
|
" if (filled_chunks[nr])",
|
|
" { z = filled_chunks[nr];",
|
|
" filled_chunks[nr] = filled_chunks[nr]->nxt;",
|
|
" } else ",
|
|
" { z = (IntChunks *) emalloc(sizeof(IntChunks));",
|
|
" z->ptr = (int *) emalloc(nr * sizeof(int));",
|
|
" }",
|
|
" z->nxt = empty_chunks[nr];",
|
|
" empty_chunks[nr] = z;",
|
|
" return z->ptr;",
|
|
"}",
|
|
"void",
|
|
"ungrab_ints(int *p, int nr)",
|
|
"{ IntChunks *z;",
|
|
" if (!empty_chunks[nr]) Uerror(\"cannot happen ungrab_int\");",
|
|
" z = empty_chunks[nr];",
|
|
" empty_chunks[nr] = empty_chunks[nr]->nxt;",
|
|
" z->ptr = p;",
|
|
" z->nxt = filled_chunks[nr];",
|
|
" filled_chunks[nr] = z;",
|
|
"}",
|
|
"int",
|
|
"delproc(int sav, int h)",
|
|
"{ int d, i=0;",
|
|
"#ifndef NOCOMP",
|
|
" int o_vsize = vsize;",
|
|
"#endif",
|
|
" if (h+1 != (int) now._nr_pr) return 0;\n",
|
|
" while (now._nr_qs",
|
|
" && q_offset[now._nr_qs-1] > proc_offset[h])",
|
|
" { delq(sav);",
|
|
" i++;",
|
|
" }",
|
|
" d = vsize - proc_offset[h];",
|
|
" if (sav)",
|
|
" { if (!stack->nxt)",
|
|
" { stack->nxt = (Stack *)",
|
|
" emalloc(sizeof(Stack));",
|
|
" stack->nxt->body = ",
|
|
" emalloc(Maxbody*sizeof(char));",
|
|
" stack->nxt->lst = stack;",
|
|
" smax++;",
|
|
" }",
|
|
" stack = stack->nxt;",
|
|
" stack->o_offset = proc_offset[h];",
|
|
"#if VECTORSZ>32000",
|
|
" stack->o_skip = (int) proc_skip[h];",
|
|
"#else",
|
|
" stack->o_skip = (short) proc_skip[h];",
|
|
"#endif",
|
|
"#ifndef XUSAFE",
|
|
" stack->o_name = p_name[h];",
|
|
"#endif",
|
|
" stack->o_delta = d;",
|
|
" stack->o_delqs = i;",
|
|
" memcpy(stack->body, (char *)pptr(h), d);",
|
|
" }",
|
|
" vsize = proc_offset[h];",
|
|
" now._nr_pr = now._nr_pr - 1;",
|
|
" memset((char *)pptr(h), 0, d);",
|
|
" vsize -= (int) proc_skip[h];",
|
|
"#ifndef NOVSZ",
|
|
" now._vsz = vsize;",
|
|
"#endif",
|
|
"#ifndef NOCOMP",
|
|
" for (i = vsize; i < o_vsize; i++)",
|
|
" Mask[i] = 0; /* reset */",
|
|
"#endif",
|
|
" return 1;",
|
|
"}\n",
|
|
"void",
|
|
"delq(int sav)",
|
|
"{ int h = now._nr_qs - 1;",
|
|
" int d = vsize - q_offset[now._nr_qs - 1];",
|
|
"#ifndef NOCOMP",
|
|
" int k, o_vsize = vsize;",
|
|
"#endif",
|
|
" if (sav)",
|
|
" { if (!stack->nxt)",
|
|
" { stack->nxt = (Stack *)",
|
|
" emalloc(sizeof(Stack));",
|
|
" stack->nxt->body = ",
|
|
" emalloc(Maxbody*sizeof(char));",
|
|
" stack->nxt->lst = stack;",
|
|
" smax++;",
|
|
" }",
|
|
" stack = stack->nxt;",
|
|
" stack->o_offset = q_offset[h];",
|
|
"#if VECTORSZ>32000",
|
|
" stack->o_skip = (int) q_skip[h];",
|
|
"#else",
|
|
" stack->o_skip = (short) q_skip[h];",
|
|
"#endif",
|
|
"#ifndef XUSAFE",
|
|
" stack->o_name = q_name[h];",
|
|
"#endif",
|
|
" stack->o_delta = d;",
|
|
" memcpy(stack->body, (char *)qptr(h), d);",
|
|
" }",
|
|
" vsize = q_offset[h];",
|
|
" now._nr_qs = now._nr_qs - 1;",
|
|
" memset((char *)qptr(h), 0, d);",
|
|
" vsize -= (int) q_skip[h];",
|
|
"#ifndef NOVSZ",
|
|
" now._vsz = vsize;",
|
|
"#endif",
|
|
"#ifndef NOCOMP",
|
|
" for (k = vsize; k < o_vsize; k++)",
|
|
" Mask[k] = 0; /* reset */",
|
|
"#endif",
|
|
"}\n",
|
|
"int",
|
|
"qs_empty(void)",
|
|
"{ int i;",
|
|
" for (i = 0; i < (int) now._nr_qs; i++)",
|
|
" { if (q_sz(i) > 0)",
|
|
" return 0;",
|
|
" }",
|
|
" return 1;",
|
|
"}\n",
|
|
"int",
|
|
"endstate(void)",
|
|
"{ int i; P0 *ptr;",
|
|
" for (i = BASE; i < (int) now._nr_pr; i++)",
|
|
" { ptr = (P0 *) pptr(i);",
|
|
" if (!stopstate[ptr->_t][ptr->_p])",
|
|
" return 0;",
|
|
" }",
|
|
" if (strict) return qs_empty();",
|
|
"#if defined(EVENT_TRACE) && !defined(OTIM)",
|
|
" if (!stopstate[EVENT_TRACE][now._event] && !a_cycles)",
|
|
" { printf(\"pan: event_trace not completed\\n\");",
|
|
" return 0;",
|
|
" }",
|
|
"#endif",
|
|
" return 1;",
|
|
"}\n",
|
|
"#ifndef SAFETY",
|
|
"void",
|
|
"checkcycles(void)",
|
|
"{ uchar o_a_t = now._a_t;",
|
|
"#ifndef NOFAIR",
|
|
" uchar o_cnt = now._cnt[1];",
|
|
"#endif",
|
|
"#ifdef FULLSTACK",
|
|
"#ifndef MA",
|
|
" struct H_el *sv = trpt->ostate; /* save */",
|
|
"#else",
|
|
" uchar prov = trpt->proviso; /* save */",
|
|
"#endif",
|
|
"#endif",
|
|
"#ifdef DEBUG",
|
|
" { int i; uchar *v = (uchar *) &now;",
|
|
" printf(\" set Seed state \");",
|
|
"#ifndef NOFAIR",
|
|
" if (fairness) printf(\"(cnt = %%d:%%d, nrpr=%%d) \",",
|
|
" now._cnt[0], now._cnt[1], now._nr_pr);",
|
|
"#endif",
|
|
" /* for (i = 0; i < n; i++) printf(\"%%d,\", v[i]); */",
|
|
" printf(\"\\n\");",
|
|
" }",
|
|
" printf(\"%%d: cycle check starts\\n\", depth);",
|
|
"#endif",
|
|
" now._a_t |= (1|16|32);",
|
|
" /* 1 = 2nd DFS; (16|32) to help hasher */",
|
|
"#ifndef NOFAIR",
|
|
#if 0
|
|
" if (fairness)",
|
|
" { now._a_t &= ~2; /* pre-apply Rule 3 */",
|
|
" now._cnt[1] = 0;", /* reset both a-bit and cnt=0 */
|
|
" /* avoid matching seed on claim stutter on this state */",
|
|
" }",
|
|
#else
|
|
" now._cnt[1] = now._cnt[0];",
|
|
#endif
|
|
"#endif",
|
|
" memcpy((char *)&A_Root, (char *)&now, vsize);",
|
|
" A_depth = depthfound = depth;",
|
|
" new_state(); /* start 2nd DFS */",
|
|
" now._a_t = o_a_t;",
|
|
"#ifndef NOFAIR",
|
|
" now._cnt[1] = o_cnt;",
|
|
"#endif",
|
|
" A_depth = 0; depthfound = -1;",
|
|
"#ifdef DEBUG",
|
|
" printf(\"%%d: cycle check returns\\n\", depth);",
|
|
"#endif",
|
|
"#ifdef FULLSTACK",
|
|
"#ifndef MA",
|
|
" trpt->ostate = sv; /* restore */",
|
|
"#else",
|
|
" trpt->proviso = prov;",
|
|
"#endif",
|
|
"#endif",
|
|
"}",
|
|
"#endif\n",
|
|
"#if defined(FULLSTACK) && defined(BITSTATE)",
|
|
"struct H_el *Free_list = (struct H_el *) 0;",
|
|
"void",
|
|
"onstack_init(void) /* to store stack states in a bitstate search */",
|
|
"{ S_Tab = (struct H_el **) emalloc(maxdepth*sizeof(struct H_el *));",
|
|
"}",
|
|
"struct H_el *",
|
|
"grab_state(int n)",
|
|
"{ struct H_el *v, *last = 0;",
|
|
" if (H_tab == S_Tab)",
|
|
" { for (v = Free_list; v && ((int) v->tagged >= n); v=v->nxt)",
|
|
" { if ((int) v->tagged == n)",
|
|
" { if (last)",
|
|
" last->nxt = v->nxt;",
|
|
" else",
|
|
"gotcha: Free_list = v->nxt;",
|
|
" v->tagged = 0;",
|
|
" v->nxt = 0;",
|
|
"#ifdef COLLAPSE",
|
|
" v->ln = 0;",
|
|
"#endif",
|
|
" return v;",
|
|
" }",
|
|
" Fh++; last=v;",
|
|
" }",
|
|
" /* new: second try */",
|
|
" v = Free_list;", /* try to avoid emalloc */
|
|
" if (v && ((int) v->tagged >= n))",
|
|
" goto gotcha;",
|
|
" ngrabs++;",
|
|
" }",
|
|
" return (struct H_el *)",
|
|
" emalloc(sizeof(struct H_el)+n-sizeof(unsigned));",
|
|
"}\n",
|
|
"#else",
|
|
"#define grab_state(n) (struct H_el *) \\",
|
|
" emalloc(sizeof(struct H_el)+n-sizeof(unsigned));",
|
|
"#endif",
|
|
"#ifdef COLLAPSE",
|
|
"unsigned long",
|
|
"ordinal(char *v, long n, short tp)",
|
|
"{ struct H_el *tmp, *ntmp; long m;",
|
|
" struct H_el *olst = (struct H_el *) 0;",
|
|
" s_hash((uchar *)v, n);",
|
|
" tmp = H_tab[j1];",
|
|
" if (!tmp)",
|
|
" { tmp = grab_state(n);",
|
|
" H_tab[j1] = tmp;",
|
|
" } else",
|
|
" for ( ;; olst = tmp, tmp = tmp->nxt)",
|
|
" { m = memcmp(((char *)&(tmp->state)), v, n);",
|
|
" if (n == tmp->ln)",
|
|
" {",
|
|
" if (m == 0)",
|
|
" goto done;",
|
|
" if (m < 0)",
|
|
" {",
|
|
"Insert: ntmp = grab_state(n);",
|
|
" ntmp->nxt = tmp;",
|
|
" if (!olst)",
|
|
" H_tab[j1] = ntmp;",
|
|
" else",
|
|
" olst->nxt = ntmp;",
|
|
" tmp = ntmp;",
|
|
" break;",
|
|
" } else if (!tmp->nxt)",
|
|
" {",
|
|
"Append: tmp->nxt = grab_state(n);",
|
|
" tmp = tmp->nxt;",
|
|
" break;",
|
|
" }",
|
|
" continue;",
|
|
" }",
|
|
" if (n < tmp->ln)",
|
|
" goto Insert;",
|
|
" else if (!tmp->nxt)",
|
|
" goto Append;",
|
|
" }",
|
|
" m = ++ncomps[tp];",
|
|
"#ifdef FULLSTACK",
|
|
" tmp->tagged = m;",
|
|
"#else",
|
|
" tmp->st_id = m;",
|
|
"#endif",
|
|
" memcpy(((char *)&(tmp->state)), v, n);",
|
|
" tmp->ln = n;",
|
|
"done:",
|
|
"#ifdef FULLSTACK",
|
|
" return tmp->tagged;",
|
|
"#else",
|
|
" return tmp->st_id;",
|
|
"#endif",
|
|
"}",
|
|
"",
|
|
"int",
|
|
"compress(char *vin, int nin) /* collapse compression */",
|
|
"{ char *w, *v = (char *) &comp_now;",
|
|
" int i, j;",
|
|
" unsigned long n;",
|
|
" static char *x;",
|
|
" static uchar nbytes[513]; /* 1 + 256 + 256 */",
|
|
" static unsigned short nbytelen;",
|
|
" long col_q(int, char *);",
|
|
" long col_p(int, char *);",
|
|
"#ifndef SAFETY",
|
|
" if (a_cycles)",
|
|
" *v++ = now._a_t;",
|
|
"#ifndef NOFAIR",
|
|
" if (fairness)",
|
|
" for (i = 0; i < NFAIR; i++)",
|
|
" *v++ = now._cnt[i];",
|
|
"#endif",
|
|
"#endif",
|
|
" nbytelen = 0;",
|
|
|
|
"#ifndef JOINPROCS",
|
|
" for (i = 0; i < (int) now._nr_pr; i++)",
|
|
" { n = col_p(i, (char *) 0);",
|
|
"#ifdef NOFIX",
|
|
" nbytes[nbytelen] = 0;",
|
|
"#else",
|
|
" nbytes[nbytelen] = 1;",
|
|
" *v++ = ((P0 *) pptr(i))->_t;",
|
|
"#endif",
|
|
" *v++ = n&255;",
|
|
" if (n >= (1<<8))",
|
|
" { nbytes[nbytelen]++;",
|
|
" *v++ = (n>>8)&255;",
|
|
" }",
|
|
" if (n >= (1<<16))",
|
|
" { nbytes[nbytelen]++;",
|
|
" *v++ = (n>>16)&255;",
|
|
" }",
|
|
" if (n >= (1<<24))",
|
|
" { nbytes[nbytelen]++;",
|
|
" *v++ = (n>>24)&255;",
|
|
" }",
|
|
" nbytelen++;",
|
|
" }",
|
|
"#else",
|
|
" x = scratch;",
|
|
" for (i = 0; i < (int) now._nr_pr; i++)",
|
|
" x += col_p(i, x);",
|
|
" n = ordinal(scratch, x-scratch, 2); /* procs */",
|
|
" *v++ = n&255;",
|
|
" nbytes[nbytelen] = 0;",
|
|
" if (n >= (1<<8))",
|
|
" { nbytes[nbytelen]++;",
|
|
" *v++ = (n>>8)&255;",
|
|
" }",
|
|
" if (n >= (1<<16))",
|
|
" { nbytes[nbytelen]++;",
|
|
" *v++ = (n>>16)&255;",
|
|
" }",
|
|
" if (n >= (1<<24))",
|
|
" { nbytes[nbytelen]++;",
|
|
" *v++ = (n>>24)&255;",
|
|
" }",
|
|
" nbytelen++;",
|
|
"#endif",
|
|
"#ifdef SEPQS",
|
|
" for (i = 0; i < (int) now._nr_qs; i++)",
|
|
" { n = col_q(i, (char *) 0);",
|
|
" nbytes[nbytelen] = 0;",
|
|
" *v++ = n&255;",
|
|
" if (n >= (1<<8))",
|
|
" { nbytes[nbytelen]++;",
|
|
" *v++ = (n>>8)&255;",
|
|
" }",
|
|
" if (n >= (1<<16))",
|
|
" { nbytes[nbytelen]++;",
|
|
" *v++ = (n>>16)&255;",
|
|
" }",
|
|
" if (n >= (1<<24))",
|
|
" { nbytes[nbytelen]++;",
|
|
" *v++ = (n>>24)&255;",
|
|
" }",
|
|
" nbytelen++;",
|
|
" }",
|
|
"#endif",
|
|
|
|
"#ifdef NOVSZ",
|
|
" /* 3 = _a_t, _nr_pr, _nr_qs */",
|
|
" w = (char *) &now + 3 * sizeof(uchar);",
|
|
"#ifndef NOFAIR",
|
|
" w += NFAIR;",
|
|
"#endif",
|
|
"#else",
|
|
"#if VECTORSZ<65536",
|
|
" w = (char *) &(now._vsz) + sizeof(unsigned short);",
|
|
"#else",
|
|
" w = (char *) &(now._vsz) + sizeof(unsigned long);",
|
|
"#endif",
|
|
"#endif",
|
|
" x = scratch;",
|
|
" *x++ = now._nr_pr;",
|
|
" *x++ = now._nr_qs;",
|
|
|
|
" if (now._nr_qs > 0 && qptr(0) < pptr(0))",
|
|
" n = qptr(0) - (uchar *) w;",
|
|
" else",
|
|
" n = pptr(0) - (uchar *) w;",
|
|
" j = w - (char *) &now;",
|
|
" for (i = 0; i < (int) n; i++, w++)",
|
|
" if (!Mask[j++]) *x++ = *w;",
|
|
"#ifndef SEPQS",
|
|
" for (i = 0; i < (int) now._nr_qs; i++)",
|
|
" x += col_q(i, x);",
|
|
"#endif",
|
|
|
|
" x--;",
|
|
" for (i = 0, j = 6; i < nbytelen; i++)",
|
|
" { if (j == 6)",
|
|
" { j = 0;",
|
|
" *(++x) = 0;",
|
|
" } else",
|
|
" j += 2;",
|
|
" *x |= (nbytes[i] << j);",
|
|
" }",
|
|
" x++;",
|
|
" for (j = 0; j < WS-1; j++)",
|
|
" *x++ = 0;",
|
|
" x -= j; j = 0;",
|
|
" n = ordinal(scratch, x-scratch, 0); /* globals */",
|
|
" *v++ = n&255;",
|
|
" if (n >= (1<< 8)) { *v++ = (n>> 8)&255; j++; }",
|
|
" if (n >= (1<<16)) { *v++ = (n>>16)&255; j++; }",
|
|
" if (n >= (1<<24)) { *v++ = (n>>24)&255; j++; }",
|
|
" *v++ = j; /* add last count as a byte */",
|
|
|
|
" for (i = 0; i < WS-1; i++)",
|
|
" *v++ = 0;",
|
|
" v -= i;",
|
|
"#if 0",
|
|
" printf(\"collapse %%d -> %%d\\n\",",
|
|
" vsize, v - (char *)&comp_now);",
|
|
"#endif",
|
|
" return v - (char *)&comp_now;",
|
|
"}",
|
|
|
|
"#else",
|
|
"#if !defined(NOCOMP)",
|
|
"int",
|
|
"compress(char *vin, int n) /* default compression */",
|
|
"{",
|
|
"#ifdef HC",
|
|
" int delta = 0;",
|
|
" s_hash((uchar *)vin, n); /* sets K1 and K2 */",
|
|
"#ifndef SAFETY",
|
|
" if (S_A)",
|
|
" { delta++; /* _a_t */",
|
|
"#ifndef NOFAIR",
|
|
" if (S_A > NFAIR)",
|
|
" delta += NFAIR; /* _cnt[] */",
|
|
"#endif",
|
|
" }",
|
|
"#endif",
|
|
" memcpy((char *) &comp_now + delta, (char *) &K1, WS);",
|
|
" delta += WS;",
|
|
"#if HC>0",
|
|
" memcpy((char *) &comp_now + delta, (char *) &K2, HC);",
|
|
" delta += HC;",
|
|
"#endif",
|
|
" return delta;",
|
|
"#else",
|
|
" char *vv = vin;",
|
|
" char *v = (char *) &comp_now;",
|
|
" int i;",
|
|
" for (i = 0; i < n; i++, vv++)",
|
|
" if (!Mask[i]) *v++ = *vv;",
|
|
" for (i = 0; i < WS-1; i++)",
|
|
" *v++ = 0;",
|
|
" v -= i;",
|
|
"#if 0",
|
|
" printf(\"compress %%d -> %%d\\n\",",
|
|
" n, v - (char *)&comp_now);",
|
|
"#endif",
|
|
" return v - (char *)&comp_now;",
|
|
"#endif",
|
|
"}",
|
|
"#endif",
|
|
"#endif",
|
|
"#if defined(FULLSTACK) && defined(BITSTATE)",
|
|
"#if defined(MA)",
|
|
"#if !defined(onstack_now)",
|
|
"int onstack_now(void) {}", /* to suppress compiler errors */
|
|
"#endif",
|
|
"#if !defined(onstack_put)",
|
|
"void onstack_put(void) {}", /* for this invalid combination */
|
|
"#endif",
|
|
"#if !defined(onstack_zap)",
|
|
"void onstack_zap(void) {}", /* of directives */
|
|
"#endif",
|
|
"#else",
|
|
"void",
|
|
"onstack_zap(void)",
|
|
"{ struct H_el *v, *w, *last = 0;",
|
|
" struct H_el **tmp = H_tab;",
|
|
" char *nv; int n, m;\n",
|
|
" H_tab = S_Tab;",
|
|
"#ifndef NOCOMP",
|
|
" nv = (char *) &comp_now;",
|
|
" n = compress((char *)&now, vsize);",
|
|
"#else",
|
|
"#if defined(BITSTATE) && defined(LC)",
|
|
" nv = (char *) &comp_now;",
|
|
" n = compact_stack((char *)&now, vsize);",
|
|
"#else",
|
|
" nv = (char *) &now;",
|
|
" n = vsize;",
|
|
"#endif",
|
|
"#endif",
|
|
"#if !defined(HC) && !(defined(BITSTATE) && defined(LC))",
|
|
" s_hash((uchar *)nv, n);",
|
|
"#endif",
|
|
" H_tab = tmp;",
|
|
" for (v = S_Tab[j1]; v; Zh++, last=v, v=v->nxt)",
|
|
" { m = memcmp(&(v->state), nv, n);",
|
|
" if (m == 0)",
|
|
" goto Found;",
|
|
" if (m < 0)",
|
|
" break;",
|
|
" }",
|
|
"/* NotFound: */",
|
|
" Uerror(\"stack out of wack - zap\");",
|
|
" return;",
|
|
"Found:",
|
|
" ZAPS++;",
|
|
" if (last)",
|
|
" last->nxt = v->nxt;",
|
|
" else",
|
|
" S_Tab[j1] = v->nxt;",
|
|
" v->tagged = (unsigned) n;",
|
|
"#if !defined(NOREDUCE) && !defined(SAFETY)",
|
|
" v->proviso = 0;",
|
|
"#endif",
|
|
" v->nxt = last = (struct H_el *) 0;",
|
|
" for (w = Free_list; w; Fa++, last=w, w = w->nxt)",
|
|
" { if ((int) w->tagged <= n)",
|
|
" { if (last)",
|
|
" { v->nxt = w; /* was: v->nxt = w->nxt; */",
|
|
" last->nxt = v;",
|
|
" } else",
|
|
" { v->nxt = Free_list;",
|
|
" Free_list = v;",
|
|
" }",
|
|
" return;",
|
|
" }",
|
|
" if (!w->nxt)",
|
|
" { w->nxt = v;",
|
|
" return;",
|
|
" } }",
|
|
" Free_list = v;",
|
|
"}",
|
|
"void",
|
|
"onstack_put(void)",
|
|
"{ struct H_el **tmp = H_tab;",
|
|
" H_tab = S_Tab;",
|
|
" if (hstore((char *)&now, vsize) != 0)",
|
|
"#if defined(BITSTATE) && defined(LC)",
|
|
" printf(\"pan: warning, double stack entry\\n\");",
|
|
"#else",
|
|
" Uerror(\"cannot happen - unstack_put\");",
|
|
"#endif",
|
|
" H_tab = tmp;",
|
|
" trpt->ostate = Lstate;",
|
|
" PUT++;",
|
|
"}",
|
|
"int",
|
|
"onstack_now(void)",
|
|
"{ struct H_el *tmp;",
|
|
" struct H_el **tmp2 = H_tab;",
|
|
" char *v; int n, m = 1;\n",
|
|
" H_tab = S_Tab;",
|
|
"#ifdef NOCOMP",
|
|
"#if defined(BITSTATE) && defined(LC)",
|
|
" v = (char *) &comp_now;",
|
|
" n = compact_stack((char *)&now, vsize);",
|
|
"#else",
|
|
" v = (char *) &now;",
|
|
" n = vsize;",
|
|
"#endif",
|
|
"#else",
|
|
" v = (char *) &comp_now;",
|
|
" n = compress((char *)&now, vsize);",
|
|
"#endif",
|
|
"#if !defined(HC) && !(defined(BITSTATE) && defined(LC))",
|
|
" s_hash((uchar *)v, n);",
|
|
"#endif",
|
|
" H_tab = tmp2;",
|
|
" for (tmp = S_Tab[j1]; tmp; Zn++, tmp = tmp->nxt)",
|
|
" { m = memcmp(((char *)&(tmp->state)),v,n);",
|
|
" if (m <= 0)",
|
|
" { Lstate = (struct H_el *) tmp;",
|
|
" break;",
|
|
" } }",
|
|
" PROBE++;",
|
|
" return (m == 0);",
|
|
"}",
|
|
"#endif",
|
|
"#endif",
|
|
|
|
"#ifndef BITSTATE",
|
|
"void",
|
|
"hinit(void)",
|
|
"{",
|
|
"#ifdef MA",
|
|
"#ifdef R_XPT",
|
|
" { void r_xpoint(void);",
|
|
" r_xpoint();",
|
|
" }",
|
|
"#else",
|
|
" dfa_init((unsigned short) (MA+a_cycles));",
|
|
"#endif",
|
|
"#endif",
|
|
"#if !defined(MA) || defined(COLLAPSE)",
|
|
" H_tab = (struct H_el **)",
|
|
" emalloc((1L<<ssize)*sizeof(struct H_el *));",
|
|
"#endif",
|
|
"}",
|
|
"#endif\n",
|
|
|
|
"#if !defined(BITSTATE) || defined(FULLSTACK)",
|
|
|
|
"#ifdef DEBUG",
|
|
"void",
|
|
"dumpstate(int wasnew, char *v, int n, int tag)",
|
|
"{ int i;",
|
|
"#ifndef SAFETY",
|
|
" if (S_A)",
|
|
" { printf(\"\tstate tags %%d (%%d::%%d): \",",
|
|
" V_A, wasnew, v[0]);",
|
|
"#ifdef FULLSTACK",
|
|
" printf(\" %%d \", tag);",
|
|
"#endif",
|
|
" printf(\"\\n\");",
|
|
" }",
|
|
"#endif",
|
|
"#ifdef SDUMP",
|
|
"#ifndef NOCOMP",
|
|
" printf(\"\t State: \");",
|
|
" for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",",
|
|
" ((char *)&now)[i], Mask[i]?\"*\":\"\");",
|
|
"#endif",
|
|
" printf(\"\\n\tVector: \");",
|
|
" for (i = 0; i < n; i++) printf(\"%%d,\", v[i]);",
|
|
" printf(\"\\n\");",
|
|
"#endif",
|
|
"}",
|
|
"#endif",
|
|
|
|
"#ifdef MA",
|
|
"int",
|
|
"gstore(char *vin, int nin, uchar pbit)",
|
|
"{ int n, i;",
|
|
" uchar *v;",
|
|
" static uchar Info[MA+1];",
|
|
"#ifndef NOCOMP",
|
|
" n = compress(vin, nin);",
|
|
" v = (uchar *) &comp_now;",
|
|
"#else",
|
|
" n = nin;",
|
|
" v = vin;",
|
|
"#endif",
|
|
" if (n >= MA)",
|
|
" { printf(\"pan: error, MA too small, recompile pan.c\");",
|
|
" printf(\" with -DMA=N with N>%%d\\n\", n);",
|
|
" Uerror(\"aborting\");",
|
|
" }",
|
|
" if (n > (int) maxgs) maxgs = (unsigned int) n;",
|
|
|
|
" for (i = 0; i < n; i++)",
|
|
" Info[i] = v[i];",
|
|
" for ( ; i < MA-1; i++)",
|
|
" Info[i] = 0;",
|
|
" Info[MA-1] = pbit;",
|
|
" if (a_cycles) /* place _a_t at the end */",
|
|
" { Info[MA] = Info[0]; Info[0] = 0; }",
|
|
" if (!dfa_store(Info))",
|
|
" { if (pbit == 0",
|
|
" && (now._a_t&1)",
|
|
" && depth > A_depth)",
|
|
" { Info[MA] &= ~(1|16|32); /* _a_t */",
|
|
" if (dfa_member(MA))", /* was !dfa_member(MA) */
|
|
" { Info[MA-1] = 4; /* off-stack bit */",
|
|
" nShadow++;",
|
|
" if (!dfa_member(MA-1))",
|
|
" {",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"intersected 1st dfs stack\\n\");",
|
|
"#endif",
|
|
" return 3;",
|
|
" } } }",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"new state\\n\");",
|
|
"#endif",
|
|
" return 0; /* new state */",
|
|
" }",
|
|
"#ifdef FULLSTACK",
|
|
" if (pbit == 0)",
|
|
" { Info[MA-1] = 1; /* proviso bit */",
|
|
"#ifndef BFS",
|
|
" trpt->proviso = dfa_member(MA-1);",
|
|
"#endif",
|
|
" Info[MA-1] = 4; /* off-stack bit */",
|
|
" if (dfa_member(MA-1)) {",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"old state\\n\");",
|
|
"#endif",
|
|
" return 1; /* off-stack */",
|
|
" } else {",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"on-stack\\n\");",
|
|
"#endif",
|
|
" return 2; /* on-stack */",
|
|
" }",
|
|
" }",
|
|
"#endif",
|
|
"#ifdef VERBOSE",
|
|
" printf(\"old state\\n\");",
|
|
"#endif",
|
|
" return 1; /* old state */",
|
|
"}",
|
|
"#endif",
|
|
|
|
"#if defined(BITSTATE) && defined(LC)",
|
|
"int",
|
|
"compact_stack(char *vin, int n)", /* special case of HC4 */
|
|
"{ int delta = 0;",
|
|
" s_hash((uchar *)vin, n); /* sets K1 and K2 */",
|
|
"#ifndef SAFETY",
|
|
" delta++; /* room for state[0] |= 128 */",
|
|
"#endif",
|
|
" memcpy((char *) &comp_now + delta, (char *) &K1, WS);",
|
|
" delta += WS;",
|
|
" memcpy((char *) &comp_now + delta, (char *) &K2, WS);",
|
|
" delta += WS; /* use all available bits */",
|
|
" return delta;",
|
|
"}",
|
|
"#endif",
|
|
|
|
"int",
|
|
"hstore(char *vin, int nin) /* hash table storage */",
|
|
"{ struct H_el *tmp, *ntmp, *olst = (struct H_el *) 0;",
|
|
" char *v; int n, m=0;",
|
|
"#ifdef HC",
|
|
" uchar rem_a;",
|
|
"#endif",
|
|
"#ifdef NOCOMP", /* defined by BITSTATE */
|
|
"#if defined(BITSTATE) && defined(LC)",
|
|
" if (S_Tab == H_tab)",
|
|
" { v = (char *) &comp_now;",
|
|
" n = compact_stack(vin, nin);",
|
|
" } else",
|
|
" { v = vin; n = nin;",
|
|
" }",
|
|
"#else",
|
|
" v = vin; n = nin;",
|
|
"#endif",
|
|
"#else",
|
|
" v = (char *) &comp_now;",
|
|
" #ifdef HC",
|
|
" rem_a = now._a_t;", /* 4.3.0 */
|
|
" now._a_t = 0;", /* for hashing/state matching to work right */
|
|
" #endif",
|
|
" n = compress(vin, nin);", /* with HC, this calls s_hash */
|
|
" #ifdef HC",
|
|
" now._a_t = rem_a;", /* 4.3.0 */
|
|
" #endif",
|
|
"#ifndef SAFETY",
|
|
" if (S_A)",
|
|
" { v[0] = 0; /* _a_t */",
|
|
"#ifndef NOFAIR",
|
|
" if (S_A > NFAIR)",
|
|
" for (m = 0; m < NFAIR; m++)",
|
|
" v[m+1] = 0; /* _cnt[] */",
|
|
"#endif",
|
|
" m = 0;",
|
|
" }",
|
|
"#endif",
|
|
"#endif",
|
|
"#if !defined(HC) && !(defined(BITSTATE) && defined(LC))",
|
|
" s_hash((uchar *)v, n);",
|
|
"#endif",
|
|
" tmp = H_tab[j1];",
|
|
" if (!tmp)",
|
|
" { tmp = grab_state(n);",
|
|
" H_tab[j1] = tmp;",
|
|
" } else",
|
|
" { for (;; hcmp++, olst = tmp, tmp = tmp->nxt)",
|
|
" { /* skip the _a_t and the _cnt bytes */",
|
|
"#ifdef COLLAPSE",
|
|
" if (tmp->ln != 0)",
|
|
" { if (!tmp->nxt) goto Append;",
|
|
" continue;",
|
|
" }",
|
|
"#endif",
|
|
" m = memcmp(((char *)&(tmp->state)) + S_A, ",
|
|
" v + S_A, n - S_A);",
|
|
" if (m == 0) {",
|
|
"#ifdef SAFETY",
|
|
"#define wasnew 0",
|
|
"#else",
|
|
" int wasnew = 0;",
|
|
"#endif",
|
|
|
|
"#ifndef SAFETY",
|
|
"#ifndef NOCOMP",
|
|
" if (S_A)",
|
|
" { if ((((char *)&(tmp->state))[0] & V_A) != V_A)",
|
|
" { wasnew = 1; nShadow++;",
|
|
" ((char *)&(tmp->state))[0] |= V_A;",
|
|
" }",
|
|
"#ifndef NOFAIR",
|
|
" if (S_A > NFAIR)",
|
|
" { /* 0 <= now._cnt[now._a_t&1] < MAXPROC */",
|
|
" unsigned ci, bp; /* index, bit pos */",
|
|
" ci = (now._cnt[now._a_t&1] / 8);",
|
|
" bp = (now._cnt[now._a_t&1] - 8*ci);",
|
|
" if (now._a_t&1) /* use tail-bits in _cnt */",
|
|
" { ci = (NFAIR - 1) - ci;",
|
|
" bp = 7 - bp; /* bp = 0..7 */",
|
|
" }",
|
|
" ci++; /* skip over _a_t */",
|
|
" bp = 1 << bp; /* the bit mask */",
|
|
" if ((((char *)&(tmp->state))[ci] & bp)==0)",
|
|
" { if (!wasnew)",
|
|
" { wasnew = 1;",
|
|
" nShadow++;",
|
|
" }",
|
|
" ((char *)&(tmp->state))[ci] |= bp;",
|
|
" }",
|
|
" }",
|
|
" /* else: wasnew == 0, i.e., old state */",
|
|
"#endif",
|
|
" }",
|
|
"#endif",
|
|
"#endif",
|
|
|
|
"#ifdef FULLSTACK",
|
|
"#ifndef SAFETY", /* or else wasnew == 0 */
|
|
" if (wasnew)",
|
|
" { Lstate = (struct H_el *) tmp;",
|
|
" tmp->tagged |= V_A;",
|
|
" if ((now._a_t&1)",
|
|
" && (tmp->tagged&A_V)",
|
|
" && depth > A_depth)",
|
|
" {",
|
|
"intersect:",
|
|
"#ifdef CHECK",
|
|
" printf(\"1st dfs-stack intersected on state %%d+\\n\",",
|
|
" (int) tmp->st_id);",
|
|
"#endif",
|
|
" return 3;",
|
|
" }",
|
|
"#ifdef CHECK",
|
|
" printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);",
|
|
"#endif",
|
|
"#ifdef DEBUG",
|
|
" dumpstate(1, (char *)&(tmp->state),n,tmp->tagged);",
|
|
"#endif",
|
|
" return 0;",
|
|
" } else",
|
|
"#endif",
|
|
" if ((S_A)?(tmp->tagged&V_A):tmp->tagged)",
|
|
" { Lstate = (struct H_el *) tmp;",
|
|
"#ifndef SAFETY",
|
|
" /* already on current dfs stack */",
|
|
" /* but may also be on 1st dfs stack */",
|
|
" if ((now._a_t&1)",
|
|
" && (tmp->tagged&A_V)",
|
|
|
|
" && depth > A_depth",
|
|
/* new (Zhang's example) */
|
|
"#ifndef NOFAIR",
|
|
" && (!fairness || now._cnt[1] <= 1)",
|
|
"#endif",
|
|
" )",
|
|
|
|
" goto intersect;",
|
|
"#endif",
|
|
"#ifdef CHECK",
|
|
" printf(\"\tStack state %%d\\n\", (int) tmp->st_id);",
|
|
"#endif",
|
|
"#ifdef DEBUG",
|
|
" dumpstate(0, (char *)&(tmp->state),n,tmp->tagged);",
|
|
"#endif",
|
|
" return 2; /* match on stack */",
|
|
" }",
|
|
"#else",
|
|
" if (wasnew)",
|
|
" {",
|
|
"#ifdef CHECK",
|
|
" printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);",
|
|
"#endif",
|
|
"#ifdef DEBUG",
|
|
" dumpstate(1, (char *)&(tmp->state), n, 0);",
|
|
"#endif",
|
|
" return 0;",
|
|
" }",
|
|
"#endif",
|
|
"#ifdef CHECK",
|
|
" printf(\"\tOld state %%d\\n\", (int) tmp->st_id);",
|
|
"#endif",
|
|
"#ifdef DEBUG",
|
|
" dumpstate(0, (char *)&(tmp->state), n, 0);",
|
|
"#endif",
|
|
"#ifdef REACH",
|
|
" if (tmp->D > depth)",
|
|
" { tmp->D = depth;",
|
|
"#ifdef CHECK",
|
|
" printf(\"\t\tReVisiting (from smaller depth)\\n\");",
|
|
"#endif",
|
|
" nstates--;",
|
|
#if 0
|
|
possible variation of iterative search for shortest counter-example (pan -i
|
|
and pan -I) suggested by Pierre Moro (for safety properties):
|
|
state revisits on shorter depths do not start until after
|
|
the first counter-example is found. this assumes that the max search
|
|
depth is set large enough that a first (possibly long) counter-example
|
|
can be found
|
|
if set too short, this variant can miss the counter-example, even if
|
|
it would otherwise be shorter than the depth-limit.
|
|
(p.m. unsure if this preserves the guarantee of finding the
|
|
shortest counter-example - so not enabled yet)
|
|
" if (errors > 0 && iterative)", /* Moro */
|
|
#endif
|
|
" return 0;",
|
|
" }",
|
|
"#endif",
|
|
"#if defined(BFS) && defined(Q_PROVISO)",
|
|
" Lstate = (struct H_el *) tmp;",
|
|
"#endif",
|
|
" return 1; /* match outside stack */",
|
|
" } else if (m < 0)",
|
|
" { /* insert state before tmp */",
|
|
" ntmp = grab_state(n);",
|
|
" ntmp->nxt = tmp;",
|
|
" if (!olst)",
|
|
" H_tab[j1] = ntmp;",
|
|
" else",
|
|
" olst->nxt = ntmp;",
|
|
" tmp = ntmp;",
|
|
" break;",
|
|
" } else if (!tmp->nxt)",
|
|
" { /* append after tmp */",
|
|
"#ifdef COLLAPSE",
|
|
"Append:",
|
|
"#endif",
|
|
" tmp->nxt = grab_state(n);",
|
|
" tmp = tmp->nxt;",
|
|
" break;",
|
|
" } }",
|
|
" }",
|
|
"#ifdef CHECK",
|
|
" tmp->st_id = (unsigned) nstates;",
|
|
"#ifdef BITSTATE",
|
|
" printf(\" Push state %%d\\n\", ((int) nstates) - 1);",
|
|
"#else",
|
|
" printf(\" New state %%d\\n\", (int) nstates);",
|
|
"#endif",
|
|
"#endif",
|
|
"#if !defined(SAFETY) || defined(REACH)",
|
|
" tmp->D = depth;",
|
|
"#endif",
|
|
"#ifndef SAFETY",
|
|
"#ifndef NOCOMP",
|
|
" if (S_A)",
|
|
" { v[0] = V_A;",
|
|
"#ifndef NOFAIR",
|
|
" if (S_A > NFAIR)",
|
|
" { unsigned ci, bp; /* as above */",
|
|
" ci = (now._cnt[now._a_t&1] / 8);",
|
|
" bp = (now._cnt[now._a_t&1] - 8*ci);",
|
|
" if (now._a_t&1)",
|
|
" { ci = (NFAIR - 1) - ci;",
|
|
" bp = 7 - bp; /* bp = 0..7 */",
|
|
" }",
|
|
" v[1+ci] = 1 << bp;",
|
|
" }",
|
|
"#endif",
|
|
" }",
|
|
"#endif",
|
|
"#endif",
|
|
" memcpy(((char *)&(tmp->state)), v, n);",
|
|
"#ifdef FULLSTACK",
|
|
" tmp->tagged = (S_A)?V_A:(depth+1);",
|
|
"#ifdef DEBUG",
|
|
" dumpstate(-1, v, n, tmp->tagged);",
|
|
"#endif",
|
|
" Lstate = (struct H_el *) tmp;",
|
|
"#else",
|
|
"#ifdef DEBUG",
|
|
" dumpstate(-1, v, n, 0);",
|
|
"#endif",
|
|
"#endif",
|
|
" return 0;",
|
|
"}",
|
|
"#endif",
|
|
"#include TRANSITIONS",
|
|
"void",
|
|
"do_reach(void)",
|
|
"{",
|
|
0,
|
|
};
|