pangen1.h

来自「这是一个同样来自贝尔实验室的和UNIX有着渊源的操作系统, 其简洁的设计和实现易」· C头文件 代码 · 共 2,500 行 · 第 1/5 页

	"",
	"	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 + 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 + i) & nmask;",
	"		y = (y + j4) & 7;",
	"		i++;",
	"	}",
		"#ifdef DEBUG",
	"	printf(\"New bitstate\\n\");",
		"#endif",
	"	return 0;",
	"}",
	"#endif",
	"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;",
	"",
	"	if (iterative == 0 && Nr_Trails++ > 0)",
	"		sprintf(fnm, \"%%s%%d.%%s\",",
	"			TrailFile, Nr_Trails-1, tprefix);",
	"	else",
	"		sprintf(fnm, \"%%s.%%s\", TrailFile, tprefix);",
	"",
	"	if ((fd = creat(fnm, (unsigned short) TMODE)) < 0)",
	"	{	if ((q = strchr(TrailFile, \'.\')))",
	"		{	*q = \'\\0\';",		/* strip .pml */
	"			if (iterative == 0 && Nr_Trails-1 > 0)",
	"				sprintf(fnm, \"%%s%%d.%%s\",",
	"					TrailFile, Nr_Trails-1, tprefix);",
	"			else",
	"				sprintf(fnm, \"%%s.%%s\", TrailFile, tprefix);",
	"			*q = \'.\';",
	"			fd = creat(fnm, (unsigned short) TMODE);",
	"	}	}",
	"	if (fd < 0)",
	"	{	printf(\"cannot create %%s\\n\", fnm);",
	"		perror(\"cause\");",
	"	} else",
	"		printf(\"pan: wrote %%s\\n\", fnm);",
	"",
	"	return fd;",
	"}",
	0
};

static char *Code2b[] = {	/* breadth-first search option */
	"#ifdef BFS",
	"#define QPROVISO",
	"#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;",
	"	int *po, *ps;",
	"	int *qo, *qs;",
	"	struct EV_Hold *nxt;",
	"} EV_Hold;",
	"",
	"typedef struct BFS_Trail {",
	"	Trail	*frame;",
	"	SV_Hold *onow;",
	"	EV_Hold *omask;",
	"#ifdef QPROVISO",
	"	struct H_el *lstate;",
	"#endif",
	"	short boq;",
	"	struct BFS_Trail *nxt;",
	"} BFS_Trail;",
	"",
	"BFS_Trail *bfs_trail, *bfs_bot, *bfs_free;",
	"",
	"SV_Hold *svhold, *svfree;",
	"",
	"uchar do_reverse(Trans *, short, uchar);",
	"void snapshot(void);",
	"",
	"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;",
	"		h->sv = (State *) emalloc(sizeof(State) - VECTORSZ + 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)",
	"		&&  (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(int)) == 0)",
	"		&&  (memcmp((char *) proc_skip,   (char *) h->ps, now._nr_pr * sizeof(int)) == 0)",
	"		&&  (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(int)) == 0)",
	"		&&  (memcmp((char *) q_skip,   (char *) h->qs, now._nr_qs * sizeof(int)) == 0))",
	"			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);",
	"",
	"		if (now._nr_pr > 0)",
	"		{	h->po = (int *) emalloc(now._nr_pr * sizeof(int));",
	"			h->ps = (int *) emalloc(now._nr_pr * sizeof(int));",
	"			memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(int));",
	"			memcpy((char *) h->ps, (char *) proc_skip,   now._nr_pr * sizeof(int));",
	"		}",
	"		if (now._nr_qs > 0)",
	"		{	h->qo = (int *) emalloc(now._nr_qs * sizeof(int));",
	"			h->qs = (int *) emalloc(now._nr_qs * sizeof(int));",
	"			memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(int));",
	"			memcpy((char *) h->qs, (char *) q_skip,   now._nr_qs * sizeof(int));",
	"		}",
	"",
	"		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 */
	"	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;",
	"	t->onow = getsv(vsize);",
	"	memcpy((char *)t->onow->sv, (char *)&now, vsize);",
	"	t->omask = getsv_mask(vsize);",
	"#if defined(FULLSTACK) && defined(QPROVISO)",
	"	t->lstate = Lstate;",
	"#endif",
	"	if (!bfs_bot)",
	"	{	bfs_bot = bfs_trail = t;",
	"	} else",
	"	{	bfs_bot->nxt = t;",
	"		bfs_bot = t;",
	"	}",
	"#ifdef CHECK",
	"	printf(\"PUSH %%u (%%d)\\n\", t->frame, d);",
	"#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(QPROVISO) && !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;",
	"",
	"	memcpy((uchar *) &now, (uchar *) t->onow->sv, vsize);",
	"	memcpy((uchar *) Mask, (uchar *) t->omask->sv, vsize);",

	"	if (now._nr_pr > 0)",
	"	{	memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(int));",
	"		memcpy((char *)proc_skip,   (char *)t->omask->ps, now._nr_pr * sizeof(int));",
	"	}",
	"	if (now._nr_qs > 0)",
	"	{	memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(int));",
	"		memcpy((uchar *)q_skip,   (uchar *)t->omask->qs, now._nr_qs * sizeof(int));",
	"	}",

	"	freesv(t->onow);	/* omask not freed */",
	"#ifdef CHECK",
	"	printf(\"POP %%u (%%d)\\n\", t->frame, t->frame->o_tt);",
	"#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  = (((uchar *)&now)+proc_offset[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",
	"				check_claim(t2->st);",
		"#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)",	/* atomic in claim */
	"			Uerror(\"atomic in claim not supported in BFS mode\");",
	"store_it:",
	"",
	"#endif",	/* VERI */
	"",
	"#ifdef BITSTATE",
	"			if (!bstore((char *)&now, vsize))",
	"#else",
		"#ifdef MA",
	"			if (!gstore((char *)&now, vsize, 0))",
		"#else",
	"			if (!hstore((char *)&now, vsize))",
		"#endif",
	"#endif",
	"			{	nstates++;",
	"#ifndef NOREDUCE",
	"				trpt->tau |= 64;", /* succ definitely outside stack */
	"#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(QPROVISO)",
		"#if !defined(QLIST) && !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 (!memcmp((uchar *)&now, (uchar *)tprov->onow->sv, vsize))",
	"					{	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",
	"}",
	"",
	"void",
	"bfs(void)",
	"{	Trans *t; Trail *ntrpt, *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)",
	"			{	printf(\"Depth= %%7d States= %%7g \", mreached, nstates);",
	"				printf(\"Transitions= %%7g \", nstates+truncs);",
	"#ifdef MA",
	"				printf(\"Nodes= %%7d \", nr_states);",
	"#endif",
	"				printf(\"Memory= %%-6.3f\\n\", memcnt/1000000.);",
	"				fflush(stdout);",
	"		}	}",
	"		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;",
	"		}",

/* PO */
	"#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",