/***** spin: pangen5.h *****/ /* Copyright (c) 1997-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: bugs@spinroot.com            */ static char *Xpt[] = {	"#if defined(MA) && (defined(W_XPT) || defined(R_XPT))",	"static Vertex	**temptree;",	"static char	wbuf[4096];",	"static int	WCNT = 4096, wcnt=0;",	"static uchar	stacker[MA+1];",	"static ulong	stackcnt = 0;",	"extern double	nstates, nlinks, truncs, truncs2;",	"",	"static void",	"xwrite(int fd, char *b, int n)",	"{",	"	if (wcnt+n >= 4096)",	"	{	write(fd, wbuf, wcnt);",	"		wcnt = 0;",	"	}",	"	memcpy(&wbuf[wcnt], b, n);",	"	wcnt += n;",	"}",	"",	"static void",	"wclose(fd)",	"{",	"	if (wcnt > 0)",	"		write(fd, wbuf, wcnt);",	"	wcnt = 0;",	"	close(fd);",	"}",	"",	"static void",	"w_vertex(int fd, Vertex *v)",	"{	char t[3]; int i; Edge *e;",	"",	"	xwrite(fd, (char *) &v,  sizeof(Vertex *));",	"	t[0] = 0;",	"	for (i = 0; i < 2; i++)",	"		if (v->dst[i])",	"		{	t[1] = v->from[i], t[2] = v->to[i];",	"			xwrite(fd, t, 3);",	"			xwrite(fd, (char *) &(v->dst[i]), sizeof(Vertex *));",	"		}",	"	for (e = v->Succ; e; e = e->Nxt)",	"	{	t[1] = e->From, t[2] = e->To;",	"		xwrite(fd, t, 3);",	"		xwrite(fd, (char *) &(e->Dst), sizeof(Vertex *));",	"",	"		if (e->s)",	"		{	t[1] = t[2] = e->S;",	"			xwrite(fd, t, 3);",	"			xwrite(fd, (char *) &(e->Dst), sizeof(Vertex *));",	"	}	}",	"}",	"",	"static void",	"w_layer(int fd, Vertex *v)",	"{	uchar c=1;",	"",	"	if (!v) return;",	"	xwrite(fd, (char *) &c, 1);",	"	w_vertex(fd, v);",	"	w_layer(fd, v->lnk);",	"	w_layer(fd, v->left);",	"	w_layer(fd, v->right);",	"}",	"",	"void",	"w_xpoint(void)",	"{	int fd; char nm[64];",	"	int i, j;  uchar c;",	"	static uchar xwarned = 0;",	"",	"	sprintf(nm, \"%%s.xpt\", PanSource);",	"	if ((fd = creat(nm, 0666)) <= 0)",	"	if (!xwarned)",	"	{	xwarned = 1;",	"		printf(\"cannot creat checkpoint file\\n\");",	"		return;",	"	}",	"	xwrite(fd, (char *) &nstates, sizeof(double));",	"	xwrite(fd, (char *) &truncs, sizeof(double));",	"	xwrite(fd, (char *) &truncs2, sizeof(double));",	"	xwrite(fd, (char *) &nlinks, sizeof(double));",	"	xwrite(fd, (char *) &dfa_depth, sizeof(int));",	"	xwrite(fd, (char *) &R,  sizeof(Vertex *));",	"	xwrite(fd, (char *) &F,  sizeof(Vertex *));",	"	xwrite(fd, (char *) &NF, sizeof(Vertex *));",	"",	"	for (j = 0; j < TWIDTH; j++)",	"	for (i = 0; i < dfa_depth+1; i++)",	"	{	w_layer(fd, layers[i*TWIDTH+j]);",	"		c = 2; xwrite(fd, (char *) &c, 1);",	"	}",	"	wclose(fd);",	"}",	"",	"static void",	"xread(int fd, char *b, int n)",	"{	int m = wcnt; int delta = 0;",	"	if (m < n)",	"	{	if (m > 0) memcpy(b, &wbuf[WCNT-m], m);",	"		delta = m;",	"		WCNT = wcnt = read(fd, wbuf, 4096);",	"		if (wcnt < n-m)",	"			Uerror(\"xread failed -- insufficient data\");",	"		n -= m;",	"	}",	"	memcpy(&b[delta], &wbuf[WCNT-wcnt], n);",	"	wcnt -= n;",	"}",	"",	"static void",	"x_cleanup(Vertex *c)",	"{	Edge *e;	/* remove the tree and edges from c */",	"	if (!c) return;",	"	for (e = c->Succ; e; e = e->Nxt)",	"		x_cleanup(e->Dst);",	"	recyc_vertex(c);",	"}",	"",	"static void",	"x_remove(void)",	"{	Vertex *tmp; int i, s;",	"	int r, j;",	"	/* double-check: */",	"	stacker[dfa_depth-1] = 0; r = dfa_store(stacker);",	"	stacker[dfa_depth-1] = 4; j = dfa_member(dfa_depth-1);",	"	if (r != 1 || j != 0)",	"	{	printf(\"%%d: \", stackcnt);",	"		for (i = 0; i < dfa_depth; i++)",	"			printf(\"%%d,\", stacker[i]);",	"		printf(\" -- not a stackstate <o:%%d,4:%%d>\\n\", r, j);",	"		return;",	"	}",	"	stacker[dfa_depth-1] = 1;",	"	s = dfa_member(dfa_depth-1);",	"",	"	{ tmp = F; F = NF; NF = tmp; }	/* complement */",	"		if (s) dfa_store(stacker);",	"		stacker[dfa_depth-1] = 0;",	"		dfa_store(stacker);",	"		stackcnt++;",	"	{ tmp = F; F = NF; NF = tmp; }",	"}",	"",	"static void",	"x_rm_stack(Vertex *t, int k)",	"{	int j; Edge *e;",	"",	"	if (k == 0)",	"	{	x_remove();",	"		return;",	"	}",	"	if (t)",	"	for (e = t->Succ; e; e = e->Nxt)",	"	{	for (j = e->From; j <= (int) e->To; j++)",	"		{	stacker[k] = (uchar) j;",	"			x_rm_stack(e->Dst, k-1);",	"		}",	"		if (e->s)",	"		{	stacker[k] = e->S;",	"			x_rm_stack(e->Dst, k-1);",	"	}	}",	"}",	"",	"static Vertex *",	"insert_withkey(Vertex *v, int L)",	"{	Vertex *new, *t = temptree[L];",	"",	"	if (!t) { temptree[L] = v; return v; }",	"	t = splay(v->key, t);",	"	if (v->key < t->key)",	"	{	new = v;",	"		new->left = t->left;",	"		new->right = t;",	"		t->left = (Vertex *) 0;",	"	} else if (v->key > t->key)",	"	{	new = v;",	"		new->right = t->right;",	"		new->left = t;",	"		t->right = (Vertex *) 0;",	"	} else",	"	{	if (t != R && t != F && t != NF)",	"			Uerror(\"double insert, bad checkpoint data\");",	"		else",	"		{	recyc_vertex(v);",	"			new = t;",	"	}	}",	"	temptree[L] = new;",	"",	"	return new;",	"}",	"",	"static Vertex *",	"find_withkey(Vertex *v, int L)",	"{	Vertex *t = temptree[L];",	"	if (t)",	"	{	temptree[L] = t = splay((ulong) v, t);",	"		if (t->key == (ulong) v)",	"			return t;",	"	}",	"	Uerror(\"not found error, bad checkpoint data\");",	"	return (Vertex *) 0;",	"}",	"",	"void",	"r_layer(int fd, int n)",	"{	Vertex *v;",	"	Edge *e;",	"	char c, t[2];",	"",	"	for (;;)",	"	{	xread(fd, &c, 1);",	"		if (c == 2) break;",	"		if (c == 1)",	"		{	v = new_vertex();",	"			xread(fd, (char *) &(v->key), sizeof(Vertex *));",	"			v = insert_withkey(v, n);",	"		} else	/* c == 0 */",	"		{	e = new_edge((Vertex *) 0);",	"			xread(fd, t, 2);",	"			e->From = t[0];",	"			e->To = t[1];",	"			xread(fd, (char *) &(e->Dst), sizeof(Vertex *));",	"			insert_edge(v, e);",	"	}	}",	"}",	"",	"static void",	"v_fix(Vertex *t, int nr)",	"{	int i; Edge *e;",	"",	"	if (!t) return;",	"",	"	for (i = 0; i < 2; i++)",	"	if (t->dst[i])",	"		t->dst[i] = find_withkey(t->dst[i], nr);",	"",	"	for (e = t->Succ; e; e = e->Nxt)",	"		e->Dst = find_withkey(e->Dst, nr);",	"		",	"	v_fix(t->left, nr);",	"	v_fix(t->right, nr);",	"}",	"",	"static void",	"v_insert(Vertex *t, int nr)",	"{	Edge *e; int i;",	"",	"	if (!t) return;",	"	v_insert(t->left, nr);",	"	v_insert(t->right, nr);",	"",	"	/* remove only leafs from temptree */",	"	t->left = t->right = t->lnk = (Vertex *) 0;",	"	insert_it(t, nr);	/* into layers */",	"	for (i = 0; i < 2; i++)",	"		if (t->dst[i])",	"			t->dst[i]->num += (t->to[i] - t->from[i] + 1);",	"	for (e = t->Succ; e; e = e->Nxt)",	"		e->Dst->num += (e->To - e->From + 1 + e->s);",	"}",	"",	"static void",	"x_fixup(void)",	"{	int i;",	"",	"	for (i = 0; i < dfa_depth; i++)",	"		v_fix(temptree[i], (i+1));",	"",	"	for (i = dfa_depth; i >= 0; i--)",	"		v_insert(temptree[i], i);",	"}",	"",	"static Vertex *",	"x_tail(Vertex *t, ulong want)",	"{	int i, yes, no; Edge *e; Vertex *v = (Vertex *) 0;",	"",	"	if (!t) return v;",	"",	"	yes = no = 0;",	"	for (i = 0; i < 2; i++)",	"		if ((ulong) t->dst[i] == want)",	"		{	/* was t->from[i] <= 0 && t->to[i] >= 0 */",	"			/* but from and to are uchar */",	"			if (t->from[i] == 0)",	"				yes = 1;",	"			else",	"			if (t->from[i] <= 4 && t->to[i] >= 4)",	"				no = 1;",	"		}",	"",	"	for (e = t->Succ; e; e = e->Nxt)",	"		if ((ulong) e->Dst == want)",	"		{	/* was INRANGE(e,0) but From and To are uchar */",	"			if ((e->From == 0) || (e->s==1 && e->S==0))",	"				yes = 1;",	"			else if (INRANGE(e, 4))",	"				no = 1;",	"		}",	"	if (yes && !no) return t;",	"	v = x_tail(t->left, want);  if (v) return v;",	"	v = x_tail(t->right, want); if (v) return v;",	"	return (Vertex *) 0;",	"}",	"",	"static void",	"x_anytail(Vertex *t, Vertex *c, int nr)",	"{	int i; Edge *e, *f; Vertex *v;",	"",	"	if (!t) return;",	"",	"	for (i = 0; i < 2; i++)",	"		if ((ulong) t->dst[i] == c->key)",	"		{	v = new_vertex(); v->key = t->key;",	"			f = new_edge(v);",	"			f->From = t->from[i];",	"			f->To = t->to[i];",	"			f->Nxt = c->Succ;",	"			c->Succ = f;",	"			if (nr > 0)",	"			x_anytail(temptree[nr-1], v, nr-1);",	"		}",	"",	"	for (e = t->Succ; e; e = e->Nxt)",	"		if ((ulong) e->Dst == c->key)",	"		{	v = new_vertex(); v->key = t->key;",	"			f = new_edge(v);",	"			f->From = e->From;",	"			f->To = e->To;",	"			f->s = e->s;",	"			f->S = e->S;",	"			f->Nxt = c->Succ;",	"			c->Succ = f;",	"			x_anytail(temptree[nr-1], v, nr-1);",	"		}",	"",	"	x_anytail(t->left, c, nr);",	"	x_anytail(t->right, c, nr);",	"}",	"",	"static Vertex *",	"x_cpy_rev(void)",	"{	Vertex *c, *v;	/* find 0 and !4 predecessor of F */",	"",	"	v = x_tail(temptree[dfa_depth-1], F->key);",	"	if (!v) return (Vertex *) 0;",	"",	"	c = new_vertex(); c->key = v->key;",	"",	"	/* every node on dfa_depth-2 that has v->key as succ */",	"	/* make copy and let c point to these (reversing ptrs) */",	"",	"	x_anytail(temptree[dfa_depth-2], c, dfa_depth-2);",	" ",	"	return c;",	"}",	"",	"void",	"r_xpoint(void)",	"{	int fd; char nm[64]; Vertex *d;",	"	int i, j;",	"",	"	wcnt = 0;",	"	sprintf(nm, \"%%s.xpt\", PanSource);",	"	if ((fd = open(nm, 0)) < 0)	/* O_RDONLY */",	"		Uerror(\"cannot open checkpoint file\");",	"",	"	xread(fd, (char *) &nstates,   sizeof(double));",	"	xread(fd, (char *) &truncs,    sizeof(double));",	"	xread(fd, (char *) &truncs2,   sizeof(double));",	"	xread(fd, (char *) &nlinks,    sizeof(double));",	"	xread(fd, (char *) &dfa_depth, sizeof(int));",	"",	"	if (dfa_depth != MA+a_cycles)",	"		Uerror(\"bad dfa_depth in checkpoint file\");",	"",	"	path	  = (Vertex **) emalloc((dfa_depth+1)*sizeof(Vertex *));",	"	layers	  = (Vertex **) emalloc(TWIDTH*(dfa_depth+1)*sizeof(Vertex *));",	"	temptree  = (Vertex **) emalloc((dfa_depth+2)*sizeof(Vertex *));",	"	lastword  = (uchar *)   emalloc((dfa_depth+1)*sizeof(uchar));",	"	lastword[dfa_depth] = lastword[0] = 255; ",	"",	"	path[0] = R = new_vertex();",	"	xread(fd, (char *) &R->key, sizeof(Vertex *));",	"	R = insert_withkey(R, 0);",	"",	"	F = new_vertex();",	"	xread(fd, (char *) &F->key, sizeof(Vertex *));",	"	F = insert_withkey(F, dfa_depth);",	"",	"	NF = new_vertex();",	"	xread(fd, (char *) &NF->key, sizeof(Vertex *));",	"	NF = insert_withkey(NF, dfa_depth);",	"",	"	for (j = 0; j < TWIDTH; j++)",	"	for (i = 0; i < dfa_depth+1; i++)",	"		r_layer(fd, i);",	"",	"	if (wcnt != 0) Uerror(\"bad count in checkpoint file\");",	"",	"	d = x_cpy_rev();",	"	x_fixup();",	"	stacker[dfa_depth-1] = 0;",	"	x_rm_stack(d, dfa_depth-2);",	"	x_cleanup(d);",	"	close(fd);",	"",	"	printf(\"pan: removed %%d stackstates\\n\", stackcnt);",	"	nstates -= (double) stackcnt;",	"}",	"#endif",	0,};