harvey/sys/src/cmd/spin/pangen1.h

/***** 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,
};