pangen1.h

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

/***** spin: pangen1.h *****/

/* Copyright (c) 1989-2007 by Lucent Technologies, Bell Laboratories.     */
/* All Rights Reserved.  This software is for educational purposes only.  */
/* No guarantee whatsoever is expressed or implied by the distribution of */
/* this code.  Permission is given to distribute this code provided that  */
/* this introductory message is not removed and no monies are exchanged.  */
/* Software written by Gerard J. Holzmann.  For tool documentation see:   */
/*             http://spinroot.com/                                       */
/* Send all bug-reports and/or questions to: [e-mail]            */
/* (c) 2007: small additions for V5.0 to support multi-core verifications */

static char *Code2a[] = { /* the tail of procedure run() */
	"#if defined(VERI) && !defined(NOREDUCE) && !defined(NP)",
	"	if (!state_tables",
	"#ifdef HAS_CODE",
	"	&& !readtrail",
	"#endif",
	"#if NCORE>1",
	"	&& core_id == 0",
	"#endif",
	"	)",
	"	{ printf(\"warning: for p.o. reduction to be valid \");",
	"	  printf(\"the never claim must be stutter-invariant\\n\");",
	"	  printf(\"(never claims generated from LTL \");",
	"	  printf(\"formulae are stutter-invariant)\\n\");",
	"	}",
	"#endif",
	"	UnBlock;	/* disable rendez-vous */",
	"#ifdef BITSTATE",
#ifndef POWOW
	"	if (udmem)",
	"	{	udmem *= 1024L*1024L;",
	"	#if NCORE>1",
	"		if (!readtrail)",
	"		{	void init_SS(unsigned long);",
	"			init_SS((unsigned long) udmem);",
	"		} else",
	"	#endif",
	"		SS = (uchar *) emalloc(udmem);",
	"		bstore = bstore_mod;",
	"	} else",
#endif
	"	#if NCORE>1",
	"		{ void init_SS(unsigned long);",
	"		  init_SS(ONE_L<<(ssize-3));",
	"		}",
	"	#else",
	"		SS = (uchar *) emalloc(ONE_L<<(ssize-3));",
	"	#endif",
	"#else",	/* if not BITSTATE */
	"	hinit();",
	"#endif",
	"#if defined(FULLSTACK) && defined(BITSTATE)",
	"	onstack_init();",
	"#endif",
	"#if defined(CNTRSTACK) && !defined(BFS)",
	"	LL = (uchar *) emalloc(ONE_L<<(ssize-3));",
	"#endif",
	"	stack	= ( Stack *) emalloc(sizeof(Stack));",
	"	svtack	= (Svtack *) emalloc(sizeof(Svtack));",
	"	/* a place to point for Pptr of non-running procs: */",
	"	noptr	= (uchar *) emalloc(Maxbody * sizeof(char));",
	"#ifdef SVDUMP",
	"	if (vprefix > 0)",
	"		write(svfd, (uchar *) &vprefix, sizeof(int));",
	"#endif",
	"#ifdef VERI",
	"	Addproc(VERI);	/* never - pid = 0 */",
	"#endif",
	"	active_procs();	/* started after never */",
	"#ifdef EVENT_TRACE",
	"	now._event = start_event;",
	"	reached[EVENT_TRACE][start_event] = 1;",
	"#endif",

	"#ifdef HAS_CODE",
	"	globinit();",
	"#endif",
	"#ifdef BITSTATE",
	"go_again:",
	"#endif",
	"#ifdef BUDGET",
	"	/* max nr of states that may be explored below this depth */",
	"	#ifdef BITSTATE",
	"	budget = (double) (ONE_L<<(ssize - 1));	/* every subtree can create 0.5 of max */",
	"	#else",		/* half the number of available bits */
	"	budget = (double) (ONE_L<<(ssize - 3)) / (double) (VECTORSZ); /* conservative */",
	"	#endif",	/* nr of bytes divided by max size of a state */
	"#endif",
	"	do_the_search();",
	"#ifdef BITSTATE",
	"	if (--Nrun > 0 && HASH_CONST[++HASH_NR])",
	"	{	printf(\"Run %%d:\\n\", HASH_NR);",
	"		wrap_stats();",
	"		printf(\"\\n\");",
	"		memset(SS, 0, ONE_L<<(ssize-3));",
		"#if defined(CNTRSTACK)",
	"		memset(LL, 0, ONE_L<<(ssize-3));",
		"#endif",
		"#if defined(FULLSTACK)",
	"		memset((uchar *) S_Tab, 0, ",
	"		maxdepth*sizeof(struct H_el *));",
		"#endif",
	"		nstates=nlinks=truncs=truncs2=ngrabs = 0;",
	"		nlost=nShadow=hcmp = 0;",
	"		Fa=Fh=Zh=Zn = 0;",
	"		PUT=PROBE=ZAPS=Ccheck=Cholds = 0;",
	"		goto go_again;",
	"	}",
	"#endif",
	"}",
	"#ifdef HAS_PROVIDED",
	"int provided(int, uchar, int, Trans *);",
	"#endif",

	"#if NCORE>1",
	"#define GLOBAL_LOCK	(0)",
	"#ifndef CS_N",
	"#define CS_N		(32*NCORE)",
	"#endif",

	"#ifdef NGQ",	/* no global queue */
	"#define NR_QS		(NCORE)",
	"#define CS_NR		(CS_N+1)	/* 2^N + 1, nr critical sections */",
	"#define GQ_RD		GLOBAL_LOCK",	/* not really used in this mode */
	"#define GQ_WR		GLOBAL_LOCK",	/* but just in case... */
	"#define CS_ID		(1 + (int) (j1 & (CS_N-1)))	/* mask: 2^N - 1, zero reserved */",
	"#else",
	"#define NR_QS		(NCORE+1)",	/* add a global queue */
	"#define CS_NR		(CS_N+3)",	/* 2 extra locks for access to global q */
	"#define GQ_RD		(1)",		/* read access to global q */
	"#define GQ_WR		(2)",		/* write access to global q */
	"#define CS_ID		(3 + (int) (j1 & (CS_N-1)))	/* mask: 2^N - 1, zero reserved */",
	"#endif",
	"",
	"extern void enter_critical(int);",
	"extern void leave_critical(int);",
	"double cnt_shared = 0.;",
	"",
	"int",
	"cpu_printf(const char *fmt, ...)", /* only used with VERBOSE/CHECK/DEBUG */
	"{	va_list args;",
	"	enter_critical(GLOBAL_LOCK);	/* printing */",
	"	printf(\"cpu%%d: \", core_id);",
	"	fflush(stdout);",
	"	va_start(args, fmt);",
	"	vprintf(fmt, args);",
	"	va_end(args);",
	"	fflush(stdout);",
	"	leave_critical(GLOBAL_LOCK);",
	"	return 1;",
	"}",
	"#else",
	"int",
	"cpu_printf(const char *fmt, ...)",
	"{	va_list args;",
	"	va_start(args, fmt);",
	"	vprintf(fmt, args);",
	"	va_end(args);",
	"	return 1;",
	"}",
	"#endif",

#ifndef PRINTF
	"int",
	"Printf(const char *fmt, ...)",
	"{	/* Make sure the args to Printf",
	"	 * are always evaluated (e.g., they",
	"	 * could contain a run stmnt)",
	"	 * but do not generate the output",
	"	 * during verification runs",
	"	 * unless explicitly wanted",
	"	 * If this fails on your system",
	"	 * compile SPIN itself -DPRINTF",
	"	 * and this code is not generated",
	"	 */",
	"#ifdef HAS_CODE",
	"	if (readtrail)",
	"	{	va_list args;",
	"		va_start(args, fmt);",
	"		vprintf(fmt, args);",
	"		va_end(args);",
	"		return 1;",
	"	}",
	"#endif",
	"#ifdef PRINTF",
	"	va_list args;",
	"	va_start(args, fmt);",
	"	vprintf(fmt, args);",
	"	va_end(args);",
	"#endif",
	"	return 1;",
	"}",
#endif
	"extern void printm(int);",

	"#ifndef SC",
	"#define getframe(i)	&trail[i];",
	"#else",
	"static long HHH, DDD, hiwater;",
	"static long CNT1, CNT2;",
	"static int stackwrite;",
	"static int stackread;",
	"static Trail frameptr;",
	"Trail *",
	"getframe(int d)",
	"{",
	"	if (CNT1 == CNT2)",
	"		return &trail[d];",
	"",
	"	if (d >= (CNT1-CNT2)*DDD)",
	"		return &trail[d - (CNT1-CNT2)*DDD];",
	"",
	"	if (!stackread",
	"	&&  (stackread = open(stackfile, 0)) < 0)",
	"	{	printf(\"getframe: cannot open %%s\\n\", stackfile);",
	"		wrapup();",
	"	}",
	"	if (lseek(stackread, d* (off_t) sizeof(Trail), SEEK_SET) == -1",
	"	|| read(stackread, &frameptr, sizeof(Trail)) != sizeof(Trail))",
	"	{	printf(\"getframe: frame read error\\n\");",
	"		wrapup();",
	"	}",
	"	return &frameptr;",
	"}",
	"#endif",

	"#if !defined(SAFETY) && !defined(BITSTATE)",
	"#if !defined(FULLSTACK) || defined(MA)",
	"#define depth_of(x)	A_depth /* an estimate */",
	"#else",
	"int",
	"depth_of(struct H_el *s)",
	"{	Trail *t; int d;",
	"	for (d = 0; d <= A_depth; d++)",
	"	{	t = getframe(d);",
	"		if (s == t->ostate)",
	"			return d;",
	"	}",
	"	printf(\"pan: cannot happen, depth_of\\n\");",
	"	return depthfound;",
	"}",
	"#endif",
	"#endif",

	"#if NCORE>1",
	"extern void cleanup_shm(int);",
	"volatile unsigned int	*search_terminated;	/* to signal early termination */",
	/*
	 *	Meaning of bitflags in search_terminated:
	 *	  1	set by pan_exit
	 *	  2	set by wrapup
	 *	  4	set by uerror
	 *	  8	set by sudden_stop -- called after someone_crashed and [Uu]error
	 *	 16	set by cleanup_shm
	 *	 32	set by give_up	-- called on signal
	 *	 64	set by proxy_exit
	 *	128	set by proxy on write port failure
	 *	256	set by proxy on someone_crashed
	 *
	 *	Flags 8|32|128|256 indicate abnormal termination
	 *
	 *	The flags are checked in 4 functions in the code:
	 *		sudden_stop()
	 *		someone_crashed() (proxy and pan version)
	 *		mem_hand_off()
	 */
	"#endif",
	"void",
	"pan_exit(int val)",
	"{	void stop_timer(void);",
	"	if (signoff)",
	"	{	printf(\"--end of output--\\n\");",
	"	}",
	"#if NCORE>1",
	"	if (search_terminated != NULL)",
	"	{	*search_terminated |= 1;	/* pan_exit */",
	"	}",
		"#ifdef USE_DISK",
	"	{ void	dsk_stats(void);",
	"		dsk_stats();",
	"	}",
		"#endif",
	"	if (!state_tables && !readtrail)",
	"	{	cleanup_shm(1);",
	"	}",
	"#endif",
	"	stop_timer();",
	"	exit(val);",
	"}",

	"#ifdef HAS_CODE",
	"char *",
	"transmognify(char *s)",
	"{	char *v, *w;",
	"	static char buf[2][2048];",
	"	int i, toggle = 0;",

	"	if (!s || strlen(s) > 2047) return s;",
	"	memset(buf[0], 0, 2048);",
	"	memset(buf[1], 0, 2048);",
	"	strcpy(buf[toggle], s);",
	"	while ((v = strstr(buf[toggle], \"{c_code\")))",	/* assign v */
	"	{	*v = '\\0'; v++;",
	"		strcpy(buf[1-toggle], buf[toggle]);",
	"		for (w = v; *w != '}' && *w != '\\0'; w++) /* skip */;",
	"		if (*w != '}') return s;",
	"		*w = '\\0'; w++;",
	"		for (i = 0; code_lookup[i].c; i++)",
	"			if (strcmp(v, code_lookup[i].c) == 0",
	"			&&  strlen(v) == strlen(code_lookup[i].c))",
	"			{	if (strlen(buf[1-toggle])",
	"				 +  strlen(code_lookup[i].t)",
	"				 +  strlen(w) > 2047)",
	"					return s;",
	"				strcat(buf[1-toggle], code_lookup[i].t);",
	"				break;",
	"			}",
	"		strcat(buf[1-toggle], w);",
	"		toggle = 1 - toggle;",
	"	}",
	"	buf[toggle][2047] = '\\0';",
	"	return buf[toggle];",
	"}",
	"#else",
	"char * transmognify(char *s) { return s; }",
	"#endif",

	"#ifdef HAS_CODE",
	"void",
	"add_src_txt(int ot, int tt)",
	"{	Trans *t;",
	"	char *q;",
	"",
	"	for (t = trans[ot][tt]; t; t = t->nxt)",
	"	{	printf(\"\\t\\t\");",

	"		q = transmognify(t->tp);",
	"		for ( ; q && *q; q++)",
	"			if (*q == '\\n')",
	"				printf(\"\\\\n\");",
	"			else",
	"				putchar(*q);",
	"		printf(\"\\n\");",
	"	}",
	"}",
	"void",
	"wrap_trail(void)",
	"{	static int wrap_in_progress = 0;",
	"	int i; short II;",
	"	P0 *z;",
	"",
	"	if (wrap_in_progress++) return;",
	"",
	"	printf(\"spin: trail ends after %%ld steps\\n\", depth);",
	"	if (onlyproc >= 0)",
	"	{	if (onlyproc >= now._nr_pr) { pan_exit(0); }",
	"		II = onlyproc;",
	"		z = (P0 *)pptr(II);",
	"		printf(\"%%3ld:\tproc %%d (%%s) \",",
	"			depth, II, procname[z->_t]);",
	"		for (i = 0; src_all[i].src; i++)",
	"			if (src_all[i].tp == (int) z->_t)",
	"			{	printf(\" line %%3d\",",
	"					src_all[i].src[z->_p]);",
	"				break;",
	"			}",
	"		printf(\" (state %%2d)\", z->_p);",
	"		if (!stopstate[z->_t][z->_p])",
	"			printf(\" (invalid end state)\");",
	"		printf(\"\\n\");",
	"		add_src_txt(z->_t, z->_p);",
	"		pan_exit(0);",
	"	}",
	"	printf(\"#processes %%d:\\n\", now._nr_pr);",
	"	if (depth < 0) depth = 0;",
	"	for (II = 0; II < now._nr_pr; II++)",
	"	{	z = (P0 *)pptr(II);",
	"		printf(\"%%3ld:\tproc %%d (%%s) \",",
	"			depth, II, procname[z->_t]);",
	"		for (i = 0; src_all[i].src; i++)",
	"			if (src_all[i].tp == (int) z->_t)",
	"			{	printf(\" line %%3d\",",
	"					src_all[i].src[z->_p]);",
	"				break;",
	"			}",
	"		printf(\" (state %%2d)\", z->_p);",
	"		if (!stopstate[z->_t][z->_p])",
	"			printf(\" (invalid end state)\");",
	"		printf(\"\\n\");",
	"		add_src_txt(z->_t, z->_p);",
	"	}",
	"	c_globals();",
	"	for (II = 0; II < now._nr_pr; II++)",
	"	{	z = (P0 *)pptr(II);",
	"		c_locals(II, z->_t);",
	"	}",
	"#ifdef ON_EXIT",
	"	ON_EXIT;",
	"#endif",
	"	pan_exit(0);",
	"}",
	"FILE *",
	"findtrail(void)",
	"{	FILE *fd;",
	"	char fnm[512], *q;",
	"	char MyFile[512];",	/* avoid using a non-writable string */
	"	char MySuffix[16];",
	"	int  try_core;",
	"	int  candidate_files;",
	"talk:",
	"	try_core = 1;",
	"	candidate_files = 0;",
	"	tprefix = \"trail\";",
	"	strcpy(MyFile, TrailFile);",
	"	do { /* see if there's more than one possible trailfile */",
	"		if (whichtrail)",
	"		{	sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);",
	"			fd = fopen(fnm, \"r\");",
	"			if (fd != NULL)",
	"			{	candidate_files++;",
	"				if (verbose==100) printf(\"trail%%d: %%s\\n\", candidate_files, fnm);",
	"				fclose(fd);",
	"			}",
	"			if ((q = strchr(MyFile, \'.\')) != NULL)",
	"			{	*q = \'\\0\';",	/* e.g., strip .pml on original file */
	"				sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);",
	"				*q = \'.\';",
	"				fd = fopen(fnm, \"r\");",
	"				if (fd != NULL)",
	"				{	candidate_files++;",
	"					if (verbose==100) printf(\"trail%%d: %%s\\n\", candidate_files, fnm);",
	"					fclose(fd);",
	"			}	}",
	"		} else",
	"		{	sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
	"			fd = fopen(fnm, \"r\");",
	"			if (fd != NULL)",
	"			{	candidate_files++;",
	"				if (verbose==100) printf(\"trail%%d: %%s\\n\", candidate_files, fnm);",
	"				fclose(fd);",
	"			}",
	"			if ((q = strchr(MyFile, \'.\')) != NULL)",
	"			{	*q = \'\\0\';",	/* e.g., strip .pml on original file */
	"				sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
	"				*q = \'.\';",
	"				fd = fopen(fnm, \"r\");",
	"				if (fd != NULL)",
	"				{	candidate_files++;",
	"					if (verbose==100) printf(\"trail%%d: %%s\\n\", candidate_files, fnm);",
	"					fclose(fd);",
	"		}	}	}",
	"		tprefix = MySuffix;",
	"		sprintf(tprefix, \"cpu%%d_trail\", try_core++);",
	"	} while (try_core <= NCORE);",
	"",
	"	if (candidate_files != 1)",
	"	{	if (verbose != 100)",
	"		{	printf(\"error: there are %%d possible trail files:\\n\",",
	"				candidate_files);",
	"			verbose = 100;",
	"			goto talk;",
	"		} else",
	"		{	printf(\"pan: remove or rename all except the most recent of these files\\n\");",
	"			exit(1);",
	"	}	}",

	"	try_core = 1;",
	"	strcpy(MyFile, TrailFile); /* restore */",
	"	tprefix = \"trail\";",
	"try_again:",
	"	if (whichtrail)",
	"	{	sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);",
	"		fd = fopen(fnm, \"r\");",
	"		if (fd == NULL && (q = strchr(MyFile, \'.\')))",
	"		{	*q = \'\\0\';",	/* e.g., strip .pml on original file */
	"			sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);",
	"			*q = \'.\';",
	"			fd = fopen(fnm, \"r\");",
	"		}",
	"	} else",
	"	{	sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
	"		fd = fopen(fnm, \"r\");",
	"		if (fd == NULL && (q = strchr(MyFile, \'.\')))",
	"		{	*q = \'\\0\';",	/* e.g., strip .pml on original file */
	"			sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
	"			*q = \'.\';",
	"			fd = fopen(fnm, \"r\");",
	"	}	}",
	"	if (fd == NULL)",
	"	{	if (try_core < NCORE)",
	"		{	tprefix = MySuffix;",