pangen1.h

来自「这是一个同样来自贝尔实验室的和UNIX有着渊源的操作系统, 其简洁的设计和实现易」· C头文件 代码 · 共 2,500 行 · 第 1/5 页

	"				printf(\"%%3d: proc %%d PreSelected (tau=%%d)\\n\", ",
	"					depth, II, trpt->tau);",
		"#endif",
	"				goto MainLoop;",
	"		}	}",
	"		trpt->tau &= ~32;",	/* not preselected */
	"#endif",
/* PO */
	"Repeat:",
	"		if (trpt->tau&8)		/* atomic */",
	"		{	From = To = (short ) trpt->pr;",
	"			nlinks++;",
	"		} else",
	"		{	From = now._nr_pr-1;",
	"			To = BASE;",
	"		}",
	"MainLoop:",
	"		_n = _m = 0;",
	"		for (II = From; II >= To; II -= 1)",
	"		{",
	"			this = (((uchar *)&now)+proc_offset[II]);",
	"			tt = (int) ((P0 *)this)->_p;",
	"			ot = (uchar) ((P0 *)this)->_t;",
	"#if SYNC",
	"			/* no rendezvous with same proc */",
	"			if (boq != -1 && trpt->pr == II) continue;",
	"#endif",
	"			ntrpt->pr = (uchar) II;",
	"			ntrpt->st = tt;	",
	"			trpt->o_pm &= ~1;		/* no move yet */",
	"#ifdef EVENT_TRACE",
	"			trpt->o_event = now._event;",
	"#endif",
	"#ifdef HAS_PROVIDED",
	"			if (!provided(II, ot, tt, t)) continue;",
	"#endif",
	"#ifdef HAS_UNLESS",
	"			E_state = 0;",
	"#endif",
	"			for (t = trans[ot][tt]; t; t = t->nxt)",
	"			{",
	"#ifdef HAS_UNLESS",
	"				if (E_state > 0",
	"				&&  E_state != t->e_trans)",
	"					break;",
	"#endif",
	"				ntrpt->o_t = t;",
	"",
	"				oboq = boq;",
	"",
	"				if (!(_m = do_transit(t, II)))",
	"					continue;",
	"",
	"				trpt->o_pm |= 1;	/* we moved */",
	"				(trpt+1)->o_m = _m;	/* for unsend */",
		"#ifdef PEG",
	"				peg[t->forw]++;",
		"#endif",
	"#ifdef CHECK",
	"				printf(\"%%3d: proc %%d exec %%d, \",",
	"					depth, II, t->forw);",
	"				printf(\"%%d to %%d, %%s %%s %%s\",",
	"					tt, t->st, t->tp,",
	"					(t->atom&2)?\"atomic\":\"\",",
	"					(boq != -1)?\"rendez-vous\":\"\");",
		"#ifdef HAS_UNLESS",
	"				if (t->e_trans)",
	"					printf(\" (escapes to state %%d)\", t->st);",
		"#endif",
	"				printf(\" %%saccepting [tau=%%d]\\n\",",
	"					(trpt->o_pm&2)?\"\":\"non-\", trpt->tau);",
	"#endif",
	"#ifdef HAS_UNLESS",
	"				E_state = t->e_trans;",
		"#if SYNC>0",
	"				if (t->e_trans > 0 && (boq != -1 /* || oboq != -1 */))",
	"				{ fprintf(efd, \"error:\tthe use of rendezvous stmnt in the escape clause\\n\");",
	"				  fprintf(efd, \"\tof an unless stmnt is not compatible with -DBFS\\n\");",
	"				  pan_exit(1);",
	"				}",
		"#endif",
	"#endif",
	"				if (t->st > 0) ((P0 *)this)->_p = t->st;",
	"",
	"	/* ptr to pred: */	ntrpt->ostate = (struct H_el *) otrpt;",
	"				ntrpt->st = tt;",
	"				if (boq == -1 && (t->atom&2))	/* atomic */",
	"					ntrpt->tau = 8;	/* record for next move */",
	"				else",
	"					ntrpt->tau = 0;",
	"",
	"				store_state(ntrpt, (boq != -1 || (t->atom&2)), oboq);",
	"#ifdef EVENT_TRACE",
	"				now._event = trpt->o_event;",
	"#endif",
	"",
	"				/* undo move and continue */",
	"				trpt++;	/* this is where ovals and ipt are set */",
	"				do_reverse(t, II, _m);	/* restore now. */",
	"				trpt--;",
	"#ifdef CHECK",
	"				printf(\"%%3d: proc %%d \", depth, II);",
	"				printf(\"reverses %%d, %%d to %%d,\",",
	"					t->forw, tt, t->st);",
	"				printf(\" %%s [abit=%%d,adepth=%%d,\",",
	"					t->tp, now._a_t, A_depth);",
	"				printf(\"tau=%%d,%%d]\\n\",",
	"					trpt->tau, (trpt-1)->tau);",
	"#endif",
	"				reached[ot][t->st] = 1;",
	"				reached[ot][tt] = 1;",
	"",
	"				((P0 *)this)->_p = tt;",
	"				_n |= _m;",
	"		}	}",
/* PO */
	"#ifndef NOREDUCE",
	"		/* preselected - no succ definitely outside stack */",
	"		if ((trpt->tau&32) && !(trpt->tau&64))",
	"		{	From = now._nr_pr-1; To = BASE;",
	"#ifdef DEBUG",
	"			printf(\"%%3d: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
	"				depth, II+1, (int) _n, trpt->tau);",
	"#endif",
	"			_n = 0; trpt->tau &= ~32;",
	"			if (II >= BASE)",
	"				goto Pickup;",
	"			goto MainLoop;",
	"		}",
	"		trpt->tau &= ~(32|64);",
	"#endif",
/* PO */
	"		if (_n != 0)",
	"			continue;",
	"#ifdef DEBUG",
	"		printf(\"%%3d: no move [II=%%d, tau=%%d, boq=%%d, _nr_pr=%%d]\\n\",",
	"			depth, II, trpt->tau, boq, now._nr_pr);",
	"#endif",
	"		if (boq != -1)",
	"		{	failedrv++;",
	"			x = (Trail *) trpt->ostate; /* pre-rv state */",
	"			if (!x) continue; /* root state */",
	"			if ((x->tau&8) || (x->tau&32)) /* break atomic or preselect at parent */",
	"			{	x->o_pm |= 8; /* mark failure */",
	"				this = (((uchar *)&now)+proc_offset[otrpt->pr]);",
	"#ifdef VERBOSE",
	"				printf(\"\\treset state of %%d from %%d to %%d\\n\",",
	"					otrpt->pr, ((P0 *)this)->_p, otrpt->st);",
	"#endif",
	"				((P0 *)this)->_p = otrpt->st;",
	"				unsend(boq);	/* retract rv offer */",
	"				boq = -1;",

	"				push_bfs(x, x->o_tt);",
	"#ifdef VERBOSE",
	"				printf(\"failed rv, repush with %%d\\n\", x->o_pm);",
	"#endif",
	"			}",
	"#ifdef VERBOSE",
	"			else printf(\"failed rv, tau at parent: %%d\\n\", x->tau);",
	"#endif",
	"		} else if (now._nr_pr > 0)",
	"		{",
	"			if ((trpt->tau&8))		/* atomic */",
	"			{	trpt->tau &= ~(1|8);	/* 1=timeout, 8=atomic */",
	"#ifdef DEBUG",
	"				printf(\"%%3d: atomic step proc %%d blocks\\n\",",
	"					depth, II+1);",
	"#endif",
	"				goto Repeat;",
	"			}",
	"",
	"			if (!(trpt->tau&1)) /* didn't try timeout yet */",
	"			{	trpt->tau |=  1;",
	"#ifdef DEBUG",
	"				printf(\"%%d: timeout\\n\", depth);",
	"#endif",
	"				goto MainLoop;",
	"			}",
	"#ifndef VERI",
	"			if (!noends && !a_cycles && !endstate())",
	"				uerror(\"invalid end state\");",
	"#endif",
	"	}	}",
	"}",
	"",
	"void",
	"putter(Trail *trpt, int fd)",
	"{	long j;",
	"",
	"	if (!trpt) return;",
	"",
	"	if (trpt != (Trail *) trpt->ostate)",
	"		putter((Trail *) trpt->ostate, fd);",
	"",
	"	if (trpt->o_t)",
	"	{	sprintf(snap, \"%%d:%%d:%%d\\n\",",
	"			trcnt++, trpt->pr, trpt->o_t->t_id);",
	"		j = strlen(snap);",
	"		if (write(fd, snap, j) != j)",
	"		{       printf(\"pan: error writing %%s\\n\", fnm);",
	"			exit(1);",
	"	}	}",
	"}",
	"",
	"void",
	"nuerror(char *str)",
	"{	int fd = make_trail();",
	"	if (fd < 0) return;",
	"#ifdef VERI",
	"	sprintf(snap, \"-2:%%d:-2\\n\", VERI);",
	"	write(fd, snap, strlen(snap));",
	"#endif",
	"#ifdef MERGED",
	"	sprintf(snap, \"-4:-4:-4\\n\");",
	"	write(fd, snap, strlen(snap));",
	"#endif",
	"	trcnt = 1;",
	"	putter(trpt, fd);",
	"	close(fd);",
	"	if (errors >= upto && upto != 0)",
	"		wrapup();",
	"}",
	"#endif",	/* BFS */
	0,
};

static char *Code2c[] = {
	"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",

	"#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",
	"#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",
	"	new_state();	/* start 1st DFS */",
	"#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 = start_event; /* only 1st try will count */",
	"#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",
	"snapshot(void)",
	"{	static long sdone = (long) 0;",
	"	long ndone = (unsigned long) nstates/1000000;",
	"	if (ndone == sdone) return;",
	"	sdone = ndone;",
	"	printf(\"Depth= %%7d States= %%7g \", mreached, nstates);",
	"	printf(\"Transitions= %%7g \", nstates+truncs);",
	"#ifdef MA",
	"	printf(\"Nodes= %%7d \", nr_states);",
	"#endif",
	"	printf(\"Memory= %%-6.3f\\n\", memcnt/1000000.);",
	"	fflush(stdout);",
	"}",

	"#ifdef SC",
	"void",
	"stack2disk(void)",
	"{",
	"	if (!stackwrite",
	"	&&  (stackwrite = creat(stackfile, 0666)) < 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);",
	"}",