pangen6.h

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

	"		}",
	"	#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",
	"",
	"	#if defined(C_States) && (HAS_TRACK==1)",
	"		/* restore state of tracked C objects */",
	"		c_revert((uchar *) &(now.c_state[0]));",
	"		#if (HAS_STACK==1)",
	"		c_unstack((uchar *) f->m_c_stack); /* unmatched tracked data */",
	"		#endif",
	"	#endif",
	"	return 1;",
	"}",
	"",
	"void",
	"write_root(void)	/* for trail file */",
	"{	int fd;",
	"",
	"	if (iterative == 0 && Nr_Trails > 1)",
	"		sprintf(fnm, \"%%s%%d.%%s\", TrailFile, Nr_Trails-1, sprefix);",
	"	else",
	"		sprintf(fnm, \"%%s.%%s\", TrailFile, sprefix);",
	"",
	"	if (cur_Root.m_vsize == 0)",
	"	{	(void) unlink(fnm); /* remove possible old copy */",
	"		return;	/* its the default initial state */",
	"	}",
	"",
	"	if ((fd = creat(fnm, TMODE)) < 0)",
	"	{	char *q;",
	"		if ((q = strchr(TrailFile, \'.\')))",
	"		{	*q = \'\\0\';		/* strip .pml */",
	"			if (iterative == 0 && Nr_Trails-1 > 0)",
	"				sprintf(fnm, \"%%s%%d.%%s\", TrailFile, Nr_Trails-1, sprefix);",
	"			else",
	"				sprintf(fnm, \"%%s.%%s\", TrailFile, sprefix);",
	"			*q = \'.\';",
	"			fd = creat(fnm, TMODE);",
	"		}",
	"		if (fd < 0)",
	"		{	cpu_printf(\"pan: cannot create %%s\\n\", fnm);",
	"			perror(\"cause\");",
	"			return;",
	"	}	}",
	"",
	"	if (write(fd, &cur_Root, sizeof(SM_frame)) != sizeof(SM_frame))",
	"	{	cpu_printf(\"pan: error writing %%s\\n\", fnm);",
	"	} else",
	"	{	cpu_printf(\"pan: wrote %%s\\n\", fnm);",
	"	}",
	"	close(fd);",
	"}",
	"",
	"void",
	"set_root(void)",
	"{	int fd;",
	"	char *q;",
	"	char MyFile[512];",	/* enough to hold a reasonable pathname */
	"	char MySuffix[16];",
	"	char *ssuffix = \"rst\";",
	"	int  try_core = 1;",
	"",
	"	strcpy(MyFile, TrailFile);",
	"try_again:",
	"	if (whichtrail > 0)",
	"	{	sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, ssuffix);",
	"		fd = open(fnm, O_RDONLY, 0);",
	"		if (fd < 0 && (q = strchr(MyFile, \'.\')))",
	"		{	*q = \'\\0\';	/* strip .pml */",
	"			sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, ssuffix);",
	"			*q = \'.\';",
	"			fd = open(fnm, O_RDONLY, 0);",
	"		}",
	"	} else",
	"	{	sprintf(fnm, \"%%s.%%s\", MyFile, ssuffix);",
	"		fd = open(fnm, O_RDONLY, 0);",
	"		if (fd < 0 && (q = strchr(MyFile, \'.\')))",
	"		{	*q = \'\\0\';	/* strip .pml */",
	"			sprintf(fnm, \"%%s.%%s\", MyFile, ssuffix);",
	"			*q = \'.\';",
	"			fd = open(fnm, O_RDONLY, 0);",
	"	}	}",
	"",
	"	if (fd < 0)",
	"	{	if (try_core < NCORE)",
	"		{	ssuffix = MySuffix;",
	"			sprintf(ssuffix, \"cpu%%d_rst\", try_core++);",
	"			goto try_again;",
	"		}",
	"		cpu_printf(\"no file '%%s.rst' or '%%s' (not an error)\\n\", MyFile, fnm);",
	"	} else",
	"	{	if (read(fd, &cur_Root, sizeof(SM_frame)) != sizeof(SM_frame))",
	"		{	cpu_printf(\"read error %%s\\n\", fnm);",
	"			close(fd);",
	"			pan_exit(1);",
	"		}",
	"		close(fd);",
	"		(void) unpack_state(&cur_Root, -2);",
	"#ifdef SEP_STATE",
	"		cpu_printf(\"partial trail -- last few steps only\\n\");",
	"#endif",
	"		cpu_printf(\"restored root from '%%s'\\n\", fnm);",
	"		printf(\"=====State:=====\\n\");",
	"		{	int i, j; P0 *z;",
	"			for (i = 0; i < now._nr_pr; i++)",
	"			{	z = (P0 *)pptr(i);",
	"				printf(\"proc %%2d (%%s) \", i, procname[z->_t]);",

	"				for (j = 0; src_all[j].src; j++)",
	"				if (src_all[j].tp == (int) z->_t)",
	"				{	printf(\" line %%3d \\\"%%s\\\" \",",
	"						src_all[j].src[z->_p], PanSource);",
	"					break;",
	"				}",
	"				printf(\"(state %%d)\\n\", z->_p);",
	"				c_locals(i, z->_t);",
	"			}",
	"			c_globals();",
	"		}",
	"		printf(\"================\\n\");",
	"	}",
	"}",
	"",
	"#ifdef USE_DISK",
	"unsigned long dsk_written, dsk_drained;",
	"void mem_drain(void);",
	"#endif",
	"",
	"void",
	"m_clear_frame(SM_frame *f)", /* clear room for stats */
	"{	int i, clr_sz = sizeof(SM_results);",
	"",
	"	for (i = 0; i <= _NP_; i++)	/* all proctypes */",
	"	{	clr_sz += NrStates[i]*sizeof(uchar);",
	"	}",
	"	memset(f, 0, clr_sz);",
	"	/* caution if sizeof(SM_results) > sizeof(SM_frame) */",
	"}",
	"",
	"void",
	"Read_Queue(int q)",
	"{	SM_frame   *f, *of;",
	"	int	remember, target_q;",
	"	SM_results *r;",
	"	double patience = 0.0;",
	"",
	"	target_q = (q + 1) %% NCORE;",
	"",
	"	for (;;)",
	"	{	f = Get_Full_Frame(q);",
	"		if (!f)	/* 1 second timeout -- and trigger for Query */",
	"		{	if (someone_crashed(2))",
	"			{	printf(\"cpu%%d: search terminated [code %%d]\\n\",",
	"					core_id, search_terminated?*search_terminated:-1);",
	"				sudden_stop(\"\");",
	"				pan_exit(1);",
	"			}",
	"#ifdef TESTING",
	"	/* to profile with cc -pg and gprof pan.exe -- set handoff depth beyond maxdepth */",
	"	exit(0);",
	"#endif",
	"			remember = *grfree;",
	"			if (core_id == 0		/* root can initiate termination */",
	"			&& remote_party == 0		/* and only the original root */",
	"			&& query_in_progress == 0	/* unless its already in progress */",
	"			&& remember == *grfull		/* global queue is empty */",
	"			&& TargetQ_NotFull(target_q))	/* avoid getting wedged */",
	"			{	f = Get_Free_Frame(target_q);",
	"				query_in_progress = 1;	/* only root process can do this */",
	"				if (!f) { Uerror(\"Fatal1: no free slot\"); }",
	"				f->m_boq = QUERY;	/* initiate Query */",
	"				if (verbose)",
	"				{  cpu_printf(\"snd QUERY to q%%d (%%d) into slot %%d\\n\",",
	"					target_q, nstates_get + 1, prfree[target_q]-1);",
	"				}",
	"				f->m_vsize = remember + 1;",
	"				/* number will not change unless we receive more states */",
	"			} else if (patience++ > OneHour) /* one hour watchdog timer */",
	"			{	cpu_printf(\"timeout -- giving up\\n\");",
	"				sudden_stop(\"queue timeout\");",
	"				pan_exit(1);",
	"			}",
	"			if (0) cpu_printf(\"timed out -- try again\\n\");",
	"			continue;	",
	"		}",
	"		patience = 0.0; /* reset watchdog */",
	"",
	"		if (f->m_boq == QUERY)",
	"		{	if (verbose)",
	"			{	cpu_printf(\"got QUERY on q%%d (%%d <> %%d) from slot %%d\\n\",",
	"					q, f->m_vsize, nstates_put + 1, prfull[q]-1);",
	"				snapshot();",
	"			}",
	"			remember = f->m_vsize;",
	"			f->m_vsize = 0;	/* release slot */",
	"",
	"			if (core_id == 0 && remote_party == 0)	/* original root cpu0 */",
	"			{	if (query_in_progress == 1	/* didn't send more states in the interim */",
	"				&&  *grfree + 1 == remember)	/* no action on global queue meanwhile */",
	"				{	if (verbose) cpu_printf(\"Termination detected\\n\");",
	"					if (!TargetQ_NotFull(target_q))",
	"					{	if (verbose)",
	"						cpu_printf(\"warning: target q is full\\n\");",
	"					}",
	"					f = Get_Free_Frame(target_q);",
	"					if (!f) { Uerror(\"Fatal2: no free slot\"); }",
	"					m_clear_frame(f);",
	"					f->m_boq = QUIT; /* send final Quit, collect stats */",
	"					f->m_vsize = 111; /* anything non-zero will do */",
	"					if (verbose)",
	"					cpu_printf(\"put QUIT on q%%d\\n\", target_q);",
	"				} else",
	"				{	if (verbose) cpu_printf(\"Stale Query\\n\");",
	"#ifdef USE_DISK",
	"					mem_drain();",
	"#endif",
	"				}",
	"				query_in_progress = 0;",
	"			} else",
	"			{	if (!TargetQ_NotFull(target_q))",
	"				{	if (verbose)",
	"					cpu_printf(\"warning: forward query - target q full\\n\");",
	"				}",
	"				f = Get_Free_Frame(target_q);",
	"				if (verbose)",
	"				cpu_printf(\"snd QUERY response to q%%d (%%d <> %%d) in slot %%d\\n\",",
	"					target_q, remember, *grfree + 1, prfree[target_q]-1);",
	"				if (!f) { Uerror(\"Fatal4: no free slot\"); }",
	"",
	"				if (*grfree + 1 == remember)	/* no action on global queue */",
	"				{	f->m_boq = QUERY;	/* forward query, to root */",
	"					f->m_vsize = remember;",
	"				} else",
	"				{	f->m_boq = QUERY_F;	/* no match -- busy */",
	"					f->m_vsize = 112;	/* anything non-zero */",
	"#ifdef USE_DISK",
	"					if (dsk_written != dsk_drained)",
	"					{	mem_drain();",
	"					}",
	"#endif",
	"				}",
	"			}",
	"			continue;",
	"		}",
	"",
	"		if (f->m_boq == QUERY_F)",
	"		{	if (verbose)",
	"			{	cpu_printf(\"got QUERY_F on q%%d from slot %%d\\n\", q, prfull[q]-1);",
	"			}",
	"			f->m_vsize = 0;	/* release slot */",
	"",
	"			if (core_id == 0 && remote_party == 0)		/* original root cpu0 */",
	"			{	if (verbose) cpu_printf(\"No Match on Query\\n\");",
	"				query_in_progress = 0;",
	"			} else",
	"			{	if (!TargetQ_NotFull(target_q))",
	"				{	if (verbose) cpu_printf(\"warning: forwarding query_f, target queue full\\n\");",
	"				}",
	"				f = Get_Free_Frame(target_q);",
	"				if (verbose) cpu_printf(\"forward QUERY_F to q%%d into slot %%d\\n\",",
	"						target_q, prfree[target_q]-1);",
	"				if (!f) { Uerror(\"Fatal5: no free slot\"); }",
	"				f->m_boq = QUERY_F;		/* cannot terminate yet */",
	"				f->m_vsize = 113;		/* anything non-zero */",
	"			}",
	"#ifdef USE_DISK",
	"			if (dsk_written != dsk_drained)",
	"			{	mem_drain();",
	"			}",
	"#endif",
	"			continue;",
	"		}",
	"",
	"		if (f->m_boq == QUIT)",
	"		{	if (0) cpu_printf(\"done -- local memcnt %%g Mb\\n\", memcnt/(1024.*1024.));",
	"			retrieve_info((SM_results *) f); /* collect and combine stats */",
	"			if (verbose)",
	"			{	cpu_printf(\"received Quit\\n\");",
	"				snapshot();",
	"			}",
	"			f->m_vsize = 0;	/* release incoming slot */",
	"			if (core_id != 0)",
	"			{	f = Get_Free_Frame(target_q); /* new outgoing slot */",
	"				if (!f) { Uerror(\"Fatal6: no free slot\"); }",
	"				m_clear_frame(f);	/* start with zeroed stats */",
	"				record_info((SM_results *) f);",
	"				f->m_boq = QUIT;	/* forward combined results */",
	"				f->m_vsize = 114;	/* anything non-zero */",
	"				if (verbose>1)",
	"				cpu_printf(\"fwd Results to q%%d\\n\", target_q);",
	"			}",
	"			break;			/* successful termination */",
	"		}",
	"",
	"		/* else: 0<= boq <= 255, means STATE transfer */",
	"		if (unpack_state(f, q) != 0)",
	"		{	nstates_get++;",
	"			f->m_vsize = 0;	/* release slot */",
	"			if (VVERBOSE) cpu_printf(\"Got state\\n\");",
	"",
	"			if (search_terminated != NULL",
	"			&&  *search_terminated == 0)",
	"			{	new_state();	/* explore successors */",
	"				memset((uchar *) &cur_Root, 0, sizeof(SM_frame));	/* avoid confusion */",
	"			} else",
	"			{	pan_exit(0);",
	"			}",
	"		} else",
	"		{	pan_exit(0);",
	"	}	}",
	"	if (verbose) cpu_printf(\"done got %%d put %%d\\n\", nstates_get, nstates_put);",
	"	sleep_report();",
	"}",
	"",
	"void",
	"give_up(int unused_x)",
	"{",
	"	if (search_terminated != NULL)",
	"	{	*search_terminated |= 32;	/* give_up */",
	"	}",
	"	if (!writing_trail)",
	"	{	was_interrupted = 1;",
	"		snapshot();",
	"		cpu_printf(\"Give Up\\n\");",
	"		sleep_report();",
	"		pan_exit(1);",
	"	} else /* we are already terminating */",
	"	{	cpu_printf(\"SIGINT\\n\");",
	"	}",
	"}",
	"",
	"void",
	"check_overkill(void)",
	"{	int cnt = 0;",
	"",
	"	if (core_id == 0",
	"	&&  !remote_party",
	"	&&  nstates_put > 0",
	"	&& (VMAX > vmax_seen",
	"	||  PMAX > pmax_seen",
	"	||  QMAX > qmax_seen && QMAX > 1))",
	"	{",
	"#ifdef BITSTATE",
	"		printf(\"cpu0: max values seen in this run: \");",
	"#else",
	"		printf(\"cpu0: recommend recompiling with \");",
	"#endif",
	"		cnt++;",
	"	} else",
	"	{	return;",
	"	}",
	"	if (VMAX > vmax_seen) { printf(\"-DVMAX=%%d \", vmax_seen); }",
	"	if (PMAX > pmax_seen) { printf(\"-DPMAX=%%d \", pmax_seen); }",
	"	if (QMAX > qmax_seen && QMAX > 1) { printf(\"-DQMAX=%%d \", qmax_seen==0?1:qmax_seen); }",
	"	if (cnt) printf(\"\\n\");",
	"}",
	"",
	"void",
	"mem_put(int q)	/* handoff state to other cpu, workq q */",
	"{	SM_frame *f;",
	"	int i, j;",
	"",
	"	if (vsize > VMAX)",
	"	{	printf(\"pan: recompile with -DVMAX=N with N >= %%d\\n\", vsize);",
	"		Uerror(\"aborting\");",
	"	}",
	"	if (now._nr_pr > PMAX)",
	"	{	printf(\"pan: recompile with -DPMAX=N with N >= %%d\\n\", now._nr_pr);",
	"		Uerror(\"aborting\");",
	"	}",
	"	if (now._nr_qs > QMAX)",
	"	{	printf(\"pan: recompile with -DQMAX=N with N >= %%d\\n\", now._nr_qs);",
	"		Uerror(\"aborting\");",
	"	}",
	"	if (vsize > vmax_seen) vmax_seen = vsize;",
	"	if (now._nr_pr > pmax_seen) pmax_seen = now._nr_pr;",
	"	if (now._nr_qs > qmax_seen) qmax_seen = now._nr_qs;",
	"",
	"	f = Get_Free_Frame(q);	/* not called in likely deadlock states */",
	"	if (!f) { Uerror(\"Fatal3: no free slot\"); }",
	"",
	"	if (VVERBOSE) cpu_printf(\"putting st