pangen1.h

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

	"			trcnt++, ntrpt->pr, ntrpt->o_t->t_id);",
	"		j = strlen(snap);",
	"		if (write(fd, snap, j) != j)",
	"		{       printf(\"pan: error writing %%s\\n\", fnm);",
	"			pan_exit(1);",
	"	}	}",
	"	close(fd);",
	"	if (errors >= upto && upto != 0)",
	"	{	wrapup();",
	"	}",
	"}",
	"#endif",	/* BFS */
	0,
};

static char *Code2d[] = {
	"clock_t start_time;",
	"#if NCORE>1",
	"clock_t crash_stamp;",
	"#endif",
	"#if !defined(WIN32) && !defined(WIN64)",
	"struct tms start_tm;",
	"#endif",
	"",
	"void",
	"start_timer(void)",
	"{",
	"#if defined(WIN32) || defined(WIN64)",
	"	start_time = clock();",
	"#else",
	"	start_time = times(&start_tm);",
	"#endif",
	"}",
	"",
	"void",
	"stop_timer(void)",
	"{	clock_t stop_time;",
	"	double delta_time;",
	"#if !defined(WIN32) && !defined(WIN64)",
	"	struct tms stop_tm;",
	"	stop_time = times(&stop_tm);",
	"	delta_time = ((double) (stop_time - start_time)) / ((double) sysconf(_SC_CLK_TCK));",
	"#else",
	"	stop_time = clock();",
	"	delta_time = ((double) (stop_time - start_time)) / ((double) CLOCKS_PER_SEC);",
	"#endif",
	"	if (readtrail || delta_time < 0.00) return;",
	"#if NCORE>1",
	"	if (core_id == 0 && nstates > (double) 0)",
	"	{	printf(\"\\ncpu%%d: elapsed time %%.3g seconds (%%g states visited)\\n\", core_id, delta_time, nstates);",
	"		if (delta_time > 0.01)",
	"		{	printf(\"cpu%%d: rate %%g states/second\\n\", core_id, nstates/delta_time);",
	"		}",
	"		{ void check_overkill(void);",
	"	 	  check_overkill();",
	"	}	}",
	"#else",
	"	printf(\"\\npan: elapsed time %%.3g seconds\\n\", delta_time);",
	"	if (delta_time > 0.01)",
	"	{	printf(\"pan: rate %%9.8g states/second\\n\", nstates/delta_time);",
	"		if (verbose)",
	"		{	printf(\"pan: avg transition delay %%.5g usec\\n\",",
	"				delta_time/(nstates+truncs));",
	"	}	}",
	"#endif",
	"}",
	"",
	"#if NCORE>1",
	"#ifdef T_ALERT",
	"double t_alerts[17];",
	"",
	"void",
	"crash_report(void)",
	"{	int i;",
	"	printf(\"crash alert intervals:\\n\");",
	"	for (i = 0; i < 17; i++)",
	"	{	printf(\"%%d\\t%%g\\n\", i, t_alerts[i]);",
	"}	}",
	"#endif",
	"",
	"void",
	"crash_reset(void)",
	"{	/* false alarm */",
	"	if (crash_stamp != (clock_t) 0)",
	"	{",
	"#ifdef T_ALERT",
	"		double delta_time;",
	"		int i;",
		"#if defined(WIN32) || defined(WIN64)",
	"		delta_time = ((double) (clock() - crash_stamp)) / ((double) CLOCKS_PER_SEC);",
		"#else",
	"		delta_time = ((double) (times(&start_tm) - crash_stamp)) / ((double) sysconf(_SC_CLK_TCK));",
		"#endif",
	"		for (i = 0; i < 16; i++)",
	"		{	if (delta_time <= (i*30))",
	"			{	t_alerts[i] = delta_time;",
	"				break;",
	"		}	}",
	"		if (i == 16) t_alerts[i] = delta_time;",
	"#endif",
	"		if (verbose)",
	"		printf(\"cpu%%d: crash alert off\\n\", core_id);",
	"	}",
	"	crash_stamp = (clock_t) 0;",
	"}",
	"",
	"int",
	"crash_test(double maxtime)",
	"{	double delta_time;",
	"	if (crash_stamp == (clock_t) 0)",
	"	{	/* start timing */",
	"#if defined(WIN32) || defined(WIN64)",
	"		crash_stamp = clock();",
	"#else",
	"		crash_stamp = times(&start_tm);",
	"#endif",
	"		if (verbose)",
	"		{	printf(\"cpu%%d: crash detection\\n\", core_id);",
	"		}",
	"		return 0;",
	"	}",
	"#if defined(WIN32) || defined(WIN64)",
	"	delta_time = ((double) (clock() - crash_stamp)) / ((double) CLOCKS_PER_SEC);",
	"#else",
	"	delta_time = ((double) (times(&start_tm) - crash_stamp)) / ((double) sysconf(_SC_CLK_TCK));",
	"#endif",
	"	return (delta_time >= maxtime);",
	"}",
	"#endif",
	"",
	"void",
	"do_the_search(void)",
	"{	int i;",
	"	depth = mreached = 0;",
	"	trpt = &trail[0];",
	"#ifdef VERI",
	"	trpt->tau |= 4;	/* the claim moves first */",
	"#endif",
	"	for (i = 0; i < (int) now._nr_pr; i++)",
	"	{	P0 *ptr = (P0 *) pptr(i);",
	"#ifndef NP",
	"		if (!(trpt->o_pm&2)",
	"		&&  accpstate[ptr->_t][ptr->_p])",
	"		{	trpt->o_pm |= 2;",
	"		}",
	"#else",
	"		if (!(trpt->o_pm&4)",
	"		&&  progstate[ptr->_t][ptr->_p])",
	"		{	trpt->o_pm |= 4;",
	"		}",
	"#endif",
	"	}",
	"#ifdef EVENT_TRACE",
	"#ifndef NP",
	"	if (accpstate[EVENT_TRACE][now._event])",
	"	{	trpt->o_pm |= 2;",
	"	}",
	"#else",
	"	if (progstate[EVENT_TRACE][now._event])",
	"	{	trpt->o_pm |= 4;",
	"	}",
	"#endif",
	"#endif",
	"#ifndef NOCOMP",
	"	Mask[0] = Mask[1] = 1;	/* _nr_pr, _nr_qs */",
	"	if (!a_cycles)",
	"	{	i = &(now._a_t) - (uchar *) &now;",
	"		Mask[i] = 1; /* _a_t */",
	"	}",
	"#ifndef NOFAIR",
	"	if (!fairness)",
	"	{	int j = 0;",
	"		i = &(now._cnt[0]) - (uchar *) &now;",
	"		while (j++ < NFAIR)",
	"			Mask[i++] = 1; /* _cnt[] */",
	"	}",
	"#endif",
	"#endif",
	"#ifndef NOFAIR",
	"	if (fairness",
	"	&&  (a_cycles && (trpt->o_pm&2)))",
	"	{	now._a_t = 2;	/* set the A-bit */",
	"		now._cnt[0] = now._nr_pr + 1;",	/* NEW: +1 */
		"#ifdef VERBOSE",
	"	printf(\"%%3d: fairness Rule 1, cnt=%%d, _a_t=%%d\\n\",",
	"		depth, now._cnt[now._a_t&1], now._a_t);",
		"#endif",
	"	}",
	"#endif",

	"	c_stack_start = (char *) &i; /* meant to be read-only */",

	"#if defined(HAS_CODE) && defined (C_INIT)",
	"	C_INIT; /* initialization of data that must precede fork() */",
	"	c_init_done++;",
	"#endif",

	"#if defined(C_States) && (HAS_TRACK==1)",
	"	/* capture initial state of tracked C objects */",
	"	c_update((uchar *) &(now.c_state[0]));",
	"#endif",

	"#ifdef HAS_CODE",
	"	if (readtrail) getrail(); /* no return */",
	"#endif",
	"	start_timer();",
	"#ifdef BFS",
	"	bfs();",
	"#else",
		"#if defined(C_States) && defined(HAS_STACK) && (HAS_TRACK==1)",
		"	/* initial state of tracked & unmatched objects */",
		"	c_stack((uchar *) &(svtack->c_stack[0]));",
		"#endif",
		"#ifdef RANDOMIZE",
	"	srand(123);",
		"#endif",
	"#if NCORE>1",
	"	mem_get();",
	"#else",
	"	new_state();	/* start 1st DFS */",
	"#endif",
	"#endif",
	"}",

	"#ifdef INLINE_REV",
	"uchar",
	"do_reverse(Trans *t, short II, uchar M)",
	"{	uchar _m = M;",
	"	int  tt = (int) ((P0 *)this)->_p;",
	"#include REVERSE_MOVES",
	"R999:	return _m;",
	"}",
	"#endif",

	"#ifndef INLINE",
	"#ifdef EVENT_TRACE",
	"static char _tp = 'n'; static int _qid = 0;",
	"#endif",
	"uchar",
	"do_transit(Trans *t, short II)",
	"{	uchar _m = 0;",
	"	int  tt = (int) ((P0 *)this)->_p;",
	"#ifdef M_LOSS",
	"	uchar delta_m = 0;",
	"#endif",
	"#ifdef EVENT_TRACE",
	"	short oboq = boq;",
	"	uchar ot = (uchar)  ((P0 *)this)->_t;",
	"	if (ot == EVENT_TRACE) boq = -1;",
		"#define continue	{ boq = oboq; return 0; }",
	"#else",
		"#define continue	return 0",
		"#ifdef SEPARATE",
	"	uchar ot = (uchar)  ((P0 *)this)->_t;",
		"#endif",
	"#endif",
	"#include FORWARD_MOVES",
	"P999:",
	"#ifdef EVENT_TRACE",
	"	if (ot == EVENT_TRACE) boq = oboq;",
	"#endif",
	"	return _m;",
	"#undef continue",
	"}",

	"#ifdef EVENT_TRACE",
	"void",
	"require(char tp, int qid)",
	"{	Trans *t;",
	"	_tp = tp; _qid = qid;",
	"",
	"	if (now._event != endevent)",
	"	for (t = trans[EVENT_TRACE][now._event]; t; t = t->nxt)",
	"	{	if (do_transit(t, EVENT_TRACE))",
	"		{	now._event = t->st;",
	"			reached[EVENT_TRACE][t->st] = 1;",
	"#ifdef VERBOSE",
	"	printf(\"	event_trace move to -> %%d\\n\", t->st);",
	"#endif",
	"#ifndef BFS",
		"#ifndef NP",
	"			if (accpstate[EVENT_TRACE][now._event])",
	"				(trpt+1)->o_pm |= 2;",
		"#else",
	"			if (progstate[EVENT_TRACE][now._event])",
	"				(trpt+1)->o_pm |= 4;",
		"#endif",
	"#endif",
	"#ifdef NEGATED_TRACE",
	"			if (now._event == endevent)",
	"			{",
		"#ifndef BFS",
	"				depth++; trpt++;",
		"#endif",
	"				uerror(\"event_trace error (all events matched)\");",
		"#ifndef BFS",
	"				trpt--; depth--;",
		"#endif",
	"				break;",
	"			}",
	"#endif",
	"			for (t = t->nxt; t; t = t->nxt)",
	"			{	if (do_transit(t, EVENT_TRACE))",
	"				 Uerror(\"non-determinism in event-trace\");",
	"			}",
	"			return;",
	"		}",
	"#ifdef VERBOSE",
	"		 else",
	"	printf(\"	event_trace miss '%%c' -- %%d, %%d, %%d\\n\",",
	"			tp, qid, now._event, t->forw);",
	"#endif",
	"	}",
	"#ifdef NEGATED_TRACE",
	"	now._event = endevent; /* only 1st try will count -- fixed 4.2.6 */",
	"#else",	
		"#ifndef BFS",
	"	depth++; trpt++;",
		"#endif",
	"	uerror(\"event_trace error (no matching event)\");",
		"#ifndef BFS",
	"	trpt--; depth--;",
		"#endif",
	"#endif",
	"}",
	"#endif",

	"int",
	"enabled(int iam, int pid)",
	"{	Trans *t; uchar *othis = this;",
	"	int res = 0; int tt; uchar ot;",
	"#ifdef VERI",
	"	/* if (pid > 0) */ pid++;",
	"#endif",
	"	if (pid == iam)",
	"		Uerror(\"used: enabled(pid=thisproc)\");",
	"	if (pid < 0 || pid >= (int) now._nr_pr)",
	"		return 0;",
	"	this = pptr(pid);",
	"	TstOnly = 1;",
	"	tt = (int) ((P0 *)this)->_p;",
	"	ot = (uchar) ((P0 *)this)->_t;",
	"	for (t = trans[ot][tt]; t; t = t->nxt)",
	"		if (do_transit(t, (short) pid))",
	"		{	res = 1;",
	"			break;",
	"		}",
	"	TstOnly = 0;",
	"	this = othis;",
	"	return res;",
	"}",
	"#endif",
	"void",
	"snap_time(void)",
	"{	clock_t stop_time;",
	"	double delta_time;",
	"#if !defined(WIN32) && !defined(WIN64)",
	"	struct tms stop_tm;",
	"	stop_time  = times(&stop_tm);",
	"	delta_time = ((double) (stop_time - start_time)) / ((double) sysconf(_SC_CLK_TCK));",
	"#else",
	"	stop_time  = clock();",
	"	delta_time = ((double) (stop_time - start_time)) / ((double) CLOCKS_PER_SEC);",
	"#endif",
	"	printf(\"t= %%-7.3g \", delta_time);",
	"	if (delta_time > 0.01)",
	"	{	printf(\"R= %%-9g\", nstates/delta_time);",
	"	}",
	"	printf(\"\\n\");",
	"}",
	"void",
	"snapshot(void)",
	"{",
	"#if NCORE>1",
	"	enter_critical(GLOBAL_LOCK);	/* snapshot */",
	"	printf(\"cpu%%d: \", core_id);",
	"#endif",
	"	printf(\"Depth= %%7ld States= %%-8g \",",
	"#if NCORE>1",
	"		(long) (nr_handoffs * z_handoff) +",
	"#endif",
	"		mreached, nstates);",
	"	printf(\"Transitions= %%-8g \", nstates+truncs);",
	"#ifdef MA",
	"	printf(\"Nodes= %%7d \", nr_states);",
	"#endif",
	"	printf(\"Memory= %%-9.5g\\t\", memcnt/1048576.);",
	"	snap_time();",
	"	fflush(stdout);",
	"#if NCORE>1",
	"	leave_critical(GLOBAL_LOCK);",
	"#endif",
	"}",

	"#ifdef SC",
	"void",
	"stack2disk(void)",
	"{",
	"	if (!stackwrite",
	"	&&  (stackwrite = creat(stackfile, TMODE)) < 0)",
	"		Uerror(\"cannot create stackfile\");",
	"",
	"	if (write(stackwrite, trail, DDD*sizeof(Trail))",
	"	!=  DDD*sizeof(Trail))",
	"		Uerror(\"stackfile write error -- disk is full?\");",
	"",
	"	memmove(trail, &trail[DDD], (HHH-DDD+2)*sizeof(Trail));",
	"	memset(&trail[HHH-DDD+2], 0, (omaxdepth - HHH + DDD - 2)*sizeof(Trail));",
	"	CNT1++;",
	"}",
	"void",
	"disk2stack(void)",
	"{	long have;",
	"",
	"	CNT2++;",
	"	memmove(&trail[DDD], trail, (HHH-DDD+2)*sizeof(Trail));",
	"",
	"	if (!stackwrite",
	"	||  lseek(stackwrite, -DDD* (off_t) sizeof(Trail), SEEK_CUR) == -1)",
	"		Uerror(\"disk2stack lseek error\");",
	"",
	"	if (!stackread",
	"	&&  (stackread = open(stackfile, 0)) < 0)",
	"		Uerror(\"cannot open stackfile\");",
	"",
	"	if (lseek(stackread, (CNT1-CNT2)*DDD* (off_t) sizeof(Trail), SEEK_SET) == -1)",
	"		Uerror(\"disk2stack lseek error\");",
	"",
	"	have = read(stackread, trail, DDD*sizeof(Trail));",
	"	if (have !=  DDD*sizeof(Trail))",
	"		Uerror(\"stackfile read error\");",
	"}",
	"#endif",

	"uchar *",
	"Pptr(int x)",	/* as a fct, to avoid a problem with the p9 compiler */
	"{	if (x < 0 || x >= MAXPROC || !proc_offset[x])",	/* does not exist */
	"		return noptr;",
	"	else",
	"		return (uchar *) pptr(x);",
	"}",
	"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))",
	"",
	"#ifdef NSUCC",
	"int N_succ[512];",
	"void",
	"tally_succ(int cnt)",
	"{	if (cnt < 512) N_succ[cnt]++;",
	"	else printf(\"tally_succ: cnt %%d exceeds range\\n\", cnt);",
	"}",
	"",
	"void",
	"dump_succ(void)",
	"{	int i; double sum = 0.0;",
	"	double w_avg = 0.0;",
	"	printf(\"Successor counts:\\n\");",
	"	for (i = 0; i < 512; i++)",
	"	{	sum += (double) N_succ[i];",
	"	}",
	"	for (i = 0; i < 512; i++)",
	"	{	if (N_succ[i] > 0)",
	"		{	printf(\"%%3d\t%%10d\t(%%.4g %%%% of total)\\n\",",
	"				i, N_succ[i], (100.0 * (double) N_succ[i])/sum);",
	"			w_avg += (double) i * (double) N_succ[i];",
	"	}	}",
	"	if (sum > N_succ[0])",
	"	printf(\"mean %%.4g (without 0: %%.4g)\\n\", w_avg / sum, w_avg / (sum - (double) N_succ[0]));",
	"}",
	"#endif",
	"",
	"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;",