/***** 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 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 = %d\n", c);#endif	return c;} 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 (islower(c))	{	tl_getword(c, isalnum_);		if (strcmp("true", yytext) == 0)		{	Token(TRUE);		}		if (strcmp("false", yytext) == 0)		{	Token(FALSE);		}		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;}