trunk/verif/Spin/Src5.1.6/tl_lex.c

   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 }