[lttv.git] / trunk / verif / Spin / Src5.1.6 / tl_lex.c

/***** 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 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 = %d\n", c);
#endif
	return c;
}

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 (islower(c))
	{	tl_getword(c, isalnum_);
		if (strcmp("true", yytext) == 0)
		{	Token(TRUE);
		}
		if (strcmp("false", yytext) == 0)
		{	Token(FALSE);
		}
		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;
}
Commit	Line	Data
0b55f123	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	}