pangen1.h

这是一个同样来自贝尔实验室的和UNIX有着渊源的操作系统, 其简洁的设计和实现易于我们学习和理解

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

/* Copyright (c) 1989-2003 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]            */

static char *Code2a[] = { /* the tail of procedure run() */
	"#if defined(VERI) && !defined(NOREDUCE) && !defined(NP)",
	"	if (!state_tables",
	"#ifdef HAS_CODE",
	"	&& !readtrail",
	"#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;",
	"		SS = (uchar *) emalloc(udmem);",
	"		bstore = bstore_mod;",
	"	} else",
#endif
	"	SS = (uchar *) emalloc(1L<<(ssize-3));",
	"#else",
	"	hinit();",
	"#endif",
	"#if defined(FULLSTACK) && defined(BITSTATE)",
	"	onstack_init();",
	"#endif",
	"#if defined(CNTRSTACK) && !defined(BFS)",
	"	LL = (uchar *) emalloc(1L<<(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",
	"	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, 1L<<(ssize-3));",
		"#if defined(CNTRSTACK)",
	"		memset(LL, 0, 1L<<(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",

#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",

	"void",
	"pan_exit(int val)",
	"{	if (signoff) printf(\"--end of output--\\n\");",
	"	exit(val);",
	"}",

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

	"	if (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++)",
	"			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 %%d steps\\n\", depth);",
	"	if (onlyproc >= 0)",
	"	{	if (onlyproc >= now._nr_pr) pan_exit(0);",
	"		II = onlyproc;",
	"		z = (P0 *)pptr(II);",
	"		printf(\"%%3d:\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(\"%%3d:\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;",
	"	if (whichtrail)",
	"	{	sprintf(fnm, \"%%s%%d.%%s\", TrailFile, whichtrail, tprefix);",
	"		fd = fopen(fnm, \"r\");",
	"		if (fd == NULL && (q = strchr(TrailFile, \'.\')))",
	"		{	*q = \'\\0\';",	/* e.g., strip .pml on original file */
	"			sprintf(fnm, \"%%s%%d.%%s\", TrailFile, whichtrail, tprefix);",
	"			*q = \'.\';",
	"			fd = fopen(fnm, \"r\");",
	"			if (fd == NULL)",
	"			{	printf(\"pan: cannot find %%s%%d.%%s or %%s\\n\", ",
	"					TrailFile, whichtrail, tprefix, fnm);",
	"				pan_exit(1);",
	"		}	}",
	"	} else",
	"	{	sprintf(fnm, \"%%s.%%s\", TrailFile, tprefix);",
	"		fd = fopen(fnm, \"r\");",
	"		if (fd == NULL && (q = strchr(TrailFile, \'.\')))",
	"		{	*q = \'\\0\';",	/* e.g., strip .pml on original file */
	"			sprintf(fnm, \"%%s.%%s\", TrailFile, tprefix);",
	"			*q = \'.\';",
	"			fd = fopen(fnm, \"r\");",
	"			if (fd == NULL)",
	"			{	printf(\"pan: cannot find %%s.%%s or %%s\\n\", ",
	"					TrailFile, tprefix, fnm);",
	"				pan_exit(1);",
	"	}	}	}",
	"	if (fd == NULL)",
	"	{	printf(\"pan: cannot find trailfile %%s\\n\", fnm);",
	"		pan_exit(1);",
	"	}",
	"	return fd;",
	"}",
	"",
	"uchar do_transit(Trans *, short);",
	"",
	"void",
	"getrail(void)",
	"{	FILE *fd;",
	"	char *q;",
	"	int i, t_id, lastnever=-1; short II;",
	"	Trans *t;",
	"	P0 *z;",
	"",
	"	fd = findtrail();	/* exits if unsuccessful */",
	"	while (fscanf(fd, \"%%d:%%d:%%d\\n\", &depth, &i, &t_id) == 3)",
	"	{	if (depth == -1)",
	"			printf(\"<<<<<START OF CYCLE>>>>>\\n\");",
	"		if (depth < 0)",
	"			continue;",
	"		II = i;",
	"",
	"		z = (P0 *)pptr(II);",
	"		for (t = trans[z->_t][z->_p]; t; t = t->nxt)",
	"			if (t->t_id == t_id)",
	"				break;",
	"		if (!t)",
	"		{	for (i = 0; i < NrStates[z->_t]; i++)",
	"			{	t = trans[z->_t][i];",
	"				if (t && t->t_id == t_id)",
	"				{	printf(\"	Recovered at state %%d\\n\", i);",
	"					z->_p = i;",
	"					goto recovered;",
	"			}	}",
	"			printf(\"pan: Error, proc %%d type %%d state %%d: \",",
	"				II, z->_t, z->_p);",
	"			printf(\"transition %%d not found\\n\", t_id);",
	"			for (t = trans[z->_t][z->_p]; t; t = t->nxt)",
	"				printf(\"	t_id %%d -- case %%d, [%%s]\\n\",",
	"					t->t_id, t->forw, t->tp);",
	"			break; /* pan_exit(1); */",
	"		}",
	"recovered:",
	"		q = transmognify(t->tp);",
	"		if (gui) simvals[0] = \'\\0\';",

	"		this = pptr(II);",
	"		trpt->tau |= 1;",	/* timeout always possible */
	"		if (!do_transit(t, II))",
	"		{	if (onlyproc >= 0 && II != onlyproc)",
	"				goto moveon;",
	"			printf(\"pan: error, next transition UNEXECUTABLE on replay\\n\");",
	"			printf(\"     most likely causes: missing c_track statements\\n\");",
	"			printf(\"       or illegal side-effects in c_expr statements\\n\");",
	"		}",

	"		if (onlyproc >= 0 && II != onlyproc)",
	"			goto moveon;",

	"		if (verbose)",
	"		{	printf(\"depth: %%3d proc: %%3d trans: %%3d (%%d procs)  \",",
	"				depth, II, t_id, now._nr_pr);",
	"			printf(\"forw=%%3d [%%s]\\n\", t->forw, q);",
	"",
	"			c_globals();",
	"			for (i = 0; i < now._nr_pr; i++)",
	"			{	c_locals(i, ((P0 *)pptr(i))->_t);",
	"			}",
	"		} else",
	"		if (strcmp(procname[z->_t], \":never:\") == 0)",
	"		{	if (lastnever != (int) z->_p)",
	"			{	for (i = 0; src_all[i].src; i++)",
	"					if (src_all[i].tp == (int) z->_t)",
	"					{	printf(\"MSC: ~G %%d\\n\",",
	"							src_all[i].src[z->_p]);",
	"						break;",
	"					}",
	"				if (!src_all[i].src)",
	"					printf(\"MSC: ~R %%d\\n\", z->_p);",
	"			}",
	"			lastnever = z->_p;",
	"			goto sameas;",
	"		} else",
	"		if (strcmp(procname[z->_t], \":np_:\") != 0)",
	"		{",
	"sameas:		if (no_rck) goto moveon;",
	"			if (coltrace)",
	"			{	printf(\"%%d: \", depth);",
	"				for (i = 0; i < II; i++)",
	"					printf(\"\\t\\t\");",
	"				printf(\"%%s(%%d):\", procname[z->_t], II);",
	"				printf(\"[%%s]\\n\", q);",
	"			} else",
	"			{	if (strlen(simvals) > 0) {",
	"				printf(\"%%3d:	proc %%2d (%%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 \\\"pan_in\\\" \",",
	"							src_all[i].src[z->_p]);",
	"						break;",
	"					}",
	"				printf(\"(state %%d)\t[values: %%s]\\n\", z->_p, simvals);",
	"				}",
	"				printf(\"%%3d:	proc %%2d (%%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 \\\"pan_in\\\" \",",
	"							src_all[i].src[z->_p]);",
	"						break;",
	"					}",
	"				printf(\"(state %%d)\t[%%s]\\n\", z->_p, q);",
	"				printf(\"\\n\");",
	"		}	}",
	"moveon:	z->_p = t->st;",
	"	}",
	"	wrap_trail();",
	"}",
	"#endif",
	"int",
	"f_pid(int pt)",
	"{	int i;",
	"	P0 *z;",
	"	for (i = 0; i < now._nr_pr; i++)",
	"	{	z = (P0 *)pptr(i);",
	"		if (z->_t == (unsigned) pt)",
	"			return BASE+z->_pid;",
	"	}",
	"	return -1;",
	"}",
	"#ifdef VERI",
	"void check_claim(int);",
	"#endif",
	"",
	"#ifdef BITSTATE",
#ifndef POWOW
	"int",
	"bstore_mod(char *v, int n)	/* hasharray size not a power of two */",
	"{	unsigned long x, y;",
	"	unsigned int i = 1;",
	"",
	"	d_hash((uchar *) v, n); /* sets j3, j4, K1, K2 */",
	"	x = K2; y = j3;",
	"	for (;;)",
	"	{	if (!(SS[x%%udmem]&(1<<y))) break;",	/* take the hit in speed */
	"		if (i == hfns) {",
				"#ifdef DEBUG",
	"			printf(\"Old bitstate\\n\");",
				"#endif",
	"			return 1;",
	"		}",
	"		x = (x + K1 + i);",	/* no mask, using mod */
	"		y = (y + j4) & 7;",
	"		i++;",
	"	}",
		"#ifdef RANDSTOR",
	"	if (rand()%%100 > RANDSTOR) return 0;",
		"#endif",
	"	for (;;)",
	"	{	SS[x%%udmem] |= (1<<y);",
	"		if (i == hfns) break;",	/* done */
	"		x = (x + K1 + i);",	/* no mask */
	"		y = (y + j4) & 7;",
	"		i++;",
	"	}",
		"#ifdef DEBUG",
	"	printf(\"New bitstate\\n\");",
		"#endif",
	"	return 0;",
	"}",
#endif
	"int",
	"bstore_reg(char *v, int n)	/* extended hashing, Peter Dillinger, 2004 */",
	"{	unsigned long x, y;",
	"	unsigned int i = 1;",