pangen1.h

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

	"	int tt;",
	"	short From = now._nr_pr-1, To = BASE;",
	"Down:",
	"#ifdef CHECK",
	"	cpu_printf(\"%%d: Down - %%s %%saccepting [pids %%d-%%d]\\n\",",
	"		depth, (trpt->tau&4)?\"claim\":\"program\",",
	"		(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",
	"#ifdef NSUCC",
	"	trpt->n_succ = 0;",
	"#endif",

	"#if defined(BUDGET)",
	"	if (budget < 1.0)",
	"	{	goto deficit;",
	"	}",
	"#endif",

	"#if NCORE>1",
	"	if (mem_hand_off())",
	"	{",
	"#if SYNC",
	"		(trpt+1)->o_n = 1;	/* not a deadlock: as below  */",
	"#endif",
	"#ifndef LOOPSTATE",
	"		(trpt-1)->tau |= 16;	/* worstcase guess: as below */",
	"#endif",
	"#if NCORE>1 && defined(FULL_TRAIL)",
	"		if (upto > 0)",
	"		{	Pop_Stack_Tree();",
	"		}",
	"#endif",
	"		goto Up;",
	"	}",
	"#endif",

	"	if (depth >= maxdepth)",
	"	{	if (!warned)",
	"		{ warned = 1;",
	"		  printf(\"error: max search depth too small\\n\");",
	"		}",
	"		if (bounded)",
	"		{	uerror(\"depth limit reached\");",
	"		}",
	"#if defined(BUDGET)",
	"deficit:",
	"#endif",
	"		truncs++;",
	"#if SYNC",
	"		(trpt+1)->o_n = 1; /* not a deadlock */",
	"#endif",
	"#ifndef LOOPSTATE",
	"		(trpt-1)->tau |= 16;	/* worstcase guess */",
	"#endif",

	"#if NCORE>1 && defined(FULL_TRAIL)",
	"		if (upto > 0)",
	"		{	Pop_Stack_Tree();",
	"		}",
	"#endif",
	"		goto Up;",
	"	}",
	"AllOver:",
	"#if (defined(FULLSTACK) && !defined(MA)) || NCORE>1",
	"	/* if atomic or rv move, carry forward previous state */",
	"	trpt->ostate = (trpt-1)->ostate;",	/* was: = (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",
	"#if NCORE>1 && defined(FULL_TRAIL)",
	"			if (upto > 0)",
	"			{	Pop_Stack_Tree();",
	"			}",
	"#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);",

				/* II==0 new state */
				/* II==1 old state */
				/* II==2 on current dfs stack */
				/* II==3 on 1st dfs stack */
	"#ifndef SAFETY",

		"#if NCORE==1 || defined (SEP_STATE)",	/* or else we don't know which stack its on */
	"			if (II == 2 && ((trpt->o_pm&2) || ((trpt-1)->o_pm&2)))",
	"			{	II = 3; /* Schwoon & Esparza 2005, Gastin&Moro 2004 */",
			"#ifdef VERBOSE",
	"				printf(\"state match on dfs stack\\n\");",
			"#endif",
	"				goto same_case;",
	"			}",
		"#endif",

		"#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",
	"			   {",
		"#ifndef BITSTATE",
	"				nShadow--;",
		"#endif",
	"same_case:			if (Lstate) depthfound = Lstate->D;",
		"#ifdef NP",
	"				uerror(\"non-progress cycle\");",
		"#else",
	"				uerror(\"acceptance cycle\");",
		"#endif",
	"#if NCORE>1 && defined(FULL_TRAIL)",
	"				if (upto > 0)",
	"				{	Pop_Stack_Tree();",
	"				}",
	"#endif",
	"				goto Up;",
	"			   }",
	"			}",
	"#endif",

	"#ifndef NOREDUCE",
		"#ifndef SAFETY",
	"#if NCORE>1 && !defined(SEP_STATE) && defined(V_PROVISO)",
	"			if (II != 0 && (!Lstate || Lstate->cpu_id < core_id))",
	"			{	(trpt-1)->tau |= 16;",	/* treat as a stack state */
	"			}",
	"#endif",
	"			if ((II && JJ) || (II == 3))",
	"			{	/* marker for liveness proviso */",
	"#ifndef LOOPSTATE",
	"				(trpt-1)->tau |= 16;",	/* truncated on stack */
	"#endif",
	"				truncs2++;",
	"			}",
		"#else",
	"#if NCORE>1 && !defined(SEP_STATE) && defined(V_PROVISO)",
	"			if (!(II != 0 && (!Lstate || Lstate->cpu_id < core_id)))",
	"			{	/* treat as stack state */",
	"				(trpt-1)->tau |= 16;",
	"			} else",
	"			{	/* treat as non-stack state */",
	"				(trpt-1)->tau |= 64;",
	"			}",
	"#endif",
	"			if (!II || !JJ)",
	"			{	/* successor outside stack */",
	"				(trpt-1)->tau |= 64;",
	"			}",
		"#endif",
	"#endif",
	"			if (II)",
	"			{	truncs++;",
	"#if NCORE>1 && defined(FULL_TRAIL)",
	"				if (upto > 0)",
	"				{	Pop_Stack_Tree();",
	"					if (depth == 0)",
	"					{	return;",
	"				}	}",
	"#endif",
	"				goto Up;",
	"			}",
	"#ifndef FREQ",
	"#define FREQ	(1000000)",
	"#endif",
	"			if (!kk)",
	"			{	static long sdone = (long) 0; long ndone;",
	"				nstates++;",
	"#if defined(BUDGET)",
	"				budget--;",
	"#endif",
	"				ndone = (unsigned long) (nstates/((double) FREQ));",
	"				if (ndone != sdone)",
	"				{	snapshot();",
	"					sdone = ndone;",
	"				}",
	"#ifdef SVDUMP",
	"				if (vprefix > 0)",
	"				if (write(svfd, (uchar *) &now, vprefix) != vprefix)",
	"				{	fprintf(efd, \"writing %%s.svd failed\\n\", PanSource);",
	"					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",
	"#else",
	"	#if NCORE>1",
	"			trpt->ostate = Lstate;",
	"	#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) */",
	"	if (boq == -1 && From != To",
"#ifdef SAFETY",
	"#if NCORE>1",
	"	&& (depth < z_handoff)", /* not for border states */
	"#endif",
	"	)",
"#else",
	"#if NCORE>1",
	"	&& ((a_cycles) || (!a_cycles && depth < z_handoff))",
	"#endif",
	"	&&  (!(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))", /* proviso bit in _a_t */
			"#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",
	"	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; /* the process preselected */",
	"#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",
	"",
	"#ifndef THROTTLE",
	"#define THROTTLE	1.5",	/* some value >= 1 */
	"#endif",
	"#if defined(BUDGET)",
	"	if (From > To)"	/* more than one successor likely */
	"	{	budget /= THROTTLE;", /* reduce budget */
	"	}",
	"#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",
	"