/*** Generated by Spin Version 3.4.5 -- 8 March 2000 ***/
/*** From source: deadlock.philosophers.prm ***/

#include <stdio.h>
#include <signal.h>
#include <stdlib.h>
#include <string.h>
#include <errno.h>
#define Offsetof(X, Y)	((unsigned long)(&(((X *)0)->Y)))
#ifndef HSFSPIN
#ifndef max
#define max(a,b) (((a)<(b)) ? (b) : (a))
#endif //
#else
#define spin_max(a,b) (((a)<(b)) ? (b) : (a))
#endif //
#include "pan.h"
#ifndef HSFSPIN
#ifdef INDFS
#if VERI
#include "scc.spin.h"
#endif //
#endif //
#endif //
#ifdef CNTRSTACK
#define onstack_now()	(LL[trpt->j6] && LL[trpt->j7])
#define onstack_put()	 LL[trpt->j6]++; LL[trpt->j7]++
#define onstack_zap()	 LL[trpt->j6]--; LL[trpt->j7]--
#endif //
#if !defined(SAFETY) && !defined(NOCOMP)
#ifndef HSFSPIN
#define V_A	(((now._a_t&1)?2:1) << (now._a_t&2))
#define A_V	(((now._a_t&1)?1:2) << (now._a_t&2))
#else
#define V_A	(((now->_a_t&1)?2:1) << (now->_a_t&2))
#define A_V	(((now->_a_t&1)?1:2) << (now->_a_t&2))
#endif //
int	S_A = 0;
#else
#define V_A	0
#define A_V	0
#define S_A	0
#endif //
#ifdef MA
#define onstack_put()	;
#define onstack_zap()	gstore((char *) &now, vsize, 4)
#else
#if defined(FULLSTACK) && !defined(BITSTATE)
#define onstack_put()	trpt->ostate = Lstate
#define onstack_zap()	{ \
	if (trpt->ostate) \
		trpt->ostate->tagged = \
		(S_A)? (trpt->ostate->tagged&~V_A) : 0; \
	}
#endif //
#endif //
struct H_el {
	struct H_el *nxt;
#ifdef FULLSTACK
	unsigned tagged;
#if defined(BITSTATE) && !defined(NOREDUCE) && !defined(SAFETY)
	unsigned proviso;
#endif //
#endif //
#if defined(CHECK) || (defined(COLLAPSE) && !defined(FULLSTACK))
	unsigned long st_id;
#endif //
#ifdef COLLAPSE
#if VECTORSZ<65536
	unsigned short ln;
#else
	unsigned long ln;
#endif //
#endif //
#ifdef REACH
	unsigned D;
#endif //
	unsigned state;
} **H_tab, **S_Tab;

typedef struct Trail {
	short st;	/* current state */
	uchar pr;	/* process id */
	uchar tau;	/* 8 bit-flags */
	uchar o_pm;	/* 8 more bit-flags */
#if 0
	Meaning of bit-flags:
	tau&1   -> timeout enabled
	tau&2   -> request to enable timeout 1 level up (in claim)
	tau&4   -> current transition is a  claim move
	tau&8   -> current transition is an atomic move
	tau&16  -> last move was truncated on stack
	tau&32  -> current transition is a preselected move
	tau&64  -> at least one next state is not on the stack
	tau&128 -> current transition is a stutter move
	o_pm&1	-> the current pid moved -- implements else
	o_pm&2	-> this is an acceptance state
	o_pm&4	-> this is a  progress state
	o_pm&8	-> fairness alg rule 1 undo mark
	o_pm&16	-> fairness alg rule 3 undo mark
	o_pm&32	-> fairness alg rule 2 undo mark
	o_pm&64 -> the current proc applied rule2
	o_pm&128 -> a fairness, dummy move - all procs blocked
#endif //
#if defined(FULLSTACK) && defined(MA)
	uchar proviso;
#endif //
	char  o_n, o_ot, o_m;	/* to save locals */
#ifdef EVENT_TRACE
#if nstates_event<256
	uchar o_event;
#else
	unsigned short o_event;
#endif //
#endif //
	short o_tt, o_To;
#ifdef HAS_UNLESS
	short e_state;	/* if escape trans - state of origin */
#endif //
#if defined(FULLSTACK) && !defined(MA)
	struct H_el *ostate;	/* pointer to stored state */
#endif //
#ifdef CNTRSTACK
	long	j6, j7;
#endif //
	Trans *o_t;
	union {
		int oval;
		int *ovals;
	} bup;
} Trail;
Trail	*trail, *trpt;
FILE	*efd;
#ifndef HSFSPIN
uchar	*this;
#else
uchar	*this_p;
#endif //
long	maxdepth=10000;
#ifdef SC
long	omaxdepth;
char	*stackfile;
#endif //
uchar	*SS, *LL;
uchar	HASH_NR = 0;

#ifdef MEMCNT
double memcnt = (double) 0;
double overhead = (double) 0;
double memlim = (double) (1<<30);
#endif //
/* for emalloc: */
static char *have;
static long left = 0L;
static double fragment = (double) 0;
static unsigned long grow;

unsigned int HASH_CONST[] = {
	/* asuming 4 bytes per int */
	0x88888EEF,	0x00400007,
	0x04c11db7,	0x100d4e63,
	0x0fc22f87,	0x3ff0c3ff,
	0x38e84cd7,	0x02b148e9,
	0x98b2e49d,	0xb616d379,
	0xa5247fd9,	0xbae92a15,
	0xb91c8bc5,	0x8e5880f3,
	0xacd7c069,	0xb4c44bb3,
	0x2ead1fb7,	0x8e428171,
	0xdbebd459,	0x828ae611,
	0x6cb25933,	0x86cdd651,
	0x9e8f5f21,	0xd5f8d8e7,
	0x9c4e956f,	0xb5cf2c71,
	0x2e805a6d,	0x33fc3a55,
	0xaf203ed1,	0xe31f5909,
	0x5276db35,	0x0c565ef7,
	0x273d1aa5,	0x8923b1dd,
	0
};
int	mreached=0, done=0, errors=0, Nrun=1, single=0;
double	nstates=0, nlinks=0, truncs=0, truncs2=0;
double	nlost=0, nShadow=0, hcmp=0, ngrabs=0;
unsigned long	nr_states=0; /* nodes in DFA */
long	Fa=0, Fh=0, Zh=0, Zn=0;
long	PUT=0, PROBE=0, ZAPS=0;
long	Ccheck=0, Cholds=0;
unsigned long mask;
int	a_cycles=0, upto=1, strict=0, verbose = 0;
int	state_tables=0, fairness=0, no_rck=0, Nr_Trails=0;
#ifndef INLINE
int	TstOnly=0;
#endif //
#ifdef BITSTATE
int	ssize=22;
#else
int	ssize=18;
#endif //
int	hmax=0, svmax=0, smax=0;
int	Maxbody=0, XX;
uchar	*noptr;	/* used by macro Pptr(x) */
#ifndef HSFSPIN
State	A_Root;		/* root of acceptance cycles */
#endif //
#ifndef HSFSPIN
State	now;		/* the full state vector */
#else
PackedState	*now;		/* the full state vector */
#endif //
#ifdef VAR_RANGES
void logval(char *, int);
void dumpranges(void);
#endif //
#ifdef MA
#define INLINE_REV
extern void dfa_init(unsigned short);
extern int  dfa_member(unsigned short);
extern int  dfa_store(unsigned char *);
unsigned int	maxgs = 0;
#endif //
#if !defined(NOCOMP) || defined(BITSTATE)
#ifndef HSFSPIN
State	comp_now;	/* compressed state vector */
State	comp_msk;
#else
PackedState	comp_now;	/* compressed state vector */
PackedState	comp_msk;
#endif //
uchar	*Mask = (uchar *) &comp_msk;
#endif //
#ifdef COLLAPSE
#ifndef HSFSPIN
State	comp_tmp;
#else
PackedState	comp_tmp;
#endif //
char	*scratch = (char *) &comp_tmp;
#endif //
Stack	*stack; 	/* for queues, processes */
Svtack	*svtack;	/* for old state vectors */
long	J1, J2, J3, J4, j1, j2, j3, j4;
long	A_depth = 0, depth = 0;
uchar	warned = 0, iterative = 0, like_java = 0, every_error = 0;
uchar	noasserts = 0, noends = 0;
#if SYNC>0 && ASYNC==0
void set_recvs(void);
int  no_recvs(int);
#endif //
#if SYNC
#ifndef HSFSPIN
#define IfNotBlocked	if (boq != -1) continue;
#define UnBlock     	boq = -1
#else
#define IfNotBlocked	if (now->boq != -1) continue;
#define UnBlock     	now->boq = -1
#endif //
#else
#define IfNotBlocked	/* cannot block */
#define UnBlock     	/* don't bother */
#endif //

void active_procs(void);
void cleanup(void);
#ifndef HSFSPIN
void do_the_search(void);
#endif //
void find_shorter(int);
void iniglobals(void);
void stopped(int);
void wrapup(void);
int *grab_ints(int);
void ungrab_ints(int *, int);
#ifndef NOBOUNDCHECK
#define Index(x, y)	Boundcheck(x, y, II, tt, t)
#else
#define Index(x, y)	x
#endif //
#ifdef HSFSPIN
#define NOW now->
#define THIS this_p
#else
#define NOW now.
#define THIS this
#endif //
short Air[] = {  (short) Air0, (short) Air1, (short) Air2 };
int
addproc(int n, int par0)
{
#ifndef HSFSPIN
	int k, j, h = now._nr_pr;
	uchar *o_this = this;

#else
	int k, j, h = now->_nr_pr;
	uchar *o_this = this_p;

#endif //
#ifndef INLINE
	if (TstOnly) return (h < MAXPROC);
#endif //
#ifndef NOBOUNDCHECK
/* redefine Index only within this procedure */
#undef Index
#define Index(x, y)	Boundcheck(x, y, 0, 0, 0)
#endif //
	if (h >= MAXPROC)
		Uerror("too many processes");
	switch (n) {
	case 0: j = sizeof(P0); break;
	case 1: j = sizeof(P1); break;
	case 2: j = sizeof(P2); break;
	default: Uerror("bad proc - addproc");
	}
	if (vsize%WS)
		proc_skip[h] = WS-(vsize%WS);
	else
		proc_skip[h] = 0;
#ifndef NOCOMP
	for (k = vsize + proc_skip[h]; k > vsize; k--)
		Mask[k-1] = 1; /* align */
#endif //
	vsize += proc_skip[h];
	proc_offset[h] = vsize;
#ifdef SVDUMP
	if (vprefix > 0)
	{	int dummy = 0;
		write(svfd, (uchar *) &dummy, sizeof(int)); /* mark */
		write(svfd, (uchar *) &h, sizeof(int));
		write(svfd, (uchar *) &n, sizeof(int));
		write(svfd, (uchar *) &proc_offset[h], sizeof(int));
#ifndef HSFSPIN
		write(svfd, (uchar *) &now, vprefix-4*sizeof(int)); /* padd */
#else
		write(svfd, (uchar *) now, vprefix-4*sizeof(int)); /* padd */
#endif //
	}
#endif //
#ifndef HSFSPIN
	now._nr_pr += 1;
	if (fairness && ((int) now._nr_pr + 1 >= (8*NFAIR)/2))
#else
	now->_nr_pr += 1;
	if (fairness && ((int) now->_nr_pr + 1 >= (8*NFAIR)/2))
#endif //
	{	printf("Error: too many processes -- current");
		printf(" max is %d procs (-DNFAIR=%d)\n",
			(8*NFAIR)/2 - 2, NFAIR);
		printf("\trecompile with -DNFAIR=%d\n",
			NFAIR+1);
		exit(1);
	}
	vsize += j;
#ifndef NOVSZ
#ifndef HSFSPIN
	now._vsz = vsize;
#else
	now->_vsz = vsize;
#endif //
#endif //
#ifndef NOCOMP
	for (k = 1; k <= Air[n]; k++)
		Mask[vsize - k] = 1; /* pad */
	Mask[vsize-j] = 1; /* _pid */
#endif //
#ifndef HSFSPIN
	hmax = max(hmax, vsize);
#else
	hmax = spin_max(hmax, vsize);
#endif //
	if (vsize >= VECTORSZ)
	{	printf("pan: error, VECTORSZ too small, recompile pan.c");
		printf(" with -DVECTORSZ=N with N>%d\n", vsize);
		Uerror("aborting");
	}
	memset((char *)pptr(h), 0, j);
#ifndef HSFSPIN
	this = pptr(h);
#else
	this_p = pptr(h);
#endif //
	if (BASE > 0 && h > 0)
#ifndef HSFSPIN
		((P0 *)this)->_pid = h-BASE;
	else
		((P0 *)this)->_pid = h;
#else
		((P0 *)this_p)->_pid = h-BASE;
	else
		((P0 *)this_p)->_pid = h;
#endif //
	switch (n) {
	case 2:	/* np_ */
		((P2 *)pptr(h))->_t = 2;
		((P2 *)pptr(h))->_p = 0;
		reached2[0] = 1;
		accpstate[2][1] = 1;
		break;
	case 1:	/* :init: */
		((P1 *)pptr(h))->_t = 1;
		((P1 *)pptr(h))->_p = 10; reached1[10]=1;
		/* params: */
		/* locals: */
		((P1 *)pptr(h))->philosophers = 4;
#ifdef VAR_RANGES
		logval(":init::philosophers", ((P1 *)pptr(h))->philosophers);
#endif //
		break;
	case 0:	/* philosopher */
		((P0 *)pptr(h))->_t = 0;
		((P0 *)pptr(h))->_p = 5; reached0[5]=1;
		/* params: */
		((P0 *)pptr(h))->my_id = par0;
		/* locals: */
#ifdef VAR_RANGES
		logval("philosopher:my_id", ((P0 *)pptr(h))->my_id);
#endif //
		break;
	}
#ifndef HSFSPIN
	this = o_this;
#else
	this_p = o_this;
#endif //
	return h-BASE;
#ifndef NOBOUNDCHECK
#undef Index
#define Index(x, y)	Boundcheck(x, y, II, tt, t)
#endif //
}

#if defined(BITSTATE) && defined(COLLAPSE)
/* just to allow compilation, to generate the error */
long col_p(int i, char *z) { return 0; }
long col_q(int i, char *z) { return 0; }
#endif //
#ifndef BITSTATE
#ifdef COLLAPSE
long
col_p(int i, char *z)
{	int j, k; unsigned long ordinal(char *, long, short);
	char *x, *y;
	P0 *ptr = (P0 *) pptr(i);
	switch (ptr->_t) {
	case 0: j = sizeof(P0); break;
	case 1: j = sizeof(P1); break;
	case 2: j = sizeof(P2); break;
	default: Uerror("bad proctype - collapse");
	}
	if (z) x = z; else x = scratch;
	y = (char *) ptr; k = proc_offset[i];
	for ( ; j > 0; j--, y++)
		if (!Mask[k++]) *x++ = *y;
	if (z) return (long) (x - z);
	for (j = 0; j < WS-1; j++)
		*x++ = 0;
	x -= j;
	return ordinal(scratch, x-scratch, 2+ptr->_t);
}
#endif //
#endif //
void
run(void)
{
#ifndef HSFSPIN
	int i;
	memset((char *)&now, 0, sizeof(State));
	vsize = sizeof(State) - VECTORSZ;
#ifndef NOVSZ
	now._vsz = vsize;
#endif //
/* optional provisioning statements, e.g. to */
/* set hidden variables, used as constants */
#ifdef PROV
#include PROV
#endif //
#else

       noptr=new unsigned char[VECTORSZ];
       memset(noptr,VECTORSZ,0);
#endif //
	settable();
#ifndef HSFSPIN /* may appear several times */
#ifndef HSFSPIN /* may appear several times */
#ifndef HSFSPIN /* may appear several times */
	Maxbody = max(Maxbody, sizeof(P0));
	Maxbody = max(Maxbody, sizeof(P1));
	Maxbody = max(Maxbody, sizeof(P2));
	reached[0] = reached0;
	reached[1] = reached1;
	reached[2] = reached2;
	accpstate[0] = (uchar *) emalloc(nstates0);
	accpstate[1] = (uchar *) emalloc(nstates1);
	accpstate[2] = (uchar *) emalloc(nstates2);
	progstate[0] = (uchar *) emalloc(nstates0);
	progstate[1] = (uchar *) emalloc(nstates1);
	progstate[2] = (uchar *) emalloc(nstates2);
	stopstate[0] = (uchar *) emalloc(nstates0);
	stopstate[1] = (uchar *) emalloc(nstates1);
	stopstate[2] = (uchar *) emalloc(nstates2);
	visstate[0] = (uchar *) emalloc(nstates0);
	visstate[1] = (uchar *) emalloc(nstates1);
	visstate[2] = (uchar *) emalloc(nstates2);
	stopstate[0][endstate0] = 1;
	stopstate[1][endstate1] = 1;
	stopstate[2][endstate2] = 1;
#endif //
#endif //
#endif //
#ifdef HSFSPIN /* may appear several times */
#ifdef HSFSPIN /* may appear several times */
#ifdef HSFSPIN /* may appear several times */
	Maxbody = spin_max(Maxbody, sizeof(P0));
	Maxbody = spin_max(Maxbody, sizeof(P1));
	Maxbody = spin_max(Maxbody, sizeof(P2));
       reached[0] = reached0;
       reached[1] = reached1;
       reached[2] = reached2;
	accpstate[0] = new unsigned char[nstates0];
	accpstate[1] = new unsigned char[nstates1];
	accpstate[2] = new unsigned char[nstates2];
       memset(accpstate[0], 0, nstates0);
       memset(accpstate[1], 0, nstates1);
       memset(accpstate[2], 0, nstates2);
	progstate[0] = new unsigned char[nstates0];
	progstate[1] = new unsigned char[nstates1];
	progstate[2] = new unsigned char[nstates2];
       memset(progstate[0], 0, nstates0);
       memset(progstate[1], 0, nstates1);
       memset(progstate[2], 0, nstates2);
	stopstate[0] = new unsigned char[nstates0];
	stopstate[1] = new unsigned char[nstates1];
	stopstate[2] = new unsigned char[nstates2];
       memset(stopstate[0], 0, nstates0);
       memset(stopstate[1], 0, nstates1);
       memset(stopstate[2], 0, nstates2);
	visstate[0] = new unsigned char[nstates0];
	visstate[1] = new unsigned char[nstates1];
	visstate[2] = new unsigned char[nstates2];
       memset(visstate[0], 0, nstates0);
       memset(visstate[1], 0, nstates1);
       memset(visstate[2], 0, nstates2);
	stopstate[0][endstate0] = 1;
	stopstate[1][endstate1] = 1;
	stopstate[2][endstate2] = 1;
	dangstate[0] = new unsigned char[nstates0];
	dangstate[1] = new unsigned char[nstates1];
	dangstate[2] = new unsigned char[nstates2];
       memset(dangstate[0], 0, nstates0);
       memset(dangstate[1], 0, nstates1);
       memset(dangstate[2], 0, nstates2);
#endif //
#endif //
#endif //
#ifdef HSFSPIN
	dangstate[0][2] = 1;
#endif //
	retrans(0, nstates0, start0, src_ln0, reached0);
	retrans(1, nstates1, start1, src_ln1, reached1);
	if (state_tables)
	{ printf("\nTransition Type: ");
	  printf("A=atomic; D=d_step; L=local; G=global\n");
	  printf("Source-State Labels: ");
	  printf("p=progress; e=end; a=accept;\n");
#ifdef MERGED
	  printf("Note: statement merging was used. Only the first\n");
	  printf("      stmnt executed in each merge sequence is shown\n");
	  printf("      (use spin -a -o3 to disable statement merging)\n");
#endif //
	  exit(0);
	}
#ifndef HSFSPIN
	iniglobals();
#endif //
#ifndef HSFSPIN
#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 //
#ifdef INDFS
#if VERI
Classify_SCC();
#endif //
#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 //
#endif //
}
#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 //
}
#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 //
#ifndef HSFSPIN
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;
#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 //
#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;
#ifndef HSFSPIN
	short tt = (short) ((P0 *)this)->_p;
	char  ot = (char)  ((P0 *)this)->_t;
#else
	short tt = (short) ((P0 *)this_p)->_p;
	char  ot = (char)  ((P0 *)this_p)->_t;
#endif //
#ifdef EVENT_TRACE
	short oboq = boq;
	if (ot == EVENT_TRACE) boq = -1;
#define continue	{ boq = oboq; return 0; }
#else
#define continue	return 0
#endif //
#include FORWARD_MOVES
P999:
#ifdef EVENT_TRACE
	if (ot == EVENT_TRACE) boq = oboq;
#endif //
	return m;
#undef continue
}
#ifndef HSFSPIN
#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 //
#endif //
#ifndef HSFSPIN
int
enabled(int iam, int pid)
{
#ifndef HSFSPIN
	Trans *t; uchar *othis = this;
#else
	Trans *t; uchar *othis = this_p;
#endif //
	int res = 0; short tt; char ot;
#ifdef VERI
	/* if (pid > 0) */ pid++;
#endif //
	if (pid == iam)
		Uerror("used: enabled(pid=thisproc)");
#ifndef HSFSPIN
	if (pid < 0 || pid >= (int) now._nr_pr)
#else
	if (pid < 0 || pid >= (int) now->_nr_pr)
#endif //
		return 0;
#ifndef HSFSPIN
	this = pptr(pid);
#else
	this_p = pptr(pid);
#endif //
	TstOnly = 1;
#ifndef HSFSPIN
	tt = (short) ((P0 *)this)->_p;
	ot = (uchar) ((P0 *)this)->_t;
#else
	tt = (short) ((P0 *)this_p)->_p;
	ot = (uchar) ((P0 *)this_p)->_t;
#endif //
	for (t = trans[ot][tt]; t; t = t->nxt)
		if (do_transit(t, pid, 0))
		{	res = 1;
			break;
		}
	TstOnly = 0;
#ifndef HSFSPIN
	this = othis;
#else
	this_p = othis;
#endif //
	return res;
}
#endif //
#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)
{	if (proc_offset[x])
		return (uchar *) pptr(x);
	else
		return noptr;
}
extern void check_claim(int);
#ifndef HSFSPIN
/* 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, delta_m = 0;
	short II, JJ = 0, tt, kk;

	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
			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
			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 //
#ifdef INDFS
#if VERI
                       if (a_cycles &&(II && JJ) || (II == 3)){
                               /* INDFS: During dfs1 state found in stack? */
                               /* INDFS: check if F-SCCC */
                               if(F_SCC((int)((P0*)pptr(0))->_p)){
                                       A_depth=depth;
#ifdef BITSTATE
                                       depthfound = Lstate->tagged - 1;
#else
                                       depthfound = depth_of(Lstate);
#endif //
                                       uerror("acceptance cycle in dfs1");
                               }
                       }
#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))
		{
			if (a_cycles && (trpt->o_pm&2))
			{	/* Accepting state */
				now._a_t |= 2;
				now._cnt[now._a_t&1] = now._nr_pr + 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 = 0 when Cnt 0 */
			if (now._cnt[now._a_t&1] == 1)
			{	now._a_t &= ~2;
				now._cnt[now._a_t&1] = 0;
				trpt->o_pm |= 16;
#ifdef DEBUG
	printf("%3d: fairness Rule 3: _a_t = %d\n",
		depth, now._a_t);
#endif //
	}	}	}
#endif //
	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)
		&& !(trpt->tau&1)
		&& !(trpt->tau&32)
		&& (t->atom & 8)
		&& boq == -1
		&& From != To)
		{	if (t->qu[0] == 0
			||  q_cond(II, t))
			{	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
		&& !(trpt->o_pm&32)
		&& (now._a_t&2)
		&&  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 */
#ifdef INDFS
#if VERI
                       /* INDFS If( (now._a_t&1) && SCC(now)!=SCC(pred)) continue */
                       if(a_cycles && (now._a_t&1) && (II==0) && (scc[((P0*)pptr(0))->_p]!=scc[t->st])) continue;
#endif //
#endif //
			if (boq == -1)
#ifdef CTL
	/* for branching-time, can accept reduction only if */
	/* the persistent set contains just 1 transition */
			{	if ((trpt->tau&32) && (trpt->o_pm&1))
					trpt->tau |= 16;
				trpt->o_pm |= 1; /* we moved */
			}
#else
				trpt->o_pm |= 1; /* we moved */
#endif //
#ifdef PEG
			peg[t->forw]++;
#endif //
#if defined(VERBOSE) || defined(CHECK)
#if defined(SVDUMP)
			printf("%3d: proc %d exec %d \n", 
				depth, II, t->t_id);
#else
			printf("%3d: proc %d exec %d, ", 
				depth, II, t->forw);
			printf("%d to %d, %s %s %s", 
				tt, t->st, t->tp,
				(t->atom&2)?"atomic":"",
				(boq != -1)?"rendez-vous":"");
#ifdef HAS_UNLESS
	if (t->e_trans)
		printf(" (escapes to state %d)", t->st);
#endif //
	printf(" %saccepting [tau=%d]\n",
		(trpt->o_pm&2)?"":"non-", trpt->tau);
#endif //
#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)
		&&  (trpt->o_pm&64))
		{	if (trpt->o_pm&1)
			{
#ifdef VERI
				if (now._cnt[now._a_t&1] == 1)
					now._cnt[now._a_t&1] = 2;
#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
			{	if (n > 0)
				{
					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)
			now._cnt[now._a_t&1] = 2;
#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
	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;
		now._cnt[now._a_t&1] = 1;
		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;
		if ((trpt->tau&8) && !(trpt->tau&4))
		{	trpt->tau &= ~(1|8);
			/* 1=timeout, 8=atomic */
			From = now._nr_pr-1; To = BASE;
#ifdef DEBUG
		printf("%3d: atomic step proc %d ", depth, II+1);
		printf("unexecutable\n");
#endif //
#ifdef VERI
			trpt->tau |= 4;	/* switch to claim */
#endif //
			goto AllOver;
		}
#ifdef ETIM
		if (!(trpt->tau&1)) /* didn't try timeout yet */
		{
#ifdef VERI
			if (trpt->tau&4)
			{
#ifndef NTIM
				if (trpt->tau&2) /* requested */
#endif //
				{	trpt->tau |=  1;
					trpt->tau &= ~2;
#ifdef DEBUG
				printf("%d: timeout\n", depth);
#endif //
					goto Stutter;
			}	}
			else
			{	/* only claim can enable timeout */
				if ((trpt->tau&8)
				&&  !((trpt-1)->tau&4))
/* blocks inside an atomic */		goto BreakOut;
#ifdef DEBUG
				printf("%d: req timeout\n",
					depth);
#endif //
				(trpt-1)->tau |= 2; /* request */
				goto Up;
			}
#else
#ifdef DEBUG
			printf("%d: timeout\n", depth);
#endif //
			trpt->tau |=  1;
			goto Again;
#endif //
		}
#endif //
BreakOut:
#ifdef VERI
#ifndef NOSTUTTER
		if (!(trpt->tau&4))
		{	trpt->tau |= 4;   /* claim stuttering */
			trpt->tau |= 128; /* stutter mark */
#ifdef DEBUG
			printf("%d: claim stutter\n", depth);
#endif //
			goto Stutter;
		}
#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
#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))
		{
#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 0
                       if (a_cycles && (trpt->o_pm&2))
#endif //
#ifdef INDFS
                       /* INDFS: If (accept(s) and P-SCC(neverstate(s)) */
                       if (a_cycles && (P_SCC(((P0*)pptr(0))->_p))) /* if P-SCC */
#else
                       if (a_cycles && (trpt->o_pm&2))
#endif //
				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;
}

#endif //
#ifdef HSFSPIN
int assertion_violated=0;
#endif //
void
assert(int a, char *s, int ii, int tt, Trans *t)
{
#ifndef HSFSPIN
	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--;
	}
#else
       assertion_violated=!a;
#endif //
}
#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 //
#ifndef HSFSPIN
void
wrap_stats(void)
{	double a, b;
#ifdef COVEST
	extern double log(double);

#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("	notrace assertion  	+\n");
#else
	printf("	trace assertion    	+\n");
#endif //
#endif //
#ifdef VERI
	printf("	never-claim         	+\n");
	printf("	assertion violations	");
	if (noasserts)
		printf("- (disabled by -A flag)\n");
	else
		printf("+ (if within scope of claim)\n");
#else
#ifdef NOCLAIM
	printf("	never-claim         	- (not selected)\n");
#else
	printf("	never-claim         	- (none specified)\n");
#endif //
	printf("	assertion violations	");
	if (noasserts)
		printf("- (disabled by -A flag)\n");
	else
		printf("+\n");
#endif //
#ifndef SAFETY
#ifdef NP
	printf("	non-progress cycles 	");
#else
	printf("	acceptance   cycles 	");
#endif //
	if (a_cycles)
		printf("+ (fairness %sabled)\n",
			fairness?"en":"dis");
	else printf("- (not selected)\n");
#else
	printf("	cycle checks       	- (disabled by -DSAFETY)\n");
#endif //
#ifdef VERI
	printf("	invalid endstates	- ");
	printf("(disabled by ");
	if (noends)
		printf("-E flag)\n\n");
	else
		printf("never-claim)\n\n");
#else
	printf("	invalid endstates	");
	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	equivalent memory usage for states",
			nr1/1000000.);
		printf(" (stored*(State-vector + overhead))\n");
#ifdef BITSTATE
		printf("%-6.3f	memory 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	actual 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("	State-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	memory used for hash-table (-w%d)\n",
			nr3/1000000., ssize);
#endif //
#endif //
		printf("%-6.3f	memory 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	total actual memory usage\n\n",
			memcnt/1000000.);
	} else
#endif //
		printf("%-6.3f	memory 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);
}

void
stopped(int arg)
{	printf("Interrupted\n");
	wrapup();
}
#endif //
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;
	}
}

#ifndef HSFSPIN
#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);

	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 = (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, "	of an unless clause, could make p.o. reduction\n");
	fprintf(efd, "	invalid (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;
}

void
usage(FILE *fd)
{
	fprintf(fd, "Valid Options are:\n");
#ifndef SAFETY
#ifdef NP
	fprintf(fd, "	-a  -> is disabled by -DNP ");
	fprintf(fd, "(-DNP compiles for -l only)\n");
#else
	fprintf(fd, "	-a  find acceptance cycles\n");
#endif //
#else
	fprintf(fd, "	-a,-l,-f  -> are disabled by -DSAFETY\n");
#endif //
	fprintf(fd, "	-A  ignore assert() violations\n");
	fprintf(fd, "	-cN stop at Nth error ");
	fprintf(fd, "(defaults to -c1)\n");
	fprintf(fd, "	-d  print state tables and stop\n");
	fprintf(fd, "	-e  create trails for all errors\n");
	fprintf(fd, "	-E  ignore invalid endstates\n");
#ifdef SC
	fprintf(fd, "	-Ffile  use 'file' to store disk-stack\n");
#endif //
#ifndef NOFAIR
	fprintf(fd, "	-f  add weak fairness (to -a or -l)\n");
#endif //
	fprintf(fd, "	-hN choose other hash-function 1..32\n");
	fprintf(fd, "	-i  search for shortest path to error\n");
	fprintf(fd, "	-I  like -i, but approximate and faster\n");
	fprintf(fd, "	-J  reverse eval order of nested unlesses\n");
#ifndef SAFETY
#ifdef NP
	fprintf(fd, "	-l  find non-progress cycles\n");
#else
	fprintf(fd, "	-l  find non-progress cycles -> ");
	fprintf(fd, "disabled, requires ");
	fprintf(fd, "compilation with -DNP\n");
#endif //
#endif //
	fprintf(fd, "	-mN max depth N steps (default=10k)\n");
	fprintf(fd, "	-n  no listing of unreached states\n");
#ifdef SVDUMP
	fprintf(fd, "	-pN create svfile (save N bytes per state)\n");
#endif //
	fprintf(fd, "	-q  require empty chans in valid endstates\n");
#ifdef BITSTATE
	fprintf(fd, "	-RN repeat run Nx with N ");
	fprintf(fd, "[1..32] independent hash functions\n");
#endif //
	fprintf(fd, "	-s  1-bit hashing (default is 2-bit)\n");
	fprintf(fd, "	-T  create trail files in read-only mode\n");
	fprintf(fd, "	-tsuf replace .trail with .suf on trailfiles\n");
	fprintf(fd, "	-V  print SPIN version number\n");
	fprintf(fd, "	-v  verbose -- filenames in unreached state listing\n");
	fprintf(fd, "	-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)
	{
err:
		printf("pan: out of memory\n");
#ifdef MEMCNT
		printf("	%g bytes used\n", memcnt);
		printf("	%g bytes more needed\n", (double) n);
		printf("	%g bytes limit (2^MEMCNT)\n",
			memlim);
#endif //
#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;
}
#endif //
void
Uerror(char *str)
{	/* always fatal */
	uerror(str);
#ifndef HSFSPIN
	wrapup();
#endif //
}

#ifndef HSFSPIN
#if defined(MA) && !defined(SAFETY)
int
Unwind(void)
{	Trans *t; char ot, m; short tt; short II, i;

	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 //
#endif //
void
uerror(char *str)
{	static char laststr[256];

	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");
#ifndef HSFSPIN
			wrapup(); /* no recovery from unwind */
#endif //
		}
#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)
#ifndef HSFSPIN
		wrapup();
#endif //
	depthfound = -1;	/* tripakis */
}

void
r_ck(uchar *which, int N, int M, short *src, S_F_MAP *mp)
{	int i, m=0;

#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("	(%d of %d states)\n", N-1-m, N-1);
}

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");
	}
}

void
putrail(void)
#ifndef HSFSPIN
{	int fd; long i, j;
#else
{	FILE *fd;
       int long i, j;
#endif //
	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);
#ifndef HSFSPIN
	if ((fd = creat(fnm, TMODE)) < 0)
#else
	if ((fd = fopen(fnm, "w")) <= 0)
#endif //
	{	printf("cannot create %s\n", fnm);
		perror("cause");
		return;
	}
#ifdef VERI
	sprintf(snap, "-2:%d:-2\n", VERI);
#ifndef HSFSPIN
	write(fd, snap, strlen(snap));
#else
	fprintf(fd, snap);
#endif //
#endif //
#ifdef MERGED
	sprintf(snap, "-4:-4:-4\n");
#ifndef HSFSPIN
	write(fd, snap, strlen(snap));
#else
	fprintf(fd, snap);
#endif //
#endif //
	for (i = 1; i <= depth; i++)
	{	if (i == depthfound+1)
#ifndef HSFSPIN
			write(fd, "-1:-1:-1\n", 9);
#else
                       fprintf(fd, "-1:-1:-1\n");
#endif //
		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);
#ifndef HSFSPIN
		if (write(fd, snap, j) != j)
#else
		if (fprintf(fd, snap) != j)
#endif //
		{	printf("pan: error writing %s\n", fnm);
#ifndef HSFSPIN
	                close(fd);
			wrapup();
#else
			fclose(fd);
#endif //
		}
	}
#ifndef HSFSPIN
	printf("pan: wrote %s\n", fnm);
	close(fd);
#else
	printf("Wrote %s\n", fnm);
	fclose(fd);
#endif //
}

#ifndef HSFSPIN 
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 //
}

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 //
}

void
p_restor(int h)
{	int i; char *z = (char *) &now;

	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();
}

void
q_restor(void)
{	int k; char *z = (char *) &now;

	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;
}
#endif //
int
delproc(int sav, int h)
{	int d, i=0, o_vsize = vsize;

#ifndef HSFSPIN
	if (h+1 != (int) now._nr_pr) return 0;

	while (now._nr_qs
	&&     q_offset[now._nr_qs-1] > proc_offset[h])
	{	delq(sav);
		i++;
	}
	d = vsize - proc_offset[h];
#else
	if (h+1 != (int) now->_nr_pr) return 0;

	d = vsize - proc_offset[h];
#endif //
#ifndef HSFSPIN
	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);
	}
#endif //
	vsize = proc_offset[h];
#ifndef HSFSPIN
	now._nr_pr = now._nr_pr - 1;
#else
	now->_nr_pr = now->_nr_pr - 1;
#endif //
	memset((char *)pptr(h), 0, d);
	vsize -= proc_skip[h];
#ifndef NOVSZ
#ifndef HSFSPIN
	now._vsz = vsize;
#else
	now->_vsz = vsize;
#endif //
#endif //
#ifndef NOCOMP
	for (i = vsize; i < o_vsize; i++)
		Mask[i] = 0; /* reset */
#endif //
	return 1;
}

#ifndef HSFSPIN
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 //
}

#endif //
int
qs_empty(void)
{	int i;
#ifndef HSFSPIN
	for (i = 0; i < (int) now._nr_qs; i++)
#else
	for (i = 0; i < (int) now->_nr_qs; i++)
#endif //
	{	if (q_sz(i) > 0)
			return 0;
	}
	return 1;
}

int
endstate(void)
{	int i; P0 *ptr;
#ifndef HSFSPIN
	for (i = BASE; i < (int) now._nr_pr; i++)
#else
	for (i = BASE; i < (int) now->_nr_pr; i++)
#endif //
	{	ptr = (P0 *) pptr(i);
		if (!stopstate[ptr->_t][ptr->_p])
			return 0;
	}
	if (strict) return qs_empty();
#if defined(EVENT_TRACE) && !defined(OTIM)
#ifndef HSFSPIN
	if (!stopstate[EVENT_TRACE][now._event] && !a_cycles)
#else
	if (!stopstate[EVENT_TRACE][now->_event] && !a_cycles)
#endif //
	{	printf("pan: event_trace not completed\n");
		return 0;
	}
#endif //
	return 1;
}

#ifndef HSFSPIN
#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
	now._cnt[1] = now._cnt[0];
#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 //

#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;
		if (v && v->tagged >= n)
			goto gotcha;
		ngrabs++;
	}
	return (struct H_el *)
	      emalloc(sizeof(struct H_el)+n-sizeof(unsigned));
}

#else
#define grab_state(n) (struct H_el *) \
		emalloc(sizeof(struct H_el)+n-sizeof(unsigned));
#endif //
#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)
#ifndef HSFSPIN
		*v++ = now._a_t;
#else
		*v++ = now->_a_t;
#endif //
#ifndef NOFAIR
	if (fairness)
	for (i = 0; i < NFAIR; i++)
#ifndef HSFSPIN
		*v++ = now._cnt[i];
#else
		*v++ = now->_cnt[i];
#endif //
#endif //
#endif //
	nbytelen = 0;
#ifndef JOINPROCS
#ifndef HSFSPIN
	for (i = 0; i < (int) now._nr_pr; i++)
#else
	for (i = 0; i < (int) now->_nr_pr; i++)
#endif //
	{	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;
#ifndef HSFSPIN
	for (i = 0; i < (int) now._nr_pr; i++)
#else
	for (i = 0; i < (int) now->_nr_pr; i++)
#endif //
		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
#ifndef HSFSPIN
	for (i = 0; i < (int) now._nr_qs; i++)
#else
	for (i = 0; i < (int) now->_nr_qs; i++)
#endif //
	{	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 */
#ifndef HSFSPIN
	w = (char *) &now + 3 * sizeof(uchar);
#else
	w = (char *) now + 3 * sizeof(uchar);
#endif //
#ifndef NOFAIR
	w += NFAIR;
#endif //
#else
#ifndef HSFSPIN
#if VECTORSZ<65536
	w = (char *) &(now._vsz) + sizeof(unsigned short);
#else
	w = (char *) &(now._vsz) + sizeof(unsigned long);
#endif //
#else
#if VECTORSZ<65536
	w = (char *) &(now->_vsz) + sizeof(unsigned short);
#else
	w = (char *) &(now->_vsz) + sizeof(unsigned long);
#endif //
#endif //
#endif //
	x = scratch;
#ifndef HSFSPIN
	*x++ = now._nr_pr;
	*x++ = now._nr_qs;
	if (now._nr_qs > 0 && qptr(0) < pptr(0))
#else
	*x++ = now->_nr_pr;
	*x++ = now->_nr_qs;
	if (now->_nr_qs > 0 && qptr(0) < pptr(0))
#endif //
		n = qptr(0) - (uchar *) w;
	else
		n = pptr(0) - (uchar *) w;
#ifndef HSFSPIN
	j = w - (char *) &now;
#else
	j = w - (char *) now;
#endif //
	for (i = 0; i < n; i++, w++)
		if (!Mask[j++]) *x++ = *w;
#ifndef SEPQS
#ifndef HSFSPIN
	for (i = 0; i < (int) now._nr_qs; i++)
#else
	for (i = 0; i < (int) now->_nr_qs; i++)
#endif //
		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 //
#ifndef HSFSPIN
#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;

	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;

	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 //

#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("	state tags %d (%d::%d): ",
			V_A, wasnew, v[0]);
#ifdef FULLSTACK
		printf(" %d ", tag);
#endif //
		printf("\n");
	}
#endif //
#ifdef SDUMP
#ifndef NOCOMP
	printf("	 State: ");
	for (i = 0; i < vsize; i++) printf("%d%s,",
		((char *)&now)[i], Mask[i]?"*":"");
#endif //
	printf("\n	Vector: ");
	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))
			{	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)
{	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
		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("	New 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
#ifndef NOFAIR
			&& (!fairness || now._cnt[1] <= 1)
#endif //
			)
				goto intersect;
#endif //
#ifdef CHECK
	printf("	Stack 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("	New state %d+\n", (int) tmp->st_id);
#endif //
#ifdef DEBUG
	dumpstate(1, (char *)&(tmp->state), n, 0);
#endif //
			return 0;
		}
#endif //
#ifdef CHECK
	printf("	Old 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("		ReVisiting (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 //
#endif //
#ifdef HSFSPIN
#undef Index
#define Index(x,y) x

#include <y.tab.h>
#include LEXTOK_WOOD_VALFUNCS
#include LEXTOK_WOOD_CONSTRUCTOR

#undef Index
#define Index(x,y) Boundcheck(x,y,II,tt,t)

#endif //
#include TRANSITIONS
void
do_reach(void)
{
	r_ck(reached0, nstates0, 0, src_ln0, src_file0);
	r_ck(reached1, nstates1, 1, src_ln1, src_file1);
}

void
iniglobals(void)
{
		NOW
forks[0] = addqueue(1, 0);
		NOW
forks[1] = addqueue(2, 0);
		NOW
forks[2] = addqueue(3, 0);
		NOW
forks[3] = addqueue(4, 0);
#ifdef VAR_RANGES
#endif //
#ifndef HSFSPIN /* may appear several times */
#ifndef HSFSPIN /* may appear several times */
#ifndef HSFSPIN /* may appear several times */
#ifndef HSFSPIN /* may appear several times */
	Maxbody = max(Maxbody, sizeof(Q1));
	Maxbody = max(Maxbody, sizeof(Q2));
	Maxbody = max(Maxbody, sizeof(Q3));
	Maxbody = max(Maxbody, sizeof(Q4));
#endif //
#endif //
#endif //
#endif //
#if HSF-SPIN /* may appear several times */
#if HSF-SPIN /* may appear several times */
#if HSF-SPIN /* may appear several times */
#if HSF-SPIN /* may appear several times */
	Maxbody = spin_max(Maxbody, sizeof(Q1));
	Maxbody = spin_max(Maxbody, sizeof(Q2));
	Maxbody = spin_max(Maxbody, sizeof(Q3));
	Maxbody = spin_max(Maxbody, sizeof(Q4));
#endif //
#endif //
#endif //
#endif //
#ifndef HSFSPIN
	Maxbody = max(Maxbody, sizeof(State)-VECTORSZ);
#else
	Maxbody = spin_max(Maxbody, sizeof(PackedState)-VECTORSZ);
#endif //

}

int
addqueue(int n, int is_rv)
#ifndef HSFSPIN
{	int j=0, i = now._nr_qs, k;

#else
{	int j=0, i = now->_nr_qs, k;

#endif //
	if (i >= MAXQ)
		Uerror("too many queues");
	switch (n) {
	case 4: j = sizeof(Q4); q_flds[4] = 1; q_max[4] = 1; break;
	case 3: j = sizeof(Q3); q_flds[3] = 1; q_max[3] = 1; break;
	case 2: j = sizeof(Q2); q_flds[2] = 1; q_max[2] = 1; break;
	case 1: j = sizeof(Q1); q_flds[1] = 1; q_max[1] = 1; break;
	default: Uerror("bad queue - addqueue");
	}
	if (vsize%WS)
		q_skip[i] = WS-(vsize%WS);
	else
		q_skip[i] = 0;
#ifndef NOCOMP
	k = vsize; if (is_rv) k += j;
	for (k += q_skip[i]; k > vsize; k--)
		Mask[k-1] = 1; /* align */
#endif //
	vsize += q_skip[i];
	q_offset[i] = vsize;
#ifndef HSFSPIN
	now._nr_qs += 1;
#else
	now->_nr_qs += 1;
#endif //
	vsize += j;
#ifndef NOVSZ
#ifndef HSFSPIN
	now._vsz = vsize;
#else
	now->_vsz = vsize;
#endif //
#endif //
#ifndef HSFSPIN
	hmax = max(hmax, vsize);
#else
	hmax = spin_max(hmax, vsize);
#endif //
	if (vsize >= VECTORSZ)
		Uerror("VECTORSZ is too small, edit pan.h");
	memset((char *)qptr(i), 0, j);
	((Q0 *)qptr(i))->_t = n;
	return i+1;
}

void
qsend(int into, int sorted, int fld0)
{	int j, k; uchar *z;

	if (!into--)
	uerror("ref to uninitialized chan name (sending)");
#ifndef HSFSPIN
	if (into >= (int) now._nr_qs || into < 0)
#else
	if (into >= (int) now->_nr_qs || into < 0)
#endif //
		Uerror("qsend bad queue#");
	z = qptr(into);
	j = ((Q0 *)qptr(into))->Qlen;
	switch (((Q0 *)qptr(into))->_t) {
	case 4:
#ifndef HSFSPIN
		(trpt+1)->bup.oval = j;
#endif //
		((Q4 *)z)->Qlen = ((Q4 *)z)->Qlen + 1;
		((Q4 *)z)->contents[j].fld0 = fld0;
		break;
	case 3:
#ifndef HSFSPIN
		(trpt+1)->bup.oval = j;
#endif //
		((Q3 *)z)->Qlen = ((Q3 *)z)->Qlen + 1;
		((Q3 *)z)->contents[j].fld0 = fld0;
		break;
	case 2:
#ifndef HSFSPIN
		(trpt+1)->bup.oval = j;
#endif //
		((Q2 *)z)->Qlen = ((Q2 *)z)->Qlen + 1;
		((Q2 *)z)->contents[j].fld0 = fld0;
		break;
	case 1:
#ifndef HSFSPIN
		(trpt+1)->bup.oval = j;
#endif //
		((Q1 *)z)->Qlen = ((Q1 *)z)->Qlen + 1;
		((Q1 *)z)->contents[j].fld0 = fld0;
		break;
	case 0: printf("queue %d was deleted\n", into+1);
	default: Uerror("bad queue - qsend");
	}
#ifdef EVENT_TRACE
	if (in_s_scope(into+1))
		require('s', into);
#endif //
}

#if SYNC
int
q_zero(int from)
{	if (!from--)
	uerror("ref to uninitialized chan name (q_zero)");
	switch(((Q0 *)qptr(from))->_t) {
	case 4: return 0;
	case 3: return 0;
	case 2: return 0;
	case 1: return 0;
	case 0: printf("queue %d was deleted\n", from+1);
	}
	Uerror("bad queue q-zero");
	return -1;
}
int
not_RV(int from)
{	if (q_zero(from))
	{	printf("==>> a test of the contents of a rv ");
		printf("channel always returns FALSE\n");
		uerror("error to poll rendezvous channel");
	}
	return 1;
}
#endif //
#ifndef XUSAFE
void
setq_claim(int x, int m, char *s, int y, char *p)
{	if (x == 0)
	uerror("x[rs] claim on uninitialized channel");
	if (x < 0 || x > MAXQ)
		Uerror("cannot happen setq_claim");
	q_claim[x] |= m;
	p_name[y] = p;
	q_name[x] = s;
	if (m&2) q_S_check(x, y);
	if (m&1) q_R_check(x, y);
}
short q_sender[MAXQ+1];
int
q_S_check(int x, int who)
{	if (!q_sender[x])
	{	q_sender[x] = who+1;
#if SYNC
		if (q_zero(x))
		{	printf("chan %s (%d), ",
				q_name[x], x-1);
			printf("sndr proc %s (%d)\n",
				p_name[who], who);
			uerror("xs chans cannot be used for rv");
		}
#endif //
	} else
	if (q_sender[x] != who+1)
	{	printf("pan: xs assertion violated: ");
		printf("access to chan <%s> (%d)\npan: by ",
			q_name[x], x-1);
		printf("%s (proc %d) and by %s (proc %d)\n",
			p_name[q_sender[x]-1], q_sender[x]-1,
			p_name[who], who);
		uerror("error, partial order reduction invalid");
	}
	return 1;
}
short q_recver[MAXQ+1];
int
q_R_check(int x, int who)
{	if (!q_recver[x])
	{	q_recver[x] = who+1;
#if SYNC
		if (q_zero(x))
		{	printf("chan %s (%d), ",
				q_name[x], x-1);
			printf("recv proc %s (%d)\n",
				p_name[who], who);
			uerror("xr chans cannot be used for rv");
		}
#endif //
	} else
	if (q_recver[x] != who+1)
	{	printf("pan: xr assertion violated: ");
		printf("access to chan %s (%d)\n",
			q_name[x], x-1);
		printf("pan: by %s (proc %d) ",
			p_name[q_recver[x]-1], q_recver[x]-1);
		printf("and by %s (proc %d)\n",
			p_name[who], who);
		uerror("error, partial order reduction invalid");
	}
	return 1;
}
#endif //
int
q_len(int x)
{	if (!x--)
	uerror("ref to uninitialized chan name (len)");
	return ((Q0 *)qptr(x))->Qlen;
}

int
q_full(int from)
{	if (!from--)
	uerror("ref to uninitialized chan name (qfull)");
	switch(((Q0 *)qptr(from))->_t) {
	case 4: return (q_sz(from) == 1);
	case 3: return (q_sz(from) == 1);
	case 2: return (q_sz(from) == 1);
	case 1: return (q_sz(from) == 1);
	case 0: printf("queue %d was deleted\n", from+1);
	}
	Uerror("bad queue - q_full");
	return 0;
}

#ifdef HAS_UNLESS
int
q_e_f(int from)
{	/* empty or full */
	return !q_len(from) || q_full(from);
}
#endif //
int
qrecv(int from, int slot, int fld, int done)
{	uchar *z;
	int j, k, r=0;

	if (!from--)
	uerror("ref to uninitialized chan name (receiving)");
#ifndef HSFSPIN
	if (from >= (int) now._nr_qs || from < 0)
#else
	if (from >= (int) now->_nr_qs || from < 0)
#endif //
		Uerror("qrecv bad queue#");
	z = qptr(from);
#ifdef EVENT_TRACE
	if (done && (in_r_scope(from+1)))
		require('r', from);
#endif //
	switch (((Q0 *)qptr(from))->_t) {
	case 4:
		if (fld == 0) r = ((Q4 *)z)->contents[slot].fld0;
		if (done)
		{	j = ((Q4 *)z)->Qlen;
			((Q4 *)z)->Qlen = --j;
			for (k=slot; k<j; k++)
			{
				((Q4 *)z)->contents[k].fld0 = 
					((Q4 *)z)->contents[k+1].fld0;
			}
			((Q4 *)z)->contents[j].fld0 = 0;
			if (fld+1 != 1)
				uerror("missing pars in receive");
		}
		break;
	case 3:
		if (fld == 0) r = ((Q3 *)z)->contents[slot].fld0;
		if (done)
		{	j = ((Q3 *)z)->Qlen;
			((Q3 *)z)->Qlen = --j;
			for (k=slot; k<j; k++)
			{
				((Q3 *)z)->contents[k].fld0 = 
					((Q3 *)z)->contents[k+1].fld0;
			}
			((Q3 *)z)->contents[j].fld0 = 0;
			if (fld+1 != 1)
				uerror("missing pars in receive");
		}
		break;
	case 2:
		if (fld == 0) r = ((Q2 *)z)->contents[slot].fld0;
		if (done)
		{	j = ((Q2 *)z)->Qlen;
			((Q2 *)z)->Qlen = --j;
			for (k=slot; k<j; k++)
			{
				((Q2 *)z)->contents[k].fld0 = 
					((Q2 *)z)->contents[k+1].fld0;
			}
			((Q2 *)z)->contents[j].fld0 = 0;
			if (fld+1 != 1)
				uerror("missing pars in receive");
		}
		break;
	case 1:
		if (fld == 0) r = ((Q1 *)z)->contents[slot].fld0;
		if (done)
		{	j = ((Q1 *)z)->Qlen;
			((Q1 *)z)->Qlen = --j;
			for (k=slot; k<j; k++)
			{
				((Q1 *)z)->contents[k].fld0 = 
					((Q1 *)z)->contents[k+1].fld0;
			}
			((Q1 *)z)->contents[j].fld0 = 0;
			if (fld+1 != 1)
				uerror("missing pars in receive");
		}
		break;
	case 0: printf("queue %d was deleted\n", from+1);
	default: Uerror("bad queue - qrecv");
	}
	return r;
}

#ifndef BITSTATE
#ifdef COLLAPSE
long
col_q(int i, char *z)
{	int j, k;
	char *x, *y;
	Q0 *ptr = (Q0 *) qptr(i);
	switch (ptr->_t) {
	case 4: j = sizeof(Q4); break;
	case 3: j = sizeof(Q3); break;
	case 2: j = sizeof(Q2); break;
	case 1: j = sizeof(Q1); break;
	default: Uerror("bad qtype - collapse");
	}
	if (z) x = z; else x = scratch;
	y = (char *) ptr; k = q_offset[i];
	/* no need to store the empty slots at the end */
	j -= (q_max[ptr->_t] - ptr->Qlen) * ((j - 2)/q_max[ptr->_t]);
	for ( ; j > 0; j--, y++)
		if (!Mask[k++]) *x++ = *y;
	if (z) return (long) (x - z);
	for (j = 0; j < WS-1; j++)
		*x++ = 0;
	x -= j;
	return ordinal(scratch, x-scratch, 1); /* chan */
}
#endif //
#endif //
#ifndef HSFSPIN
int 
unsend(int into)
{	int m=0, j, k; uchar *z;

	if (!into--)
		uerror("ref to uninitialized chan (unsend)");
	z = qptr(into);
	j = ((Q0 *)z)->Qlen;
	((Q0 *)z)->Qlen = --j;
	switch (((Q0 *)qptr(into))->_t) {
	case 4:
		((Q4 *)z)->contents[j].fld0 = 0;
		m = trpt->o_m;
		break;
	case 3:
		((Q3 *)z)->contents[j].fld0 = 0;
		m = trpt->o_m;
		break;
	case 2:
		((Q2 *)z)->contents[j].fld0 = 0;
		m = trpt->o_m;
		break;
	case 1:
		((Q1 *)z)->contents[j].fld0 = 0;
		m = trpt->o_m;
		break;
	default: Uerror("bad queue - unsend");
	}
	return m;
}

void
unrecv(int from, int slot, int fld, int fldvar, int strt)
{	int j; uchar *z;

	if (!from--)
		uerror("ref to uninitialized chan (unrecv)");
	z = qptr(from);
	j = ((Q0 *)z)->Qlen;
	if (strt) ((Q0 *)z)->Qlen = j+1;
	switch (((Q0 *)qptr(from))->_t) {
	case 4:
		if (strt) {
			((Q4 *)z)->contents[slot].fld0 = 0;
		}
		if (fld == 0) ((Q4 *)z)->contents[slot].fld0 = fldvar;
		break;
	case 3:
		if (strt) {
			((Q3 *)z)->contents[slot].fld0 = 0;
		}
		if (fld == 0) ((Q3 *)z)->contents[slot].fld0 = fldvar;
		break;
	case 2:
		if (strt) {
			((Q2 *)z)->contents[slot].fld0 = 0;
		}
		if (fld == 0) ((Q2 *)z)->contents[slot].fld0 = fldvar;
		break;
	case 1:
		if (strt) {
			((Q1 *)z)->contents[slot].fld0 = 0;
		}
		if (fld == 0) ((Q1 *)z)->contents[slot].fld0 = fldvar;
		break;
	default: Uerror("bad queue - qrecv");
	}
}
#endif //
int
q_cond(short II, Trans *t)
{	int i = 0;
	for (i = 0; i < 6; i++)
	{	if (t->ty[i] == TIMEOUT_F) return 1;
		if (t->ty[i] == ALPHA_F)
#ifdef GLOB_ALPHA
			return 0;
#else
			return 
#ifndef HSFSPIN
(II+1 == (short) now._nr_pr && II+1 < MAXPROC);
#else
(II+1 == (short) now->_nr_pr && II+1 < MAXPROC);
#endif //
#endif //
		switch (t->qu[i]) {
		case 0: break;
		case 1: if (	(t->ty[i] == Q_FULL_F && ( q_full(NOW
forks[0])
			 ||     q_full(NOW
forks[1])
			 ||     q_full(NOW
forks[2])
			 ||     q_full(NOW
forks[3])))
			 || 	(t->ty[i] == Q_FULL_T && (!q_full(NOW
forks[0])
			 ||    !q_full(NOW
forks[1])
			 ||    !q_full(NOW
forks[2])
			 ||    !q_full(NOW
forks[3])))
			 || 	(t->ty[i] == Q_EMPT_F && ( !q_len(NOW
forks[0])
			 ||     !q_len(NOW
forks[1])
			 ||     !q_len(NOW
forks[2])
			 ||     !q_len(NOW
forks[3])))
			 || 	(t->ty[i] == Q_EMPT_T && (  q_len(NOW
forks[0])
			 ||      q_len(NOW
forks[1])
			 ||      q_len(NOW
forks[2])
			 ||      q_len(NOW
forks[3])))
			    ) return 0; break;
		default: Uerror("unknown qid - q_cond");
				return 0;
		}
	}
	return 1;
}
void
to_compile(void)
{	char ctd[1024], carg[64]; int n;
#ifdef BITSTATE
	strcpy(ctd, "-DBITSTATE ");
#else
	strcpy(ctd, "");
#endif //
#ifdef PC
	strcat(ctd, "-DPC ");
#endif //
#ifdef NOVSZ
	strcat(ctd, "-DNOVSZ ");
#endif //
#ifdef MEMCNT
#ifdef PC
	n = 25;
#else
	n = 28;
#endif //
	if (MEMCNT != n)
	{	sprintf(carg, "-DMEMCNT=%d ", MEMCNT);
		strcat(ctd, carg);
	}
#endif //
#ifdef MEMLIM
	sprintf(carg, "-DMEMLIM=%d ", MEMLIM);
	strcat(ctd, carg);
#endif //
#ifdef NOCLAIM
	strcat(ctd, "-DNOCLAIM ");
#endif //
#ifdef SAFETY
	strcat(ctd, "-DSAFETY ");
#else
#ifdef NOFAIR
	strcat(ctd, "-DNOFAIR ");
#else
#ifdef NFAIR
	if (NFAIR != 2)
	{	sprintf(carg, "-DNFAIR=%d ", NFAIR);
		strcat(ctd, carg);
	}
#endif //
#endif //
#endif //
#ifdef NOREDUCE
	strcat(ctd, "-DNOREDUCE ");
#else
#ifdef XUSAFE
	strcat(ctd, "-DXUSAFE ");
#endif //
#endif //
#ifdef NP
	strcat(ctd, "-DNP ");
#endif //
#ifdef PEG
	strcat(ctd, "-DPEG ");
#endif //
#ifdef VAR_RANGES
	strcat(ctd, "-DVAR_RANGES ");
#endif //
#ifdef HC0
	strcat(ctd, "-DHC0 ");
#endif //
#ifdef HC1
	strcat(ctd, "-DHC1 ");
#endif //
#ifdef HC2
	strcat(ctd, "-DHC2 ");
#endif //
#ifdef HC3
	strcat(ctd, "-DHC3 ");
#endif //
#ifdef HC4
	strcat(ctd, "-DHC4 ");
#endif //
#ifdef CHECK
	strcat(ctd, "-DCHECK ");
#endif //
#ifdef CTL
	strcat(ctd, "-DCTL ");
#endif //
#ifdef NIBIS
	strcat(ctd, "-DNIBIS ");
#endif //
#ifdef NOBOUNDCHECK
	strcat(ctd, "-DNOBOUNDCHECK ");
#endif //
#ifdef NOSTUTTER
	strcat(ctd, "-DNOSTUTTER ");
#endif //
#ifdef REACH
	strcat(ctd, "-DREACH ");
#endif //
#ifdef PRINTF
	strcat(ctd, "-DPRINTF ");
#endif //
#ifdef OTIM
	strcat(ctd, "-DOTIM ");
#endif //
#ifdef COLLAPSE
	strcat(ctd, "-DCOLLAPSE ");
#endif //
#ifdef SVDUMP
	strcat(ctd, "-DSVDUMP ");
#endif //
#ifdef VECTORSZ
	if (VECTORSZ != 1024)
	{	sprintf(carg, "-DVECTORSZ=%d ", VECTORSZ);
		strcat(ctd, carg);
	}
#endif //
#ifdef VERBOSE
	strcat(ctd, "-DVERBOSE ");
#endif //
#ifdef CHECK
	strcat(ctd, "-DCHECK ");
#endif //
#ifdef SDUMP
	strcat(ctd, "-DSDUMP ");
#endif //
#ifdef COVEST
		strcat(ctd, "-DCOVEST ");
#endif //
		printf("Compiled as: cc -o pan %span.c", ctd);
#if defined(COVEST) && defined(BITSTATE)
		printf(" -lm\n");
#else
		printf("\n");
#endif //
}
void
active_procs(void)
{
	Addproc(1);
}
#ifdef MA
/*
#include <stdio.h>
#define uchar	unsigned char
*/
#define ulong	unsigned long
#define ushort	unsigned short

#define TWIDTH		256
#define HASH(y,n)	(n)*(((int)y))
#define INRANGE(e,h)	((h>=e->From && h<=e->To)||(e->s==1 && e->S==h))

#ifndef HSFSPIN
extern char	*emalloc(unsigned long);	/* imported routine  */
#endif //
extern void	dfa_init(ushort);	/* 4 exported routines */
extern int	dfa_member(ushort);
extern int	dfa_store(uchar *);
extern void	dfa_stats(void);

typedef struct Edge {
	uchar From, To;		/* max range 0..255 */
	uchar s, S;		/* if s=1, S is singleton */
	struct Vertex	*Dst;
	struct Edge	*Nxt;
} Edge;

typedef struct Vertex {
	ulong	key, num;	/* key for splay tree, nr incoming edges */
	uchar	from[2], to[2];	/* in-node predefined edge info    */
	struct	Vertex	*dst[2];/* most nodes have 2 or more edges */
	struct	Edge	*Succ;	/* in case there are more edges */
	struct	Vertex	*lnk, *left, *right; /* splay tree plumbing */
} Vertex;

static Edge	*free_edges;
static Vertex	*free_vertices;
static Vertex	**layers;	/* one splay tree of nodes per layer */
static Vertex	**path;		/* run of word in the DFA */
static Vertex	*R, *F, *NF;	/* Root, Final, Not-Final */
static uchar	*word, *lastword;/* string, and last string inserted */
static int	dfa_depth, iv=0, nv=0, pfrst=0, Tally;

static void	insert_it(Vertex *, int);	/* splay-tree code */
static void	delete_it(Vertex *, int);
static Vertex	*find_it(Vertex *, Vertex *, uchar, int);

static void
recyc_edges(Edge *e)
{
	if (!e) return;
	recyc_edges(e->Nxt);
	e->Nxt = free_edges;
	free_edges = e;
}

static Edge *
new_edge(Vertex *dst)
{	Edge *e;

	if (free_edges)
	{	e = free_edges;
		free_edges = e->Nxt;
		e->From = e->To = e->s = e->S = 0;
		e->Nxt = (Edge *) 0;
	} else
#ifndef HSFSPIN
		e = (Edge *) emalloc(sizeof(Edge));
#else
		e = new Edge;
#endif //
	e->Dst = dst;

	return e;
}

static void
recyc_vertex(Vertex *v)
{
	recyc_edges(v->Succ);
	v->Succ = (Edge *) free_vertices;
	free_vertices = v;
	nr_states--;
}

static Vertex *
new_vertex(void)
{	Vertex *v;

	if (free_vertices)
	{	v = free_vertices;
		free_vertices = (Vertex *) v->Succ;
		v->Succ = (Edge *) 0;
		v->num  = 0;
	} else
#ifndef HSFSPIN
		v = (Vertex *) emalloc(sizeof(Vertex));
#else
		v = new Vertex;
#endif //

	nr_states++;
	return v; 
}

static Vertex *
allDelta(Vertex *v, int n)
{	Vertex *dst = new_vertex();

	v->from[0] = 0;
	v->to[0] = 255;
	v->dst[0] = dst;
	dst->num = 256;
	insert_it(v, n);
	return dst;
}

static void
insert_edge(Vertex *v, Edge *e)
{	/* put new edge first */
	if (!v->dst[0])
	{	v->dst[0] = e->Dst;
		v->from[0] = e->From;
		v->to[0] = e->To;
		recyc_edges(e);
		return;
	}
	if (!v->dst[1])
	{	v->from[1] = v->from[0]; v->from[0] = e->From;
		v->to[1]   = v->to[0];   v->to[0]   = e->To;
		v->dst[1]  = v->dst[0];  v->dst[0]  = e->Dst;
		recyc_edges(e);
		return;
	} /* shift */
	{	int f      = v->from[1];
		int t      = v->to[1];
		Vertex *d  = v->dst[1];
		v->from[1] = v->from[0]; v->from[0] = e->From;
		v->to[1]   = v->to[0];   v->to[0]   = e->To;
		v->dst[1]  = v->dst[0];  v->dst[0]  = e->Dst;
		e->From = f;
		e->To   = t;
		e->Dst  = d;
	}
	e->Nxt = v->Succ;
	v->Succ = e;
}

static void
copyRecursive(Vertex *v, Edge *e)
{	Edge *f;
	if (e->Nxt) copyRecursive(v, e->Nxt);
	f = new_edge(e->Dst);
	f->From = e->From;
	f->To   = e->To;
	f->s    = e->s;
	f->S    = e->S;
	f->Nxt  = v->Succ;
	v->Succ = f;
}

static void
copyEdges(Vertex *to, Vertex *from)
{	int i;
	for (i = 0; i < 2; i++)
	{	to->from[i] = from->from[i];
		to->to[i]   = from->to[i];
		to->dst[i]  = from->dst[i];
	}
	if (from->Succ) copyRecursive(to, from->Succ);
}

static Edge *
cacheDelta(Vertex *v, int h, int first)
{	static Edge *ov, tmp;  int i;

	if (!first && INRANGE(ov,h))
		return ov; /* intercepts about 10% */
	for (i = 0; i < 2; i++)
		if (v->dst[i] && h >= v->from[i] && h <= v->to[i])
		{	tmp.From = v->from[i];
			tmp.To   = v->to[i];
			tmp.Dst  = v->dst[i];
			tmp.s    =  tmp.S = 0;
			ov = &tmp;
			return ov;
		}
	for (ov = v->Succ; ov; ov = ov->Nxt)
		if (INRANGE(ov,h)) return ov;

	Uerror("cannot get here, cacheDelta");
	return (Edge *) 0;
}

static Vertex *
Delta(Vertex *v, int h)	/* v->delta[h] */
{	register Edge *e;

	if (v->dst[0] && h >= v->from[0] && h <= v->to[0])
		return v->dst[0];	/* oldest edge */
	if (v->dst[1] && h >= v->from[1] && h <= v->to[1])
		return v->dst[1];
	for (e = v->Succ; e; e = e->Nxt)
		if (INRANGE(e,h))
			return e->Dst;
	Uerror("cannot happen Delta");
	return (Vertex *) 0;
}

static void
numDelta(Vertex *v, int d)
{	register Edge *e;
	register ulong cnt;
	int i;

	for (i = 0; i < 2; i++)
	if (v->dst[i])
	{	cnt = v->dst[i]->num + d*(1 + v->to[i] - v->from[i]);
		if (d == 1 && cnt < v->dst[i]->num) goto bad;
		v->dst[i]->num = cnt;
	}
	for (e = v->Succ; e; e = e->Nxt)
	{	cnt = e->Dst->num + d*(1 + e->To - e->From + e->s);
		if (d == 1 && cnt < e->Dst->num)
bad:			Uerror("too many incoming edges");
		e->Dst->num = cnt;
	}
}

static void
setDelta(Vertex *v, int h, Vertex *newdst)	/* v->delta[h] = newdst; */
{	Edge *e, *f = (Edge *) 0, *g;
	int i;

	/* remove the old entry, if there */
	for (i = 0; i < 2; i++)
		if (v->dst[i] && h >= v->from[i] && h <= v->to[i])
		{	if (h == v->from[i])
			{	if (h == v->to[i])
				{	v->dst[i] = (Vertex *) 0;
					v->from[i] = v->to[i] = 0;
				} else
					v->from[i]++;
			} else if (h == v->to[i])
			{	v->to[i]--;
			} else
			{	g = new_edge(v->dst[i]);/* same dst */
				g->From    = v->from[i];
				g->To      = h-1;	/* left half */
				v->from[i] = h+1;	/* right half */
				insert_edge(v, g);
			}
			goto part2;
		}
	for (e = v->Succ; e; f = e, e = e->Nxt)
	{	if (e->s == 1 && e->S == h)
		{	e->s = e->S = 0;
			goto rem_tst;
		}
		if (h >= e->From && h <= e->To)
		{	if (h == e->From)
			{	if (h == e->To)
				{	if (e->s)
					{	e->From = e->To = e->S;
						e->s = 0;
						break;
					} else
						goto rem_do;
				} else
					e->From++;
			} else if (h == e->To)
			{	e->To--;
			} else				/* split */
			{	g = new_edge(e->Dst);	/* same dst */
				g->From = e->From;
				g->To   = h-1;		/* g=left half */
				e->From = h+1;		/* e=right half */
				g->Nxt  = e->Nxt;	/* insert g */
				e->Nxt  = g;		/* behind e */
				break;			/* done */
			}

rem_tst:		if (e->From > e->To)
			{	if (e->s == 0) {
rem_do:				if (f)
						f->Nxt = e->Nxt;
					else
						v->Succ = e->Nxt;
					e->Nxt = (Edge *) 0;
					recyc_edges(e);
				} else
				{	e->From = e->To = e->S;
					e->s = 0;
			}	}
			break;
	}	}
part2:
	/* check if newdst is already there */
	for (i = 0; i < 2; i++)
		if (v->dst[i] == newdst)
		{	if (h+1 == (int) v->from[i])
			{	v->from[i] = h;
				return;
			}
			if (h == (int) v->to[i]+1)
			{	v->to[i] = h;
				return;
		}	}
	for (e = v->Succ; e; e = e->Nxt)
	{	if (e->Dst == newdst)
		{	if (h+1 == (int) e->From)
			{	e->From = h;
				if (e->s == 1 && e->S+1 == e->From)
				{	e->From = e->S;
					e->s = e->S = 0;
				}
				return;
			}
			if (h == (int) e->To+1)
			{	e->To = h;
				if (e->s == 1 && e->S == e->To+1)
				{	e->To = e->S;
					e->s = e->S = 0;
				}
				return;
			}
			if (e->s == 0)
			{	e->s = 1;
				e->S = h;
				return;
	}	}	}
	/* add as a new edge */
	e = new_edge(newdst);
	e->From = e->To = h;
	insert_edge(v, e);
}

static ulong
cheap_key(Vertex *v)
{	ulong vk2 = 0;

	if (v->dst[0])
	{	vk2 = (ulong) v->dst[0];
		if ((ulong) v->dst[1] > vk2)
			vk2 = (ulong) v->dst[1];
	} else if (v->dst[1])
		vk2 = (ulong) v->dst[1]; 
	if (v->Succ)
	{	Edge *e;
		for (e = v->Succ; e; e = e->Nxt)
			if ((ulong) e->Dst > vk2)
				vk2 = (ulong) e->Dst;
	}
	Tally = (vk2>>2)&(TWIDTH-1);
	return v->key;
}

static ulong
mk_key(Vertex *v)	/* not sensitive to order */
{	register ulong m = 0, vk2 = 0;
	register Edge *e;

	if (v->dst[0])
	{	m += HASH(v->dst[0], v->to[0] - v->from[0] + 1);
		vk2 = (ulong) v->dst[0]; 
	}
	if (v->dst[1])
	{	m += HASH(v->dst[1], v->to[1] - v->from[1] + 1);
		if ((ulong) v->dst[1] > vk2) vk2 = (ulong) v->dst[1]; 
	}
	for (e = v->Succ; e; e = e->Nxt)
	{	m += HASH(e->Dst, e->To - e->From + 1 + e->s);
		if ((ulong) e->Dst > vk2) vk2 = (ulong) e->Dst; 
	}
	Tally = (vk2>>2)&(TWIDTH-1);
	return m;
}

static ulong
mk_special(int sigma, Vertex *n, Vertex *v)
{	register ulong m = 0, vk2 = 0;
	register Edge *f; Vertex *last = (Vertex *) 0;
	int i;

	for (i = 0; i < 2; i++)
		if (v->dst[i])
		{	if (sigma >= v->from[i] && sigma <= v->to[i])
			{	m += HASH(v->dst[i], v->to[i]-v->from[i]);
				if ((ulong) v->dst[i] > vk2
				&&   v->to[i] > v->from[i])
					vk2 = (ulong) v->dst[i]; 
			} else
			{	m += HASH(v->dst[i], v->to[i]-v->from[i]+1);
				if ((ulong) v->dst[i] > vk2)
					vk2 = (ulong) v->dst[i]; 
		}	}
	for (f = v->Succ; f; f = f->Nxt)
	{	if (sigma >= f->From && sigma <= f->To)
		{	m += HASH(f->Dst, f->To - f->From + f->s);
			if ((ulong) f->Dst > vk2
			&&   f->To - f->From + f->s > 0)
				vk2 = (ulong) f->Dst; 
		} else if (f->s == 1 && sigma == f->S)
		{	m += HASH(f->Dst, f->To - f->From + 1);
			if ((ulong) f->Dst > vk2) vk2 = (ulong) f->Dst; 
		} else
		{	m += HASH(f->Dst, f->To - f->From + 1 + f->s);
			if ((ulong) f->Dst > vk2) vk2 = (ulong) f->Dst; 
	}	}

	if ((ulong) n > vk2) vk2 = (ulong) n; 
	Tally = (vk2>>2)&(TWIDTH-1);
	m += HASH(n, 1);
	return m;
}

void 
dfa_init(ushort nr_layers)
{	int i; Vertex *r, *t;

	dfa_depth = nr_layers;	/* one byte per layer */
#ifndef HSFSPIN
	path   = (Vertex **) emalloc((dfa_depth+1)*sizeof(Vertex *));
	layers = (Vertex **) emalloc(TWIDTH*(dfa_depth+1)*sizeof(Vertex *));
	lastword = (uchar *) emalloc((dfa_depth+1)*sizeof(uchar));
#else
	path   = new Vertex*[dfa_depth+1);
	layers = new Vertex*[TWIDTH*(dfa_depth+1)];
	lastword = new unsigned char[dfa_depth+1];
#endif //
	lastword[dfa_depth] = lastword[0] = 255;
	path[0] = R = new_vertex(); F = new_vertex();

	for (i = 1, r = R; i < dfa_depth; i++, r = t)
		t = allDelta(r, i-1);
	NF = allDelta(r, i-1);
}

#if 0
static void complement_dfa(void) { Vertex *tmp = F; F = NF; NF = tmp; }
#endif //

double
tree_stats(Vertex *t)
{	Edge *e; double cnt=0.0;
	if (!t) return 0;
	if (!t->key) return 0;
	t->key = 0; /* precaution */
	if (t->dst[0]) cnt++;
	if (t->dst[1]) cnt++;
	for (e = t->Succ; e; e = e->Nxt)
		cnt++;
	cnt += tree_stats(t->lnk);
	cnt += tree_stats(t->left);
	cnt += tree_stats(t->right);
	return cnt;
}

void
dfa_stats(void)
{	int i, j; double cnt = 0.0;
	for (j = 0; j < TWIDTH; j++)
	for (i = 0; i < dfa_depth+1; i++)
		cnt += tree_stats(layers[i*TWIDTH+j]);
	printf("Minimized Automaton:	%6d nodes and %6g edges\n",
		nr_states, cnt);
}

int
dfa_member(ushort n)
{	Vertex **p, **q;
	uchar *w = &word[n];
	int i;

	p = &path[n]; q = (p+1);
	for (i = n; i < dfa_depth; i++)
		*q++ = Delta(*p++, *w++);
	return (*p == F);
}

int
dfa_store(uchar *sv)
{	Vertex **p, **q, *s, *y, *old, *new = F;
	uchar *w, *u = lastword;
	int i, j, k;

	w = word = sv;
	while (*w++ == *u++)	/* find first byte that differs */
		;
	pfrst = (int) (u - lastword) - 1;
	memcpy(&lastword[pfrst], &sv[pfrst], dfa_depth-pfrst);
	if (pfrst > iv) pfrst = iv;
	if (pfrst > nv) pfrst = nv;
phase1:
	p = &path[pfrst]; q = (p+1); w = &word[pfrst];
	for (i = pfrst; i < dfa_depth; i++)
		*q++ = Delta(*p++, *w++);	/* (*p)->delta[*w++]; */

	if (*p == F) return 1;	/* it's already there */
phase2:
	iv = dfa_depth;
	do {	iv--;
		old = new;
		new = find_it(path[iv], old, word[iv], iv);
	} while (new && iv > 0);

phase3:
	nv = k = 0; s = path[0];
	for (j = 1; j <= iv; ++j) 
		if (path[j]->num > 1)
		{	y = new_vertex();
			copyEdges(y, path[j]);
			insert_it(y, j);
			numDelta(y, 1);
			delete_it(s, j-1);
			setDelta(s, word[j-1], y);
			insert_it(s, j-1);
			y->num = 1;	/* initial value 1 */
			s = y;
			path[j]->num--;	/* only 1 moved from j to y */
			k = 1;
		} else
		{	s = path[j];
			if (!k) nv = j;
		}
	y = Delta(s, word[iv]);
	y->num--;
	delete_it(s, iv); 
	setDelta(s, word[iv], old);
	insert_it(s, iv); 
	old->num++;

	for (j = iv+1; j < dfa_depth; j++)
		if (path[j]->num == 0)
		{	numDelta(path[j], -1);
			delete_it(path[j], j);
			recyc_vertex(path[j]);
		} else
			break;
	return 0;
}

static Vertex *
splay(ulong i, Vertex *t)
{	Vertex N, *l, *r, *y;

	if (!t) return t;
	N.left = N.right = (Vertex *) 0;
	l = r = &N;
	for (;;)
	{	if (i < t->key)
		{	if (!t->left) break;
			if (i < t->left->key)
			{	y = t->left;
				t->left = y->right;
				y->right = t;
				t = y;
				if (!t->left) break;
			}
			r->left = t;
			r = t;
			t = t->left;
		} else if (i > t->key)
		{	if (!t->right) break;
			if (i > t->right->key)
			{	y = t->right;
				t->right = y->left;
				y->left = t;
				t = y;
				if (!t->right) break;
			}
			l->right = t;
			l = t;
			t = t->right;
		} else
			break;
	}
	l->right = t->left;
	r->left = t->right;
	t->left = N.right;
	t->right = N.left;
	return t;
}

static void
insert_it(Vertex *v, int L)
{	Vertex *new, *t;
	ulong i; int nr;

	i = mk_key(v);
	nr = ((L*TWIDTH)+Tally);
	t = layers[nr];

	v->key = i; 
	if (!t)
	{	layers[nr] = v;
		return;
	}
	t = splay(i, t);
	if (i < t->key)
	{	new = v;
		new->left = t->left;
		new->right = t;
		t->left = (Vertex *) 0;
	} else if (i > t->key)
	{	new = v;
		new->right = t->right;
		new->left = t;
		t->right = (Vertex *) 0;
	} else	 /* it's already there */
	{	v->lnk = t->lnk; /* put in linked list off v */
		t->lnk = v;
		new = t;
	}
	layers[nr] = new;
}

static int
checkit(Vertex *h, Vertex *v, Vertex *n, uchar sigma)
{	Edge *g, *f;
	int i, k, j = 1;

	for (k = 0; k < 2; k++)
		if (h->dst[k])
		{	if (sigma >= h->from[k] && sigma <= h->to[k])
			{	if (h->dst[k] != n) goto no_match;
			}
			for (i = h->from[k]; i <= h->to[k]; i++)
			{	if (i == sigma) continue;
				g = cacheDelta(v, i, j); j = 0;
				if (h->dst[k] != g->Dst)
					goto no_match;
				if (g->s == 0 || g->S != i)
					i = g->To;
		}	}
	for (f = h->Succ; f; f = f->Nxt)
	{	if (INRANGE(f,sigma))
		{	if (f->Dst != n) goto no_match;
		}
		for (i = f->From; i <= f->To; i++)
		{	if (i == sigma) continue;
			g = cacheDelta(v, i, j); j = 0;
			if (f->Dst != g->Dst)
				goto no_match;
			if (g->s == 1 && i == g->S)
				continue;
			i = g->To;
		}
		if (f->s && f->S != sigma)
		{	g = cacheDelta(v, f->S, 1);
			if (f->Dst != g->Dst)
				goto no_match;
		}
	}
	if (h->Succ || h->dst[0] || h->dst[1]) return 1;
no_match:
	return 0;
}

static Vertex *
find_it(Vertex *v, Vertex *n, uchar sigma, int L)
{	Vertex *z, *t;
	ulong i; int nr;

	i = mk_special(sigma,n,v);
	nr = ((L*TWIDTH)+Tally);
	t = layers[nr];

	if (!t) return (Vertex *) 0;
	layers[nr] = t = splay(i, t);
	if (i == t->key)
	for (z = t; z; z = z->lnk)
		if (checkit(z, v, n, sigma))
			return z;

	return (Vertex *) 0;
}

static void
delete_it(Vertex *v, int L)
{	Vertex *x, *t;
	ulong i; int nr;

	i = cheap_key(v);
	nr = ((L*TWIDTH)+Tally);
	t = layers[nr];
	if (!t) return;

	t = splay(i, t);
	if (i == t->key)
	{	Vertex *z, *y = (Vertex *) 0;
		for (z = t; z && z != v; y = z, z = z->lnk)
			;
		if (z != v) goto bad;
		if (y)
		{	y->lnk = z->lnk;
			z->lnk = (Vertex *) 0;
			layers[nr] = t;
			return;
		} else if (z->lnk)	/* z == t == v */
		{	y = z->lnk;
			y->left = t->left;
			y->right = t->right;
			t->left = t->right = t->lnk = (Vertex *) 0;
			layers[nr] = y;
			return;
		}
		/* delete the node itself */
		if (!t->left)
		{	x = t->right;
		} else
		{	x = splay(i, t->left);
			x->right = t->right;
		}
		t->left = t->right = t->lnk = (Vertex *) 0;
		layers[nr] = x;
		return;
	}
bad:	Uerror("cannot happen delete");
}
#endif //
#if defined(W_XPT) || defined(R_XPT)
static Vertex	**temptree;
static char	wbuf[4096];
static int	WCNT = 4096, wcnt=0;
static uchar	stacker[MA+1];
static ulong	stackcnt = 0;
extern double	nstates, nlinks, truncs, truncs2;

static void
xwrite(int fd, char *b, int n)
{
	if (wcnt+n >= 4096)
	{	write(fd, wbuf, wcnt);
		wcnt = 0;
	}
	memcpy(&wbuf[wcnt], b, n);
	wcnt += n;
}

static void
wclose(fd)
{
	if (wcnt > 0)
		write(fd, wbuf, wcnt);
	wcnt = 0;
	close(fd);
}

static void
w_vertex(int fd, Vertex *v)
{	char t[3]; int i; Edge *e;

	xwrite(fd, (char *) &v,  sizeof(Vertex *));
	t[0] = 0;
	for (i = 0; i < 2; i++)
		if (v->dst[i])
		{	t[1] = v->from[i], t[2] = v->to[i];
			xwrite(fd, t, 3);
			xwrite(fd, (char *) &(v->dst[i]), sizeof(Vertex *));
		}
	for (e = v->Succ; e; e = e->Nxt)
	{	t[1] = e->From, t[2] = e->To;
		xwrite(fd, t, 3);
		xwrite(fd, (char *) &(e->Dst), sizeof(Vertex *));

		if (e->s)
		{	t[1] = t[2] = e->S;
			xwrite(fd, t, 3);
			xwrite(fd, (char *) &(e->Dst), sizeof(Vertex *));
	}	}
}

static void
w_layer(int fd, Vertex *v)
{	uchar c=1;

	if (!v) return;
	xwrite(fd, (char *) &c, 1);
	w_vertex(fd, v);
	w_layer(fd, v->lnk);
	w_layer(fd, v->left);
	w_layer(fd, v->right);
}

void
w_xpoint(void)
{	int fd; char nm[64];
	int i, j;  uchar c;
	static uchar xwarned = 0;

	sprintf(nm, "%s.xpt", Source);
	if ((fd = creat(nm, 0666)) <= 0)
	if (!xwarned)
	{	xwarned = 1;
		printf("cannot creat checkpoint file\n");
		return;
	}
	xwrite(fd, (char *) &nstates, sizeof(double));
	xwrite(fd, (char *) &truncs, sizeof(double));
	xwrite(fd, (char *) &truncs2, sizeof(double));
	xwrite(fd, (char *) &nlinks, sizeof(double));
	xwrite(fd, (char *) &dfa_depth, sizeof(int));
	xwrite(fd, (char *) &R,  sizeof(Vertex *));
	xwrite(fd, (char *) &F,  sizeof(Vertex *));
	xwrite(fd, (char *) &NF, sizeof(Vertex *));

	for (j = 0; j < TWIDTH; j++)
	for (i = 0; i < dfa_depth+1; i++)
	{	w_layer(fd, layers[i*TWIDTH+j]);
		c = 2; xwrite(fd, (char *) &c, 1);
	}
	wclose(fd);
}

static void
xread(int fd, char *b, int n)
{	int m = wcnt; int delta = 0;
	if (m < n)
	{	if (m > 0) memcpy(b, &wbuf[WCNT-m], m);
		delta = m;
		WCNT = wcnt = read(fd, wbuf, 4096);
		if (wcnt < n-m)
			Uerror("xread failed -- insufficient data");
		n -= m;
	}
	memcpy(&b[delta], &wbuf[WCNT-wcnt], n);
	wcnt -= n;
}

static void
x_cleanup(Vertex *c)
{	Edge *e;	/* remove the tree and edges from c */
	if (!c) return;
	for (e = c->Succ; e; e = e->Nxt)
		x_cleanup(e->Dst);
	recyc_vertex(c);
}

static void
x_remove(void)
{	Vertex *tmp; int i, s;
#if 1
	int r, j;
	/* double-check: */
	stacker[dfa_depth-1] = 0; r = dfa_store(stacker);
	stacker[dfa_depth-1] = 4; j = dfa_member(dfa_depth-1);
	if (r != 1 || j != 0)
	{	printf("%d: ", stackcnt);
		for (i = 0; i < dfa_depth; i++)
			printf("%d,", stacker[i]);
		printf(" -- not a stackstate <o:%d,4:%d>\n", r, j);
		return;
	}
#endif //
	stacker[dfa_depth-1] = 1;
	s = dfa_member(dfa_depth-1);

	{ tmp = F; F = NF; NF = tmp; }	/* complement */
		if (s) dfa_store(stacker);
		stacker[dfa_depth-1] = 0;
		dfa_store(stacker);
		stackcnt++;
	{ tmp = F; F = NF; NF = tmp; }
}

static void
x_rm_stack(Vertex *t, int k)
{	int j; Edge *e;

	if (k == 0)
	{	x_remove();
		return;
	}
	if (t)
	for (e = t->Succ; e; e = e->Nxt)
	{	for (j = e->From; j <= (int) e->To; j++)
		{	stacker[k] = (uchar) j;
			x_rm_stack(e->Dst, k-1);
		}
		if (e->s)
		{	stacker[k] = e->S;
			x_rm_stack(e->Dst, k-1);
	}	}
}

static Vertex *
insert_withkey(Vertex *v, int L)
{	Vertex *new, *t = temptree[L];

	if (!t) { temptree[L] = v; return v; }
	t = splay(v->key, t);
	if (v->key < t->key)
	{	new = v;
		new->left = t->left;
		new->right = t;
		t->left = (Vertex *) 0;
	} else if (v->key > t->key)
	{	new = v;
		new->right = t->right;
		new->left = t;
		t->right = (Vertex *) 0;
	} else
	{	if (t != R && t != F && t != NF)
			Uerror("double insert, bad checkpoint data");
		else
		{	recyc_vertex(v);
			new = t;
	}	}
	temptree[L] = new;

	return new;
}

static Vertex *
find_withkey(Vertex *v, int L)
{	Vertex *t = temptree[L];
	if (t)
	{	temptree[L] = t = splay((ulong) v, t);
		if (t->key == (ulong) v)
			return t;
	}
	Uerror("not found error, bad checkpoint data");
	return (Vertex *) 0;
}

void
r_layer(int fd, int n)
{	Vertex *v;
	Edge *e;
	char c, t[2];

	for (;;)
	{	xread(fd, &c, 1);
		if (c == 2) break;
		if (c == 1)
		{	v = new_vertex();
			xread(fd, (char *) &(v->key), sizeof(Vertex *));
			v = insert_withkey(v, n);
		} else	/* c == 0 */
		{	e = new_edge((Vertex *) 0);
			xread(fd, t, 2);
			e->From = t[0];
			e->To = t[1];
			xread(fd, (char *) &(e->Dst), sizeof(Vertex *));
			insert_edge(v, e);
	}	}
}

static void
v_fix(Vertex *t, int nr)
{	int i; Edge *e;

	if (!t) return;

	for (i = 0; i < 2; i++)
	if (t->dst[i])
		t->dst[i] = find_withkey(t->dst[i], nr);

	for (e = t->Succ; e; e = e->Nxt)
		e->Dst = find_withkey(e->Dst, nr);
		
	v_fix(t->left, nr);
	v_fix(t->right, nr);
}

static void
v_insert(Vertex *t, int nr)
{	Edge *e; int i;

	if (!t) return;
	v_insert(t->left, nr);
	v_insert(t->right, nr);

	/* remove only leafs from temptree */
	t->left = t->right = t->lnk = (Vertex *) 0;
	insert_it(t, nr);	/* into layers */
	for (i = 0; i < 2; i++)
		if (t->dst[i])
			t->dst[i]->num += (t->to[i] - t->from[i] + 1);
	for (e = t->Succ; e; e = e->Nxt)
		e->Dst->num += (e->To - e->From + 1 + e->s);
}

static void
x_fixup(void)
{	int i;

	for (i = 0; i < dfa_depth; i++)
		v_fix(temptree[i], (i+1));

	for (i = dfa_depth; i >= 0; i--)
		v_insert(temptree[i], i);
}

static Vertex *
x_tail(Vertex *t, ulong want)
{	int i, yes, no; Edge *e; Vertex *v = (Vertex *) 0;

	if (!t) return v;

	yes = no = 0;
	for (i = 0; i < 2; i++)
		if ((ulong) t->dst[i] == want)
		{	if (t->from[i] <= 0 && t->to[i] >= 0)
				yes = 1;
			else
			if (t->from[i] <= 4 && t->to[i] >= 4)
				no = 1;
		}

	for (e = t->Succ; e; e = e->Nxt)
		if ((ulong) e->Dst == want)
		{	if (INRANGE(e, 0))
				yes = 1;
			else if (INRANGE(e, 4))
				no = 1;
		}
	if (yes && !no) return t;
	v = x_tail(t->left, want);  if (v) return v;
	v = x_tail(t->right, want); if (v) return v;
	return (Vertex *) 0;
}

static void
x_anytail(Vertex *t, Vertex *c, int nr)
{	int i; Edge *e, *f; Vertex *v;

	if (!t) return;

	for (i = 0; i < 2; i++)
		if ((ulong) t->dst[i] == c->key)
		{	v = new_vertex(); v->key = t->key;
			f = new_edge(v);
			f->From = t->from[i];
			f->To = t->to[i];
			f->Nxt = c->Succ;
			c->Succ = f;
			if (nr > 0)
			x_anytail(temptree[nr-1], v, nr-1);
		}

	for (e = t->Succ; e; e = e->Nxt)
		if ((ulong) e->Dst == c->key)
		{	v = new_vertex(); v->key = t->key;
			f = new_edge(v);
			f->From = e->From;
			f->To = e->To;
			f->s = e->s;
			f->S = e->S;
			f->Nxt = c->Succ;
			c->Succ = f;
			x_anytail(temptree[nr-1], v, nr-1);
		}

	x_anytail(t->left, c, nr);
	x_anytail(t->right, c, nr);
}

static Vertex *
x_cpy_rev(void)
{	Vertex *c, *v;

	/* find 0 and !4 predecessor of F */

	v = x_tail(temptree[dfa_depth-1], F->key);
	if (!v) return (Vertex *) 0;

	c = new_vertex(); c->key = v->key;

	/* every node on dfa_depth-2 that has v->key as succ */
	/* make copy and let c point to these (reversing ptrs) */

	x_anytail(temptree[dfa_depth-2], c, dfa_depth-2);
 
	return c;
}

void
r_xpoint(void)
{	int fd; char nm[64]; Vertex *d;
	int i, j;

	wcnt = 0;
	sprintf(nm, "%s.xpt", Source);
	if ((fd = open(nm, 0)) < 0)	/* O_RDONLY */
		Uerror("cannot open checkpoint file");

	xread(fd, (char *) &nstates,   sizeof(double));
	xread(fd, (char *) &truncs,    sizeof(double));
	xread(fd, (char *) &truncs2,   sizeof(double));
	xread(fd, (char *) &nlinks,    sizeof(double));
	xread(fd, (char *) &dfa_depth, sizeof(int));

	if (dfa_depth != MA+a_cycles)
		Uerror("bad dfa_depth in checkpoint file");

#ifndef HSFSPIN
	path	  = (Vertex **) emalloc((dfa_depth+1)*sizeof(Vertex *));
	layers	  = (Vertex **) emalloc(TWIDTH*(dfa_depth+1)*sizeof(Vertex *));
	temptree  = (Vertex **) emalloc((dfa_depth+2)*sizeof(Vertex *));
	lastword  = (uchar *)   emalloc((dfa_depth+1)*sizeof(uchar));
#else
	path	  = new Vertex*[dfa_depth+1];
	layers	  = new Vertex*[TWIDTH*(dfa_depth+1)];
	temptree  = new Vertex*[dfa_depth+2];
	lastword  = new unsigned char[dfa_depth+1];
#endif //
	lastword[dfa_depth] = lastword[0] = 255; 

	path[0] = R = new_vertex();
	xread(fd, (char *) &R->key, sizeof(Vertex *));
	R = insert_withkey(R, 0);

	F = new_vertex();
	xread(fd, (char *) &F->key, sizeof(Vertex *));
	F = insert_withkey(F, dfa_depth);

	NF = new_vertex();
	xread(fd, (char *) &NF->key, sizeof(Vertex *));
	NF = insert_withkey(NF, dfa_depth);

	for (j = 0; j < TWIDTH; j++)
	for (i = 0; i < dfa_depth+1; i++)
		r_layer(fd, i);

	if (wcnt != 0) Uerror("bad count in checkpoint file");

	d = x_cpy_rev();
	x_fixup();
	stacker[dfa_depth-1] = 0;
	x_rm_stack(d, dfa_depth-2);
	x_cleanup(d);
	close(fd);

	printf("pan: removed %d stackstates\n", stackcnt);
	nstates -= (double) stackcnt;
}
#endif //
#ifdef VERI
void
check_claim(int st)
{
	if (st == endclaim)
		uerror("claim violated!");
	if (stopstate[VERI][st])
		uerror("endstate in claim reached");
}
#endif //
