| 1 | /***** tl_spin: tl_lex.c *****/ |
| 2 | |
| 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 */ |
| 11 | |
| 12 | /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */ |
| 13 | /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */ |
| 14 | |
| 15 | #include <stdlib.h> |
| 16 | #include <ctype.h> |
| 17 | #include "tl.h" |
| 18 | |
| 19 | static Symbol *symtab[Nhash+1]; |
| 20 | static int tl_lex(void); |
| 21 | |
| 22 | extern YYSTYPE tl_yylval; |
| 23 | extern char yytext[]; |
| 24 | |
| 25 | #define Token(y) tl_yylval = tl_nn(y,ZN,ZN); return y |
| 26 | |
| 27 | static void |
| 28 | tl_getword(int first, int (*tst)(int)) |
| 29 | { int i=0; char c; |
| 30 | |
| 31 | yytext[i++] = (char ) first; |
| 32 | while (tst(c = tl_Getchar())) |
| 33 | yytext[i++] = c; |
| 34 | yytext[i] = '\0'; |
| 35 | tl_UnGetchar(); |
| 36 | } |
| 37 | |
| 38 | static int |
| 39 | tl_follow(int tok, int ifyes, int ifno) |
| 40 | { int c; |
| 41 | char buf[32]; |
| 42 | extern int tl_yychar; |
| 43 | |
| 44 | if ((c = tl_Getchar()) == tok) |
| 45 | return ifyes; |
| 46 | tl_UnGetchar(); |
| 47 | tl_yychar = c; |
| 48 | sprintf(buf, "expected '%c'", tok); |
| 49 | tl_yyerror(buf); /* no return from here */ |
| 50 | return ifno; |
| 51 | } |
| 52 | |
| 53 | int |
| 54 | tl_yylex(void) |
| 55 | { int c = tl_lex(); |
| 56 | #if 0 |
| 57 | printf("c = %d\n", c); |
| 58 | #endif |
| 59 | return c; |
| 60 | } |
| 61 | |
| 62 | static int |
| 63 | tl_lex(void) |
| 64 | { int c; |
| 65 | |
| 66 | do { |
| 67 | c = tl_Getchar(); |
| 68 | yytext[0] = (char ) c; |
| 69 | yytext[1] = '\0'; |
| 70 | |
| 71 | if (c <= 0) |
| 72 | { Token(';'); |
| 73 | } |
| 74 | |
| 75 | } while (c == ' '); /* '\t' is removed in tl_main.c */ |
| 76 | |
| 77 | if (islower(c)) |
| 78 | { tl_getword(c, isalnum_); |
| 79 | if (strcmp("true", yytext) == 0) |
| 80 | { Token(TRUE); |
| 81 | } |
| 82 | if (strcmp("false", yytext) == 0) |
| 83 | { Token(FALSE); |
| 84 | } |
| 85 | tl_yylval = tl_nn(PREDICATE,ZN,ZN); |
| 86 | tl_yylval->sym = tl_lookup(yytext); |
| 87 | return PREDICATE; |
| 88 | } |
| 89 | if (c == '<') |
| 90 | { c = tl_Getchar(); |
| 91 | if (c == '>') |
| 92 | { Token(EVENTUALLY); |
| 93 | } |
| 94 | if (c != '-') |
| 95 | { tl_UnGetchar(); |
| 96 | tl_yyerror("expected '<>' or '<->'"); |
| 97 | } |
| 98 | c = tl_Getchar(); |
| 99 | if (c == '>') |
| 100 | { Token(EQUIV); |
| 101 | } |
| 102 | tl_UnGetchar(); |
| 103 | tl_yyerror("expected '<->'"); |
| 104 | } |
| 105 | |
| 106 | switch (c) { |
| 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; |
| 116 | #ifdef NXT |
| 117 | case 'X' : c = NEXT; break; |
| 118 | #endif |
| 119 | default : break; |
| 120 | } |
| 121 | Token(c); |
| 122 | } |
| 123 | |
| 124 | Symbol * |
| 125 | tl_lookup(char *s) |
| 126 | { Symbol *sp; |
| 127 | int h = hash(s); |
| 128 | |
| 129 | for (sp = symtab[h]; sp; sp = sp->next) |
| 130 | if (strcmp(sp->name, s) == 0) |
| 131 | return sp; |
| 132 | |
| 133 | sp = (Symbol *) tl_emalloc(sizeof(Symbol)); |
| 134 | sp->name = (char *) tl_emalloc((int) strlen(s) + 1); |
| 135 | strcpy(sp->name, s); |
| 136 | sp->next = symtab[h]; |
| 137 | symtab[h] = sp; |
| 138 | |
| 139 | return sp; |
| 140 | } |
| 141 | |
| 142 | Symbol * |
| 143 | getsym(Symbol *s) |
| 144 | { Symbol *n = (Symbol *) tl_emalloc(sizeof(Symbol)); |
| 145 | |
| 146 | n->name = s->name; |
| 147 | return n; |
| 148 | } |