pangen1.h

对软件进行可达性测试的软件

	"	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;",
	"",
	"	memcpy((uchar *) &now, (uchar *) t->onow->sv, vsize);",
	"	memcpy((uchar *) Mask, (uchar *) t->omask->sv, vsize);",

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

	"	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(Q_PROVISO)",
		"#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",
	"}",
	"",
	"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)",
	"			{	printf(\"Depth= %%7d States= %%7g \", mreached, nstates);",
	"				printf(\"Transitions= %%7g \", nstates+truncs);",
	"#ifdef MA",
	"				printf(\"Nodes= %%7d \", nr_states);",
	"#endif",
	"				printf(\"Memory= %%-9.3f\\n\", memcnt/1048576.);",
	"				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",
	"				printf(\"%%3d: proc %%d PreSelected (tau=%%d)\\n\", ",
	"					depth, II, trpt->tau);",
		"#endif",
	"				goto MainLoop;",
	"		}	}",
	"		trpt->tau &= ~32;",	/* not preselected */
	"#endif",
/* PO */
	"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 = (((uchar *)&now)+proc_offset[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(\"%%3d: proc %%d exec %%d, \",",
	"					depth, II, t->forw);",
	"				printf(\"%%d to %%d, %%s %%s %%s\",",
	"					tt, t->st, t->tp,",
	"					(t->atom&2)?\"atomic\":\"\",",
	"					(boq != -1)?\"rendez-vous\":\"\");",
		"#ifdef HAS_UNLESS",
	"				if (t->e_trans)",
	"					printf(\" (escapes to state %%d)\", t->st);",
		"#endif",
	"				printf(\" %%saccepting [tau=%%d]\\n\",",
	"					(trpt->o_pm&2)?\"\":\"non-\", trpt->tau);",
	"#endif",
	"#ifdef HAS_UNLESS",
	"				E_state = t->e_trans;",
		"#if SYNC>0",
	"				if (t->e_trans > 0 && (boq != -1 /* || oboq != -1 */))",
	"				{ fprintf(efd, \"error:\tthe use of 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);	/* in verbose mode only */",
	"				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;",
	"		}	}",
/* PO */
	"#ifndef NOREDUCE",
	"		/* preselected - no succ definitely outside stack */",
	"		if ((trpt->tau&32) && !(trpt->tau&64))",
	"		{	From = now._nr_pr-1; To = BASE;",
	"#ifdef DEBUG",
	"			cpu_printf(\"%%3d: 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(\"%%3d: 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 = (((uchar *)&now)+proc_offset[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(\"%%3d: 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\", VERI);",
	"	write(fd, snap, strlen(snap));",
	"#endif",
	"#ifdef MERGED",
	"	sprintf(snap, \"-4:-4:-4\\n\");",
	"	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\",",