tl_trans.c

对软件进行可达性测试的软件

	/* 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 != 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;
}

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");
	}
}