123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254 |
- /*
- * This file is part of the UCB release of Plan 9. It is subject to the license
- * terms in the LICENSE file found in the top-level directory of this
- * distribution and at http://akaros.cs.berkeley.edu/files/Plan9License. No
- * part of the UCB release of Plan 9, including this file, may be copied,
- * modified, propagated, or distributed except according to the terms contained
- * in the LICENSE file.
- */
- /***** 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;
- }
|