Import sources from 2011-03-30 iso image

1 files changed, 875 insertions, 0 deletions

diff --git a/sys/src/cmd/spin/tl_trans.c b/sys/src/cmd/spin/tl_trans.c
new file mode 100755
index 000000000..72964ca6b
--- /dev/null
+++ b/sys/src/cmd/spin/tl_trans.c
@@ -0,0 +1,875 @@
+/***** tl_spin: tl_trans.c *****/
+
+/* Copyright (c) 1995-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            */
+
+/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
+/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.   */
+
+#include "tl.h"
+
+extern FILE	*tl_out;
+extern int	tl_errs, tl_verbose, tl_terse, newstates;
+
+int	Stack_mx=0, Max_Red=0, Total=0;
+
+static Mapping	*Mapped = (Mapping *) 0;
+static Graph	*Nodes_Set = (Graph *) 0;
+static Graph	*Nodes_Stack = (Graph *) 0;
+
+static char	dumpbuf[2048];
+static int	Red_cnt  = 0;
+static int	Lab_cnt  = 0;
+static int	Base     = 0;
+static int	Stack_sz = 0;
+
+static Graph	*findgraph(char *);
+static Graph	*pop_stack(void);
+static Node	*Duplicate(Node *);
+static Node	*flatten(Node *);
+static Symbol	*catSlist(Symbol *, Symbol *);
+static Symbol	*dupSlist(Symbol *);
+static char	*newname(void);
+static int	choueka(Graph *, int);
+static int	not_new(Graph *);
+static int	set_prefix(char *, int, Graph *);
+static void	Addout(char *, char *);
+static void	fsm_trans(Graph *, int, char *);
+static void	mkbuchi(void);
+static void	expand_g(Graph *);
+static void	fixinit(Node *);
+static void	liveness(Node *);
+static void	mk_grn(Node *);
+static void	mk_red(Node *);
+static void	ng(Symbol *, Symbol *, Node *, Node *, Node *);
+static void	push_stack(Graph *);
+static void	sdump(Node *);
+
+static void
+dump_graph(Graph *g)
+{	Node *n1;
+
+	printf("\n\tnew:\t");
+	for (n1 = g->New; n1; n1 = n1->nxt)
+	{ dump(n1); printf(", "); }
+	printf("\n\told:\t");
+	for (n1 = g->Old; n1; n1 = n1->nxt)
+	{ dump(n1); printf(", "); }
+	printf("\n\tnxt:\t");
+	for (n1 = g->Next; n1; n1 = n1->nxt)
+	{ dump(n1); printf(", "); }
+	printf("\n\tother:\t");
+	for (n1 = g->Other; n1; n1 = n1->nxt)
+	{ dump(n1); printf(", "); }
+	printf("\n");
+}
+
+static void
+push_stack(Graph *g)
+{
+	if (!g) return;
+
+	g->nxt = Nodes_Stack;
+	Nodes_Stack = g;
+	if (tl_verbose)
+	{	Symbol *z;
+		printf("\nPush %s, from ", g->name->name);
+		for (z = g->incoming; z; z = z->next)
+			printf("%s, ", z->name);
+		dump_graph(g);
+	}
+	Stack_sz++;
+	if (Stack_sz > Stack_mx) Stack_mx = Stack_sz;
+}
+
+static Graph *
+pop_stack(void)
+{	Graph *g = Nodes_Stack;
+
+	if (g) Nodes_Stack = g->nxt;
+
+	Stack_sz--;
+
+	return g;
+}
+
+static char *
+newname(void)
+{	static int cnt = 0;
+	static char buf[32];
+	sprintf(buf, "S%d", cnt++);
+	return buf;
+}
+
+static int
+has_clause(int tok, Graph *p, Node *n)
+{	Node *q, *qq;
+
+	switch (n->ntyp) {
+	case AND:
+		return	has_clause(tok, p, n->lft) &&
+			has_clause(tok, p, n->rgt);
+	case OR:
+		return	has_clause(tok, p, n->lft) ||
+			has_clause(tok, p, n->rgt);
+	}
+
+	for (q = p->Other; q; q = q->nxt)
+	{	qq = right_linked(q);
+		if (anywhere(tok, n, qq))
+			return 1;
+	}
+	return 0;
+}
+
+static void
+mk_grn(Node *n)
+{	Graph *p;
+
+	n = right_linked(n);
+more:
+	for (p = Nodes_Set; p; p = p->nxt)
+		if (p->outgoing
+		&&  has_clause(AND, p, n))
+		{	p->isgrn[p->grncnt++] =
+				(unsigned char) Red_cnt;
+			Lab_cnt++;
+		}
+
+	if (n->ntyp == U_OPER)	/* 3.4.0 */
+	{	n = n->rgt;
+		goto more;
+	}
+}
+
+static void
+mk_red(Node *n)
+{	Graph *p;
+
+	n = right_linked(n);
+	for (p = Nodes_Set; p; p = p->nxt)
+	{	if (p->outgoing
+		&&  has_clause(0, p, n))
+		{	if (p->redcnt >= 63)
+				Fatal("too many Untils", (char *)0);
+			p->isred[p->redcnt++] =
+				(unsigned char) Red_cnt;
+			Lab_cnt++; Max_Red = Red_cnt;
+	}	}
+}
+
+static void
+liveness(Node *n)
+{
+	if (n)
+	switch (n->ntyp) {
+#ifdef NXT
+	case NEXT:
+		liveness(n->lft);
+		break;
+#endif
+	case U_OPER:
+		Red_cnt++;
+		mk_red(n);
+		mk_grn(n->rgt);
+		/* fall through */
+	case V_OPER:
+	case OR: case AND:
+		liveness(n->lft);
+		liveness(n->rgt);
+		break;
+	}
+}
+
+static Graph *
+findgraph(char *nm)
+{	Graph	*p;
+	Mapping *m;
+
+	for (p = Nodes_Set; p; p = p->nxt)
+		if (!strcmp(p->name->name, nm))
+			return p;
+	for (m = Mapped; m; m = m->nxt)
+		if (strcmp(m->from, nm) == 0)
+			return m->to;
+
+	printf("warning: node %s not found\n", nm);
+	return (Graph *) 0;
+}
+
+static void
+Addout(char *to, char *from)
+{	Graph	*p = findgraph(from);
+	Symbol	*s;
+
+	if (!p) return;
+	s = getsym(tl_lookup(to));
+	s->next = p->outgoing;
+	p->outgoing = s;
+}
+
+#ifdef NXT
+int
+only_nxt(Node *n)
+{
+	switch (n->ntyp) {
+	case NEXT:
+		return 1;
+	case OR:
+	case AND:
+		return only_nxt(n->rgt) && only_nxt(n->lft);
+	default:
+		return 0;
+	}
+}
+#endif
+
+int
+dump_cond(Node *pp, Node *r, int first)
+{	Node *q;
+	int frst = first;
+
+	if (!pp) return frst;
+
+	q = dupnode(pp);
+	q = rewrite(q);
+
+	if (q->ntyp == PREDICATE
+	||  q->ntyp == NOT
+#ifndef NXT
+	||  q->ntyp == OR
+#endif
+	||  q->ntyp == FALSE)
+	{	if (!frst) fprintf(tl_out, " && ");
+		dump(q);
+		frst = 0;
+#ifdef NXT
+	} else if (q->ntyp == OR)
+	{	if (!frst) fprintf(tl_out, " && ");
+		fprintf(tl_out, "((");
+		frst = dump_cond(q->lft, r, 1);
+
+		if (!frst)
+			fprintf(tl_out, ") || (");
+		else
+		{	if (only_nxt(q->lft))
+			{	fprintf(tl_out, "1))");
+				return 0;
+			}
+		}
+
+		frst = dump_cond(q->rgt, r, 1);
+
+		if (frst)
+		{	if (only_nxt(q->rgt))
+				fprintf(tl_out, "1");
+			else
+				fprintf(tl_out, "0");
+			frst = 0;
+		}
+
+		fprintf(tl_out, "))");
+#endif
+	} else  if (q->ntyp == V_OPER
+		&& !anywhere(AND, q->rgt, r))
+	{	frst = dump_cond(q->rgt, r, frst);
+	} else  if (q->ntyp == AND)
+	{
+		frst = dump_cond(q->lft, r, frst);
+		frst = dump_cond(q->rgt, r, frst);
+	}
+
+	return frst;
+}
+
+static int
+choueka(Graph *p, int count)
+{	int j, k, incr_cnt = 0;
+
+	for (j = count; j <= Max_Red; j++) /* for each acceptance class */
+	{	int delta = 0;
+
+		/* is state p labeled Grn-j OR not Red-j ? */
+
+		for (k = 0; k < (int) p->grncnt; k++)
+			if (p->isgrn[k] == j)
+			{	delta = 1;
+				break;
+			}
+		if (delta)
+		{	incr_cnt++;
+			continue;
+		}
+		for (k = 0; k < (int) p->redcnt; k++)
+			if (p->isred[k] == j)
+			{	delta = 1;
+				break;
+			}
+
+		if (delta) break;
+
+		incr_cnt++;
+	}
+	return incr_cnt;
+}
+
+static int
+set_prefix(char *pref, int count, Graph *r2)
+{	int incr_cnt = 0;	/* acceptance class 'count' */
+
+	if (Lab_cnt == 0
+	||  Max_Red == 0)
+		sprintf(pref, "accept");	/* new */
+	else if (count >= Max_Red)
+		sprintf(pref, "T0");		/* cycle */
+	else
+	{	incr_cnt = choueka(r2, count+1);
+		if (incr_cnt + count >= Max_Red)
+			sprintf(pref, "accept"); /* last hop */
+		else
+			sprintf(pref, "T%d", count+incr_cnt);
+	}
+	return incr_cnt;
+}
+
+static void
+fsm_trans(Graph *p, int count, char *curnm)
+{	Graph	*r;
+	Symbol	*s;
+	char	prefix[128], nwnm[128];
+
+	if (!p->outgoing)
+		addtrans(p, curnm, False, "accept_all");
+
+	for (s = p->outgoing; s; s = s->next)
+	{	r = findgraph(s->name);
+		if (!r) continue;
+		if (r->outgoing)
+		{	(void) set_prefix(prefix, count, r);
+			sprintf(nwnm, "%s_%s", prefix, s->name);
+		} else
+			strcpy(nwnm, "accept_all");
+
+		if (tl_verbose)
+		{	printf("maxred=%d, count=%d, curnm=%s, nwnm=%s ",
+				Max_Red, count, curnm, nwnm);
+			printf("(greencnt=%d,%d, redcnt=%d,%d)\n",
+				r->grncnt, r->isgrn[0],
+				r->redcnt, r->isred[0]);
+		}
+		addtrans(p, curnm, r->Old, nwnm);
+	}
+}
+
+static void
+mkbuchi(void)
+{	Graph	*p;
+	int	k;
+	char	curnm[64];
+
+	for (k = 0; k <= Max_Red; k++)
+	for (p = Nodes_Set; p; p = p->nxt)
+	{	if (!p->outgoing)
+			continue;
+		if (k != 0
+		&& !strcmp(p->name->name, "init")
+		&&  Max_Red != 0)
+			continue;
+
+		if (k == Max_Red
+		&&  strcmp(p->name->name, "init") != 0)
+			strcpy(curnm, "accept_");
+		else
+			sprintf(curnm, "T%d_", k);
+
+		strcat(curnm, p->name->name);
+
+		fsm_trans(p, k, curnm);
+	}
+	fsm_print();
+}
+
+static Symbol *
+dupSlist(Symbol *s)
+{	Symbol *p1, *p2, *p3, *d = ZS;
+
+	for (p1 = s; p1; p1 = p1->next)
+	{	for (p3 = d; p3; p3 = p3->next)
+		{	if (!strcmp(p3->name, p1->name))
+				break;
+		}
+		if (p3) continue;	/* a duplicate */
+
+		p2 = getsym(p1);
+		p2->next = d;
+		d = p2;
+	}
+	return d;
+}
+
+static Symbol *
+catSlist(Symbol *a, Symbol *b)
+{	Symbol *p1, *p2, *p3, *tmp;
+
+	/* remove duplicates from b */
+	for (p1 = a; p1; p1 = p1->next)
+	{	p3 = ZS;
+		for (p2 = b; p2; p2 = p2->next)
+		{	if (strcmp(p1->name, p2->name))
+			{	p3 = p2;
+				continue;
+			}
+			tmp = p2->next;
+			tfree((void *) p2);
+			if (p3)
+				p3->next = tmp;
+			else
+				b = tmp;
+	}	}
+	if (!a) return b;
+	if (!b) return a;
+	if (!b->next)
+	{	b->next = a;
+		return b;
+	}
+	/* find end of list */
+	for (p1 = a; p1->next; p1 = p1->next)
+		;
+	p1->next = b;
+	return a;
+}
+
+static void
+fixinit(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 void
+ng(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 void
+sdump(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 int
+not_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 void
+expand_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->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:
+		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;
+}
+
+void
+trans(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");
+	}
+}