/***** 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 int tl_peek(int);
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 = %c (%d)\n", c, c);
#endif
return c;
}
static int
is_predicate(int z)
{ char c, c_prev = z;
char want = (z == '{') ? '}' : ')';
int i = 0, j, nesting = 0;
char peek_buf[512];
c = tl_peek(i++); /* look ahead without changing position */
while ((c != want || nesting > 0) && c != -1 && i < 2047)
{ if (islower((int) c))
{ peek_buf[0] = c;
j = 1;
while (j < (int) sizeof(peek_buf) && isalnum((int)(c = tl_peek(i))))
{ peek_buf[j++] = c;
i++;
}
c = 0; /* make sure we don't match on z or want on the peekahead */
if (j >= (int) sizeof(peek_buf))
{ peek_buf[j-1] = '\0';
fatal("name '%s' in ltl formula too long", peek_buf);
}
peek_buf[j] = '\0';
if (strcmp(peek_buf, "always") == 0
|| strcmp(peek_buf, "eventually") == 0
|| strcmp(peek_buf, "until") == 0
|| strcmp(peek_buf, "next") == 0)
{ return 0;
}
} else
{ char c_nxt = tl_peek(i);
if (((c == 'U' || c == 'V' || c == 'X') && !isalnum_(c_prev) && !isalnum_(c_nxt))
|| (c == '<' && c_nxt == '>')
|| (c == '[' && c_nxt == ']'))
{ return 0;
} }
if (c == z)
{ nesting++;
}
if (c == want)
{ nesting--;
}
c_prev = c;
c = tl_peek(i++);
}
return 1;
}
static void
read_upto_closing(int z)
{ char c, want = (z == '{') ? '}' : ')';
int i = 0, nesting = 0;
c = tl_Getchar();
while ((c != want || nesting > 0) && c != -1 && i < 2047) /* yytext is 2048 */
{ yytext[i++] = c;
if (c == z)
{ nesting++;
}
if (c == want)
{ nesting--;
}
c = tl_Getchar();
}
yytext[i] = '\0';
}
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 (c == '{' || c == '(') /* new 6.0.0 */
{ if (is_predicate(c))
{ read_upto_closing(c);
tl_yylval = tl_nn(PREDICATE,ZN,ZN);
tl_yylval->sym = tl_lookup(yytext);
return PREDICATE;
} }
if (c == '}')
{ tl_yyerror("unexpected '}'");
}
if (islower(c))
{ tl_getword(c, isalnum_);
if (strcmp("true", yytext) == 0)
{ Token(TRUE);
}
if (strcmp("false", yytext) == 0)
{ Token(FALSE);
}
if (strcmp("always", yytext) == 0)
{ Token(ALWAYS);
}
if (strcmp("eventually", yytext) == 0)
{ Token(EVENTUALLY);
}
if (strcmp("until", yytext) == 0)
{ Token(U_OPER);
}
#ifdef NXT
if (strcmp("next", yytext) == 0)
{ Token(NEXT);
}
#endif
if (strcmp("not", yytext) == 0)
{ Token(NOT);
}
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;
}
|