/***** 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 <stdarg.h>",
"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<<ssize)*sizeof(struct H_el *);",
"#endif",
"#else",
" nr3 = (double) (1<<(ssize-3));",
"#ifdef CNTRSTACK",
" nr3 += (double) (1<<(ssize-3));",
"#endif",
"#ifdef FULLSTACK",
" overhead += (double) (1<<(ssize-3))*sizeof(struct H_el *);",
"#endif",
"#endif",
" nr4 = (double) (svmax * (sizeof(Svtack) + hmax))",
" + (double) (smax * (sizeof(Stack) + Maxbody));",
" overhead = overhead - nr2 + fragment;",
"#ifndef MA",
" if (memcnt < nr1+nr2+nr3+nr4)",
"#else",
" if (1)",
"#endif",
" { printf(\"Stats on memory usage (in Megabytes):\\n\");",
" printf(\"%%-6.3f\tequivalent memory usage for states\",",
" nr1/1000000.);",
" printf(\" (stored*(State-vector + overhead))\\n\");",
"#ifdef BITSTATE",
" printf(\"%%-6.3f\tmemory used for hash-array (-w%%d)\\n\",",
" nr3/1000000., ssize);",
"#else",
" tmp_nr = memcnt-nr3-nr4-(overhead+nr2-fragment);",
" if (tmp_nr < 0.0) tmp_nr = 0.;",
" printf(\"%%-6.3f\tactual memory usage for states\",",
" tmp_nr/1000000.);",
" printf(\" (\");",
" if (tmp_nr > 0.)",
" { if (tmp_nr > nr1)",
" printf(\"unsuccessful \");",
" printf(\"compression: %%.2f%%%%)\\n\",",
" (100.0*tmp_nr)/nr1);",
" } else",
" printf(\"less than 1k)\\n\");",
"#ifndef MA",
" if (tmp_nr > 0.)",
" { printf(\"\tState-vector as stored = %%.0f byte\",",
" (tmp_nr)/(nstates-nShadow) -",
" (double) (sizeof(struct H_el) - sizeof(unsigned)));",
" printf(\" + %%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<<MEMCNT);",
"#else",
" memlim = (double) (1<<30);",
" memlim *= (double) (1<<(MEMCNT-30));",
"#endif",
"#endif",
"#endif",
"#ifndef BITSTATE",
" if (Nrun > 1) HASH_NR = Nrun - 1;",
"#endif",
" if (Nrun < 1 || Nrun > 32)",
" { fprintf(efd, \"error: invalid arg for -R\\n\");",
" usage(efd);",
" }",
"#ifndef SAFETY",
" if (fairness && !a_cycles)",
" { fprintf(efd, \"error: -f requires -a or -l\\n\");",
" usage(efd);",
" }",
"#if ACCEPT_LAB==0",
" if (a_cycles)",
"#ifndef VERI",
" { fprintf(efd, \"error: no accept labels defined \");",
" fprintf(efd, \"in model (for option -a)\\n\");",
" usage(efd);",
" }",
"#else",
" { fprintf(efd, \"warning: no explicit accept labels \");",
" fprintf(efd, \"defined in model (for -a)\\n\");",
" }",
"#endif",
"#endif",
"#endif",
"#if !defined(NOREDUCE)",
"#if defined(HAS_ENABLED)",
" fprintf(efd, \"error: reduced search precludes \");",
" fprintf(efd, \"use of 'enabled()'\\n\");",
" 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<<ssize)-1); /* hash init */",
" trail = (Trail *) emalloc((maxdepth+3)*sizeof(Trail));",
" trail++; /* protect trpt-1 refs at depth 0 */",
"#ifdef SVDUMP",
" if (vprefix > 0)",
" { char nm[64];",
" sprintf(nm, \"%%s.svd\", Source);",
" if ((svfd = creat(nm, 0666)) <= 0)",
" { fprintf(efd, \"couldn't create %%s\\n\", nm);",
" vprefix = 0;",
" } }",
"#endif",
"#ifdef RANDSTOR",
" srand(123);",
"#endif",
"#if SYNC>0 && ASYNC==0",
" set_recvs();",
"#endif",
" run();",
" done = 1;",
" wrapup();",
" return 0;",
"}\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] <unwind>\\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<<ssize)*sizeof(struct H_el *));",
"#endif",
"}",
"#endif\n",
"#if !defined(BITSTATE) || defined(FULLSTACK)",
"#ifdef DEBUG",
"void",
"dumpstate(int wasnew, char *v, int n, int tag)",
"{ int i;",
"#ifndef SAFETY",
" if (S_A)",
" { printf(\"\tstate tags %%d (%%d::%%d): \",",
" V_A, wasnew, v[0]);",
"#ifdef FULLSTACK",
" printf(\" %%d \", tag);",
"#endif",
" printf(\"\\n\");",
" }",
"#endif",
"#ifdef SDUMP",
"#ifndef NOCOMP",
" printf(\"\t State: \");",
" for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",",
" ((char *)&now)[i], Mask[i]?\"*\":\"\");",
"#endif",
" printf(\"\\n\tVector: \");",
" for (i = 0; i < n; i++) printf(\"%%d,\", v[i]);",
" printf(\"\\n\");",
"#endif",
"}",
"#endif",
"#ifdef MA",
"int",
"gstore(char *vin, int nin, uchar pbit)",
"{ int n = compress(vin, nin);",
" int i, j=0;",
" static uchar Info[MA+1];",
" if (n >= MA)",
" { printf(\"pan: error, MA too small, recompile pan.c\");",
" printf(\" with -DMA=N with N>%%d\\n\", n);",
" Uerror(\"aborting\");",
" }",
" if (n > 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,
};
|
