/***** tl_spin: tl_buchi.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 int tl_verbose, tl_clutter, Total, Max_Red;extern char *claim_name; FILE	*tl_out;	/* if standalone: = stdout; */ typedef struct Transition {	Symbol *name;	Node *cond;	int redundant, merged, marked;	struct Transition *nxt;} Transition; typedef struct State {	Symbol	*name;	Transition *trans;	Graph	*colors;	unsigned char redundant;	unsigned char accepting;	unsigned char reachable;	struct State *nxt;} State; static State *never = (State *) 0;static int hitsall; voidini_buchi(void){	never = (State *) 0;	hitsall = 0;} static intsametrans(Transition *s, Transition *t){	if (strcmp(s->name->name, t->name->name) != 0)		return 0;	return isequal(s->cond, t->cond);} static Node *Prune(Node *p){	if (p)	switch (p->ntyp) {	case PREDICATE:	case NOT:	case FALSE:	case TRUE:#ifdef NXT	case NEXT:#endif		return p;	case OR:		p->lft = Prune(p->lft);		if (!p->lft)		{	releasenode(1, p->rgt);			return ZN;		}		p->rgt = Prune(p->rgt);		if (!p->rgt)		{	releasenode(1, p->lft);			return ZN;		}		return p;	case AND:		p->lft = Prune(p->lft);		if (!p->lft)			return Prune(p->rgt);		p->rgt = Prune(p->rgt);		if (!p->rgt)			return p->lft;		return p;	}	releasenode(1, p);	return ZN;} static State *findstate(char *nm){	State *b;	for (b = never; b; b = b->nxt)		if (!strcmp(b->name->name, nm))			return b;	if (strcmp(nm, "accept_all"))	{	if (strncmp(nm, "accept", 6))		{	int i; char altnm[64];			for (i = 0; i < 64; i++)				if (nm[i] == '_')					break;			if (i >= 64)				Fatal("name too long %s", nm);			sprintf(altnm, "accept%s", &nm[i]);			return findstate(altnm);		}	/*	Fatal("buchi: no state %s", nm); */	}	return (State *) 0;} static voidDfs(State *b){	Transition *t; 	if (!b || b->reachable) return;	b->reachable = 1; 	if (b->redundant)		printf("/* redundant state %s */\n",			b->name->name);	for (t = b->trans; t; t = t->nxt)	{	if (!t->redundant)		{	Dfs(findstate(t->name->name));			if (!hitsall			&&  strcmp(t->name->name, "accept_all") == 0)				hitsall = 1;		}	}} voidretarget(char *from, char *to){	State *b;	Transition *t;	Symbol *To = tl_lookup(to); 	if (tl_verbose) printf("replace %s with %s\n", from, to); 	for (b = never; b; b = b->nxt)	{	if (!strcmp(b->name->name, from))			b->redundant = 1;		else		for (t = b->trans; t; t = t->nxt)		{	if (!strcmp(t->name->name, from))				t->name = To;	}	}} #ifdef NXTstatic Node *nonxt(Node *n){	switch (n->ntyp) {	case U_OPER:	case V_OPER:	case NEXT:		return ZN;	case OR:		n->lft = nonxt(n->lft);		n->rgt = nonxt(n->rgt);		if (!n->lft || !n->rgt)			return True;		return n;	case AND:		n->lft = nonxt(n->lft);		n->rgt = nonxt(n->rgt);		if (!n->lft)		{	if (!n->rgt)				n = ZN;			else				n = n->rgt;		} else if (!n->rgt)			n = n->lft;		return n;	}	return n;}#endif static Node *combination(Node *s, Node *t){	Node *nc;#ifdef NXT	Node *a = nonxt(s);	Node *b = nonxt(t); 	if (tl_verbose)	{	printf("\tnonxtA: "); dump(a);		printf("\n\tnonxtB: "); dump(b);		printf("\n");	}	/* if there's only a X(f), its equivalent to true */	if (!a || !b)		nc = True;	else		nc = tl_nn(OR, a, b);#else	nc = tl_nn(OR, s, t);#endif	if (tl_verbose)	{	printf("\tcombo: "); dump(nc);		printf("\n");	}	return nc;} Node *unclutter(Node *n, char *snm){	Node *t, *s, *v, *u;	Symbol *w; 	/* check only simple cases like !q && q */	for (t = n; t; t = t->rgt)	{	if (t->rgt)		{	if (t->ntyp != AND || !t->lft)				return n;			if (t->lft->ntyp != PREDICATE#ifdef NXT			&&  t->lft->ntyp != NEXT#endif			&&  t->lft->ntyp != NOT)				return n;		} else		{	if (t->ntyp != PREDICATE#ifdef NXT			&&  t->ntyp != NEXT#endif			&&  t->ntyp != NOT)				return n;		}	} 	for (t = n; t; t = t->rgt)	{	if (t->rgt)			v = t->lft;		else			v = t;		if (v->ntyp == NOT		&&  v->lft->ntyp == PREDICATE)		{	w = v->lft->sym;			for (s = n; s; s = s->rgt)			{	if (s == t) continue;				if (s->rgt)					u = s->lft;				else					u = s;				if (u->ntyp == PREDICATE				&&  strcmp(u->sym->name, w->name) == 0)				{	if (tl_verbose)					{	printf("BINGO %s:\t", snm);						dump(n);						printf("\n");					}					return False;				}			}	}	}	return n;} static voidclutter(void){	State *p;	Transition *s; 	for (p = never; p; p = p->nxt)	for (s = p->trans; s; s = s->nxt)	{	s->cond = unclutter(s->cond, p->name->name);		if (s->cond		&&  s->cond->ntyp == FALSE)		{	if (s != p->trans 			||  s->nxt)				s->redundant = 1;		}	}} static voidshowtrans(State *a){	Transition *s; 	for (s = a->trans; s; s = s->nxt)	{	printf("%s ", s->name?s->name->name:"-");		dump(s->cond);		printf(" %d %d %d\n", s->redundant, s->merged, s->marked);	}} static intmergetrans(void){	State *b;	Transition *s, *t;	Node *nc; int cnt = 0; 	for (b = never; b; b = b->nxt)	{	if (!b->reachable) continue; 		for (s = b->trans; s; s = s->nxt)		{	if (s->redundant) continue; 			for (t = s->nxt; t; t = t->nxt)			if (!t->redundant			&&  !strcmp(s->name->name, t->name->name))			{	if (tl_verbose)				{	printf("===\nstate %s, trans to %s redundant\n",					b->name->name, s->name->name);					showtrans(b);					printf(" conditions ");					dump(s->cond); printf(" <-> ");					dump(t->cond); printf("\n");				} 				if (!s->cond) /* same as T */				{	releasenode(1, t->cond); /* T or t */					nc = True;				} else if (!t->cond)				{	releasenode(1, s->cond);					nc = True;				} else				{	nc = combination(s->cond, t->cond);				}				t->cond = rewrite(nc);				t->merged = 1;				s->redundant = 1;				cnt++;				break;	}	}	}	return cnt;} static intall_trans_match(State *a, State *b){	Transition *s, *t;	int found, result = 0; 	if (a->accepting != b->accepting)		goto done; 	for (s = a->trans; s; s = s->nxt)	{	if (s->redundant) continue;		found = 0;		for (t = b->trans; t; t = t->nxt)		{	if (t->redundant) continue;			if (sametrans(s, t))			{	found = 1;				t->marked = 1;				break;		}	}		if (!found)			goto done;	}	for (s = b->trans; s; s = s->nxt)	{	if (s->redundant || s->marked) continue;		found = 0;		for (t = a->trans; t; t = t->nxt)		{	if (t->redundant) continue;			if (sametrans(s, t))			{	found = 1;				break;		}	}		if (!found)			goto done;	}	result = 1;done:	for (s = b->trans; s; s = s->nxt)		s->marked = 0;	return result;} #ifndef NO_OPT#define BUCKY#endif #ifdef BUCKYstatic intall_bucky(State *a, State *b){	Transition *s, *t;	int found, result = 0; 	for (s = a->trans; s; s = s->nxt)	{	if (s->redundant) continue;		found = 0;		for (t = b->trans; t; t = t->nxt)		{	if (t->redundant) continue; 			if (isequal(s->cond, t->cond))			{	if (strcmp(s->name->name, b->name->name) == 0				&&  strcmp(t->name->name, a->name->name) == 0)				{	found = 1;	/* they point to each other */					t->marked = 1;					break;				}				if (strcmp(s->name->name, t->name->name) == 0				&&  strcmp(s->name->name, "accept_all") == 0)				{	found = 1;					t->marked = 1;					break;				/* same exit from which there is no return */				}			}		}		if (!found)			goto done;	}	for (s = b->trans; s; s = s->nxt)	{	if (s->redundant || s->marked) continue;		found = 0;		for (t = a->trans; t; t = t->nxt)		{	if (t->redundant) continue; 			if (isequal(s->cond, t->cond))			{	if (strcmp(s->name->name, a->name->name) == 0				&&  strcmp(t->name->name, b->name->name) == 0)				{	found = 1;					t->marked = 1;					break;				}				if (strcmp(s->name->name, t->name->name) == 0				&&  strcmp(s->name->name, "accept_all") == 0)				{	found = 1;					t->marked = 1;					break;				}			}		}		if (!found)			goto done;	}	result = 1;done:	for (s = b->trans; s; s = s->nxt)		s->marked = 0;	return result;} static intbuckyballs(void){	State *a, *b, *c, *d;	int m, cnt=0; 	do {		m = 0; cnt++;		for (a = never; a; a = a->nxt)		{	if (!a->reachable) continue; 			if (a->redundant) continue; 			for (b = a->nxt; b; b = b->nxt)			{	if (!b->reachable) continue; 				if (b->redundant) continue; 				if (all_bucky(a, b))				{	m++;					if (tl_verbose)					{	printf("%s bucky match %s\n",						a->name->name, b->name->name);					} 					if (a->accepting && !b->accepting)					{	if (strcmp(b->name->name, "T0_init") == 0)						{	c = a; d = b;							b->accepting = 1;						} else						{	c = b; d = a;						}					} else					{	c = a; d = b;					} 					retarget(c->name->name, d->name->name);					if (!strncmp(c->name->name, "accept", 6)					&&  Max_Red == 0)					{	char buf[64];						sprintf(buf, "T0%s", &(c->name->name[6]));						retarget(buf, d->name->name);					}					break;				}		}	}	} while (m && cnt < 10);	return cnt-1;}#endif static intmergestates(int v){	State *a, *b;	int m, cnt=0; 	if (tl_verbose)		return 0; 

Lines 1–500 of 674. Load more