/***** spin: pangen1.h *****/ /* Copyright (c) 1991,1995 by AT&T Corporation. 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.att.com */ char *Code2[] = { /* the tail of procedure run() */ "#if defined(VERI) && defined(PARTIAL)", " if (!state_tables)", " { printf(\"warning: the reduction may be invalid if \");", " printf(\"the never claim is not stutter-closed\\n\");", " printf(\"(note: never claims derived from next-time-free \");", " printf(\"LTL formulae are stutter-closed)\\n\");", " }", "#endif", " UnBlock; /* disable rendez-vous */", "#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 VERI", " Addproc(VERI); /* never - pid = 0 */", "#endif", " active_procs(); /* started after never */", "go_again:", " depth=mreached=0;", " trpt = &trail[depth];", "#ifdef VERI", " trpt->tau |= 4; /* the claim moves first */", "#endif", " if (a_cycles)", " for (i = 0; i < now._nr_pr; i++)", " { P0 *ptr = (P0 *) pptr(i);", " if (accpstate[ptr->_t][ptr->_p])", " {", "#ifdef CHECK", " if (!(trpt->o_pm&2))", " printf(\"initial state is accepting\\n\");", "#endif", " trpt->o_pm |= 2;", " }", " if (progstate[ptr->_t][ptr->_p])", " {", "#ifdef CHECK", " if (!(trpt->o_pm&4))", " printf(\"initial state is progress\\n\");", "#endif", " trpt->o_pm |= 4;", " }", " }", "#ifndef NOCOMP", " Mask[0] = Mask[1] = 1; /* _nr_pr, _nr_qs implicit in vsize */", " if (!a_cycles && !np_cycles)", " { i = &(now._a_t) - (unsigned char *) &now;", " Mask[i] = 1;", " }", " if (!fairness)", " { int j = 0;", " i = &(now._cnt[0]) - (unsigned char *) &now;", " while (j++ < NFAIR)", " Mask[i++] = 1;", " }", "#endif", " if (fairness", " && (( a_cycles && (trpt->o_pm&2))", " || (np_cycles && !(trpt->o_pm&4))))", " { now._a_t = 2; /* set the A-bit */", " now._cnt[0] = now._nr_pr;", "#ifdef VERBOSE", " printf(\"%%3d: fairness Rule 1, cnt=%%d, _a_t=%%d\\n\",", " depth, now._cnt[now._a_t&1], now._a_t);", "#endif", " }", " new_state(); /* start 1st DFS */", "#ifdef 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(FULLSTACK)", " memset((uchar *) S_tab, 0, (1<<(ssize-3))*sizeof(struct H_el *));", "#endif", "#ifdef CNTRSTACK", " memset(LL, 0, 1<<(ssize-3));", "#endif", " nstates=nlinks=truncs=truncs2 = 0;", " nlost=nShadow=hcmp = 0;", " Fa=Fh=Zh=Zn = 0;", " PUT=PROBE=ZAPS=Ccheck=Cholds = 0;", " goto go_again;", " }", "#endif", "}", "#ifndef INLINE", "char", "do_transit(Trans *t, short II, int n)", "{ char m;", " short tt = (short) ((P0 *)this)->_p;", "#define continue return 0", "#include \"pan.m\"", "P999: return m;", "#undef continue", "}", "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 >= 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", "new_state(void)", "{ register Trans *t;", " char n, m, ot;", " short II, JJ=0, tt;\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", " trpt->tau &= ~(16|32|64); /* make sure these bits are off */", "#if PROG_LAB>0", " if (np_cycles", " && (now._a_t&1)", " && (trpt->o_pm&4))", " { (trpt-1)->tau |= 16; /* pm for 1 level up */", " goto Up; /* no move through progstates */", " }", "#endif", " if (depth >= maxdepth)", " { static unsigned char warned=0;", " 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;", " }", "#if defined(FULLSTACK)", " 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 */", " { /* 2nd dfs, cycle check: */", " if ((now._a_t&1) && depth > A_depth)", " { if (!memcmp((char *)&A_Root, (char *)&now, vsize))", " {", "#ifdef CHECK", " printf(\"matches seed\\n\");", "#endif", " if (a_cycles)", " uerror(\"acceptance cycle\");", " else if (np_cycles)", " uerror(\"non-progress cycle\");", " goto Up;", " }", "#ifdef CHECK", " printf(\"not seed\\n\");", "#endif", " }", " if (!(trpt->tau&8)) /* if no atomic move */", " {", "#ifdef CNTRSTACK", " d_hash((uchar *)&now, vsize);", " trpt->j6 = j1; trpt->j7 = j2;", " JJ = LL[j1] && LL[j2];", "#endif", "#ifdef FULLSTACK", "#if defined(BITSTATE)", " JJ = onstack_now();", "#else", " II = hstore((char *)&now, vsize, 1);", " JJ = (II == 2)?1:0;", "#endif", "#endif", "#ifdef BITSTATE", "#if !defined(CNTRSTACK)", " d_hash((uchar *) &now, vsize);", "#endif", " II = ((SS[j2]&j3) && (SS[j1]&j4));", "#else", "#if !defined(FULLSTACK)", " II = hstore((char *)&now, vsize, 2);", "#endif", "#endif", "#if !defined(FULLSTACK) && !defined(CNTRSTACK)", " JJ = II; /* no stack - worstcase guess */", "#endif", " if (II && JJ) /* must do full shuffle elsewhere */", " { truncs2++;", " (trpt-1)->tau |= 16;", " }", "#if defined(SAFETY_ONLY)", " else /* has successors outside stack */", " (trpt-1)->tau |= 64;", "#endif", " if (II || JJ)", " { truncs++;", " goto Up;", " }", " nstates++;", "#ifdef BITSTATE", " SS[j2] |= j3; SS[j1] |= j4;", "#endif", "#if defined(FULLSTACK) || defined(CNTRSTACK)", " onstack_put();", "#ifdef DEBUG", "#ifdef FULLSTACK", " 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; /* timeout off */", " trpt->tau &= ~2; /* timeout request off */", " }", " n = 0;", "#if SYNC", " (trpt+1)->o_n = 0;", "#endif", "#ifdef VERI", " if (now._nr_pr == 0 /* claim terminated */", " || ((P0 *)pptr(0))->_p == endclaim)", " uerror(\"claim violated!\");", " if (stopstate[VERI][((P0 *)pptr(0))->_p])", " uerror(\"endstate in claim reached\");", "Stutter:", " if (trpt->tau&4) /* must make a claimmove */", " { II = 0; /* never */", " goto Veri0;", " }", "#endif", "#ifdef PARTIAL", " /* Attempt to preselect a process with only safe transitions */", " if (boq == -1 && From != To)", " for (II = From; II >= To; II -= 1)", " {", "Resume: /* pick up here if a 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)", "#ifndef NOCOND", " { Ccheck++;", " if (!q_cond(t))", " continue;", " Cholds++;", " }", "#else", " continue;", "#endif", " From = To = II;", "#ifdef NIBIS", " t->om = 0;", "#endif", " trpt->tau |= 32; /* preselect marker */", "#ifdef DEBUG", "#ifdef NIBIS", " printf(\"%%3d: proc %%d PreSelected (om=%%d, tau=%%d)\\n\", ", " depth, II, 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);", /* clear all fairness-marks */ " 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))", " || (np_cycles && !(trpt->o_pm&4)))", " { /* Accepting state */", " now._a_t |= 2;", " now._cnt[now._a_t&1] = now._nr_pr;", " 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] == 0)", " { now._a_t &= ~2;", " trpt->o_pm |= 16;", "#ifdef DEBUG", " printf(\"%%3d: fairness Rule 3: _a_t = %%d\\n\",", " depth, now._a_t);", "#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(t))", /* true condition */ " { m = t->om;", " if (m>n||(n>3&&m!=0)) n=m;", " continue; /* did it before */", " } }", "#endif", " /* Fairness: Cnt++ when Cnt == II */", " trpt->o_pm &= ~1; /* no move in this pid yet */", " trpt->o_pm &= ~64; /* didn't apply rule 2 */", " if (fairness", " && !(trpt->o_pm&32)", /* rule 2 not already in effect */ " && (now._a_t&2)", /* A-bit is set */ " && now._cnt[now._a_t&1] == II+1)", /* Cnt == II */ " { now._cnt[now._a_t&1] -= 1;", "#ifdef VERI", " /* claim need not participate */", " if (now._cnt[now._a_t&1] == 1)", " now._cnt[now._a_t&1] = 0;", "#endif", "#ifdef DEBUG", " printf(\"%%3d: proc %%d fairness Rule 2: --cnt to %%d (%%d)\\n\",", " depth, II, now._cnt[now._a_t&1], now._a_t);", "#endif", " trpt->o_pm |= (32|64);", " }", " /* check all transitions of process II - escapes first */", "#ifdef HAS_UNLESS", " trpt->e_state = 0;", "#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 (already did %%d)\\n\",", " t->e_trans, trpt->e_state);", "#endif", " break;", " }", "#endif", "#ifdef INLINE", "#include \"pan.m\"", "#else", " if (!(m = do_transit(t, II, n))) continue;", "#endif", "P999: /* jumps here when move succeeds */", " if (boq == -1)", " trpt->o_pm |= 1; /* we moved */", "#ifdef PEG", " peg[t->forw]++;", "#endif", "#if defined(VERBOSE) || defined(CHECK)", " printf(\"%%3d: proc %%d exec %%d, %%d to %%d, %%s %%s %%s\", ", " depth, II, t->forw, 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_LAST", "#ifdef VERI", " if (II != 0) now._last = II-1;", "#else", " now._last = II;", "#endif", "#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;", " reached[ot][t->st] = 1;", " }", " { register int ii;", "#define PQ ((P0 *)pptr(ii))", "#if ACCEPT_LAB>0", " if (a_cycles)", " for (ii = 0; ii < now._nr_pr; ii++)", " { if (accpstate[PQ->_t][PQ->_p])", " { trpt->o_pm |= 2;", " break;", " } }", "#endif", "#if PROG_LAB>0", " if (np_cycles)", " for (ii = 0; ii < now._nr_pr; ii++)", " { if (progstate[PQ->_t][PQ->_p])", " { trpt->o_pm |= 4;", " break;", " } }", "#endif", "#undef PQ", " }", " 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", " if (trpt->o_pm&128) /* fairness alg */", " { now._cnt[now._a_t&1] = trpt->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;", " }", "#ifdef HAS_LAST", "#ifdef VERI", " if (trpt->pr != 0)", " { if (depth <= 4)", " now._last = 0;", " else", " now._last = (trpt-4)->pr - 1;", " }", "#else", " now._last = (depth<2)?0:(trpt-2)->pr - 1;", "#endif", "#endif", " if ((now._a_t&1) && depth <= A_depth)", " return; /* we came from checkcycles() */", " 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;", "#include \"pan.b\"", "R999: /* jumps here when done */", "#ifdef VERBOSE", " printf(\"%%3d: proc %%d reverses %%d, %%d to %%d,\",", " depth, II, t->forw, tt, t->st);", " printf(\" %%s [abit=%%d,adepth=%%d,tau=%%d,%%d]\\n\", ", " t->tp, now._a_t, A_depth,", " trpt->tau, (trpt-1)->tau);", "#endif", "#ifdef PARTIAL", " /* pass the proviso tags */", " if ((trpt->tau&8) /* rv or atomic */", " && (trpt->tau&16))", " (trpt-1)->tau |= 16;", "#if defined(SAFETY_ONLY)", " 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; /* mark at head of list */", "#endif", " if (m>n||(n>3&&m!=0)) n=m;", " ((P0 *)this)->_p = tt;", " } /* all options */", " /* 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] == 0)", " now._cnt[now._a_t&1] = 1;", "#endif", " now._cnt[now._a_t&1] += 1;", "#ifdef VERBOSE", "printf(\"%%3d: proc %%d fairness undo Rule 2, cnt=%%d, _a_t=%%d\\n\",", " depth, II, now._cnt[now._a_t&1], now._a_t);", "#endif", " trpt->o_pm &= ~(32|64);", " } else", /* the process blocked */ " { if (n > 0)", /* previous proc didn't */ " {", /* start over */ " trpt->o_pm &= ~64;", " II = From+1;", " } } }", "#ifdef VERI", " if (II == 0) break; /* never claim */", "#endif", " } /* all processes */", " /* Fairness: undo Rule 2 */", " if (trpt->o_pm&32) /* remains if proc blocked */", " {", "#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;", "#ifdef VERBOSE", "printf(\"%%3d: proc -- fairness undo Rule 2, cnt=%%d, _a_t=%%d\\n\",", " depth, now._cnt[now._a_t&1], now._a_t);", "#endif", " trpt->o_pm &= ~32;", " }", /* new */ " 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) /* we've already tried timeout */", "#endif", "#endif", "#ifdef PARTIAL", "#ifdef SAFETY_ONLY", " && !((trpt->tau&32) && !(trpt->tau&64))", "#else", " && !((trpt->tau&32) && (n == 0 || (trpt->tau&16)))", "#endif", "#endif", " && now._cnt[now._a_t&1] > 0) /* we needed to move more procs */", " { depth++; trpt++;", " trpt->o_pm |= 128 | ((trpt-1)->o_pm&(2|4));", " trpt->oval = now._cnt[now._a_t&1];", " now._cnt[now._a_t&1] = 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 (all procs block)\\n\", depth);", "#endif", " goto Down;", " }", "Q999: /* returns here with n>0 when done */;", /* end */ " 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;", " trpt->o_pm &= ~16;", "#ifdef VERBOSE", " printf(\"%%3d: fairness undo Rule 3, _a_t=%%d\\n\",", " depth, now._a_t);", "#endif", " }", "#ifdef PARTIAL", "#ifdef SAFETY_ONLY", " /* preselected move produced at least one */", " /* successor state outside the stack */", " if ((trpt->tau&32) && !(trpt->tau&64))", " {", " if (!(n == 0 || (trpt->tau&16)))", " Uerror(\"cannot happen, can it?...\");", "#else", " /* at least one move that was preselected at this */", " /* level, blocked or truncated at the next level */", " if ((trpt->tau&32) && (n == 0 || (trpt->tau&16)))", " {", "#endif", " 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) /* it was already decremented */", " goto Resume;", " else", " goto Again;", " }", "#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", " /* it's ok if a rendez-vous fails: */", " if (boq != -1) goto Done;", "#endif", " /* it's ok if all procs terminated or we're at maxdepth */", " if (now._nr_pr == 0", "#ifdef OTIM", " || endstate()", "#endif", " || depth >= maxdepth-1) goto Done;", "#ifdef ETIM", " if (!(trpt->tau&1)) /* we didn't try timeout yet */", " {", "#ifdef VERI", " if (trpt->tau&4)", " {", "#ifndef NTIM", " if (trpt->tau&2) /* only on request */", "#endif", " { trpt->tau |= 1;", " trpt->tau &= ~2;", "#ifdef DEBUG", " printf(\"%%d: timeout\\n\", depth);", "#endif", " goto Stutter;", " } }", " else", " { /* only the claim can enable timeout */", "#ifdef DEBUG", " printf(\"%%d: req timeout\\n\", depth);", "#endif", " (trpt-1)->tau |= 2; /* request it */", " goto Up;", " }", "#else", "#ifdef DEBUG", " printf(\"%%d: timeout\\n\", depth);", "#endif", " trpt->tau |= 1;", " goto Again;", "#endif", " }", "#endif", " 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 unexecutable\\n\", depth, II);", "#endif", " goto Again;", " }", "#ifdef VERI", "#ifndef NOSTUTTER", " if ((now._a_t&1) && !(trpt->tau&4))", " { trpt->tau |= 4; /* try claim stuttering */", " trpt->tau |= 128; /* stutter mark */", "#ifdef DEBUG", " printf(\"%%d: claim stutter\\n\", depth);", "#endif", " goto Stutter;", " }", "#endif", "#else", " if (!endstate() && !(np_cycles || a_cycles))", " uerror(\"invalid endstate\");", "#endif", " }", "Done:", " if (!(trpt->tau&8)) /* not in atomic seqs */", " {", " if (n != 0", /* we made a move */ "#ifdef VERI", " /* --after-- a program-step, i.e., */", " /* after backtracking a claim-step */", " && (trpt->tau&4)", "#endif", " && !(now._a_t&1))", /* not in 2nd DFS */ " { 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] == 0))", " checkcycles();", " } else", " if (((np_cycles && !(trpt->o_pm&4))", /* !prog */ " || ( a_cycles && (trpt->o_pm&2))))", /* accpt */ " checkcycles();", " }", "#if defined(FULLSTACK) || defined(CNTRSTACK)", "#ifdef VERI", " if (boq == -1", " && (((trpt->tau&4) && !(trpt->tau&128))", " || (!(trpt->tau&4) && ((trpt-1)->tau&128))))", "#else", " if (boq == -1)", "#endif", " {", "#ifdef DEBUG", "#ifdef FULLSTACK", " printf(\"%%d: zapping %%u\\n\", depth, trpt->ostate);", "#else", " printf(\"%%d: zapping\\n\", depth);", "#endif", "#endif", " onstack_zap();", " }", "#endif", " }", " if (depth > 0) goto Up;", "}\n", "void", "assert(int a, char *s, int ii, int tt, Trans *t)", "{", " if (!a)", " { char bad[250];", " sprintf(bad, \"assertion violated %%s\", s);", " depth++; trpt++;", " trpt->pr = ii;", " trpt->st = tt;", " trpt->o_t = 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", "#ifdef MEMCNT", "double memcnt=0;", "double memlim = (double) (1<<30);", "#endif", "void", "wrap_stats(void)", "{ double a, b;\n", " 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);", "/* printf(\"%%8g matches outside stack\\n\", truncs-truncs2); */", " 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", " a = (double) (1< 100.)", " 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 (single-bit hash) if >1000)\\n\");", " }", "#else", " printf(\"hash conflicts: %%g (resolved)\\n\", hcmp);", "#endif", "}", "void", "wrapup(int arg)", "{ signal(SIGINT, SIG_DFL);", " printf(\"(%%s)\\n\", Version);", "#ifdef PARTIAL", " printf(\" + Partial Order Reduction\\n\");", "#endif", #if 0 "#ifdef FULLSTACK", " printf(\" + FullStack Matching\\n\");", "#endif", "#ifdef CNTRSTACK", " printf(\" + CntrStack Matching\\n\");", "#endif", #endif "#ifdef BITSTATE", " printf(\"\\nBit statespace search for:\\n\");", "#else", " printf(\"\\nFull statespace search for:\\n\");", "#endif", "#ifdef VERI", " printf(\"\tnever-claim \t+\\n\");", " printf(\"\tassertion violations\t+ (those 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+\\n\");", "#endif", " printf(\"\tnon-progress cycles \t\");", " if (np_cycles)", " printf(\"+ (fairness %%sabled)\\n\",", " fairness?\"en\":\"dis\");", " else printf(\"- (not selected)\\n\");", " printf(\"\tacceptance cycles\t\");", " if (a_cycles)", " printf(\"+ (fairness %%sabled)\\n\",", " fairness?\"en\":\"dis\");", " else printf(\"- (not selected)\\n\");", "#ifdef VERI", " printf(\"\tinvalid endstates\t- (disabled by never-claim)\\n\\n\");", "#else", " printf(\"\tinvalid endstates\t+\\n\\n\");", "#endif", " if (!done) printf(\"Search was not completed\\n\");", " printf(\"State-vector %%d byte, depth reached %%d\", ", " hmax, mreached);", " printf(\", errors: %%d\\n\", errors);", " wrap_stats();", " printf(\"(max size 2^%%d states\", ssize);", #if 0 " printf(\", stackframes: %%d/%%d)\\n\\n\", smax, svmax);", " printf(\"statistics: fa %%d, fh %%d, zh %%d, zn %%d - check %%d holds %%d\\n\",", " Fa, Fh, Zh, Zn, Ccheck, Cholds);", " printf(\"Statistics: put %%d, probe %%d, zaps %%d\\n\",", " PUT, PROBE, ZAPS);", #else " printf(\")\\n\\n\");", #endif "#ifdef MEMCNT", "#ifdef BITSTATE", " if (memcnt < (nstates-nShadow)*hmax + (maxdepth * sizeof(Trail))) {", " printf(\"%%8g equivalent memory usage (stored*vector + stack)\\n\",", " (nstates-nShadow)*(double)hmax + (double)(maxdepth * sizeof(Trail)));", " printf(\"%%8g actual memory usage (bytes)\\n\\n\", memcnt);", " } else", "#endif", " printf(\"%%8g memory usage (bytes)\\n\\n\", memcnt);", "#endif", " if (done && !np_cycles && !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", " exit(0);", "}\n", "void", "db_hash(uchar *cp, int om)", "{ register int z = (int) HASH_CONST[HASH_NR];", " register int *q, *r;", " register int h;", " register m, n;\n", " h = (om+sizeof(int)-1)/sizeof(int);", " m = n = -1;", " q = r = (int *) cp;", " r += (int) 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(int)-ssize)))&mask;", " J2 = (n ^ (n>>(8*sizeof(int)-ssize)))&mask;", " j3 = (1<<(J1&7)); j1 = J1>>3;", " j4 = (1<<(J2&7)); j2 = J2>>3;", "}\n", "void", "sbf_hash(uchar *cp, int om)", "{ register int z = (int) HASH_CONST[HASH_NR];", " register int *q;", " register int h;", " register m;\n", " h = (om+sizeof(int)-1)/sizeof(int);", " m = -1;", " q = (int *) cp;", " do {", " if (m < 0)", " { m += m;", " m ^= z;", " } else", " m += m;", " m ^= *q++;", " } while (--h > 0);", " J1 = (m ^ (m>>(8*sizeof(int)-ssize)))&mask;", " j3 = (1<<(J1&7)); j2 = J1>>3;", " j4 = 1; j1 = 0;", "}\n", "void", "sbb_hash(uchar *cp, int om)", "{ register int z = (int) HASH_CONST[HASH_NR];", " register int *r;", " register int h;", " register n;\n", " h = (om+sizeof(int)-1)/sizeof(int);", " n = -1;", " r = (int *) cp;", " r += (int) h;", " do {", " if (n < 0)", " { n += n;", " n ^= z;", " } else", " n += n;", " n ^= *--r;", " } while (--h > 0);", " J1 = (n ^ (n>>(8*sizeof(int)-ssize)))&mask;", " j3 = (1<<(J1&7)); j2 = J1>>3;", " j4 = 1; j1 = 0;", "}\n", "void", "s_hash(uchar *cp, int om)", "{ register int z = (int) HASH_CONST[HASH_NR];", " register int *q;", " register int h;\n", " register m = -1;", " h = (om+sizeof(int)-1)/sizeof(int);", " q = (int *) 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(int)-(ssize-3))))&((1<<(ssize-3))-1);", " else", "#endif", " j1 = (m ^ (m>>(8*sizeof(int)-ssize)))&mask;", "}\n", "void", "main(int argc, char *argv[])", "{ FILE *efd = stderr; /* default */\n", " d_hash = db_hash; /* double-bit hashing */", " while (argc > 1 && argv[1][0] == '-')", " { switch (argv[1][1]) {", " case 'a': a_cycles = 1; break;", " case 'c': upto = atoi(&argv[1][2]); break;", " case 'd': state_tables++; break;", " case 'f': fairness = 1; break;", " case 'l': np_cycles = 1; break;", " case 'm': maxdepth = atoi(&argv[1][2]); break;", " case 'n': no_rck = 1; break;", " case 's': d_hash = sbf_hash; break;", " case 'z': d_hash = sbb_hash; break;", " case 'w': ssize = atoi(&argv[1][2]); break;", " case 'R': Nrun = atoi(&argv[1][2]); break;", " case 'X': efd = stdout; break;", " case 'V': printf(\"Generated by %%s\\n\", Version);", " exit(0); break;", " default : usage(efd); break;", " }", " argc--; argv++;", " }", "#ifdef MEMCNT", "#if MEMCNT<31", " memlim = (double) (1< 32)", " { fprintf(efd, \"error: argument to -R is out of range\\n\");", " usage(efd);", " }", " if (fairness)", " { if (!a_cycles && !np_cycles)", " { fprintf(efd, \"error: -f flag requires -a or -l\\n\");", " usage(efd);", " }", " }", "#if ACCEPT_LAB==0", " if (a_cycles)", " { fprintf(efd, \"error: no accept labels defined for -a\\n\");", " usage(efd);", " }", "#endif", "#if defined(PARTIAL)", "#if defined(REM_REFS)", " fprintf(efd, \"error: reduced search precludes \");", " fprintf(efd, \"use of remote references\\n\");", " usage(efd);", "#endif", "#if !defined(INLINE)", " fprintf(efd, \"error: reduced search precludes \");", " fprintf(efd, \"use of 'enabled()'\\n\");", " usage(efd);", "#endif", "#if defined(HAS_LAST)", " fprintf(efd, \"error: reduced search precludes \");", " fprintf(efd, \"use of _last\\n\");", " usage(efd);", "#endif", "#if !defined(FULLSTACK) && !defined(CNTRSTACK) && !defined(BITSTATE)", " fprintf(efd, \"hint: adding -DFULLSTACK or -DCNTRSTACK \");", " fprintf(efd, \"may reduce statespace\\n\");", "#endif", "#else", "#if (defined(FULLSTACK) || defined(CNTRSTACK))", " fprintf(efd, \"hint: adding -DPARTIAL reduces statespace\\n\");", "#endif", "#endif", "#if defined(BITSTATE) && defined(REACH)", " fprintf(efd, \"warning: -DREACH has no effect in a bitstate search\\n\");", "#endif", "#if defined(FULLSTACK) && defined(CNTRSTACK)", " fprintf(efd, \"error: cannot combine -DFULLSTACK and -DCNTRSTACK\\n\");", " usage(efd);", "#endif", "#ifdef VERI", "#if ACCEPT_LAB>0", " if (!a_cycles)", " { fprintf(efd, \"warning: a never-claim + accept-labels \");", " fprintf(efd, \"requires -a flag to fully verify\\n\");", " }", "#endif", "#endif", "#ifndef NOCOMP", " if (!a_cycles && !np_cycles)", " S_A = 0;", " else", " { if (!fairness)", " S_A = 1; /* skip _a_t */", " else /* skip _a_t and _cnt[NFAIR] */", " S_A = (&(now._cnt[0]) - (uchar *) &now) + NFAIR;", " }", "#endif", " signal(SIGINT, wrapup);", " mask = ((1< memlim) goto err;", "#endif", " tmp = malloc(n);", " if (!tmp)", " {", "err: printf(\"pan: out of memory\\n\");", "#ifdef MEMCNT", " printf(\" %%g bytes used\\n\", memcnt);", " printf(\" %%g bytes more needed\\n\", (double) n);", " printf(\" %%g bytes limit (2^MEMCNT)\\n\", memlim);", "#endif", " wrapup(0);", " }", "#ifdef MEMCNT", " memcnt += (double) n;", "#endif", " memset(tmp, 0, n);", " return tmp;", "}\n", #else "/* include realloc and free to keep sysV libc", " * from including them and", " * finding multiple references", " */", "char *", "realloc(char *s)", "{ printf(\"aborting: cannot happen - call on realloc()\\n\");", " wrapup(0);", " return (char *)0; /* doesn't get here */", "}", "void", "free(void *s)", "{ /* never called - simply ignore it */", "}", "", "char *", "malloc(unsigned n)", "{ char *tmp;", "#ifdef MEMCNT", " if (memcnt+ (double) n > memlim) goto err;", "#endif", " tmp = (char *) sbrk(n);", " if ((int) tmp == -1)", " {", "err: printf(\"pan: out of memory\\n\");", "#ifdef MEMCNT", " printf(\" %%g bytes used\\n\", memcnt);", " printf(\" %%g bytes more needed\\n\", (double) n);", " printf(\" %%g bytes limit (2^MEMCNT)\\n\", memlim);", "#endif", " wrapup(0);", " }", "#ifdef MEMCNT", " memcnt += n;", "#endif", " return tmp;", "}", "", "#define CHUNK 4096", "", "char *", "emalloc(unsigned n) /* memory is never released or reallocated */", "{ char *tmp;", " static char *have;", " static long left = 0L;", " static long fragment = 0L;\n", " if (n == 0)", " return (char *) NULL;", " if (n&(sizeof(void *)-1)) /* for proper alignment */", " n += sizeof(void *)-(n&(sizeof(void *)-1));", " if (left < n)", " { unsigned grow = (n < CHUNK) ? CHUNK : n;", " have = malloc(grow);", " fragment += left;", " left = grow;", " }", " tmp = have;", " have += (long) n;", " left -= (long) n;", "", " memset(tmp, 0, n);", " return tmp;", "}", #endif "void", "Uerror(char *str)", "{ /* always fatal */", " uerror(str);", " wrapup(0);", "}\n", "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);", " if (++errors == upto)", " { putrail();", " wrapup(0);", " }", " strcpy(laststr, str);", "}\n", "void", "r_ck(uchar *which, int N, int M, short *src)", "{ int i, m=0;\n", "#ifdef VERI", " if (M == VERI) return; /* no useful info there */", "#endif", " printf(\"unreached in proctype %%s\\n\", procname[M]);", " for (i = 1; i < N; i++)", " if (which[i] == 0 && trans[M][i])", " xrefsrc(src[i], M, i);", " else", " m++;", " printf(\"\t(%%d of %%d states)\\n\", N-1-m, N-1);", "}\n", "void", "xrefsrc(int lno, int M, int i)", "{ Trans *T;", " for (T = trans[M][i]; T; T = T->nxt)", " if (T && T->tp)", " { printf(\"\\tline %%d, state %%d\", lno, 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, i;", " char snap[256];\n", " sprintf(snap, \"%%s.trail\", Source);", " if ((fd = creat(snap, 0666)) <= 0)", " { printf(\"cannot create %%s\\n\", snap);", " return;", " }", "#ifdef VERI", " sprintf(snap, \"-2:%%d:-2\\n\", VERI);", " write(fd, snap, strlen(snap));", "#endif", " for (i = 1; i <= depth; i++)", " { if (i == depthfound)", " write(fd, \"-1:-1:-1\\n\", 9);", " if (trail[i].o_pm&128) continue;", " sprintf(snap, \"%%d:%%d:%%d\\n\", ", " i, trail[i].pr, trail[i].o_t->t_id);", " write(fd, snap, strlen(snap));", " }", " printf(\"pan: wrote %%s.trail\\n\", Source);", " 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(int nonatom) /* pop state vector from save stack */", "{", "#if defined(FULLSTACK) && defined(NOCOMP)", " if (nonatom)", " memcpy((char *)&now, &(((struct H_el *)(trpt-1)->ostate)->state), vsize);", " else", "#endif", " { 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;", "#endif", " vsize += stack->o_skip;", " memcpy(z+vsize, stack->body, stack->o_delta);", " vsize += stack->o_delta;", "#ifndef NOCOMP", " for (i = 1; i <= Air[((P0 *)pptr(h))->_t]; i++)", " Mask[vsize - i] = 1;", " 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;", " now._nr_qs += 1;", "#ifndef NOCOMP", " k = vsize + stack->o_skip;", "#if SYNC", " if (q_zero(now._nr_qs)) k += stack->o_delta;", "#endif", " for ( ; k > vsize; k--)", " Mask[k-1] = 1;", "#endif", " if (!stack->lst) /* debugging */", " Uerror(\"error: q_restor\");", " stack = stack->lst;", "}\n", "int", "delproc(int sav, int h)", "{ int d, i=0, o_vsize = vsize;\n", " if (h+1 != 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 NOCOMP", " for (i = vsize; i < o_vsize; i++)", " Mask[i] = 0;", "#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 NOCOMP", " for (k = vsize; k < o_vsize; k++)", " Mask[k] = 0;", "#endif", "}\n", "int", "endstate(void)", "{ int i; P0 *ptr;\n", " for (i = BASE; i < now._nr_pr; i++)", " { ptr = (P0 *) pptr(i);", " if (!stopstate[ptr->_t][ptr->_p])", " return 0;", " }", " return 1;", "}\n", "void", "checkcycles(void)", "{", "#ifdef DEBUG", " { int i; uchar *v = (uchar *) &now;", " printf(\" set Seed state \");", " if (fairness) printf(\"(cnt = %%d) \", now._nr_pr);", " /* 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)= help hasher */", " if (fairness) now._cnt[1] = 0;", " memcpy((char *)&A_Root, (char *)&now, vsize);", " A_depth = depthfound = depth;", " if (fairness) now._a_t &= ~2; /* pre-apply Rule 3 */", " /* avoids matching seed on claim stutter on this state */", " new_state(); /* start 2nd DFS */", " if (fairness) now._a_t |= 2; /* undo Rule 3 */", " A_depth = 0; depthfound = -1;", " now._a_t &= ~(1|16|32);", "#ifdef DEBUG", " printf(\"%%d: cycle check returns\\n\", depth);", "#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 **)", "#ifdef BITSTATE", " emalloc((1<<(ssize-3))*sizeof(struct H_el *));", "#else", " emalloc((1<tagged >= n; Fh++, last=v, v=v->nxt)", " if (v->tagged == n)", " { if (last)", " last->nxt = v->nxt;", " else", " Free_list = v->nxt;", " v->tagged = 0;", " v->nxt = 0;", " return v;", " }", " 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", "#ifndef BITSTATE", "#ifndef NOCOMP", "short", "compress(char *vin, short n)", "{ register char *vv = vin;", " register char *v = (char *) &comp_now;", " register 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", "#if defined(FULLSTACK) && defined(BITSTATE)", "void", "onstack_zap(void)", "{ register struct H_el *v, *w, *last = 0;", " struct H_el **tmp = H_tab;", " int m;\n", "#ifndef NOCOMP", " char *nv = (char *) &comp_now;", " short n = compress((char *)&now, vsize);", "#else", " char *nv = &now;", " short n = vsize;", "#endif", " H_tab = S_tab;", " s_hash((uchar *)nv, n);", " 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;", " 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;", " hstore((char *)&now, vsize, 3);", " H_tab = tmp;", " PUT++;", "}", "int", "onstack_now(void)", "{ register struct H_el *tmp;", " struct H_el **tmp2 = H_tab;", " int m = 1;\n", "#ifndef NOCOMP", " char *v = (char *) &comp_now;", " short n = compress((char *)&now, vsize);", "#else", " char *v = &now;", " short n = vsize;", "#endif", " H_tab = S_tab;", " s_hash((uchar *)v, n);", " H_tab = tmp2;", " for (tmp = S_tab[j1]; tmp; Zn++, tmp = tmp->nxt)", " { m = memcmp(&(tmp->state), (char *)&now, vsize);", " if (m <= 0) break;", " }", " PROBE++;", " return (m == 0);", "}", "#endif", "#ifndef BITSTATE", "void", "hinit(void)", "{ H_tab = (struct H_el **)", " emalloc((1< NFAIR)", " for (m = 0; m < NFAIR; m++)", " v[m+1] = 0; /* clear the _cnt bytes */", " m = 0;", " }", "#else", " char *v = vin;", " short n = nin;", "#endif", " s_hash((uchar *)v, n);", " 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 */", " m = memcmp(((char *)&(tmp->state)) + S_A, v + S_A, n - S_A);", " if (m == 0)", " { int wasnew = 0;", "#ifndef NOCOMP", " if (S_A)", " { if ((((char *)&(tmp->state))[0] & V_A) != V_A)", " { wasnew = 1; nShadow++;", " ((char *)&(tmp->state))[0] |= V_A;", " }", " if (S_A > NFAIR)", " { /* 0 <= now._cnt[now._a_t&1] < MAXPROC */", " unsigned ci, bp; /* index and bit position */", " 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., an old state */", " }", "#endif", "#ifdef FULLSTACK", " if (wasnew)", " { tmp->tagged |= V_A;", " Lstate = tmp;", "#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 if (tmp->tagged)", " { if (xx == 3)", " Uerror(\"cannot happen - hstore\");", " Lstate = tmp;", "#ifdef CHECK", " printf(\"\tOld state %%d\\n\", (int) tmp->st_id);", "#endif", "#ifdef DEBUG", " dumpstate(0, (char *)&(tmp->state),", " n, tmp->tagged);", "#endif", " return 2;", " }", "#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;", " }", "#ifdef CHECK", " printf(\"\tOld state %%d\\n\", (int) tmp->st_id);", "#endif", "#ifdef DEBUG", " dumpstate(0, (char *)&(tmp->state), n, 0);", "#endif", "#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 */", " tmp->nxt = (struct H_el *)", " emalloc(sizeof(struct H_el)+n-sizeof(unsigned));", " tmp = tmp->nxt;", " break;", " } }", " }", "#ifdef CHECK", " tmp->st_id = (unsigned) nstates;", " printf(\" New state %%d\\n\", (int) nstates);", "#endif", "#ifdef REACH", " tmp->D = depth;", "#endif", "#ifndef NOCOMP", " if (S_A)", " { v[0] = V_A;", " 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", " memcpy(((char *)&(tmp->state)), v, n);", "#ifdef FULLSTACK", " tmp->tagged = (S_A)?V_A:(depth+1);", " Lstate = tmp;", "#ifdef DEBUG", " dumpstate(-1, v, n, tmp->tagged);", "#endif", "#else", "#ifdef DEBUG", " dumpstate(-1, v, n, 0);", "#endif", "#endif", " return 0;", "}", "#endif", "#include \"pan.t\"", "void", "do_reach(void)", "{", 0, };