text: 
  
  
  
  static const char *pan_par[] = {	
  	"#include <sys/ipc.h>",
  	"#include <sys/shm.h>",
  	"#include <time.h>",	
  	"#include <assert.h>",
  	"#include <limits.h>",
  	"#ifdef BFS_DISK",
  	"#include <unistd.h>",		
  	"#include <sys/stat.h>",	
  	"#include <sys/types.h>",
  	"#include <fcntl.h>",		
  	"#endif",
  	"",
  	"#define Max(a,b)	(((a)>(b))?(a):(b))",
  	"#ifndef WAIT_MAX",
  	"	#define WAIT_MAX	2	/* seconds */",
  	"#endif",
  	"#define BFS_GEN 	2	/* current and next generation */",
  	"",
  	"typedef struct BFS_Slot BFS_Slot;",
  	"typedef struct BFS_shared BFS_shared;",
  	"typedef struct BFS_data BFS_data;",
  	"",
  	"struct BFS_Slot {",
  	" #ifdef BFS_FIFO",
  	"	enum bfs_types	type;		/* message type */",
  	" #endif",
  	"	BFS_State	*s_data;	/* state data */",
  	" #ifndef BFS_QSZ",
  	"	BFS_Slot	*nxt;		/* linked list */",
  	" #endif",
  	"};",
  	"",
  	"struct BFS_data {",
  	"	double memcnt;",
  	"	double nstates;",
  	"	double nlinks;",
  	"	double truncs;",
  	"	ulong mreached;",
  	"	ulong vsize;",
  	"	ulong memory_left;",
  	"	ulong punted;",
  	"	ulong errors;",
  	"	int   override;	/* after crash, if another proc clears locks */",
  	"};",
  	"",
  	"struct BFS_shared {	/* about 13K for BFS_MAXPROCS=16 and BFS_MAXLOCKS=1028 */",
  	"	volatile ulong	quit;	/* set to signal termination -- one word */",
  	"	volatile ulong	started;",
  	"",
  	"	volatile uchar	sh_owner[BFS_MAXLOCKS];		/* optional */",
  	"#ifdef BFS_CHECK",
  	"	volatile uchar	in_count[BFS_MAXLOCKS];		/* optional */",
  	"#endif",
  	"	volatile int	sh_locks[BFS_MAXLOCKS];",
  	"	volatile ulong	wait_count[BFS_MAXLOCKS];	/* optional */",
  	"",
  	"	volatile BFS_data bfs_data[BFS_MAXPROCS];",
  	"	volatile uchar	bfs_flag[BFS_MAXPROCS]; /* running 0, normal exit 1, abnormal 2 */",
  	"	volatile uchar	bfs_idle[BFS_MAXPROCS]; /* set when all input queues are empty */",
  	"#ifdef BFS_DISK",
  	"	volatile uchar	bfs_out_cnt[BFS_MAXPROCS]; /* set when core writes a state */",
  	"#endif",
  	"",
  	"#ifdef BFS_QSZ",
  	"	#define BFS_NORECYCLE",
  	"	#if BFS_QSZ<=0",
  	"		#error BFS_QSZ must be positive",
  	"	#endif",
  	"	#ifdef BFS_FIFO",
  	"		#error BFS_QSZ cannot be combined with BFS_FIFO",
  	"	#endif",
  	"	#ifdef BFS_DISK",
  	"		#error BFS_QSZ cannot be combined with BFS_DISK",
  	"	#endif",
  	"	volatile BFS_Slot bfsq[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS][BFS_QSZ];",
  	"	volatile uint bfs_ix[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS];",
  	"#else",
  	"	volatile BFS_Slot *head[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS];",
  	"#endif",
  	"",
  	"#ifdef BFS_FIFO",
  	"	volatile BFS_Slot *tail[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS];",
  	"	volatile BFS_Slot *dels[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS];",
  	"#endif",
  	"#ifdef BFS_LOGMEM",
  	"	volatile ulong logmem[1024];",
  	"#endif",
  	"	volatile ulong mem_left;",
  	"	volatile uchar *allocator;	/* start of shared heap, must be last */",
  	"};",
  	"",
  	"enum bfs_types { EMPTY = 0, STATE, DELETED };",
  	"",
  	"extern volatile uchar *bfs_get_shared_mem(key_t, size_t);",
  	"extern BFS_Slot  * bfs_new_slot(BFS_Trail *);",
  	"extern BFS_Slot  * bfs_prep_slot(BFS_Trail *, BFS_Slot *);",
  	"extern BFS_Slot  * bfs_next(void);",
  	"extern BFS_Slot  * bfs_pack_state(Trail *, BFS_Trail *, int, BFS_Slot *);",
  	"extern SV_Hold   * bfs_new_sv(int);",
  	"#if NRUNS>0",
  	"extern EV_Hold   * bfs_new_sv_mask(int);",
  	"#endif",
  	"extern BFS_Trail * bfs_grab_trail(void);",
  	"extern BFS_Trail * bfs_unpack_state(BFS_Slot *);",
  	"extern int         bfs_all_empty(void);",
  	"extern int         bfs_all_idle(void);",
  	"extern int         bfs_all_running(void);",
  	"extern int         bfs_idle_and_empty(void);",
  	"extern size_t	    bfs_find_largest(key_t);",
  	"",
  	"extern void	bfs_clear_locks(void);",
  	"extern void	bfs_drop_shared_memory(void);",
  	"extern void	bfs_explore_state(BFS_Slot *);",
  	"extern void	bfs_initial_state(void);",
  	"extern void	bfs_mark_done(int);",
  	"extern void	bfs_printf(const char *fmt, ...);",
  	"extern void	bfs_push_state(Trail *, BFS_Trail *, int);",
  	"extern void	bfs_recycle(BFS_Slot *);",
  	"extern void	bfs_release_trail(BFS_Trail *);",
  	"extern void	bfs_run(void);",
  	"extern void	bfs_setup_mem(void);",
  	"extern void	bfs_setup(void);",
  	"extern void	bfs_shutdown(const char *);",
  	"extern void	bfs_statistics(void);",
  	"extern void	bfs_store_state(Trail *, short);",
  	"extern void	bfs_set_toggle(void);",
  	"extern void	bfs_update(void);",
  	"",
  	"#ifdef MA",
  	"	#error cannot combine -DMA with -DBFS_PAR",
  	"	/* would require us to parallelize g_store */",
  	"#endif",
  	"#ifdef BCS",
  	"	#error cannot combine -DBCS with -DBFS_PAR",
  	"#endif",
  	"#ifdef BFS_DISK",
  	"	#ifdef BFS_FIFO",
  	"		#error cannot combine BFS_DISK and BFS_FIFO",
  	"	#endif",
  	"	extern void bfs_disk_start(void);",
  	"	extern void bfs_disk_stop(void);",
  	"	extern void bfs_disk_out(void);",
  	"	extern void bfs_disk_inp(void);",
  	"	extern void bfs_disk_iclose(void);",
  	"	extern void bfs_disk_oclose(void);",
  	"	int bfs_out_fd[BFS_MAXPROCS];",
  	"	int bfs_inp_fd[BFS_MAXPROCS];",
  	"#endif",
  	"",
  	"static BFS_shared *shared_memory;",
  	"#ifndef BFS_QSZ",
  	"static BFS_Slot   *bfs_free_slot; /* local free list */",
  	"#endif",
  	"static BFS_Slot    bfs_null;",
  	"static SV_Hold    *bfs_svfree[VECTORSZ];",
  	"static uchar	*bfs_heap;	/* local pointer into heap */",
  	"static ulong	bfs_left;	/* local part of shared heap */",
  	"#if NRUNS>0",
  	"static void	bfs_keep(EV_Hold *);",
  	"#endif",
  	"static long	bfs_sent;	/* nr msgs sent -- local to each process */",
  	"static long	bfs_rcvd;	/* nr msgs rcvd */",
  	"static long	bfs_sleep_cnt;	/* stats */",
  	"static long	bfs_wcount;",
  	"static long	bfs_gcount;",
  	"static ulong	bfs_total_shared;",
  	"#ifdef BFS_STAGGER",
  	" static int	bfs_stage_cnt = 0;",
  	" static void	bfs_stagger_flush(void);",
  	"#endif",
  	"static int	bfs_toggle;	/* local variable, 0 or 1 */",
  	"static int	bfs_qscan;	/* scan input queues in order */",
  	"static ulong	bfs_snapped;",
  	"static int	shared_mem_id;",
  	"#ifndef NOREDUCE",
  	"static int	bfs_nps;	/* no preselection */",
  	"#endif",
  	"ulong	bfs_punt;	/* states dropped for lack of memory */",
  	"#if defined(VERBOSE) || defined(BFS_CHECK)",
  	"static const char *bfs_sname[] = {",
  	"	\"EMPTY\",	/* 0 */",
  	"	\"STATE\",	/* 1 */",
  	"	\"STATE\",	/* 2 = DELETED */",
  	"	0",
  	"};",
  	"#endif",
  	"static const char *bfs_lname[] = { /* match values defined in pangen2.c */",
  	"	\"global lock\",	/* BFS_GLOB  */",
  	"	\"ordinal\",		/* BFS_ORD  */",
  	"	\"shared memory\",	/* BFS_MEM   */",
  	"	\"print to stdout\",	/* BFS_PRINT */",
  	"	\"hashtable\",		/* BFS_STATE */",
  	"	0",
  	"};",
  	"",
  	"static ulong bfs_count[DELETED+1];	/* indexed with bfs_types: EMPTY=0, STATE=1, DELETED=2 */",
  	"",
  	"static int bfs_keep_state;",
  	"",
  	"int Cores = 1;",
  	"int who_am_i = 0;	/* root */",
  	"",
  	"#ifdef L_BOUND",
  	"	int L_bound = L_BOUND;",
  	"#endif",
  	"",
  	"#ifdef BFS_CHECK",
  	"void",
  	"bfs_dump_now(char *s)",
  	"{	int i; char *p = (char *) &now;",
  	"",
  	"	e_critical(BFS_PRINT);",
  	"	printf(\"%%s\\t\", s);",
  	"	printf(\"%%3lu: \", vsize);",
  	"	for (i = 0; i < vsize; i++)",
  	"	{	printf(\"%%3d \", *p++);",
  	"	}",
  	"	printf(\"	%%s\\noffsets:\\t\", s);",
  	"	for (i = 0; i < now._nr_pr; i++)",
  	"	{	printf(\"%%3d \", proc_offset[i]);",
  	"	}",
  	"	printf(\"\\n\");",
  	"	x_critical(BFS_PRINT);",
  	"}",
  	"",
  	"void",
  	"view_state(char *s)	/* debugging */",
  	"{	int i;",
  	"	char *p;",
  	"	e_critical(BFS_PRINT);",
  	"	printf(\"cpu%%02d %%s: \", who_am_i, s);",
  	"	p = (char *)&now;",
  	"	for (i = 0; i < vsize; i++)",
  	"		printf(\"%%3d, \", *p++);",
  	"	printf(\"\\n\"); fflush(stdout);",
  	"	x_critical(BFS_PRINT);",
  	"}",
  	"#endif",
  	"",
  	"void",
  	"bfs_main(int ncores, int cycles)",
  	"{",
  	"	if (cycles)",
  	"	{	fprintf(stderr, \"pan: cycle detection is not supported in this mode\\n\");",
  	"		exit(1);",
  	"	}",
  	"",
  	"	if (ncores == 0)	/* i.e., find out */",
  	"	{	FILE *fd;",
  	"		char buf[512];",
  	"		if ((fd = fopen(\"/proc/cpuinfo\", \"r\")) == NULL)",
  	"		{	/* cannot tell */",
  	"			ncores = Cores; /* use the default */",
  	"		} else",
  	"		{	while (fgets(buf, sizeof(buf), fd))",
  	"			{	if (strncmp(buf, \"processor\", strlen(\"processor\")) == 0)",
  	"				{	ncores++;",
  	"			}	}",
  	"			fclose(fd);",
  	"			ncores--;",
  	"			if (verbose)",
  	"			{	printf(\"pan: %%d available cores\\n\", ncores+1);",
  	"	}	}	}",
  	"	if (ncores >= BFS_MAXPROCS)",
  	"	{	Cores = BFS_MAXPROCS-1; /* why -1? */",
  	"	} else if (ncores <  1)",
  	"	{	Cores = 1;",
  	"	} else",
  	"	{	Cores = ncores;",
  	"	}",
  	"	printf(\"pan: using %%d core%%s\\n\", Cores, (Cores>1)?\"s\":\"\");",
  	"	fflush(stdout);",
  	"#ifdef BFS_DISK",
  	"	bfs_disk_start();",	
  	"#endif",
  	"	bfs_setup();	/* shared memory segments and fork */",
  	"	bfs_run();",
  	"	if (who_am_i == 0)",
  	"	{	stop_timer(0);",
  	"	}",
  	"	bfs_statistics();",
  	"	bfs_mark_done(1);",
  	"	if (who_am_i == 0)",
  	"	{	report_time();",
  	"#ifdef BFS_DISK",
  	"		bfs_disk_stop();",
  	"#endif",
  	"	}",
  	"#ifdef C_EXIT",
  	"	C_EXIT; /* trust that it defines a fct */",
  	"#endif",
  	"	bfs_drop_shared_memory();",
  	"	exit(0);",
  	"}",
  	"",
  	"void",
  	"bfs_setup_mem(void)",
  	"{	size_t n;",
  	"	key_t key;",
  	"#ifdef BFS_FIFO",
  	"	bfs_null.type = EMPTY;",
  	"#endif",
  	"	ntrpt = (Trail *) emalloc(sizeof(Trail));", 
  	"",
  	"	if ((key = ftok(\".\", (int) 'L')) == -1)",
  	"	{	perror(\"ftok shared memory\");",
  	"		exit(1);",
  	"	}",
  	"	n = bfs_find_largest(key);",
  	"	bfs_total_shared = (ulong) n;",
  	"",
  	"	shared_memory            = (BFS_shared *) bfs_get_shared_mem(key, n);	/* root */",
  	"	shared_memory->allocator = (uchar *) shared_memory + sizeof(BFS_shared);",
  	"	shared_memory->mem_left  = (ulong) (n - sizeof(BFS_shared));",
  	"}",
  	"",
  	"ulong bfs_LowLim;",
  	"#ifndef BFS_RESERVE",
  	"	#define BFS_RESERVE 5",
  	
  	
  	
  	"#else",
  	"	#if BFS_RESERVE<1",
  	"	#error BFS_RESERVE must be at least 1",
  	"	#endif",
  	"#endif",
  	"",
  	"void",
  	"bfs_setup(void)	/* executed by root */",
  	"{	int i, j;",
  	"	ulong n;	/* share of shared memory allocated to each core */",
  	"",
  	"	n = shared_memory->mem_left / (Cores + Cores/(BFS_RESERVE)); /* keep some reserve */",
  	"",
  	"	if ((n%%sizeof(void *)) != 0)",
  	"	{       n -= (n%%sizeof(void *)); /* align, without exceeding total */",
  	"	}",
  	"	for (i = 0; i < Cores-1; i++)",
  	"	{	j = fork();",
  	"		if (j == -1)",
  	"		{	bfs_printf(\"fork failed\\n\");",
  	"			exit(1);",
  	"		}",
  	"		if (j == 0)",
  	"		{	who_am_i = i+1;	/* 1..Cores-1 */",
  	"			break;",
  	"	}	}",
  	"",
  	"	e_critical(BFS_MEM);",
  	"	 bfs_heap = (uchar *) shared_memory->allocator;",
  	"	 shared_memory->allocator += n;",
  	"	 shared_memory->mem_left  -= n;",
  	"	x_critical(BFS_MEM);",
  	"",
  	"	bfs_left = n;",
  	"	bfs_runs = 1;",
  	"	bfs_LowLim = n / (2 * (ulong) Cores);", 
  	"}",
  	"",
  	"void",
  	"bfs_run(void)",
  	"{	BFS_Slot *v;",
  	"",
  	"#ifdef BFS_DISK",
  	"	bfs_disk_out();",	
  	"#endif",
  	"	if (who_am_i == 0)",
  	"	{	bfs_initial_state();",
  	"	}",
  	"#ifdef BFS_DISK",
  	"	#ifdef BFS_STAGGER",
  	"	bfs_stagger_flush();",
  	"	#endif",
  	"	bfs_disk_oclose();",	
  	"#endif",
  	"#ifdef BFS_FIFO",
  	"	static int i_count;",
  	"#endif",
  	"",
  	"	srand(s_rand+HASH_NR);",
  	"	bfs_qscan = 0;",
  	"	bfs_toggle = 1 - bfs_toggle; /* after initial state */",
  	"	e_critical(BFS_GLOB);",
  	"	 shared_memory->started++;",
  	"	x_critical(BFS_GLOB);",
  	"",
  	"	while (shared_memory->started != Cores)	/* wait for all cores to connect */",
  	"	{	usleep(1);",
  	"	}",
  	"",
  	"#ifdef BFS_DISK",
  	"	bfs_disk_out();",
  	"	bfs_disk_inp();",
  	"#endif",
  	"",
  	"	start_timer();",
  	"	while (shared_memory->quit == 0)",
  	"	{	v = bfs_next(); /* get next message from current generation */",
  	"		if (v->s_data) /* v->type == STATE || v->type == DELETED */",
  	"		{	bfs_count[STATE]++;",
  	"#ifdef VERBOSE",
  	"			bfs_printf(\"GOT STATE (depth %%d, nr %%u)\\n\",",
  	"				v->s_data->t_info->o_tt, v->s_data->nr);",
  	"#endif",
  	"			/* last resort: start dropping states when out of memory */",
  	"			if (bfs_left > 1024 || shared_memory->mem_left > 1024)",
  	"			{	bfs_explore_state(v);",
  	"			} else",
  	"			{	static int warned_loss = 0;",
  	"				if (warned_loss == 0 && who_am_i == 0)",
  	"				{	warned_loss++;",
  	"					bfs_printf(\"out of shared memory - losing states\\n\");",
  	"				}",
  	"				bfs_punt++;",
  	"			}",
  	"#if !defined(BFS_FIFO) && !defined(BFS_NORECYCLE)",
  	"			bfs_recycle(v);",
  	"#endif",
  	"#ifdef BFS_FIFO",
  	"			i_count = 0;",
  	"#endif",
  	"		} else",
  	"		{	bfs_count[EMPTY]++;",
  	"#if defined(BFS_FIFO) && defined(BFS_CHECK)",
  	"			assert(v->type == EMPTY);",
  	"#endif",
  	"#ifdef BFS_FIFO",
  	"			if (who_am_i == 0)",
  	"			{	if (bfs_idle_and_empty())",
  	"				{	if (i_count++ > 10)",
  	"					{	shared_memory->quit = 1;",
  	"					}",
  	"					else usleep(1);",
  	"				}",
  	"			} else if (!bfs_all_running())",
  	"			{	bfs_shutdown(\"early termination\");",
  	"			}",
  	"#else",
  	"			if (who_am_i == 0)",
  	"			{	if (bfs_all_idle())		/* wait for it */",
  	"				{	if (!bfs_all_empty())	/* more states to process */",
  	"					{	bfs_set_toggle();",
  	"						goto do_toggle;",
  	"					} else			/* done */",
  	"					{	shared_memory->quit = 1; /* step 4 */",
  	"					}",
  	"				} else",
  	"				{	bfs_sleep_cnt++;",
  	"				}",
  	"			} else",
  	"			{	/* wait for quit or idle bit to be reset by root */",
  	"				while (shared_memory->bfs_idle[who_am_i] == 1",
  	"				&&     shared_memory->quit == 0)",
  	"				{	if (bfs_all_running())",
  	"					{	bfs_sleep_cnt++;",
  	"						usleep(10);	/* new 6.2.3 */",
  	"					} else",
  	"					{	bfs_shutdown(\"early termination\");",
  	"						/* no return */",
  	"				}	}",
  	"do_toggle:			bfs_qscan = 0;",
  	"#ifdef BFS_DISK",
  	"				bfs_disk_iclose();",
  	"				bfs_disk_oclose();",
  	"#endif",
  	"				bfs_toggle = 1 - bfs_toggle;",
  	"#ifdef BFS_DISK",
  	"				bfs_disk_out();",
  	"				bfs_disk_inp();",
  	"#endif",
  	"	#ifdef BFS_CHECK",
  	"				bfs_printf(\"toggle: recv from %%d, send to %%d\\n\",",
  	"					bfs_toggle, 1 - bfs_toggle);",
  	"	#endif",
  	"			}",
  	"#endif",
  	"	}	}",
  	"#ifdef BFS_CHECK",
  	"	bfs_printf(\"done, sent %%5ld recvd %%5ld punt %%5lu sleep: %%ld\\n\",",
  	"		bfs_sent, bfs_rcvd, bfs_punt, bfs_sleep_cnt);",
  	"#endif",
  	"}",
  	"",
  	"void",
  	"bfs_report_mem(void)	/* called from within wrapup() */",
  	"{",
  	"	printf(\"%%9.3f	total shared memory usage\\n\\n\",",
  	"		((double) bfs_total_shared - (double) bfs_left)/(1024.*1024.));",
  	"}",
  	"",
  	"void",
  	"bfs_statistics(void)",
  	"{",
  	"	#ifdef VERBOSE",
  	"	enum bfs_types i;",
  	"	#endif",
  	"	if (verbose)",
  	"		bfs_printf(\"states sent %%7ld recvd %%7ld stored %%8g sleeps: %%4ld, %%4ld, %%ld\\n\",",
  	"			bfs_sent, bfs_rcvd, nstates, bfs_wcount, bfs_gcount, bfs_sleep_cnt);",
  	"	if (0) bfs_printf(\"states punted %%7lu\\n\", bfs_punt);",
  	"	#ifdef VERBOSE",
  	"	for (i = EMPTY; i <= DELETED; i++)",
  	"	{	if (bfs_count[i] > 0)",
  	"		{	bfs_printf(\"%%6s	%%8lu\\n\",",
  	"				bfs_sname[i], bfs_count[i]);",
  	"	}	}",
  	"	#endif",
  	"	bfs_update();",
  	"",
  	"	if (who_am_i == 0 && shared_memory)",
  	"	{	int i; ulong count = 0L;",
  	"		done = 1;",
  	"",
  	"		e_critical(BFS_PRINT);",
  	"		  wrapup();",
  	"		  if (verbose)",
  	"		  {	  printf(\"\\nlock-wait counts:\\n\");",
  	"	 	  	for (i = 0; i < BFS_STATE; i++)",
  	"	 			printf(\"%%16s  %%9lu\\n\",",
  	"					bfs_lname[i], shared_memory->wait_count[i]);",
  	"#ifndef BITSTATE",
  	"		  	for (i = BFS_STATE; i < BFS_MAXLOCKS; i++)",
  	"		  	{	if (0)",
  	"				printf(\"	[%%6d]  %%9lu\\n\",",
  	"					i, shared_memory->wait_count[i]);",
  	"				count += shared_memory->wait_count[i];",
  	"		  	}",
  	"	 	  	printf(\"%%16s  %%9lu (avg per region)\\n\",",
  	"				bfs_lname[BFS_STATE], count/(BFS_MAXLOCKS - BFS_STATE));",
  	"#endif",
  	"		  }",
  	"		  fflush(stdout);",
  	"		x_critical(BFS_PRINT);",
  	"	}",
  	"}",
  	"",
  	"void",
  	"bfs_snapshot(void)",
  	"{	clock_t stop_time;",
  	"	double delta_time;",
  	"	struct tms stop_tm;",
  	"	volatile BFS_data *s;",
  	"",
  	"	e_critical(BFS_PRINT);",
  	"	 printf(\"cpu%%02d Depth= %%7lu States= %%8.3g Transitions= %%8.3g \",",
  	"		who_am_i, mreached, nstates, nstates+truncs);",
  	"	 printf(\"Memory= %%9.3f\\t\", memcnt/1048576.);",
  	"	 printf(\"SharedMLeft= %%4lu \", bfs_left/1048576);",
  	"	 stop_time  = times(&stop_tm);",
  	"	 delta_time = ((double) (stop_time - start_time))/((double) sysconf(_SC_CLK_TCK));",
  	"	 if (delta_time > 0.01)",
  	"	 {	printf(\"t= %%6.3g R= %%6.0g\\n\", delta_time, nstates/delta_time);",
  	"	 } else",
  	"	 {	printf(\"t= %%6.3g R= %%6.0g\\n\", 0., 0.);",
  	"	 }",
  	"	 fflush(stdout);",
  	"	x_critical(BFS_PRINT);",
  	"",
  	"	s = &shared_memory->bfs_data[who_am_i];",
  	"	s->mreached = (ulong) mreached;",
  	"	s->vsize    = (ulong) vsize;",
  	"	s->errors   = (int) errors;",
  	"	s->memcnt   = (double) memcnt;",
  	"	s->nstates  = (double) nstates;",
  	"	s->nlinks   = (double) nlinks;",
  	"	s->truncs   = (double) truncs;",
  	"	s->memory_left = (ulong) bfs_left;",
  	"	s->punted      = (ulong) bfs_punt;",
  	"	bfs_snapped++; /* for bfs_best */",
  	"}",
  	"",
  	"void",
  	"bfs_shutdown(const char *s)",
  	"{",
  	"	bfs_clear_locks(); /* in case we interrupted at a bad point */",
  	"	if (!strstr(s, \"early \") || verbose)",
  	"	{	bfs_printf(\"stop (%%s)\\n\", s);",
  	"	}",
  	"	bfs_update();",
  	"	if (who_am_i == 0)",
  	"	{	wrapup();",
  	"#ifdef BFS_DISK",
  	"		bfs_disk_stop();",
  	"#endif",
  	"	}",
  	"	bfs_mark_done(2);",
  	"	pan_exit(2);",
  	"}",
  	"",
  	"SV_Hold *bfs_free_hold;",
  	"",
  	"SV_Hold *",
  	"bfs_get_hold(void)",
  	"{	SV_Hold *x;",
  	"	if (bfs_free_hold)",
  	"	{	x = bfs_free_hold;",
  	"		bfs_free_hold = bfs_free_hold->nxt;",
  	"	} else",
  	"	{	x = (SV_Hold *) sh_malloc((ulong) sizeof(SV_Hold));",
  	"	}",
  	"	return x;",
  	"}",
  	"",
  	"BFS_Trail *",
  	"bfs_unpack_state(BFS_Slot *n)		/* called in bfs_explore_state */",
  	"{	BFS_Trail *otrpt;",
  	"	BFS_State *bfs_t;",
  	"	int vecsz;",
  	"",
  	"	if (!n || !n->s_data || !n->s_data->t_info)",
  	"	{	bfs_Uerror(\"internal error\");",
  	"	}",
  	"	otrpt = (BFS_Trail *) ((BFS_State *) n->s_data)->t_info;",
  	"",
  	"	trpt->ostate = otrpt->ostate;",
  	"	trpt->st     = otrpt->st;",
  	"	trpt->o_tt   = otrpt->o_tt;",
  	"	trpt->pr     = otrpt->pr;",
  	"	trpt->tau    = otrpt->tau;",
  	"	trpt->o_pm   = otrpt->o_pm;",
  	"	if (trpt->ostate)",
  	"	trpt->o_t    = t_id_lkup[otrpt->t_id];",
  	"#if defined(C_States) && (HAS_TRACK==1)",
  	"	c_revert((uchar *) &(now.c_state[0]));",
  	"#endif",
  	"	if (trpt->o_pm & 4)			/* rv succeeded */",
  	"	{	return (BFS_Trail *) 0;		/* revisit not needed */",
  	"	}",
  	"#ifndef NOREDUCE",
  	"	bfs_nps = 0;",
  	"#endif",
  	"	if (trpt->o_pm & 8)			/* rv attempt failed */",
  	"	{	revrv++;",
  	"		if (trpt->tau&8)",
  	"		{	trpt->tau &= ~8;	/* break atomic */",
  	"#ifndef NOREDUCE",
  	"		} else if (trpt->tau&32)	/* void preselection */",
  	"		{	trpt->tau &= ~32;",
  	"			bfs_nps = 1;		/* no preselection in repeat */",
  	"#endif",
  	"	}	}",
  	"	trpt->o_pm &= ~(4|8);",
  	"	if (trpt->o_tt > mreached)",
  	"	{	static ulong nr = 0L, nc;",
  	"		mreached = trpt->o_tt;",
  	"		nc = (long) nstates/FREQ;",
  	"		if (nc > nr)",
  	"		{	nr = nc;",
  	"			bfs_snapshot();",
  	"	}	}",
  	"	depth = trpt->o_tt;",
  	"	if (depth >= maxdepth)",
  	"	{",
  	"#if SYNC",
  	"		if (boq != -1)",
  	"		{	BFS_Trail *x = (BFS_Trail *) trpt->ostate;",
  	"			if (x) x->o_pm |= 4; /* rv not failing */",
  	"		}",
  	"#endif",
  	"		truncs++;",
  	"		if (!warned)",
  	"		{	warned = 1;",
  	"			bfs_printf(\"error: max search depth too small\\n\");",
  	"		}",
  	"		if (bounded)",
  	"		{	bfs_uerror(\"depth limit reached\");",
  	"		}",
  	"		return (BFS_Trail *) 0;",
  	"	}",
  	"",
  	"	bfs_t = n->s_data;",
  	"#if NRUNS>0",
  	"	vsize = bfs_t->omask->sz;",
  	"#else",
  	"	vsize = ((State *) (bfs_t->osv))->_vsz;",
  	"#endif",
  	"#if SYNC",
  	"	boq   = bfs_t->boq;",
  	"#endif",
  	"",
  	"#if defined(Q_PROVISO) && !defined(BITSTATE) && defined(FULLSTACK)",
  	"	#ifdef USE_TDH",
  	"		if (((uchar *)(bfs_t->lstate)))		/* if BFS_INQ is set */",
  	"		{	*((uchar *) bfs_t->lstate) = 0;	/* turn it off */",
  	"		}",
  	"	#else",
  	"		if (bfs_t->lstate)			/* bfs_par */",
  	"		{	bfs_t->lstate->tagged = 0;	/* bfs_par state removed from q */",
  	"		}",
  	"	#endif",
  	"#endif",
  	"	memcpy((char *) &now, (uchar *) bfs_t->osv, vsize);",
  	"#if !defined(NOCOMP) && !defined(HC) && NRUNS>0",
  	"	Mask = (uchar *) bfs_t->omask->sv;	/* in shared memory */",
  	"#endif",
  	"#ifdef BFS_CHECK",
  	"	if (0) bfs_dump_now(\"got1\");",
  	"#endif",
  	"#ifdef TRIX",
  	"	re_populate();",
  	"#else",
  	"	#if NRUNS>0",
  	"		if (now._nr_pr > 0)",
  	"		{",
  	"		#if VECTORSZ>32000",
  	"			proc_offset = (int *) bfs_t->omask->po;",
  	"		#else",
  	"			proc_offset = (short *) bfs_t->omask->po;",
  	"		#endif",
  	"			proc_skip   = (uchar *) bfs_t->omask->ps;",
  	"		}",
  	"		if (now._nr_qs > 0)",
  	"		{",
  	"		#if VECTORSZ>32000",
  	"			q_offset = (int *) bfs_t->omask->qo;",
  	"		#else",
  	"			q_offset = (short *) bfs_t->omask->qo;",
  	"		#endif",
  	"			q_skip   = (uchar *) bfs_t->omask->qs;",
  	"		}",
  	"	#endif",
  	"#endif",
  	"	vecsz = ((State *) bfs_t->osv)->_vsz;",
  	"#ifdef BFS_CHECK",
  	"	assert(vecsz > 0 && vecsz < VECTORSZ);",
  	"#endif",
  	"	{ SV_Hold *x = bfs_get_hold();",
  	"		x->sv  = bfs_t->osv;",
  	"		x->nxt = bfs_svfree[vecsz];",
  	"		bfs_svfree[vecsz] = x;",
  	"		bfs_t->osv = (State *) 0;",
  	"	}",
  	"#if NRUNS>0",
  	"	bfs_keep(bfs_t->omask);",
  	"#endif",
  	"",
  	"#ifdef BFS_CHECK",
  	"	if (0) bfs_dump_now(\"got2\");",
  	"	if (0) view_state(\"after\");",
  	"#endif",
  	"	return (BFS_Trail *) bfs_t->t_info;",
  	"}",
  	"void",
  	"bfs_initial_state(void)",
  	"{",
  	"#ifdef BFS_CHECK",
  	"	assert(trpt != NULL);",
  	"#endif",
  	"	trpt->ostate = (H_el *) 0;",
  	"	trpt->o_tt   = -1;",
  	"	trpt->tau    = 0;",
  	"#ifdef VERI",
  	"	trpt->tau |= 4;	/* claim moves first */",
  	"#endif",
  	"	bfs_store_state(trpt, boq);	/* initial state : bfs_lib.c */",
  	"}",
  	"",
  	"#ifdef BITSTATE",
  	"		#define bfs_do_store(v, n) b_store(v, n)",
  	"#else",
  	"	#ifdef USE_TDH",
  	"		#define bfs_do_store(v, n) o_store(v, n)",
  	"	#else",
  	"		#define bfs_do_store(v, n) h_store(v, n)",
  	"	#endif",
  	"#endif",
  	"",
  	"#ifdef BFS_SEP_HASH",
  	"int",
  	"bfs_seen_before(void)",
  	"{	/* cannot set trpt->tau |= 64 to mark successors outside stack */",
  	"	/* since the check is done remotely and the trpt value is gone */",
  	" #ifdef VERI",
  	"	if (!trpt->ostate		/* initial state */",
  	"	|| ((trpt->tau&4)		/* starting claim moves(s) */",
  	"	&& !(((BFS_Trail *)trpt->ostate)->tau&4))) /* prev move: prog */",
  	"	{	return 0; /* claim move: mid-state not stored */",
  	"	} /* else */",
  	" #endif",
  	"	if (!bfs_do_store((char *)&now, vsize))	/* sep_hash */",
  	"	{	nstates++;		/* local count */",
  	"		return 0;		/* new state */",
  	"	}",
  	" #ifdef BFS_CHECK",
  	"	bfs_printf(\"seen before\\n\");",
  	" #endif",
  	"	truncs++;",
  	"	return 1;			/* old state */",
  	"}",
  	"#endif",
  	"",
  	"void",
  	"bfs_explore_state(BFS_Slot *v)		/* generate all successors of v */",
  	"{	BFS_Trail *otrpt;",
  	"	Trans *t;",
  	"#ifdef HAS_UNLESS",
  	"	int E_state;",
  	"#endif",
  	"	int tt;",
  	"	short II, To = BASE, From = (short) (now._nr_pr-1);",
  	"	short oboq = boq;",
  	"	uchar _n, _m, ot;",
  	"",
  	"	memset(ntrpt, 0, sizeof(Trail));",
  	"	otrpt = bfs_unpack_state(v); /* BFS_Trail */",
  	"",
  	"	if (!otrpt) { return; } /* e.g., depth limit reached */",
  	"#ifdef L_BOUND",
  	"	#if defined(VERBOSE)",
  	"	bfs_printf(\"Unpacked state with l_bound %%d -- sds %%p\\n\",",
  	"		now._l_bnd, now._l_sds);",
  	"	#endif",
  	"#endif",
  	"",
  	"#if defined(C_States) && (HAS_TRACK==1)",
  	"	c_revert((uchar *) &(now.c_state[0]));",
  	"#endif",
  	"",
  	"#ifdef BFS_SEP_HASH",
  	"	if (bfs_seen_before()) return;",
  	"#endif",
  	"",
  	"#ifdef VERI",	
  	"	if (now._nr_pr == 0	/* claim terminated */",
  	"	||  stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])",
  	"	{	bfs_uerror(\"end state in claim reached\");",
  	"	}",
  	"#endif",
  	"	trpt->tau &= ~1;	/* timeout off */",
  	"#ifdef VERI",
  	"	if (trpt->tau&4)	/* claim move */",
  	"	{	trpt->tau |= (otrpt->tau)&1; /* inherit from prog move */",
  	"		From = To = 0;	/* claim */",
  	"		goto Repeat_two;",
  	"	}",
  	"#endif",
  	"#ifndef NOREDUCE",
  	"	if (boq == -1 && !(trpt->tau&8) && bfs_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)",
  	"		{	t = trans[ot][tt];",
  	"			if (t->qu[0] != 0)",
  	"			{	if (!q_cond(II, t))",
  	"					continue;",
  	"			}",
  	"			From = To = II;",
  	"			trpt->tau |= 32; /* preselect marker */",
  	"	#ifdef VERBOSE",
  	"			bfs_printf(\"%%3ld: proc %%d PreSelected (tau=%%d)\\n\", ",
  	"				depth, II, trpt->tau);",
  	"	#endif",
  	"			goto Repeat_two;",
  	"	}	}",
  	"	trpt->tau &= ~32;",
  	"#endif",
  	"",
  	"Repeat_one:",
  	"	if (trpt->tau&8)",
  	"	{	From = To = (short ) trpt->pr;	/* atomic */",
  	"	} else",
  	"	{	From = now._nr_pr-1;",
  	"		To = BASE;",
  	"	}",
  	"#if defined(VERI) || !defined(NOREDUCE) || defined(ETIM)",
  	"Repeat_two: /* MainLoop */",
  	"#endif",
  	"	_n = _m = 0;",
  	"	for (II = From; II >= To; II -= 1)	/* all processes */",
  	"	{",
  	"#ifdef BFS_CHECK",
  	"		bfs_printf(\"proc %%d (%%d - %%d)\\n\", II, From, To);",
  	"#endif",
  	"#if SYNC	",
  	"		if (boq != -1 && trpt->pr == II)",
  	"		{	continue;	/* no rendezvous with same proc */",
  	"		}",
  	"#endif",
  	"		this = pptr(II);",
  	"		tt = (int) ((P0 *)this)->_p;",
  	"		ot = (uchar) ((P0 *)this)->_t;",
  	"		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_PRIORITY",
  	"		if (!highest_priority(((P0 *)this)->_pid, II, t))",
  	"		{	continue;",
  	"		}",
  	"#else",
  	"	#ifdef HAS_PROVIDED",
  	"		if (!provided(II, ot, tt, t))",
  	"		{	continue;",
  	"		}",
  	"	#endif",
  	"#endif",
  	"#ifdef HAS_UNLESS",
  	"		E_state = 0;",
  	"#endif",
  	"		for (t = trans[ot][tt]; t; t = t->nxt)	/* all process transitions */",
  	"		{",
  	"#ifdef BFS_CHECK",
  	"			assert(t_id_lkup[t->t_id] == t); /* for reverse lookup in bfs_unpack_state */",
  	"#endif",
  	"#ifdef VERBOSE",
  	"			if (0) bfs_printf(\"\\tproc %%d tr %%d\\n\", II, t->forw);",
  	"#endif",
  	"#ifdef HAS_UNLESS",
  	"			if (E_state > 0",
  	"			&&  E_state != t->e_trans)",
  	"				break;",
  	"#endif",
  	"			/* trpt->o_t = */ 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 VERBOSE",
  	"			e_critical(BFS_PRINT);",
  	"			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);",
  	"			x_critical(BFS_PRINT);",
  	"#endif",
  	"#ifdef HAS_UNLESS",
  	"			E_state = t->e_trans;",
  	"	#if SYNC>0",
  	"			if (t->e_trans > 0 && boq != -1)",
  	"			{ fprintf(efd, \"error:	rendezvous stmnt in the escape clause\\n\");",
  	"			  fprintf(efd, \"	of unless stmnt not compatible with -DBFS\\n\");",
  	"			  pan_exit(1);",
  	"			}",
  	"	#endif",
  	"#endif",
  	"			if (t->st > 0)",
  	"			{	((P0 *)this)->_p = t->st;",
  	"			}",
  	"			/* use the ostate ptr, with type *H_el, to temporarily store *BFS_Trail */",
  	"#ifdef BFS_NOTRAIL",
  	"			ntrpt->ostate = (H_el *) 0;	/* no error-traces in this mode */",
  	"#else",
  	"			ntrpt->ostate = (H_el *) otrpt;	/* parent stackframe */",
  	"#endif",
  	"		/*	ntrpt->st = tt;		* was already set above */",
  	"",
  	"			if (boq == -1 && (t->atom&2))	/* atomic */",
  	"			{	ntrpt->tau = 8;		/* record for next move */",
  	"			} else",
  	"			{	ntrpt->tau = 0;		/* no timeout or preselect etc */",
  	"			}",
  	"#ifdef VERI",
  	"			ntrpt->tau |= trpt->tau&4;	/* if claim, inherit */",
  	"			if (boq == -1 && !(ntrpt->tau&8))	/* unless rv or atomic */",
  	"			{	if (ntrpt->tau&4)	/* claim */",
  	"				{	ntrpt->tau &= ~4; /* switch to prog */",
  	"				} else",
  	"				{	ntrpt->tau |=  4; /* switch to claim */",
  	"			}	}",
  	"#endif",
  	"#ifdef L_BOUND",
  	"			{  uchar obnd = now._l_bnd;",
  	"			   uchar *os  = now._l_sds;",
  	"	#ifdef VERBOSE",
  	"			   bfs_printf(\"saving bound %%d -- sds %%p\\n\", obnd, (void *) os);",
  	"	#endif",
  	"#endif",
  	"",
  	"			   bfs_store_state(ntrpt, oboq);",
  	"#ifdef EVENT_TRACE",
  	"			   now._event = trpt->o_event;",
  	"#endif",
  	"			   /* undo move and generate other successor states */",
  	"			   trpt++;	/* this is where ovals and ipt are set */",
  	"			   do_reverse(t, II, _m);	/* restore now. */",
  	"#ifdef L_BOUND",
  	"	#ifdef VERBOSE",
  	"			   bfs_printf(\"restoring bound %%d -- sds %%p\\n\", obnd, (void *) os);",
  	"	#endif",
  	"			   now._l_bnd = obnd;",
  	"			   now._l_sds = os;",
  	"			}",
  	"#endif",
  	"			trpt--;",
  	"#ifdef VERBOSE",
  	"			e_critical(BFS_PRINT);",
  	"			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, 0);",
  	"			printf(\"tau=%%d,%%d]\\n\", trpt->tau, (trpt-1)->tau);",
  	"			x_critical(BFS_PRINT);",
  	"#endif",
  	"			reached[ot][t->st] = 1;",
  	"			reached[ot][tt]    = 1;",
  	"",
  	"			((P0 *)this)->_p = tt;",
  	"			_n |= _m;",
  	"	}	}",
  	"#ifdef VERBOSE",
  	"	bfs_printf(\"done _n = %%d\\n\", _n);",
  	"#endif",
  	"",
  	"#ifndef NOREDUCE",
  	"	/* preselected - no succ definitely outside stack */",
  	"	if ((trpt->tau&32) && !(trpt->tau&64))",
  	"	{	From = now._nr_pr-1; To = BASE;",
  	"	#ifdef VERBOSE",
  	"		bfs_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 Repeat_two;",
  	"	}",
  	"	trpt->tau &= ~(32|64);",
  	"#endif",
  	"	if (_n == 0",
  	"#ifdef VERI",
  	"	&& !(trpt->tau&4)",
  	"#endif",
  	"	)",
  	"	{	/* no successor states generated */",
  	"		if (boq != -1)				/* was rv move */",
  	"		{	BFS_Trail *x = (BFS_Trail *) trpt->ostate; /* pre-rv state */",
  	"			if (x && ((x->tau&8) || (x->tau&32))) /* break atomic or preselect */",
  	"			{	x->o_pm |= 8;		/* mark failure */",
  	"				this = pptr(otrpt->pr);",
  	"				((P0 *) this)->_p = otrpt->st;	/* reset state */",
  	"				unsend(boq);		/* retract rv offer */",
  	"				boq = -1;",
  	"#ifdef VERBOSE",
  	"				printf(\"repush state\\n\");",
  	"#endif",
  	"				bfs_push_state(NULL, x, x->o_tt); /* repush rv fail */",
  	"			} /* else the rv need not be retried */",
  	"		} else if (now._nr_pr > BASE)		/* possible deadlock */",
  	"		{	if ((trpt->tau&8))		/* atomic step blocked */",
  	"			{	trpt->tau &= ~(1|8);	/* 1=timeout, 8=atomic */",
  	"				goto Repeat_one;",
  	"			}",
  	"#ifdef ETIM",
  	"			/* if timeouts were used in the model */",
  	"			if (!(trpt->tau&1))",
  	"			{	trpt->tau |= 1;		/* enable timeout */",
  	"				goto Repeat_two;",
  	"			}",
  	"#endif",
  	"			if (!noends && !endstate())",
  	"			{	bfs_uerror(\"invalid end state.\");",
  	"			}",
  	"		}",
  	"#ifdef VERI",
  	"		else /* boq == -1 && now._nr_pr == BASE && trpt->tau != 4 */",
  	"		{	trpt->tau |= 4; /* switch to claim for stutter moves */",
  	"	#ifdef VERBOSE",
  	"			printf(\"%%3ld: proc -1 exec -1, (stutter move)\\n\", depth, II);",
  	"	#endif",
  	"			bfs_store_state(trpt, boq);", 
  	"	#ifdef VERBOSE",
  	"			printf(\"%%3ld: proc -1 reverses -1, (stutter move)\\n\", depth, II);",
  	"	#endif",
  	"			trpt->tau &= ~4; /* undo, probably not needed */",
  	"		}",
  	"#endif",
  	"	}",
  	"#ifdef BFS_NOTRAIL",
  	"	bfs_release_trail(otrpt);",
  	"#endif",
  	"}",
  	"#if !defined(BFS_FIFO) && !defined(BFS_NORECYCLE)",
  	"void",
  	"bfs_recycle(BFS_Slot *n)",
  	"{",
  	"	#ifdef BFS_CHECK",
  	"	 assert(n != &bfs_null);",
  	"	#endif",
  	"	n->nxt = bfs_free_slot;",
  	"	bfs_free_slot = n;",
  	"",
  	"	#ifdef BFS_CHECK",
  	"	 bfs_printf(\"recycles %%s -- %%p\\n\",",
  	"		n->s_data?\"STATE\":\"EMPTY\", (void *) n);",
  	"	#endif",
  	"}",
  	"#endif",
  	"#ifdef BFS_FIFO",
  	"int",
  	"bfs_empty(int p)",	
  	"{	int i;",
  	"	const int dst = 0;",
  	"	for (i = 0; i < Cores; i++)",
  	"	{	if (shared_memory->head[dst][p][i] != (BFS_Slot *) 0)",
  	"		{",
  	"			volatile BFS_Slot *x = shared_memory->head[dst][p][i];",
  	"			while (x && x->type == DELETED)",
  	"			{	x = x->nxt;",
  	"			}",
  	"			if (!x)",
  	"			{	continue;",
  	"			}",
  	"			if (p == who_am_i)",
  	"			{	shared_memory->head[dst][p][i] = x;",
  	"			}",
  	"	#ifdef BFS_CHECK",
  	"			bfs_printf(\"input q [%%d][%%d][%%d] !empty\\n\",",
  	"				dst, p, i);",
  	"	#endif",
  	"			return i;",
  	"	}	}",
  	"	#ifdef BFS_CHECK",
  	"	 bfs_printf(\"all input qs [%%d][%%d][0..max] empty\\n\",",
  	"		dst, p);",
  	"	#endif		",
  	"	return Cores;",
  	"}",
  	"#endif",
  	"#ifdef BFS_DISK",
  	"void",
  	"bfs_ewrite(int fd, const void *p, size_t count)",
  	"{",
  	"	if (write(fd, p, count) != count)",
  	"	{	perror(\"diskwrite\");",
  	"		Uerror(\"aborting\");",
  	"	}",
  	"}",
  	"",
  	"void",
  	"bfs_eread(int fd, void *p, size_t count)",
  	"{",
  	"	if (read(fd, p, count) != count)",
  	"	{	perror(\"diskread\");",
  	"		Uerror(\"aborting\");",
  	"	}",
  	"}",
  	"",
  	"void",
  	"bfs_sink_disk(int who_are_you, BFS_Slot *n)",
  	"{	SV_Hold *x;",
  	"#ifdef VERBOSE",
  	"	bfs_printf(\"sink_disk -> %%d\\n\", who_are_you);",
  	"#endif",
  	"	bfs_ewrite(bfs_out_fd[who_are_you], (const void *) n->s_data->t_info, sizeof(BFS_Trail));",
  	"	bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &vsize, sizeof(ulong));",
  	"	bfs_ewrite(bfs_out_fd[who_are_you], &now, vsize);",
  	"",
  	"	bfs_release_trail(n->s_data->t_info);",
  	"	n->s_data->t_info = (BFS_Trail *) 0;",
  	"",
  	"#if NRUNS>0",
  	"	bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->omask), sizeof(EV_Hold *));",
  	"#endif",
  	"#ifdef Q_PROVISO",
  	"	bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->lstate), sizeof(H_el *));",
  	"#endif",
  	"#if SYNC>0",
  	"	bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->boq), sizeof(short));",
  	"#endif",
  	"#if VERBOSE",
  	"	bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->nr), sizeof(ulong));",
  	"#endif",
  	"	shared_memory->bfs_out_cnt[who_am_i] = 1;", 
  	"}",
  	"void",
  	"bfs_source_disk(int fd, volatile BFS_Slot *n)",
  	"{	ulong	  nb; /* local temporary */",
  	"	SV_Hold  *x;",
  	"#ifdef VERBOSE",
  	"	bfs_printf(\"source_disk <- %%d\\n\", who_am_i);",
  	"#endif",
  	"	n->s_data->t_info = bfs_grab_trail();",
  	"	bfs_eread(fd, (void *) n->s_data->t_info, sizeof(BFS_Trail));",
  	"	bfs_eread(fd, (void *) &nb, sizeof(ulong));",
  	"",
  	"	x = bfs_new_sv(nb);	/* space for osv isn't already allocated */",
  	"	n->s_data->osv = x->sv;",
  	"	x->sv = (State *) 0;",
  	"	x->nxt = bfs_free_hold;",
  	"	bfs_free_hold = x;",
  	"",
  	"	bfs_eread(fd, (void *) n->s_data->osv, (size_t) nb);",
  	"#if NRUNS>0",
  	"	bfs_eread(fd, (void *) &(n->s_data->omask), sizeof(EV_Hold *));",
  	"#endif",
  	"#ifdef Q_PROVISO",
  	"	bfs_eread(fd, (void *) &(n->s_data->lstate), sizeof(H_el *));",
  	"#endif",
  	"#if SYNC>0",
  	"	bfs_eread(fd, (void *) &(n->s_data->boq), sizeof(short));",
  	"#endif",
  	"#if VERBOSE",
  	"	bfs_eread(fd, (void *) &(n->s_data->nr), sizeof(ulong));",
  	"#endif",
  	"}",
  	"#endif",
  	"",
  	"#ifndef BFS_QSZ",
  	" #ifdef BFS_STAGGER",
  	"static BFS_Slot *bfs_stage[BFS_STAGGER];",
  	"",
  	"static void",
  	"bfs_stagger_flush(void)",
  	"{	int i, who_are_you;",
  	"	int dst = 1 - bfs_toggle;",
  	"	BFS_Slot *n;",
  	"	who_are_you = (rand()%%Cores);", 
  	"	for (i = bfs_stage_cnt-1; i >= 0; i--)",
  	"	{	n = bfs_stage[i];",
  	" #ifdef BFS_DISK",
  	"		bfs_sink_disk(who_are_you, n);",
  	"		bfs_stage[i] = (BFS_Slot *) 0;",
  	" #endif",
  	"		n->nxt = (BFS_Slot *) shared_memory->head[dst][who_are_you][who_am_i];",
  	"		shared_memory->head[dst][who_are_you][who_am_i] = n;",
  	"		/* bfs_sent++; */",
  	"	}",
  	"	#ifdef VERBOSE",
  	"		bfs_printf(\"stagger flush %%d states to %%d\\n\",",
  	"			bfs_stage_cnt, who_are_you);",
  	"	#endif",
  	"	bfs_stage_cnt = 0;",
  	"}",
  	"",
  	"void",
  	"bfs_stagger_add(BFS_Slot *n)",
  	"{",
  	"	if (bfs_stage_cnt == BFS_STAGGER)",
  	"	{	bfs_stagger_flush();",
  	"	}",
  	"	bfs_stage[bfs_stage_cnt++] = n;",
  	"}",
  	" #endif",
  	"#endif",
  	"",
  	"void",
  	"bfs_push_state(Trail *x, BFS_Trail *y, int tt)",
  	"{	int who_are_you;",
  	"#ifdef BFS_FIFO",
  	"	const int dst = 0;",
  	"#else",
  	"	int dst = 1 - bfs_toggle;",
  	"#endif",
  	"#ifdef BFS_QSZ",
  	"	uint z;",
  	"	if (bfs_keep_state > 0)",
  	"	{	who_are_you = bfs_keep_state - 1;",
  	"	} else",
  	"	{	who_are_you = (rand()%%Cores);",
  	"	}",
  	"	z = shared_memory->bfs_ix[dst][who_are_you][who_am_i];",
  	"	if (z >= BFS_QSZ)",
  	"	{	static int warned_qloss = 0;",
  	"		if (warned_qloss == 0 && who_am_i == 0)",
  	"		{	warned_qloss++;",
  	"			bfs_printf(\"BFS_QSZ too small - losing states\\n\");",
  	"		}",
  	"		bfs_punt++;",
  	"		return;",
  	"	}",
  	"	shared_memory->bfs_ix[dst][who_are_you][who_am_i] = z+1;",
  	"	BFS_Slot *n = bfs_pack_state(x, y, tt, bfs_prep_slot(y, ",
  	"		(BFS_Slot *) &(shared_memory->bfsq[dst][who_are_you][who_am_i][z])));",
  	"#else",
  	"	BFS_Slot *n = bfs_pack_state(x, y, tt, bfs_new_slot(y));",
  	"",
  	" #ifdef BFS_GREEDY",
  	"	who_are_you = who_am_i; /* for testing only */",
  	" #else",
  	"	if (bfs_keep_state > 0)",
  	"	{	who_are_you = bfs_keep_state - 1;",
  	"	} else",
  	"	{",
  	"	#ifdef BFS_STAGGER",
  	"		who_are_you = -1;",
  	"		bfs_stagger_add(n);",
  	"		goto done;",
  	"	#else",
  	"		who_are_you = (rand()%%Cores);",
  	"	#endif",
  	"	}",
  	" #endif",
  	" #ifdef BFS_FIFO",
  	"	  if (!shared_memory->tail[dst][who_are_you][who_am_i])",
  	"	  {	shared_memory->dels[dst][who_are_you][who_am_i] =",
  	"		shared_memory->tail[dst][who_are_you][who_am_i] =",
  	"		shared_memory->head[dst][who_are_you][who_am_i] = n;",
  	"	  } else",
  	"	  {	shared_memory->tail[dst][who_are_you][who_am_i]->nxt = n;",
  	"		shared_memory->tail[dst][who_are_you][who_am_i] = n;",
  	"	  }",
  	"	  shared_memory->bfs_idle[who_are_you] = 0;",
  	" #else",
  	"  #ifdef BFS_DISK",
  	"	  bfs_sink_disk(who_are_you, n);",
  	"  #endif",
  	"	  n->nxt = (BFS_Slot *) shared_memory->head[dst][who_are_you][who_am_i];",
  	"	  shared_memory->head[dst][who_are_you][who_am_i] = n;",
  	" #endif",
  	" #ifdef BFS_STAGGER",
  	"done:",
  	" #endif",
  	"#endif", 
  	"#ifdef VERBOSE",
  	"	bfs_printf(\"PUT STATE (depth %%ld, nr %%u) to %%d -- s_data: %%p\\n\",",
  	"		tt, n->s_data->nr, who_are_you, n->s_data);",
  	"#endif",
  	"	bfs_sent++;",
  	"}",
  	"",
  	"BFS_Slot *",
  	"bfs_next(void)",
  	"{	volatile BFS_Slot *n = &bfs_null;",
  	" #ifdef BFS_FIFO",
  	"	const int src = 0;",
  	"	bfs_qscan = bfs_empty(who_am_i);",
  	" #else",
  	"	const int src = bfs_toggle;",
  	"  #ifdef BFS_QSZ",
  	"	while (bfs_qscan < Cores",
  	"	&& shared_memory->bfs_ix[src][who_am_i][bfs_qscan] == 0)",
  	"	{	bfs_qscan++;",
  	"	}",
  	"  #else",
  	"	while (bfs_qscan < Cores",
  	"	&& shared_memory->head[src][who_am_i][bfs_qscan] == (BFS_Slot *) 0)",
  	"	{	bfs_qscan++;",
  	"	}",
  	"  #endif",
  	" #endif",
  	"	if (bfs_qscan < Cores)",
  	"	{",
  	" #ifdef BFS_FIFO",			
  	"		shared_memory->bfs_idle[who_am_i] = 0;",
  	"		for (n = shared_memory->head[src][who_am_i][bfs_qscan]; n; n = n->nxt)",
  	"		{	if (n->type != DELETED)",
  	"			{	break;",
  	"		}	}",
  	"	#ifdef BFS_CHECK",
  	"		assert(n && n->type == STATE); /* q cannot be empty */",
  	"	#endif",
  	"		if (n->nxt)",
  	"		{	shared_memory->head[src][who_am_i][bfs_qscan] = n->nxt;",
  	"		}",	
  	"		n->type = DELETED;",
  	" #else",
  	"	#ifdef BFS_QSZ",
  	"		uint x = --shared_memory->bfs_ix[src][who_am_i][bfs_qscan];",
  	"		n = &(shared_memory->bfsq[src][who_am_i][bfs_qscan][x]);",
  	"	#else",
  	"		n = shared_memory->head[src][who_am_i][bfs_qscan];",
  	"		shared_memory->head[src][who_am_i][bfs_qscan] = n->nxt;",
  	"		#if defined(BFS_FIFO) && defined(BFS_CHECK)",
  	"			assert(n->type == STATE);",
  	"		#endif",
  	"		n->nxt = (BFS_Slot *) 0;",
  	"	#endif",
  	"	#ifdef BFS_DISK",
  	"		/* the states actually show up in reverse order (FIFO iso LIFO) here */",
  	"		/* but that doesnt really matter as long as the count is right */",
  	"		bfs_source_disk(bfs_inp_fd[bfs_qscan], n); /* get the data */",
  	"	#endif",
  
  	" #endif",
  	" #ifdef BFS_CHECK",
  	"		bfs_printf(\"rcv STATE from [%%d][%%d][%%d]\\n\",",
  	"			src, who_am_i, bfs_qscan);",
  	" #endif",
  	"		bfs_rcvd++;",
  	"	} else",
  	"	{",
  	" #if defined(BFS_STAGGER) && !defined(BFS_QSZ)",
  	"		if (bfs_stage_cnt > 0)",
  	"		{	bfs_stagger_flush();",
  	"		}",
  	" #endif",
  	"		shared_memory->bfs_idle[who_am_i] = 1;",
  	" #if defined(BFS_FIFO) && defined(BFS_CHECK)",
  	"		assert(n->type == EMPTY);",
  	" #endif",
  	"	}",
  	"	return (BFS_Slot *) n;",
  	"}",
  	"",
  	"int",
  	"bfs_all_empty(void)",
  	"{	int i;",
  	"#ifdef BFS_DISK",
  	"	for (i = 0; i < Cores; i++)",
  	"	{	if (shared_memory->bfs_out_cnt[i] != 0)",
  	"		{",
  	"  #ifdef VERBOSE",
  	"			bfs_printf(\"bfs_all_empty %%d not empty\\n\", i);",
  	"  #endif",
  	"			return 0;",
  	"	}	}",
  	"#else",
  	"	int p;",
  	"  #ifdef BFS_FIFO",
  	"	const int dst = 0;",
  	"  #else",
  	"	int dst = 1 - bfs_toggle; /* next generation */",
  	"  #endif",
  	"	for (p = 0; p < Cores; p++)",
  	"	for (i = 0; i < Cores; i++)",
  	"  #ifdef BFS_QSZ",
  	"	{	if (shared_memory->bfs_ix[dst][p][i] > 0)",
  	"  #else",
  	"	{	if (shared_memory->head[dst][p][i] != (BFS_Slot *) 0)",
  	"  #endif",
  	"		{	return 0;",
  	"	}	}",
  	"#endif",
  	"#ifdef VERBOSE",
  	"	bfs_printf(\"bfs_all_empty\\n\");",
  	"#endif",
  	"	return 1;",
  	"}",
  	"",
  	"#ifdef BFS_FIFO",
  	"BFS_Slot *",
  	"bfs_sweep(void)",
  	"{	BFS_Slot *n;",
  	"	int i;",
  	"	for (i = 0; i < Cores; i++)",
  	"	for (n = (BFS_Slot *) shared_memory->dels[0][who_am_i][i];",
  	"		n && n != shared_memory->head[0][who_am_i][i];",
  	"		n = n->nxt)",
  	"	{	if (n->type == DELETED && n->nxt)",
  	"		{	shared_memory->dels[0][who_am_i][i] = n->nxt;",
  	"			n->nxt = (BFS_Slot *) 0;",
  	"			return n;",
  	"	}	}",
  	"	return (BFS_Slot *) sh_malloc((ulong) sizeof(BFS_Slot));",
  	"}",
  	"#endif",
  	"",
  	"typedef struct BFS_T_Hold BFS_T_Hold;",
  	"struct BFS_T_Hold {",
  	"	volatile BFS_Trail *t;",
  	"	BFS_T_Hold *nxt;",
  	"};",
  	"BFS_T_Hold *bfs_t_held, *bfs_t_free;",
  	"",
  	"BFS_Trail *",
  	"bfs_grab_trail(void)",			
  	"{	BFS_Trail *t;",
  	"	BFS_T_Hold *h;",
  	"",
  	"#ifdef VERBOSE",
  	"	bfs_printf(\"grab trail - bfs_t_held %%p\\n\", (void *) bfs_t_held);",
  	"#endif",
  	"	if (bfs_t_held)",
  	"	{	h = bfs_t_held;",
  	"		bfs_t_held = bfs_t_held->nxt;",
  	"		t = (BFS_Trail *) h->t;",
  	"		h->t = (BFS_Trail *) 0; /* make sure it cannot be reused */",
  	"		h->nxt = bfs_t_free;",
  	"		bfs_t_free = h;",
  	"",
  	"	} else",
  	"	{	t = (BFS_Trail *) sh_malloc((ulong) sizeof(BFS_Trail));",
  	"	}",
  	"#ifdef BFS_CHECK",
  	"	assert(t);",
  	"#endif",
  	"	t->ostate = (H_el *) 0;",
  	"#ifdef VERBOSE",
  	"	bfs_printf(\"grab trail %%p\\n\", (void *) t);",
  	"#endif",
  	"	return t;",
  	"}",
  	"",
  	"#if defined(BFS_DISK) || defined(BFS_NOTRAIL)",
  	"void",
  	"bfs_release_trail(BFS_Trail *t)",	
  	"{	BFS_T_Hold *h;",
  	" #ifdef BFS_CHECK",
  	"	assert(t);",
  	" #endif",
  	" #ifdef VERBOSE",
  	"	bfs_printf(\"release trail %%p\\n\", (void *) t);",
  	"	#endif",
  	"	if (bfs_t_free)",
  	"	{	h = bfs_t_free;",
  	"		bfs_t_free = bfs_t_free->nxt;",
  	"	} else",
  	"	{	h = (BFS_T_Hold *) emalloc(sizeof(BFS_T_Hold));",
  	"	}",
  	"	h->t = t;",
  	"	h->nxt = bfs_t_held;",
  	"	bfs_t_held = h;",
  	" #ifdef VERBOSE",
  	"	bfs_printf(\"release trail - bfs_t_held %%p\\n\", (void *) bfs_t_held);",
  	" #endif",
  	"}",
  	"#endif",
  	"",
  	"#ifndef BFS_QSZ",
  	"BFS_Slot *",
  	"bfs_new_slot(BFS_Trail *f)",
  	"{	BFS_Slot *t;",
  	"",
  	"#ifdef BFS_FIFO",
  	"	t = bfs_sweep();",
  	"#else",
  	"	if (bfs_free_slot)	/* local */",
  	"	{	t = bfs_free_slot;",
  	"		bfs_free_slot = bfs_free_slot->nxt;",
  	"		t->nxt = (BFS_Slot *) 0;",
  	"	} else",
  	"	{	t = (BFS_Slot *) sh_malloc((ulong) sizeof(BFS_Slot));",
  	"	}",
  	"#endif",
  	"	if (t->s_data)",
  	"	{	memset(t->s_data, 0, sizeof(BFS_State));",
  	"	} else",
  	"	{	t->s_data = (BFS_State *) sh_malloc((ulong) sizeof(BFS_State));",
  	"	}",
  	"",
  	"	/* we keep a ptr to the frame of parent states, which is */",
  	"	/* used for reconstructing path and recovering failed rvs etc */",
  	"	/* we should not overwrite the data at this address with a memset */",
  	"",
  	"	if (f)",
  	"	{	t->s_data->t_info = f;",
  	"	} else",
  	"	{	t->s_data->t_info = bfs_grab_trail();",
  	"	}",
  	"	return t;",
  	"}",
  	"#else",
  	"BFS_Slot *",
  	"bfs_prep_slot(BFS_Trail *f, BFS_Slot *t)",
  	"{",
  	"	if (t->s_data)",
  	"	{	memset(t->s_data, 0, sizeof(BFS_State));",
  	"	} else",
  	"	{	t->s_data = (BFS_State *) sh_malloc((ulong) sizeof(BFS_State));",
  	"	}",
  	"	if (f)",
  	"	{	t->s_data->t_info = f;",
  	"	} else",
  	"	{	t->s_data->t_info = bfs_grab_trail();",
  	"	}",
  	"	return t;",
  	"}",
  	"#endif",
  	"",
  	"SV_Hold *",
  	"bfs_new_sv(int n)",
  	"{	SV_Hold *h;",
  	"",
  	"	if (bfs_svfree[n])",
  	"	{	h = bfs_svfree[n];",
  	"		bfs_svfree[n] = h->nxt;",
  	"		h->nxt = (SV_Hold *) 0;",
  	"	} else",
  	"	{	h = (SV_Hold *) sh_malloc((ulong) sizeof(SV_Hold));",
  	"#if 0",
  	"		h->sz = n;",
  	"#endif",
  	"		h->sv = (State *) sh_malloc((ulong)(sizeof(State) - VECTORSZ + n));",
  	"	}",
  	"	memcpy((char *)h->sv, (char *)&now, n);",
  	"	return h;",
  	"}",
  	"#if NRUNS>0",
  	"static EV_Hold *kept[VECTORSZ];	/* local */",
  	"",
  	"static void",
  	"bfs_keep(EV_Hold *v)",
  	"{	EV_Hold *h;",
  	"",
  	"	for (h = kept[v->sz]; h; h = h->nxt) /* check local list */",
  	"	{	if (v->nrpr == h->nrpr",
  	"		&&  v->nrqs == h->nrqs",
  	"#if !defined(NOCOMP) && !defined(HC)",
  	"		&&  (v->sv == h->sv || memcmp((char *) v->sv, (char *) h->sv, v->sz) == 0)",
  	"#endif",
  	"#ifdef TRIX",
  	"		)",
  	"#else",
  	"	#if NRUNS>0",
  	"		#if VECTORSZ>32000",
  	"		&&  (memcmp((char *) v->po, (char *) h->po, v->nrpr * sizeof(int)) == 0)",
  	"		&&  (memcmp((char *) v->qo, (char *) h->qo, v->nrqs * sizeof(int)) == 0)",
  	"		#else",
  	"		&&  (memcmp((char *) v->po, (char *) h->po, v->nrpr * sizeof(short)) == 0)",
  	"		&&  (memcmp((char *) v->qo, (char *) h->qo, v->nrqs * sizeof(short)) == 0)",
  	"		#endif",
  	"		&&  (memcmp((char *) v->ps, (char *) h->ps, v->nrpr * sizeof(uchar)) == 0)",
  	"		&&  (memcmp((char *) v->qs, (char *) h->qs, v->nrqs * sizeof(uchar)) == 0))",
  	"	#else",
  	"		)",
  	"	#endif",
  	"#endif",
  	"		{	break;",
  	"	}	}",
  	"",
  	"	if (!h)	/* we don't have one like it yet */",
  	"	{	v->nxt = kept[v->sz];	/* keep the original owner field */",
  	"		kept[v->sz] = v;",
  	"		/* all ptrs inside are to shared memory, but nxt is local */",
  	"	}",
  	"}",
  	"",
  	"EV_Hold *",
  	"bfs_new_sv_mask(int n)",
  	"{	EV_Hold *h;",
  	"",
  	"	for (h = kept[n]; h; h = h->nxt)",
  	"	{	if ((now._nr_pr == h->nrpr)",
  	"		&&  (now._nr_qs == h->nrqs)",
  	"#if !defined(NOCOMP) && !defined(HC) && NRUNS>0",
  	"		&& ((char *) Mask == h->sv || (memcmp((char *) Mask, h->sv, n) == 0))",
  	"#endif",
  	"#ifdef TRIX",
  	"		)",
  	"#else",
  	"	#if NRUNS>0",
  	"		#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))",
  	"	#else",
  	"		)",
  	"	#endif",
  	"#endif",
  	"		{	break;",
  	"	}	}",
  	"",
  	"	if (!h)",
  	"	{	/* once created, the contents are never modified */",
  	"		h = (EV_Hold *) sh_malloc((ulong)sizeof(EV_Hold));",
  	"		h->owner = who_am_i;",
  	"		h->sz = n;",
  	"		h->nrpr = now._nr_pr;",
  	"		h->nrqs = now._nr_qs;",
  	"#if !defined(NOCOMP) && !defined(HC) && NRUNS>0",
  	"		h->sv = (char *) Mask;	/* in shared memory, and never modified */",
  	"#endif",
  	"#if NRUNS>0 && !defined(TRIX)",
  	"		if (now._nr_pr > 0)",
  	"		{	h->ps = (char *) proc_skip;",
  	"			h->po = (char *) proc_offset;",
  	"		}",
  	"		if (now._nr_qs > 0)",
  	"		{	h->qs = (char *) q_skip;",
  	"			h->qo = (char *) q_offset;",
  	"		}",
  	"#endif",
  	"		h->nxt = kept[n];",
  	"		kept[n] = h;",
  	"	}",
  	"	return h;",
  	"}",
  	"#endif", 
  	"BFS_Slot *",
  	"bfs_pack_state(Trail *f, BFS_Trail *g, int search_depth, BFS_Slot *t)",
  	"{",
  	"#ifdef BFS_CHECK",
  	"	assert(t->s_data != NULL);",
  	"	assert(t->s_data->t_info != NULL);",
  	"	assert(f || g);",
  	"#endif",
  	"	if (!g)",
  	"	{	t->s_data->t_info->ostate = f->ostate;",
  	"		t->s_data->t_info->st   = f->st;",
  	"		t->s_data->t_info->o_tt = search_depth;",
  	"		t->s_data->t_info->pr   = f->pr;",
  	"		t->s_data->t_info->tau  = f->tau;",
  	"		t->s_data->t_info->o_pm = f->o_pm;",
  	"		if (f->o_t)",
  	"		{	t->s_data->t_info->t_id = f->o_t->t_id;",
  	"		} else",
  	"		{	t->s_data->t_info->t_id = -1;",
  	"			t->s_data->t_info->ostate = NULL;",
  	"		}",
  	"	} /* else t->s_data->t_info == g */",
  	"#if SYNC",
  	"	t->s_data->boq = boq;",
  	"#endif",
  	"#ifdef VERBOSE",
  	"	{	static ulong u_cnt;",
  	"		t->s_data->nr = u_cnt++;",
  	"	}",
  	"#endif",
  	"#ifdef TRIX",
  	"	sv_populate(); /* make sure now is up to date */",
  	"#endif",
  	"#ifndef BFS_DISK",
  	"	{ 	SV_Hold *x = bfs_new_sv(vsize);",
  	"		t->s_data->osv = x->sv;",
  	"		x->sv = (State *) 0;",
  	"		x->nxt = bfs_free_hold;",
  	"		bfs_free_hold = x;",
  	"	}",
  	"#endif",
  	"#if NRUNS>0",
  	"	t->s_data->omask = bfs_new_sv_mask(vsize);",
  	"#endif",
  	"",
  	"#if defined(Q_PROVISO) && !defined(BITSTATE) && !defined(NOREDUCE)",
  	"	t->s_data->lstate = Lstate;	/* Lstate is set in o_store or h_store */",
  	"#endif",
  	"#ifdef BFS_FIFO",
  	"	t->type = STATE;",
  	"#endif",
  	"	return t;",
  	"}",
  	"",
  	"void",
  	"bfs_store_state(Trail *t, short oboq)",
  	"{",
  	"#ifdef TRIX",
  	"	sv_populate();",
  	"#endif",
  	"#if defined(VERI) && defined(Q_PROVISO) && !defined(BITSTATE) && defined(FULLSTACK)",
  	"	if (!(t->tau&4)",	
  	"	&&    t->ostate)",	
  	"	{	t->tau |= ((BFS_Trail *) t->ostate)->tau&64;",
  	"	}	/* lift 64 across claim moves */",
  	"#endif",	
  	"",
  	"#ifdef BFS_SEP_HASH",
  	"	#if SYNC",
  	"	if (boq == -1 && oboq != -1)	/* post-rv */",
  	"	{	BFS_Trail *x =  (BFS_Trail *) trpt->ostate; /* pre-rv state */",
  	"	 	if (x)",
  	"		{	x->o_pm |= 4;	/* rv complete */",
  	"	}	}",
  	"	#endif",
  	"	d_sfh((uchar *)&now, (int) vsize); /* sep-hash -- sets K1 -- overkill */",
  	"	bfs_keep_state = K1%%Cores + 1;",
  	"	bfs_push_state(t, NULL, trpt->o_tt+1);	/* bfs_store_state - sep_hash */",
  	"	bfs_keep_state = 0;",
  	"#else",
  	"	#ifdef VERI",
  #if 0
  		in VERI mode store the state when
  		(!t->ostate || (t->tau&4)) in initial state and after each program move
  
  		i.e., dont store when !(!t->ostate || (t->tau&4)) = (t->ostate && !(t->tau&4))
  		the *first* time that the tau flag is not set:
  		possibly after a series of claim moves in an atomic sequence
  #endif
  	"		if (!(t->tau&4) && t->ostate && (((BFS_Trail *)t->ostate)->tau&4))",
  	"		{	/* do not store intermediate state */",
  	"		#if defined(VERBOSE) && defined(L_BOUND)",
  	"			bfs_printf(\"Un-Stored state bnd %%d -- sds %%p\\n\",",
  	"				now._l_bnd, now._l_sds);",
  	"		#endif",
  	"			bfs_push_state(t, NULL, trpt->o_tt+1);	/* claim move */",
  	"		} else",
  	"	#endif",
  	"		if (!bfs_do_store((char *)&now, vsize))	/* includes bfs_visited */",
  	"		{	nstates++;			/* local count */",
  	"			trpt->tau |= 64;		/* bfs: succ outside stack */",
  	"	#if SYNC",
  	"			if (boq == -1 && oboq != -1)	/* post-rv */",
  	"			{	BFS_Trail *x = ",
  	"			  	(BFS_Trail *) trpt->ostate; /* pre-rv state */",
  	"			  	if (x)",
  	"				{	x->o_pm |= 4;	/* rv complete */",
  	"			}	}",
  	"	#endif",
  	"			bfs_push_state(t, NULL, trpt->o_tt+1);	/* successor */",
  	"		} else",
  	"		{	truncs++;",
  	"	#ifdef BFS_CHECK",
  	"			bfs_printf(\"seen before\\n\");",
  	"	#endif",
  	"	#if defined(Q_PROVISO) && !defined(BITSTATE) && defined(FULLSTACK)",
  	"		#ifdef USE_TDH",
  	"			if (Lstate)",	
  	"			{	trpt->tau |= 64;",
  	"			}",
  	"		#else",
  	"			if (Lstate && Lstate->tagged)	/* bfs_store_state */",
  	"			{	trpt->tau |= 64;",
  	"			}",
  	"		#endif",
  	"	#endif",
  	"		}",
  	"#endif",
  	"}",
  	"",
  	"/*** support routines ***/",
  	"",
  	"void",
  	"bfs_clear_locks(void)",
  	"{	int i;",
  	"",
  	"	/* clear any locks held by this process only */",
  	"	if (shared_memory)",
  	"	for (i = 0; i < BFS_MAXLOCKS; i++)",
  	"	{	if (shared_memory->sh_owner[i] == who_am_i + 1)",
  	"		{	shared_memory->sh_locks[i] = 0;",
  	"#ifdef BFS_CHECK",
  	"			shared_memory->in_count[i] = 0;",
  	"#endif",
  	"			shared_memory->sh_owner[i] = 0;",
  	"	}	}",
  	"}",
  	"",
  	"void",
  	"e_critical(int which)",
  	"{	int w;",
  	"#ifdef BFS_CHECK",
  	"	assert(which >= 0 && which < BFS_MAXLOCKS);",
  	"#endif",
  	"	if (shared_memory == NULL) return;",
  	"	while (tas(&(shared_memory->sh_locks[which])) != 0)",
  	"	{	w = shared_memory->sh_owner[which]; /* sh_locks[which] could be 0 by now */",
  	"		assert(w >= 0 && w <= BFS_MAXPROCS);",
  	"		if (w > 0 && shared_memory->bfs_flag[w-1] == 2)",
  	"		{	/* multiple processes can get here; only one should do this: */",
  	"			if (tas(&(shared_memory->bfs_data[w - 1].override)) == 0)",
  	"			{	fprintf(stderr, \"cpu%%02d: override lock %%d - held by %%d\\n\",",
  	"				who_am_i, which, shared_memory->sh_owner[which]);",
  	"#ifdef BFS_CHECK",
  	"				shared_memory->in_count[which] = 0;",
  	"#endif",
  	"				shared_memory->sh_locks[which] = 0;",
  	"				shared_memory->sh_owner[which] = 0;",
  	"		}	}",
  	"		shared_memory->wait_count[which]++; /* not atomic of course */",
  	"	}",
  	"#ifdef BFS_CHECK",
  	"	if (shared_memory->in_count[which] != 0)",
  	"	{	fprintf(stderr, \"cpu%%02d: cannot happen lock %%d count %%d\\n\", who_am_i,",
  	"			which, shared_memory->in_count[which]);",
  	"	}",
  	"	shared_memory->in_count[which]++;",
  	"#endif",
  	"	shared_memory->sh_owner[which] = who_am_i+1;",
  	"}",
  	"",
  	"void",
  	"x_critical(int which)",
  	"{",
  	"	if (shared_memory == NULL) return;",
  	"#ifdef BFS_CHECK",
  	"	assert(shared_memory->in_count[which] == 1);",
  	"	shared_memory->in_count[which] = 0;",
  	"#endif",
  	"	shared_memory->sh_locks[which] = 0;",
  	"	shared_memory->sh_owner[which] = 0;",
  	"}",
  	"",
  	"void",
  	"bfs_printf(const char *fmt, ...)",
  	"{	va_list args;",
  	"",
  	"	e_critical(BFS_PRINT);",
  	"#ifdef BFS_CHECK",
  	"	if (1) { int i=who_am_i; while (i-- > 0) printf(\"  \"); }",
  	"#endif",
  	"	printf(\"cpu%%02d: \", who_am_i);",
  	"	va_start(args, fmt);",
  	"	vprintf(fmt, args);",
  	"	va_end(args);",
  	"	fflush(stdout);",
  	"	x_critical(BFS_PRINT);",
  	"}",
  	"",
  	"int",
  	"bfs_all_idle(void)",
  	"{	int i;",
  	"",
  	"	if (shared_memory)",
  	"	for (i = 0; i < Cores; i++)",
  	"	{	if (shared_memory->bfs_flag[i] == 0",
  	"		&&  shared_memory->bfs_idle[i] == 0)",
  	"		{	return 0;",
  	"	}	}",
  	"	return 1;",
  	"}",
  	"",
  	"#ifdef BFS_FIFO",
  	"int",
  	"bfs_idle_and_empty(void)",
  	"{	int p;	/* read-only */",
  	"	for (p = 0; p < Cores; p++)",
  	"	{	if (shared_memory->bfs_flag[p] == 0",
  	"		&&  shared_memory->bfs_idle[p] == 0)",
  	"		{	return 0;",
  	"	}	}",
  	"	for (p = 0; p < Cores; p++)",
  	"	{	if (bfs_empty(p) < Cores)",
  	"		{	return 0;",
  	"	}	}",
  	"	return 1;",
  	"}",
  	"#endif",
  	"",
  	"void",
  	"bfs_set_toggle(void)	/* executed by root */",
  	"{	int i;",
  	"",
  	"	if (shared_memory)",
  	"	for (i = 0; i < Cores; i++)",
  	"	{	shared_memory->bfs_idle[i] = 0;",
  	"	}",
  	"}",
  	"",
  	"int",
  	"bfs_all_running(void)	/* crash detection */",
  	"{	int i;",
  	"	for (i = 0; i < Cores; i++)",
  	"	{	if (!shared_memory || shared_memory->bfs_flag[i] > 1)",
  	"		{	return 0;",
  	"	}	}",
  	"	return 1;",
  	"}",
  	"",
  	"void",
  	"bfs_mark_done(int code)",
  	"{",
  	"	if (shared_memory)",
  	"	{	shared_memory->bfs_flag[who_am_i] = (int) code;",
  	"		shared_memory->quit = 1;",
  	"	}",
  	"}",
  	"",
  	"static uchar *",
  	"bfs_offset(int c)",
  	"{	int   p, N;",
  	"#ifdef COLLAPSE",
  	"	uchar *q = (uchar *) ncomps; /* it is the first object allocated */",
  	"	q += (256+2) * sizeof(ulong); /* preserve contents of ncomps */",
  	"#else",
  	"	uchar *q = (uchar *) &(shared_memory->allocator);",
  	"#endif",
  	"	/* _NP_+1 proctypes, reachability info:",
  	"	 * reached[x : 0 .. _NP_+1][ 0 .. NrStates[x] ]",
  	"	 */",
  	"	for (p = N = 0; p <= _NP_; p++)",
  	"	{	N += NrStates[p];	/* sum for all proctypes */",
  	"	}",
  	"",
  	"	/* space needed per proctype: N bytes */",
  	"	/* rounded up to a multiple of the word size */",
  	"	if ((N%%sizeof(void *)) != 0)	/* aligned */",
  	"	{	N += sizeof(void *) - (N%%sizeof(void *));",
  	"	}",
  	"",
  	"	q += ((c - 1) * (_NP_ + 1) * N);",
  	"	return q;",
  	"}",
  	"",
  	"static void",
  	"bfs_putreached(void)",
  	"{	uchar *q;",
  	"	int p;",
  	"",
  	"	assert(who_am_i > 0);",
  	"",
  	"	q = bfs_offset(who_am_i);",
  	"	for (p = 0; p <= _NP_; p++)",
  	"	{	memcpy((void *) q, (const void *) reached[p], (size_t) NrStates[p]);",
  	"		q += NrStates[p];",
  	"	}",
  	"}",
  	"",
  	"static void",
  	"bfs_getreached(int c)",
  	"{	uchar *q;",
  	"	int p, i;",
  	"",
  	"	assert(who_am_i == 0 && c >= 1 && c < Cores);",
  	"",
  	"	q = (uchar *) bfs_offset(c);",
  	"	for (p = 0; p <= _NP_; p++)",
  	"	for (i = 0; i < NrStates[p]; i++)",
  	"	{	reached[p][i] += *q++; /* update local copy */",
  	"	}",
  	"}",
  	"",
  	"void",
  	"bfs_update(void)",
  	"{	int i;",
  	"	volatile BFS_data *s;",
  	"",
  	"	if (!shared_memory) return;",
  	"",
  	"	s = &shared_memory->bfs_data[who_am_i];",
  	"	if (who_am_i == 0)",
  	"	{	shared_memory->bfs_flag[who_am_i] = 3; /* or else others dont stop */",
  	"		bfs_gcount = 0;",
  	"		for (i = 1; i < Cores; i++) /* start at 1 not 0 */",
  	"		{	while (shared_memory->bfs_flag[i] == 0)",
  	"			{	sleep(1);",
  	"				if (bfs_gcount++ > WAIT_MAX)	/* excessively long wait */",
  	"				{	printf(\"cpu00: give up waiting for cpu%%2d (%%d cores)\\n\", i, Cores);",
  	"					bfs_gcount = 0;",
  	"					break;",
  	"			}	}",
  	"			s = &shared_memory->bfs_data[i];",
  	"			mreached     = Max(mreached, s->mreached);",
  	"			hmax = vsize = Max(vsize,    s->vsize);",
  	"			errors   += s->errors;",
  	"			memcnt   += s->memcnt;",
  	"			nstates  += s->nstates;",
  	"			nlinks   += s->nlinks;",
  	"			truncs   += s->truncs;",
  	"			bfs_left += s->memory_left;",
  	"			bfs_punt += s->punted;",
  	"			bfs_getreached(i);",
  	"		}",
  	"	} else",
  	"	{	s->mreached = (ulong) mreached;",
  	"		s->vsize    = (ulong) vsize;",
  	"		s->errors   = (int) errors;",
  	"		s->memcnt   = (double) memcnt;",
  	"		s->nstates  = (double) nstates;",
  	"		s->nlinks   = (double) nlinks;",
  	"		s->truncs   = (double) truncs;",
  	"		s->memory_left = (ulong) bfs_left;",
  	"		s->punted      = (ulong) bfs_punt;",
  	"		bfs_putreached();",
  	"	}",
  	"}",
  	"",
  	"volatile uchar *",
  	"sh_pre_malloc(ulong n)	/* used before the local heaps are populated */",
  	"{	volatile uchar *ptr = NULL;",
  	"",
  	"	assert(!bfs_runs);",
  	"	if ((n%%sizeof(void *)) != 0)",
  	"	{	n += sizeof(void *) - (n%%sizeof(void *));",
  	"		assert((n%%sizeof(void *)) == 0);",
  	"	}",
  	"",
  	"	e_critical(BFS_MEM);	/* needed? */",
  	"		if (shared_memory->mem_left < n + 7)", 
  	"		{	x_critical(BFS_MEM);",
  	"			bfs_printf(\"want %%lu, have %%lu\\n\",",
  	"				n, shared_memory->mem_left);",
  	"			bfs_shutdown(\"out of shared memory\");",
  	"			assert(0); /* should be unreachable */",
  	"		}",
  	"		ptr = shared_memory->allocator;",
  	"#if WS>4", 
  	"		{	int b = (int) ((uint64_t) ptr)&7;",
  	"			if (b != 0)",
  	"			{	ptr += (8-b);",
  	"				shared_memory->allocator = ptr;",
  	"		}	}",
  	"#endif",
  	"		shared_memory->allocator += n;",
  	"		shared_memory->mem_left -= n;",
  	"	x_critical(BFS_MEM);",
  	"",
  	"	bfs_pre_allocated += n;",
  	"",
  	"	return ptr;",
  	"}",
  	"",
  	"volatile uchar *",
  	"sh_malloc(ulong n)",
  	"{	volatile uchar *ptr = NULL;",
  	"#ifdef BFS_CHECK",
  	"	assert(bfs_runs);",
  	"#endif",
  	"	if ((n%%sizeof(void *)) != 0)",
  	"	{	n += sizeof(void *) - (n%%sizeof(void *));",
  	"#ifdef BFS_CHECK",
  	"		assert((n%%sizeof(void *)) == 0);",
  	"#endif",
  	"	}",
  	"",
  	"	/* local heap -- no locks needed */",
  	"	if (bfs_left < n)",
  	"	{	e_critical(BFS_MEM);",
  	"		if (shared_memory->mem_left >= n)",
  	"		{	ptr = (uchar *) shared_memory->allocator;",
  	"			shared_memory->allocator += n;",
  	"			shared_memory->mem_left  -= n;",
  	"			x_critical(BFS_MEM);",
  	"			return ptr;",
  	"		}",
  	"		x_critical(BFS_MEM);",
  	"#ifdef BFS_LOGMEM",
  	"		int i;",
  	"		e_critical(BFS_MEM);",
  	"		for (i = 0; i < 1024; i++)",
  	"		{	if (shared_memory->logmem[i] > 0)",
  	"			{	bfs_printf(\"\tlog[%%d]\t%%d\\n\", i, shared_memory->logmem[i]);",
  	"		}	}",
  	"		x_critical(BFS_MEM);",
  	"#endif",
  	"		bfs_shutdown(\"out of shared memory\"); /* no return */",
  	"	}",
  	"#ifdef BFS_LOGMEM",
  	"	e_critical(BFS_MEM);",
  	"	if (n < 1023)",
  	"	{	shared_memory->logmem[n]++;",
  	"	} else",
  	"	{	shared_memory->logmem[1023]++;",
  	"	}",
  	"	x_critical(BFS_MEM);",
  	"#endif",
  	"	ptr = (uchar *) bfs_heap;",
  	"	bfs_heap += n;",
  	"	bfs_left -= n;",
  	"",
  	"	if (0) printf(\"sh_malloc %%ld\\n\", n);",
  	"	return ptr;",
  	"}",
  	"",
  	"volatile uchar *",
  	"bfs_get_shared_mem(key_t key, size_t n)",
  	"{	char *rval;",
  	"",
  	"	assert(who_am_i == 0);",
  	"",
  	"	shared_mem_id = shmget(key, n, 0600 | IPC_CREAT | IPC_EXCL);	/* create */",
  	"	if (shared_mem_id == -1)",
  	"	{	fprintf(stderr, \"cpu%%02d: tried to get %%d MB of shared memory\\n\",",
  	"			who_am_i, (int) n/(1024*1024));",
  	"		perror(\"shmget\");",
  	"		exit(1);",
  	"	}",
  	"	if ((rval = (char *) shmat(shared_mem_id, (void *) 0, 0)) == (char *) -1) /* attach */",
  	"	{	perror(\"shmat\");",
  	"		exit(1);",
  	"	}",
  	"	return (uchar *) rval;",
  	"}",
  	"",
  	"void",
  	"bfs_drop_shared_memory(void)",
  	"{",
  	"	if (who_am_i == 0)",
  	"	{	printf(\"pan: releasing shared memory...\");",
  	"		fflush(stdout);",
  	"	}",
  	"	if (shared_memory)",
  	"	{	shmdt(shared_memory);					/* detach */",
  	"		if (who_am_i == 0)",
  	"		{	shmctl(shared_mem_id, IPC_RMID, (void *) 0);	/* remove */",
  	"	}	}",
  	"	if (who_am_i == 0)",
  	"	{	printf(\"done\\n\");",
  	"		fflush(stdout);",
  	"	}",
  	"}",
  	"",
  	"size_t",
  	"bfs_find_largest(key_t key)",
  	"{	size_t n;",
  	"	const size_t delta = 32*1024*1024;",
  	"	int temp_id = -1;",
  	"	int atleastonce = 0;",
  	"",
  	"	for (n = delta; ; n += delta)",
  	"	{	if (WS <= 4 && n >= 1024*1024*1024)", 
  	"		{	n = 1024*1024*1024;",
  	"			break;",
  	"		}",
  	"#ifdef MEMLIM",
  	"		if ((double) n > memlim)",
  	"		{	n = (size_t) memlim;",
  	"			break;",
  	"		}",
  	"#endif",
  	"		temp_id = shmget(key, n, 0600);		/* check for stale copy */",
  	"		if (temp_id != -1)",
  	"		{	if (shmctl(temp_id, IPC_RMID, ((void *) 0)) < 0) /* remove */",
  	"			{	perror(\"remove_segment_fails 2\");",
  	"				exit(1);",
  	"		}	}",
  	"",
  	"		temp_id = shmget(key, n, 0600 | IPC_CREAT | IPC_EXCL);	/* create new */",
  	"		if (temp_id == -1)",
  	"		{	n -= delta;",
  	"			break;",
  	"		} else",
  	"		{	atleastonce++;",
  	"			if (shmctl(temp_id, IPC_RMID, ((void *) 0)) < 0)",
  	"			{	perror(\"remove_segment_fails 0\");",
  	"				exit(1);",
  	"	}	}	}",
  	"",
  	"	if (!atleastonce)",
  	"	{	printf(\"cpu%%02d: no shared memory n=%%d\\n\", who_am_i, (int) n);",
  	"		exit(1);",
  	"	}",
  	"",
  	"	printf(\"cpu%%02d: largest shared memory segment: %%lu MB\\n\",",
  	"		who_am_i, (ulong) n/(1024*1024));",
  	"#if 0",
  	"	#ifdef BFS_SEP_HASH",
  	"	n /= 2;	/* not n /= Cores because the queues take most memory */",
  	"	printf(\"cpu%%02d: using %%lu MB\\n\", who_am_i, (ulong) n/(1024*1024));",
  	"	#endif",
  	"#endif",
  	"	fflush(stdout);",
  	"",
  	"	if ((n/(1024*1024)) == 32)",
  	"	{ if (sizeof(void *) == 4) 	/* a 32 bit machine */",
  	"	  { fprintf(stderr, \"\\t32MB is the default; increase it to 1 GB with:\\n\");",
  	"	    fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmmax=%%d\\n\", (1<<30));",
  	"	    fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmall=%%d\\n\", (1<<30)/8192);",
  	"	  } else if (sizeof(void *) == 8)	/* a 64 bit machine */",
  	"	  { fprintf(stderr, \"\\t32MB is the default; increase it to 30 GB with:\\n\");",
  	"	    fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmmax=32212254720\\n\");",
  	"	    fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmall=7864320\\n\");",
  	"	    fprintf(stderr, \"\\tor for 60 GB:\\n\");",
  	"	    fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmmax=60000000000\\n\");",
  	"	    fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmall=30000000\\n\");",
  	"	  } else",
  	"	  { fprintf(stderr, \"\\tweird wordsize %%d\\n\", (int) sizeof(void *));",
  	"	} }",
  	"",
  	"	return n;",
  	"}",
  	"#ifdef BFS_DISK",
  	"void",
  	"bfs_disk_start(void)",	
  	"{	int unused = system(\"rm -fr .spin\");",
  	"	if (mkdir(\".spin\", 0777) != 0)",
  	"	{	perror(\"mkdir\");",
  	"		Uerror(\"aborting\");",
  	"	}",
  	"}",
  	"void",
  	"bfs_disk_stop(void)",	
  	"{",
  	"	if (system(\"rm -fr .spin\") < 0)",
  	"	{	perror(\"rm -fr .spin/\");",
  	"	}",
  	"}",
  	"void",
  	"bfs_disk_inp(void)", 
  	"{	int i; char fnm[16];",
  	"#ifdef VERBOSE",
  	"	bfs_printf(\"inp %%d %%d 0..%%d\\n\", bfs_toggle, who_am_i, Cores);",
  	"#endif",
  	"	for (i = 0; i < Cores; i++)",
  	"	{	sprintf(fnm, \".spin/q%%d_%%d_%%d\", bfs_toggle, who_am_i, i);",
  	"		if ((bfs_inp_fd[i] = open(fnm, 0444)) < 0)",
  	"		{	perror(\"open\");",
  	"			Uerror(fnm);",
  	"	}	}",
  	"}",
  	"void",
  	"bfs_disk_out(void)", 
  	"{	int i; char fnm[16];",
  	"#ifdef VERBOSE",
  	"	bfs_printf(\"out %%d 0..%%d %%d\\n\", 1-bfs_toggle, Cores, who_am_i);",
  	"#endif",
  	"	shared_memory->bfs_out_cnt[who_am_i] = 0;",
  	"	for (i = 0; i < Cores; i++)",
  	"	{	sprintf(fnm, \".spin/q%%d_%%d_%%d\", 1-bfs_toggle, i, who_am_i);",
  	"		if ((bfs_out_fd[i] = creat(fnm, 0666)) < 0)",
  	"		{	perror(\"creat\");",
  	"			Uerror(fnm);",
  	"	}	}",
  	"}",
  	"void",
  	"bfs_disk_iclose(void)",
  	"{	int i;",
  	"#ifdef VERBOSE",
  	"	bfs_printf(\"close_inp\\n\");",
  	"#endif",
  	"	for (i = 0; i < Cores; i++)",
  	"	{	if (close(bfs_inp_fd[i]) < 0)",
  	"		{	perror(\"iclose\");",
  	"	}	}",
  	"}",
  	"void",
  	"bfs_disk_oclose(void)",
  	"{	int i;",
  	"#ifdef VERBOSE",
  	"	bfs_printf(\"close_out\\n\");",
  	"#endif",
  	"	for (i = 0; i < Cores; i++)",
  	"	{	if (fsync(bfs_out_fd[i]) < 0)",
  	"		{	perror(\"fsync\");",
  	"		}",
  	"		if (close(bfs_out_fd[i]) < 0)",
  	"		{	perror(\"oclose\");",
  	"	}	}",
  	"}",
  	"#endif",
  	"void",
  	"bfs_write_snap(int fd)",
  	"{	if (write(fd, snap, strlen(snap)) != strlen(snap))",
  	"	{       printf(\"pan: error writing %%s\\n\", fnm);",
  	"		bfs_shutdown(\"file system error\");",
  	"	}",
  	"}",
  	"",
  	"void",
  	"bfs_one_step(BFS_Trail *t, int fd)",
  	"{	if (t && t->t_id != (T_ID) -1)",
  	"	{	sprintf(snap, \"%%d:%%d:%%d\\n\",",
  	"			trcnt++, t->pr, t->t_id);",
  	"		bfs_write_snap(fd);",
  	"	}",
  	"}",
  	"",
  	"void",
  	"bfs_putter(BFS_Trail *t, int fd)",
  	"{	if (t && t != (BFS_Trail *) t->ostate)",
  	"		bfs_putter((BFS_Trail *) t->ostate, fd);",
  	"#ifdef L_BOUND",
  	"	if (depthfound == trcnt)",
  	"	{	strcpy(snap, \"-1:-1:-1\\n\");",
  	"		bfs_write_snap(fd);",
  	"		depthfound = -1;",
  	"	}",
  	"#endif",
  	"	bfs_one_step(t, fd);",
  	"}",
  	"",
  	"void",
  	"bfs_nuerror(char *str)",
  	"{	int fd = make_trail();",
  	"",
  	"	if (fd < 0) return;",
  	"#ifdef VERI",
  	"	sprintf(snap, \"-2:%%d:-2\\n\", (uchar) ((P0 *)pptr(0))->_t);",
  	"	bfs_write_snap(fd);",
  	"#endif",
  	"#ifdef MERGED",
  	"	sprintf(snap, \"-4:-4:-4\\n\");",
  	"	bfs_write_snap(fd);",
  	"#endif",
  	"	trcnt = 1;",
  	"	if (strstr(str, \"invalid\"))",
  	"	{	bfs_putter((BFS_Trail *) trpt->ostate, fd);",
  	"	} else",
  	"	{	BFS_Trail x;",
  	"		memset((char *) &x, 0, sizeof(BFS_Trail));",
  	"		x.pr = trpt->pr;",
  	"		x.t_id = (trpt->o_t)?trpt->o_t->t_id:0;",
  	"		x.ostate = trpt->ostate;",
  	"		bfs_putter(&x, fd);",
  	"	}",
  	"	close(fd);",
  	"	if (errors >= upto && upto != 0)",
  	"	{	bfs_shutdown(str);",
  	"	}",
  	"}",
  	"",
  	"void",
  	"bfs_uerror(char *str)",
  	"{	static char laststr[256];",
  	"",
  	"	errors++;",
  	"	if (strncmp(str, laststr, 254) != 0)",
  	"	{	bfs_printf(\"pan:%%d: %%s (at depth %%ld)\\n\",",
  	"			errors, str, ((depthfound == -1)?depth:depthfound));",
  	"		strncpy(laststr, str, 254);",
  	"	}",
  	"#ifdef HAS_CODE",
  	"	if (readtrail) { wrap_trail(); return; }",
  	"#endif",
  	"	if (every_error != 0 || errors == upto)",
  	"	{	bfs_nuerror(str);",
  	"	}",
  	"	if (errors >= upto && upto != 0)",
  	"	{	bfs_shutdown(\"bfs_uerror\");",
  	"	}",
  	"	depthfound = -1;",
  	"}\n",
  	"void",
  	"bfs_Uerror(char *str)",
  	"{	/* bfs_uerror(str); */",
  	"	bfs_printf(\"pan:%%d: %%s (at depth %%ld)\\n\", ++errors, str,",
  	"		((depthfound == -1)?depth:depthfound));",
  	"	bfs_shutdown(\"bfs_Uerror\");",
  	"}",
  	0,
  };
  