pangen1.h

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

	"int qs_empty(void);",

	"/*",
	" * new_state() is the main DFS search routine in the verifier",
	" * it has a lot of code ifdef-ed together to support",
	" * different search modes, which makes it quite unreadable.",
	" * if you are studying the code, first use the C preprocessor",
	" * to generate a specific version from the pan.c source,",
	" * e.g. by saying:",
	" *	gcc -E -DNOREDUCE -DBITSTATE pan.c > ppan.c",
	" * and then study the resulting file, rather than this one",
	" */",
	"#if !defined(BFS) && (!defined(BITSTATE) || !defined(MA))",
	"void",
	"new_state(void)",
	"{	Trans *t;",
	"	uchar _n, _m, ot;",
	"#ifdef RANDOMIZE",
	"	short ooi, eoi;",
	"#endif",
	"#ifdef M_LOSS",
	"	uchar delta_m = 0;",
	"#endif",
	"	short II, JJ = 0, kk;",
	"	int tt;",
	"	short From = now._nr_pr-1, To = BASE;",
	"Down:",
	"#ifdef CHECK",
	"	printf(\"%%d: Down - %%s\",",
	"		depth, (trpt->tau&4)?\"claim\":\"program\");",
	"	printf(\" %%saccepting [pids %%d-%%d]\\n\",",
	"		(trpt->o_pm&2)?\"\":\"non-\", From, To);",
	"#endif",

	"#ifdef SC",
	"	if (depth > hiwater)",
	"	{	stack2disk();",
	"		maxdepth += DDD;",
	"		hiwater += DDD;",
	"		trpt -= DDD;",
	"		if(verbose)",
	"		printf(\"zap %%d: %%d (maxdepth now %%d)\\n\",",
	"			CNT1, hiwater, maxdepth);",
	"	}",
	"#endif",

	"	trpt->tau &= ~(16|32|64); /* make sure these are off */",
	"#if defined(FULLSTACK) && defined(MA)",
	"	trpt->proviso = 0;",
	"#endif",
	"	if (depth >= maxdepth)",
	"	{	truncs++;",
	"#if SYNC",
	"		(trpt+1)->o_n = 1; /* not a deadlock */",
	"#endif",
	"		if (!warned)",
	"		{ warned = 1;",
	"		  printf(\"error: max search depth too small\\n\");",
	"		}",
	"		if (bounded) uerror(\"depth limit reached\");",
	"		(trpt-1)->tau |= 16; /* worstcase guess */",
	"		goto Up;",
	"	}",
	"AllOver:",
	"#if defined(FULLSTACK) && !defined(MA)",
	"	trpt->ostate = (struct H_el *) 0;",
	"#endif",
	"#ifdef VERI",
	"	if ((trpt->tau&4) || ((trpt-1)->tau&128))",
	"#endif",
	"	if (boq == -1) {	/* if not mid-rv */",
	"#ifndef SAFETY",
	"		/* this check should now be redundant",
	"		 * because the seed state also appears",
	"		 * on the 1st dfs stack and would be",
	"		 * matched in hstore below",
	"		 */",
	"		if ((now._a_t&1) && depth > A_depth)",
	"		{	if (!memcmp((char *)&A_Root, ",
	"				(char *)&now, vsize))",
	"			{",
	"				depthfound = A_depth;",
		"#ifdef CHECK",
	"			  printf(\"matches seed\\n\");",
		"#endif",
		"#ifdef NP",
	"			  uerror(\"non-progress cycle\");",
		"#else",
	"			  uerror(\"acceptance cycle\");",
		"#endif",
	"			  goto Up;",
	"			}",
		"#ifdef CHECK",
	"			printf(\"not seed\\n\");",
		"#endif",
	"		}",
	"#endif",
	"		if (!(trpt->tau&8)) /* if no atomic move */",
	"		{",
	"#ifdef BITSTATE",
		"#ifdef CNTRSTACK",	/* -> bitstate, reduced, safety */
	"			II = bstore((char *)&now, vsize);",
	"			trpt->j6 = j1; trpt->j7 = j2;",
	"			JJ = LL[j1] && LL[j2];",
		"#else",
			"#ifdef FULLSTACK",
	"			JJ = onstack_now();",		    /* sets j1 */
			"#else",
				"#ifndef NOREDUCE",
	"			JJ = II; /* worstcase guess for p.o. */",
				"#endif",
			"#endif",
	"			II = bstore((char *)&now, vsize);", /* sets j1-j4 */
		"#endif",
	"#else",
		"#ifdef MA",
	"			II = gstore((char *)&now, vsize, 0);",
			"#ifndef FULLSTACK",
	"			JJ = II;",
			"#else",
	"			JJ = (II == 2)?1:0;",
			"#endif",
		"#else",
	"			II = hstore((char *)&now, vsize);",
			"#ifdef FULLSTACK",
	"			JJ = (II == 2)?1:0;",
			"#endif",
		"#endif",
	"#endif",
	"			kk = (II == 1 || II == 2);",

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

	"#ifndef NOREDUCE",
		"#ifndef SAFETY",
	"			if ((II && JJ) || (II == 3))",
	"			{	/* marker for liveness proviso */",
	"				(trpt-1)->tau |= 16;",
	"				truncs2++;",
	"			}",
		"#else",
	"			if (!II || !JJ)",
	"			{	/* successor outside stack */",
	"				(trpt-1)->tau |= 64;",
	"			}",
		"#endif",
	"#endif",
	"			if (II)",
	"			{	truncs++;",
	"				goto Up;",
	"			}",
	"			if (!kk)",
	"			{	nstates++;",
	"				if ((unsigned long) nstates%%1000000 == 0)",
	"					snapshot();",
	"#ifdef SVDUMP",
	"				if (vprefix > 0)",
	"				if (write(svfd, (uchar *) &now, vprefix) != vprefix)",
	"				{	fprintf(efd, \"writing %%s.svd failed\\n\", Source);",
	"					wrapup();",
	"				}",
	"#endif",
	"#if defined(MA) && defined(W_XPT)",
	"				if ((unsigned long) nstates%%W_XPT == 0)",
	"				{	void w_xpoint(void);",
	"					w_xpoint();",
	"				}",
	"#endif",
	"			}",
	"#if defined(FULLSTACK) || defined(CNTRSTACK)",
	"			onstack_put();",
		"#ifdef DEBUG2",
		"#if defined(FULLSTACK) && !defined(MA)",
	"			printf(\"%%d: putting %%u (%%d)\\n\", depth,",
	"				trpt->ostate, ",
	"				(trpt->ostate)?trpt->ostate->tagged:0);",
		"#else",
	"			printf(\"%%d: putting\\n\", depth);",
		"#endif",
		"#endif",
	"#endif",
	"	}	}",


	"	if (depth > mreached)",
	"		mreached = depth;",
	"#ifdef VERI",
	"	if (trpt->tau&4)",
	"#endif",
	"	trpt->tau &= ~(1|2);	/* timeout and -request off */",
	"	_n = 0;",
	"#if SYNC",
	"	(trpt+1)->o_n = 0;",
	"#endif",
	"#ifdef VERI",
	"	if (now._nr_pr == 0)	/* claim terminated */",
	"		uerror(\"end state in claim reached\");",
	"	check_claim(((P0 *)pptr(0))->_p);",
	"Stutter:",
	"	if (trpt->tau&4)	/* must make a claimmove */",
	"	{",

	"#ifndef NOFAIR",
	"		if ((now._a_t&2)	/* A-bit set */",
	"		&&   now._cnt[now._a_t&1] == 1)",
	"		{	now._a_t &= ~2;",
	"			now._cnt[now._a_t&1] = 0;",
	"			trpt->o_pm |= 16;",
		"#ifdef DEBUG",
	"	printf(\"%%3d: fairness Rule 3.: _a_t = %%d\\n\",",
	"		depth, now._a_t);",
		"#endif",
	"		}",
	"#endif",

	"		II = 0;		/* never */",
	"		goto Veri0;",
	"	}",
	"#endif",
	"#ifndef NOREDUCE",
	"	/* Look for a process with only safe transitions */",
	"	/* (special rules apply in the 2nd dfs) */",
"#ifdef SAFETY",
	"	if (boq == -1 && From != To)",
"#else",
	"/* implied: #ifdef FULLSTACK */",
	"	if (boq == -1 && From != To",
	"	&&  (!(now._a_t&1)",
	"	    ||	(a_cycles &&",
	"#ifndef BITSTATE",
		"#ifdef MA",
			"#ifdef VERI",
	"		 !((trpt-1)->proviso))",
			"#else",
	"		!(trpt->proviso))",
			"#endif",
		"#else",
			"#ifdef VERI",
	"		 (trpt-1)->ostate &&",
	"		!(((char *)&((trpt-1)->ostate->state))[0] & 128))",
			"#else",
	"		!(((char *)&(trpt->ostate->state))[0] & 128))",
			"#endif",
		"#endif",
	"#else",
		"#ifdef VERI",
	"		(trpt-1)->ostate &&",
	"		(trpt-1)->ostate->proviso == 0)",
		"#else",
	"		trpt->ostate->proviso == 0)",
		"#endif",
	"#endif",
	"	   ))",
	"/* #endif */",
"#endif",
	"	for (II = From; II >= To; II -= 1)",
	"	{",
	"Resume:	/* pick up here if preselect fails */",
	"		this = pptr(II);",
	"		tt = (int) ((P0 *)this)->_p;",
	"		ot = (uchar) ((P0 *)this)->_t;",
	"		if (trans[ot][tt]->atom & 8)",
	"		{	t = trans[ot][tt];",
	"			if (t->qu[0] != 0)",
	"			{	Ccheck++;",
	"				if (!q_cond(II, t))",
	"					continue;",
	"				Cholds++;",
	"			}",
	"			From = To = II;",
	"#ifdef NIBIS",
	"			t->om = 0;",
	"#endif",
	"			trpt->tau |= 32; /* preselect marker */",
		"#ifdef DEBUG",
		"#ifdef NIBIS",
	"			printf(\"%%3d: proc %%d Pre\", depth, II);",
	"			printf(\"Selected (om=%%d, tau=%%d)\\n\", ",
	"				t->om, trpt->tau);",
		"#else",
	"	printf(\"%%3d: proc %%d PreSelected (tau=%%d)\\n\", ",
	"		depth, II, trpt->tau);",
		"#endif",
		"#endif",
	"			goto Again;",
	"		}",
	"	}",
	"	trpt->tau &= ~32;",
	"#endif",
	"#if !defined(NOREDUCE) || (defined(ETIM) && !defined(VERI))",
	"Again:",
	"#endif",
	"	/* The Main Expansion Loop over Processes */",

	"	trpt->o_pm &= ~(8|16|32|64); /* fairness-marks */",

	"#ifndef NOFAIR",
	"	if (fairness && boq == -1",
		"#ifdef VERI",
	"	&& (!(trpt->tau&4) && !((trpt-1)->tau&128))",
		"#endif",
	"	&& !(trpt->tau&8))",
	"	{	/* A_bit = 1; Cnt = N in acc states with A_bit 0 */",
	"		if (!(now._a_t&2))",	/* A-bit not set */
	"		{",
	"			if (a_cycles && (trpt->o_pm&2))",
	"			{	/* Accepting state */",
	"				now._a_t |= 2;",
	"				now._cnt[now._a_t&1] = now._nr_pr + 1;", /* NEW +1 */
	"				trpt->o_pm |= 8;",
		"#ifdef DEBUG",
	"	printf(\"%%3d: fairness Rule 1: cnt=%%d, _a_t=%%d\\n\",",
	"			depth, now._cnt[now._a_t&1], now._a_t);",
		"#endif",
	"			}",
	"		} else",		/* A-bit set */
	"		{	/* A_bit = 0 when Cnt 0 */",
	"			if (now._cnt[now._a_t&1] == 1)",	/* NEW: 1 iso 0 */
	"			{	now._a_t &= ~2;",		/* reset a-bit */
	"				now._cnt[now._a_t&1] = 0;",	/* NEW: reset cnt */
	"				trpt->o_pm |= 16;",
		"#ifdef DEBUG",
	"	printf(\"%%3d: fairness Rule 3: _a_t = %%d\\n\",",
	"		depth, now._a_t);",
		"#endif",
	"	}	}	}",
	"#endif",

	"	for (II = From; II >= To; II -= 1)",
	"	{",
	"#if SYNC",
	"		/* no rendezvous with same proc */",
	"		if (boq != -1 && trpt->pr == II) continue;",
	"#endif",
	"#ifdef VERI",
	"Veri0:",
	"#endif",
	"		this = pptr(II);",
	"		tt = (int) ((P0 *)this)->_p;",
	"		ot = (uchar) ((P0 *)this)->_t;",

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

	"#ifdef RANDOMIZE",
	"		for (ooi = eoi = 0, t = trans[ot][tt]; t; t = t->nxt, ooi++)",
	"			if (strcmp(t->tp, \"else\") == 0)",
	"				eoi++;",
	"",
	"		if (eoi)",
	"		{	t = trans[ot][tt];",
	"#ifdef VERBOSE",
	"			printf(\"randomizer: suppressed, saw else\\n\");",
	"#endif",
	"		} else",
	"		{	eoi = rand()%%ooi;",
	"#ifdef VERBOSE",
	"			printf(\"randomizer: skip %%d in %%d\\n\", eoi, ooi);",
	"#endif",
	"			for (t = trans[ot][tt]; t; t = t->nxt)",
	"				if (eoi-- <= 0) break;",
	"		}",
	"DOMORE:",
	"		for ( ; t && ooi > 0; t = t->nxt, ooi--)",
	"#else",
	"		for (t = trans[ot][tt]; t; t = t->nxt)",
	"#endif",
	"		{",
	"#ifdef HAS_UNLESS",
	"			/* exploring all transitions from",
	"			 * a single escape state suffices",
	"			 */",
	"			if (trpt->e_state > 0",
	"			&&  trpt->e_state != t->e_trans)",
	"			{",
		"#ifdef DEBUG",
	"		printf(\"skip 2nd escape %%d (did %%d before)\\n\",",
	"			t->e_trans, trpt->e_state);",
		"#endif",
	"				break;",
	"			}",
	"#endif",
	"			(trpt+1)->o_t = t;",	/* for uerror */
	"#ifdef INLINE",
	"#include FORWARD_MOVES",
	"P999:			/* jumps here when move succeeds */",
	"#else",
	"			if (!(_m = do_transit(t, II))) continue;",
	"#endif",
	"			if (boq == -1)",
"#ifdef CTL",
	"	/* for branching-time, can accept reduction only if */",
	"	/* the persistent set contains just 1 transition */",
	"			{	if ((trpt->tau&32) && (trpt->o_pm&1))",
	"					trpt->tau |= 16;",
	"				trpt->o_pm |= 1; /* we moved */",
	"			}",
"#else",
	"				trpt->o_pm |= 1; /* we moved */",
"#endif",
	"#ifdef PEG",
	"			peg[t->forw]++;",
	"#endif",

	"#if defined(VERBOSE) || defined(CHECK)",
		"#if defined(SVDUMP)",
	"			printf(\"%%3d: proc %%d exec %%d \\n\", ",
	"				depth, II, t->t_id);",