1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
/***** tl_spin: tl_lex.c *****/
/* Copyright (c) 1995-2003 by Lucent Technologies, Bell Laboratories. */
/* All Rights Reserved. This software is for educational purposes only. */
/* No guarantee whatsoever is expressed or implied by the distribution of */
/* this code. Permission is given to distribute this code provided that */
/* this introductory message is not removed and no monies are exchanged. */
/* Software written by Gerard J. Holzmann. For tool documentation see: */
/* http://spinroot.com/ */
/* Send all bug-reports and/or questions to: bugs@spinroot.com */
/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
#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
tl_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
tl_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))
{ tl_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 = tl_follow('\\', AND, '/'); break;
case '\\': c = tl_follow('/', OR, '\\'); break;
case '&' : c = tl_follow('&', AND, '&'); break;
case '|' : c = tl_follow('|', OR, '|'); break;
case '[' : c = tl_follow(']', ALWAYS, '['); break;
case '-' : c = tl_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((int) 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;
}
|
