pangen1.h

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

		"#else",
	"			printf(\"%%3d: proc %%d exec %%d, \", ",
	"				depth, II, t->forw);",
	"			printf(\"%%d to %%d, %%s %%s %%s\", ",
	"				tt, t->st, t->tp,",
	"				(t->atom&2)?\"atomic\":\"\",",
	"				(boq != -1)?\"rendez-vous\":\"\");",
			"#ifdef HAS_UNLESS",
	"			if (t->e_trans)",
	"				printf(\" (escapes to state %%d)\",",
	"					t->st);",
			"#endif",
	"			printf(\" %%saccepting [tau=%%d]\\n\",",
	"				(trpt->o_pm&2)?\"\":\"non-\", trpt->tau);",
		"#endif",
		"#ifdef RANDOMIZE",
	"			printf(\"	randomizer %%d\\n\", ooi);",
		"#endif",
	"#endif",

	"#ifdef HAS_LAST",
	"#ifdef VERI",
	"			if (II != 0)",
	"#endif",
	"				now._last = II - BASE;",
	"#endif",
	"#ifdef HAS_UNLESS",
	"			trpt->e_state = t->e_trans;",
	"#endif",

	"			depth++; trpt++;",
	"			trpt->pr = (uchar) II;",
	"			trpt->st = tt;",
	"			trpt->o_pm &= ~(2|4);",
	"			if (t->st > 0)",
	"			{	((P0 *)this)->_p = t->st;",
	"/*	moved down		reached[ot][t->st] = 1; */",
	"			}",
	"#ifndef SAFETY",
	"			if (a_cycles)",
	"			{",
		"#if (ACCEPT_LAB>0 && !defined(NP)) || (PROG_LAB>0 && defined(HAS_NP))",
	"				int ii;",
		"#endif",
		"#define P__Q	((P0 *)pptr(ii))",
		"#if ACCEPT_LAB>0",
			"#ifdef NP",
	"				/* state 1 of np_ claim is accepting */",
	"				if (((P0 *)pptr(0))->_p == 1)",
	"					trpt->o_pm |= 2;",
			"#else",
	"				for (ii = 0; ii < (int) now._nr_pr; ii++)",
	"				{ if (accpstate[P__Q->_t][P__Q->_p])",
	"				  {	trpt->o_pm |= 2;",
	"					break;",
	"			   	} }",
			"#endif",
		"#endif",
		"#if defined(HAS_NP) && PROG_LAB>0",
	"				for (ii = 0; ii < (int) now._nr_pr; ii++)",
	"				{ if (progstate[P__Q->_t][P__Q->_p])",
	"				  {	trpt->o_pm |= 4;",
	"					break;",
	"			   	} }",
		"#endif",
		"#undef P__Q",
	"			}",
	"#endif",
	"			trpt->o_t  =  t; trpt->o_n  = _n;",
	"			trpt->o_ot = ot; trpt->o_tt = tt;",
	"			trpt->o_To = To; trpt->o_m  = _m;",
	"			trpt->tau = 0;",
"#ifdef RANDOMIZE",
	"			trpt->oo_i = ooi;",
"#endif",
	"			if (boq != -1 || (t->atom&2))",
	"			{	trpt->tau |= 8;",
	"#ifdef VERI",
	"				/* atomic sequence in claim */",
	"				if((trpt-1)->tau&4)",
	"					trpt->tau |= 4;",
	"				else",
	"					trpt->tau &= ~4;",
	"			} else",
	"			{	if ((trpt-1)->tau&4)",
	"					trpt->tau &= ~4;",
	"				else",
	"					trpt->tau |= 4;",
	"			}",
	"			/* if claim allowed timeout, so */",
	"			/* does the next program-step: */",
	"			if (((trpt-1)->tau&1) && !(trpt->tau&4))",
	"				trpt->tau |= 1;",
	"#else",
	"			} else",
	"				trpt->tau &= ~8;",
	"#endif",
	"			if (boq == -1 && (t->atom&2))",
	"			{	From = To = II; nlinks++;",
	"			} else",
	"			{	From = now._nr_pr-1; To = BASE;",
	"			}",
	"			goto Down;	/* pseudo-recursion */",
	"Up:",
	"#ifdef CHECK",
	"	printf(\"%%d: Up - %%s\\n\", depth,",
	"		(trpt->tau&4)?\"claim\":\"program\");",
	"#endif",
	"#ifdef MA",
	"	if (depth <= 0) return;",
	"	/* e.g., if first state is old, after a restart */",
	"#endif",

	"#ifdef SC",
	"	if (CNT1 > CNT2",
	"		&& depth < hiwater - (HHH-DDD) + 2)",
	"	{",
	" 		trpt += DDD;",
	"		disk2stack();",
	"		maxdepth -= DDD;",
	"		hiwater -= DDD;",
	"if(verbose)",
	"printf(\"unzap %%d: %%d\\n\", CNT2, hiwater);",
	"	}",
	"#endif",

	"#ifndef NOFAIR",
	"			if (trpt->o_pm&128)	/* fairness alg */",
	"			{	now._cnt[now._a_t&1] = trpt->bup.oval;",
	"				_n = 1; trpt->o_pm &= ~128;",
	"				depth--; trpt--;",
		"#if defined(VERBOSE) || defined(CHECK)",
	"	printf(\"%%3d: reversed fairness default move\\n\", depth);",
		"#endif",
	"				goto Q999;",
	"			}",
	"#endif",

	"#ifdef HAS_LAST",
	"#ifdef VERI",
	"			{ int d; Trail *trl;",
	"			  now._last = 0;",
	"			  for (d = 1; d < depth; d++)",
	"			  {	trl = getframe(depth-d); /* was (trpt-d) */",
	"				if (trl->pr != 0)",
	"				{ now._last = trl->pr - BASE;",
	"				  break;",
	"			} }	}",
	"#else",
	"			now._last = (depth<1)?0:(trpt-1)->pr;",
	"#endif",
	"#endif",
	"#ifdef EVENT_TRACE",
	"			now._event = trpt->o_event;",
	"#endif",
	"#ifndef SAFETY",
	"			if ((now._a_t&1) && depth <= A_depth)",
	"				return;	/* to checkcycles() */",
	"#endif",
	"			t  = trpt->o_t;  _n = trpt->o_n;",
	"			ot = trpt->o_ot; II = trpt->pr;",
	"			tt = trpt->o_tt; this = pptr(II);",
	"			To = trpt->o_To; _m  = trpt->o_m;",
"#ifdef RANDOMIZE",
	"			ooi = trpt->oo_i;",
"#endif",
	"#ifdef INLINE_REV",
	"			_m = do_reverse(t, II, _m);",
	"#else",
	"#include REVERSE_MOVES",
	"R999:			/* jumps here when done */",
	"#endif",

	"#ifdef VERBOSE",
	"			printf(\"%%3d: proc %%d \", depth, II);",
	"			printf(\"reverses %%d, %%d to %%d,\",",
	"				t->forw, tt, t->st);",
	"			printf(\" %%s [abit=%%d,adepth=%%d,\", ",
	"				t->tp, now._a_t, A_depth);",
	"			printf(\"tau=%%d,%%d]\\n\", ",
	"				trpt->tau, (trpt-1)->tau);",
	"#endif",
	"#ifndef NOREDUCE",
	"			/* pass the proviso tags */",
	"			if ((trpt->tau&8)	/* rv or atomic */",
	"			&&  (trpt->tau&16))",
	"				(trpt-1)->tau |= 16;",
	"#ifdef SAFETY",
	"			if ((trpt->tau&8)	/* rv or atomic */",
	"			&&  (trpt->tau&64))",
	"				(trpt-1)->tau |= 64;",
	"#endif",
	"#endif",
	"			depth--; trpt--;",
	"#ifdef NIBIS",
	"			(trans[ot][tt])->om = _m; /* head of list */",
	"#endif",

	"			/* i.e., not set if rv fails */",
	"			if (_m)",
	"			{",
	"#if defined(VERI) && !defined(NP)",
	"				if (II == 0 && verbose && !reached[ot][t->st])",
	"				{",
	"			printf(\"depth %%d: Claim reached state %%d (line %%d)\\n\",",
	"					depth, t->st, src_claim [t->st]);",
	"					fflush(stdout);",
	"				}",
	"#endif",
	"				reached[ot][t->st] = 1;",
	"				reached[ot][tt] = 1;",
	"			}",
	"#ifdef HAS_UNLESS",
	"			else trpt->e_state = 0; /* undo */",
	"#endif",

	"			if (_m>_n||(_n>3&&_m!=0)) _n=_m;",
	"			((P0 *)this)->_p = tt;",
	"		} /* all options */",

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

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

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

	"#ifndef NOFAIR",
	"	/* Fairness: undo Rule 2 */",
	"	if (trpt->o_pm&32)	/* remains if proc blocked */",
	"	{",
		"#ifdef VERI",
	"		if (now._cnt[now._a_t&1] == 1)",	/* NEW: 1 iso 0 */
	"			now._cnt[now._a_t&1] = 2;",	/* NEW: 2 iso 1 */
		"#endif",
	"		now._cnt[now._a_t&1] += 1;",
		"#ifdef VERBOSE",
	"		printf(\"%%3d: proc -- fairness \", depth);",
	"		printf(\"undo Rule 2, cnt=%%d, _a_t=%%d\\n\",",
	"			now._cnt[now._a_t&1], now._a_t);",
		"#endif",
	"		trpt->o_pm &= ~32;",
	"	}",
"#ifndef NP",
	/* 12/97 non-progress cycles cannot be created
	 * by stuttering extension, here or elsewhere
	 */
	"	if (fairness",
	"	&&  _n == 0		/* nobody moved */",
		"#ifdef VERI",
		"	&& !(trpt->tau&4)	/* in program move */",
		"#endif",
	"	&& !(trpt->tau&8)	/* not an atomic one */",
		"#ifdef OTIM",
		"	&& ((trpt->tau&1) || endstate())",
		"#else",
			"#ifdef ETIM",
			"	&&  (trpt->tau&1)	/* already tried timeout */",
			"#endif",
		"#endif",
		"#ifndef NOREDUCE",
		"	/* see below  */",
		"	&& !((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
		"#endif",
	"	&& now._cnt[now._a_t&1] > 0)	/* needed more procs */",
	"	{	depth++; trpt++;",
	"		trpt->o_pm |= 128 | ((trpt-1)->o_pm&(2|4));",
	"		trpt->bup.oval = now._cnt[now._a_t&1];",
	"		now._cnt[now._a_t&1] = 1;",
		"#ifdef VERI",
	"		trpt->tau = 4;",
		"#else",
	"		trpt->tau = 0;",
		"#endif",
	"		From = now._nr_pr-1; To = BASE;",
		"#if defined(VERBOSE) || defined(CHECK)",
	"		printf(\"%%3d: fairness default move \", depth);",
	"		printf(\"(all procs block)\\n\");",
		"#endif",
	"		goto Down;",
	"	}",
"#endif",
	"Q999:	/* returns here with _n>0 when done */;",

	"	if (trpt->o_pm&8)",
	"	{	now._a_t &= ~2;",
	"		now._cnt[now._a_t&1] = 0;",
	"		trpt->o_pm &= ~8;",
		"#ifdef VERBOSE",
	"		printf(\"%%3d: fairness undo Rule 1, _a_t=%%d\\n\",",
	"			depth, now._a_t);",
		"#endif",
	"	}",
	"	if (trpt->o_pm&16)",
	"	{	now._a_t |= 2;",		/* restore a-bit */
	"		now._cnt[now._a_t&1] = 1;",	/* NEW: restore cnt */
	"		trpt->o_pm &= ~16;",
		"#ifdef VERBOSE",
	"		printf(\"%%3d: fairness undo Rule 3, _a_t=%%d\\n\",",
	"			depth, now._a_t);",
		"#endif",
	"	}",
	"#endif",

	"#ifndef NOREDUCE",
"#ifdef SAFETY",
	"	/* preselected move - no successors outside stack */",
	"	if ((trpt->tau&32) && !(trpt->tau&64))",
	"	{	From = now._nr_pr-1; To = BASE;",
		"#ifdef DEBUG",
	"	printf(\"%%3d: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
	"	depth, II+1, _n, trpt->tau);",
		"#endif",
	"		_n = 0; trpt->tau &= ~(16|32|64);",
	"		if (II >= BASE)	/* II already decremented */",
	"			goto Resume;",
	"		else",
	"			goto Again;",
	"	}",
"#else",
	"	/* at least one move that was preselected at this */",
	"	/* level, blocked or truncated at the next level  */",
	"/* implied: #ifdef FULLSTACK */",
	"	if ((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
	"	{",
		"#ifdef DEBUG",
	"	printf(\"%%3d: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
	"	depth, II+1, (int) _n, trpt->tau);",
		"#endif",
	"		if (a_cycles && (trpt->tau&16))",
	"		{	if (!(now._a_t&1))",
	"			{",
		"#ifdef DEBUG",
	"	printf(\"%%3d: setting proviso bit\\n\", depth);",
		"#endif",
	"#ifndef BITSTATE",
		"#ifdef MA",
			"#ifdef VERI",
	"			(trpt-1)->proviso = 1;",
			"#else",
	"			trpt->proviso = 1;",
			"#endif",
		"#else",
			"#ifdef VERI",
	"			if ((trpt-1)->ostate)",
	"			((char *)&((trpt-1)->ostate->state))[0] |= 128;",
			"#else",
	"			((char *)&(trpt->ostate->state))[0] |= 128;",
			"#endif",
		"#endif",
	"#else",
		"#ifdef VERI",
	"			if ((trpt-1)->ostate)",
	"			(trpt-1)->ostate->proviso = 1;",
		"#else",
	"			trpt->ostate->proviso = 1;",
		"#endif",
	"#endif",
	"				From = now._nr_pr-1; To = BASE;",
	"				_n = 0; trpt->tau &= ~(16|32|64);",
	"				goto Again; /* do full search */",
	"			} /* else accept reduction */",
	"		} else",
	"		{	From = now._nr_pr-1; To = BASE;",
	"			_n = 0; trpt->tau &= ~(16|32|64);",
	"			if (II >= BASE)	/* already decremented */",
	"				goto Resume;",
	"			else",
	"				goto Again;",
	"	}	}",
	"/* #endif */",
"#endif",
	"#endif",

	"	if (_n == 0 || ((trpt->tau&4) && (trpt->tau&2)))",
	"	{",
		"#ifdef DEBUG",
	"	printf(\"%%3d: no move [II=%%d, tau=%%d, boq=%%d]\\n\",",
	"		 depth, II, trpt->tau, boq);",
		"#endif",
	"#if SYNC",
	"		/* ok if a rendez-vous fails: */",
	"		if (boq != -1) goto Done;",
	"#endif",
	"		/* ok if no procs or we're at maxdepth */",
	"		if ((now._nr_pr == 0 && (!strict || qs_empty()))",
	"#ifdef OTIM",
	"		||  endstate()",
	"#endif",
	"		||  depth >= maxdepth-1) goto Done;",

	"		if ((trpt->tau&8) && !(trpt->tau&4))",
	"		{	trpt->tau &= ~(1|8);",
	"			/* 1=timeout, 8=atomic */",
	"			From = now._nr_pr-1; To = BASE;",
		"#ifdef DEBUG",
	"		printf(\"%%3d: atomic step proc %%d \", depth, II+1);",
	"		printf(\"unexecutable\\n\");",
		"#endif",
	"#ifdef VERI",
	"			trpt->tau |= 4;	/* switch to claim */",
	"#endif",
	"			goto AllOver;",
	"		}",

	"#ifdef ETIM",
	"		if (!(trpt->tau&1)) /* didn't try timeout yet */",
	"		{",
	"#ifdef VERI",
	"			if (trpt->tau&4)",
	"			{",
		"#ifndef NTIM",
	"				if (trpt->tau&2) /* requested */",
		"#endif",
	"				{	trpt->tau |=  1;",
	"					trpt->tau &= ~2;",
				"#ifdef DEBUG",
	"				printf(\"%%d: timeout\\n\", depth);",
				"#endif",
	"					goto Stutter;",
	"			}	}",
	"			else",
	"			{	/* only claim can enable timeout */",
	"				if ((trpt->tau&8)",
	"				&&  !((trpt-1)->tau&4))",
	"/* blocks inside an atomic */		goto BreakOut;",
				"#ifdef DEBUG",
	"				printf(\"%%d: req timeout\\n\",",
	"					depth);",
				"#endif",
	"				(trpt-1)->tau |= 2; /* request */",
	"				goto Up;",
	"			}",
	"#else",

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

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