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

/*
 * This file is part of the UCB release of Plan 9. It is subject to the license
 * terms in the LICENSE file found in the top-level directory of this
 * distribution and at http://akaros.cs.berkeley.edu/files/Plan9License. No
 * part of the UCB release of Plan 9, including this file, may be copied,
 * modified, propagated, or distributed except according to the terms contained
 * in the LICENSE file.
 */

/***** spin: pangen1.h *****/

/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories.     */
/* All Rights Reserved.  This software is for educational purposes only.  */
/* No guarantee whatsoever is expressed or implied by the distribution of */
/* this code.  Permission is given to distribute this code provided that  */
/* this introductory message is not removed and no monies are exchanged.  */
/* Software written by Gerard J. Holzmann.  For tool documentation see:   */
/*             http://spinroot.com/                                       */
/* Send all bug-reports and/or questions to: bugs@spinroot.com            */
/* (c) 2007-2011: additions, enhancements, and bugfixes GJH               */

static char *Code2a[] = { /* the tail of procedure run() */
	"	if (state_tables)",
	"	{ if (dodot) exit(0);",
	"	  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",
	"	  pan_exit(0);",
	"	}",
	"#if defined(BFS) && defined(TRIX)", /* before iniglobals */
	"	{ int i;",
	"	  for (i = 0; i < MAXPROC+1; i++)",
	"	  {	processes[i] = (TRIX_v6 *) emalloc(sizeof(TRIX_v6));",
	"		processes[i]->body = (uchar *) emalloc(Maxbody * sizeof(char));",
	"	  }",
	"	  for (i = 0; i < MAXQ+1; i++)",
	"	  {	channels[i] = (TRIX_v6 *) emalloc(sizeof(TRIX_v6));",
	"		channels[i]->body = (uchar *) emalloc(Maxbody * sizeof(char));",
	"	} }",
	"#endif",
	"	iniglobals(258); /* arg outside range of pids */",
	"#if defined(VERI) && !defined(NOREDUCE) && !defined(NP)",
	"	if (!state_tables",
	"#ifdef HAS_CODE",
	"	&& !readtrail",
	"#endif",
	"#if NCORE>1",
	"	&& core_id == 0",
	"#endif",
	"	)",
	"	{ printf(\"warning: for p.o. reduction to be valid \");",
	"	  printf(\"the never claim must be stutter-invariant\\n\");",
	"	  printf(\"(never claims generated from LTL \");",
	"	  printf(\"formulae are stutter-invariant)\\n\");",
	"	}",
	"#endif",
	"	UnBlock;	/* disable rendez-vous */",
	"#ifdef BITSTATE",
	"	if (udmem)",
	"	{	udmem *= 1024L*1024L;",
	"	#if NCORE>1",
	"		if (!readtrail)",
	"		{	void init_SS(unsigned long);",
	"			init_SS((unsigned long) udmem);",
	"		} else",
	"	#endif",
	"		SS = (uchar *) emalloc(udmem);",
	"		bstore = bstore_mod;",
	"	} else",
	"	#if NCORE>1",
	"		{ void init_SS(unsigned long);",
	"		  init_SS(ONE_L<<(ssize-3));",
	"		}",
	"	#else",
	"		SS = (uchar *) emalloc(ONE_L<<(ssize-3));",
	"	#endif",
	"#else",	/* if not BITSTATE */
	"	hinit();",
	"#endif",
	"#if defined(FULLSTACK) && defined(BITSTATE)",
	"	onstack_init();",
	"#endif",
	"#if defined(CNTRSTACK) && !defined(BFS)",
	"	LL = (uchar *) emalloc(ONE_L<<(ssize-3));",
	"#endif",
	"	stack	= (_Stack *) emalloc(sizeof(_Stack));",
	"	svtack	= (Svtack *) emalloc(sizeof(Svtack));",
	"	/* a place to point for Pptr of non-running procs: */",
	"	noqptr = noptr	= (uchar *) emalloc(Maxbody * sizeof(char));",
	"#if defined(SVDUMP) && defined(VERBOSE)",
	"	if (vprefix > 0)",
	"		(void) write(svfd, (uchar *) &vprefix, sizeof(int));",
	"#endif",
	"#ifdef VERI",
	"	Addproc(VERI);	/* pid = 0 */",
	"	#if NCLAIMS>1",
	"	if (claimname != NULL)",
	"	{	whichclaim = find_claim(claimname);",
	"		select_claim(whichclaim);",
	"	}",
	"	#endif",
	"#endif",
	"	active_procs();	/* started after never */",
	"#ifdef EVENT_TRACE",
	"	now._event = start_event;",
	"	reached[EVENT_TRACE][start_event] = 1;",
	"#endif",

	"#ifdef HAS_CODE",
	"	globinit();",
	"#endif",
	"#ifdef BITSTATE",
	"go_again:",
	"#endif",
	"	do_the_search();",
	"#ifdef BITSTATE",
	"	if (--Nrun > 0 && HASH_CONST[++HASH_NR])",
	"	{	printf(\"Run %%d:\\n\", HASH_NR);",
	"		wrap_stats();",
	"		printf(\"\\n\");",

	"		if (udmem)	/* Dillinger 3/2/09 */",
	"		{	memset(SS, 0, udmem);",
	"		} else",
	"		{	memset(SS, 0, ONE_L<<(ssize-3));",
	"		}",

		"#ifdef CNTRSTACK",
	"		memset(LL, 0, ONE_L<<(ssize-3));",
		"#endif",
		"#ifdef FULLSTACK",
	"		memset((uchar *) S_Tab, 0, ",
	"		maxdepth*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",
	"}",
	"#ifdef HAS_PROVIDED",
	"int provided(int, uchar, int, Trans *);",
	"#endif",

	"#if NCORE>1",
	"#define GLOBAL_LOCK	(0)",
	"#ifndef CS_N",
	"#define CS_N		(256*NCORE)", /* must be a power of 2 */
	"#endif",

	"#ifdef NGQ",	/* no global queue */
	"#define NR_QS		(NCORE)",
	"#define CS_NR		(CS_N+1)	/* 2^N + 1, nr critical sections */",
	"#define GQ_RD		GLOBAL_LOCK",	/* not really used in this mode */
	"#define GQ_WR		GLOBAL_LOCK",	/* but just in case... */
	"#define CS_ID		(1 + (int) (j1_spin & (CS_N-1))) /* mask: 2^N - 1, zero reserved */",
	"#define QLOCK(n)	(1+n)", /* overlaps first n zones of hashtable */
	"#else",
	"#define NR_QS		(NCORE+1)",	/* add a global queue */
	"#define CS_NR		(CS_N+3)",	/* 2 extra locks for global q */
	"#define GQ_RD		(1)",		/* read access to global q */
	"#define GQ_WR		(2)",		/* write access to global q */
	"#define CS_ID		(3 + (int) (j1_spin & (CS_N-1)))",
	"#define QLOCK(n)	(3+n)",/* overlaps first n zones of hashtable */
	"#endif",
	"",
	"void e_critical(int);",
	"void x_critical(int);",
	"",
	"#ifndef SEP_STATE",
	"	#define enter_critical(w)	e_critical(w)",
	"	#define leave_critical(w)	x_critical(w)",
	"#else",
	"	#ifdef NGQ",
	"	#define enter_critical(w)	{ if (w < 1+NCORE) e_critical(w); }",
	"	#define leave_critical(w)	{ if (w < 1+NCORE) x_critical(w); }",
	"	#else",
	"	#define enter_critical(w)	{ if (w < 3+NCORE) e_critical(w); }",
	"	#define leave_critical(w)	{ if (w < 3+NCORE) x_critical(w); }",
	"	#endif",
	"#endif",
	"",
	"int",
	"cpu_printf(const char *fmt, ...)", /* only used with VERBOSE/CHECK/DEBUG */
	"{	va_list args;",
	"	enter_critical(GLOBAL_LOCK);	/* printing */",
	"	printf(\"cpu%%d: \", core_id);",
	"	fflush(stdout);",
	"	va_start(args, fmt);",
	"	vprintf(fmt, args);",
	"	va_end(args);",
	"	fflush(stdout);",
	"	leave_critical(GLOBAL_LOCK);",
	"	return 1;",
	"}",
	"#else",
	"int",
	"cpu_printf(const char *fmt, ...)",
	"{	va_list args;",
	"	va_start(args, fmt);",
	"	vprintf(fmt, args);",
	"	va_end(args);",
	"	return 1;",
	"}",
	"#endif",

#ifndef PRINTF
	"int",
	"Printf(const char *fmt, ...)",
	"{	/* Make sure the args to Printf",
	"	 * are always evaluated (e.g., they",
	"	 * could contain a run stmnt)",
	"	 * but do not 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 HAS_CODE",
	"	if (readtrail)",
	"	{	va_list args;",
	"		va_start(args, fmt);",
	"		vprintf(fmt, args);",
	"		va_end(args);",
	"		return 1;",
	"	}",
	"#endif",
	"#ifdef PRINTF",
	"	va_list args;",
	"	va_start(args, fmt);",
	"	vprintf(fmt, args);",
	"	va_end(args);",
	"#endif",
	"	return 1;",
	"}",
#endif
	"extern void printm(int);",

	"#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* (off_t) 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",

	"#if NCORE>1",
	"extern void cleanup_shm(int);",
	"volatile unsigned int	*search_terminated; /* to signal early termination */",
	/*
	 *	Meaning of bitflags in search_terminated:
	 *	  1	set by pan_exit
	 *	  2	set by wrapup
	 *	  4	set by uerror
	 *	  8	set by sudden_stop -- called after someone_crashed and [Uu]error
	 *	 16	set by cleanup_shm
	 *	 32	set by give_up	-- called on signal
	 *	 64	set by proxy_exit
	 *	128	set by proxy on write port failure
	 *	256	set by proxy on someone_crashed
	 *
	 *	Flags 8|32|128|256 indicate abnormal termination
	 *
	 *	The flags are checked in 4 functions in the code:
	 *		sudden_stop()
	 *		someone_crashed() (proxy and pan version)
	 *		mem_hand_off()
	 */
	"#endif",
	"void",
	"pan_exit(int val)",
	"{	void stop_timer(void);",
	"	if (signoff)",
	"	{	printf(\"--end of output--\\n\");",
	"	}",
	"#if NCORE>1",
	"	if (search_terminated != NULL)",
	"	{	*search_terminated |= 1;	/* pan_exit */",
	"	}",
		"#ifdef USE_DISK",
	"	{ void	dsk_stats(void);",
	"		dsk_stats();",
	"	}",
		"#endif",
	"	if (!state_tables && !readtrail)",
	"	{	cleanup_shm(1);",
	"	}",
	"#endif",
	"	if (val == 2)",
	"	{	val = 0;",
	"	} else",
	"	{	stop_timer();",
	"	}",
	"",
	"#ifdef C_EXIT",
	"	C_EXIT; /* trust that it defines a fct */",
	"#endif",
	"	exit(val);",
	"}",

	"#ifdef HAS_CODE",
	"static char tbuf[2][2048];",
	"",
	"char *",
	"transmognify(char *s)",
	"{	char *v, *w;",
	"	int i, toggle = 0;",
	"	if (!s || strlen(s) > 2047) return s;",
	"	memset(tbuf[0], 0, 2048);",
	"	memset(tbuf[1], 0, 2048);",
	"	strcpy(tbuf[toggle], s);",
	"	while ((v = strstr(tbuf[toggle], \"{c_code\")))",	/* assign v */
	"	{	*v = '\\0'; v++;",
	"		strcpy(tbuf[1-toggle], tbuf[toggle]);",
	"		for (w = v; *w != '}' && *w != '\\0'; w++) /* skip */;",
	"		if (*w != '}') return s;",
	"		*w = '\\0'; w++;",
	"		for (i = 0; code_lookup[i].c; i++)",
	"			if (strcmp(v, code_lookup[i].c) == 0",
	"			&&  strlen(v) == strlen(code_lookup[i].c))",
	"			{	if (strlen(tbuf[1-toggle])",
	"				 +  strlen(code_lookup[i].t)",
	"				 +  strlen(w) > 2047)",
	"					return s;",
	"				strcat(tbuf[1-toggle], code_lookup[i].t);",
	"				break;",
	"			}",
	"		strcat(tbuf[1-toggle], w);",
	"		toggle = 1 - toggle;",
	"	}",
	"	tbuf[toggle][2047] = '\\0';",
	"	return tbuf[toggle];",
	"}",
	"#else",
	"char * transmognify(char *s) { return s; }",
	"#endif",

	"#ifdef HAS_CODE",
	"void",
	"add_src_txt(int ot, int tt)",
	"{	Trans *t;",
	"	char *q;",
	"",
	"	for (t = trans[ot][tt]; t; t = t->nxt)",
	"	{	printf(\"\\t\\t\");",
	"		q = transmognify(t->tp);",
	"		for ( ; q && *q; q++)",
	"			if (*q == '\\n')",
	"				printf(\"\\\\n\");",
	"			else",
	"				putchar(*q);",
	"		printf(\"\\n\");",
	"	}",
	"}",
	"",
	"char *",
	"find_source(int tp, int s)",
	"{",
	"	if (s >= flref[tp]->from",
	"	&&  s <= flref[tp]->upto)",
	"	{	return flref[tp]->fnm;",
	"	}",
	"	return PanSource; /* i.e., don't know */",
	"}",
	"",
	"void",
	"wrap_trail(void)",
	"{	static int wrap_in_progress = 0;",
	"	int i; short II;",
	"	P0 *z;",
	"",
	"	if (wrap_in_progress++) return;",
	"",
	"	printf(\"spin: trail ends after %%ld steps\\n\", depth);",
	"	if (onlyproc >= 0)",
	"	{	if (onlyproc >= now._nr_pr) { pan_exit(0); }",
	"		II = onlyproc;",
	"		z = (P0 *)pptr(II);",
	"		printf(\"%%3ld:\tproc %%d (%%s) \",",
	"			depth, II, procname[z->_t]);",
	"		for (i = 0; src_all[i].src; i++)",
	"			if (src_all[i].tp == (int) z->_t)",
	"			{	printf(\" %%s:%%d\",",
	"					find_source((int) z->_t, (int) z->_p),",
	"					src_all[i].src[z->_p]);",
	"				break;",
	"			}",
	"		printf(\" (state %%2d)\", z->_p);",
	"		if (!stopstate[z->_t][z->_p])",
	"			printf(\" (invalid end state)\");",
	"		printf(\"\\n\");",
	"		add_src_txt(z->_t, z->_p);",
	"		pan_exit(0);",
	"	}",
	"	printf(\"#processes %%d:\\n\", now._nr_pr);",
	"	if (depth < 0) depth = 0;",
	"	for (II = 0; II < now._nr_pr; II++)",
	"	{	z = (P0 *)pptr(II);",
	"		printf(\"%%3ld:\tproc %%d (%%s) \",",
	"			depth, II, procname[z->_t]);",
	"		for (i = 0; src_all[i].src; i++)",
	"			if (src_all[i].tp == (int) z->_t)",
	"			{	printf(\" %%s:%%d\",",
	"					find_source((int) z->_t, (int) z->_p),",
	"					src_all[i].src[z->_p]);",
	"				break;",
	"			}",
	"		printf(\" (state %%2d)\", z->_p);",
	"		if (!stopstate[z->_t][z->_p])",
	"			printf(\" (invalid end state)\");",
	"		printf(\"\\n\");",
	"		add_src_txt(z->_t, z->_p);",
	"	}",
	"	c_globals();",
	"	for (II = 0; II < now._nr_pr; II++)",
	"	{	z = (P0 *)pptr(II);",
	"		c_locals(II, z->_t);",
	"	}",
	"#ifdef ON_EXIT",
	"	ON_EXIT;",
	"#endif",
	"	pan_exit(0);",
	"}",
	"FILE *",
	"findtrail(void)",
	"{	FILE *fd;",
	"	char fnm[512], *q;",
	"	char MyFile[512];",	/* avoid using a non-writable string */
	"	char MySuffix[16];",
	"	int  try_core;",
	"	int  candidate_files;",
	"",
	"	if (trailfilename != NULL)",
	"	{	fd = fopen(trailfilename, \"r\");",
	"		if (fd == NULL)",
	"		{	printf(\"pan: cannot find %%s\\n\", trailfilename);",
	"			pan_exit(1);",
	"		} /* else */",
	"		goto success;",
	"	}",
	"talk:",
	"	try_core = 1;",
	"	candidate_files = 0;",
	"	tprefix = \"trail\";",
	"	strcpy(MyFile, TrailFile);",
	"	do { /* see if there's more than one possible trailfile */",
	"		if (whichtrail)",
	"		{	sprintf(fnm, \"%%s%%d.%%s\",",
	"				MyFile, whichtrail, tprefix);",
	"			fd = fopen(fnm, \"r\");",
	"			if (fd != NULL)",
	"			{	candidate_files++;",
	"				if (verbose==100)",
	"					printf(\"trail%%d: %%s\\n\",",
	"						candidate_files, fnm);",
	"				fclose(fd);",
	"			}",
	"			if ((q = strchr(MyFile, \'.\')) != NULL)",
	"			{	*q = \'\\0\';",	/* e.g., strip .pml */
	"				sprintf(fnm, \"%%s%%d.%%s\",",
	"					MyFile, whichtrail, tprefix);",
	"				*q = \'.\';",
	"				fd = fopen(fnm, \"r\");",
	"				if (fd != NULL)",
	"				{	candidate_files++;",
	"					if (verbose==100)",
	"						printf(\"trail%%d: %%s\\n\",",
	"							candidate_files, fnm);",
	"					fclose(fd);",
	"			}	}",
	"		} else",
	"		{	sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
	"			fd = fopen(fnm, \"r\");",
	"			if (fd != NULL)",
	"			{	candidate_files++;",
	"				if (verbose==100)",
	"					printf(\"trail%%d: %%s\\n\",",
	"						candidate_files, fnm);",
	"				fclose(fd);",
	"			}",
	"			if ((q = strchr(MyFile, \'.\')) != NULL)",
	"			{	*q = \'\\0\';",	/* e.g., strip .pml */
	"				sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
	"				*q = \'.\';",
	"				fd = fopen(fnm, \"r\");",
	"				if (fd != NULL)",
	"				{	candidate_files++;",
	"					if (verbose==100)",
	"						printf(\"trail%%d: %%s\\n\",",
	"							candidate_files, fnm);",
	"					fclose(fd);",
	"		}	}	}",
	"		tprefix = MySuffix;",
	"		sprintf(tprefix, \"cpu%%d_trail\", try_core++);",
	"	} while (try_core <= NCORE);",
	"",
	"	if (candidate_files != 1)",
	"	{	if (verbose != 100)",
	"		{	printf(\"error: there are %%d trail files:\\n\",",
	"				candidate_files);",
	"			verbose = 100;",
	"			goto talk;",
	"		} else",
	"		{	printf(\"pan: rm or mv all except one\\n\");",
	"			exit(1);",
	"	}	}",

	"	try_core = 1;",
	"	strcpy(MyFile, TrailFile); /* restore */",
	"	tprefix = \"trail\";",
	"try_again:",
	"	if (whichtrail)",
	"	{	sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);",
	"		fd = fopen(fnm, \"r\");",
	"		if (fd == NULL && (q = strchr(MyFile, \'.\')))",
	"		{	*q = \'\\0\';",	/* e.g., strip .pml on original file */
	"			sprintf(fnm, \"%%s%%d.%%s\",",
	"				MyFile, whichtrail, tprefix);",
	"			*q = \'.\';",
	"			fd = fopen(fnm, \"r\");",
	"		}",
	"	} else",
	"	{	sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
	"		fd = fopen(fnm, \"r\");",
	"		if (fd == NULL && (q = strchr(MyFile, \'.\')))",
	"		{	*q = \'\\0\';",	/* e.g., strip .pml on original file */
	"			sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
	"			*q = \'.\';",
	"			fd = fopen(fnm, \"r\");",
	"	}	}",
	"	if (fd == NULL)",
	"	{	if (try_core < NCORE)",
	"		{	tprefix = MySuffix;",
	"			sprintf(tprefix, \"cpu%%d_trail\", try_core++);",
	"			goto try_again;",
	"		}",
	"		printf(\"pan: cannot find trailfile %%s\\n\", fnm);",
	"		pan_exit(1);",
	"	}",
	"success:",
	"#if NCORE>1 && defined(SEP_STATE)",
	"	{	void set_root(void); /* for partial traces from local root */",
	"		set_root();",
	"	}",
	"#endif",
	"	return fd;",
	"}",
	"",
	"uchar do_transit(Trans *, short);",
	"",
	"void",
	"getrail(void)",
	"{	FILE *fd;",
	"	char *q;",
	"	int i, t_id, lastnever=-1; short II;",
	"	Trans *t;",
	"	P0 *z;",
	"",
	"	fd = findtrail();	/* exits if unsuccessful */",
	"	while (fscanf(fd, \"%%ld:%%d:%%d\\n\", &depth, &i, &t_id) == 3)",
	"	{	if (depth == -1)",
	"			printf(\"<<<<<START OF CYCLE>>>>>\\n\");",
	"		if (depth < 0)",
	"			continue;",
	"		if (i > now._nr_pr)",
	"		{	printf(\"pan: Error, proc %%d invalid pid \", i);",
	"			printf(\"transition %%d\\n\", t_id);",
	"			break;",
	"		}",
	"		II = i;",
	"		z = (P0 *)pptr(II);",
	"		for (t = trans[z->_t][z->_p]; t; t = t->nxt)",
	"			if (t->t_id == (T_ID) t_id)",
	"				break;",
	"		if (!t)",
	"		{	for (i = 0; i < NrStates[z->_t]; i++)",
	"			{	t = trans[z->_t][i];",
	"				if (t && t->t_id == (T_ID) t_id)",
	"				{	printf(\"\\tRecovered at state %%d\\n\", i);",
	"					z->_p = i;",
	"					goto recovered;",
	"			}	}",
	"			printf(\"pan: Error, proc %%d type %%d state %%d: \",",
	"				II, z->_t, z->_p);",
	"			printf(\"transition %%d not found\\n\", t_id);",
	"			printf(\"pan: list of possible transitions in this process:\\n\");",
	"			if (z->_t >= 0 && z->_t <= _NP_)",
	"			for (t = trans[z->_t][z->_p]; t; t = t->nxt)",
	"				printf(\"	t_id %%d -- case %%d, [%%s]\\n\",",
	"					t->t_id, t->forw, t->tp);",
	"			break; /* pan_exit(1); */",
	"		}",
	"recovered:",
	"		q = transmognify(t->tp);",
	"		if (gui) simvals[0] = \'\\0\';",

	"		this = pptr(II);",
	"		trpt->tau |= 1;",	/* timeout always possible */
	"		if (!do_transit(t, II))",
	"		{	if (onlyproc >= 0 && II != onlyproc)",
	"				goto moveon;",
	"			printf(\"pan: error, next transition UNEXECUTABLE on replay\\n\");",
	"			printf(\"     most likely causes: missing c_track statements\\n\");",
	"			printf(\"       or illegal side-effects in c_expr statements\\n\");",
	"		}",

	"		if (onlyproc >= 0 && II != onlyproc)",
	"			goto moveon;",

	"		if (verbose)",
	"		{	printf(\"%%3ld: proc %%2d (%%s) \", depth, II, procname[z->_t]);",

	"			for (i = 0; src_all[i].src; i++)",
	"				if (src_all[i].tp == (int) z->_t)",
	"				{	printf(\" %%s:%%d \",",
	"						find_source((int) z->_t, (int) z->_p),",
	"						src_all[i].src[z->_p]);",
	"					break;",
	"				}",

	"			printf(\"(state %%d) trans {%%d,%%d} [%%s]\\n\",",
	"				z->_p, t_id, t->forw, q?q:\"\");",

	"			c_globals();",
	"			for (i = 0; i < now._nr_pr; i++)",
	"			{	c_locals(i, ((P0 *)pptr(i))->_t);",
	"			}",
	"		} else if (Btypes[z->_t] == N_CLAIM)",
	"		{	if (lastnever != (int) z->_p)",
	"			{	for (i = 0; src_all[i].src; i++)",
	"					if (src_all[i].tp == (int) z->_t)",
	"					{	printf(\"MSC: ~G %%d\\n\",",
	"							src_all[i].src[z->_p]);",
	"						break;",
	"					}",
	"				if (!src_all[i].src)",
	"					printf(\"MSC: ~R %%d\\n\", z->_p);",
	"			}",
	"			lastnever = z->_p;",
	"			goto sameas;",
	"		} else if (Btypes[z->_t] != 0) /* not :np_: */",
	"		{",
	"sameas:		if (no_rck) goto moveon;",
	"			if (coltrace)",
	"			{	printf(\"%%ld: \", depth);",
	"				for (i = 0; i < II; i++)",
	"					printf(\"\\t\\t\");",
	"				printf(\"%%s(%%d):\", procname[z->_t], II);",
	"				printf(\"[%%s]\\n\", q?q:\"\");",
	"			} else if (!silent)",
	"			{	if (strlen(simvals) > 0) {",
	"				printf(\"%%3ld:	proc %%2d (%%s)\", ",
	"					depth, II, procname[z->_t]);",
	"				for (i = 0; src_all[i].src; i++)",
	"					if (src_all[i].tp == (int) z->_t)",
	"					{	printf(\" %%s:%%d \",",
	"							find_source((int) z->_t, (int) z->_p),",
	"							src_all[i].src[z->_p]);",
	"						break;",
	"					}",
	"				printf(\"(state %%d)\t[values: %%s]\\n\", z->_p, simvals);",
	"				}",
	"				printf(\"%%3ld:	proc %%2d (%%s)\", ",
	"					depth, II, procname[z->_t]);",
	"				for (i = 0; src_all[i].src; i++)",
	"					if (src_all[i].tp == (int) z->_t)",
	"					{	printf(\" %%s:%%d \",",
	"							find_source((int) z->_t, (int) z->_p),",
	"							src_all[i].src[z->_p]);",
	"						break;",
	"					}",
	"				printf(\"(state %%d)\t[%%s]\\n\", z->_p, q?q:\"\");",
	"			/*	printf(\"\\n\");	*/",
	"		}	}",
	"moveon:	z->_p = t->st;",
	"	}",
	"	wrap_trail();",
	"}",
	"#endif",
	"int",
	"f_pid(int pt)",
	"{	int i;",
	"	P0 *z;",
	"	for (i = 0; i < now._nr_pr; i++)",
	"	{	z = (P0 *)pptr(i);",
	"		if (z->_t == (unsigned) pt)",
	"			return BASE+z->_pid;",
	"	}",
	"	return -1;",
	"}",
	"",
	"#if !defined(HASH64) && !defined(HASH32)",
	"	#if WS>4",
	"		#define HASH64",
	"	#else",
	"		#define HASH32",
	"	#endif",
	"#endif",
	"#if defined(HASH32) && defined(SAFETY) && !defined(SFH) && !defined(SPACE)",
	"	#define SFH",
	"#endif",
	"#if defined(SFH) && (defined(BITSTATE) || defined(COLLAPSE) || defined(HC) || defined(HASH64) || defined(MA))",
	"	#undef SFH",	/* need 2 hash fcts, for which Jenkins is best */
	"#endif",		/* or a 64 bit hash, which we dont have for SFH */
	/* for MA, it would slow down the search to use a larger sv then possible */
	"#if defined(SFH) && !defined(NOCOMP)",
	"	#define NOCOMP	/* go for speed */",
	"#endif",
	"#if NCORE>1 && !defined(GLOB_HEAP)",
	"	#define SEP_HEAP /* version 5.1.2 */",
	"#endif",
	"",
	"#ifdef BITSTATE",
	"int",
	"bstore_mod(char *v, int n)	/* hasharray size not a power of two */",
	"{	unsigned long x, y;",
	"	unsigned int i = 1;",
	"",
	"	d_hash((uchar *) v, n); /* sets j3, j4, K1, K2 */",
	"	x = K1; y = j3;",	/* was K2 before 5.1.1 */
	"	for (;;)",
	"	{	if (!(SS[x%%umem]&(1<<y))) break;",	/* take the hit in speed */
	"		if (i == hfns) {",
				"#ifdef DEBUG",
	"			printf(\"Old bitstate\\n\");",
				"#endif",
	"			return 1;",
	"		}",
	"		x = (x + K2 + i);",	/* no mask, using mod - was K1 before 5.1.1 */
	"		y = (y + j4) & 7;",
	"		i++;",
	"	}",
		"#ifdef RANDSTOR",
	"	if (rand()%%100 > RANDSTOR) return 0;",
		"#endif",
	"	for (;;)",
	"	{	SS[x%%umem] |= (1<<y);",
	"		if (i == hfns) break;",	/* done */
	"		x = (x + K2 + i);",	/* no mask - was K1 before 5.1.1 */
	"		y = (y + j4) & 7;",
	"		i++;",
	"	}",
		"#ifdef DEBUG",
	"	printf(\"New bitstate\\n\");",
		"#endif",
	"	if (now._a_t&1)",
	"	{	nShadow++;",
	"	}",
	"	return 0;",
	"}",
	"int",
	"bstore_reg(char *v, int n)	/* extended hashing, Peter Dillinger, 2004 */",
	"{	unsigned long x, y;",
	"	unsigned int i = 1;",
	"",
	"	d_hash((uchar *) v, n); /* sets j1-j4 */",
	"	x = j2; y = j3;",
	"	for (;;)",
	"	{	if (!(SS[x]&(1<<y))) break;",	/* at least one bit not set */
	"		if (i == hfns) {",
				"#ifdef DEBUG",
	"			printf(\"Old bitstate\\n\");",
				"#endif",
	"			return 1;",
	"		}",
	"		x = (x + j1_spin + i) & nmask;",
	"		y = (y + j4) & 7;",
	"		i++;",
	"	}",
		"#ifdef RANDSTOR",
	"	if (rand()%%100 > RANDSTOR) return 0;",
		"#endif",
	"	for (;;)",
	"	{	SS[x] |= (1<<y);",
	"		if (i == hfns) break;",		/* done */
	"		x = (x + j1_spin + i) & nmask;",
	"		y = (y + j4) & 7;",
	"		i++;",
	"	}",
		"#ifdef DEBUG",
	"	printf(\"New bitstate\\n\");",
		"#endif",
	"	if (now._a_t&1)",
	"	{	nShadow++;",
	"	}",
	"	return 0;",
	"}",
	"#endif", /* BITSTATE */
	"unsigned long TMODE = 0666; /* file permission bits for trail files */",
	"",
	"int trcnt=1;",
	"char snap[64], fnm[512];",
	"",
	"int",
	"make_trail(void)",
	"{	int fd;",
	"	char *q;",
	"	char MyFile[512];",
	"	int w_flags = O_CREAT|O_WRONLY|O_TRUNC;",
	"",
	"	if (exclusive == 1 && iterative == 0)",
	"	{	w_flags |= O_EXCL;",
	"	}",
	"",
	"	q = strrchr(TrailFile, \'/\');",
	"	if (q == NULL) q = TrailFile; else q++;",
	"	strcpy(MyFile, q); /* TrailFile is not a writable string */",
	"",
	"	if (iterative == 0 && Nr_Trails++ > 0)",
	"	{	sprintf(fnm, \"%%s%%d.%%s\",",
	"			MyFile, Nr_Trails-1, tprefix);",
	"	} else",
	"	{",
	"#ifdef PUTPID",
	"		sprintf(fnm, \"%%s_%%s_%%d.%%s\", MyFile, progname, getpid(), tprefix);",
	"#else",
	"		sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
	"#endif",
	"	}",
	"	if ((fd = open(fnm, w_flags, TMODE)) < 0)",
	"	{	if ((q = strchr(MyFile, \'.\')))",
	"		{	*q = \'\\0\';",		/* strip .pml */
	"			if (iterative == 0 && Nr_Trails-1 > 0)",
	"				sprintf(fnm, \"%%s%%d.%%s\",",
	"					MyFile, Nr_Trails-1, tprefix);",
	"			else",
	"				sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
	"			*q = \'.\';",
	"			fd = open(fnm, w_flags, TMODE);",
	"	}	}",
	"	if (fd < 0)",
	"	{	printf(\"pan: cannot create %%s\\n\", fnm);",
	"		perror(\"cause\");",
	"	} else",
	"	{",
	"#if NCORE>1 && (defined(SEP_STATE) || !defined(FULL_TRAIL))",
	"	void write_root(void); ",
	"	write_root();",
	"#else",
	"		printf(\"pan: wrote %%s\\n\", fnm);",
	"#endif",
	"	}",
	"	return fd;",
	"}",
	"",
	"#ifndef FREQ",
	"#define FREQ	(1000000)",
	"#endif",
	"double freq = (double) FREQ;\n",

	"#ifdef TRIX",
	"void sv_populate(void);",
	"",
	"void",
	"re_populate(void) /* restore procs and chans from now._ids_ */",
	"{	int i, cnt = 0;",
	"	char *b;",
	"#ifdef V_TRIX",
	"	printf(\"%%4d: re_populate\\n\", depth);",
	"#endif",
	"	for (i = 0; i < now._nr_pr; i++, cnt++)",
	"	{	b = now._ids_[cnt];",
	"		processes[i]->psize = what_p_size( ((P0 *)b)->_t );",
	"		memcpy(processes[i]->body, b, processes[i]->psize);",
	"#ifdef TRIX_RIX",
	"		((P0 *)pptr(i))->_pid = i;",
	"#endif",
	"#ifndef BFS",
	"		processes[i]->modified = 1; /* re-populate */",
	"#endif",
	"	}",
	"	for (i = 0; i < now._nr_qs; i++, cnt++)",
	"	{	b = now._ids_[cnt];",
	"		channels[i]->psize = what_q_size( ((Q0 *)b)->_t );",
	"		memcpy(channels[i]->body, b, channels[i]->psize);",
	"#ifndef BFS",
	"		channels[i]->modified = 1; /* re-populate */",
	"#endif",
	"	}",
	"}",
	"#endif\n",

	"#ifdef BFS",	/* breadth-first search */
	"#define Q_PROVISO",
	"	#ifndef INLINE_REV",
	"		#define INLINE_REV",
	"	#endif",
	"",
	"typedef struct SV_Hold {",
	"	State *sv;",
	"	int  sz;",
	"	struct SV_Hold *nxt;",
	"} SV_Hold;",
	"",
	"typedef struct EV_Hold {",
	"	char *sv;",	/* Mask */
	"	int  sz;",	/* vsize */
	"	int nrpr;",
	"	int nrqs;",
	"#ifndef TRIX",
	"	char *po, *qo;",
	"	char *ps, *qs;",
	"#endif",
	"	struct EV_Hold *nxt;",
	"} EV_Hold;",
	"",
	"typedef struct BFS_Trail {",
	"	Trail	*frame;",
	"	SV_Hold *onow;",
	"	EV_Hold *omask;",
	"#ifdef Q_PROVISO",
	"	struct H_el *lstate;",
	"#endif",
	"	short boq;",
	"#ifdef VERBOSE",
	"	unsigned long nr;",
	"#endif",
	"	struct BFS_Trail *nxt;",
	"} BFS_Trail;",
	"",
	"BFS_Trail *bfs_trail, *bfs_bot, *bfs_free;",
	"",
	"SV_Hold *svhold, *svfree;",
	"",
	"#ifdef BFS_DISK",
	"	#ifndef BFS_LIMIT",
	"	#define BFS_LIMIT	100000",
	"	#endif",
	"	#ifndef BFS_DSK_LIMIT",
	"	#define BFS_DSK_LIMIT	1000000",
	"	#endif",
	"	#if defined(WIN32) || defined(WIN64)",
	"	#define RFLAGS	(O_RDONLY|O_BINARY)",
	"	#define WFLAGS	(O_CREAT|O_WRONLY|O_TRUNC|O_BINARY)",
	"	#else",
	"	#define RFLAGS	(O_RDONLY)",
	"	#define WFLAGS	(O_CREAT|O_WRONLY|O_TRUNC)",
	"	#endif",

	"long bfs_size_limit;",
	"int bfs_dsk_write = -1;",
	"int bfs_dsk_read = -1;",
	"long bfs_dsk_writes, bfs_dsk_reads;",
	"int bfs_dsk_seqno_w, bfs_dsk_seqno_r;",
	"#endif",
	"",
	"uchar do_reverse(Trans *, short, uchar);",
	"void snapshot(void);",
	"",
	"void",
	"select_claim(int x)	/* ignored in BFS mode */",
	"{	if (verbose)",
	"	{	printf(\"select %%d (ignored)\\n\", x);",
	"	}",
	"}",
	"",
	"SV_Hold *",
	"getsv(int n)",
	"{	SV_Hold *h = (SV_Hold *) 0, *oh;",
	"",
	"	oh = (SV_Hold *) 0;",
	"	for (h = svfree; h; oh = h, h = h->nxt)",
	"	{	if (n == h->sz)",
	"		{	if (!oh)",
	"				svfree = h->nxt;",
	"			else",
	"				oh->nxt = h->nxt;",
	"			h->nxt = (SV_Hold *) 0;",
	"			break;",
	"		}",
	"		if (n < h->sz)",
	"		{	h = (SV_Hold *) 0;",
	"			break;",
	"		}",
	"		/* else continue */",
	"	}",
	"",
	"	if (!h)",
	"	{	h = (SV_Hold *) emalloc(sizeof(SV_Hold));",
	"		h->sz = n;",
	"#ifdef BFS_DISK",
	"		if (bfs_size_limit >= BFS_LIMIT)",
	"		{	h->sv = (State *) 0;	/* means: read disk */",
	"			bfs_dsk_writes++;	/* count */",
	"			if (bfs_dsk_write < 0	/* file descriptor */",
	"			||  bfs_dsk_writes%%BFS_DSK_LIMIT == 0)",
	"			{	char dsk_nm[32];",
	"				if (bfs_dsk_write >= 0)",
	"				{	(void) close(bfs_dsk_write);",
	"				}",
	"				sprintf(dsk_nm, \"pan_bfs_%%d.tmp\", bfs_dsk_seqno_w++);",
	"				bfs_dsk_write = open(dsk_nm, WFLAGS, 0644);",
	"				if (bfs_dsk_write < 0)",
	"				{	Uerror(\"could not create tmp disk file\");",
	"				}",
	"				printf(\"pan: created disk file %%s\\n\", dsk_nm);",
	"			}",
	"			if (write(bfs_dsk_write, (char *) &now, n) != n)",
	"			{	Uerror(\"aborting -- disk write failed (disk full?)\");",
	"			}",
	"			return h; /* no memcpy */",
	"		}", /* else */
	"		bfs_size_limit++;",
	"#endif",
	"		h->sv = (State *) emalloc(sizeof(State) - VECTORSZ + n);",
	"	}",
	"",
	"	memcpy((char *)h->sv, (char *)&now, n);",
	"	return h;",
	"}",
	"",
	"EV_Hold *",
	"getsv_mask(int n)",
	"{	EV_Hold *h;",
	"	static EV_Hold *kept = (EV_Hold *) 0;",
	"",
	"	for (h = kept; h; h = h->nxt)",
	"		if (n == h->sz",
	"		&&  (memcmp((char *) Mask, (char *) h->sv, n) == 0)",
	"		&&  (now._nr_pr == h->nrpr)",
	"		&&  (now._nr_qs == h->nrqs)",
	"#ifdef TRIX",
	"		)",
	"#else",
	"	#if VECTORSZ>32000",
	"		&&  (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(int)) == 0)",
	"		&&  (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(int)) == 0)",
	"	#else",
	"		&&  (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(short)) == 0)",
	"		&&  (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(short)) == 0)",
	"	#endif",
	"		&&  (memcmp((char *) proc_skip, (char *) h->ps, now._nr_pr * sizeof(uchar)) == 0)",
	"		&&  (memcmp((char *) q_skip,    (char *) h->qs, now._nr_qs * sizeof(uchar)) == 0))",
	"#endif",
	"			break;",
	"	if (!h)",
	"	{	h = (EV_Hold *) emalloc(sizeof(EV_Hold));",
	"		h->sz = n;",
	"		h->nrpr = now._nr_pr;",
	"		h->nrqs = now._nr_qs;",
	"",
	"		h->sv = (char *) emalloc(n * sizeof(char));",
	"		memcpy((char *) h->sv, (char *) Mask, n);",
	"#ifndef TRIX",
	"		if (now._nr_pr > 0)",
	"		{	h->ps = (char *) emalloc(now._nr_pr * sizeof(int));",
	"			memcpy((char *) h->ps, (char *) proc_skip,   now._nr_pr * sizeof(uchar));",
	"	#if VECTORSZ>32000",
	"			h->po = (char *) emalloc(now._nr_pr * sizeof(int));",
	"			memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(int));",
	"	#else",
	"			h->po = (char *) emalloc(now._nr_pr * sizeof(short));",
	"			memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(short));",
	"	#endif",
	"		}",
	"		if (now._nr_qs > 0)",
	"		{	h->qs = (char *) emalloc(now._nr_qs * sizeof(int));",
	"			memcpy((char *) h->qs, (char *) q_skip,   now._nr_qs * sizeof(uchar));",
	"	#if VECTORSZ>32000",
	"			h->qo = (char *) emalloc(now._nr_qs * sizeof(int));",
	"			memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(int));",
	"	#else",
	"			h->qo = (char *) emalloc(now._nr_qs * sizeof(short));",
	"			memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(short));",
	"	#endif",
	"		}",
	"#endif",
	"		h->nxt = kept;",
	"		kept = h;",
	"	}",
	"	return h;",
	"}",
	"",
	"void",
	"freesv(SV_Hold *p)",
	"{	SV_Hold *h, *oh;",
	"",
	"	oh = (SV_Hold *) 0;",
	"	for (h = svfree; h; oh = h, h = h->nxt)",
	"	{	if (h->sz >= p->sz)",
	"			break;",
	"	}",
	"	if (!oh)",
	"	{	p->nxt = svfree;",
	"		svfree = p;",
	"	} else",
	"	{	p->nxt = h;",
	"		oh->nxt = p;",
	"	}",
	"}",
	"",
	"BFS_Trail *",
	"get_bfs_frame(void)",
	"{	BFS_Trail *t;",
	"",
	"	if (bfs_free)",
	"	{	t = bfs_free;",
	"		bfs_free = bfs_free->nxt;",
	"		t->nxt = (BFS_Trail *) 0;",
	"	} else",
	"	{	t = (BFS_Trail *) emalloc(sizeof(BFS_Trail));",
	"	}",
	"	t->frame = (Trail *) emalloc(sizeof(Trail));", /* always new */
	"	/* new because we keep a ptr to the frame of parent states */",
	"	/* used for reconstructing path and recovering failed rvs etc */",
	"	return t;",
	"}",
	"",
	"void",
	"push_bfs(Trail *f, int d)",
	"{	BFS_Trail *t;",
	"",
	"	t = get_bfs_frame();",
	"	memcpy((char *)t->frame, (char *)f, sizeof(Trail));",
	"	t->frame->o_tt = d;	/* depth */",
	"",
	"	t->boq = boq;",
	"#ifdef TRIX",
	"	sv_populate();",
	"#endif",
	"	t->onow = getsv(vsize);",
	"	t->omask = getsv_mask(vsize);",
	"#if defined(FULLSTACK) && defined(Q_PROVISO)",
	"	t->lstate = Lstate;",
	"#endif",
	"	if (!bfs_bot)",
	"	{	bfs_bot = bfs_trail = t;",
	"	} else",
	"	{	bfs_bot->nxt = t;",
	"		bfs_bot = t;",
	"	}",
	"#ifdef VERBOSE",
	"	t->nr = nstates;",
	"#endif",
	"#ifdef CHECK",
	"	printf(\"PUSH %%u (depth %%d, nr %%d)\\n\", t->frame, d, t->nr);",
	"#endif",
	"}",
	"",
	"Trail *",
	"pop_bfs(void)",
	"{	BFS_Trail *t;",
	"",
	"	if (!bfs_trail)",
	"	{	return (Trail *) 0;",
	"	}",
	"	t = bfs_trail;",
	"	bfs_trail = t->nxt;",
	"	if (!bfs_trail)",
	"	{	bfs_bot = (BFS_Trail *) 0;",
	"	}",
	"#if defined(Q_PROVISO) && !defined(BITSTATE) && !defined(NOREDUCE)",
	"	if (t->lstate)",
	"	{	t->lstate->tagged = 0;",
	"	}",
	"#endif",
	"	t->nxt = bfs_free;",
	"	bfs_free = t;",
	"",
	"	vsize = t->onow->sz;",
	"	boq = t->boq;",
	"#ifdef BFS_DISK",
	"	if (t->onow->sv == (State *) 0)",
	"	{	char dsk_nm[32];",
	"		bfs_dsk_reads++;	/* count */",
	"		if (bfs_dsk_read >= 0	/* file descriptor */",
	"		&&  bfs_dsk_reads%%BFS_DSK_LIMIT == 0)",
	"		{	(void) close(bfs_dsk_read);",
	"			sprintf(dsk_nm, \"pan_bfs_%%d.tmp\", bfs_dsk_seqno_r-1);",
	"			(void) unlink(dsk_nm);",
	"			bfs_dsk_read = -1;",
	"		}",
	"		if (bfs_dsk_read < 0)",
	"		{	sprintf(dsk_nm, \"pan_bfs_%%d.tmp\", bfs_dsk_seqno_r++);",
	"			bfs_dsk_read = open(dsk_nm, RFLAGS);",
	"			if (bfs_dsk_read < 0)",
	"			{	Uerror(\"could not open temp disk file\");",
	"		}	}",
	"		if (read(bfs_dsk_read, (char *) &now, vsize) != vsize)",
	"		{	Uerror(\"bad bfs disk file read\");",
	"		}",
	"	#ifndef NOVSZ",
	"		if (now._vsz != vsize)",
	"		{	Uerror(\"disk read vsz mismatch\");",
	"		}",
	"	#endif",
	"	} else",
	"#endif",
	"	{	memcpy((uchar *) &now, (uchar *) t->onow->sv, vsize);",
	"	}",
	"	memcpy((uchar *) Mask, (uchar *) t->omask->sv, vsize);",
	"#ifdef TRIX",
	"	re_populate();",
	"#else",
	"	if (now._nr_pr > 0)",
	"	#if VECTORSZ>32000",
	"	{	memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(int));",
	"	#else",
	"	{	memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(short));",
	"	#endif",
	"		memcpy((char *)proc_skip,   (char *)t->omask->ps, now._nr_pr * sizeof(uchar));",
	"	}",
	"	if (now._nr_qs > 0)",
	"	#if VECTORSZ>32000",
	"	{	memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(int));",
	"	#else",
	"	{	memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(short));",
	"	#endif",
	"		memcpy((uchar *)q_skip,   (uchar *)t->omask->qs, now._nr_qs * sizeof(uchar));",
	"	}",
	"#endif",
	"#ifdef BFS_DISK",
	"	if (t->onow->sv != (State *) 0)",
	"#endif",
	"	{	freesv(t->onow);	/* omask not freed */",
	"	}",
	"#ifdef CHECK",
	"	printf(\"POP %%u (depth %%d, nr %%d)\\n\", t->frame, t->frame->o_tt, t->nr);",
	"#endif",
	"	return t->frame;",
	"}",
	"",
	"void",
	"store_state(Trail *ntrpt, int shortcut, short oboq)",
	"{",
	"#ifdef VERI",
	"	Trans *t2 = (Trans *) 0;",
	"	uchar ot; int tt, E_state;",
	"	uchar o_opm = trpt->o_pm, *othis = this;",
	"",
	"	if (shortcut)",
	"	{",
	"	#ifdef VERBOSE",
	"		printf(\"claim: shortcut\\n\");",
	"	#endif",
	"		goto store_it;	/* no claim move */",
	"	}",
	"",
	"	this  = pptr(0);	/* 0 = never claim */",
	"	trpt->o_pm = 0;",	/* to interpret else in never claim */
	"",
	"	tt    = (int)   ((P0 *)this)->_p;",
	"	ot    = (uchar) ((P0 *)this)->_t;",
	"",
	"	#ifdef HAS_UNLESS",
	"	E_state = 0;",
	"	#endif",
	"	for (t2 = trans[ot][tt]; t2; t2 = t2?t2->nxt:(Trans *)0)",
	"	{",
	"	#ifdef HAS_UNLESS",
	"		if (E_state > 0 && E_state != t2->e_trans)",
	"		{	break;",
	"		}",
	"	#endif",
	"		if (do_transit(t2, 0))",
	"		{",
	"	#ifdef VERBOSE",
	"			if (!reached[ot][t2->st])",
	"			printf(\"depth: %%d -- claim move from %%d -> %%d\\n\",",
	"				trpt->o_tt, ((P0 *)this)->_p, t2->st);",
	"	#endif",
	"	#ifdef HAS_UNLESS",
	"			E_state = t2->e_trans;",
	"	#endif",
	"			if (t2->st > 0)",
	"			{	((P0 *)this)->_p = t2->st;",
	"				reached[ot][t2->st] = 1;",
	"	#ifndef NOCLAIM",
	"				if (stopstate[ot][t2->st])",
	"				{	uerror(\"end state in claim reached\");",
	"				}",
	"	#endif",
	"			}",
	"			if (now._nr_pr == 0)	/* claim terminated */",
	"				uerror(\"end state in claim reached\");",
	"",
	"	#ifdef PEG",
	"			peg[t2->forw]++;",
	"	#endif",
	"			trpt->o_pm |= 1;",
	"			if (t2->atom&2)",
	"			{ Uerror(\"atomic in claim not supported in BFS\");",
	"			}",
	"store_it:",
	"",
	"#endif",	/* VERI */
	"",
	"#if defined(BITSTATE)",
	"			if (!bstore((char *)&now, vsize))",
	"#elif defined(MA)",
	"			if (!gstore((char *)&now, vsize, 0))",
	"#else",
	"			if (!hstore((char *)&now, vsize))",
	"#endif",
	"			{	static long sdone = (long) 0; long ndone;",
	"				nstates++;",
	"#ifndef NOREDUCE",
	"				trpt->tau |= 64;", /* bfs: succ definitely outside stack */
	"#endif",
	"				ndone = (unsigned long) (nstates/(freq));",
	"				if (ndone != sdone && mreached%%10 != 0)",
	"				{	snapshot();",
	"					sdone = ndone;",
	"#if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)",
	"					if (nstates > ((double)(1<<(ssize+1))))",
	"					{	void resize_hashtable(void);",
	"						resize_hashtable();",
	"					}",
	"#endif",
	"				}",
	"#if SYNC",
	"				if (boq != -1)",
	"					midrv++;",
	"				else if (oboq != -1)",
	"				{	Trail *x;",
	"					x = (Trail *) trpt->ostate; /* pre-rv state */",
	"					if (x) x->o_pm |= 4; /* mark success */",
	"				}",
	"#endif",
	"				push_bfs(ntrpt, trpt->o_tt+1);",
	"			} else",
	"			{	truncs++;",

	"#if !defined(NOREDUCE) && defined(FULLSTACK) && defined(Q_PROVISO)",
	"	#if !defined(BITSTATE)",
	"				if (Lstate && Lstate->tagged)",
	"				{  trpt->tau |= 64;",
	"				}",
	"	#else",
	"				if (trpt->tau&32)",
	"				{  BFS_Trail *tprov;",
	"				   for (tprov = bfs_trail; tprov; tprov = tprov->nxt)",
	"					if (tprov->onow->sv != (State *) 0",
	"					&&  memcmp((uchar *)&now, (uchar *)tprov->onow->sv, vsize) == 0)",
	"					{	trpt->tau |= 64;",
	"						break;	/* state is in queue */",
	"				}	}",
	"	#endif",
	"#endif",
	"			}",
	"#ifdef VERI",
	"			((P0 *)this)->_p = tt;	/* reset claim */",
	"			if (t2)",
	"				do_reverse(t2, 0, 0);",
	"			else",
	"				break;",
	"	}	}",
	"	this = othis;",
	"	trpt->o_pm = o_opm;",
	"#endif",
	"}",
	"",
	"Trail *ntrpt;",	/* 4.2.8 */
	"",
	"void",
	"bfs(void)",
	"{	Trans *t; Trail *otrpt, *x;",
	"	uchar _n, _m, ot, nps = 0;",
	"	int tt, E_state;",
	"	short II, From = (short) (now._nr_pr-1), To = BASE;",
	"	short oboq = boq;",
	"",
	"	ntrpt = (Trail *) emalloc(sizeof(Trail));",
	"	trpt->ostate = (struct H_el *) 0;",
	"	trpt->tau = 0;",
	"",
	"	trpt->o_tt = -1;",
	"	store_state(ntrpt, 0, oboq);	/* initial state */",
	"",
	"	while ((otrpt = pop_bfs()))	/* also restores now */",
	"	{	memcpy((char *) trpt, (char *) otrpt, sizeof(Trail));",
	"#if defined(C_States) && (HAS_TRACK==1)",
	"		c_revert((uchar *) &(now.c_state[0]));",
	"#endif",
	"		if (trpt->o_pm & 4)",
	"		{",
	"#ifdef VERBOSE",
	"			printf(\"Revisit of atomic not needed (%%d)\\n\",",
	"				trpt->o_pm);",	/* at least 1 rv succeeded */
	"#endif",
	"			continue;",
	"		}",
	"#ifndef NOREDUCE",
	"		nps = 0;",
	"#endif",
	"		if (trpt->o_pm == 8)",
	"		{	revrv++;",
	"			if (trpt->tau&8)",
	"			{",
	"#ifdef VERBOSE",
	"				printf(\"Break atomic (pm:%%d,tau:%%d)\\n\",",
	"					trpt->o_pm, trpt->tau);",
	"#endif",
	"				trpt->tau &= ~8;",
	"			}",
	"#ifndef NOREDUCE",
	"			else if (trpt->tau&32)",	/* was a preselected move */
	"			{",
	"	#ifdef VERBOSE",
	"				printf(\"Void preselection (pm:%%d,tau:%%d)\\n\",",
	"					trpt->o_pm, trpt->tau);",
	"	#endif",
	"				trpt->tau &= ~32;",
	"				nps = 1; /* no preselection in repeat */",
	"			}",
	"#endif",
	"		}",
	"		trpt->o_pm &= ~(4|8);",
	"		if (trpt->o_tt > mreached)",
	"		{	mreached = trpt->o_tt;",
	"			if (mreached%%10 == 0)",
	"			{	snapshot();",
	"		}	}",
	"		depth = trpt->o_tt;",

	"		if (depth >= maxdepth)",
	"		{",
	"#if SYNC",
	"			Trail *x;",
	"			if (boq != -1)",
	"			{	x = (Trail *) trpt->ostate;",
	"				if (x) x->o_pm |= 4; /* not failing */",
	"			}",
	"#endif",
	"			truncs++;",
	"			if (!warned)",
	"			{	warned = 1;",
	"		  		printf(\"error: max search depth too small\\n\");",
	"			}",
	"			if (bounded)",
	"			{	uerror(\"depth limit reached\");",
	"			}",
	"			continue;",
	"		}",
	"#ifndef NOREDUCE",
	"		if (boq == -1 && !(trpt->tau&8) && nps == 0)",
	"		for (II = now._nr_pr-1; II >= BASE; II -= 1)",
	"		{",
	"Pickup:		this = pptr(II);",
	"			tt = (int) ((P0 *)this)->_p;",
	"			ot = (uchar) ((P0 *)this)->_t;",
	"			if (trans[ot][tt]->atom & 8)",	/* safe */
	"			{	t = trans[ot][tt];",
	"				if (t->qu[0] != 0)",
	"				{	Ccheck++;",
	"					if (!q_cond(II, t))",
	"						continue;",
	"					Cholds++;",
	"				}",
	"				From = To = II;",
	"				trpt->tau |= 32; /* preselect marker */",
	"	#ifdef DEBUG",
	"				printf(\"%%3ld: proc %%d PreSelected (tau=%%d)\\n\", ",
	"					depth, II, trpt->tau);",
	"	#endif",
	"				goto MainLoop;",
	"		}	}",
	"		trpt->tau &= ~32;",	/* not preselected */
	"#endif",	/* if !NOREDUCE */
	"Repeat:",
	"		if (trpt->tau&8)		/* atomic */",
	"		{	From = To = (short ) trpt->pr;",
	"			nlinks++;",
	"		} else",
	"		{	From = now._nr_pr-1;",
	"			To = BASE;",
	"		}",
	"MainLoop:",
	"		_n = _m = 0;",
	"		for (II = From; II >= To; II -= 1)",
	"		{",
	"			this = pptr(II);",
	"			tt = (int) ((P0 *)this)->_p;",
	"			ot = (uchar) ((P0 *)this)->_t;",
	"#if SYNC",
	"			/* no rendezvous with same proc */",
	"			if (boq != -1 && trpt->pr == II)",
	"			{	continue;",
	"			}",
	"#endif",
	"			ntrpt->pr = (uchar) II;",
	"			ntrpt->st = tt;	",
	"			trpt->o_pm &= ~1; /* no move yet */",
	"#ifdef EVENT_TRACE",
	"			trpt->o_event = now._event;",
	"#endif",
	"#ifdef HAS_PROVIDED",
	"			if (!provided(II, ot, tt, t))",
	"			{	continue;",
	"			}",
	"#endif",
	"#ifdef HAS_UNLESS",
	"			E_state = 0;",
	"#endif",
	"			for (t = trans[ot][tt]; t; t = t->nxt)",
	"			{",
	"#ifdef HAS_UNLESS",
	"				if (E_state > 0",
	"				&&  E_state != t->e_trans)",
	"					break;",
	"#endif",
	"				ntrpt->o_t = t;",
	"",
	"				oboq = boq;",
	"",
	"				if (!(_m = do_transit(t, II)))",
	"					continue;",
	"",
	"				trpt->o_pm |= 1;	/* we moved */",
	"				(trpt+1)->o_m = _m;	/* for unsend */",
	"#ifdef PEG",
	"				peg[t->forw]++;",
	"#endif",
	"#ifdef CHECK",
	"				printf(\"%%3ld: 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",
	"#ifdef HAS_UNLESS",
	"				E_state = t->e_trans;",
	"	#if SYNC>0",
	"				if (t->e_trans > 0 && (boq != -1 /* || oboq != -1 */))",
	"				{ fprintf(efd, \"error:\ta rendezvous stmnt in the escape clause\\n\");",
	"				  fprintf(efd, \"\tof an unless stmnt is not compatible with -DBFS\\n\");",
	"				  pan_exit(1);",
	"				}",
	"	#endif",
	"#endif",
	"				if (t->st > 0)",
	"				{	((P0 *)this)->_p = t->st;",
	"				}",
	"",
	"	/* ptr to pred: */	ntrpt->ostate = (struct H_el *) otrpt;",
	"				ntrpt->st = tt;",
	"				if (boq == -1 && (t->atom&2))	/* atomic */",
	"					ntrpt->tau = 8;	/* record for next move */",
	"				else",
	"					ntrpt->tau = 0;",
	"				store_state(ntrpt, (boq != -1 || (t->atom&2)), oboq);",
	"#ifdef EVENT_TRACE",
	"				now._event = trpt->o_event;",
	"#endif",
	"				/* undo move and continue */",
	"				trpt++;	/* this is where ovals and ipt are set */",
	"				do_reverse(t, II, _m);	/* restore now. */",
	"				trpt--;",
	"#ifdef CHECK",
	"	#if NCORE>1",
	"				enter_critical(GLOBAL_LOCK);	/* verbose mode */",
	"				printf(\"cpu%%d: \", core_id);",
	"	#endif",
	"				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);",
	"	#if NCORE>1",
	"				leave_critical(GLOBAL_LOCK);",
	"	#endif",
	"#endif",
	"				reached[ot][t->st] = 1;",
	"				reached[ot][tt]    = 1;",
	"",
	"				((P0 *)this)->_p = tt;",
	"				_n |= _m;",
	"		}	}",
	"#ifndef NOREDUCE",	/* with PO */
	"		/* preselected - no succ definitely outside stack */",
	"		if ((trpt->tau&32) && !(trpt->tau&64))",
	"		{	From = now._nr_pr-1; To = BASE;",
	"	#ifdef DEBUG",
	"			cpu_printf(\"%%3ld: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
	"				depth, II+1, (int) _n, trpt->tau);",
	"	#endif",
	"			_n = 0; trpt->tau &= ~32;",
	"			if (II >= BASE)",
	"			{	goto Pickup;",
	"			}",
	"			goto MainLoop;",
	"		}",
	"		trpt->tau &= ~(32|64);",
	"#endif",	/* PO */
	"		if (_n != 0)",
	"		{	continue;",
	"		}",
	"#ifdef DEBUG",
	"		printf(\"%%3ld: no move [II=%%d, tau=%%d, boq=%%d, _nr_pr=%%d]\\n\",",
	"			depth, II, trpt->tau, boq, now._nr_pr);",
	"#endif",
	"		if (boq != -1)",
	"		{	failedrv++;",
	"			x = (Trail *) trpt->ostate;	/* pre-rv state */",
	"			if (!x)",
	"			{	continue;		/* root state */",
	"			}",
	"			if ((x->tau&8) || (x->tau&32)) /* break atomic or preselect at parent */",
	"			{	x->o_pm |= 8; /* mark failure */",
	"				this = pptr(otrpt->pr);",
	"#ifdef VERBOSE",
	"				printf(\"\\treset state of %%d from %%d to %%d\\n\",",
	"					otrpt->pr, ((P0 *)this)->_p, otrpt->st);",
	"#endif",
	"				((P0 *)this)->_p = otrpt->st;",
	"				unsend(boq);	/* retract rv offer */",
	"				boq = -1;",

	"				push_bfs(x, x->o_tt);",
	"#ifdef VERBOSE",
	"				printf(\"failed rv, repush with %%d\\n\", x->o_pm);",
	"#endif",
	"			}",
	"#ifdef VERBOSE",
	"			else",
	"			{	printf(\"failed rv, tau at parent: %%d\\n\", x->tau);",
	"			}",
	"#endif",
	"		} else if (now._nr_pr > 0)",
	"		{",
	"			if ((trpt->tau&8))		/* atomic */",
	"			{	trpt->tau &= ~(1|8);	/* 1=timeout, 8=atomic */",
	"#ifdef DEBUG",
	"				printf(\"%%3ld: atomic step proc %%d blocks\\n\",",
	"					depth, II+1);",
	"#endif",
	"				goto Repeat;",
	"			}",
	"",
	"			if (!(trpt->tau&1)) /* didn't try timeout yet */",
	"			{	trpt->tau |=  1;",
	"#ifdef DEBUG",
	"				printf(\"%%d: timeout\\n\", depth);",
	"#endif",
	"				goto MainLoop;",
	"			}",
	"#ifndef VERI",
	"			if (!noends && !a_cycles && !endstate())",
	"			{	uerror(\"invalid end state\");",
	"			}",
	"#endif",
	"	}	}",
	"}",
	"",
	"void",
	"putter(Trail *trpt, int fd)",
	"{	long j;",
	"",
	"	if (!trpt) return;",
	"",
	"	if (trpt != (Trail *) trpt->ostate)",
	"		putter((Trail *) trpt->ostate, fd);",
	"",
	"	if (trpt->o_t)",
	"	{	sprintf(snap, \"%%d:%%d:%%d\\n\",",
	"			trcnt++, trpt->pr, trpt->o_t->t_id);",
	"		j = strlen(snap);",
	"		if (write(fd, snap, j) != j)",
	"		{       printf(\"pan: error writing %%s\\n\", fnm);",
	"			pan_exit(1);",
	"	}	}",
	"}",
	"",
	"void",
	"nuerror(char *str)",
	"{	int fd = make_trail();",
	"	int j;",
	"",
	"	if (fd < 0) return;",
	"#ifdef VERI",
	"	sprintf(snap, \"-2:%%d:-2\\n\", (uchar) ((P0 *)pptr(0))->_t);",
	"	(void) write(fd, snap, strlen(snap));",
	"#endif",
	"#ifdef MERGED",
	"	sprintf(snap, \"-4:-4:-4\\n\");",
	"	(void) write(fd, snap, strlen(snap));",
	"#endif",
	"	trcnt = 1;",
	"	putter(trpt, fd);",
	"	if (ntrpt->o_t)",	/* 4.2.8 -- Alex example, missing last transition */
	"	{	sprintf(snap, \"%%d:%%d:%%d\\n\",",
	"			trcnt++, ntrpt->pr, ntrpt->o_t->t_id);",
	"		j = strlen(snap);",
	"		if (write(fd, snap, j) != j)",
	"		{       printf(\"pan: error writing %%s\\n\", fnm);",
	"			pan_exit(1);",
	"	}	}",
	"	close(fd);",
	"	if (errors >= upto && upto != 0)",
	"	{	wrapup();",
	"	}",
	"}",
	"#endif",	/* BFS */
	0,
};

static char *Code2d[] = {
	"clock_t start_time;",
	"#if NCORE>1",
	"clock_t crash_stamp;",
	"#endif",
	"#if !defined(WIN32) && !defined(WIN64)",
	"struct tms start_tm;",
	"#endif",
	"",
	"void",
	"start_timer(void)",
	"{",
	"#if defined(WIN32) || defined(WIN64)",
	"	start_time = clock();",
	"#else",
	"	start_time = times(&start_tm);",
	"#endif",
	"}",
	"",
	"void",
	"stop_timer(void)",
	"{	clock_t stop_time;",
	"	double delta_time;",
	"#if !defined(WIN32) && !defined(WIN64)",
	"	struct tms stop_tm;",
	"	stop_time = times(&stop_tm);",
	"	delta_time = ((double) (stop_time - start_time)) / ((double) sysconf(_SC_CLK_TCK));",
	"#else",
	"	stop_time = clock();",
	"	delta_time = ((double) (stop_time - start_time)) / ((double) CLOCKS_PER_SEC);",
	"#endif",
	"	if (readtrail || delta_time < 0.00) return;",
	"#if NCORE>1",
	"	if (core_id == 0 && nstates > (double) 0)",
	"	{	printf(\"\\ncpu%%d: elapsed time %%.3g seconds (%%g states visited)\\n\",",
	"			core_id, delta_time, nstates);",
	"		if (delta_time > 0.01)",
	"		{	printf(\"cpu%%d: rate %%g states/second\\n\", core_id, nstates/delta_time);",
	"		}",
	"		{ void check_overkill(void);",
	"	 	  check_overkill();",
	"	}	}",
	"#else",
	"	printf(\"\\npan: elapsed time %%.3g seconds\\n\", delta_time);",
	"	if (delta_time > 0.01)",
	"	{	printf(\"pan: rate %%9.8g states/second\\n\", nstates/delta_time);",
	"		if (verbose)",
	"		{	printf(\"pan: avg transition delay %%.5g usec\\n\",",
	"				delta_time/(nstates+truncs));",
	"	}	}",
	"#endif",
	"}",
	"",
	"#if NCORE>1",
	"#ifdef T_ALERT",
	"double t_alerts[17];",
	"",
	"void",
	"crash_report(void)",
	"{	int i;",
	"	printf(\"crash alert intervals:\\n\");",
	"	for (i = 0; i < 17; i++)",
	"	{	printf(\"%%d\\t%%g\\n\", i, t_alerts[i]);",
	"}	}",
	"#endif",
	"",
	"void",
	"crash_reset(void)",
	"{	/* false alarm */",
	"	if (crash_stamp != (clock_t) 0)",
	"	{",
	"#ifdef T_ALERT",
	"		double delta_time;",
	"		int i;",
		"#if defined(WIN32) || defined(WIN64)",
	"		delta_time = ((double) (clock() - crash_stamp)) / ((double) CLOCKS_PER_SEC);",
		"#else",
	"		delta_time = ((double) (times(&start_tm) - crash_stamp)) / ((double) sysconf(_SC_CLK_TCK));",
		"#endif",
	"		for (i = 0; i < 16; i++)",
	"		{	if (delta_time <= (i*30))",
	"			{	t_alerts[i] = delta_time;",
	"				break;",
	"		}	}",
	"		if (i == 16) t_alerts[i] = delta_time;",
	"#endif",
	"		if (verbose)",
	"		printf(\"cpu%%d: crash alert off\\n\", core_id);",
	"	}",
	"	crash_stamp = (clock_t) 0;",
	"}",
	"",
	"int",
	"crash_test(double maxtime)",
	"{	double delta_time;",
	"	if (crash_stamp == (clock_t) 0)",
	"	{	/* start timing */",
	"#if defined(WIN32) || defined(WIN64)",
	"		crash_stamp = clock();",
	"#else",
	"		crash_stamp = times(&start_tm);",
	"#endif",
	"		if (verbose)",
	"		{	printf(\"cpu%%d: crash detection\\n\", core_id);",
	"		}",
	"		return 0;",
	"	}",
	"#if defined(WIN32) || defined(WIN64)",
	"	delta_time = ((double) (clock() - crash_stamp)) / ((double) CLOCKS_PER_SEC);",
	"#else",
	"	delta_time = ((double) (times(&start_tm) - crash_stamp)) / ((double) sysconf(_SC_CLK_TCK));",
	"#endif",
	"	return (delta_time >= maxtime);",
	"}",
	"#endif",
	"",
	"void",
	"do_the_search(void)",
	"{	int i;",
	"	depth = mreached = 0;",
	"	trpt = &trail[0];",
	"#ifdef VERI",
	"	trpt->tau |= 4;	/* the claim moves first */",
	"#endif",
	"	for (i = 0; i < (int) now._nr_pr; i++)",
	"	{	P0 *ptr = (P0 *) pptr(i);",
	"#ifndef NP",
	"		if (!(trpt->o_pm&2)",
	"		&&  accpstate[ptr->_t][ptr->_p])",
	"		{	trpt->o_pm |= 2;",
	"		}",
	"#else",
	"		if (!(trpt->o_pm&4)",
	"		&&  progstate[ptr->_t][ptr->_p])",
	"		{	trpt->o_pm |= 4;",
	"		}",
	"#endif",
	"	}",
	"#ifdef EVENT_TRACE",
	"#ifndef NP",
	"	if (accpstate[EVENT_TRACE][now._event])",
	"	{	trpt->o_pm |= 2;",
	"	}",
	"#else",
	"	if (progstate[EVENT_TRACE][now._event])",
	"	{	trpt->o_pm |= 4;",
	"	}",
	"#endif",
	"#endif",
	"#ifndef NOCOMP",
	"	Mask[0] = Mask[1] = 1;	/* _nr_pr, _nr_qs */",
	"	if (!a_cycles)",
	"	{	i = &(now._a_t) - (uchar *) &now;",
	"		Mask[i] = 1; /* _a_t */",
	"	}",
	"#ifndef NOFAIR",
	"	if (!fairness)",
	"	{	int j = 0;",
	"		i = &(now._cnt[0]) - (uchar *) &now;",
	"		while (j++ < NFAIR)",
	"			Mask[i++] = 1; /* _cnt[] */",
	"	}",
	"#endif",
	"#endif",
	"#ifndef NOFAIR",
	"	if (fairness",
	"	&&  (a_cycles && (trpt->o_pm&2)))",
	"	{	now._a_t = 2;	/* set the A-bit */",
	"		now._cnt[0] = now._nr_pr + 1;",	/* NEW: +1 */
		"#ifdef VERBOSE",
	"	printf(\"%%3ld: fairness Rule 1, cnt=%%d, _a_t=%%d\\n\",",
	"		depth, now._cnt[now._a_t&1], now._a_t);",
		"#endif",
	"	}",
	"#endif",

	"	c_stack_start = (char *) &i; /* meant to be read-only */",

	"#if defined(HAS_CODE) && defined (C_INIT)",
	"	C_INIT; /* initialization of data that must precede fork() */",
	"	c_init_done++;",
	"#endif",

	"#if defined(C_States) && (HAS_TRACK==1)",
	"	/* capture initial state of tracked C objects */",
	"	c_update((uchar *) &(now.c_state[0]));",
	"#endif",

	"#ifdef HAS_CODE",
	"	if (readtrail) getrail(); /* no return */",
	"#endif",
	"	start_timer();",
	"#ifdef BFS",
	"	bfs();",
	"#else",
		"#if defined(C_States) && defined(HAS_STACK) && (HAS_TRACK==1)",
		"	/* initial state of tracked & unmatched objects */",
		"	c_stack((uchar *) &(svtack->c_stack[0]));",
		"#endif",

	"#if defined(P_RAND) || defined(T_RAND)",
	"	srand(s_rand);",
	"#endif",

	"#if NCORE>1",
	"	mem_get();",
	"#else",
	"	new_state();	/* start 1st DFS */",
	"#endif",
	"#endif",
	"}",

	"#ifdef INLINE_REV",
	"uchar",
	"do_reverse(Trans *t, short II, uchar M)",
	"{	uchar _m = M;",
	"	int  tt = (int) ((P0 *)this)->_p;",
	"#include REVERSE_MOVES",
	"R999:	return _m;",
	"}",
	"#endif",

	"#ifndef INLINE",
	"#ifdef EVENT_TRACE",
	"static char _tp = 'n'; static int _qid = 0;",
	"#endif",
	"uchar",
	"do_transit(Trans *t, short II)",
	"{	uchar _m = 0;",
	"	int  tt = (int) ((P0 *)this)->_p;",
	"#ifdef M_LOSS",
	"	uchar delta_m = 0;",
	"#endif",
	"#ifdef EVENT_TRACE",
	"	short oboq = boq;",
	"	uchar ot = (uchar)  ((P0 *)this)->_t;",
	"	if (II == -EVENT_TRACE) boq = -1;",
		"#define continue	{ boq = oboq; return 0; }",
	"#else",
		"#define continue	return 0",
		"#ifdef SEPARATE",
	"	uchar ot = (uchar)  ((P0 *)this)->_t;",
		"#endif",
	"#endif",
	"#include FORWARD_MOVES",
	"P999:",
	"#ifdef EVENT_TRACE",
	"	if (II == -EVENT_TRACE) boq = oboq;",
	"#endif",
	"	return _m;",
	"#undef continue",
	"}",
	"#ifdef EVENT_TRACE",
	"void",
	"require(char tp, int qid)",
	"{	Trans *t;",
	"	_tp = tp; _qid = qid;",
	"",
	"	if (now._event != endevent)",
	"	for (t = trans[EVENT_TRACE][now._event]; t; t = t->nxt)",
	"	{	if (do_transit(t, -EVENT_TRACE))",
	"		{	now._event = t->st;",
	"			reached[EVENT_TRACE][t->st] = 1;",
	"#ifdef VERBOSE",
	"	printf(\"	event_trace move to -> %%d\\n\", t->st);",
	"#endif",
	"#ifndef BFS",
		"#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",
	"#endif",
	"#ifdef NEGATED_TRACE",
	"			if (now._event == endevent)",
	"			{",
		"#ifndef BFS",
	"				depth++; trpt++;",
		"#endif",
	"				uerror(\"event_trace error (all events matched)\");",
		"#ifndef BFS",
	"				trpt--; depth--;",
		"#endif",
	"				break;",
	"			}",
	"#endif",
	"			for (t = t->nxt; t; t = t->nxt)",
	"			{	if (do_transit(t, -EVENT_TRACE))",
	"				 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 = endevent; /* only 1st try will count -- fixed 4.2.6 */",
	"#else",
		"#ifndef BFS",
	"	depth++; trpt++;",
		"#endif",
	"	uerror(\"event_trace error (no matching event)\");",
		"#ifndef BFS",
	"	trpt--; depth--;",
		"#endif",
	"#endif",
	"}",
	"#endif",
	"int",
	"enabled(int iam, int pid)",
	"{	Trans *t; uchar *othis = this;",
	"	int res = 0; int tt; uchar ot;",
	"#ifdef VERI",
	"	/* if (pid > 0) */ pid++;",
	"#endif",
	"	if (pid == iam)",
	"		Uerror(\"used: enabled(pid=thisproc)\");",
	"	if (pid < 0 || pid >= (int) now._nr_pr)",
	"		return 0;",
	"	this = pptr(pid);",
	"	TstOnly = 1;",
	"	tt = (int) ((P0 *)this)->_p;",
	"	ot = (uchar) ((P0 *)this)->_t;",
	"	for (t = trans[ot][tt]; t; t = t->nxt)",
	"		if (do_transit(t, (short) pid))",
	"		{	res = 1;",
	"			break;",
	"		}",
	"	TstOnly = 0;",
	"	this = othis;",
	"	return res;",
	"}",
	"#endif",
	"void",
	"snap_time(void)",
	"{	clock_t stop_time;",
	"	double delta_time;",
	"#if !defined(WIN32) && !defined(WIN64)",
	"	struct tms stop_tm;",
	"	stop_time  = times(&stop_tm);",
	"	delta_time = ((double) (stop_time - start_time)) / ((double) sysconf(_SC_CLK_TCK));",
	"#else",
	"	stop_time  = clock();",
	"	delta_time = ((double) (stop_time - start_time)) / ((double) CLOCKS_PER_SEC);",
	"#endif",
	"	if (delta_time > 0.01)",
	"	{	printf(\"t= %%8.3g \", delta_time);",
	"		printf(\"R= %%7.0g\", nstates/delta_time);",
	"	}",
	"	printf(\"\\n\");",
	"	if (quota > 0.1 && delta_time > quota)",
	"	{	printf(\"Time limit of %%6.3g minutes exceeded\\n\", quota/60.0);",
	"#if NCORE>1",
	"		fflush(stdout);",
	"		leave_critical(GLOBAL_LOCK);",
	"		sudden_stop(\"time-limit\");",
	"		exit(1);",
	"#endif",
	"		wrapup();",
	"	}",
	"}",
	"void",
	"snapshot(void)",
	"{",
	"#if NCORE>1",
	"	enter_critical(GLOBAL_LOCK);	/* snapshot */",
	"	printf(\"cpu%%d: \", core_id);",
	"#endif",
	"	printf(\"Depth= %%7ld States= %%8.3g \",",
	"#if NCORE>1",
	"		(long) (nr_handoffs * z_handoff) +",
	"#endif",
	"		mreached, nstates);",
	"	printf(\"Transitions= %%8.3g \", nstates+truncs);",
	"#ifdef MA",
	"	printf(\"Nodes= %%7d \", nr_states);",
	"#endif",
	"	printf(\"Memory= %%9.3f\\t\", memcnt/1048576.);",
	"	snap_time();",
	"	fflush(stdout);",
	"#if NCORE>1",
	"	leave_critical(GLOBAL_LOCK);",
	"#endif",
	"}",
	"#ifdef SC",
	"void",
	"stack2disk(void)",
	"{",
	"	if (!stackwrite",
	"	&&  (stackwrite = creat(stackfile, TMODE)) < 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* (off_t) 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* (off_t) sizeof(Trail), SEEK_SET) == -1)",
	"		Uerror(\"disk2stack lseek error\");",
	"",
	"	have = read(stackread, trail, DDD*sizeof(Trail));",
	"	if (have !=  DDD*sizeof(Trail))",
	"		Uerror(\"stackfile read error\");",
	"}",
	"#endif",

	"uchar *",
	"Pptr(int x)",
	"{	if (x < 0 || x >= MAXPROC",	/* does not exist */
	"#ifdef TRIX",
	"	|| !processes[x])",
	"#else",
	"	|| !proc_offset[x])",
	"#endif",
	"		return noptr;",
	"	else",
	"		return (uchar *) pptr(x);",
	"}\n",
	"uchar *",
	"Qptr(int x)",
	"{	if (x < 0 || x >= MAXQ",
	"#ifdef TRIX",
	"	|| !channels[x])",
	"#else",
	"	|| !q_offset[x])",
	"#endif",
	"		return noqptr;",
	"	else",
	"		return (uchar *) qptr(x);",
	"}\n",

	"int qs_empty(void);",
	"#if !defined(BFS) && (!defined(BITSTATE) || !defined(MA))",
	"#ifdef NSUCC",
	"int N_succ[512];",
	"void",
	"tally_succ(int cnt)",
	"{	if (cnt < 512) N_succ[cnt]++;",
	"	else printf(\"tally_succ: cnt %%d exceeds range\\n\", cnt);",
	"}",
	"",
	"void",
	"dump_succ(void)",
	"{	int i; double sum = 0.0;",
	"	double w_avg = 0.0;",
	"	printf(\"Successor counts:\\n\");",
	"	for (i = 0; i < 512; i++)",
	"	{	sum += (double) N_succ[i];",
	"	}",
	"	for (i = 0; i < 512; i++)",
	"	{	if (N_succ[i] > 0)",
	"		{	printf(\"%%3d\t%%10d\t(%%.4g %%%% of total)\\n\",",
	"				i, N_succ[i], (100.0 * (double) N_succ[i])/sum);",
	"			w_avg += (double) i * (double) N_succ[i];",
	"	}	}",
	"	if (sum > N_succ[0])",
	"	printf(\"mean %%.4g (without 0: %%.4g)\\n\", w_avg / sum, w_avg / (sum - (double) N_succ[0]));",
	"}",
	"#endif",
	"",
	"#if NCLAIMS>1",
	"void",
	"select_claim(int n)",
	"{	int m, i;",
	"	if (n < 0 || n >= NCLAIMS)",
	"	{	uerror(\"non-existing claim\");",
	"	} else",
	"	{	m = ((Pclaim *)pptr(0))->_n;",
	"		if (verbose)",
	"		{	printf(\"%%d: Claim %%s (%%d), from state %%d\\n\",",
	"				(int) depth, procname[spin_c_typ[n]],",
	"				n, ((Pclaim *)pptr(0))->c_cur[n]);",
	"		}",
	"		((Pclaim *)pptr(0))->c_cur[m] = ((Pclaim *)pptr(0))->_p;",
	"		((Pclaim *)pptr(0))->_t = spin_c_typ[n];",
	"		((Pclaim *)pptr(0))->_p = ((Pclaim *)pptr(0))->c_cur[n];",
	"		((Pclaim *)pptr(0))->_n = n;",
	"		for (i = 0; src_all[i].src != (short *) 0; i++)",
	"		{	if (src_all[i].tp == spin_c_typ[n])",
	"			{	src_claim = src_all[i].src;",
	"				break;",
	"		}	}",
	"		if (src_all[i].src == (short *) 0)",
	"		{	uerror(\"cannot happen: src_ln ref\");",
	"	}	}",
	"}",
	"#else",
	"void",
	"select_claim(int n)",
	"{	if (n != 0) uerror(\"non-existing claim\");",
	"}",
	"#endif",
	"",
	"#ifdef REVERSE",
	"	#define FROM_P	(BASE)",
	"	#define UPTO_P	(now._nr_pr-1)",
	"	#define MORE_P	(II <= To)",	/* p.o. only */
	"	#define INI_P	(From-1)",	/* fairness only */
	"	#define ALL_P	(II = From; II <= To; II++)",
	"#else",
	"	#define FROM_P	(now._nr_pr-1)",
	"	#define UPTO_P	(BASE)",
	"	#define MORE_P	(II >= BASE)",
	"	#define INI_P	(From+1)",
	"	#define ALL_P	(II = From; II >= To; II--)",
	"#endif",
	"/*",
	" * new_state() is the main DFS search routine in the verifier",
	" * it has a lot of code ifdef-ed together to support",
	" * different search modes, which makes it quite unreadable.",
	" * if you are studying the code, use the C preprocessor",
	" * to generate a specific version from the pan.c source,",
	" * e.g. by saying:",
	" *	gcc -E -DNOREDUCE -DBITSTATE pan.c > ppan.c",
	" * and then study the resulting file, instead of this version",
	" */",
	"",
	"void",
	"new_state(void)",
	"{	Trans *t;",
	"	uchar _n, _m, ot;",
	"#ifdef T_RAND",
	"	short ooi, eoi;",
	"#endif",

	"#ifdef M_LOSS",
	"	uchar delta_m = 0;",
	"#endif",
	"	short II, JJ = 0, kk;",
	"	int tt;",
	"	short From = FROM_P, To = UPTO_P;",
	"#ifdef BCS",
	"	trpt->sched_limit = 0; /* at depth=0 only */",
	"#endif",
	"Down:",
	"#ifdef CHECK",
	"	cpu_printf(\"%%d: Down - %%s %%saccepting [pids %%d-%%d]\\n\",",
	"		depth, (trpt->tau&4)?\"claim\":\"program\",",
	"		(trpt->o_pm&2)?\"\":\"non-\", From, To);",
	"#endif",

	"#ifdef P_RAND",
	"	trpt->p_skip = -1;",
	"#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",
	"#ifdef NSUCC",
	"	trpt->n_succ = 0;",
	"#endif",
	"#if NCORE>1",
	"	if (mem_hand_off())",
	"	{",
	"#if SYNC",
	"		(trpt+1)->o_n = 1;	/* not a deadlock: as below  */",
	"#endif",
	"#ifndef LOOPSTATE",
	"		(trpt-1)->tau |= 16;	/* worstcase guess: as below */",
	"#endif",
	"#if NCORE>1 && defined(FULL_TRAIL)",
	"		if (upto > 0)",
	"		{	Pop_Stack_Tree();",
	"		}",
	"#endif",
	"		goto Up;",
	"	}",
	"#endif",

	"	if (depth >= maxdepth)",
	"	{	if (!warned)",
	"		{ warned = 1;",
	"		  printf(\"error: max search depth too small\\n\");",
	"		}",
	"		if (bounded)",
	"		{	uerror(\"depth limit reached\");",
	"		}",
	"		truncs++;",
	"#if SYNC",
	"		(trpt+1)->o_n = 1; /* not a deadlock */",
	"#endif",
	"#ifndef LOOPSTATE",
	"		(trpt-1)->tau |= 16;	/* worstcase guess */",
	"#endif",

	"#if NCORE>1 && defined(FULL_TRAIL)",
	"		if (upto > 0)",
	"		{	Pop_Stack_Tree();",
	"		}",
	"#endif",
	"		goto Up;",
	"	}",
	"AllOver:",
	"#if (defined(FULLSTACK) && !defined(MA)) || NCORE>1",
	"	/* if atomic or rv move, carry forward previous state */",
	"	trpt->ostate = (trpt-1)->ostate;",
	"#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",
	"#if NCORE>1 && defined(FULL_TRAIL)",
	"			if (upto > 0)",
	"			{	Pop_Stack_Tree();",
	"			}",
	"#endif",
	"			  goto Up;",
	"			}",
		"#ifdef CHECK",
	"			printf(\"not seed\\n\");",
		"#endif",
	"		}",
	"#endif",
	"		if (!(trpt->tau&8)) /* if no atomic move */",
	"		{",
	"#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
	"			uchar was_last = now._last;",
	"			now._last = 0;	/* value not stored */",
	"#endif",
	"#ifdef BITSTATE",
		"#ifdef CNTRSTACK",	/* -> bitstate, reduced, safety */
	"		#if defined(BCS) && defined(STORE_CTX)",
	"		{ int xj;",
	"			for (xj = trpt->sched_limit; xj <= sched_max; xj++)",
	"			{	now._ctx = xj;",
	"				II = bstore((char *)&now, vsize);",
	"				trpt->j6 = j1_spin; trpt->j7 = j2;",
	"				JJ = LL[j1_spin] && LL[j2];",
	"				if (II != 0) { break; }",
	"			}",
	"			now._ctx = 0; /* just in case */",
	"		}",
	"		#else",
	"			II = bstore((char *)&now, vsize);",
	"			trpt->j6 = j1_spin; trpt->j7 = j2;",
	"			JJ = LL[j1_spin] && LL[j2];",
	"		#endif",
		"#else",
	"		#ifdef FULLSTACK", /* bstore after onstack_now, to preserve j1-j4 */
	"		   #if defined(BCS) && defined(STORE_CTX)",
	"		   { int xj;",
	"			now._ctx = 0;",
	"			JJ = onstack_now();",		    /* mangles j1 */
	"			for (xj = trpt->sched_limit; xj <= sched_max; xj++)",
	"			{	now._ctx = xj;",
	"				II = bstore((char *)&now, vsize);", /* sets j1-j4 */
	"				if (II != 0) { break; }",
	"			}",
	"			now._ctx = 0;",
	"		   }",
	"		   #else",
	"			JJ = onstack_now();",		    /* mangles j1 */
	"			II = bstore((char *)&now, vsize);", /* sets j1-j4 */
	"		   #endif",
	"		#else",
	"		   #if defined(BCS) && defined(STORE_CTX)",
	"		   { int xj;",
	"			for (xj = trpt->sched_limit; xj <= sched_max; xj++)",
	"			{	now._ctx = xj;",
	"				II = bstore((char *)&now, vsize);", /* sets j1-j4 */
	"				JJ = II; /* worstcase guess for p.o. - order corrected in 5.2.1 */",
	"				if (II != 0) { break; }",
	"			}",
	"			now._ctx = 0;",
	"		   }",
	"		   #else",
	"			II = bstore((char *)&now, vsize);", /* sets j1-j4 */
	"			JJ = II; /* worstcase guess for p.o. - order corrected in 5.2.1 */",
	"		   #endif",
	"		#endif",
		"#endif",
	"#else",
		"#ifdef MA",
	"			II = gstore((char *)&now, vsize, 0);",
			"#ifndef FULLSTACK",
	"			JJ = II;",
			"#else",
	"			JJ = (II == 2)?1:0;",
			"#endif",
		"#else",
	"			II = hstore((char *)&now, vsize);",
	"			/* @hash j1_spin II */",
			"#ifdef FULLSTACK",
	"			JJ = (II == 2)?1:0;",
			"#endif",
		"#endif",
	"#endif",
	"			kk = (II == 1 || II == 2);",
	/* actually, BCS implies HAS_LAST */
	"#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
	"			now._last = was_last;	/* restore value */",
	"#endif",

				/* II==0 new state */
				/* II==1 old state */
				/* II==2 on current dfs stack */
				/* II==3 on 1st dfs stack */
	"#ifndef SAFETY",

		"#if NCORE==1 || defined (SEP_STATE)",	/* or else we don't know which stack its on */
	"			if (II == 2 && ((trpt->o_pm&2) || ((trpt-1)->o_pm&2)))",
	"		#ifndef NOFAIR",
	"#if 0",
	"			if (!fairness || ((now._a_t&1) && now._cnt[1] == 1)) /* 5.1.4 */",
	"#else",
	"			if (a_cycles && !fairness) /* 5.1.6 -- example by Hirofumi Watanabe */",
	"#endif",
	"		#endif",
	"			{",
	"				II = 3; /* Schwoon & Esparza 2005, Gastin&Moro 2004 */",
			"#ifdef VERBOSE",
	"				printf(\"state match on dfs stack\\n\");",
			"#endif",
	"				goto same_case;",
	"			}",
		"#endif",

		"#if defined(FULLSTACK) && defined(BITSTATE)",
	"			if (!JJ && (now._a_t&1) && depth > A_depth)",
	"			{	int oj1 = j1_spin;",
	"				uchar o_a_t = now._a_t;",
	"				now._a_t &= ~(1|16|32);", /* 1st stack  */
	"				if (onstack_now())",	  /* changes j1_spin */
	"				{	II = 3;",
		"#ifdef VERBOSE",
	"					printf(\"state match on 1st dfs stack\\n\");",
		"#endif",
	"				}",
	"				now._a_t = o_a_t;",	/* restore */
	"				j1_spin = oj1;",
	"			}",
		"#endif",
	"			if (II == 3 && a_cycles && (now._a_t&1))",
	"			{",
		"#ifndef NOFAIR",
	"			   if (fairness && now._cnt[1] > 1)	/* was != 0 */",
	"			   {",
		"#ifdef VERBOSE",
	"				printf(\"\tfairness count non-zero\\n\");",
		"#endif",
	"				II = 0;", /* treat as new state */
	"			   } else",
		"#endif",
	"			   {",
		"#ifndef BITSTATE",
	"				nShadow--;",
		"#endif",
	"same_case:			if (Lstate) depthfound = Lstate->D;",
		"#ifdef NP",
	"				uerror(\"non-progress cycle\");",
		"#else",
	"				uerror(\"acceptance cycle\");",
		"#endif",
	"#if NCORE>1 && defined(FULL_TRAIL)",
	"				if (upto > 0)",
	"				{	Pop_Stack_Tree();",
	"				}",
	"#endif",
	"				goto Up;",
	"			   }",
	"			}",
	"#endif",

	"#ifndef NOREDUCE",
	"	#ifndef SAFETY",
	"		#if NCORE>1 && !defined(SEP_STATE) && defined(V_PROVISO)",
	"			if (II != 0 && (!Lstate || Lstate->cpu_id < core_id))",
	"			{	(trpt-1)->tau |= 16;",	/* treat as a stack state */
	"			}",
	"		#endif",
	"			if ((II && JJ) || (II == 3))",
	"			{	/* marker for liveness proviso */",
	"		#ifndef LOOPSTATE",
	"				(trpt-1)->tau |= 16;",	/* truncated on stack */
	"		#endif",
	"				truncs2++;",
	"			}",
		"#else",
	"		#if NCORE>1 && !defined(SEP_STATE) && defined(V_PROVISO)",
	"			if (!(II != 0 && (!Lstate || Lstate->cpu_id < core_id)))",
	"			{	/* treat as stack state */",
	"				(trpt-1)->tau |= 16;",
	"			} else",
	"			{	/* treat as non-stack state */",
	"				(trpt-1)->tau |= 64;",
	"			}",
	"		#endif",
	"			if (!II || !JJ)",
	"			{	/* successor outside stack */",
	"				(trpt-1)->tau |= 64;",
	"			}",
	"	#endif",
	"#endif",
	"#if defined(BCS) && (defined(NOREDUCE) || !defined(SAFETY))",
	/* needed for BCS - cover cases where it would not otherwise be set */
	"			if (!II || !JJ)",
	"			{	(trpt-1)->tau |= 64;",
	"			}",
	"#endif",
	"			if (II)",
	"			{	truncs++;",
	"#if NCORE>1 && defined(FULL_TRAIL)",
	"				if (upto > 0)",
	"				{	Pop_Stack_Tree();",
	"					if (depth == 0)",
	"					{	return;",
	"				}	}",
	"#endif",
	"				goto Up;",
	"			}",
	"			if (!kk)",
	"			{	static long sdone = (long) 0; long ndone;",
	"				nstates++;",
	"#if defined(ZAPH) && defined(BITSTATE)",
	"				zstates += (double) hfns;",
	"#endif",
	"				ndone = (unsigned long) (nstates/(freq));",
	"				if (ndone != sdone)",
	"				{	snapshot();",
	"					sdone = ndone;",
	"#if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)",
	"					if (nstates > ((double)(ONE_L<<(ssize+1))))",
	"					{	void resize_hashtable(void);",
	"						resize_hashtable();",
	"					}",
	"#endif",
	"#if defined(ZAPH) && defined(BITSTATE)",
	"					if (zstates > ((double)(ONE_L<<(ssize-2))))",
	"					{	/* more than half the bits set */",
	"						void zap_hashtable(void);",
	"						zap_hashtable();",
	"						zstates = 0;",
	"					}",
	"#endif",
	"				}",
	"#ifdef SVDUMP",
	"				if (vprefix > 0)",
	"	#ifdef SHO",	/* Store Hash Only */
	"			/* always use the same hashfunction, for consistency across runs */",
	"				if (HASH_NR != 0)",
	"				{	int oh = HASH_NR;",
	"					HASH_NR = 0;",
	"					d_hash((char *) &now, vsize); /* set K1 */",
	"					HASH_NR = oh;",
	"				}",
	"				if (write(svfd, (uchar *) &K1, sizeof(unsigned long)) != sizeof(unsigned long))",
	"	#else",
	"				if (write(svfd, (uchar *) &now, vprefix) != vprefix)",
	"	#endif",
	"				{	fprintf(efd, \"writing %%s.svd failed\\n\", PanSource);",
	"					wrapup();",
	"				}",
	"#endif",
	"#if defined(MA) && defined(W_XPT)",
	"				if ((unsigned long) nstates%%W_XPT == 0)",
	"				{	void w_xpoint(void);",
	"					w_xpoint();",
	"				}",
	"#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",
	"#else",
	"	#if NCORE>1",
	"			trpt->ostate = Lstate;",
	"	#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(\"end state in claim reached\");",
	"",
	"	if (stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])",
	"	{	uerror(\"end state in claim reached\");",
	"	}",
	"Stutter:",
	"	if (trpt->tau&4)	/* must make a claimmove */",
	"	{",
	"#ifndef NOFAIR",
	"		if ((now._a_t&2)	/* A-bit set */",
	"		&&   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",
	"		II = 0;		/* never */",
	"		goto Veri0;",
	"	}",
	"#endif",
	"#ifndef NOREDUCE",
	"	/* Look for a process with only safe transitions */",
	"	/* (special rules apply in the 2nd dfs) */",
	"	if (boq == -1 && From != To",
	"",
	"#ifdef SAFETY",
	" #if NCORE>1",
	"	&& (depth < z_handoff)", /* not for border states */
	" #endif",
	"	)",
	"#else",
	" #if NCORE>1",
	"	&& ((a_cycles) || (!a_cycles && depth < z_handoff))",
	" #endif",
	" #ifdef BCS",
	"	&& (sched_max > 0 || depth > BASE)", /* no po in initial state if -L0 */
	" #endif",
	"	&&  (!(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))", /* proviso bit in _a_t */
			"#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", /* SAFETY */
	"	/* attempt Partial Order Reduction as preselect moves */",
	"#ifdef BCS",
	"	if (trpt->sched_limit < sched_max)",	/* po only if we can switch */
	"#endif",
	"	{	for ALL_P",
	"		{",
	"Resume:		/* pick up here if preselect fails */",
	"			this = pptr(II);",
	"			tt = (int) ((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++;",
	"				}",
	"SelectIt:			From = To = II; /* preselect process */",
	"#ifdef NIBIS",
	"				t->om = 0;",
	"#endif",
	"				trpt->tau |= 32; /* preselect marker */",
	"#ifdef DEBUG",
	"				printf(\"%%3ld: proc %%d PreSelected (tau=%%d)\\n\", ",
	"					depth, II, trpt->tau);",
	"#endif",
	"				goto Again;",
	"	}	}	}",
	"	trpt->tau &= ~32;",
	"#endif",
	"#if !defined(NOREDUCE) || (defined(ETIM) && !defined(VERI))",
	"Again:",
	"#endif",
	"	trpt->o_pm &= ~(8|16|32|64); /* clear fairness-marks */",
	"#ifndef NOFAIR",
	"	if (fairness && boq == -1",
		"#ifdef VERI",
	"	&& (!(trpt->tau&4) && !((trpt-1)->tau&128))",
		"#endif",
	"	&& !(trpt->tau&8))",
	"	{	/* A_bit = 1; Cnt = N in acc states with A_bit 0 */",
	"		if (!(now._a_t&2))",	/* A-bit not set */
	"		{	if (a_cycles && (trpt->o_pm&2))",
	"			{	/* Accepting state */",
	"				now._a_t |= 2;",
	"				now._cnt[now._a_t&1] = now._nr_pr + 1;",
	"				trpt->o_pm |= 8;",
		"#ifdef DEBUG",
	"	printf(\"%%3ld: fairness Rule 1: cnt=%%d, _a_t=%%d\\n\",",
	"			depth, now._cnt[now._a_t&1], now._a_t);",
		"#endif",
	"			}",
	"		} else",		/* A-bit set */
	"		{	/* A_bit = 0 when Cnt 0 */",
	"			if (now._cnt[now._a_t&1] == 1)",
	"			{	now._a_t &= ~2;",	/* reset a-bit */
	"				now._cnt[now._a_t&1] = 0;",
	"				trpt->o_pm |= 16;",
		"#ifdef DEBUG",
	"	printf(\"%%3ld: fairness Rule 3: _a_t = %%d\\n\",",
	"		depth, now._a_t);",
		"#endif",
	"	}	}	}",
	"#endif",

	"#ifdef BCS",	/* bounded context switching */
	"	trpt->bcs = trpt->b_pno = 0;	/* initial */",
	"	if (From != To		/* not a PO or atomic move */",
	"	&&  depth > BASE)	/* there is a prior move */",
	"	{	trpt->b_pno = now._last + BASE;",
	"		trpt->bcs = B_PHASE1;",
	"	#ifdef VERBOSE",
	"		printf(\"%%3ld: BCS phase 1 proc %%d limit %%d\\n\",",
	"			depth, trpt->b_pno, trpt->sched_limit);",
	"	#endif",
	"		/* allow only process b_pno to move in this phase */",
	"	}",
	"c_switch:	/* jumps here with bcs == B_PHASE2 with or wo B_FORCED added */",
	"	#ifdef VERBOSE",
	"		printf(\"%%3ld: BCS c_switch phase=%%d pno=%%d [forced %%d]\\n\",",
	"			depth, trpt->bcs, trpt->b_pno, (trpt->bcs&B_FORCED)?1:0);",
	"	#endif",
	"#endif",

	"#ifdef P_RAND",
	"	#ifdef REVERSE",
	"	trpt->p_left = 1 + (To - From);",
	"	#else",
	"	trpt->p_left = 1 + (From - To);",
	"	#endif",
	"	if (trpt->p_left > 1)",
	"	{	trpt->p_skip = rand() %% (trpt->p_left);",
	"	} else",
	"	{	trpt->p_skip = -1;",
	"	}",
	"r_switch:",
	"	#ifdef VERBOSE",
	"		printf(\"%%3ld: P_RAND r_switch p_skip=%%d p_left=%%d\\n\",",
	"			depth, trpt->p_skip, trpt->p_left);",
	"	#endif",
	"#endif",

	"	/* Main Expansion Loop over Processes */",
	"	for ALL_P",
	"	{",
	"#ifdef P_RAND",
	"		if (trpt->p_skip >= 0)",
	"		{	trpt->p_skip--; /* skip random nr of procs */",
	"	#ifdef VERBOSE",
	"		printf(\"%%3ld: P_RAND skipping %%d [new p_skip=%%d p_left=%%d]\\n\",",
	"			depth, II, trpt->p_skip, trpt->p_left);",
	"	#endif",
	"			continue;",
	"		}",
	"		if (trpt->p_left == 0)",
	"		{",
	"	#ifdef VERBOSE",
	"		printf(\"%%3ld: P_RAND done at %%d\\n\", depth, II);",
	"	#endif",
	"			break;	/* done */",
	"		}",
	"	#ifdef VERBOSE",
	"		printf(\"%%3ld: P_RAND explore %%d [p_left=%%d]\\n\",",
	"			depth, II, trpt->p_left);",
	"	#endif",
	"		trpt->p_left--;",
	"#endif",

	"#if SYNC",
	"		/* no rendezvous with same proc */",
	"		if (boq != -1 && trpt->pr == II) continue;",
	"#endif",

	"#ifdef BCS",	/* never claim with II==0 cannot get here */
	"		if ((trpt->bcs & B_PHASE1)",
	"		&&  trpt->b_pno != II)",
	"		{",
	"	#ifdef VERBOSE",
	"		printf(\"%%3ld: BCS NotPre II=%%d bcs=%%d pno=%%d [forced %%d]\\n\",",
	"			depth, II, trpt->bcs, trpt->b_pno, (trpt->bcs&B_FORCED)?1:0);",
	"	#endif",
	"			continue;",	/* avoid context switch */
	"		}",
	"	#ifdef VERBOSE",
	"		else if ((trpt->bcs & B_PHASE1) && trpt->b_pno == II)",
	"		printf(\"%%3ld: BCS IsPre II=%%d bcs=%%d pno=%%d [forced %%d]\\n\",",
	"			depth, II, trpt->bcs, trpt->b_pno, (trpt->bcs&B_FORCED)?1:0);",
	"	#endif",

	"		if (trpt->bcs & B_PHASE2)	/* 2nd phase */",
	"		{	if (trpt->b_pno == II)	/* was already done in phase 1 */",
	"			{",
	"	#ifdef VERBOSE",
	"		printf(\"%%3ld: BCS NoRepeat II=%%d bcs=%%d pno=%%d [forced %%d]\\n\",",
	"			depth, II, trpt->bcs, trpt->b_pno, (trpt->bcs&B_FORCED)?1:0);",
	"	#endif",
	"				continue;",
	"			}",
	"			if (!(trpt->bcs & B_FORCED)	/* unless forced */",
	"			&&  trpt->sched_limit >= sched_max)",
	"			{",
	"	#ifdef VERBOSE",
	"		printf(\"%%3ld: BCS Bound II=%%d bcs=%%d pno=%%d [forced %%d]\\n\",",
	"			depth, II, trpt->bcs, trpt->b_pno, (trpt->bcs&B_FORCED)?1:0);",
	"	#endif",
	"				continue;	/* enforce bound */",
	"		}	}",
	"#endif",

	"#ifdef VERI",
	"Veri0:",
	"#endif",
	"		this = pptr(II);",
	"		tt = (int) ((P0 *)this)->_p;",
	"		ot = (uchar) ((P0 *)this)->_t;",

	"#ifdef NIBIS",
	"		/* don't repeat a previous preselected expansion */",
	"		/* could hit this if reduction proviso was false */",
	"		t = trans[ot][tt];",
	"		if (!(trpt->tau&4)",	/* not claim */
	"		&& !(trpt->tau&1)",	/* not timeout */
	"		&& !(trpt->tau&32)",	/* not preselected */
	"		&& (t->atom & 8)",	/* local */
	"		&& boq == -1",		/* not inside rendezvous */
	"		&& From != To)",	/* not inside atomic seq */
	"		{	if (t->qu[0] == 0",	/* unconditional */
	"			||  q_cond(II, t))",	/* true condition */
	"			{	_m = t->om;",
	"				if (_m>_n||(_n>3&&_m!=0)) _n=_m;",
	"				continue; /* did it before */",
	"		}	}",
	"#endif",
	"		trpt->o_pm &=  ~1; /* no move in this pid yet */",
	"#ifdef EVENT_TRACE",
	"		(trpt+1)->o_event = now._event;",
	"#endif",
	"		/* Fairness: Cnt++ when Cnt == II */",
	"#ifndef NOFAIR",
	"		trpt->o_pm &= ~64; /* didn't apply rule 2 */",
	"		if (fairness",
	"		&& boq == -1",	/* not mid rv - except rcv - NEW 3.0.8 */
	"		&& !(trpt->o_pm&32)",	/* Rule 2 not in effect */
	"		&& (now._a_t&2)",	/* A-bit is set */
	"		&&  now._cnt[now._a_t&1] == II+2)",
	"		{	now._cnt[now._a_t&1] -= 1;",
		"#ifdef VERI",
	"			/* claim need not participate */",
	"			if (II == 1)",
	"				now._cnt[now._a_t&1] = 1;",
		"#endif",
		"#ifdef DEBUG",
	"		printf(\"%%3ld: 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",
	"		(trpt+1)->pr = (uchar) II;",	/* for uerror */
	"		(trpt+1)->st = tt;",

	"#ifdef T_RAND",
	"		for (ooi = eoi = 0, t = trans[ot][tt]; t; t = t->nxt, ooi++)",
	"		{	if (strcmp(t->tp, \"else\") == 0",
	"#ifdef HAS_UNLESS",
	"			||  t->e_trans != 0",
	"#endif",
	"			)",
	"			{	eoi++;", /* no break, must count ooi */
	"		}	}",
	"		if (eoi > 0)",
	"		{	t = trans[ot][tt];",
	"	#ifdef VERBOSE",
	"			printf(\"randomizer: suppressed, saw else or escape\\n\");",
	"	#endif",
	"		} else",
	"		{	eoi = rand()%%ooi;",
	"	#ifdef VERBOSE",
	"			printf(\"randomizer: skip %%d in %%d\\n\", eoi, ooi);",
	"	#endif",
	"			for (t = trans[ot][tt]; t; t = t->nxt)",
	"				if (eoi-- <= 0) break;",
	"		}",
	"domore:",
	"		for ( ; t && ooi > 0; t = t->nxt, ooi--)",
	"#else", /* ie dont randomize */
	"		for (t = trans[ot][tt]; t; t = t->nxt)",
	"#endif",
	"		{",
	"#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",
	"	#if defined(TRIX) && !defined(TRIX_ORIG) && !defined(BFS)",
	"			(trpt+1)->p_bup = now._ids_[II];",
	"	#endif",
	"			(trpt+1)->o_t = t;",	/* for uerror */
	"#ifdef INLINE",
	"#include FORWARD_MOVES",
	"P999:			/* jumps here when move succeeds */",
	"#else",
	"			if (!(_m = do_transit(t, II))) continue;",
	"#endif",
	"#ifdef BCS",
	"			if (depth > BASE",	/* has prior move */
	"			&& II >= BASE",		/* not claim */
	"			&& From != To",		/* not atomic or po */
	"	#ifndef BCS_NOFIX",
	"			/* added 5.2.5: prior move was not po */",
	"			&& !((trpt-(BASE+1))->tau & 32)",
	"	#endif",
	"			&& boq == -1",		/* not rv */
	"			&& (trpt->bcs & B_PHASE2)",
	"			&&  trpt->b_pno != II	/* context switch */", /* redundant */
	"			&& !(trpt->bcs & B_FORCED))	/* unless forced */",
	"			{	(trpt+1)->sched_limit = 1 + trpt->sched_limit;",
	"	#ifdef VERBOSE",
	"		printf(\"%%3ld: up sched count to %%d\\n\", depth, (trpt+1)->sched_limit);",
	"	#endif",
	"			} else",
	"			{	(trpt+1)->sched_limit = trpt->sched_limit;",
	"	#ifdef VERBOSE",
	"		printf(\"%%3ld: keep sched count at %%d\\n\", depth, (trpt+1)->sched_limit);",
	"	#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;",	/* CTL */
	"				trpt->o_pm |= 1; /* we moved */",
	"			}",
		"#else",
	"				trpt->o_pm |= 1; /* we moved */",
		"#endif",

	"#ifdef LOOPSTATE",
	"			if (loopstate[ot][tt])",
	"			{",
		"#ifdef VERBOSE",
	"				printf(\"exiting from loopstate:\\n\");",
		"#endif",
	"				trpt->tau |= 16;",	/* exiting loopstate */
	"				cnt_loops++;",
	"			}",
	"#endif",

	"#ifdef PEG",
	"			peg[t->forw]++;",
	"#endif",
	"#if defined(VERBOSE) || defined(CHECK)",
		"#if defined(SVDUMP)",
	"	cpu_printf(\"%%3ld: proc %%d exec %%d \\n\", depth, II, t->t_id);",
		"#else",
	"	cpu_printf(\"%%3ld: proc %%d exec %%d, %%d to %%d, %%s %%s %%s %%saccepting [tau=%%d]\\n\", ",
	"				depth, II, t->forw, tt, t->st, t->tp,",
	"				(t->atom&2)?\"atomic\":\"\",",
	"				(boq != -1)?\"rendez-vous\":\"\",",
	"				(trpt->o_pm&2)?\"\":\"non-\", trpt->tau);",
		"#ifdef HAS_UNLESS",
	"			if (t->e_trans)",
	"			cpu_printf(\"\\t(escape to state %%d)\\n\", t->st);",
		"#endif",
		"#endif",
		"#ifdef T_RAND",
	"			cpu_printf(\"\\t(randomizer %%d)\\n\", ooi);",
		"#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 = (uchar) 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)",
	"			{",
		"#if (ACCEPT_LAB>0 && !defined(NP)) || (PROG_LAB>0 && defined(HAS_NP))",
	"				int ii;",
		"#endif",
		"#define P__Q	((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[P__Q->_t][P__Q->_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[P__Q->_t][P__Q->_p])",
	"				  {	trpt->o_pm |= 4;",
	"					break;",
	"			   	} }",
		"#endif",
		"#undef P__Q",
	"			}",
	"#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;",

	"#ifdef T_RAND",
	"			trpt->oo_i = ooi;",
	"#endif",
	"			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 = FROM_P; To = UPTO_P;",
	"			}",
	"#if NCORE>1 && defined(FULL_TRAIL)",
	"			if (upto > 0)",
	"			{	Push_Stack_Tree(II, t->t_id);",
	"			}",
	"#endif",
	"#ifdef TRIX",
	"			if (processes[II])", /* last move could have been a delproc */
	"			{	processes[II]->modified = 1; /* transition in II */",
	"	#ifdef V_TRIX",
	"				printf(\"%%4d: process %%d modified\\n\", depth, II);",
	"			} else",
	"			{	printf(\"%%4d: process %%d modified but gone (%%p)\\n\",",
	"					depth, II, trpt);",
	"	#endif",
	"			}",
	"#endif",
	"			goto Down;	/* pseudo-recursion */",
	"Up:",
	"#ifdef TRIX",
	"	#ifndef TRIX_ORIG",
	"		#ifndef BFS",
	"			now._ids_[trpt->pr] = trpt->p_bup;",
	"		#endif",
	"	#else",
	"			if (processes[trpt->pr])",
	"			{",
	"				processes[trpt->pr]->modified = 1; /* reverse move */",
	"		#ifdef V_TRIX",
	"				printf(\"%%4d: unmodify pr %%d (%%p)\\n\",",
	"					depth, trpt->pr, trpt);",
	"			} else",
	"			{	printf(\"%%4d: unmodify pr %%d (gone) (%%p)\\n\",",
	"					depth, trpt->pr, trpt);",
	"		#endif",
	"			}",
	"	#endif",
	"#endif",
	"#ifdef CHECK",
	"			cpu_printf(\"%%d: Up - %%s\\n\", depth,",
	"				(trpt->tau&4)?\"claim\":\"program\");",
	"#endif",
	"#if NCORE>1",
	"			iam_alive();",
	"	#ifdef USE_DISK",
	"			mem_drain();",
	"	#endif",
	"#endif",
	"#if defined(MA) || NCORE>1",
	"			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)",	/* 5.1.6: was + 2 */
	"			{",
	" 				trpt += DDD;",
	"				disk2stack();",
	"				maxdepth -= DDD;",
	"				hiwater -= DDD;",
	"				if(verbose)",
	"				printf(\"unzap %%d: %%d\\n\", CNT2, hiwater);",
	"			}",
	"#endif",

	"#ifndef SAFETY",	/* moved earlier in version 5.2.5 */
	"			if ((now._a_t&1) && depth <= A_depth)",
	"				return;	/* to checkcycles() */",
	"#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(\"%%3ld: 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",
	"			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 T_RAND",
	"			ooi = trpt->oo_i;",
	"#endif",
	"#ifdef INLINE_REV",
	"			_m = do_reverse(t, II, _m);",
	"#else",
	"#include REVERSE_MOVES",
	"R999:			/* jumps here when done */",
	"#endif",

	"#ifdef VERBOSE",
	"			cpu_printf(\"%%3ld: proc %%d reverses %%d, %%d to %%d\\n\",",
	"				depth, II, t->forw, tt, t->st);",
	"			cpu_printf(\"\\t%%s [abit=%%d,adepth=%%d,tau=%%d,%%d]\\n\", ",
	"				t->tp, now._a_t, A_depth, 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;",	/* pass upward */
	"	#ifdef SAFETY",
	"			if ((trpt->tau&8)	/* rv or atomic */",
	"			&&  (trpt->tau&64))",
	"				(trpt-1)->tau |= 64;",
	"	#endif",
	"#endif",

	"#if defined(BCS) && (defined(NOREDUCE) || !defined(SAFETY))",
	/* for BCS, cover cases where 64 is otherwise not handled */
	"			if ((trpt->tau&8)",
	"			&&  (trpt->tau&64))",
	"				(trpt-1)->tau |= 64;",
	"#endif",

	"			depth--; trpt--;",
	"",
	"#ifdef NSUCC",
	"			trpt->n_succ++;",
	"#endif",
	"#ifdef NIBIS",
	"			(trans[ot][tt])->om = _m; /* head of list */",
	"#endif",

	"			/* i.e., not set if rv fails */",
	"			if (_m)",
	"			{	reached[ot][t->st] = 1;",
	"				reached[ot][tt] = 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 */",

	"#ifdef T_RAND",
	"		if (!t && ooi > 0)",	/* means we skipped some initial options */
	"		{	t = trans[ot][tt];",
	"	#ifdef VERBOSE",
	"			printf(\"randomizer: continue for %%d more\\n\", ooi);",
	"	#endif",
	"			goto domore;",
	"		}",
	"	#ifdef VERBOSE",
	"		  else",
	"			printf(\"randomizer: done\\n\");",
	"	#endif",
	"#endif",

	"#ifndef NOFAIR",
	"		/* Fairness: undo Rule 2 */",
	"		if ((trpt->o_pm&32)",/* rule 2 was applied */
	"		&&  (trpt->o_pm&64))",/* by this process II */
	"		{	if (trpt->o_pm&1)",/* it didn't block */
	"			{",
		"#ifdef VERI",
	"				if (now._cnt[now._a_t&1] == 1)",
	"					now._cnt[now._a_t&1] = 2;",
		"#endif",
	"				now._cnt[now._a_t&1] += 1;",
		"#ifdef VERBOSE",
	"		printf(\"%%3ld: proc %%d fairness \", depth, II);",
	"		printf(\"undo Rule 2, cnt=%%d, _a_t=%%d\\n\",",
	"			now._cnt[now._a_t&1], now._a_t);",
		"#endif",
	"				trpt->o_pm &= ~(32|64);",
	"			} else",	/* process blocked  */
	"			{	if (_n > 0)", /* a prev proc didn't */
	"				{",	/* start over */
	"					trpt->o_pm &= ~64;",
	"					II = INI_P;", /* after loop incr II == From */
	"		}	}	}",
	"#endif",

	"#ifdef VERI",
	"		if (II == 0) break;	/* never claim */",
	"#endif",
	"	} /* all processes */",

	"#ifdef NSUCC",
	"	tally_succ(trpt->n_succ);",
	"#endif",

	"#ifdef P_RAND",
	"	if (trpt->p_left > 0)",
	"	{	trpt->p_skip = -1; /* probably rendundant */",
	"	#ifdef VERBOSE",
	"		printf(\"%%3ld: P_RAND -- explore remainder\\n\", depth);",
	"	#endif",
	"		goto r_switch; /* explore the remaining procs */",
	"	} else",
	"	{",
	"	#ifdef VERBOSE",
	"		printf(\"%%3ld: P_RAND -- none left\\n\", depth);",
	"	#endif",
	"	}",
	"#endif",

	"#ifdef BCS",
	"	if (trpt->bcs & B_PHASE1)",
	"	{	trpt->bcs = B_PHASE2;	/* start 2nd phase */",
	"		if (_n == 0 || !(trpt->tau&64))	/* pre-move unexecutable or led to stackstate */",
	"		{	trpt->bcs |= B_FORCED; /* forced switch */",
	"		}",
	"	#ifdef VERBOSE",
	"		printf(\"%%3ld: BCS move to phase 2, _n=%%d %%s\\n\", depth, _n,",
	"			(trpt->bcs & B_FORCED)?\"forced\":\"free\");",
	"	#endif",
	"		From = FROM_P; To = UPTO_P;",
	"		goto c_switch;",
	"	}",
	"",
	"	if (_n == 0	/* no process could move */",
	"	&&  II >= BASE	/* not the never claim */",
	"	&&  trpt->sched_limit >= sched_max)",
	"	{	_n = 1;",
	"	#ifdef VERBOSE",
	"		printf(\"%%3ld: BCS not a deadlock\\n\", depth);",
	"	#endif",
	"	}",
	"#endif",

	"#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(\"%%3ld: proc -- fairness \", depth);",
	"		printf(\"undo Rule 2, cnt=%%d, _a_t=%%d\\n\",",
	"			now._cnt[now._a_t&1], now._a_t);",
		"#endif",
	"		trpt->o_pm &= ~32;",
	"	}",
	"#ifndef NP",
	/* 12/97 non-progress cycles cannot be created
	 * by stuttering extension, here or elsewhere
	 */
	"	if (fairness",
	"	&&  _n == 0		/* nobody moved */",
		"#ifdef VERI",
		"	&& !(trpt->tau&4)	/* in program move */",
		"#endif",
	"	&& !(trpt->tau&8)	/* not an atomic one */",
		"#ifdef OTIM",
		"	&& ((trpt->tau&1) || endstate())",
		"#else",
			"#ifdef ETIM",
			"	&&  (trpt->tau&1)	/* already tried timeout */",
			"#endif",
		"#endif",
		"#ifndef NOREDUCE",
		"	/* see below  */",
		"	&& !((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
		"#endif",
	"	&& now._cnt[now._a_t&1] > 0)	/* needed more procs */",
	"	{	depth++; trpt++;",
	"		trpt->o_pm |= 128 | ((trpt-1)->o_pm&(2|4));",
	"		trpt->bup.oval = now._cnt[now._a_t&1];",
	"		now._cnt[now._a_t&1] = 1;",
		"#ifdef VERI",
	"		trpt->tau = 4;",
		"#else",
	"		trpt->tau = 0;",
		"#endif",
	"		From = FROM_P; To = UPTO_P;",
		"#if defined(VERBOSE) || defined(CHECK)",
	"		printf(\"%%3ld: 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(\"%%3ld: fairness undo Rule 1, _a_t=%%d\\n\",",
	"			depth, now._a_t);",
		"#endif",
	"	}",
	"	if (trpt->o_pm&16)",
	"	{	now._a_t |= 2;",		/* restore a-bit */
	"		now._cnt[now._a_t&1] = 1;",	/* NEW: restore cnt */
	"		trpt->o_pm &= ~16;",
		"#ifdef VERBOSE",
	"		printf(\"%%3ld: fairness undo Rule 3, _a_t=%%d\\n\",",
	"			depth, now._a_t);",
		"#endif",
	"	}",
	"#endif",

	"#ifndef NOREDUCE",
"#ifdef SAFETY",
	"	#ifdef LOOPSTATE",
	"	/* at least one move that was preselected at this */",
	"	/* level, blocked or was a loop control flow point */",
	"	if ((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
	"	#else",
	"	/* preselected move - no successors outside stack */",
	"	if ((trpt->tau&32) && !(trpt->tau&64))",
	"	#endif",
	"	{	From = FROM_P; To = UPTO_P;",
	"	#ifdef DEBUG",
	"		printf(\"%%3ld: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
	"			depth, II+1, _n, trpt->tau);",
	"	#endif",
	"		_n = 0; trpt->tau &= ~(16|32|64);",

	"		if (MORE_P)	/* 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  */",
	"	if ((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
	"	{",
	"	#ifdef DEBUG",
	"		printf(\"%%3ld: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
	"		depth, II+1, (int) _n, trpt->tau);",
	"	#endif",
	"		if (a_cycles && (trpt->tau&16))",
	"		{	if (!(now._a_t&1))",
	"			{",
	"	#ifdef DEBUG",
	"			printf(\"%%3ld: 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 = FROM_P; To = UPTO_P;",
	"				_n = 0; trpt->tau &= ~(16|32|64);",
	"				goto Again; /* do full search */",
	"			} /* else accept reduction */",
	"		} else",
	"		{	From = FROM_P; To = UPTO_P;",
	"			_n = 0; trpt->tau &= ~(16|32|64);",
	"			if (MORE_P)	/* II already decremented */",
	"				goto Resume;",
	"			else",
	"				goto Again;",
	"	}	}",
"#endif",
	"#endif",

	"	if (_n == 0 || ((trpt->tau&4) && (trpt->tau&2)))",
	"	{",
		"#ifdef DEBUG",
	"		cpu_printf(\"%%3ld: 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 && (!strict || qs_empty()))",
	"#ifdef OTIM",
	"		||  endstate()",
	"#endif",
	"		||  depth >= maxdepth-1) goto Done;	/* undo change from 5.2.3 */",

	"		if ((trpt->tau&8) && !(trpt->tau&4))",
	"		{	trpt->tau &= ~(1|8);",
	"			/* 1=timeout, 8=atomic */",
	"			From = FROM_P; To = UPTO_P;",
		"#ifdef DEBUG",
	"		cpu_printf(\"%%3ld: atomic step proc %%d unexecutable\\n\", depth, II+1);",
		"#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",
	"				cpu_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",
	"				cpu_printf(\"%%d: req timeout\\n\",",
	"					depth);",
				"#endif",
	"				(trpt-1)->tau |= 2; /* request */",
	"#if NCORE>1 && defined(FULL_TRAIL)",
	"				if (upto > 0)",
	"				{	Pop_Stack_Tree();",
	"				}",
	"#endif",
	"				goto Up;",
	"			}",
	"#else",

				"#ifdef DEBUG",
	"			cpu_printf(\"%%d: timeout\\n\", depth);",
				"#endif",
	"			trpt->tau |=  1;",
	"			goto Again;",
	"#endif",
	"		}",
	"#endif",

	/* old location of atomic block code */
	"#ifdef VERI",
	"BreakOut:",
		"#ifndef NOSTUTTER",
	"		if (!(trpt->tau&4))",
	"		{	trpt->tau |= 4;   /* claim stuttering */",
	"			trpt->tau |= 128; /* stutter mark */",
				"#ifdef DEBUG",
	"			cpu_printf(\"%%d: claim stutter\\n\", depth);",
				"#endif",
	"			goto Stutter;",
	"		}",
		"#else",
	"		;",
		"#endif",
	"#else",
	"		if (!noends && !a_cycles && !endstate())",
	"		{	depth--; trpt--;	/* new 4.2.3 */",
	"			uerror(\"invalid end state\");",
	"			depth++; trpt++;",
	"		}",
		"#ifndef NOSTUTTER",
	"		else if (a_cycles && (trpt->o_pm&2)) /* new 4.2.4 */",
	"		{	depth--; trpt--;",
	"			uerror(\"accept stutter\");",
	"			depth++; trpt++;",
	"		}",
		"#endif",
	"#endif",
	"	}",
	"Done:",
	"	if (!(trpt->tau&8))	/* not in atomic seqs */",
	"	{",

"#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",

	"#ifndef SAFETY",
	"		if (_n != 0",		/* we made a move */
		"#ifdef VERI",
	"		/* --after-- a program-step, i.e., */",
	"		/* after backtracking a claim-step */",
	"		&& (trpt->tau&4)",
	"		/* with at least one running process */",
	"		/* unless in a stuttered accept state */",
	"		&& ((now._nr_pr > 1) || (trpt->o_pm&2))",
		"#endif",
	"		&& !(now._a_t&1))",	/* not in 2nd DFS */
	"		{",
		"#ifndef NOFAIR",
	"			if (fairness)",	/* implies a_cycles */
	"			{",
			"#ifdef VERBOSE",
	"			cpu_printf(\"Consider check %%d %%d...\\n\",",
	"				now._a_t, now._cnt[0]);",
			"#endif",
#if 0
		the a-bit is set, which means that the fairness
		counter is running -- it was started in an accepting state.
		we check that the counter reached 1, which means that all
		processes moved least once.
		this means we can start the search for cycles -
		to be able to return to this state, we should be able to
		run down the counter to 1 again -- which implies a visit to
		the accepting state -- even though the Seed state for this
		search is itself not necessarily accepting
#endif
	"				if ((now._a_t&2) /* A-bit */",
	"				&&  (now._cnt[0] == 1))",
	"					checkcycles();",
	"			} else",
		"#endif",
	"			if (a_cycles && (trpt->o_pm&2))",
	"				checkcycles();",
	"		}",
	"#endif",
	"	}",
	"	if (depth > 0)",
	"	{",
	"#if NCORE>1 && defined(FULL_TRAIL)",
	"		if (upto > 0)",
	"		{	Pop_Stack_Tree();",
	"		}",
	"#endif",
	"		goto Up;",
	"	}",
	"}\n",
	"#else",
	"void new_state(void) { /* place holder */ }",
	"#endif",	/* BFS */
	"",
	"void",
	"spin_assert(int a, char *s, int ii, int tt, Trans *t)",
	"{",
	"	if (!a && !noasserts)",
	"	{	char bad[1024];",
	"		strcpy(bad, \"assertion violated \");",
	"		if (strlen(s) > 1000)",
	"		{	strncpy(&bad[19], (const char *) s, 1000);",
	"			bad[1019] = '\\0';",
	"		} else",
	"			strcpy(&bad[19], s);",
	"		uerror(bad);",
	"	}",
	"}",
	"#ifndef NOBOUNDCHECK",
	"int",
	"Boundcheck(int x, int y, int a1, int a2, Trans *a3)",
	"{",
	"	spin_assert((x >= 0 && x < y), \"- invalid array index\",",
	"		a1, a2, a3);",
	"	return x;",
	"}",
	"#endif",
	"void",
	"wrap_stats(void)",
	"{",
	"	if (nShadow>0)",
	"	  printf(\"%%9.8g states, stored (%%g visited)\\n\",",
	"			nstates - nShadow, nstates);",
	"	else",
	"	  printf(\"%%9.8g states, stored\\n\", nstates);",
	"#ifdef BFS",
	"#if SYNC",
	"	printf(\"	%%8g nominal states (- rv and atomic)\\n\", nstates-midrv-nlinks+revrv);",
	"	printf(\"	%%8g rvs succeeded\\n\", midrv-failedrv);",
	"#else",
	"	printf(\"	%%8g nominal states (stored-atomic)\\n\", nstates-nlinks);",
	"#endif",
	"#ifdef DEBUG",
	"	printf(\"	%%8g midrv\\n\", midrv);",
	"	printf(\"	%%8g failedrv\\n\", failedrv);",
	"	printf(\"	%%8g revrv\\n\", revrv);",
	"#endif",
	"#endif",
	"	printf(\"%%9.8g states, matched\\n\", truncs);",
	"#ifdef CHECK",
	"	printf(\"%%9.8g matches within stack\\n\",truncs2);",
	"#endif",
	"	if (nShadow>0)",
	"	printf(\"%%9.8g transitions (= visited+matched)\\n\",",
	"		nstates+truncs);",
	"	else",
	"	printf(\"%%9.8g transitions (= stored+matched)\\n\",",
	"		nstates+truncs);",
	"	printf(\"%%9.8g atomic steps\\n\", nlinks);",
	"	if (nlost) printf(\"%%g lost messages\\n\", (double) nlost);",
	"",
	"#ifndef BITSTATE",
	"	#ifndef MA",
	"	printf(\"hash conflicts: %%9.8g (resolved)\\n\", hcmp);",
	"	#ifndef AUTO_RESIZE",
	"	if (hcmp > (double) (1<<ssize))",
	"	{	printf(\"hint: increase hashtable-size (-w) to reduce runtime\\n\");",
	"	}	/* in multi-core: also reduces lock delays on access to hashtable */",
	"	#endif",
	"	#endif",
	"#else",
		"#ifdef CHECK",
		"	printf(\"%%8g states allocated for dfs stack\\n\", ngrabs);",
		"#endif",
	"	if (udmem)",
	"	printf(\"\\nhash factor: %%4g (best if > 100.)\\n\\n\",",
	"		(double)(((double) udmem) * 8.0) / (double) nstates);",
	"	else",
	"	printf(\"\\nhash factor: %%4g (best if > 100.)\\n\\n\",",
	"		(double)(1<<(ssize-8)) / (double) nstates * 256.0);",
	"       printf(\"bits set per state: %%u (-k%%u)\\n\", hfns, hfns);",
	"  #if 0",
	"	if (udmem)",
	"	{	printf(\"total bits available: %%8g (-M%%ld)\\n\",",
	"		((double) udmem) * 8.0, udmem/(1024L*1024L));",
	"	} else",
	"	{	printf(\"total bits available: %%8g (-w%%d)\\n\",",
	"			((double) (ONE_L << (ssize-4)) * 16.0), ssize);",
	"	}",
	"  #endif",
	"#endif",
	"#ifdef BFS_DISK",
	"	printf(\"bfs disk reads: %%ld writes %%ld -- diff %%ld\\n\",",
	"		bfs_dsk_reads, bfs_dsk_writes, bfs_dsk_writes-bfs_dsk_reads);",
	"	if (bfs_dsk_read  >= 0) (void) close(bfs_dsk_read);",
	"	if (bfs_dsk_write >= 0) (void) close(bfs_dsk_write);",
	"	(void) unlink(\"pan_bfs_dsk.tmp\");",
	"#endif",
	"}",
	"",
	"void",
	"wrapup(void)",
	"{	double nr1, nr2, nr3 = 0.0, nr4, nr5 = 0.0;",
	"#if !defined(MA) && (defined(MEMCNT) || defined(MEMLIM))",
	"	int mverbose = 1;",
	"#else",
	"	int mverbose = verbose;",
	"#endif",
	"#if NCORE>1",
	"	if (verbose) cpu_printf(\"wrapup -- %%d error(s)\\n\", errors);",
	"	if (core_id != 0)",
	"	{",
	"#ifdef USE_DISK",
	"		void	dsk_stats(void);",
	"		dsk_stats();",
	"#endif",
	"		if (search_terminated != NULL)",
	"		{	*search_terminated |= 2;	/* wrapup */",
	"		}",
	"		exit(0); /* normal termination, not an error */",
	"	}",
	"#endif",
	"#if !defined(WIN32) && !defined(WIN64)",
	"	signal(SIGINT, SIG_DFL);",
	"#endif",
	"	printf(\"\\n(%%s)\\n\", SpinVersion);",
	"	if (!done) printf(\"Warning: Search not completed\\n\");",
	"#ifdef SC",
	"	(void) unlink((const char *)stackfile);",
	"#endif",
	"#if NCORE>1",
	"	if (a_cycles)",
	"	{	printf(\"	+ Multi-Core (NCORE=%%d)\\n\", NCORE);",
	"	} else",
	"	{	printf(\"	+ Multi-Core (NCORE=%%d -z%%ld)\\n\", NCORE, z_handoff);",
	"	}",
	"#endif",
	"#ifdef BFS",
	"	printf(\"	+ Using Breadth-First Search\\n\");",
	"#endif",
	"#ifndef NOREDUCE",
	"	printf(\"	+ Partial Order Reduction\\n\");",
	"#endif",
	"#ifdef REVERSE",
	"	printf(\"	+ Reverse Depth-First Search Order\\n\");",
	"#endif",
	"#ifdef T_REVERSE",
	"	printf(\"	+ Reverse Transition Ordering\\n\");",
	"#endif",
	"#ifdef T_RAND",
	"	printf(\"	+ Randomized Transition Ordering\\n\");",
	"#endif",
	"#ifdef P_RAND",
	"	printf(\"	+ Randomized Process Ordering\\n\");",
	"#endif",
	"#ifdef BCS",
	"	printf(\"	+ Scheduling Restriction (-L%%d)\\n\", sched_max);",
	"#endif",
	"#ifdef TRIX",
	"	printf(\"	+ Tree Index Compression\\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\", PanSource);",
	"  #endif",
	"#endif",
	"#ifdef CHECK",
	"  #ifdef FULLSTACK",
	"	printf(\"	+ FullStack Matching\\n\");",
	"  #endif",
	"  #ifdef CNTRSTACK",
	"	printf(\"	+ CntrStack Matching\\n\");",
	"  #endif",
	"#endif",
	"#ifdef BITSTATE",
	"	printf(\"\\nBit statespace search for:\\n\");",
	"#else",
	"  #ifdef HC",
	"	printf(\"\\nHash-Compact %%d search for:\\n\", HC);",
	"  #else",
	"	printf(\"\\nFull statespace search for:\\n\");",
	"  #endif",
	"#endif",
	"#ifdef EVENT_TRACE",
	"#ifdef NEGATED_TRACE",
	"	printf(\"\tnotrace assertion  \t+\\n\");",
	"#else",
	"	printf(\"\ttrace assertion    \t+\\n\");",
	"#endif",
	"#endif",
	"#ifdef VERI",
	"	printf(\"\tnever claim         \t+\");",
	"	printf(\" (%%s)\\n\", procname[((Pclaim *)pptr(0))->_t]);",
	"	printf(\"\tassertion violations\t\");",
	"	if (noasserts)",
	"		printf(\"- (disabled by -A flag)\\n\");",
	"	else",
	"		printf(\"+ (if within scope of claim)\\n\");",
	"#else",
		"#ifdef NOCLAIM",
	"	printf(\"\tnever claim         \t- (not selected)\\n\");",
		"#else",
	"	printf(\"\tnever claim         \t- (none specified)\\n\");",
		"#endif",
	"	printf(\"\tassertion violations\t\");",
	"	if (noasserts)",
	"		printf(\"- (disabled by -A flag)\\n\");",
	"	else",
	"		printf(\"+\\n\");",
	"#endif",
	"#ifndef SAFETY",
		"#ifdef NP",
	"	printf(\"\tnon-progress cycles \t\");",
		"#else",
	"	printf(\"\tacceptance   cycles \t\");",
		"#endif",
	"	if (a_cycles)",
	"		printf(\"+ (fairness %%sabled)\\n\",",
	"			fairness?\"en\":\"dis\");",
	"	else printf(\"- (not selected)\\n\");",
	"#else",
	"	printf(\"\tcycle checks       \t- (disabled by -DSAFETY)\\n\");",
	"#endif",
	"#ifdef VERI",
	"	printf(\"\tinvalid end states\t- \");",
	"	printf(\"(disabled by \");",
	"	if (noends)",
	"		printf(\"-E flag)\\n\\n\");",
	"	else",
	"		printf(\"never claim)\\n\\n\");",
	"#else",
	"	printf(\"\tinvalid end states\t\");",
	"	if (noends)",
	"		printf(\"- (disabled by -E flag)\\n\\n\");",
	"	else",
	"		printf(\"+\\n\\n\");",
	"#endif",
	"	printf(\"State-vector %%d byte, depth reached %%ld\", hmax,",
	"#if NCORE>1",
	"					(nr_handoffs * z_handoff) +",
	"#endif",
	"					mreached);",
	"	printf(\", errors: %%d\\n\", errors);",
	"	fflush(stdout);",
	"#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();",
	"#ifdef CHECK",
	"	printf(\"stackframes: %%d/%%d\\n\\n\", smax, svmax);",
	"	printf(\"stats: fa %%ld, fh %%ld, zh %%ld, zn %%ld - \",",
	"		Fa, Fh, Zh, Zn);",
	"	printf(\"check %%ld holds %%ld\\n\", Ccheck, Cholds);",
	"	printf(\"stack stats: puts %%ld, probes %%ld, zaps %%ld\\n\",",
	"		PUT, PROBE, ZAPS);",
	"#else",
	"	printf(\"\\n\");",
	"#endif",
	"",
	"#if !defined(BITSTATE) && defined(NOCOMP)",
	"	if (!verbose) { goto jump_here; }",	/* added 5.2.0 */
	"#endif",
	"",
	"#if 1",	/* omitted 5.2.0:  defined(BITSTATE) || !defined(NOCOMP) */
	"	nr1 = (nstates-nShadow)*",
	"	      (double)(hmax+sizeof(struct H_el)-sizeof(unsigned));",
	"	#ifdef BFS",
	"	nr2 = 0.0;",
	"	#else",
	"	nr2 = (double) ((maxdepth+3)*sizeof(Trail));",
	"	#endif",

	"	#ifndef BITSTATE",
			"#if !defined(MA) || defined(COLLAPSE)",
	"	nr3 = (double) (ONE_L<<ssize)*sizeof(struct H_el *);",
			"#endif",
	"	#else",
	"	if (udmem)",
	"		nr3 = (double) (udmem);",
	"	else",
	"		nr3 = (double) (ONE_L<<(ssize-3));",
			"#ifdef CNTRSTACK",
	"	nr5 = (double) (ONE_L<<(ssize-3));",
			"#endif",
			"#ifdef FULLSTACK",
	"	nr5 = (double) (maxdepth*sizeof(struct H_el *));",
			"#endif",
	"	#endif",

	"	nr4 = (double) (svmax * (sizeof(Svtack) + hmax))",
	"	    + (double) (smax  * (sizeof(_Stack) + Maxbody * sizeof(char)));",
		"#ifndef MA",
	"	if (1 /* mverbose || memcnt < nr1+nr2+nr3+nr4+nr5 */)",
		"#endif",
	"	{ double remainder = memcnt;",
	"	  double tmp_nr = memcnt-nr3-nr4-(nr2-fragment)-nr5;",
	"",
	"	#if NCORE>1 && !defined(SEP_STATE)",
	"		tmp_nr -= ((double) NCORE * LWQ_SIZE) + GWQ_SIZE;",
	"	#endif",
	"		if (tmp_nr < 0.0) tmp_nr = 0.;",
	"		printf(\"Stats on memory usage (in Megabytes):\\n\");",
	"		printf(\"%%9.3f\tequivalent memory usage for states\",",
	"			nr1/1048576.); /* 1024*1024=1048576 */",
	"		printf(\" (stored*(State-vector + overhead))\\n\");",
	"	#if NCORE>1 && !defined(WIN32) && !defined(WIN64)",
	"		printf(\"%%9.3f\tshared memory reserved for state storage\\n\",",
	"			mem_reserved/1048576.);",
	"		#ifdef SEP_HEAP",
	"		printf(\"\t\tin %%d local heaps of %%7.3f MB each\\n\",",
	"			NCORE, mem_reserved/(NCORE*1048576.));",
	"		#endif",
	"		printf(\"\\n\");",
	"	#endif",
		"#ifdef BITSTATE",
	"		if (udmem)",
	"			printf(\"%%9.3f\tmemory used for hash array (-M%%ld)\\n\",",
	"			nr3/1048576., udmem/(1024L*1024L));",
	"		else",
	"			printf(\"%%9.3f\tmemory used for hash array (-w%%d)\\n\",",
	"			nr3/1048576., ssize);",
	"		if (nr5 > 0.0)",
	"		printf(\"%%9.3f\tmemory used for bit stack\\n\",",
	"			nr5/1048576.);",
	"		remainder = remainder - nr3 - nr5;",
		"#else",
	"		printf(\"%%9.3f\tactual memory usage for states\",",
	"			tmp_nr/1048576.);",
	"		remainder -= tmp_nr;",
	"		printf(\" (\");",
	"		if (tmp_nr > 0.)",
	"		{	if (tmp_nr > nr1) printf(\"unsuccessful \");",
	"			printf(\"compression: %%.2f%%%%)\\n\",",
	"				(100.0*tmp_nr)/nr1);",
	"		} else",
	"			printf(\"less than 1k)\\n\");",
			"#ifndef MA",
	"		if (tmp_nr > 0.)",
	"		{	printf(\"         \tstate-vector as stored = %%.0f byte\",",
	"			(tmp_nr)/(nstates-nShadow) -",
	"			(double) (sizeof(struct H_el) - sizeof(unsigned)));",
	"			printf(\" + %%ld byte overhead\\n\",",
	"			(long int) sizeof(struct H_el)-sizeof(unsigned));",
	"		}",
			"#endif",
			"#if !defined(MA) || defined(COLLAPSE)",
	"		printf(\"%%9.3f\tmemory used for hash table (-w%%d)\\n\",",
	"			nr3/1048576., ssize);",
	"		remainder -= nr3;",
			"#endif",
		"#endif",
	"	#ifndef BFS",
	"		printf(\"%%9.3f\tmemory used for DFS stack (-m%%ld)\\n\",",
	"			nr2/1048576., maxdepth);",
	"		remainder -= nr2;",
	"	#endif",
		"#if NCORE>1",
	"		remainder -= ((double) NCORE * LWQ_SIZE) + GWQ_SIZE;",
	"		printf(\"%%9.3f\tshared memory used for work-queues\\n\",",
	"			(GWQ_SIZE + (double) NCORE * LWQ_SIZE) /1048576.);",
	"		printf(\"\t\tin %%d queues of %%7.3f MB each\",",
	"			NCORE, (double) LWQ_SIZE /1048576.);",
	"		#ifndef NGQ",
	"		printf(\" + a global q of %%7.3f MB\\n\",",
	"			(double) GWQ_SIZE / 1048576.);",
	"		#else",
	"		printf(\"\\n\");",
	"		#endif",
	"	#endif",
	"		if (remainder - fragment > 1048576.)",
	"		printf(\"%%9.3f\tother (proc and chan stacks)\\n\",",
	"			(remainder-fragment)/1048576.);",
	"		if (fragment > 1048576.)",
	"		printf(\"%%9.3f\tmemory lost to fragmentation\\n\",",
	"			fragment/1048576.);",
	"		printf(\"%%9.3f\ttotal actual memory usage\\n\\n\",",
	"			memcnt/1048576.);",
	"	}",
	"	#ifndef MA",
	"	else",
	"	#endif",
	"#endif",

	"#if !defined(BITSTATE) && defined(NOCOMP)",
	"jump_here:",
	"#endif",

		"#ifndef MA",
	"		printf(\"%%9.3f\tmemory usage (Mbyte)\\n\\n\",",
	"			memcnt/1048576.);",
		"#endif",
	"#ifdef COLLAPSE",
	"	printf(\"nr of templates: [ globals chans procs ]\\n\");",
	"	printf(\"collapse counts: [ \");",
	"	{ int i; for (i = 0; i < 256+2; i++)",
	"		if (ncomps[i] != 0)",
	"			printf(\"%%d \", (int) ncomps[i]);",
	"		printf(\"]\\n\");",
	"	}",
	"#endif",
	"	#ifdef TRIX",
	"	if (mverbose)",
	"	{	int i;",
	"		printf(\"TRIX counts:\\n\");",
	"		printf(\"  processes: \");",
	"		for (i = 0; i < MAXPROC; i++)",
	"			if (_p_count[i] != 0)",
	"			{	printf(\"%%3d:%%ld \",",
	"					i, _p_count[i]);",
	"			}",
	"		printf(\"\\n  channels : \");",
	"		for (i = 0; i < MAXQ; i++)",
	"			if (_c_count[i] != 0)",
	"			{	printf(\"%%3d:%%ld \",",
	"					i, _c_count[i]);",
	"			}",
	"		printf(\"\\n\\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",
	"#ifdef LOOPSTATE",
	"	printf(\"%%g loopstates hit\\n\", cnt_loops);",
	"#endif",
	"#ifdef NSUCC",
	"	dump_succ();",
	"#endif",
	"#if NCORE>1 && defined(T_ALERT)",
	"	crash_report();",
	"#endif",
	"	pan_exit(0);",
	"}\n",
	"void",
	"stopped(int arg)",
	"{	printf(\"Interrupted\\n\");",
	"#if NCORE>1",
	"	was_interrupted = 1;",
	"#endif",
	"	wrapup();",
	"	pan_exit(0);",
	"}",
	"",
	"#ifdef SFH",
	"/*",
	" * super fast hash, based on Paul Hsieh's function",
	" * http://www.azillionmonkeys.com/qed/hash.html",
	" */",
	"#include <stdint.h>",	/* for uint32_t etc */
	"	#undef get16bits",
	"	#if (defined(__GNUC__) && defined(__i386__)) || defined(__WATCOMC__) \\",
	"	|| defined(_MSC_VER) || defined (__BORLANDC__) || defined (__TURBOC__)",
	"		#define get16bits(d) (*((const uint16_t *) (d)))",
	"	#endif",
	"",
	"	#ifndef get16bits",
	"		#define get16bits(d) ((((uint32_t)(((const uint8_t *)(d))[1])) << 8)\\",
	"                       +(uint32_t)(((const uint8_t *)(d))[0]) )",
	"	#endif",
	"",
	"void",
	"d_sfh(const char *s, int len)",
	"{	uint32_t h = len, tmp;",
	"	int rem;",
	"",
	"	rem = len & 3;",
	"	len >>= 2;",
	"",
	"	for ( ; len > 0; len--)",
	"	{	h  += get16bits(s);",
	"        	tmp = (get16bits(s+2) << 11) ^ h;",
	"        	h   = (h << 16) ^ tmp;",
	"        	s  += 2*sizeof(uint16_t);",
	"		h  += h >> 11;",
	"	}",
	"	switch (rem) {",
	"	case 3: h += get16bits(s);",
	"		h ^= h << 16;",
	"		h ^= s[sizeof(uint16_t)] << 18;",
	"		h += h >> 11;",
	"		break;",
	"	case 2: h += get16bits(s);",
	"		h ^= h << 11;",
	"		h += h >> 17;",
	"		break;",
	"	case 1: h += *s;",
	"		h ^= h << 10;",
	"		h += h >> 1;",
	"		break;",
	"	}",
	"	h ^= h << 3;",
	"	h += h >> 5;",
	"	h ^= h << 4;",
	"	h += h >> 17;",
	"	h ^= h << 25;",
	"	h += h >> 6;",
	"",
	"	K1 = h;",
	"}",
	"#endif", /* SFH */
	"",
	"#include <stdint.h>", /* uint32_t etc. */
	"#if defined(HASH64) || defined(WIN64)",
	"/* 64-bit Jenkins hash, 1997",
	" * http://burtleburtle.net/bob/c/lookup8.c",
	" */",
	"#define mix(a,b,c) \\",
	"{ a -= b; a -= c; a ^= (c>>43); \\",
	"  b -= c; b -= a; b ^= (a<<9);  \\",
	"  c -= a; c -= b; c ^= (b>>8);  \\",
	"  a -= b; a -= c; a ^= (c>>38); \\",
	"  b -= c; b -= a; b ^= (a<<23); \\",
	"  c -= a; c -= b; c ^= (b>>5);  \\",
	"  a -= b; a -= c; a ^= (c>>35); \\",
	"  b -= c; b -= a; b ^= (a<<49); \\",
	"  c -= a; c -= b; c ^= (b>>11); \\",
	"  a -= b; a -= c; a ^= (c>>12); \\",
	"  b -= c; b -= a; b ^= (a<<18); \\",
	"  c -= a; c -= b; c ^= (b>>22); \\",
	"}",
	"#else",
	"/* 32-bit Jenkins hash, 2006",
	" * http://burtleburtle.net/bob/c/lookup3.c",
	" */",
	"#define rot(x,k)	(((x)<<(k))|((x)>>(32-(k))))",
	"",
	"#define mix(a,b,c) \\",
	"{ a -= c;  a ^= rot(c, 4);  c += b; \\",
	"  b -= a;  b ^= rot(a, 6);  a += c; \\",
	"  c -= b;  c ^= rot(b, 8);  b += a; \\",
	"  a -= c;  a ^= rot(c,16);  c += b; \\",
	"  b -= a;  b ^= rot(a,19);  a += c; \\",
	"  c -= b;  c ^= rot(b, 4);  b += a; \\",
	"}",
	"",
	"#define final(a,b,c) \\",
	"{ c ^= b; c -= rot(b,14); \\",
	"  a ^= c; a -= rot(c,11); \\",
	"  b ^= a; b -= rot(a,25); \\",
	"  c ^= b; c -= rot(b,16); \\",
	"  a ^= c; a -= rot(c,4);  \\",
	"  b ^= a; b -= rot(a,14); \\",
	"  c ^= b; c -= rot(b,24); \\",
	"}",
	"#endif",
	"",
	"void",
	"d_hash(uchar *kb, int nbytes)",
	"{	uint8_t  *bp;",
	"#if defined(HASH64) || defined(WIN64)",
	"	uint64_t a = 0, b, c, n;",
	"	uint64_t *k = (uint64_t *) kb;",
	"#else",
	"	uint32_t a = 0, b, c, n;",
	"	uint32_t *k = (uint32_t *) kb;",
	"#endif",
	"	n = nbytes/WS;	/* nr of words */",
	"	/* extend to multiple of words, if needed */",
	"	a = WS - (nbytes %% WS);",
	"	if (a > 0 && a < WS)",
	"	{	n++;",
	"		bp = kb + nbytes;",
	"		switch (a) {",
	"#if defined(HASH64) || defined(WIN64)",
	"		case 7: *bp++ = 0; /* fall thru */",
	"		case 6: *bp++ = 0; /* fall thru */",
	"		case 5: *bp++ = 0; /* fall thru */",
	"		case 4: *bp++ = 0; /* fall thru */",
	"#endif",
	"		case 3: *bp++ = 0; /* fall thru */",
	"		case 2: *bp++ = 0; /* fall thru */",
	"		case 1: *bp   = 0;",
	"		case 0: break;",
	"	}	}",
	"#if defined(HASH64) || defined(WIN64)",
	"	b = HASH_CONST[HASH_NR];",
	"	c = 0x9e3779b97f4a7c13LL; /* arbitrary value */",
	"	while (n >= 3)",
	"	{	a += k[0];",
	"		b += k[1];",
	"		c += k[2];",
	"		mix(a,b,c);",
	"		n -= 3;",
	"		k += 3;",
	"	}",
	"	c += (((uint64_t) nbytes)<<3);",
	"	switch (n) {",
	"	case 2: b += k[1];",
	"	case 1: a += k[0];",
	"	case 0: break;",
	"	}",
	"	mix(a,b,c);",
	"#else", /* 32 bit version: */
	"	a = c = 0xdeadbeef + (n<<2);",
	"	b = HASH_CONST[HASH_NR];",
	"	while (n > 3)",
	"	{	a += k[0];",
	"		b += k[1];",
	"		c += k[2];",
	"		mix(a,b,c);",
	"		n -= 3;",
	"		k += 3;",
	"	}",
	"	switch (n) { ",
	"	case 3: c += k[2];",
	"	case 2: b += k[1];",
	"	case 1: a += k[0];",
	"		final(a,b,c);",
	"	case 0: break;",
	"	}",
	"#endif",
	"	j1_spin = c&nmask; j3 = a&7; /* 1st bit */",
	"	j2 = b&nmask; j4 = (a>>3)&7; /* 2nd bit */",
	"	K1 = c; K2 = b;",
	"}",
	"",
	"void",
	"s_hash(uchar *cp, int om)",
	"{",
	"#if defined(SFH)",
	"	d_sfh((const char *) cp, om); /* sets K1 */",
	"#else",
	"	d_hash(cp, om);	/* sets K1 etc */",
	"#endif",
	"#ifdef BITSTATE",
	"	if (S_Tab == H_tab)",	/* state stack in bitstate search */
	"		j1_spin = K1 %% omaxdepth;",
	"	else",
	"#endif", /* if (S_Tab != H_Tab) */
	"		if (ssize < 8*WS)",
	"			j1_spin = K1&mask;",
	"		else",
	"			j1_spin = K1;",
	"}",
	"#ifndef RANDSTOR",
	"int *prerand;",
	"void",
	"inirand(void)",
	"{	int i;",
	"	srand(123);	/* fixed startpoint */",
	"	prerand = (int *) emalloc((omaxdepth+3)*sizeof(int));",
	"	for (i = 0; i < omaxdepth+3; i++)",
	"		prerand[i] = rand();",
	"}",
	"int",
	"pan_rand(void)",
	"{	if (!prerand) inirand();",
	"	return prerand[depth];",
	"}",
	"#endif",
	"",
	"void",
	"set_masks(void)	/* 4.2.5 */",
	"{",
	"	if (WS == 4 && ssize >= 32)",
	"	{	mask = 0xffffffff;",
	"#ifdef BITSTATE",
	"		switch (ssize) {",
	"		case 34: nmask = (mask>>1); break;",
	"		case 33: nmask = (mask>>2); break;",
	"		default: nmask = (mask>>3); break;",
	"		}",
	"#else",
	"		nmask = mask;",
	"#endif",
	"	} else if (WS == 8)",
	"	{	mask = ((ONE_L<<ssize)-1);	/* hash init */",
	"#ifdef BITSTATE",
	"		nmask = mask>>3;",
	"#else",
	"		nmask = mask;",
	"#endif",
	"	} else if (WS != 4)",
	"	{	fprintf(stderr, \"pan: wordsize %%ld not supported\\n\", (long int) WS);",
	"		exit(1);",
	"	} else	/* WS == 4 and ssize < 32 */",
	"	{	mask = ((ONE_L<<ssize)-1);	/* hash init */",
	"		nmask = (mask>>3);",
	"	}",
	"}",
	"",
	"static long reclaim_size;",
	"static char *reclaim_mem;",
	"#if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)",
	"#if NCORE>1",
	"	#error cannot combine AUTO_RESIZE with NCORE>1 yet",
	"#endif",
	"static struct H_el **N_tab;",
	"void",
	"reverse_capture(struct H_el *p)",
	"{	if (!p) return;",
	"	reverse_capture(p->nxt);",
	"	/* last element of list moves first */",
	"	/* to preserve list-order */",
	"	j2 = p->m_K1;",
	"	if (ssize < 8*WS) /* probably always true */",
	"	{	j2 &= mask;",
	"	}",
	"	p->nxt = N_tab[j2];",
	"	N_tab[j2] = p;",
	"}",
	"void",
	"resize_hashtable(void)",
	"{",
	"	if (WS == 4 && ssize >= 27 - 1)",
	"	{	return;	/* cannot increase further */",
	"	}",
	"",
	"	ssize += 2; /* 4x size @htable ssize */",
	"",
	"	printf(\"pan: resizing hashtable to -w%%d.. \", ssize);",
	"",
	"	N_tab = (struct H_el **)",
	"		emalloc((ONE_L<<ssize)*sizeof(struct H_el *));",
	"",
	"	set_masks();	/* they changed */",
	"",
	"	for (j1_spin = 0; j1_spin < (ONE_L << (ssize - 2)); j1_spin++)",
	"	{	reverse_capture(H_tab[j1_spin]);",
	"	}",
	"	reclaim_mem = (char *) H_tab;",
	"	reclaim_size = (ONE_L << (ssize - 2));",
	"	H_tab = N_tab;",
	"",
	"	printf(\" done\\n\");",
	"}",
	"#endif",
	"#if defined(ZAPH) && defined(BITSTATE)",
	"void",
	"zap_hashtable(void)",
	"{	cpu_printf(\"pan: resetting hashtable\\n\");",
	"	if (udmem)",
	"	{	memset(SS, 0, udmem);",
	"	} else",
	"	{	memset(SS, 0, ONE_L<<(ssize-3));",
	"	}",
	"}",
	"#endif",
	"",
	"#if NCLAIMS>1",
	"int",
	"find_claim(char *s)",
	"{	int i, j;",
	"	for (i = 0; procname[i] != \":np_:\"; i++)",
	"	{	if (strcmp(s, procname[i]) == 0)",
	"		{	for (j = 0; j < NCLAIMS; j++)",
	"			{	if (spin_c_typ[j] == i)",
	"				{	return j;",
	"			}	}",
	"			break;",
	"	}	}",
	"	printf(\"pan: error: cannot find claim '%%s'\\n\", s);",
	"	exit(1);",
	"	return -1; /* unreachable */",
	"}",
	"#endif",
	"",
	"int",
	"main(int argc, char *argv[])",
	"{	void to_compile(void);\n",
	"	efd = stderr;	/* default */",
	"",
	"	if (G_long != sizeof(long)",
	"	||  G_int  != sizeof(int))",
	"	{	printf(\"spin: error, the version of spin \");",
	"		printf(\"that generated this pan.c assumed a different \");",
	"		printf(\"wordsize (%%d iso %%d)\\n\", G_long, (int) sizeof(long));",
	"		exit(1);",
	"	}",
	"",
	"#if defined(T_RAND) && (T_RAND>0)",
	"	s_rand = T_RAND;", /* so that -RS can override */
	"#elif defined(P_RAND) && (P_RAND>0)",
	"	s_rand = P_RAND;",
	"#endif", /* else, could use time as seed... */
	"",
	"#ifdef PUTPID",
	"	{	char *ptr = strrchr(argv[0], '/');",
	"		if (ptr == NULL)",
	"		{	ptr = argv[0];",
	"		} else",
	"		{	ptr++;",
	"		}",
	"		progname = emalloc(strlen(ptr));",
	"		strcpy(progname, ptr);",
	"		/* printf(\"progname: %%s\\n\", progname); */",
	"	}",
	"#endif",
	"",
	"#ifdef BITSTATE",
	"	bstore = bstore_reg; /* default */",
	"#endif",
	"#if NCORE>1",
	"	{	int i, j;",
	"		strcpy(o_cmdline, \"\");",
	"		for (j = 1; j < argc; j++)",
	"		{	strcat(o_cmdline, argv[j]);",
	"			strcat(o_cmdline, \" \");",
	"		}",
	"		/* printf(\"Command Line: %%s\\n\", o_cmdline); */",
	"		if (strlen(o_cmdline) >= sizeof(o_cmdline))",
	"		{	Uerror(\"option list too long\");",
	"	}	}",
	"#endif",
	"	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 'b': bounded = 1; break;",
	"#ifdef HAS_CODE",
	"		case 'C': coltrace = 1; goto samething;",
	"#endif",
	"		case 'c': upto  = atoi(&argv[1][2]); break;",
	"		case 'D': dodot++; state_tables++; break;",
	"		case 'd': state_tables++; break;",
	"		case 'e': every_error = 1; upto = 0; Nr_Trails = 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",
	"#ifdef HAS_CODE",
	"		case 'g': gui = 1; goto samething;",
	"#endif",
	"		case 'h': if (!argv[1][2]) usage(efd); else",
	"			  HASH_NR = atoi(&argv[1][2])%%100; 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 */",
	"#ifdef BITSTATE",
	"		case 'k': hfns = atoi(&argv[1][2]); break;",
	"#endif",
	"#ifdef BCS",
	"		case 'L':",
	"			sched_max = atoi(&argv[1][2]);",
	"			if (sched_max > 255)	/* stored as one byte */",
	"			{	fprintf(efd, \"warning: using max bound (255)\\n\");",
	"				sched_max = 255;",
	"			}",
	"	#ifndef NOREDUCE",
	"			if (sched_max == 0)",
	"			{	fprintf(efd, \"warning: with (default) bound -L0, \");",
	"				fprintf(efd, \"using -DNOREDUCE performs better\\n\");",
	"			}",
	"	#endif",
	"			break;",
	"#endif",
	"#ifndef SAFETY",
		"#ifdef NP",
	"		case 'l': a_cycles = 1; break;",
		"#else",
	"		case 'l': fprintf(efd, \"error: -l disabled\");",
	"			  usage(efd); break;",
		"#endif",
	"#endif",
	"#ifdef BITSTATE",
	"		case 'M': udmem = atoi(&argv[1][2]); break;",
	"		case 'G': udmem = atoi(&argv[1][2]); udmem *= 1024; break;",
	"#else",
	"		case 'M': case 'G':",
	"			  fprintf(stderr, \"-M and -G affect only -DBITSTATE\\n\");",
	"			  break;",
	"#endif",
	"		case 'm': maxdepth = atoi(&argv[1][2]); break;",
"#ifndef NOCLAIM",
	"		case 'N':",
	"#if NCLAIMS>1",
	"			  if (isdigit(argv[1][2]))",
	"				whichclaim = atoi(&argv[1][2]);",
	"			  else if (isalpha(argv[1][2]))",
	"			  {     claimname = &argv[1][2];",
	"			  } else if (argc > 2 && argv[2][0] != '-') /* check next arg */",
	"			  {	claimname = argv[2];",
	"				argc--; argv++; /* skip next arg */",
	"			  }",
	"#else",
	"	#if NCLAIMS==1",
	"			  fprintf(stderr, \"warning: only one claim defined, -N ignored\\n\");",
	"	#else",
	"			  fprintf(stderr, \"warning: no claims defined, -N ignored\\n\");",
	"	#endif",
	"			  if (!isdigit(argv[1][2]) && argc > 2 && argv[2][0] != '-')",
	"			  {	argc--; argv++;",
	"			  }",
	"#endif",
"#endif",
	"			  break;\n",
	"		case 'n': no_rck = 1; break;",
	"		case 'P': readtrail = 1; onlyproc = atoi(&argv[1][2]);",
	"			  if (argv[2][0] != '-') /* check next arg */",
	"			  {	trailfilename = argv[2];",
	"				argc--; argv++; /* skip next arg */",
	"			  }",
	"			  break;",
	"#ifdef SVDUMP",
	"		case 'p': vprefix = atoi(&argv[1][2]); break;",
	"#endif",
	"#if NCORE==1",
	"		case 'Q': quota = (double) 60.0 * (double) atoi(&argv[1][2]);",
	"	#ifndef FREQ",
	"			  freq /= 10.; /* for better resolution */",
	"	#endif",
	"			  break;",
	"#endif",
	"		case 'q': strict = 1; break;",
	"		case 'R':",
	"#if defined(T_RAND) || defined(P_RAND) || defined(RANDSTOR)",
	"			if (argv[1][2] == 'S') /* e.g., -RS76842 */",
	"			{	s_rand = atoi(&argv[1][3]);",
	"			} else",
	"#endif",
	"			{	Nrun = atoi(&argv[1][2]);",
	"			}",
	"			break;",
	"#ifdef HAS_CODE",
	"		case 'r':",
	"samething:		  readtrail = 1;",
	"			  if (isdigit(argv[1][2]))",
	"				whichtrail = atoi(&argv[1][2]);",
	"			  else if (argc > 2 && argv[2][0] != '-') /* check next arg */",
	"			  {	trailfilename = argv[2];",
	"				argc--; argv++; /* skip next arg */",
	"			  }",
	"			  break;",
	"		case 'S': silent = 1; goto samething;",
	"#endif",
	"#ifdef BITSTATE",
	"		case 's': hfns = 1; break;",
	"#endif",
	"		case 'T': TMODE = 0444; break;",
	"		case 't': if (argv[1][2]) tprefix = &argv[1][2]; break;",
	"		case 'V': start_timer(); printf(\"Generated by %%s\\n\", SpinVersion);",
	"			  to_compile(); pan_exit(2); break;",
	"		case 'v': verbose++; break;",
	"		case 'w': ssize = atoi(&argv[1][2]); break;",
	"		case 'Y': signoff = 1; break;",
	"		case 'X': efd = stdout; break;",
	"		case 'x': exclusive = 1; break;",
	"#if NCORE>1",
	"		/* -B ip is passthru to proxy of remote ip address: */",
	"		case 'B': argc--; argv++; break;",
	"		case 'Q': worker_pids[0] = atoi(&argv[1][2]); break;",
	"			/* -Un means that the nth worker should be instantiated as a proxy */",
	"		case 'U': proxy_pid = atoi(&argv[1][2]); break;",
	"			/* -W means that this copy is started by a cluster-server as a remote */",
	"			/* this flag is passed to ./pan_proxy, which interprets it */",
	"		case 'W': remote_party++; break;",
	"		case 'Z': core_id = atoi(&argv[1][2]);",
	"			  if (verbose)",
	"			  { printf(\"cpu%%d: pid %%d parent %%d\\n\",",
	"				core_id, getpid(), worker_pids[0]);",
	"			  }",
	"			  break;",
	"		case 'z': z_handoff = atoi(&argv[1][2]); break;",
	"#else",
	"		case 'z': break; /* ignored for single-core */",
	"#endif",
	"		default : fprintf(efd, \"saw option -%%c\\n\", argv[1][1]); usage(efd); break;",
	"		}",
	"		argc--; argv++;",
	"	}",
	"	if (iterative && TMODE != 0666)",
	"	{	TMODE = 0666;",
	"		fprintf(efd, \"warning: -T ignored when -i or -I is used\\n\");",
	"	}",
	"#if defined(HASH32) && !defined(SFH)",
	"	if (WS > 4)",
	"	{	fprintf(efd, \"strong warning: compiling -DHASH32 on a 64-bit machine\\n\");",
	"		fprintf(efd, \" without -DSFH can slow down performance a lot\\n\");",
	"	}",
	"#endif",
	"#if defined(WIN32) || defined(WIN64)",
	"	if (TMODE == 0666)",
	"		TMODE = _S_IWRITE | _S_IREAD;",
	"	else",
	"		TMODE = _S_IREAD;",
	"#endif",
	"#if NCORE>1",
	"	store_proxy_pid = proxy_pid; /* for checks in mem_file() and someone_crashed() */",
	"	if (core_id != 0) { proxy_pid = 0; }",
	"	#ifndef SEP_STATE",
	"	if (core_id == 0 && a_cycles)",
	"	{	fprintf(efd, \"hint: this search may be more efficient \");",
	"		fprintf(efd, \"if pan.c is compiled -DSEP_STATE\\n\");",
	"	}",
	"	#endif",
	"	if (z_handoff < 0)",
	"	{	z_handoff =  20; /* conservative default - for non-liveness checks */",
	"	}",
	"#if defined(NGQ) || defined(LWQ_FIXED)",
	"	LWQ_SIZE = (double) (128.*1048576.);",
	"#else",
	"	LWQ_SIZE = (double) ( z_handoff + 2.) * (double) sizeof(SM_frame);",
		/* the added margin of +2 is not really necessary */
	"#endif",
	"	#if NCORE>2",
	"	if (a_cycles)",
	"	{	fprintf(efd, \"warning: the intended nr of cores to be used in liveness mode is 2\\n\");",
	"		#ifndef SEP_STATE",
	"		fprintf(efd, \"warning: without -DSEP_STATE there is no guarantee that all liveness violations are found\\n\");",
	"		#endif",
	"	}",	/* it still works though, the later cores get states from the global q */
	"	#endif",
	"	#ifdef HAS_HIDDEN",
	"	#error cannot use hidden variables when compiling multi-core",
	"	#endif",
	"#endif",
	"#ifdef BITSTATE",
	"	if (hfns <= 0)",
	"	{	hfns = 1;",
	"		fprintf(efd, \"warning: using -k%%d as minimal usable value\\n\", hfns);",
	"	}",
	"#endif",
	"	omaxdepth = maxdepth;",
	"#ifdef BITSTATE",
	"	if (WS == 4 && ssize > 34)",	/* 32-bit word size */
	"	{	ssize = 34;",
	"		fprintf(efd, \"warning: using -w%%d as max usable value\\n\", ssize);",
	"/*",
	" *	-w35 would not work: 35-3 = 32 but 1^31 is the largest",
	" *	power of 2 that can be represented in an unsigned long",
	" */",
	"	}",
	"#else",
	"	if (WS == 4 && ssize > 27)",
	"	{	ssize = 27;",
	"		fprintf(efd, \"warning: using -w%%d as max usable value\\n\", ssize);",
	"/*",
	" *	for emalloc, the lookup table size multiplies by 4 for the pointers",
	" *	the largest power of 2 that can be represented in a ulong is 1^31",
	" *	hence the largest number of lookup table slots is 31-4 = 27",
	" */",
	"	}",

	"#endif",
	"#ifdef SC",
	"	hiwater = HHH = maxdepth-10;",
	"	DDD = HHH/2;",
	"	if (!stackfile)",
	"	{	stackfile = (char *) emalloc(strlen(PanSource)+4+1);",
	"		sprintf(stackfile, \"%%s._s_\", PanSource);",
	"	}",
	"	if (iterative)",
	"	{	fprintf(efd, \"error: cannot use -i or -I with -DSC\\n\");",
	"		pan_exit(1);",
	"	}",
	"#endif",

	"#if (defined(R_XPT) || defined(W_XPT)) && !defined(MA)",
	"	#warning -DR_XPT and -DW_XPT assume -DMA (ignored)",
	"#endif",

	"	if (iterative && a_cycles)",
	"	fprintf(efd, \"warning: -i or -I work for safety properties only\\n\");",

	"#ifdef BFS",
	"	#ifdef SC",
	"		#error -DBFS not compatible with -DSC",
	"	#endif",
	"	#ifdef HAS_LAST",
	"		#error -DBFS not compatible with _last",
	"	#endif",
	"	#ifdef HAS_STACK",
	"		#error cannot use c_track UnMatched with BFS",
	"	#endif",
	"	#ifdef BCS",
	"		#error -DBFS not compatible with -DBCS",
	"	#endif",
	"	#ifdef REACH",
	"		#warning -DREACH is redundant when -DBFS is used",
	"	#endif",
	"#endif",

	"#ifdef TRIX",
	"	#ifdef BITSTATE",
	"		#error cannot combine -DTRIX and -DBITSTATE",
	"	#endif",
	"	#ifdef COLLAPSE",
	"		#error cannot combine -DTRIX and -DCOLLAPSE",
	"	#endif",
	"	#ifdef MA",
	"		#error cannot combine -DTRIX and -DMA",
	"	#endif",
	"#endif",

	"#ifdef BCS",
	"	#ifdef P_RAND",
	"		#error cannot combine -DBCS and -DP_RAND",
	"	#endif",
	"	#ifdef BFS",
	"		#error cannot combine -DBCS and -DBFS",
	"	#endif",
	"#endif",

	"#if defined(MERGED) && defined(PEG)",
	"	#error to use -DPEG use: spin -o3 -a",
	"#endif",
	"#ifdef HC",
	"	#ifdef SFH", /* cannot happen -- undef-ed in this case */
	"		#error cannot combine -DHC and -DSFH",
	"		/* use of NOCOMP is the real reason */",
	"	#else",
	"		#ifdef NOCOMP",
	"		#error cannot combine -DHC and -DNOCOMP",
	"		#endif",
	"	#endif",
	"	#ifdef BITSTATE",
	"		#error cannot combine -DHC and -DBITSTATE",
	"	#endif",
	"#endif",
	"#if defined(SAFETY) && defined(NP)",
	"	#error cannot combine -DNP and -DBFS or -DSAFETY",
	"#endif",
	"#ifdef MA",
	"	#ifdef BITSTATE",
	"		#error cannot combine -DMA and -DBITSTATE",
	"	#endif",
	"	#if MA <= 0",
	"		#error usage: -DMA=N with N > 0 and N < VECTORSZ",
	"	#endif",
	"#endif",
	"#ifdef COLLAPSE",
	"	#ifdef BITSTATE",
	"		#error cannot combine -DBITSTATE and -DCOLLAPSE",
	"	#endif",
	"	#ifdef SFH",
	"		#error cannot combine -DCOLLAPSE and -DSFH",
	"		/* use of NOCOMP is the real reason */",
	"	#else",
	"		#ifdef NOCOMP",
	"		#error cannot combine -DCOLLAPSE and -DNOCOMP",
	"		#endif",
	"	#endif",
	"#endif",
	"	if (maxdepth <= 0 || ssize <= 1) 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\");",
	"	  pan_exit(1);",
	"	}",
	"#endif",
	"#if defined(REM_VARS) && !defined(NOREDUCE)",
	"	#warning p.o. reduction not compatible with remote varrefs (use -DNOREDUCE)",
	"#endif",
	"#if defined(NOCOMP) && !defined(BITSTATE)",
	"	if (a_cycles)",
	"	{ fprintf(efd, \"error: use of -DNOCOMP voids -l and -a\\n\");",
	"	  pan_exit(1);",
	"	}",
	"#endif",

	"#ifdef MEMLIM",
	"	memlim = ((double) MEMLIM) * (double) (1<<20);	/* size in Mbyte */",
	"#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)",
	"	{	fprintf(efd, \"error: no accept labels defined \");",
	"		fprintf(efd, \"in model (for option -a)\\n\");",
	"		usage(efd);",
	"	}",
	"	#endif",
	"#endif",
	"#ifndef NOREDUCE",
	"	#ifdef HAS_ENABLED",
	"		#error use of enabled() requires -DNOREDUCE",
	"	#endif",
	"	#ifdef HAS_PCVALUE",
	"		#error use of pcvalue() requires -DNOREDUCE",
	"	#endif",
	"	#ifdef HAS_BADELSE",
	"		#error use of 'else' combined with i/o stmnts requires -DNOREDUCE",
	"	#endif",
	"	#if defined(HAS_LAST) && !defined(BCS)",
	"		#error use of _last requires -DNOREDUCE",
	"	#endif",
	"#endif",

	"#if SYNC>0 && !defined(NOREDUCE)",
	"	#ifdef HAS_UNLESS",
	"	fprintf(efd, \"warning: use of a rendezvous stmnts in the escape\\n\");",
	"	fprintf(efd, \"\tof an unless clause, if present, could make p.o. reduction\\n\");",
	"	fprintf(efd, \"\tinvalid (use -DNOREDUCE to avoid this)\\n\");",
	"		#ifdef BFS",
	"		fprintf(efd, \"\t(this type of rv is also not compatible with -DBFS)\\n\");",
	"		#endif",
	"	#endif",
	"#endif",
	"#if SYNC>0 && defined(BFS)",
	"	#warning use of rendezvous with BFS does not preserve all invalid endstates",
	"#endif",
	"#if !defined(REACH) && !defined(BITSTATE)",
	"	if (iterative != 0 && a_cycles == 0)",
	"	{	fprintf(efd, \"warning: -i and -I need -DREACH to work accurately\\n\");",
	"	}",
	"#endif",
	"#if defined(BITSTATE) && defined(REACH)",
	"	#warning -DREACH is voided by -DBITSTATE",
	"#endif",
	"#if defined(MA) && defined(REACH)",
	"	#warning -DREACH is voided by -DMA",
	"#endif",
	"#if defined(FULLSTACK) && defined(CNTRSTACK)",
	"	#error cannot combine -DFULLSTACK and -DCNTRSTACK",
	"#endif",
	"#if defined(VERI)",
	"	#if ACCEPT_LAB>0",
	"		#ifndef BFS",
	"			if (!a_cycles",
	"			#ifdef HAS_CODE",
	"			&& !readtrail",
	"			#endif",
	"			#if NCORE>1",
	"			&& core_id == 0",
	"			#endif",
	"			&& !state_tables)",
	"			{ fprintf(efd, \"warning: never claim + accept labels \");",
	"			  fprintf(efd, \"requires -a flag to fully verify\\n\");",
	"			}",
	"		#else",
	"			if (!state_tables",
	"			#ifdef HAS_CODE",
	"			&& !readtrail",
	"			#endif",
	"			)",
	"			{ fprintf(efd, \"warning: verification in BFS mode \");",
	"			  fprintf(efd, \"is restricted to safety properties\\n\");",
	"			}",
	"		#endif",
	"	#endif",
	"#endif",
	"#ifndef SAFETY",
	"	if (!a_cycles",
	"	#ifdef HAS_CODE",
	"	&& !readtrail",
	"	#endif",
	"	#if NCORE>1",
	"	&& core_id == 0",
	"	#endif",
	"	&& !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);",
	"	set_masks();",
	"#ifdef BFS",
	"	trail = (Trail *) emalloc(6*sizeof(Trail));",
	"	trail += 3;",
	"#else",
	"	trail = (Trail *) emalloc((maxdepth+3)*sizeof(Trail));",
	"	trail++;	/* protect trpt-1 refs at depth 0 */",
	"#endif",
	"#ifdef SVDUMP",
	"	if (vprefix > 0)",
	"	{	char nm[64];",
	"		sprintf(nm, \"%%s.svd\", PanSource);",
	"		if ((svfd = creat(nm, TMODE)) < 0)",
	"		{	fprintf(efd, \"couldn't create %%s\\n\", nm);",
	"			vprefix = 0;",
	"	}	}",
	"#endif",
	"#ifdef RANDSTOR",
	"	srand(s_rand);",
	"#endif",
	"#if SYNC>0 && ASYNC==0",
	"	set_recvs();",
	"#endif",
	"	run();",
	"	done = 1;",
	"	wrapup();",
	"	return 0;",
	"}",	/* end of main() */
	"",
	"void",
	"usage(FILE *fd)",
	"{",
	"	fprintf(fd, \"%%s\\n\", SpinVersion);",
	"	fprintf(fd, \"Valid Options are:\\n\");",
	"#ifndef SAFETY",
		"#ifdef NP",
	"	fprintf(fd, \"\t-a  -> is disabled by -DNP \");",
	"	fprintf(fd, \"(-DNP compiles for -l only)\\n\");",
		"#else",
	"	fprintf(fd, \"\t-a  find acceptance cycles\\n\");",
		"#endif",
	"#else",
	"	fprintf(fd, \"\t-a,-l,-f  -> are disabled by -DSAFETY\\n\");",
	"#endif",
	"	fprintf(fd, \"\t-A  ignore assert() violations\\n\");",
	"	fprintf(fd, \"\t-b  consider it an error to exceed the depth-limit\\n\");",
	"	fprintf(fd, \"\t-cN stop at Nth error \");",
	"	fprintf(fd, \"(defaults to -c1)\\n\");",
	"	fprintf(fd, \"\t-D  print state tables in dot-format and stop\\n\");",
	"	fprintf(fd, \"\t-d  print state tables and stop\\n\");",
	"	fprintf(fd, \"\t-e  create trails for all errors\\n\");",
	"	fprintf(fd, \"\t-E  ignore invalid end states\\n\");",
	"#ifdef SC",
	"	fprintf(fd, \"\t-Ffile  use 'file' to store disk-stack\\n\");",
	"#endif",
	"#ifndef NOFAIR",
	"	fprintf(fd, \"\t-f  add weak fairness (to -a or -l)\\n\");",
	"#endif",
	"	fprintf(fd, \"\t-hN use different hash-seed N:1..32\\n\");",
	"	fprintf(fd, \"\t-i  search for shortest path to error\\n\");",
	"	fprintf(fd, \"\t-I  like -i, but approximate and faster\\n\");",
	"	fprintf(fd, \"\t-J  reverse eval order of nested unlesses\\n\");",
	"#ifdef BITSTATE",
	"	fprintf(fd, \"\t-kN set N bits per state (defaults to 3)\\n\");",
	"#endif",
	"#ifdef BCS",
	"	fprintf(fd, \"\t-LN set scheduling restriction to N (default 0)\\n\");",
	"#endif",
	"#ifndef SAFETY",
		"#ifdef NP",
	"	fprintf(fd, \"\t-l  find non-progress cycles\\n\");",
		"#else",
	"	fprintf(fd, \"\t-l  find non-progress cycles -> \");",
	"	fprintf(fd, \"disabled, requires \");",
	"	fprintf(fd, \"compilation with -DNP\\n\");",
		"#endif",
	"#endif",
	"#ifdef BITSTATE",
	"	fprintf(fd, \"\t-MN use N Megabytes for bitstate hash array\\n\");",
	"	fprintf(fd, \"\t-GN use N Gigabytes for bitstate hash array\\n\");",
	"#endif",
	"	fprintf(fd, \"\t-mN max depth N steps (default=10k)\\n\");",
	"#if NCLAIMS>1",
	"	fprintf(fd, \"\t-N cn -- use the claim named cn\\n\");",
	"	fprintf(fd, \"\t-Nn   -- use claim number n\\n\");",
	"#endif",
	"	fprintf(fd, \"\t-n  no listing of unreached states\\n\");",
	"#ifdef SVDUMP",
	"	fprintf(fd, \"\t-pN create svfile (save N bytes per state)\\n\");",
	"#endif",
	"	fprintf(fd, \"\t-QN set time-limit on execution of N minutes\\n\");",
	"	fprintf(fd, \"\t-q  require empty chans in valid end states\\n\");",
	"#ifdef HAS_CODE",
	"	fprintf(fd, \"\t-r  read and execute trail - can add -v,-n,-PN,-g,-C\\n\");",
	"	fprintf(fd, \"\t-rN read and execute N-th error trail\\n\");",
	"	fprintf(fd, \"\t-C  read and execute trail - columnated output (can add -v,-n)\\n\");",
	"	fprintf(fd, \"\t-PN read and execute trail - restrict trail output to proc N\\n\");",
	"	fprintf(fd, \"\t-g  read and execute trail + msc gui support\\n\");",
	"	fprintf(fd, \"\t-S  silent replay: only user defined printfs show\\n\");",
	"#endif",
	"#if defined(T_RAND) || defined(P_RAND) || defined(RANDSTOR)",
	"	fprintf(fd, \"\t-RSN use randomization seed N\\n\");",
	"#endif",
	"#ifdef BITSTATE",
	"	fprintf(fd, \"\t-RN repeat run Nx with N \");",
	"	fprintf(fd, \"[1..32] independent hash functions\\n\");",
	"	fprintf(fd, \"\t-s  same as -k1 (single bit per state)\\n\");",
	"#endif",
	"	fprintf(fd, \"\t-T  create trail files in read-only mode\\n\");",
	"	fprintf(fd, \"\t-tsuf replace .trail with .suf on trailfiles\\n\");",
	"	fprintf(fd, \"\t-V  print SPIN version number\\n\");",
	"	fprintf(fd, \"\t-v  verbose -- filenames in unreached state listing\\n\");",
	"	fprintf(fd, \"\t-wN hashtable of 2^N entries \");",
	"	fprintf(fd, \"(defaults to -w%%d)\\n\", ssize);",
	"	fprintf(fd, \"\t-x  do not overwrite an existing trail file\\n\");",
	"#if NCORE>1",
	"	fprintf(fd, \"\t-zN handoff states below depth N to 2nd cpu (multi_core)\\n\");",
	"#endif",
	"#ifdef HAS_CODE",
	"	fprintf(fd, \"\\n\toptions -r, -C, -PN, -g, and -S can optionally be followed by\\n\");",
	"	fprintf(fd, \"\ta filename argument, as in \'-r filename\', naming the trailfile\\n\");",
	"#endif",
	"#if NCORE>1",
	"	multi_usage(fd);",
	"#endif",
	"	exit(1);",
	"}",
	"",
	"char *",
	"Malloc(unsigned long n)",
	"{	char *tmp;",
	"#ifdef MEMLIM",
	"	if (memcnt + (double) n > memlim)",
	"	{	printf(\"pan: reached -DMEMLIM bound\\n\");",
	"		goto err;",
	"	}",
	"#endif",
	"	tmp = (char *) malloc(n);",
	"	if (!tmp)",
	"	{	printf(\"pan: out of memory\\n\");",
	"#ifdef MEMLIM",
	"err:",
	"		printf(\"\t%%g bytes used\\n\", memcnt);",
	"		printf(\"\t%%g bytes more needed\\n\", (double) n);",
	"		printf(\"\t%%g bytes limit\\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",
	"#if NCORE>1",
	"	#ifdef FULL_TRAIL",
	"		printf(\"  omit -DFULL_TRAIL or use pan -c0 to reduce memory\\n\");",
	"	#endif",
	"	#ifdef SEP_STATE",
	"		printf(\"hint: to reduce memory, recompile without\\n\");",
	"		printf(\"  -DSEP_STATE # may be faster, but uses more memory\\n\");",
	"	#endif",
	"#endif",
	"		wrapup();",
	"	}",
	"	memcnt += (double) n;",
	"	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 ((unsigned long) left < n)",	/* was: (left < (long)n) */
	"	{       grow = (n < CHUNK) ? CHUNK : n;",
#if 1
	"	        have = Malloc(grow);",
#else
	"		/* gcc's sbrk can give non-aligned result */",
	"		grow += sizeof(void *);	/* allow realignment */",
	"	        have = Malloc(grow);",
	"		if (((unsigned) have)&(sizeof(void *)-1))",
	"		{	have += (long) (sizeof(void *) ",
	"				- (((unsigned) have)&(sizeof(void *)-1)));",
	"			grow -= sizeof(void *);",
	"		}",
#endif
	"	        fragment += (double) left;",
	"	        left = grow;",
	"	}",
	"	tmp = have;",
	"	have += (long) n;",
	"	left -= (long) n;",
	"	memset(tmp, 0, n);",
	"	return tmp;",
	"}",

	"void",
	"Uerror(char *str)",
	"{	/* always fatal */",
	"	uerror(str);",
	"#if NCORE>1",
	"	sudden_stop(\"Uerror\");",
	"#endif",
	"	wrapup();",
	"}\n",
	"#if defined(MA) && !defined(SAFETY)",
	"int",
	"Unwind(void)",
	"{	Trans *t; uchar ot, _m; int tt; short II;",
	"#ifdef VERBOSE",
	"	int i;",
	"#endif",
	"	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(\"%%3ld: 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;	3.4.13 */",
	"	((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",
	"static char unwinding;",
	"void",
	"uerror(char *str)",
	"{	static char laststr[256];",
	"	int is_cycle;",
	"",
	"	if (unwinding) return; /* 1.4.2 */",
	"	if (strncmp(str, laststr, 254))",
	"#if NCORE>1",
	"	cpu_printf(\"pan:%%d: %%s (at depth %%ld)\\n\", errors+1, str,",
	"#else",
	"	printf(\"pan:%%d: %%s (at depth %%ld)\\n\", errors+1, str,",
	"#endif",
	"#if NCORE>1",
	"		(nr_handoffs * z_handoff) + ",
	"#endif",
	"		((depthfound==-1)?depth:depthfound));",
	"	strncpy(laststr, str, 254);",
	"	errors++;",
	"#ifdef HAS_CODE",
	"	if (readtrail) { wrap_trail(); return; }",
	"#endif",
	"	is_cycle = (strstr(str, \" cycle\") != (char *) 0);",
	"	if (!is_cycle)",
	"	{	depth++; trpt++;",	/* include failed step */
	"	}",
	"	if ((every_error != 0)",
	"	||  errors == upto)",
	"	{",
	"#if defined(MA) && !defined(SAFETY)",
	"		if (is_cycle)",
	"		{	int od = depth;",
	"			unwinding = 1;",
	"			depthfound = Unwind();",
	"			unwinding = 0;",
	"			depth = od;",
	"		}",
	"#endif",
	"#if NCORE>1",
	"		writing_trail = 1;",
	"#endif",
	"#ifdef BFS",
	"		if (depth > 1) trpt--;",
	"		nuerror(str);",
	"		if (depth > 1) trpt++;",
	"#else",
	"		putrail();",
	"#endif",
	"#if defined(MA) && !defined(SAFETY)",
	"		if (strstr(str, \" cycle\"))",
	"		{	if (every_error)",
	"			printf(\"sorry: MA writes 1 trail max\\n\");",
	"			wrapup(); /* no recovery from unwind */",
	"		}",
	"#endif",
	"#if NCORE>1",
	"		if (search_terminated != NULL)",
	"		{	*search_terminated |= 4; /* uerror */",
	"		}",
	"		writing_trail = 0;",
	"#endif",
	"	}",
	"	if (!is_cycle)",
	"	{	depth--; trpt--;	/* undo */",
	"	}",
	"#ifndef BFS",
	"	if (iterative != 0 && maxdepth > 0)",
	"	{	if (maxdepth > depth)",
	"		{	maxdepth = (iterative == 1)?(depth+1):(depth/2);",
	"		}",
	"		warned = 1;",
	"		printf(\"pan: reducing search depth to %%ld\\n\",",
	"			maxdepth);",
	"	} else",
	"#endif",
	"	if (errors >= upto && upto != 0)",
	"	{",
	"#if NCORE>1",
	"		sudden_stop(\"uerror\");",
	"#endif",
	"		wrapup();",
	"	}",
	"	depthfound = -1;",
	"}\n",
	"int",
	"xrefsrc(int lno, S_F_MAP *mp, int M, int i)",
	"{	Trans *T; int j, retval=1;",
	"	for (T = trans[M][i]; T; T = T->nxt)",
	"	if (T && T->tp)",
	"	{	if (strcmp(T->tp, \".(goto)\") == 0",
	"		||  strncmp(T->tp, \"goto :\", 6) == 0)",
	"			return 1; /* not reported */",
	"",
	"		for (j = 0; j < sizeof(mp); j++)",
	"			if (i >= mp[j].from && i <= mp[j].upto)",
	"			{	printf(\"\\t%%s:%%d\", mp[j].fnm, lno);",
	"				break;",
	"			}",
	"		if (j >= sizeof(mp))	/* fnm not found in list */",
	"		{	printf(\"\\t%%s:%%d\", PanSource, lno); /* use default */",
	"		}",
	"		printf(\", state %%d\", i);",
	"		if (strcmp(T->tp, \"\") != 0)",
	"		{	char *q;",
	"			q = transmognify(T->tp);",
	"			printf(\", \\\"%%s\\\"\", q?q:\"\");",
	"		} else if (stopstate[M][i])",
	"			printf(\", -end state-\");",
	"		printf(\"\\n\");",
	"		retval = 0; /* reported */",
	"	}",
	"	return retval;",
	"}\n",
	"void",
	"r_ck(uchar *which, int N, int M, short *src, S_F_MAP *mp)",
	"{	int i, m=0;",
	"",
	"	if ((enum btypes) Btypes[M] == N_CLAIM",
	"	&& claimname != NULL && strcmp(claimname, procname[M]) != 0)",
	"	{	return;",
	"	}",
	"",
	"	switch ((enum btypes) Btypes[M]) {",
	"	case P_PROC:",
	"	case A_PROC:",
	"		printf(\"unreached in proctype %%s\\n\", procname[M]);",
	"		break;",
	"	case I_PROC:",
	"		printf(\"unreached in init\\n\");",
	"		break;",
	"	case E_TRACE:",
	"	case N_TRACE:",
	"	case N_CLAIM:",
	"	default:",
	"		printf(\"unreached in claim %%s\\n\", procname[M]);",
	"		break;",
	"	}",
	"	for (i = 1; i < N; i++)",
	"	{	if (which[i] == 0",
	"		&&  (mapstate[M][i] == 0",
	"		||   which[mapstate[M][i]] == 0))",
	"		{	m += xrefsrc((int) src[i], mp, M, i);",
	"		} else",
	"		{	m++;",
	"	}	}",
	"	printf(\"\t(%%d of %%d states)\\n\", N-1-m, N-1);",
	"}",
	"#if NCORE>1 && !defined(SEP_STATE)",
	"static long rev_trail_cnt;",
	"",
	"#ifdef FULL_TRAIL",
	"void",
	"rev_trail(int fd, volatile Stack_Tree *st_tr)",
	"{	long j; char snap[64];",
	"",
	"	if (!st_tr)",
	"	{	return;",
	"	}",
	"	rev_trail(fd, st_tr->prv);",
	"#ifdef VERBOSE",
	"	printf(\"%%d (%%d) LRT [%%d,%%d] -- %%9u (root %%9u)\\n\",",
	"		depth, rev_trail_cnt, st_tr->pr, st_tr->t_id, st_tr, stack_last[core_id]);",
	"#endif",
	"	if (st_tr->pr != 255)", /* still needed? */
	"	{	sprintf(snap, \"%%ld:%%d:%%d\\n\", ",
	"			rev_trail_cnt++, st_tr->pr, st_tr->t_id);",
	"		j = strlen(snap);",
	"		if (write(fd, snap, j) != j)",
	"		{	printf(\"pan: error writing trailfile\\n\");",
	"			close(fd);",
	"			wrapup();",
	"			return;",
	"		}",
	"	} else  /* handoff point */",
	"	{	if (a_cycles)",
	"		{	(void) write(fd, \"-1:-1:-1\\n\", 9);",
	"	}	}",
	"}",
	"#endif", /* FULL_TRAIL */
	"#endif", /* NCORE>1 */
	"",
	"void",
	"putrail(void)",
	"{	int fd;",
	"#if defined VERI || defined(MERGED)",
	"	char snap[64];",
	"#endif",
	"#if NCORE==1 || defined(SEP_STATE) || !defined(FULL_TRAIL)",
	"	long i, j;",
	"	Trail *trl;",
	"#endif",
	"	fd = make_trail();",
	"	if (fd < 0) return;",
	"#ifdef VERI",
	"	sprintf(snap, \"-2:%%d:-2\\n\", (uchar) ((P0 *)pptr(0))->_t);",
	"	if (write(fd, snap, strlen(snap)) < 0) return;",
	"#endif",
	"#ifdef MERGED",
	"	sprintf(snap, \"-4:-4:-4\\n\");",
	"	if (write(fd, snap, strlen(snap)) < 0) return;",
	"#endif",
	"#if NCORE>1 && !defined(SEP_STATE) && defined(FULL_TRAIL)",
	"	rev_trail_cnt = 1;",
	"	enter_critical(GLOBAL_LOCK);",
	"	 rev_trail(fd, stack_last[core_id]);",
	"	leave_critical(GLOBAL_LOCK);",
	"#else",
	"	i = 1; /* trail starts at position 1 */",
	"	#if NCORE>1 && defined(SEP_STATE)",
	"	if (cur_Root.m_vsize > 0) { i++; depth++; }",
	"	#endif",
	"	for ( ; i <= depth; i++)",
	"	{	if (i == depthfound+1)",
	"		{	if (write(fd, \"-1:-1:-1\\n\", 9) != 9)",
	"			{	goto notgood;",
	"		}	}",
	"		trl = getframe(i);",
	"		if (!trl->o_t) continue;",
	"		if (trl->o_pm&128) continue;",
	"		sprintf(snap, \"%%ld:%%d:%%d\\n\", ",
	"			i, trl->pr, trl->o_t->t_id);",
	"		j = strlen(snap);",
	"		if (write(fd, snap, j) != j)",
	"		{",
	"notgood:		printf(\"pan: error writing trailfile\\n\");",
	"			close(fd);",
	"			wrapup();",
	"	}	}",
	"#endif",
	"	close(fd);",
	"#if NCORE>1",
	"	cpu_printf(\"pan: wrote trailfile\\n\");",
	"#endif",
	"}\n",
	"void",
	"sv_save(void)	/* 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",
	"#ifdef TRIX",
	"	sv_populate();",
	"#endif",
	"	svtack->o_delta = vsize; /* don't compress */",
	"	memcpy((char *)(svtack->body), (char *) &now, vsize);",
	"#if defined(C_States) && defined(HAS_STACK) && (HAS_TRACK==1)",
	"	c_stack((uchar *) &(svtack->c_stack[0]));",
	"#endif",
	"#ifdef DEBUG",
	"	cpu_printf(\"%%d:	sv_save\\n\", depth);",
	"#endif",
	"}\n",
	"void",
	"sv_restor(void)	/* pop state vector from save stack */",
	"{",
	"	memcpy((char *)&now, svtack->body, svtack->o_delta);",
	"#if SYNC",
	"	boq = svtack->o_boq;",
	"#endif",
	"#ifdef TRIX",
	"	re_populate();",
	"#endif",
	"#if defined(C_States) && (HAS_TRACK==1)",
	"#ifdef HAS_STACK",
	"	c_unstack((uchar *) &(svtack->c_stack[0]));",
	"#endif",
	"	c_revert((uchar *) &(now.c_state[0]));",
	"#endif",

	"	if (vsize != svtack->o_delta)",
	"		Uerror(\"sv_restor\");",
	"	if (!svtack->lst)",
	"		Uerror(\"error: sv_restor\");",
	"	svtack  = svtack->lst;",
	"#ifdef DEBUG",
	"	cpu_printf(\"	sv_restor\\n\");",
	"#endif",
	"}\n",
	"void",
	"p_restor(int h)",
	"{	int i;",
	"	char *z = (char *) &now;\n",
	"#ifndef TRIX",
	"	proc_offset[h] = stack->o_offset;",
	"	proc_skip[h]   = (uchar) stack->o_skip;",
	"#else",
	"	char *oi;",
	"	#ifdef V_TRIX",
	"		printf(\"%%4d: p_restor %%d\\n\", depth, h);",
	"	#endif",
	"#endif",
	"#ifndef XUSAFE",
	"	p_name[h] = stack->o_name;",
	"#endif",
	"#ifdef TRIX",
	"	vsize += sizeof(char *);",
	"	#ifndef BFS",
	"		if (processes[h] != NULL || freebodies == NULL)",
	"		{	Uerror(\"processes error\");",
	"		}",
	"		processes[h] = freebodies;",
	"		freebodies = freebodies->nxt;",
	"		processes[h]->nxt = (TRIX_v6 *) 0;",
	"		processes[h]->modified = 1;	/* p_restor */",
	"	#endif",
	"	processes[h]->parent_pid = stack->parent;",
	"	processes[h]->psize = stack->o_delta;",
	"	memcpy((char *)pptr(h), stack->b_ptr, stack->o_delta);",
	"	oi = stack->b_ptr;",
	"#else",
	"	#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 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;",
	"#endif",
	"	now._nr_pr += 1;",
	"#ifndef NOVSZ",
	"	now._vsz = vsize;",
	"#endif",
	"	i = stack->o_delqs;",
	"	if (!stack->lst)",
	"		Uerror(\"error: p_restor\");",
	"	stack = stack->lst;",
	"	this = pptr(h);",
	"	while (i-- > 0)",
	"		q_restor();",
	"#ifdef TRIX",
	"	re_mark_all(1);	/* p_restor - all chans move up in _ids_ */",
	"	now._ids_[h] = oi; /* restor the original contents */",
	"#endif",
	"}\n",
	"void",
	"q_restor(void)",
	"{	int h = now._nr_qs;",
	"#ifdef TRIX",
	"	#ifdef V_TRIX",
	"		printf(\"%%4d: q_restor %%d\\n\", depth, h);",
	"	#endif",
	"	vsize += sizeof(char *);",
	"	#ifndef BFS",
	"		if (channels[h] != NULL || freebodies == NULL)",
	"		{	Uerror(\"channels error\");",
	"		}",
	"		channels[h] = freebodies;",
	"		freebodies = freebodies->nxt;",
	"		channels[h]->nxt = (TRIX_v6 *) 0;",
	"		channels[h]->modified = 1;	/* q_restor */",
	"	#endif",
	"	channels[h]->parent_pid = stack->parent;",
	"	channels[h]->psize = stack->o_delta;",
	"	memcpy((char *)qptr(h), stack->b_ptr, stack->o_delta);",
	"	now._ids_[now._nr_pr + h] = stack->b_ptr;",
	"#else",
	"	char *z = (char *) &now;",
	"	#ifndef NOCOMP",
	"		int k, k_end;",
	"	#endif",
	"	q_offset[h] = stack->o_offset;",
	"	q_skip[h]   = (uchar) stack->o_skip;",
	"	vsize += stack->o_skip;",
	"	memcpy(z+vsize, stack->body, stack->o_delta);",
	"	vsize += stack->o_delta;",
	"#endif",
	"#ifndef XUSAFE",
	"	q_name[h] = stack->o_name;",
	"#endif",
	"#ifndef NOVSZ",
	"	now._vsz = vsize;",
	"#endif",
	"	now._nr_qs += 1;",
	"#ifndef NOCOMP",
	"#ifndef TRIX",
	"	k_end = stack->o_offset;",
	"	k = k_end - stack->o_skip;",
	"	#if SYNC",
	"	#ifndef BFS",
	"		if (q_zero(now._nr_qs)) k_end += stack->o_delta;",
	"	#endif",
	"	#endif",
	"	for ( ; k < k_end; k++)",
	"		Mask[k] = 1;",
	"#endif",
	"#endif",
	"	if (!stack->lst)",
	"		Uerror(\"error: q_restor\");",
	"	stack = stack->lst;",
	"}",

	"typedef struct IntChunks {",
	"	int	*ptr;",
	"	struct	IntChunks *nxt;",
	"} IntChunks;",
	"IntChunks *filled_chunks[512];",
	"IntChunks *empty_chunks[512];",

	"int *",
	"grab_ints(int nr)",
	"{	IntChunks *z;",
	"	if (nr >= 512) 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;",
	"}",
	"int",
	"delproc(int sav, int h)",
	"{	int d, i=0;",
	"#ifndef NOCOMP",
	"	int o_vsize = vsize;",
	"#endif",
	"	if (h+1 != (int) now._nr_pr)",
	"	{	return 0;",
	"	}",
	"#ifdef TRIX",
	"	#ifdef V_TRIX",
	"		printf(\"%%4d: delproc %%d -- parent %%d\\n\", depth, h, processes[h]->parent_pid);",
	"		if (now._nr_qs > 0)",
	"		printf(\"	top channel: %%d -- parent %%d\\n\", now._nr_qs-1, channels[now._nr_qs-1]->parent_pid);",
	"	#endif",
	"	while (now._nr_qs > 0",
	"	&&     channels[now._nr_qs-1]->parent_pid == processes[h]->parent_pid)",
	"	{	delq(sav);",
	"		i++;",
	"	}",
	"	d = processes[h]->psize;",
	"	if (sav)",
	"	{	if (!stack->nxt)",
	"		{	stack->nxt = (_Stack *) emalloc(sizeof(_Stack));",
	"			stack->nxt->lst = stack;",
	"			smax++;",
	"		}",
	"		stack = stack->nxt;",
	"	#ifndef XUSAFE",
	"		stack->o_name   = p_name[h];",
	"	#endif",
	"		stack->parent   = processes[h]->parent_pid;",
	"		stack->o_delta  = d;",
	"		stack->o_delqs  = i;",
	"		stack->b_ptr = now._ids_[h];", /* new 6.1 */
	"	}",
	"	memset((char *)pptr(h), 0, d);",
	"	#ifndef BFS",
	"		processes[h]->nxt = freebodies;",
	"		freebodies = processes[h];",
	"		processes[h] = (TRIX_v6 *) 0;",
	"	#endif",
	"	vsize -= sizeof(char *);",
	"	now._nr_pr -= 1;",
	"	re_mark_all(-1); /* delproc - all chans move down in _ids_ */",
	"#else",
	"	while (now._nr_qs",
	"	&&     q_offset[now._nr_qs-1] > proc_offset[h])",
	"	{	delq(sav);",
	"		i++;",
	"	}",
	"	d = vsize - proc_offset[h];",
	"	if (sav)",
	"	{	if (!stack->nxt)",
	"		{	stack->nxt = (_Stack *) emalloc(sizeof(_Stack));",
	"			stack->nxt->body = emalloc(Maxbody * sizeof(char));",
	"			stack->nxt->lst = stack;",
	"			smax++;",
	"		}",
	"		stack = stack->nxt;",
	"		stack->o_offset = proc_offset[h];",
	"	#if VECTORSZ>32000",
	"		stack->o_skip   = (int) proc_skip[h];",
	"	#else",
	"		stack->o_skip   = (short) proc_skip[h];",
	"	#endif",
	"	#ifndef XUSAFE",
	"		stack->o_name   = p_name[h];",
	"	#endif",
	"		stack->o_delta  = d;",
	"		stack->o_delqs  = i;",
	"		memcpy(stack->body, (char *)pptr(h), d);",
	"	}",
	"	vsize = proc_offset[h];",
	"	now._nr_pr -= 1;",
	"	memset((char *)pptr(h), 0, d);",
	"	vsize -= (int) proc_skip[h];",
	"	#ifndef NOCOMP",
	"	for (i = vsize; i < o_vsize; i++)",
	"		Mask[i] = 0; /* reset */",
	"	#endif",
	"#endif",
	"#ifndef NOVSZ",
	"	now._vsz = vsize;",
	"#endif",
	"	return 1;",
	"}\n",
	"void",
	"delq(int sav)",
	"{	int h = now._nr_qs - 1;",
	"#ifdef TRIX",
	"	int d = channels[now._nr_qs - 1]->psize;",
	"#else",
	"	int d = vsize - q_offset[now._nr_qs - 1];",
	"#endif",
	"#ifndef NOCOMP",
	"	int k, o_vsize = vsize;",
	"#endif",
	"	if (sav)",
	"	{	if (!stack->nxt)",
	"		{	stack->nxt = (_Stack *) emalloc(sizeof(_Stack));",
	"#ifndef TRIX",
	"			stack->nxt->body = emalloc(Maxbody * sizeof(char));",
	"#endif",
	"			stack->nxt->lst = stack;",
	"			smax++;",
	"		}",
	"		stack = stack->nxt;",
	"#ifdef TRIX",
	"		stack->parent = channels[h]->parent_pid;",
	"		stack->b_ptr = now._ids_[h];", /* new 6.1 */
	"#else",
	"		stack->o_offset = q_offset[h];",
	"	#if VECTORSZ>32000",
	"		stack->o_skip   = (int) q_skip[h];",
	"	#else",
	"		stack->o_skip   = (short) q_skip[h];",
	"	#endif",
	"#endif",
	"	#ifndef XUSAFE",
	"		stack->o_name   = q_name[h];",
	"	#endif",
	"		stack->o_delta  = d;",
	"#ifndef TRIX",
	"		memcpy(stack->body, (char *)qptr(h), d);",
	"#endif",
	"	}",
	"#ifdef TRIX",
	"	vsize -= sizeof(char *);",
	"	#ifdef V_TRIX",
	"		printf(\"%%4d: delq %%d parent %%d\\n\", depth, h, channels[h]->parent_pid);",
	"	#endif",
	"#else",
	"	vsize = q_offset[h];",
	"	vsize -= (int) q_skip[h];",
	"	#ifndef NOCOMP",
	"		for (k = vsize; k < o_vsize; k++)",
	"			Mask[k] = 0; /* reset */",
	"	#endif",
	"#endif",
	"	now._nr_qs -= 1;",
	"	memset((char *)qptr(h), 0, d);",
	"#ifdef TRIX",
	"	#ifndef BFS",
	"		channels[h]->nxt = freebodies;",
	"		freebodies = channels[h];",
	"		channels[h] = (TRIX_v6 *) 0;",
	"	#endif",
	"#endif",
	"#ifndef NOVSZ",
	"	now._vsz = vsize;",
	"#endif",
	"}\n",
	"int",
	"qs_empty(void)",
	"{	int i;",
	"	for (i = 0; i < (int) now._nr_qs; i++)",
	"	{	if (q_sz(i) > 0)",
	"			return 0;",
	"	}",
	"	return 1;",
	"}\n",
	"int",
	"endstate(void)",
	"{	int i; P0 *ptr;",
	"	for (i = BASE; i < (int) now._nr_pr; i++)",
	"	{	ptr = (P0 *) pptr(i);",
	"		if (!stopstate[ptr->_t][ptr->_p])",
	"			return 0;",
	"	}",
	"	if (strict) return qs_empty();",
	"#if defined(EVENT_TRACE) && !defined(OTIM)",
	"	if (!stopstate[EVENT_TRACE][now._event] && !a_cycles)",
	"	{	printf(\"pan: event_trace not completed\\n\");",
	"		return 0;",
	"	}",
	"#endif",
	"	return 1;",
	"}\n",
	"#ifndef SAFETY",
	"void",
	"checkcycles(void)",
	"{	uchar o_a_t = now._a_t;",
	"#ifndef NOFAIR",
	"	uchar o_cnt = now._cnt[1];",
	"#endif",
		"#ifdef FULLSTACK",
		"#ifndef MA",
	"	struct H_el *sv = trpt->ostate; /* save */",
		"#else",
	"	uchar prov = trpt->proviso; /* save */",
		"#endif",
		"#endif",
		"#ifdef DEBUG",
	"	{ int i; uchar *v = (uchar *) &now;",
	"	  printf(\"	set Seed state \");",
	"#ifndef NOFAIR",
	"	  if (fairness) printf(\"(cnt = %%d:%%d, nrpr=%%d) \",",
	"		now._cnt[0], now._cnt[1], now._nr_pr);",
	"#endif",
	"	/* for (i = 0; i < n; i++) printf(\"%%d,\", v[i]);	*/",
	"	  printf(\"\\n\");",
	"	}",
	"	printf(\"%%ld: 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;",

	"#if NCORE>1",
	"	mem_put_acc();", /* handoff accept states */
	"#else",
	"	new_state();	/* start 2nd DFS */",
	"#endif",

	"	now._a_t = o_a_t;",
	"#ifndef NOFAIR",
	"	now._cnt[1] = o_cnt;",
	"#endif",
	"	A_depth = 0; depthfound = -1;",
		"#ifdef DEBUG",
	"	printf(\"%%ld: cycle check returns\\n\", depth);",
		"#endif",
		"#ifdef FULLSTACK",
		"#ifndef MA",
	"	trpt->ostate = sv;	/* restore */",
		"#else",
	"	trpt->proviso = prov;",
		"#endif",
		"#endif",
	"}",
	"#endif\n",
	"#if defined(FULLSTACK) && defined(BITSTATE)",
	"struct H_el *Free_list = (struct H_el *) 0;",
	"void",
	"onstack_init(void)	/* to store stack states in a bitstate search */",
	"{	S_Tab = (struct H_el **) emalloc(maxdepth*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 && ((int) v->tagged >= n); v=v->nxt)",
	"		{	if ((int) v->tagged == n)",
	"			{	if (last)",
	"					last->nxt = v->nxt;",
	"				else",
	"gotcha:				Free_list = v->nxt;",
	"				v->tagged = 0;",
	"				v->nxt = 0;",
		"#ifdef COLLAPSE",
	"				v->ln = 0;",
		"#endif",
	"				return v;",
	"			}",
	"			Fh++; last=v;",
	"		}",
	"		/* new: second try */",
	"		v = Free_list;", /* try to avoid emalloc */
	"		if (v && ((int) v->tagged >= n))",
	"			goto gotcha;",
	"		ngrabs++;",
	"	}",
	"	return (struct H_el *)",
	"	      emalloc(sizeof(struct H_el)+n-sizeof(unsigned));",
	"}\n",
	"#else",

	"#if NCORE>1",
	"struct H_el *",
	"grab_state(int n)",
	"{	struct H_el *grab_shared(int);",
	"	return grab_shared(sizeof(struct H_el)+n-sizeof(unsigned));",
	"}",
	"#else",
	" #ifndef AUTO_RESIZE",
	"  #define grab_state(n) (struct H_el *) \\",
	"		emalloc(sizeof(struct H_el)+n-sizeof(unsigned long));",
	" #else",
	"  struct H_el *",
	"  grab_state(int n)",
	"  {	struct H_el *p;",
	"	int cnt = sizeof(struct H_el)+n-sizeof(unsigned long);",
	"",
	"	if (reclaim_size >= cnt+WS)",
	"	{	if ((cnt & (WS-1)) != 0) /* alignment */",
	"		{	cnt += WS - (cnt & (WS-1));",
	"		}",
	"		p = (struct H_el *) reclaim_mem;",
	"		reclaim_mem  += cnt;",
	"		reclaim_size -= cnt;",
	"		memset(p, 0, cnt);",
	"	} else",
	"	{	p = (struct H_el *) emalloc(cnt);",
	"	}",
	"	return p;",
	"  }",
	" #endif",
	"#endif",

	"#endif",
"#ifdef COLLAPSE",
	"unsigned long",
	"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);",

	"#if NCORE>1 && !defined(SEP_STATE)",
	"	enter_critical(CS_ID);	/* uses spinlock - 1..128 */",
	"#endif",
	"	tmp = H_tab[j1_spin];",
	"	if (!tmp)",
	"	{	tmp = grab_state(n);",
	"		H_tab[j1_spin] = tmp;",
	"	} else",
	"	for ( ;; olst = tmp, tmp = tmp->nxt)",
	"	{	if (n == tmp->ln)",
	"		{	m = memcmp(((char *)&(tmp->state)), v, n);",
	"			if (m == 0)",
	"				goto done;",
	"			if (m < 0)",
	"			{",
	"Insert:			ntmp = grab_state(n);",
	"				ntmp->nxt = tmp;",
	"				if (!olst)",
	"					H_tab[j1_spin] = 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;",
	"	}",
	"#if NCORE>1 && !defined(SEP_STATE)",
	"	enter_critical(GLOBAL_LOCK);",
	"#endif",
	"	m = ++ncomps[tp];",
	"#if NCORE>1 && !defined(SEP_STATE)",
	"	leave_critical(GLOBAL_LOCK);",
	"#endif",
	"#ifdef FULLSTACK",
	"	tmp->tagged = m;",
	"#else",
	"	tmp->st_id  = m;",
	"#endif",
	"#if defined(AUTO_RESIZE) && !defined(BITSTATE)",
	"	tmp->m_K1 = K1;",
	"#endif",
	"	memcpy(((char *)&(tmp->state)), v, n);",
	"	tmp->ln = n;",
	"done:",

	"#if NCORE>1 && !defined(SEP_STATE)",
	"	leave_critical(CS_ID);	/* uses spinlock */",
	"#endif",

	"#ifdef FULLSTACK",
	"	return tmp->tagged;",
	"#else",
	"	return tmp->st_id;",
	"#endif",
	"}",
	"",
	"int",
	"compress(char *vin, int nin)	/* collapse compression */",
	"{	char	*w, *v = (char *) &comp_now;",
	"	int	i, j;",
	"	unsigned long	n;",
	"	static char	*x;",
	"	static uchar	nbytes[513]; /* 1 + 256 + 256 */",
	"	static unsigned	short nbytelen;",
	"	long col_q(int, char *);",
	"	long col_p(int, char *);",
	"#ifndef SAFETY",
	"	if (a_cycles)",
	"		*v++ = now._a_t;",
		"#ifndef NOFAIR",
	"	if (fairness)",
	"	for (i = 0; i < NFAIR; i++)",
	"		*v++ = now._cnt[i];",
		"#endif",
	"#endif",
	"	nbytelen = 0;",

	"#ifndef JOINPROCS",
	"	for (i = 0; i < (int) now._nr_pr; i++)",
	"	{	n = col_p(i, (char *) 0);",
	"#ifdef NOFIX",
	"		nbytes[nbytelen] = 0;",
	"#else",
	"		nbytes[nbytelen] = 1;",
	"		*v++ = ((P0 *) pptr(i))->_t;",
	"#endif",
	"		*v++ = n&255;",
	"		if (n >= (1<<8))",
	"		{	nbytes[nbytelen]++;",
	"			*v++ = (n>>8)&255;",
	"		}",
	"		if (n >= (1<<16))",
	"		{	nbytes[nbytelen]++;",
	"			*v++ = (n>>16)&255;",
	"		}",
	"		if (n >= (1<<24))",
	"		{	nbytes[nbytelen]++;",
	"			*v++ = (n>>24)&255;",
	"		}",
	"		nbytelen++;",
	"	}",
	"#else",
	"	x = scratch;",
	"	for (i = 0; i < (int) now._nr_pr; i++)",
	"		x += col_p(i, x);",
	"	n = ordinal(scratch, x-scratch, 2); /* procs */",
	"	*v++ = n&255;",
	"	nbytes[nbytelen] = 0;",
	"	if (n >= (1<<8))",
	"	{	nbytes[nbytelen]++;",
	"		*v++ = (n>>8)&255;",
	"	}",
	"	if (n >= (1<<16))",
	"	{	nbytes[nbytelen]++;",
	"		*v++ = (n>>16)&255;",
	"	}",
	"	if (n >= (1<<24))",
	"	{	nbytes[nbytelen]++;",
	"		*v++ = (n>>24)&255;",
	"	}",
	"	nbytelen++;",
	"#endif",
	"#ifdef SEPQS",
	"	for (i = 0; i < (int) now._nr_qs; i++)",
	"	{	n = col_q(i, (char *) 0);",
	"		nbytes[nbytelen] = 0;",
	"		*v++ = n&255;",
	"		if (n >= (1<<8))",
	"		{	nbytes[nbytelen]++;",
	"			*v++ = (n>>8)&255;",
	"		}",
	"		if (n >= (1<<16))",
	"		{	nbytes[nbytelen]++;",
	"			*v++ = (n>>16)&255;",
	"		}",
	"		if (n >= (1<<24))",
	"		{	nbytes[nbytelen]++;",
	"			*v++ = (n>>24)&255;",
	"		}",
	"		nbytelen++;",
	"	}",
	"#endif",

	"#ifdef NOVSZ",
	"	/* 3 = _a_t, _nr_pr, _nr_qs */",
	"	w = (char *) &now + 3 * sizeof(uchar);",
		"#ifndef NOFAIR",
		"	w += NFAIR;",
		"#endif",
	"#else",
		"#if VECTORSZ<65536",
		"	w = (char *) &(now._vsz) + sizeof(unsigned short);",
		"#else",
		"	w = (char *) &(now._vsz) + sizeof(unsigned long);",
		"#endif",
	"#endif",
	"	x = scratch;",
	"	*x++ = now._nr_pr;",
	"	*x++ = now._nr_qs;",

	"	if (now._nr_qs > 0 && qptr(0) < pptr(0))",
	"		n = qptr(0) - (uchar *) w;",
	"	else",
	"		n = pptr(0) - (uchar *) w;",
	"	j = w - (char *) &now;",
	"	for (i = 0; i < (int) n; i++, w++)",
	"		if (!Mask[j++]) *x++ = *w;",
	"#ifndef SEPQS",
	"	for (i = 0; i < (int) now._nr_qs; i++)",
	"		x += col_q(i, x);",
	"#endif",

	"	x--;",
	"	for (i = 0, j = 6; i < nbytelen; i++)",
	"	{	if (j == 6)",
	"		{	j = 0;",
	"			*(++x) = 0;",
	"		} else",
	"			j += 2;",
	"		*x |= (nbytes[i] << j);",
	"	}",
	"	x++;",
	"	for (j = 0; j < WS-1; j++)",
	"		*x++ = 0;",
	"	x -= j; j = 0;",
	"	n = ordinal(scratch, x-scratch, 0); /* globals */",
	"	*v++ = n&255;",
	"	if (n >= (1<< 8)) { *v++ = (n>> 8)&255; j++; }",
	"	if (n >= (1<<16)) { *v++ = (n>>16)&255; j++; }",
	"	if (n >= (1<<24)) { *v++ = (n>>24)&255; j++; }",
	"	*v++ = j;	/* add last count as a byte */",

	"	for (i = 0; i < WS-1; i++)",
	"		*v++ = 0;",
	"	v -= i;",
	"#if 0",
	"	printf(\"collapse %%d -> %%d\\n\",",
	"		vsize, v - (char *)&comp_now);",
	"#endif",
	"	return v - (char *)&comp_now;",
	"}",

"#else",
"#if !defined(NOCOMP)",
	"int",
	"compress(char *vin, int n)	/* default compression */",
	"{",
	"#ifdef HC",
	"	int delta = 0;",
	"	s_hash((uchar *)vin, n); /* sets K1 and K2 */",
		"#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 *) &K1, WS);",
	"	delta += WS;",
		"#if HC>0",
	"	memcpy((char *) &comp_now + delta, (char *) &K2, HC);",
	"	delta += HC;",
		"#endif",
	"	return delta;",
	"#else",
	"	char *vv = vin;",
	"	char *v = (char *) &comp_now;",
	"	int i;",
	"  #ifndef NO_FAST_C", /* disable faster compress */
	"	int r = 0, unroll = n/8;", /* most sv are much longer */
	"	if (unroll > 0)",
	"	{	i = 0;",
	"		while (r++ < unroll)",
	"		{	/* unroll 8 times, avoid ifs */",
	"	/* 1 */		*v = *vv++; v += 1 - Mask[i++];",
	"	/* 2 */		*v = *vv++; v += 1 - Mask[i++];",
	"	/* 3 */		*v = *vv++; v += 1 - Mask[i++];",
	"	/* 4 */		*v = *vv++; v += 1 - Mask[i++];",
	"	/* 5 */		*v = *vv++; v += 1 - Mask[i++];",
	"	/* 6 */		*v = *vv++; v += 1 - Mask[i++];",
	"	/* 7 */		*v = *vv++; v += 1 - Mask[i++];",
	"	/* 8 */		*v = *vv++; v += 1 - Mask[i++];",
	"		}",
	"		r = n - i; /* the rest, at most 7 */",
	"		switch (r) {",
	"		case 7: *v = *vv++; v += 1 - Mask[i++];",
	"		case 6: *v = *vv++; v += 1 - Mask[i++];",
	"		case 5: *v = *vv++; v += 1 - Mask[i++];",
	"		case 4: *v = *vv++; v += 1 - Mask[i++];",
	"		case 3: *v = *vv++; v += 1 - Mask[i++];",
	"		case 2: *v = *vv++; v += 1 - Mask[i++];",
	"		case 1: *v = *vv++; v += 1 - Mask[i++];",
	"		case 0: break;",
	"		}",
	"#if 1",
	"		n = i = v - (char *)&comp_now; /* bytes written so far */",
	"#endif",
	"		r = (n+WS-1)/WS; /* in words, rounded up */",
	"		r *= WS;	 /* total bytes to fill  */",
	"		i = r - i;	 /* remaining bytes      */",
	"		switch (i) {",   /* fill word */
	"		case 7: *v++ = 0;    /* fall thru */",
	"		case 6: *v++ = 0;",
	"		case 5: *v++ = 0;",
	"		case 4: *v++ = 0;",
	"		case 3: *v++ = 0;",
	"		case 2: *v++ = 0;",
	"		case 1: *v++ = 0;",
	"		case 0: break;",
	"		default: Uerror(\"unexpected wordsize\");",
	"		}",
	"		v -= i;",
	"	} else",
	"  #endif",
	"	{	for (i = 0; i < n; i++, vv++)",
	"			if (!Mask[i]) *v++ = *vv;",
	"		for (i = 0; i < WS-1; i++)",
	"			*v++ = 0;",
	"		v -= i;",
	"	}",
		"#if 0",
	"	printf(\"compress %%d -> %%d\\n\",",
	"		n, v - (char *)&comp_now);",
		"#endif",
	"	return v - (char *)&comp_now;",
	"#endif",
	"}",
"#endif",
"#endif",
	"#if defined(FULLSTACK) && defined(BITSTATE)",
"#if defined(MA)",
	"#if !defined(onstack_now)",
	"int  onstack_now(void) {}", /* to suppress compiler errors */
	"#endif",
	"#if !defined(onstack_put)",
	"void onstack_put(void) {}", /* for this invalid combination */
	"#endif",
	"#if !defined(onstack_zap)",
	"void onstack_zap(void) {}", /* of directives */
	"#endif",
"#else",
	"void",
	"onstack_zap(void)",
	"{	struct H_el *v, *w, *last = 0;",
	"	struct H_el **tmp = H_tab;",
	"	char *nv; int n, m;",
	"	static char warned = 0;",
	"#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
	"	uchar was_last = now._last;",
	"	now._last = 0;",
	"#endif",
	"",
	"	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))",
	"	s_hash((uchar *)nv, n);",
	"#endif",
	"	H_tab = tmp;",
	"	for (v = S_Tab[j1_spin]; v; Zh++, last=v, v=v->nxt)",
	"	{	m = memcmp(&(v->state), nv, n);",
	"		if (m == 0)",
	"			goto Found;",
	"		if (m < 0)",
	"			break;",
	"	}",
	"/* NotFound: */",
	"#ifndef ZAPH",
	"	/* seen this happen, likely harmless in multicore */",
	"	if (warned == 0)",
	"	{	/* Uerror(\"stack out of wack - zap\"); */",
	"		cpu_printf(\"pan: warning, stack incomplete\\n\");",
	"		warned = 1;",
	"	}",
	"#endif",
	"	goto done;",
	"Found:",
	"	ZAPS++;",
	"	if (last)",
	"		last->nxt = v->nxt;",
	"	else",
	"		S_Tab[j1_spin] = v->nxt;",
	"	v->tagged = (unsigned) 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 ((int) w->tagged <= n)",
	"		{	if (last)",
	"			{	v->nxt = w;",
	"				last->nxt = v;",
	"			} else",
	"			{	v->nxt = Free_list;",
	"				Free_list = v;",
	"			}",
	"			goto done;",
	"		}",
	"		if (!w->nxt)",
	"		{	w->nxt = v;",
	"			goto done;",
	"	}	}",
	"	Free_list = v;",
	"done:",
	"#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
	"	now._last = was_last;",
	"#endif",
	"	return;",
	"}",
	"void",
	"onstack_put(void)",
	"{	struct H_el **tmp = H_tab;",
	"#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
	"	uchar was_last = now._last;",
	"	now._last = 0;",
	"#endif",
	"	H_tab = S_Tab;",
	"	if (hstore((char *)&now, vsize) != 0)",
	"#if defined(BITSTATE) && defined(LC)",
	"		printf(\"pan: warning, double stack entry\\n\");",
	"#else",
	"	#ifndef ZAPH",
	"		Uerror(\"cannot happen - unstack_put\");",
	"	#endif",
	"#endif",
	"	H_tab = tmp;",
	"	trpt->ostate = Lstate;",
	"	PUT++;",
	"#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
	"	now._last = was_last;",
	"#endif",
	"}",
	"int",
	"onstack_now(void)",
	"{	struct H_el *tmp;",
	"	struct H_el **tmp2 = H_tab;",
	"	char *v; int n, m = 1;\n",
	"#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
	"	uchar was_last = now._last;",
	"	now._last = 0;",
	"#endif",
	"	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))",
	"	s_hash((uchar *)v, n);",
	"#endif",
	"	H_tab = tmp2;",
	"	for (tmp = S_Tab[j1_spin]; tmp; Zn++, tmp = tmp->nxt)",
	"	{	m = memcmp(((char *)&(tmp->state)),v,n);",
	"		if (m <= 0)",
	"		{	Lstate = (struct H_el *) tmp;",
	"			break;",
	"	}	}",
	"	PROBE++;",
	"#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
	"	now._last = was_last;",
	"#endif",
	"	return (m == 0);",
	"}",
	"#endif",
"#endif",

	"#ifndef BITSTATE",
	"void",
	"hinit(void)",
	"{",
	"  #ifdef MA",
		"#ifdef R_XPT",
		"	{	void r_xpoint(void);",
		"		r_xpoint();",
		"	}",
		"#else",
		"	dfa_init((unsigned short) (MA+a_cycles));",
			"#if NCORE>1 && !defined(COLLAPSE)",
			"	if (!readtrail)",
			"	{	void init_HT(unsigned long);",
			"		init_HT(0L);",
			"	}",
			"#endif",
		"#endif",
	"  #endif",
	"  #if !defined(MA) || defined(COLLAPSE)",
		"#if NCORE>1",
			"	if (!readtrail)",
			"	{	void init_HT(unsigned long);",
			"		init_HT((unsigned long) (ONE_L<<ssize)*sizeof(struct H_el *));",
			"	} else",
		"#endif",
			"	H_tab = (struct H_el **)",
			"		emalloc((ONE_L<<ssize)*sizeof(struct H_el *));",
			"	/* @htable ssize */",
	"  #endif",
	"}",
	"#endif\n",

	"#if !defined(BITSTATE) || defined(FULLSTACK)",

	"#ifdef DEBUG",
	"void",
	"dumpstate(int wasnew, char *v, int n, int tag)",
	"{	int i;",
	"#ifndef SAFETY",
	"	if (S_A)",
	"	{	printf(\"\tstate tags %%d (%%d::%%d): \",",
	"			V_A, wasnew, v[0]);",
		"#ifdef FULLSTACK",
	"		printf(\" %%d \", tag);",
		"#endif",
	"		printf(\"\\n\");",
	"	}",
	"#endif",
	"#ifdef SDUMP",
	"#ifndef NOCOMP",
	"	printf(\"\t State: \");",
	"	for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",",
	"		((char *)&now)[i], Mask[i]?\"*\":\"\");",
	"#endif",
	"	printf(\"\\n\tVector: \");",
	"	for (i = 0; i < n; i++) printf(\"%%d,\", v[i]);",
	"	printf(\"\\n\");",
	"#endif",
	"}",
	"#endif",

"#ifdef MA",
	"int",
	"gstore(char *vin, int nin, uchar pbit)",
	"{	int n, i;",
	"	int ret_val = 1;",
	"	uchar *v;",
	"	static uchar Info[MA+1];",
	"#ifndef NOCOMP",
	"	n = compress(vin, nin);",
	"	v = (uchar *) &comp_now;",
	"#else",
	"	n = nin;",
	"	v = (uchar *) vin;",
	"#endif",
	"	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 > (int) maxgs)",
	"	{	maxgs = (unsigned int) n;",
	"	}",
	"	for (i = 0; i < n; i++)",
	"	{	Info[i] = v[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 NCORE>1 && !defined(SEP_STATE)",
	"	enter_critical(GLOBAL_LOCK); /* crude, but necessary */",
	"	/* to make this mode work, also replace emalloc with grab_shared inside store MA routines */",
	"#endif",
	"",
	"	if (!dfa_store(Info))",
	"	{	if (pbit == 0",
	"		&& (now._a_t&1)",
	"		&&  depth > A_depth)",
	"		{	Info[MA] &= ~(1|16|32);	/* _a_t */",
	"			if (dfa_member(MA))",	/* was !dfa_member(MA) */
	"			{	Info[MA-1] = 4; /* off-stack bit */",
	"				nShadow++;",
	"				if (!dfa_member(MA-1))",
	"				{	ret_val = 3;",
	"			#ifdef VERBOSE",
	"					printf(\"intersected 1st dfs stack\\n\");",
	"			#endif",
	"					goto done;",
	"		}	}	}",
	"		ret_val = 0;",
	"	#ifdef VERBOSE",
	"		printf(\"new state\\n\");",
	"	#endif",
	"		goto done;",
	"	}",
	"#ifdef FULLSTACK",
	"	if (pbit == 0)",
	"	{	Info[MA-1] = 1;	/* proviso bit */",
	"#ifndef BFS",
	"		trpt->proviso = dfa_member(MA-1);",
	"#endif",
	"		Info[MA-1] = 4;	/* off-stack bit */",
	"		if (dfa_member(MA-1))",
	"		{	ret_val = 1; /* off-stack */",
	"	#ifdef VERBOSE",
	"			printf(\"old state\\n\");",
	"	#endif",
	"		} else",
	"		{	ret_val = 2; /* on-stack */",
	"	#ifdef VERBOSE",
	"			printf(\"on-stack\\n\");",
	"	#endif",
	"		}",
	"		goto done;",
	"	}",
	"#endif",
	"	ret_val = 1;",
	"#ifdef VERBOSE",
	"	printf(\"old state\\n\");",
	"#endif",
	"done:",
	"#if NCORE>1 && !defined(SEP_STATE)",
	"	leave_critical(GLOBAL_LOCK);",
	"#endif",
	"	return ret_val;	/* old state */",
	"}",
"#endif",

	"#if defined(BITSTATE) && defined(LC)",
	"int",
	"compact_stack(char *vin, int n)",	/* special case of HC4 */
	"{	int delta = 0;",
	"	s_hash((uchar *)vin, n); /* sets K1 and K2 */",
		"#ifndef SAFETY",
	"	delta++;	/* room for state[0] |= 128 */",
		"#endif",
	"	memcpy((char *) &comp_now + delta, (char *) &K1, WS);",
	"	delta += WS;",
	"	memcpy((char *) &comp_now + delta, (char *) &K2, WS);",
	"	delta += WS; /* use all available bits */",
	"	return delta;",
	"}",
	"#endif",

	"#ifdef TRIX",
	"void",
	"sv_populate(void)",
	"{	int i, cnt = 0;",
	"	TRIX_v6 **base = processes;",
	"	int bound = now._nr_pr; /* MAXPROC+1; */",
	"#ifdef V_TRIX",
	"	printf(\"%%4d: sv_populate\\n\", depth);",
	"#endif",
	"again:",
	"	for (i = 0; i < bound; i++)",
	"	{	if (base[i] != NULL)",
	"		{	struct H_el *tmp;",
	"			int m, n; uchar *v;",
	"#ifndef BFS",
	"			if (base[i]->modified == 0)",
	"			{	cnt++;",
	"	#ifdef V_TRIX",
	"				printf(\"%%4d: %%s %%d not modified\\n\",",
	"				depth, (base == processes)?\"proc\":\"chan\", i);",
	"	#endif",
	"				continue;",
	"			}",
	"	#ifndef V_MOD",
	"			base[i]->modified = 0;",
	"	#endif",
	"#endif",
	"#ifdef TRIX_RIX",
	"			if (base == processes)",
	"			{	((P0 *)pptr(i))->_pid = 0;",
	"			}",
	"#endif",
	"			n = base[i]->psize;",
	"			v = base[i]->body;",
	"			s_hash(v, n); /* sets j1_spin */",
	"			tmp = H_tab[j1_spin];",
	"			if (!tmp)	/* new */",
	"			{	tmp = grab_state(n);",
	"				H_tab[j1_spin] = tmp;",
	"				m = 1; /* non-zero */",
	"			} else",
	"			{  struct H_el *ntmp, *olst = (struct H_el *) 0;",
	"			   for (;; hcmp++, olst = tmp, tmp = tmp->nxt)",
	"			   { 	m = memcmp(((char *)&(tmp->state)), v, n);",
	"				if (m == 0)	/* match */",
	"				{	break;",
	"				} else if (m < 0) /* insert */",
	"				{	ntmp = grab_state(n);",
	"					ntmp->nxt = tmp;",
	"					if (!olst)",
	"						H_tab[j1_spin] = ntmp;",
	"					else",
	"						olst->nxt = ntmp;",
	"					tmp = ntmp;",
	"					break;",
	"				} else if (!tmp->nxt)	/* append */",
	"				{	tmp->nxt = grab_state(n);",
	"					tmp = tmp->nxt;",
	"					break;",
	"			}  }	}",
	"			if (m != 0)",
	"			{	memcpy((char *)&(tmp->state), v, n);",
	"#if defined(AUTO_RESIZE) && !defined(BITSTATE)",
	"				tmp->m_K1 = K1; /* set via s_hash */",
	"#endif",
	"				if (base == processes)",
	"				{	_p_count[i]++;",
	"				} else",
	"				{	_c_count[i]++;",
	"			}	}",
	"			now._ids_[cnt++] = (char *)&(tmp->state);",
	"#ifdef TRIX_RIX",
	"			if (base == processes)",
	"			{	((P0 *)pptr(i))->_pid = i;",
	"			}",
	"#endif",
	"	}	}",
#if 0
	if a process appears or disappears: always secure a full sv_populate
	(channels come and go only with a process)

	only one process can disappear per step
	but any nr of channels can be removed at the same time
		if a process disappears, all subsequent entries
		are then in the wrong place in the _ids_ list
		and need to be recomputed
	but we do not need to fill out with zeros
		because vsize prevents them being used
#endif
	"	/* do the same for all channels */",
	"	if (base == processes)",
	"	{	base = channels;",
	"		bound = now._nr_qs; /* MAXQ+1; */",
	"		goto again;",
	"	}",
	"}",
	"#endif\n",
	"int",
	"hstore(char *vin, int nin)	/* hash table storage */",
	"{	struct H_el *ntmp;",
	"	struct H_el *tmp, *olst = (struct H_el *) 0;",
	"	char *v; int n, m=0;",
	"#ifdef HC",
	"	uchar rem_a;",
	"#endif",

	"#ifdef TRIX",
	"	sv_populate();	/* update proc and chan ids */",
	"#endif",

	"#ifdef NOCOMP",	/* defined by BITSTATE */
	"	#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;",
	"	#ifdef HC",
	"	rem_a = now._a_t;",	/* new 5.0 */
	"	now._a_t = 0;",	/* for hashing/state matching to work right */
	"	#endif",
	"	n = compress(vin, nin);", /* with HC, this calls s_hash -- but on vin, not on v... */
	"	#ifdef HC",
	"	now._a_t = rem_a;",	/* new 5.0 */
	"	#endif",
		/* with HC4 -a, compress copies K1 and K2 into v[], leaving v[0] free for the a-bit */
		"#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))",
	"	s_hash((uchar *)v, n);",
	"#endif",
	"#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
	"	enter_critical(CS_ID);	/* uses spinlock */",
	"#endif",

	"	tmp = H_tab[j1_spin];",
	"	if (!tmp)",
	"	{  tmp = grab_state(n);",
	"#if NCORE>1",
	"	   if (!tmp)",
	"	   {	/* if we get here -- we've already issued a warning */",
	"		/* but we want to allow the normal distributed termination */",
	"		/* to collect the stats on all cpus in the wrapup */",
	"	#if !defined(SEP_STATE) && !defined(BITSTATE)",
	"		leave_critical(CS_ID);",
	"	#endif",
	"		return 1; /* allow normal termination */",
	"	   }",
	"#endif",
	"	   H_tab[j1_spin] = 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",

	"#if NCORE>1",
	"		Lstate = (struct H_el *) tmp;",
	"#endif",

	"#ifdef FULLSTACK",
		"#ifndef SAFETY",	/* or else wasnew == 0 */
	"		if (wasnew)",
	"		{	Lstate = (struct H_el *) tmp;",
	"			tmp->tagged |= V_A;",
	"			if ((now._a_t&1)",
	"			&& (tmp->tagged&A_V)",
	"			&& depth > A_depth)",
	"			{",
	"intersect:",
		"#ifdef CHECK",
	"#if NCORE>1",
	"	printf(\"cpu%%d: \", core_id);",
	"#endif",
	"	printf(\"1st dfs-stack intersected on state %%d+\\n\",",
	"		(int) tmp->st_id);",
		"#endif",

	"#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
	"				leave_critical(CS_ID);",
	"#endif",

	"				return 3;",
	"			}",
		"#ifdef CHECK",
	"#if NCORE>1",
	"	printf(\"cpu%%d: \", core_id);",
	"#endif",
	"	printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);",
		"#endif",
		"#ifdef DEBUG",
	"	dumpstate(1, (char *)&(tmp->state),n,tmp->tagged);",
		"#endif",
	"#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
	"			leave_critical(CS_ID);",
	"#endif",
	"			return 0;",
	"		} else",
		"#endif",
	"		if ((S_A)?(tmp->tagged&V_A):tmp->tagged)",
	"		{	Lstate = (struct H_el *) tmp;",
		"#ifndef SAFETY",
	"			/* already on current dfs stack */",
	"			/* but may also be on 1st dfs stack */",
	"			if ((now._a_t&1)",
	"			&& (tmp->tagged&A_V)",

	"			&& depth > A_depth",
		/* new (Zhang's example) */
		"#ifndef NOFAIR",
	"			&& (!fairness || now._cnt[1] <= 1)",
		"#endif",
	"			)",

	"				goto intersect;",
		"#endif",
		"#ifdef CHECK",
	"#if NCORE>1",
	"	printf(\"cpu%%d: \", core_id);",
	"#endif",
	"	printf(\"\tStack state %%d\\n\", (int) tmp->st_id);",
		"#endif",
		"#ifdef DEBUG",
	"	dumpstate(0, (char *)&(tmp->state),n,tmp->tagged);",
		"#endif",
	"#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
	"			leave_critical(CS_ID);",
	"#endif",
	"			return 2; /* match on stack */",
	"		}",
	"#else",
	"		if (wasnew)",
	"		{",
		"#ifdef CHECK",
	"#if NCORE>1",
	"	printf(\"cpu%%d: \", core_id);",
	"#endif",
	"	printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);",
		"#endif",
		"#ifdef DEBUG",
	"	dumpstate(1, (char *)&(tmp->state), n, 0);",
		"#endif",
	"#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
	"			leave_critical(CS_ID);",
	"#endif",
	"			return 0;",
	"		}",
	"#endif",
		"#ifdef CHECK",
	"#if NCORE>1",
	"	printf(\"cpu%%d: \", core_id);",
	"#endif",
	"	printf(\"\tOld state %%d\\n\", (int) tmp->st_id);",
		"#endif",
		"#ifdef DEBUG",
	"	dumpstate(0, (char *)&(tmp->state), n, 0);",
		"#endif",
	"#if defined(BCS)",
	"  #ifdef CONSERVATIVE",
	"	if (tmp->ctx_low > trpt->sched_limit)",
	"	{	tmp->ctx_low = trpt->sched_limit;",
	"		tmp->ctx_pid[(now._last)/8] = 1 << ((now._last)%8); /* new */",
	"	#ifdef CHECK",
	"		#if NCORE>1",
	"		printf(\"cpu%%d: \", core_id);",
	"		#endif",
	"		printf(\"\t\tRevisit with fewer context switches\\n\");",
	"	#endif",
	"		nstates--;",
	"		#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
	"		leave_critical(CS_ID);",
	"		#endif",
	"		return 0;",
	"	} else if ((tmp->ctx_low == trpt->sched_limit",
	"	&&   (tmp->ctx_pid[(now._last)/8] & ( 1 << ((now._last)%8) )) == 0 ))",
	"	{	tmp->ctx_pid[(now._last)/8] |= 1 << ((now._last)%8); /* add */",
	"	#ifdef CHECK",
	"		#if NCORE>1",
	"		printf(\"cpu%%d: \", core_id);",
	"		#endif",
	"		printf(\"\t\tRevisit with same nr of context switches\\n\");",
	"	#endif",
	"		nstates--;",
	"		#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
	"		leave_critical(CS_ID);",
	"		#endif",
	"		return 0;",
	"	}",
	"  #endif",
	"#endif",
	"#ifdef REACH",
	"	if (tmp->D > depth)",
	"	{	tmp->D = depth;",
	"	#ifdef CHECK",
	"		#if NCORE>1",
	"		printf(\"cpu%%d: \", core_id);",
	"		#endif",
	"		printf(\"\t\tReVisiting (from smaller depth)\\n\");",
	"	#endif",
	"		nstates--;",
	"	#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
	"		leave_critical(CS_ID);",
	"	#endif",
#if 0
  a possible variation of iterative search for shortest counter-example
  (pan -i and pan -I) suggested by Pierre Moro (for safety properties):
  state revisits on shorter depths do not start until after
  the first counter-example is found.  this assumes that the max search
  depth is set large enough that a first (possibly long) counter-example
  can be found
  if set too short, this variant can miss the counter-example, even if
  it would otherwise be shorter than the depth-limit.
  (p.m. unsure if this preserves the guarantee of finding the
   shortest counter-example - so not enabled by default)
	"		if (errors > 0 && iterative)", /* Moro */
#endif
	"		return 0;",
	"	}",
	"#endif",
	"#if (defined(BFS) && defined(Q_PROVISO)) || NCORE>1",
	"		Lstate = (struct H_el *) tmp;",
	"#endif",
	"#if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
	"		leave_critical(CS_ID);",
	"#endif",
	"		return 1; /* match outside stack */",
	"	       } else if (m < 0)",
	"	       {	/* insert state before tmp */",
	"			ntmp = grab_state(n);",
	"#if NCORE>1",
	"			if (!ntmp)",
	"			{",
	"	#if !defined(SEP_STATE) && !defined(BITSTATE)",
	"				leave_critical(CS_ID);",
	"	#endif",
	"				return 1;  /* allow normal termination */",
	"			}",
	"#endif",
	"			ntmp->nxt = tmp;",
	"			if (!olst)",
	"				H_tab[j1_spin] = ntmp;",
	"			else",
	"				olst->nxt = ntmp;",
	"			tmp = ntmp;",
	"			break;",
	"	       } else if (!tmp->nxt)",
	"	       {	/* append after tmp */",
	"#ifdef COLLAPSE",
	"Append:",
	"#endif",
	"			tmp->nxt = grab_state(n);",
	"#if NCORE>1",
	"			if (!tmp->nxt)",
	"			{",
	"	#if !defined(SEP_STATE) && !defined(BITSTATE)",
	"				leave_critical(CS_ID);",
	"	#endif",
	"				return 1;  /* allow normal termination */",
	"			}",
	"#endif",
	"			tmp = tmp->nxt;",
	"			break;",
	"	   }   }",
	"	}",
	"#ifdef CHECK",
	"	tmp->st_id = (unsigned) nstates;",
	"#if NCORE>1",
	"	printf(\"cpu%%d: \", core_id);",
	"#endif",
		"#ifdef BITSTATE",
	"	printf(\"	Push state %%d\\n\", ((int) nstates) - 1);",
		"#else",
	"	printf(\"	New state %%d\\n\", (int) nstates);",
		"#endif",
	"#endif",
	"#if defined(BCS)",
	"	tmp->ctx_low = trpt->sched_limit;",
	"	#ifdef CONSERVATIVE",
	"	tmp->ctx_pid[(now._last)/8] = 1 << ((now._last)%8); /* new limit */",
	"	#endif",
	"#endif",
	"#if !defined(SAFETY) || defined(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",
	"#if defined(AUTO_RESIZE) && !defined(BITSTATE)",
	"	tmp->m_K1 = K1;",
	"#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 = (struct H_el *) tmp;",
	"#else",
	"	#ifdef DEBUG",
	"		dumpstate(-1, v, n, 0);",
	"	#endif",
	"	#if NCORE>1",
	"		Lstate = (struct H_el *) tmp;",
	"	#endif",
	"#endif",

	"/* #if NCORE>1 && !defined(SEP_STATE) */",
	"#if NCORE>1",
	"	#ifdef V_PROVISO",
	"		tmp->cpu_id = core_id;",
	"	#endif",
	"	#if !defined(SEP_STATE) && !defined(BITSTATE)",
	"		leave_critical(CS_ID);",
	"	#endif",
	"#endif",

	"	return 0;",
	"}",
	"#endif",
	"#include TRANSITIONS",
	0,
};