1 /***** tl_spin: tl_lex.c *****/
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 */
12 /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
13 /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
19 static Symbol
*symtab
[Nhash
+1];
20 static int tl_lex(void);
22 extern YYSTYPE tl_yylval
;
25 #define Token(y) tl_yylval = tl_nn(y,ZN,ZN); return y
28 tl_getword(int first
, int (*tst
)(int))
31 yytext
[i
++] = (char ) first
;
32 while (tst(c
= tl_Getchar()))
39 tl_follow(int tok
, int ifyes
, int ifno
)
44 if ((c
= tl_Getchar()) == tok
)
48 sprintf(buf
, "expected '%c'", tok
);
49 tl_yyerror(buf
); /* no return from here */
57 printf("c = %d\n", c
);
68 yytext
[0] = (char ) c
;
75 } while (c
== ' '); /* '\t' is removed in tl_main.c */
78 { tl_getword(c
, isalnum_
);
79 if (strcmp("true", yytext
) == 0)
82 if (strcmp("false", yytext
) == 0)
85 tl_yylval
= tl_nn(PREDICATE
,ZN
,ZN
);
86 tl_yylval
->sym
= tl_lookup(yytext
);
96 tl_yyerror("expected '<>' or '<->'");
103 tl_yyerror("expected '<->'");
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;
117 case 'X' : c
= NEXT
; break;
129 for (sp
= symtab
[h
]; sp
; sp
= sp
->next
)
130 if (strcmp(sp
->name
, s
) == 0)
133 sp
= (Symbol
*) tl_emalloc(sizeof(Symbol
));
134 sp
->name
= (char *) tl_emalloc((int) strlen(s
) + 1);
136 sp
->next
= symtab
[h
];
144 { Symbol
*n
= (Symbol
*) tl_emalloc(sizeof(Symbol
));
This page took 0.048549 seconds and 4 git commands to generate.