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 extern int tl_peek(int);
22
23 extern YYSTYPE tl_yylval;
24 extern char yytext[];
25
26 #define Token(y) tl_yylval = tl_nn(y,ZN,ZN); return y
27
28 static void
tl_getword(int first,int (* tst)(int))29 tl_getword(int first, int (*tst)(int))
30 { int i=0; char c;
31
32 yytext[i++] = (char ) first;
33 while (tst(c = tl_Getchar()))
34 yytext[i++] = c;
35 yytext[i] = '\0';
36 tl_UnGetchar();
37 }
38
39 static int
tl_follow(int tok,int ifyes,int ifno)40 tl_follow(int tok, int ifyes, int ifno)
41 { int c;
42 char buf[32];
43 extern int tl_yychar;
44
45 if ((c = tl_Getchar()) == tok)
46 return ifyes;
47 tl_UnGetchar();
48 tl_yychar = c;
49 sprintf(buf, "expected '%c'", tok);
50 tl_yyerror(buf); /* no return from here */
51 return ifno;
52 }
53
54 int
tl_yylex(void)55 tl_yylex(void)
56 { int c = tl_lex();
57 #if 0
58 printf("c = %c (%d)\n", c, c);
59 #endif
60 return c;
61 }
62
63 static int
is_predicate(int z)64 is_predicate(int z)
65 { char c, c_prev = z;
66 char want = (z == '{') ? '}' : ')';
67 int i = 0, j, nesting = 0;
68 char peek_buf[512];
69
70 c = tl_peek(i++); /* look ahead without changing position */
71 while ((c != want || nesting > 0) && c != -1 && i < 2047)
72 { if (islower((int) c))
73 { peek_buf[0] = c;
74 j = 1;
75 while (j < (int) sizeof(peek_buf) && isalnum((int)(c = tl_peek(i))))
76 { peek_buf[j++] = c;
77 i++;
78 }
79 c = 0; /* make sure we don't match on z or want on the peekahead */
80 if (j >= (int) sizeof(peek_buf))
81 { peek_buf[j-1] = '\0';
82 fatal("name '%s' in ltl formula too long", peek_buf);
83 }
84 peek_buf[j] = '\0';
85 if (strcmp(peek_buf, "always") == 0
86 || strcmp(peek_buf, "eventually") == 0
87 || strcmp(peek_buf, "until") == 0
88 || strcmp(peek_buf, "next") == 0)
89 { return 0;
90 }
91 } else
92 { char c_nxt = tl_peek(i);
93 if (((c == 'U' || c == 'V' || c == 'X') && !isalnum_(c_prev) && !isalnum_(c_nxt))
94 || (c == '<' && c_nxt == '>')
95 || (c == '[' && c_nxt == ']'))
96 { return 0;
97 } }
98
99 if (c == z)
100 { nesting++;
101 }
102 if (c == want)
103 { nesting--;
104 }
105 c_prev = c;
106 c = tl_peek(i++);
107 }
108 return 1;
109 }
110
111 static void
read_upto_closing(int z)112 read_upto_closing(int z)
113 { char c, want = (z == '{') ? '}' : ')';
114 int i = 0, nesting = 0;
115
116 c = tl_Getchar();
117 while ((c != want || nesting > 0) && c != -1 && i < 2047) /* yytext is 2048 */
118 { yytext[i++] = c;
119 if (c == z)
120 { nesting++;
121 }
122 if (c == want)
123 { nesting--;
124 }
125 c = tl_Getchar();
126 }
127 yytext[i] = '\0';
128 }
129
130 static int
tl_lex(void)131 tl_lex(void)
132 { int c;
133
134 do {
135 c = tl_Getchar();
136 yytext[0] = (char ) c;
137 yytext[1] = '\0';
138
139 if (c <= 0)
140 { Token(';');
141 }
142
143 } while (c == ' '); /* '\t' is removed in tl_main.c */
144
145 if (c == '{' || c == '(') /* new 6.0.0 */
146 { if (is_predicate(c))
147 { read_upto_closing(c);
148 tl_yylval = tl_nn(PREDICATE,ZN,ZN);
149 tl_yylval->sym = tl_lookup(yytext);
150 return PREDICATE;
151 } }
152
153 if (c == '}')
154 { tl_yyerror("unexpected '}'");
155 }
156 if (islower(c))
157 { tl_getword(c, isalnum_);
158 if (strcmp("true", yytext) == 0)
159 { Token(TRUE);
160 }
161 if (strcmp("false", yytext) == 0)
162 { Token(FALSE);
163 }
164 if (strcmp("always", yytext) == 0)
165 { Token(ALWAYS);
166 }
167 if (strcmp("eventually", yytext) == 0)
168 { Token(EVENTUALLY);
169 }
170 if (strcmp("until", yytext) == 0)
171 { Token(U_OPER);
172 }
173 #ifdef NXT
174 if (strcmp("next", yytext) == 0)
175 { Token(NEXT);
176 }
177 #endif
178 if (strcmp("not", yytext) == 0)
179 { Token(NOT);
180 }
181 tl_yylval = tl_nn(PREDICATE,ZN,ZN);
182 tl_yylval->sym = tl_lookup(yytext);
183 return PREDICATE;
184 }
185
186 if (c == '<')
187 { c = tl_Getchar();
188 if (c == '>')
189 { Token(EVENTUALLY);
190 }
191 if (c != '-')
192 { tl_UnGetchar();
193 tl_yyerror("expected '<>' or '<->'");
194 }
195 c = tl_Getchar();
196 if (c == '>')
197 { Token(EQUIV);
198 }
199 tl_UnGetchar();
200 tl_yyerror("expected '<->'");
201 }
202
203 switch (c) {
204 case '/' : c = tl_follow('\\', AND, '/'); break;
205 case '\\': c = tl_follow('/', OR, '\\'); break;
206 case '&' : c = tl_follow('&', AND, '&'); break;
207 case '|' : c = tl_follow('|', OR, '|'); break;
208 case '[' : c = tl_follow(']', ALWAYS, '['); break;
209 case '-' : c = tl_follow('>', IMPLIES, '-'); break;
210 case '!' : c = NOT; break;
211 case 'U' : c = U_OPER; break;
212 case 'V' : c = V_OPER; break;
213 #ifdef NXT
214 case 'X' : c = NEXT; break;
215 #endif
216 default : break;
217 }
218 Token(c);
219 }
220
221 Symbol *
tl_lookup(char * s)222 tl_lookup(char *s)
223 { Symbol *sp;
224 int h = hash(s);
225
226 for (sp = symtab[h]; sp; sp = sp->next)
227 if (strcmp(sp->name, s) == 0)
228 return sp;
229
230 sp = (Symbol *) tl_emalloc(sizeof(Symbol));
231 sp->name = (char *) tl_emalloc((int) strlen(s) + 1);
232 strcpy(sp->name, s);
233 sp->next = symtab[h];
234 symtab[h] = sp;
235
236 return sp;
237 }
238
239 Symbol *
getsym(Symbol * s)240 getsym(Symbol *s)
241 { Symbol *n = (Symbol *) tl_emalloc(sizeof(Symbol));
242
243 n->name = s->name;
244 return n;
245 }
246