0b55f123 |
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 | } |