1 /***** ltl2ba : lex.c *****/
2
3 /* Written by Denis Oddoux, LIAFA, France */
4 /* Copyright (c) 2001 Denis Oddoux */
5 /* Modified by Paul Gastin, LSV, France */
6 /* Copyright (c) 2007 Paul Gastin */
7 /* */
8 /* This program is free software; you can redistribute it and/or modify */
9 /* it under the terms of the GNU General Public License as published by */
10 /* the Free Software Foundation; either version 2 of the License, or */
11 /* (at your option) any later version. */
12 /* */
13 /* This program is distributed in the hope that it will be useful, */
14 /* but WITHOUT ANY WARRANTY; without even the implied warranty of */
15 /* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
16 /* GNU General Public License for more details. */
17 /* */
18 /* You should have received a copy of the GNU General Public License */
19 /* along with this program; if not, write to the Free Software */
20 /* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/
21 /* */
22 /* Based on the translation algorithm by Gastin and Oddoux, */
23 /* presented at the 13th International Conference on Computer Aided */
24 /* Verification, CAV 2001, Paris, France. */
25 /* Proceedings - LNCS 2102, pp. 53-65 */
26 /* */
27 /* Send bug-reports and/or questions to Paul Gastin */
28 /* http://www.lsv.ens-cachan.fr/~gastin */
29 /* */
30 /* Some of the code in this file was taken from the Spin software */
31 /* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */
32
33 #include <stdlib.h>
34 #include <ctype.h>
35 #include "ltl2ba.h"
36
37 static Symbol *symtab[Nhash+1];
38 static int tl_lex(void);
39
40 extern YYSTYPE tl_yylval;
41 char yytext[2048];
42
43 #define Token(y) tl_yylval = tl_nn(y,ZN,ZN); return y
44
45 int
isalnum_(int c)46 isalnum_(int c)
47 { return (isalnum(c) || c == '_');
48 }
49
50 int
hash(char * s)51 hash(char *s)
52 { int h=0;
53
54 while (*s)
55 { h += *s++;
56 h <<= 1;
57 if (h&(Nhash+1))
58 h |= 1;
59 }
60 return h&Nhash;
61 }
62
63 static void
getword(int first,int (* tst)(int))64 getword(int first, int (*tst)(int))
65 { int i=0; char c;
66
67 yytext[i++]= (char ) first;
68 while (tst(c = tl_Getchar()))
69 yytext[i++] = c;
70 yytext[i] = '\0';
71 tl_UnGetchar();
72 }
73
74 static int
follow(int tok,int ifyes,int ifno)75 follow(int tok, int ifyes, int ifno)
76 { int c;
77 char buf[32];
78 extern int tl_yychar;
79
80 if ((c = tl_Getchar()) == tok)
81 return ifyes;
82 tl_UnGetchar();
83 tl_yychar = c;
84 sprintf(buf, "expected '%c'", tok);
85 tl_yyerror(buf); /* no return from here */
86 return ifno;
87 }
88
89 int
tl_yylex(void)90 tl_yylex(void)
91 { int c = tl_lex();
92 #if 0
93 printf("c = %d\n", c);
94 #endif
95 return c;
96 }
97
98 static int
tl_lex(void)99 tl_lex(void)
100 { int c;
101
102 do {
103 c = tl_Getchar();
104 yytext[0] = (char ) c;
105 yytext[1] = '\0';
106
107 if (c <= 0)
108 { Token(';');
109 }
110
111 } while (c == ' '); /* '\t' is removed in tl_main.c */
112
113 if (islower(c))
114 { getword(c, isalnum_);
115 if (strcmp("true", yytext) == 0)
116 { Token(TRUE);
117 }
118 if (strcmp("false", yytext) == 0)
119 { Token(FALSE);
120 }
121 tl_yylval = tl_nn(PREDICATE,ZN,ZN);
122 tl_yylval->sym = tl_lookup(yytext);
123 return PREDICATE;
124 }
125 if (c == '<')
126 { c = tl_Getchar();
127 if (c == '>')
128 { Token(EVENTUALLY);
129 }
130 if (c != '-')
131 { tl_UnGetchar();
132 tl_yyerror("expected '<>' or '<->'");
133 }
134 c = tl_Getchar();
135 if (c == '>')
136 { Token(EQUIV);
137 }
138 tl_UnGetchar();
139 tl_yyerror("expected '<->'");
140 }
141 if (c == 'N')
142 { c = tl_Getchar();
143 if (c != 'O')
144 { tl_UnGetchar();
145 tl_yyerror("expected 'NOT'");
146 }
147 c = tl_Getchar();
148 if (c == 'T')
149 { Token(NOT);
150 }
151 tl_UnGetchar();
152 tl_yyerror("expected 'NOT'");
153 }
154
155 switch (c) {
156 case '/' : c = follow('\\', AND, '/'); break;
157 case '\\': c = follow('/', OR, '\\'); break;
158 case '&' : c = follow('&', AND, '&'); break;
159 case '|' : c = follow('|', OR, '|'); break;
160 case '[' : c = follow(']', ALWAYS, '['); break;
161 case '-' : c = follow('>', IMPLIES, '-'); break;
162 case '!' : c = NOT; break;
163 case 'U' : c = U_OPER; break;
164 case 'V' : c = V_OPER; break;
165 #ifdef NXT
166 case 'X' : c = NEXT; break;
167 #endif
168 default : break;
169 }
170 Token(c);
171 }
172
173 Symbol *
tl_lookup(char * s)174 tl_lookup(char *s)
175 { Symbol *sp;
176 int h = hash(s);
177
178 for (sp = symtab[h]; sp; sp = sp->next)
179 if (strcmp(sp->name, s) == 0)
180 return sp;
181
182 sp = (Symbol *) tl_emalloc(sizeof(Symbol));
183 sp->name = (char *) tl_emalloc(strlen(s) + 1);
184 strcpy(sp->name, s);
185 sp->next = symtab[h];
186 symtab[h] = sp;
187
188 return sp;
189 }
190
191 Symbol *
getsym(Symbol * s)192 getsym(Symbol *s)
193 { Symbol *n = (Symbol *) tl_emalloc(sizeof(Symbol));
194
195 n->name = s->name;
196 return n;
197 }
198