/***** tl_spin: tl_lex.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 <stdlib.h>#include <ctype.h>#include "tl.h" static Symbol	*symtab[Nhash+1];static int	tl_lex(void);extern int tl_peek(int); extern YYSTYPE	tl_yylval;extern char	yytext[]; #define Token(y)        tl_yylval = tl_nn(y,ZN,ZN); return y static voidtl_getword(int first, int (*tst)(int)){	int i=0; char c; 	yytext[i++] = (char ) first;	while (tst(c = tl_Getchar()))		yytext[i++] = c;	yytext[i] = '\0';	tl_UnGetchar();} static inttl_follow(int tok, int ifyes, int ifno){	int c;	char buf[32];	extern int tl_yychar; 	if ((c = tl_Getchar()) == tok)		return ifyes;	tl_UnGetchar();	tl_yychar = c;	sprintf(buf, "expected '%c'", tok);	tl_yyerror(buf);	/* no return from here */	return ifno;} inttl_yylex(void){	int c = tl_lex();#if 0	printf("c = %c (%d)\n", c, c);#endif	return c;} static intis_predicate(int z){	char c, c_prev = z;	char want = (z == '{') ? '}' : ')';	int i = 0, j, nesting = 0;	char peek_buf[512]; 	c = tl_peek(i++);	/* look ahead without changing position */	while ((c != want || nesting > 0) && c != -1 && i < 2047)	{	if (islower((int) c))		{	peek_buf[0] = c;			j = 1;			while (j < (int) sizeof(peek_buf) && isalnum((int)(c = tl_peek(i))))			{	peek_buf[j++] = c;				i++;			}			c = 0;	/* make sure we don't match on z or want on the peekahead */			if (j >= (int) sizeof(peek_buf))			{	peek_buf[j-1] = '\0';				fatal("name '%s' in ltl formula too long", peek_buf);			}			peek_buf[j] = '\0';			if (strcmp(peek_buf, "always") == 0			||  strcmp(peek_buf, "eventually") == 0			||  strcmp(peek_buf, "until") == 0			||  strcmp(peek_buf, "next") == 0)			{	return 0;			}		} else		{	char c_nxt = tl_peek(i);			if (((c == 'U' || c == 'V' || c == 'X') && !isalnum_(c_prev) && !isalnum_(c_nxt))			||  (c == '<' && c_nxt == '>')			||  (c == '[' && c_nxt == ']'))			{	return 0;		}	} 		if (c == z)		{	nesting++;		}		if (c == want)		{	nesting--;		}		c_prev = c;		c = tl_peek(i++);	}	return 1;} static voidread_upto_closing(int z){	char c, want = (z == '{') ? '}' : ')';	int i = 0, nesting = 0; 	c = tl_Getchar();	while ((c != want || nesting > 0) && c != -1 && i < 2047) /* yytext is 2048 */	{	yytext[i++] = c;		if (c == z)		{	nesting++;		}		if (c == want)		{	nesting--;		}		c = tl_Getchar();	}	yytext[i] = '\0';} static inttl_lex(void){	int c; 	do {		c = tl_Getchar();		yytext[0] = (char ) c;		yytext[1] = '\0'; 		if (c <= 0)		{	Token(';');		} 	} while (c == ' ');	/* '\t' is removed in tl_main.c */ 	if (c == '{' || c == '(')	/* new 6.0.0 */	{	if (is_predicate(c))		{	read_upto_closing(c);			tl_yylval = tl_nn(PREDICATE,ZN,ZN);			tl_yylval->sym = tl_lookup(yytext);			return PREDICATE;	}	} 	if (c == '}')	{	tl_yyerror("unexpected '}'");	}	if (islower(c))	{	tl_getword(c, isalnum_);		if (strcmp("true", yytext) == 0)		{	Token(TRUE);		}		if (strcmp("false", yytext) == 0)		{	Token(FALSE);		}		if (strcmp("always", yytext) == 0)		{	Token(ALWAYS);		}		if (strcmp("eventually", yytext) == 0)		{	Token(EVENTUALLY);		}		if (strcmp("until", yytext) == 0)		{	Token(U_OPER);		}#ifdef NXT		if (strcmp("next", yytext) == 0)		{	Token(NEXT);		}#endif		if (strcmp("not", yytext) == 0)		{	Token(NOT);		}		tl_yylval = tl_nn(PREDICATE,ZN,ZN);		tl_yylval->sym = tl_lookup(yytext);		return PREDICATE;	} 	if (c == '<')	{	c = tl_Getchar();		if (c == '>')		{	Token(EVENTUALLY);		}		if (c != '-')		{	tl_UnGetchar();			tl_yyerror("expected '<>' or '<->'");		}		c = tl_Getchar();		if (c == '>')		{	Token(EQUIV);		}		tl_UnGetchar();		tl_yyerror("expected '<->'");	} 	switch (c) {	case '/' : c = tl_follow('\\', AND, '/'); break;	case '\\': c = tl_follow('/', OR, '\\'); break;	case '&' : c = tl_follow('&', AND, '&'); break;	case '|' : c = tl_follow('|', OR, '|'); break;	case '[' : c = tl_follow(']', ALWAYS, '['); break;	case '-' : c = tl_follow('>', IMPLIES, '-'); break;	case '!' : c = NOT; break;	case 'U' : c = U_OPER; break;	case 'V' : c = V_OPER; break;#ifdef NXT	case 'X' : c = NEXT; break;#endif	default  : break;	}	Token(c);} Symbol *tl_lookup(char *s){	Symbol *sp;	int h = hash(s); 	for (sp = symtab[h]; sp; sp = sp->next)		if (strcmp(sp->name, s) == 0)			return sp; 	sp = (Symbol *) tl_emalloc(sizeof(Symbol));	sp->name = (char *) tl_emalloc((int) strlen(s) + 1);	strcpy(sp->name, s);	sp->next = symtab[h];	symtab[h] = sp; 	return sp;} Symbol *getsym(Symbol *s){	Symbol *n = (Symbol *) tl_emalloc(sizeof(Symbol)); 	n->name = s->name;	return n;}