Subversion Repositories planix.SVN

/***** 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;
}