/***** 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(\"<<<<>>>>\\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< RANDSTOR) return 0;", "#endif", " for (;;)", " { SS[x%%udmem] |= (1< RANDSTOR) return 0;", "#endif", " for (;;)", " { SS[x] |= (1< 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< 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< 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<>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<>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] \\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<= 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, };