/***** spin: pangen1.h *****/ /* Copyright (c) 1991-2000 by Lucent Technologies - Bell Laboratories */ /* All Rights Reserved. This software is for educational purposes only. */ /* Permission is given to distribute this code provided that this intro- */ /* ductory message is not removed and no monies are exchanged. */ /* No guarantee is expressed or implied by the distribution of this code. */ /* Software written by Gerard J. Holzmann as part of the book: */ /* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4, */ /* Prentice Hall, Englewood Cliffs, NJ, 07632. */ /* Send bug-reports and/or questions to: gerard@research.bell-labs.com */ static char *Code2[] = { /* the tail of procedure run() */ "#if defined(VERI) && !defined(NOREDUCE) && !defined(NP)", " if (!state_tables)", " { printf(\"warning: for p.o. reduction to be valid \");", " printf(\"the never claim must be stutter-closed\\n\");", " printf(\"(never claims generated from LTL \");", " printf(\"formulae are stutter-closed)\\n\");", " }", "#endif", " UnBlock; /* disable rendez-vous */", "#ifdef MEMCNT", " overhead = memcnt;", "#endif", "#ifdef BITSTATE", " SS = (uchar *) emalloc(1<<(ssize-3));", "#else", " hinit();", "#endif", "#if defined(FULLSTACK) && defined(BITSTATE)", " onstack_init();", "#endif", "#ifdef CNTRSTACK", " LL = (uchar *) emalloc(1<<(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", "go_again:", " do_the_search();", "#if defined(BITSTATE)", " if (--Nrun > 0 && HASH_CONST[++HASH_NR])", " { printf(\"Run %%d:\\n\", HASH_NR);", " wrap_stats();", " printf(\"\\n\");", " memset(SS, 0, 1<<(ssize-3));", "#if defined(CNTRSTACK)", " memset(LL, 0, 1<<(ssize-3));", "#endif", "#if defined(FULLSTACK)", " memset((uchar *) S_Tab, 0, ", " (1<<(ssize-3))*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", "}", #ifndef PRINTF "#include ", "void", "Printf(const char *fmt, ...)", "{ /* Make sure the args to Printf", " * are always evaluated (e.g., they", " * could contain a run stmnt)", " * but don't 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 PRINTF", " va_list args;", " va_start(args, fmt);", " vprintf(fmt, args);", " va_end(args);", "#endif", "}", #endif "#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*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", "do_the_search(void)", "{ int i;", " depth=mreached=0;", " trpt = &trail[depth];", "#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", " new_state(); /* start 1st DFS */", "}", "#ifdef INLINE_REV", "char", "do_reverse(Trans *t, short II, char M)", "{ char m = M;", " short tt = (short) ((P0 *)this)->_p;", "#include REVERSE_MOVES", "R999: return m;", "}", "#endif", "#ifndef INLINE", "#ifdef EVENT_TRACE", "static char _tp = 'n'; static int _qid = 0;", "#endif", "char", "do_transit(Trans *t, short II, int n)", "{ char m;", " short tt = (short) ((P0 *)this)->_p;", " char ot = (char) ((P0 *)this)->_t;", "#ifdef EVENT_TRACE", " short oboq = boq;", " if (II == EVENT_TRACE) boq = -1;", "#define continue { boq = oboq; return 0; }", "#else", "#define continue return 0", "#endif", "#include FORWARD_MOVES", "P999:", "#ifdef EVENT_TRACE", " boq = oboq;", "#endif", " return m;", "#undef continue", "}", "#ifdef EVENT_TRACE", "void", "require(char tp, int qid)", "{ Trans *t;", " _tp = tp; _qid = qid;", "#ifdef NEGATED_TRACE", " if (now._event == endevent)", " { depth++; trpt++;", " uerror(\"event_trace error (all events matched)\");", "#ifndef NP", " if (accpstate[EVENT_TRACE][now._event])", " trpt->o_pm |= 2;", "#else", " if (progstate[EVENT_TRACE][now._event])", " trpt->o_pm |= 4;", "#endif", " trpt--; depth--;", " now._event = start_event;", " return;", " } else", "#else", " if (now._event != endevent)", "#endif", " for (t = trans[EVENT_TRACE][now._event]; t; t = t->nxt)", " { if (do_transit(t, EVENT_TRACE, 0))", " { now._event = t->st;", " reached[EVENT_TRACE][t->st] = 1;", "#ifdef VERBOSE", " printf(\" event_trace move to -> %%d\\n\", t->st);", "#endif", "#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", " for (t = t->nxt; t; t = t->nxt)", " { if (do_transit(t, EVENT_TRACE, 0))", " 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 = start_event; /* only 1st try will count */", "#else", " depth++; trpt++;", " uerror(\"event_trace error (no matching event)\");", " trpt--; depth--;", "#endif", "}", "#endif", "int", "enabled(int iam, int pid)", "{ Trans *t; uchar *othis = this;", " int res = 0; short tt; char 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 = (short) ((P0 *)this)->_p;", " ot = (uchar) ((P0 *)this)->_t;", " for (t = trans[ot][tt]; t; t = t->nxt)", " if (do_transit(t, pid, 0))", " { 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, 0666)) <= 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*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*sizeof(Trail), SEEK_SET) == -1)", " Uerror(\"disk2stack lseek error2\");", "", " 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 (proc_offset[x])", " return (uchar *) pptr(x);", " else", " return noptr;", "}", "extern void check_claim(int);", "/* new_state() is the main search routine in the verifier", " * it has a lot of code ifdef-ed together to support", " * different search modes -- this makes it quite unreadable", " * of course. if you are studying the code, first", " * let the C preprocessor generate a specific version", " * from the pan.c source, e.g. by saying:", " * /lib/cpp -DNOREDUCE -DBITSTATE pan.c > Pan.c", " * and study the resulting file, rather than this one", " */", "void", "new_state(void)", "{ Trans *t;", " char n, m, ot;", " short II, JJ=0, tt, kk;\n", " 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\");", " }", " (trpt-1)->tau |= 16; /* worstcase guess */", " goto Up;", " }", "AllOver:", "#if defined(FULLSTACK) && !defined(MA)", " trpt->ostate = (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 CNTRSTACK", /* -> bitstate, reduced, safety */ " d_hash((uchar *)&now, vsize);", " trpt->j6 = j1; trpt->j7 = j2;", " JJ = LL[j1] && LL[j2];", "#endif", "#ifdef FULLSTACK", "#ifdef BITSTATE", " JJ = onstack_now();", "#else", "#ifdef MA", " II = gstore((char *)&now, vsize, 0);", "#else", " II = hstore((char *)&now, vsize, 1);", "#endif", " JJ = (II == 2)?1:0;", "#endif", "#endif", "#ifdef BITSTATE", "#ifndef CNTRSTACK", /* !reduced */ " d_hash((uchar *) &now, vsize);", "#endif", " kk = II = ((SS[j2]&j3) && (SS[j1]&j4));", "#ifdef DEBUG", " if (II) printf(\"Old bitstate\\n\");", " else printf(\"New bitstate\\n\");", "#endif", "#else", "#ifndef FULLSTACK", "#ifdef MA", " JJ = II = gstore((char *) &now, vsize, 0);", "#else", " II = hstore((char *)&now, vsize, 2);", "#endif", "#endif", " kk = (II == 1 || II == 2);", "#endif", "#ifndef SAFETY", "#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);", " if (onstack_now())", " { II = 3;", "#ifdef VERBOSE", " printf(\"state match on 1st dfs stack\\n\");", "#endif", " }", " now._a_t = o_a_t;", " 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(\" fairness count non-zero\\n\");", "#endif", " II = 0;", " } else", "#endif", " {", "#ifdef BITSTATE", " depthfound = Lstate->tagged - 1;", "#ifdef NP", " uerror(\"non-progress cycle\");", "#else", " uerror(\"acceptance cycle\");", "#endif", "#else", " depthfound = depth_of(Lstate);", "#ifdef NP", " uerror(\"non-progress cycle\");", "#else", " uerror(\"acceptance cycle\");", "#endif", " nShadow--;", "#endif", " goto Up;", " }", " }", "#endif", "#if !defined(FULLSTACK) && !defined(CNTRSTACK) && defined(BITSTATE)", "#ifndef NOREDUCE", " JJ = II; /* worstcase guess for p.o. */", "#endif", "#endif", "#ifndef NOREDUCE", "#ifndef SAFETY", " if ((II && JJ) || (II == 3))", " { /* marker for liveness proviso */", " truncs2++;", " (trpt-1)->tau |= 16;", " }", "#else", " if (!II || !JJ)", " { /* has successor outside stack */", " (trpt-1)->tau |= 64;", " }", "#endif", "#endif", " if (II)", " { truncs++;", " goto Up;", " }", " if (!kk)", " { nstates++;", "#ifdef SVDUMP", " if (vprefix > 0)", " if (write(svfd, (uchar *) &now, vprefix) != vprefix)", " { fprintf(efd, \"writing %%s.svd failed\\n\", Source);", " wrapup();", " }", "#endif", " if ((unsigned long) nstates%%1000000 == 0)", " snapshot();", "#ifdef MA", "#ifdef W_XPT", " if ((unsigned long) nstates%%W_XPT == 0)", " { void w_xpoint(void);", " w_xpoint();", " }", "#endif", "#endif", " }", "#ifdef BITSTATE", "#ifdef RANDSTOR", " if (rand()%%100 <= RANDSTOR)", "#endif", " { SS[j2] |= j3; SS[j1] |= j4; }", "#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(\"endstate in claim reached\");", " check_claim(((P0 *)pptr(0))->_p);", "Stutter:", " if (trpt->tau&4) /* must make a claimmove */", " { 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 = (short) ((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", "Again:", " /* 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", "Veri0: this = pptr(II);", " tt = (short) ((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", "#ifdef EVENT_TRACE", " (trpt+1)->pr = II;", "#endif", " for (t = trans[ot][tt]; t; t = t->nxt)", " {", "#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", "#ifdef EVENT_TRACE", " (trpt+1)->o_t = t;", "#endif", "#ifdef INLINE", "#include FORWARD_MOVES", "#else", " if (!(m = do_transit(t, II, n))) continue;", "#endif", "P999: /* jumps here when move succeeds */", " 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", "#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 = 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)", " { int ii;", "#define PQ ((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[PQ->_t][PQ->_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[PQ->_t][PQ->_p])", " { trpt->o_pm |= 4;", " break;", " } }", "#endif", "#undef PQ", " }", "#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;", " 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 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;", " }", "#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 */", "#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; /* gh,1/99 was 0 */", "#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, 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", "#ifdef OTIM", " || endstate()", "#endif", " || depth >= maxdepth-1) goto Done;", /* new location of atomic block code -- BEFORE timeout */ " 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);", " 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 */ "BreakOut:", "#ifdef VERI", "#ifndef NOSTUTTER", #if 1 " if (!(trpt->tau&4))", #else /* visser's example shows this is insufficient: */ " if ((now._a_t&1) && !(trpt->tau&4))", #endif " { trpt->tau |= 4; /* claim stuttering */", " trpt->tau |= 128; /* stutter mark */", "#ifdef DEBUG", " printf(\"%%d: claim stutter\\n\", depth);", "#endif", " goto Stutter;", " }", "#endif", "#else", " if (!noends && !a_cycles && !endstate())", " uerror(\"invalid endstate\");", "#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)", " {", "#ifdef VERBOSE", " printf(\"Consider check %%d %%d...\\n\",", " now._a_t, now._cnt[0]);", "#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", "void", "assert(int a, char *s, int ii, int tt, Trans *t)", "{", " if (!a && !noasserts)", " { char bad[1024];", " if (strlen(s) > 999) s[999] = '\\0';", " sprintf(bad, \"assertion violated %%s\", s);", " depth++; trpt++;", " if (t) {", " trpt->pr = ii;", " trpt->st = tt;", " trpt->o_t = t;", " } else {", " trpt->pr = (trpt-1)->pr;", " trpt->st = (trpt-1)->st;", " trpt->o_t = (trpt-1)->o_t;", " }", " uerror(bad);", " depth--; trpt--;", " }", "}", "#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)", "{ double a, b;", "#ifdef COVEST", " extern double log(double);\n", "#endif", " if (nShadow>0)", " printf(\"%%8g states, stored (%%g visited)\\n\",", " nstates - nShadow, nstates);", " else", " printf(\"%%8g states, stored\\n\", nstates);", " 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);", "#ifdef BITSTATE", "#ifdef CHECK", " printf(\"%%8g states allocated for dfs stack\\n\", ngrabs);", "#endif", " a = (double) (1<<(ssize-3)); a = 8.*a; /* avoid overflow on << */", " b = nstates+1.;", "#ifdef COVEST", " printf(\"coverage estimate: %%0.1f%%%%\\n\",", " (100.*b)/(log(1. - b / a)/log(1. - 1. / a)));", "#endif", " printf(\"hash factor: %%g \", a/b);", " if (!single)", " { if (a/b > 100.)", "#ifdef COVEST", " printf(\"(good confidence estimate)\\n\");", " else if (a/b > 10.)", " printf(\"(medium confidence estimate)\\n\");", " else", " printf(\"(low confidence estimate, best if >100)\\n\");", " } else", " { if (a/b > 1000.)", " printf(\"(good confidence estimate)\\n\");", " else if (a/b > 100.)", " printf(\"(medium confidence estimate)\\n\");", " else", " printf(\"(low confidence estimate (1-bit hash), best if >1000)\\n\");", "#else", " printf(\"(expected coverage: >= 99.9%%%% on avg.)\\n\");", " else if (a/b > 10.)", " printf(\"(expected coverage: >= 98%%%% on avg.)\\n\");", " else", " printf(\"(best coverage if >100)\\n\");", " } else", " { if (a/b > 1000.)", " printf(\"(expected coverage: >= 99.9%%%% on avg.)\\n\");", " else if (a/b > 100.)", " printf(\"(expected coverage: >= 98%%%% on avg.)\\n\");", " else", " printf(\"(best coverage (1-bit hash) if >1000)\\n\");", "#endif", " }", "#else", " printf(\"hash conflicts: %%g (resolved)\\n\", hcmp);", "#endif", "}", "void", "wrapup(void)", "{ double nr1, nr2, nr3 = 0.0, nr4;", "#ifndef BITSTATE", " double tmp_nr;", "#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", "#ifndef NOREDUCE", " printf(\" + Partial Order Reduction\\n\");", "#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 endstates\t- \");", " printf(\"(disabled by \");", " if (noends)", " printf(\"-E flag)\\n\\n\");", " else", " printf(\"never-claim)\\n\\n\");", "#else", " printf(\"\tinvalid endstates\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();", " printf(\"(max size 2^%%d states\", ssize);", "#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\\n\");", "#endif", "#ifdef MEMCNT", "#if defined(BITSTATE) || !defined(NOCOMP)", " nr1 = (nstates-nShadow)*", " (double)(hmax+sizeof(struct H_el)-sizeof(unsigned));", " nr2 = (double) ((maxdepth+3)*sizeof(Trail));", "#ifndef BITSTATE", "#if !defined(MA) || defined(COLLAPSE)", " nr3 = (double) (1< 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(\" + %%d 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);", "#endif", "#endif", " printf(\"%%-6.3f\tmemory used for DFS stack (-m%%d)\\n\",", " nr2/1000000., maxdepth);", " /* remainder is mem used for proc and chan stacks */", " /* and memory lost in allocator (=fragment) */", " printf(\"%%-6.3f\ttotal actual memory usage\\n\\n\",", " memcnt/1000000.);", " } else", "#endif", " printf(\"%%-6.3f\tmemory usage (Mbyte)\\n\\n\",", " memcnt/1000000.);", "#endif", "#ifdef COLLAPSE", " printf(\"nr of templates: [ globals procs chans ]\\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", " exit(0);", "}\n", "void", "stopped(int arg)", "{ printf(\"Interrupted\\n\");", " wrapup();", "}", "void", "d_hash(uchar *Cp, int Om)", "{ long z = (long) HASH_CONST[HASH_NR];", " long *q, *r, h;", " long m, n;", "#ifndef BCOMP", " uchar *cp = Cp;", " long om = (long) Om;", "#else", " uchar *cp = (uchar *) &comp_now;", " char *vv = (char *) Cp;", " char *v = (char *) &comp_now;", " long i, om;", " for (i = 0; i < Om; i++, vv++)", " if (!Mask[i]) *v++ = *vv;", " for (i = 0; i < WS-1; i++)", " *v++ = 0;", " v -= i;", " om = v - (char *)&comp_now;", "#endif", " h = (om+sizeof(long)-1)/sizeof(long);", " m = n = -1;", " q = r = (long *) cp;", " r += (long) h;", " do {", " if (m < 0)", " { m += m;", " m ^= z;", " } else", " m += m;", " m ^= *q++;", " if (n < 0)", " { n += n;", " n ^= z;", " } else", " n += n;", " n ^= *--r;", " } while (--h > 0);", " J1 = (m ^ (m>>(8*sizeof(long)-ssize)))&mask;", " J2 = (n ^ (n>>(8*sizeof(long)-ssize)))&mask;", "#if 0", " j3 = (1<<(J1&7)); j1 = J1>>3;", " j4 = (1<<(J2&7)); j2 = J2>>3;", "#endif", " if (!single)", " { j3 = (1<<(J1&7)); j2 = J2>>3;", " j4 = (1<<(J2&7)); j1 = J1>>3;", " } else /* single-bit address */", " { J1 = J1^J2; /* use all bits */", " j3 = (1<<(J1&7)); j2 = J1>>3;", " j1 = 0; j4 = 1;", " }", "}\n", "#ifdef HYBRID_HASH", "long", "#else", "void", "#endif", "s_hash(uchar *cp, int om) /* single forward hash */", "{ long z = (long) HASH_CONST[HASH_NR];", " long *q;", " long h;", " long m = -1;", " h = (om+sizeof(long)-1)/sizeof(long);", " q = (long *) cp;", " do {", " if (m < 0)", " { m += m;", " m ^= z;", " } else", " m += m;", " m ^= *q++;", " } while (--h > 0);", "#ifdef BITSTATE", " if (S_Tab == H_tab)", " j1 = (m^(m>>(8*sizeof(long)-(ssize-3))))&((1<<(ssize-3))-1);", " else", "#endif", " j1 = (m^(m>>(8*sizeof(long)-ssize)))&mask;", "#ifdef HYBRID_HASH", "#ifndef BITSTATE", " if ((om&(sizeof(void *)-1)) == 1) /* very badly aligned */", " { /* use last data byte as first byte of hash */", " j1 = (j1 & (~255)) | cp[om-1];", " return om-1; /* perfect alignment */", " }", "#endif", " return om;", "#endif", "}", "#if defined(HC) || (defined(BITSTATE) && defined(LC))", "void", "r_hash(uchar *cp, int om) /* reverse direction from s_hash */", "{ long z = (long) HASH_CONST[HASH_NR];", " long *r, h, n = -1;", " h = (om+sizeof(long)-1)/sizeof(long);", " r = (long *) cp + h;", " do {", " if (n < 0)", " { n += n;", " n ^= z;", " } else", " n += n;", " n ^= *--r;", " } while (--h > 0);", " J3 = n; /* the compressed state vector */", " n = -1; /* forward hash for hash_table index */", " h = (om+sizeof(long)-1)/sizeof(long);", " r = (long *) cp;", " do {", " if (n < 0)", " { n += n;", " n ^= z;", " } else", " n += n;", " n ^= *r++;", " } while (--h > 0);", " J4 = n; /* more bits, when needed */", " j1 = (n^(n>>(8*sizeof(long)-ssize)))&((1<<(ssize-3))-1);", "}", "#endif", "unsigned long TMODE = 0666; /* default permission bits for trail files */", "int", "main(int argc, char *argv[])", "{ void to_compile(void);\n", " efd = stderr; /* default */", " 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 'c': upto = atoi(&argv[1][2]); break;", " case 'd': state_tables++; break;", " case 'e': every_error = 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 */", "#ifndef SAFETY", "#ifdef NP", " case 'l': a_cycles = 1; break;", "#else", " case 'l': fprintf(efd, \"error: -l disabled\");", " usage(efd); 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;", " case 'R': Nrun = atoi(&argv[1][2]); break;", " case 's': single = 1; break;", " 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(); exit(0); break;", " case 'v': verbose = 1; break;", " case 'w': ssize = atoi(&argv[1][2]); break;", " case 'X': efd = stdout; break;", " default : usage(efd); break;", " }", " argc--; argv++;", " }", " if (iterative && TMODE != 0666)", " { TMODE = 0666;", " fprintf(efd, \"warning: -T ignored when -i or -I is used\\n\");", " }", "#ifdef SC", " omaxdepth = maxdepth;", " 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\");", " exit(1);", " }", "#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\");", " exit(1);", "#endif", "#ifdef HC", "#ifdef NOCOMP", " fprintf(efd, \"error: cannot combine -DHC and -DNOCOMP\\n\");", " exit(1);", "#endif", "#ifdef BITSTATE", " fprintf(efd, \"error: cannot combine -DHC and -DBITSTATE\\n\");", " exit(1);", "#endif", "#endif", "#if defined(SAFETY) && defined(NP)", " fprintf(efd, \"error: cannot combine -DNP and -DSAFETY\\n\");", " exit(1);", "#endif", "#ifdef MA", "#ifdef BITSTATE", " fprintf(efd, \"error: cannot combine -DMA and -DBITSTATE\\n\");", " exit(1);", "#endif", " if (MA <= 0)", " { fprintf(efd, \"usage: -DMA=N with N > 0 and < VECTORSZ\\n\");", " exit(1);", " }", "#endif", "#ifdef COLLAPSE", "#if defined(BITSTATE)", " fprintf(efd, \"error: cannot combine -DBITSTATE and -DCOLLAPSE\\n\");", " exit(1);", "#endif", "#if defined(NOCOMP)", " fprintf(efd, \"error: cannot combine -DNOCOMP and -DCOLLAPSE\\n\");", " exit(1);", "#endif", "#endif", " if (maxdepth <= 0 || ssize <= 0) 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\");", " exit(1);", " }", "#endif", "#if defined(NOCOMP) && !defined(BITSTATE)", " if (a_cycles)", " { fprintf(efd, \"error: -DNOCOMP voids -l and -a\\n\");", " 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\");", " exit(1);", "#endif", "#if defined(HAS_PCVALUE)", " fprintf(efd, \"error: reduced search precludes \");", " fprintf(efd, \"use of 'pcvalue()'\\n\");", " exit(1);", "#endif", "#if defined(HAS_BADELSE)", " fprintf(efd, \"error: reduced search precludes \");", " fprintf(efd, \"using 'else' combined with i/o stmnts\\n\");", " exit(1);", "#endif", "#if defined(HAS_LAST)", " fprintf(efd, \"error: reduced search precludes \");", " fprintf(efd, \"use of _last\\n\");", " 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, could make p.o. reduction\\n\");", " fprintf(efd, \"\tinvalid (use -DNOREDUCE to avoid this)\\n\");", "#endif", "#endif", "#if !defined(REACH) && !defined(BITSTATE)", " if (iterative != 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(FULLSTACK) && defined(CNTRSTACK)", " fprintf(efd, \"error: cannot combine\");", " fprintf(efd, \" -DFULLSTACK and -DCNTRSTACK\\n\");", " exit(1);", "#endif", "#ifdef VERI", "#if ACCEPT_LAB>0", " if (!a_cycles && !state_tables)", " { fprintf(efd, \"warning: never-claim + accept-labels \");", " fprintf(efd, \"requires -a flag to fully verify\\n\");", " }", "#endif", "#endif", "#ifndef SAFETY", " if (!a_cycles && !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);", " mask = ((1< 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;", "}\n", "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-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 endstates\\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 choose other hash-function 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\");", "#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", " 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 endstates\\n\");", "#ifdef BITSTATE", " fprintf(fd, \"\t-RN repeat run Nx with N \");", " fprintf(fd, \"[1..32] independent hash functions\\n\");", "#endif", " fprintf(fd, \"\t-s 1-bit hashing (default is 2-bit)\\n\");", " 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;", "#ifdef MEMCNT", " if (memcnt+ (double) n > memlim) goto err;", "#endif", "#ifdef PC", " tmp = (char *) malloc(n);", "#else", " tmp = (char *) sbrk(n);", "#endif", " if (tmp == (char *) -1L)", /* was: if ((int)tmp == -1) */ " {", "err:", " printf(\"pan: out of memory\\n\");", "#ifdef MEMCNT", " printf(\"\t%%g bytes used\\n\", memcnt);", " printf(\"\t%%g bytes more needed\\n\", (double) n);", " printf(\"\t%%g bytes limit (2^MEMCNT)\\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();", " }", "#ifdef MEMCNT", " memcnt += n;", "#endif", " 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 (left < (long) n)", " { grow = (n < CHUNK) ? CHUNK : n;", "#ifdef PC", " 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; char ot, m; short tt; short II, i;\n", " 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;", " ((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", "void", "uerror(char *str)", "{ static char laststr[256];\n", " if (strcmp(str, laststr))", " printf(\"pan: %%s (at depth %%d)\\n\", str,", " (depthfound==-1)?depth:depthfound);", " strcpy(laststr, str);", " errors++;", " if (every_error != 0", " || errors == upto)", " {", "#if defined(MA) && !defined(SAFETY)", " if (strstr(str, \" cycle\"))", " { int od = depth;", " depthfound = Unwind();", " depth = od;", " }", "#endif", " putrail();", "#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 (iterative != 0 && maxdepth > 0)", " { maxdepth = (iterative == 1)?(depth-1):(depth/2);", " warned = 1;", " printf(\"pan: reducing search depth to %%d\\n\",", " maxdepth);", " } else if (errors >= upto && upto != 0)", " wrapup();", " depthfound = -1; /* tripakis */", "}\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 (which[i] == 0 && trans[M][i])", " xrefsrc((int) src[i], mp, M, i);", " else", " m++;", " printf(\"\t(%%d of %%d states)\\n\", N-1-m, N-1);", "}\n", "void", "xrefsrc(int lno, S_F_MAP *mp, int M, int i)", "{ Trans *T; int j;", " for (T = trans[M][i]; T; T = T->nxt)", " if (T && T->tp)", " { 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)", " printf(\", \\\"%%s\\\"\", T->tp);", " else if (stopstate[M][i])", " printf(\", -endstate-\");", " printf(\"\\n\");", " }", "}\n", "void", "putrail(void)", "{ int fd; long i, j;", " Trail *trl;", " char snap[64], fnm[256];", " if (iterative == 0 && Nr_Trails++ > 0)", " sprintf(fnm, \"%%s%%d.%%s\",", " TrailFile, Nr_Trails, tprefix);", " else", " sprintf(fnm, \"%%s.%%s\",", " TrailFile, tprefix);", " if ((fd = creat(fnm, TMODE)) <= 0)", " { printf(\"cannot create %%s\\n\", fnm);", " perror(\"cause\");", " 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_pm&128) continue;", " sprintf(snap, \"%%d:%%d:%%d\\n\", ", " i, trl->pr, trl->o_t->t_id);", " j = strlen(snap);", " if (write(fd, snap, j) != j)", " { printf(\"pan: error writing %%s\\n\", fnm);", " close(fd);", " wrapup();", " }", " }", " printf(\"pan: wrote %%s\\n\", fnm);", " close(fd);", "}\n", "void", "sv_save(char *won) /* 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), won, vsize);", "#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 (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] = 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)", "{ int k; char *z = (char *) &now;\n", " q_offset[now._nr_qs] = stack->o_offset;", " q_skip[now._nr_qs] = 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 = stack->o_offset - stack->o_skip;", "#if SYNC", " if (q_zero(now._nr_qs)) k += stack->o_delta;", "#endif", " for ( ; k < stack->o_offset; k++)", " Mask[k] = 1; /* align */", "#endif", " if (!stack->lst) /* debugging */", " Uerror(\"error: q_restor\");", " stack = stack->lst;", "}", "typedef struct IntChunks {", " int *ptr;", " struct IntChunks *nxt;", "} IntChunks;", "IntChunks *filled_chunks[128];", "IntChunks *empty_chunks[128];", "int *", "grab_ints(int nr)", "{ IntChunks *z;", " if (nr >= 128) 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;", "}", #if 0 "void", "p_q_restor(int h, int K)", "{ int k = K-1;", " if (!stack || !stack->lst || !stack->lst->lst)", " Uerror(\"error: p_q_restor\");", " /* restore globals */", " memcpy((char *)&now, stack->body, sizeof(State)-VECTORSZ);", " stack = stack->lst;", " memcpy((char *) qptr(k), stack->body, Maxbody);", " stack = stack->lst;", "#if SYNC", " boq = stack->o_boq;", "#endif", " memcpy((char *) pptr(h), stack->body, Maxbody);", " stack = stack->lst;", "}", "Stack *", "p_q_frame(void)", "{ if (!stack->nxt)", " { stack->nxt = (Stack *)", " emalloc(sizeof(Stack));", " stack->nxt->body = ", " emalloc(Maxbody*sizeof(char));", " stack->nxt->lst = stack;", " smax++;", " }", " return stack->nxt;", "}", "void", "p_q_save(int h, int K)", "{ int k = K-1;", " stack = p_q_frame();", " memcpy(stack->body, (char *)pptr(h), Maxbody);", "#if SYNC", " stack->o_boq = boq;", "#endif", " stack = p_q_frame();", " memcpy(stack->body, (char *)qptr(k), Maxbody);", " /* save globals */", " stack = p_q_frame();", " memcpy(stack->body, (char *)&now, sizeof(State)-VECTORSZ);", "}", "void", "bup_q(int h, int K)", "{", "#if VECTORSZ<=1024", " sv_save((char *)&now);", "#else", " p_q_save(h, K);", "#endif", "}", "void", "unbup_q(int h, int K)", "{", "#if VECTORSZ<=1024", " sv_restor();", "#else", " p_q_restor(h, K);", "#endif", "}", #endif "int", "delproc(int sav, int h)", "{ int d, i=0, o_vsize = vsize;\n", " 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];", " stack->o_skip = proc_skip[h];", "#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 -= 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];", " stack->o_skip = q_skip[h];", "#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 -= 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)", "{ S_Tab = (struct H_el **)", " emalloc((1<<(ssize-3))*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 && v->tagged >= n; v=v->nxt)", " { if (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 && 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", "#ifdef HYBRID_HASH", "ordinal(char *v, long N, short tp) /* store components */", "{ struct H_el *tmp, *ntmp; long n, m;", " struct H_el *olst = (struct H_el *) 0;", " n = s_hash((uchar *)v, N);", "#else", "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);", "#endif", " 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);", " 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++;", " }", "#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 < 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;", " r_hash((uchar *)vin, n); /* sets J3 and J4 */", "#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 *) &J3, sizeof(long));", " delta += sizeof(long);", "#if HC>0", " memcpy((char *) &comp_now + delta, (char *) &J4, 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)", "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))", "#ifdef HYBRID_HASH", " n = ", "#endif", " 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 = 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 (w->tagged <= n)", " { if (last)", " { 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, 3) != 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))", "#ifdef HYBRID_HASH", " n = ", "#endif", " 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 = tmp;", " break;", " } }", " PROBE++;", " return (m == 0);", "}", "#endif", "#ifndef BITSTATE", "void", "hinit(void)", "{", "#ifdef MA", "#ifdef R_XPT", " { void r_xpoint(void);", " r_xpoint();", " }", "#else", " dfa_init(MA+a_cycles);", "#endif", "#endif", "#if !defined(MA) || defined(COLLAPSE)", " H_tab = (struct H_el **)", " emalloc((1<= MA)", " { printf(\"pan: error, MA too small, recompile pan.c\");", " printf(\" with -DMA=N with N>%%d\\n\", n);", " Uerror(\"aborting\");", " }", " if (n > maxgs) maxgs = n;", " for (i = 0; i < n; i++)", " Info[i] = ((uchar *)&comp_now)[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 */", " trpt->proviso = dfa_member(MA-1);", " 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;", " r_hash((uchar *)vin, n); /* sets J3 and J4 */", "#ifndef SAFETY", " delta++; /* room for state[0] |= 128 */", "#endif", " memcpy((char *) &comp_now + delta, (char *) &J3, sizeof(long));", " delta += sizeof(long);", " memcpy((char *) &comp_now + delta, (char *) &J4, sizeof(long));", " delta += sizeof(long); /* use all available bits */", " return delta;", "}", "#endif", "int", "hstore(char *vin, int nin, short xx)", "{ struct H_el *tmp, *ntmp, *olst = (struct H_el *) 0;", " char *v; int n, m=0;", "#ifdef NOCOMP", "#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;", " n = compress(vin, nin);", "#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))", "#ifdef HYBRID_HASH", " n = ", "#endif", " 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 = 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 = 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--;", " return 0;", " }", "#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 */", "Append: 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", "#ifdef 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 = tmp;", "#else", "#ifdef DEBUG", " dumpstate(-1, v, n, 0);", "#endif", "#endif", " return 0;", "}", "#endif", "#include TRANSITIONS", "void", "do_reach(void)", "{", 0, };