1 /***** tl_spin: tl_lex.c *****/
3 /* Copyright (c) 1995-2003 by Lucent Technologies, Bell Laboratories. */
4 /* All Rights Reserved. This software is for educational purposes only. */
5 /* No guarantee whatsoever is expressed or implied by the distribution of */
6 /* this code. Permission is given to distribute this code provided that */
7 /* this introductory message is not removed and no monies are exchanged. */
8 /* Software written by Gerard J. Holzmann. For tool documentation see: */
9 /* http://spinroot.com/ */
10 /* Send all bug-reports and/or questions to: bugs@spinroot.com */
12 /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
13 /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
19 static Symbol *symtab[Nhash+1];
20 static int tl_lex(void);
22 extern YYSTYPE tl_yylval;
25 #define Token(y) tl_yylval = tl_nn(y,ZN,ZN); return y
28 tl_getword(int first, int (*tst)(int))
31 yytext[i++] = (char ) first;
32 while (tst(c = tl_Getchar()))
39 tl_follow(int tok, int ifyes, int ifno)
44 if ((c = tl_Getchar()) == tok)
48 sprintf(buf, "expected '%c'", tok);
49 tl_yyerror(buf); /* no return from here */
57 printf("c = %d\n", c);
68 yytext[0] = (char ) c;
75 } while (c == ' '); /* '\t' is removed in tl_main.c */
78 { tl_getword(c, isalnum_);
79 if (strcmp("true", yytext) == 0)
82 if (strcmp("false", yytext) == 0)
85 tl_yylval = tl_nn(PREDICATE,ZN,ZN);
86 tl_yylval->sym = tl_lookup(yytext);
96 tl_yyerror("expected '<>' or '<->'");
103 tl_yyerror("expected '<->'");
107 case '/' : c = tl_follow('\\', AND, '/'); break;
108 case '\\': c = tl_follow('/', OR, '\\'); break;
109 case '&' : c = tl_follow('&', AND, '&'); break;
110 case '|' : c = tl_follow('|', OR, '|'); break;
111 case '[' : c = tl_follow(']', ALWAYS, '['); break;
112 case '-' : c = tl_follow('>', IMPLIES, '-'); break;
113 case '!' : c = NOT; break;
114 case 'U' : c = U_OPER; break;
115 case 'V' : c = V_OPER; break;
117 case 'X' : c = NEXT; break;
129 for (sp = symtab[h]; sp; sp = sp->next)
130 if (strcmp(sp->name, s) == 0)
133 sp = (Symbol *) tl_emalloc(sizeof(Symbol));
134 sp->name = (char *) tl_emalloc((int) strlen(s) + 1);
136 sp->next = symtab[h];
144 { Symbol *n = (Symbol *) tl_emalloc(sizeof(Symbol));