/***** tl_spin: tl_parse.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_yylex(void);extern int	tl_verbose, tl_errs; int	tl_yychar = 0;YYSTYPE	tl_yylval; static Node	*tl_formula(void);static Node	*tl_factor(void);static Node	*tl_level(int); static int	prec[2][4] = {	{ U_OPER,  V_OPER, 0, 0 },	/* left associative */	{ OR, AND, IMPLIES, EQUIV, },	/* left associative */}; static Node *tl_factor(void){	Node *ptr = ZN; 	switch (tl_yychar) {	case '(':		ptr = tl_formula();		if (tl_yychar != ')')			tl_yyerror("expected ')'");		tl_yychar = tl_yylex();		break;	case NOT:		ptr = tl_yylval;		tl_yychar = tl_yylex();		ptr->lft = tl_factor();		ptr = push_negation(ptr);		break;	case ALWAYS:		tl_yychar = tl_yylex();		ptr = tl_factor();#ifndef NO_OPT		if (ptr->ntyp == FALSE		||  ptr->ntyp == TRUE)			break;	/* [] false == false */ 		if (ptr->ntyp == V_OPER)		{	if (ptr->lft->ntyp == FALSE)				break;	/* [][]p = []p */ 			ptr = ptr->rgt;	/* [] (p V q) = [] q */		}#endif		ptr = tl_nn(V_OPER, False, ptr);		break;#ifdef NXT	case NEXT:		tl_yychar = tl_yylex();		ptr = tl_factor();		if (ptr->ntyp == TRUE)			break;	/* X true = true */		ptr = tl_nn(NEXT, ptr, ZN);		break;#endif	case EVENTUALLY:		tl_yychar = tl_yylex(); 		ptr = tl_factor();#ifndef NO_OPT		if (ptr->ntyp == TRUE		||  ptr->ntyp == FALSE)			break;	/* <> true == true */ 		if (ptr->ntyp == U_OPER		&&  ptr->lft->ntyp == TRUE)			break;	/* <><>p = <>p */ 		if (ptr->ntyp == U_OPER)		{	/* <> (p U q) = <> q */			ptr = ptr->rgt;			/* fall thru */		}#endif		ptr = tl_nn(U_OPER, True, ptr); 		break;	case PREDICATE:		ptr = tl_yylval;		tl_yychar = tl_yylex();		break;	case TRUE:	case FALSE:		ptr = tl_yylval;		tl_yychar = tl_yylex();		break;	}	if (!ptr) tl_yyerror("expected predicate");#if 0	printf("factor:	");	tl_explain(ptr->ntyp);	printf("\n");#endif	return ptr;} static Node *bin_simpler(Node *ptr){	Node *a, *b; 	if (ptr)	switch (ptr->ntyp) {	case U_OPER:#ifndef NO_OPT		if (ptr->rgt->ntyp == TRUE		||  ptr->rgt->ntyp == FALSE		||  ptr->lft->ntyp == FALSE)		{	ptr = ptr->rgt;			break;		}		if (isequal(ptr->lft, ptr->rgt))		{	/* p U p = p */				ptr = ptr->rgt;			break;		}		if (ptr->lft->ntyp == U_OPER		&&  isequal(ptr->lft->lft, ptr->rgt))		{	/* (p U q) U p = (q U p) */			ptr->lft = ptr->lft->rgt;			break;		}		if (ptr->rgt->ntyp == U_OPER		&&  ptr->rgt->lft->ntyp == TRUE)		{	/* p U (T U q)  = (T U q) */			ptr = ptr->rgt;			break;		}#ifdef NXT		/* X p U X q == X (p U q) */		if (ptr->rgt->ntyp == NEXT		&&  ptr->lft->ntyp == NEXT)		{	ptr = tl_nn(NEXT,				tl_nn(U_OPER,					ptr->lft->lft,					ptr->rgt->lft), ZN);		}#endif#endif		break;	case V_OPER:#ifndef NO_OPT		if (ptr->rgt->ntyp == FALSE		||  ptr->rgt->ntyp == TRUE		||  ptr->lft->ntyp == TRUE)		{	ptr = ptr->rgt;			break;		}		if (isequal(ptr->lft, ptr->rgt))		{	/* p V p = p */				ptr = ptr->rgt;			break;		}		/* F V (p V q) == F V q */		if (ptr->lft->ntyp == FALSE		&&  ptr->rgt->ntyp == V_OPER)		{	ptr->rgt = ptr->rgt->rgt;			break;		}		/* p V (F V q) == F V q */		if (ptr->rgt->ntyp == V_OPER		&&  ptr->rgt->lft->ntyp == FALSE)		{	ptr->lft = False;			ptr->rgt = ptr->rgt->rgt;			break;		}#endif		break;	case IMPLIES:#ifndef NO_OPT		if (isequal(ptr->lft, ptr->rgt))		{	ptr = True;			break;		}#endif		ptr = tl_nn(OR, Not(ptr->lft), ptr->rgt);		ptr = rewrite(ptr);		break;	case EQUIV:#ifndef NO_OPT		if (isequal(ptr->lft, ptr->rgt))		{	ptr = True;			break;		}#endif		a = rewrite(tl_nn(AND,			dupnode(ptr->lft),			dupnode(ptr->rgt)));		b = rewrite(tl_nn(AND,			Not(ptr->lft),			Not(ptr->rgt)));		ptr = tl_nn(OR, a, b);		ptr = rewrite(ptr);		break;	case AND:#ifndef NO_OPT		/* p && (q U p) = p */		if (ptr->rgt->ntyp == U_OPER		&&  isequal(ptr->rgt->rgt, ptr->lft))		{	ptr = ptr->lft;			break;		}		if (ptr->lft->ntyp == U_OPER		&&  isequal(ptr->lft->rgt, ptr->rgt))		{	ptr = ptr->rgt;			break;		} 		/* p && (q V p) == q V p */		if (ptr->rgt->ntyp == V_OPER		&&  isequal(ptr->rgt->rgt, ptr->lft))		{	ptr = ptr->rgt;			break;		}		if (ptr->lft->ntyp == V_OPER		&&  isequal(ptr->lft->rgt, ptr->rgt))		{	ptr = ptr->lft;			break;		} 		/* (p U q) && (r U q) = (p && r) U q*/		if (ptr->rgt->ntyp == U_OPER		&&  ptr->lft->ntyp == U_OPER		&&  isequal(ptr->rgt->rgt, ptr->lft->rgt))		{	ptr = tl_nn(U_OPER,				tl_nn(AND, ptr->lft->lft, ptr->rgt->lft),				ptr->lft->rgt);			break;		} 		/* (p V q) && (p V r) = p V (q && r) */		if (ptr->rgt->ntyp == V_OPER		&&  ptr->lft->ntyp == V_OPER		&&  isequal(ptr->rgt->lft, ptr->lft->lft))		{	ptr = tl_nn(V_OPER,				ptr->rgt->lft,				tl_nn(AND, ptr->lft->rgt, ptr->rgt->rgt));			break;		}#ifdef NXT		/* X p && X q == X (p && q) */		if (ptr->rgt->ntyp == NEXT		&&  ptr->lft->ntyp == NEXT)		{	ptr = tl_nn(NEXT,				tl_nn(AND,					ptr->rgt->lft,					ptr->lft->lft), ZN);			break;		}#endif 		if (isequal(ptr->lft, ptr->rgt)	/* (p && p) == p */		||  ptr->rgt->ntyp == FALSE	/* (p && F) == F */		||  ptr->lft->ntyp == TRUE)	/* (T && p) == p */		{	ptr = ptr->rgt;			break;		}			if (ptr->rgt->ntyp == TRUE	/* (p && T) == p */		||  ptr->lft->ntyp == FALSE)	/* (F && p) == F */		{	ptr = ptr->lft;			break;		} 		/* (p V q) && (r U q) == p V q */		if (ptr->rgt->ntyp == U_OPER		&&  ptr->lft->ntyp == V_OPER		&&  isequal(ptr->lft->rgt, ptr->rgt->rgt))		{	ptr = ptr->lft;			break;		}#endif		break; 	case OR:#ifndef NO_OPT		/* p || (q U p) == q U p */		if (ptr->rgt->ntyp == U_OPER		&&  isequal(ptr->rgt->rgt, ptr->lft))		{	ptr = ptr->rgt;			break;		} 		/* p || (q V p) == p */		if (ptr->rgt->ntyp == V_OPER		&&  isequal(ptr->rgt->rgt, ptr->lft))		{	ptr = ptr->lft;			break;		} 		/* (p U q) || (p U r) = p U (q || r) */		if (ptr->rgt->ntyp == U_OPER		&&  ptr->lft->ntyp == U_OPER		&&  isequal(ptr->rgt->lft, ptr->lft->lft))		{	ptr = tl_nn(U_OPER,				ptr->rgt->lft,				tl_nn(OR, ptr->lft->rgt, ptr->rgt->rgt));			break;		} 		if (isequal(ptr->lft, ptr->rgt)	/* (p || p) == p */		||  ptr->rgt->ntyp == FALSE	/* (p || F) == p */		||  ptr->lft->ntyp == TRUE)	/* (T || p) == T */		{	ptr = ptr->lft;			break;		}			if (ptr->rgt->ntyp == TRUE	/* (p || T) == T */		||  ptr->lft->ntyp == FALSE)	/* (F || p) == p */		{	ptr = ptr->rgt;			break;		} 		/* (p V q) || (r V q) = (p || r) V q */		if (ptr->rgt->ntyp == V_OPER		&&  ptr->lft->ntyp == V_OPER		&&  isequal(ptr->lft->rgt, ptr->rgt->rgt))		{	ptr = tl_nn(V_OPER,				tl_nn(OR, ptr->lft->lft, ptr->rgt->lft),				ptr->rgt->rgt);			break;		} 		/* (p V q) || (r U q) == r U q */		if (ptr->rgt->ntyp == U_OPER		&&  ptr->lft->ntyp == V_OPER		&&  isequal(ptr->lft->rgt, ptr->rgt->rgt))		{	ptr = ptr->rgt;			break;		}		#endif		break;	}	return ptr;} static Node *tl_level(int nr){	int i; Node *ptr = ZN; 	if (nr < 0)		return tl_factor(); 	ptr = tl_level(nr-1);again:	for (i = 0; i < 4; i++)		if (tl_yychar == prec[nr][i])		{	tl_yychar = tl_yylex();			ptr = tl_nn(prec[nr][i],				ptr, tl_level(nr-1));			ptr = bin_simpler(ptr);			goto again;		}	if (!ptr) tl_yyerror("syntax error");#if 0	printf("level %d:	", nr);	tl_explain(ptr->ntyp);	printf("\n");#endif	return ptr;} static Node *tl_formula(void){	tl_yychar = tl_yylex();	return tl_level(1);	/* 2 precedence levels, 1 and 0 */	} voidtl_parse(void){	Node *n; 	/* tl_verbose = 1; */	n = tl_formula();	if (tl_verbose)	{	printf("formula: ");		dump(n);		printf("\n");	}	if (tl_Getchar() != -1)	{	tl_yyerror("syntax error");		tl_errs++;		return;	}	trans(n);}