/***** 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 voiddump_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 voidpush_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 inthas_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 voidmk_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 voidmk_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 voidliveness(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 voidAddout(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 NXTintonly_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;	}}#endifintdump_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 intchoueka(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 intset_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 voidfsm_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 voidmkbuchi(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;	}