123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146 |
- /***** tl_spin: tl_lex.c *****/
- /* Copyright (c) 1995-2000 by Lucent Technologies - Bell Laboratories */
- /* All Rights Reserved. This software is for educational purposes only. */
- /* Permission is given to distribute this code provided that this intro- */
- /* ductory message is not removed and no monies are exchanged. */
- /* No guarantee is expressed or implied by the distribution of this code. */
- /* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */
- /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
- /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
- /* Send bug-reports and/or questions to: gerard@research.bell-labs.com */
- #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 void
- 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 int
- 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;
- }
- int
- tl_yylex(void)
- { int c = tl_lex();
- #if 0
- printf("c = %d\n", c);
- #endif
- return c;
- }
- static int
- tl_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))
- { 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 = follow('\\', AND, '/'); break;
- case '\\': c = follow('/', OR, '\\'); break;
- case '&' : c = follow('&', AND, '&'); break;
- case '|' : c = follow('|', OR, '|'); break;
- case '[' : c = follow(']', ALWAYS, '['); break;
- case '-' : c = 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(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;
- }
|