/* find end of list */	for (p1 = a; p1->next; p1 = p1->next)		;	p1->next = b;	return a;}static voidfixinit(Node *orig){	Graph	*p1, *g;	Symbol	*q1, *q2 = ZS;	ng(tl_lookup("init"), ZS, ZN, ZN, ZN);	p1 = pop_stack();	p1->nxt = Nodes_Set;	p1->Other = p1->Old = orig;	Nodes_Set = p1;	for (g = Nodes_Set; g; g = g->nxt)	{	for (q1 = g->incoming; q1; q1 = q2)		{	q2 = q1->next;			Addout(g->name->name, q1->name);			tfree((void *) q1);		}		g->incoming = ZS;	}}static Node *flatten(Node *p){	Node *q, *r, *z = ZN;	for (q = p; q; q = q->nxt)	{	r = dupnode(q);		if (z)			z = tl_nn(AND, r, z);		else			z = r;	}	if (!z) return z;	z = rewrite(z);	return z;}static Node *Duplicate(Node *n){	Node *n1, *n2, *lst = ZN, *d = ZN;	for (n1 = n; n1; n1 = n1->nxt)	{	n2 = dupnode(n1);		if (lst)		{	lst->nxt = n2;			lst = n2;		} else			d = lst = n2;	}	return d;}static voidng(Symbol *s, Symbol *in, Node *isnew, Node *isold, Node *next){	Graph *g = (Graph *) tl_emalloc(sizeof(Graph));	if (s)     g->name = s;	else       g->name = tl_lookup(newname());	if (in)    g->incoming = dupSlist(in);	if (isnew) g->New  = flatten(isnew);	if (isold) g->Old  = Duplicate(isold);	if (next)  g->Next = flatten(next);	push_stack(g);}static voidsdump(Node *n){	switch (n->ntyp) {	case PREDICATE:	strcat(dumpbuf, n->sym->name);			break;	case U_OPER:	strcat(dumpbuf, "U");			goto common2;	case V_OPER:	strcat(dumpbuf, "V");			goto common2;	case OR:	strcat(dumpbuf, "|");			goto common2;	case AND:	strcat(dumpbuf, "&");common2:		sdump(n->rgt);common1:		sdump(n->lft);			break;#ifdef NXT	case NEXT:	strcat(dumpbuf, "X");			goto common1;#endif	case NOT:	strcat(dumpbuf, "!");			goto common1;	case TRUE:	strcat(dumpbuf, "T");			break;	case FALSE:	strcat(dumpbuf, "F");			break;	default:	strcat(dumpbuf, "?");			break;	}}Symbol *DoDump(Node *n){	if (!n) return ZS;	if (n->ntyp == PREDICATE)		return n->sym;	dumpbuf[0] = '\0';	sdump(n);	return tl_lookup(dumpbuf);}static intnot_new(Graph *g){	Graph	*q1; Node *tmp, *n1, *n2;	Mapping	*map;	tmp = flatten(g->Old);	/* duplicate, collapse, normalize */	g->Other = g->Old;	/* non normalized full version */	g->Old = tmp;	g->oldstring = DoDump(g->Old);	tmp = flatten(g->Next);	g->nxtstring = DoDump(tmp);	if (tl_verbose) dump_graph(g);	Debug2("\tformula-old: [%s]\n", g->oldstring?g->oldstring->name:"true");	Debug2("\tformula-nxt: [%s]\n", g->nxtstring?g->nxtstring->name:"true");	for (q1 = Nodes_Set; q1; q1 = q1->nxt)	{	Debug2("	compare old to: %s", q1->name->name);		Debug2(" [%s]", q1->oldstring?q1->oldstring->name:"true");		Debug2("	compare nxt to: %s", q1->name->name);		Debug2(" [%s]", q1->nxtstring?q1->nxtstring->name:"true");		if (q1->oldstring != g->oldstring		||  q1->nxtstring != g->nxtstring)		{	Debug(" => different\n");			continue;		}		Debug(" => match\n");		if (g->incoming)			q1->incoming = catSlist(g->incoming, q1->incoming);		/* check if there's anything in g->Other that needs		   adding to q1->Other		*/		for (n2 = g->Other; n2; n2 = n2->nxt)		{	for (n1 = q1->Other; n1; n1 = n1->nxt)				if (isequal(n1, n2))					break;			if (!n1)			{	Node *n3 = dupnode(n2);				/* don't mess up n2->nxt */				n3->nxt = q1->Other;				q1->Other = n3;		}	}		map = (Mapping *) tl_emalloc(sizeof(Mapping));	  	map->from = g->name->name;	  	map->to   = q1;	  	map->nxt = Mapped;	  	Mapped = map;		for (n1 = g->Other; n1; n1 = n2)		{	n2 = n1->nxt;			releasenode(1, n1);		}		for (n1 = g->Old; n1; n1 = n2)		{	n2 = n1->nxt;			releasenode(1, n1);		}		for (n1 = g->Next; n1; n1 = n2)		{	n2 = n1->nxt;			releasenode(1, n1);		}		return 1;	}	if (newstates) tl_verbose=1;	Debug2("	New Node %s [", g->name->name);	for (n1 = g->Old; n1; n1 = n1->nxt)	{ Dump(n1); Debug(", "); }	Debug2("] nr %d\n", Base);	if (newstates) tl_verbose=0;	Base++;	g->nxt = Nodes_Set;	Nodes_Set = g;	return 0;}static voidexpand_g(Graph *g){	Node *now, *n1, *n2, *nx;	int can_release;	if (!g->New)	{	Debug2("\nDone with %s", g->name->name);		if (tl_verbose) dump_graph(g);		if (not_new(g))		{	if (tl_verbose) printf("\tIs Not New\n");			return;		}		if (g->Next)		{	Debug("	Has Next [");			for (n1 = g->Next; n1; n1 = n1->nxt)			{ Dump(n1); Debug(", "); }			Debug("]\n");			ng(ZS, getsym(g->name), g->Next, ZN, ZN);		}		return;	}	if (tl_verbose)	{	Symbol *z;		printf("\nExpand %s, from ", g->name->name);		for (z = g->incoming; z; z = z->next)			printf("%s, ", z->name);		printf("\n\thandle:\t"); Explain(g->New->ntyp);		dump_graph(g);	}	if (g->New->ntyp == AND)	{	if (g->New->nxt)		{	n2 = g->New->rgt;			while (n2->nxt)				n2 = n2->nxt;			n2->nxt = g->New->nxt;		}		n1 = n2 = g->New->lft;		while (n2->nxt)			n2 = n2->nxt;		n2->nxt = g->New->rgt;		releasenode(0, g->New);		g->New = n1;		push_stack(g);		return;	}	can_release = 0;	/* unless it need not go into Old */	now = g->New;	g->New = g->New->nxt;	now->nxt = ZN;	if (now->ntyp != TRUE)	{	if (g->Old)		{	for (n1 = g->Old; n1->nxt; n1 = n1->nxt)				if (isequal(now, n1))				{	can_release = 1;					goto out;				}			n1->nxt = now;		} else			g->Old = now;	}out:	switch (now->ntyp) {	case FALSE:		push_stack(g);		break;	case TRUE:		releasenode(1, now);		push_stack(g);		break;	case PREDICATE:	case NOT:		if (can_release) releasenode(1, now);		push_stack(g);		break;	case V_OPER:		Assert(now->rgt != ZN, now->ntyp);		Assert(now->lft != ZN, now->ntyp);		Assert(now->rgt->nxt == ZN, now->ntyp);		Assert(now->lft->nxt == ZN, now->ntyp);		n1 = now->rgt;		n1->nxt = g->New;		if (can_release)			nx = now;		else			nx = getnode(now); /* now also appears in Old */		nx->nxt = g->Next;		n2 = now->lft;		n2->nxt = getnode(now->rgt);		n2->nxt->nxt = g->New;		g->New = flatten(n2);		push_stack(g);		ng(ZS, g->incoming, n1, g->Old, nx);		break;	case U_OPER:		Assert(now->rgt->nxt == ZN, now->ntyp);		Assert(now->lft->nxt == ZN, now->ntyp);		n1 = now->lft;		if (can_release)			nx = now;		else			nx = getnode(now); /* now also appears in Old */		nx->nxt = g->Next;		n2 = now->rgt;		n2->nxt = g->New;		goto common;#ifdef NXT	case NEXT:		Assert(now->lft != ZN, now->ntyp);		nx = dupnode(now->lft);		nx->nxt = g->Next;		g->Next = nx;		if (can_release) releasenode(0, now);		push_stack(g);		break;#endif	case OR:		Assert(now->rgt->nxt == ZN, now->ntyp);		Assert(now->lft->nxt == ZN, now->ntyp);		n1 = now->lft;		nx = g->Next;		n2 = now->rgt;		n2->nxt = g->New;common:		n1->nxt = g->New;		ng(ZS, g->incoming, n1, g->Old, nx);		g->New = flatten(n2);		if (can_release) releasenode(1, now);		push_stack(g);		break;	}}Node *twocases(Node *p){	Node *q;	/* 1: ([]p1 && []p2) == [](p1 && p2) */	/* 2: (<>p1 || <>p2) == <>(p1 || p2) */	if (!p) return p;	switch(p->ntyp) {	case AND:	case OR:	case U_OPER:	case V_OPER:		p->lft = twocases(p->lft);		p->rgt = twocases(p->rgt);		break;#ifdef NXT	case NEXT:#endif	case NOT:		p->lft = twocases(p->lft);		break;	default:		break;	}	if (p->ntyp == AND	/* 1 */	&&  p->lft->ntyp == V_OPER	&&  p->lft->lft->ntyp == FALSE	&&  p->rgt->ntyp == V_OPER	&&  p->rgt->lft->ntyp == FALSE)	{	q = tl_nn(V_OPER, False,			tl_nn(AND, p->lft->rgt, p->rgt->rgt));	} else	if (p->ntyp == OR	/* 2 */	&&  p->lft->ntyp == U_OPER	&&  p->lft->lft->ntyp == TRUE	&&  p->rgt->ntyp == U_OPER	&&  p->rgt->lft->ntyp == TRUE)	{	q = tl_nn(U_OPER, True,			tl_nn(OR, p->lft->rgt, p->rgt->rgt));	} else		q = p;	return q;}voidtrans(Node *p){	Node	*op;	Graph	*g;	if (!p || tl_errs) return;	p = twocases(p);	if (tl_verbose || tl_terse)	{	fprintf(tl_out, "\t/* Normlzd: ");		dump(p);		fprintf(tl_out, " */\n");	}	if (tl_terse)		return;	op = dupnode(p);	ng(ZS, getsym(tl_lookup("init")), p, ZN, ZN);	while ((g = Nodes_Stack) != (Graph *) 0)	{	Nodes_Stack = g->nxt;		expand_g(g);	}	if (newstates)		return;	fixinit(p);	liveness(flatten(op));	/* was: liveness(op); */	mkbuchi();	if (tl_verbose)	{	printf("/*\n");		printf(" * %d states in Streett automaton\n", Base);		printf(" * %d Streett acceptance conditions\n", Max_Red);		printf(" * %d Buchi states\n", Total);		printf(" */\n");	}}