tl_trans.c

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

/***** 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: [e-mail]            */

/* 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[256];

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