Subversion Repositories planix.SVN

Rev

Details | Last modification | View Log | RSS feed

Rev Author Line No. Line
2 - 1 
/***** tl_spin: tl_parse.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 "tl.h"
16 
 
17 
extern int	tl_yylex(void);
18 
extern int	tl_verbose, tl_errs;
19 
 
20 
int	tl_yychar = 0;
21 
YYSTYPE	tl_yylval;
22 
 
23 
static Node	*tl_formula(void);
24 
static Node	*tl_factor(void);
25 
static Node	*tl_level(int);
26 
 
27 
static int	prec[2][4] = {
28 
	{ U_OPER,  V_OPER, 0, 0 },	/* left associative */
29 
	{ OR, AND, IMPLIES, EQUIV, },	/* left associative */
30 
};
31 
 
32 
static Node *
33 
tl_factor(void)
34 
{	Node *ptr = ZN;
35 
 
36 
	switch (tl_yychar) {
37 
	case '(':
38 
		ptr = tl_formula();
39 
		if (tl_yychar != ')')
40 
			tl_yyerror("expected ')'");
41 
		tl_yychar = tl_yylex();
42 
		break;
43 
	case NOT:
44 
		ptr = tl_yylval;
45 
		tl_yychar = tl_yylex();
46 
		ptr->lft = tl_factor();
47 
		ptr = push_negation(ptr);
48 
		break;
49 
	case ALWAYS:
50 
		tl_yychar = tl_yylex();
51 
		ptr = tl_factor();
52 
#ifndef NO_OPT
53 
		if (ptr->ntyp == FALSE
54 
		||  ptr->ntyp == TRUE)
55 
			break;	/* [] false == false */
56 
 
57 
		if (ptr->ntyp == V_OPER)
58 
		{	if (ptr->lft->ntyp == FALSE)
59 
				break;	/* [][]p = []p */
60 
 
61 
			ptr = ptr->rgt;	/* [] (p V q) = [] q */
62 
		}
63 
#endif
64 
		ptr = tl_nn(V_OPER, False, ptr);
65 
		break;
66 
#ifdef NXT
67 
	case NEXT:
68 
		tl_yychar = tl_yylex();
69 
		ptr = tl_factor();
70 
		if (ptr->ntyp == TRUE)
71 
			break;	/* X true = true */
72 
		ptr = tl_nn(NEXT, ptr, ZN);
73 
		break;
74 
#endif
75 
	case EVENTUALLY:
76 
		tl_yychar = tl_yylex();
77 
 
78 
		ptr = tl_factor();
79 
#ifndef NO_OPT
80 
		if (ptr->ntyp == TRUE
81 
		||  ptr->ntyp == FALSE)
82 
			break;	/* <> true == true */
83 
 
84 
		if (ptr->ntyp == U_OPER
85 
		&&  ptr->lft->ntyp == TRUE)
86 
			break;	/* <><>p = <>p */
87 
 
88 
		if (ptr->ntyp == U_OPER)
89 
		{	/* <> (p U q) = <> q */
90 
			ptr = ptr->rgt;
91 
			/* fall thru */
92 
		}
93 
#endif
94 
		ptr = tl_nn(U_OPER, True, ptr);
95 
 
96 
		break;
97 
	case PREDICATE:
98 
		ptr = tl_yylval;
99 
		tl_yychar = tl_yylex();
100 
		break;
101 
	case TRUE:
102 
	case FALSE:
103 
		ptr = tl_yylval;
104 
		tl_yychar = tl_yylex();
105 
		break;
106 
	}
107 
	if (!ptr) tl_yyerror("expected predicate");
108 
#if 0
109 
	printf("factor:	");
110 
	tl_explain(ptr->ntyp);
111 
	printf("\n");
112 
#endif
113 
	return ptr;
114 
}
115 
 
116 
static Node *
117 
bin_simpler(Node *ptr)
118 
{	Node *a, *b;
119 
 
120 
	if (ptr)
121 
	switch (ptr->ntyp) {
122 
	case U_OPER:
123 
#ifndef NO_OPT
124 
		if (ptr->rgt->ntyp == TRUE
125 
		||  ptr->rgt->ntyp == FALSE
126 
		||  ptr->lft->ntyp == FALSE)
127 
		{	ptr = ptr->rgt;
128 
			break;
129 
		}
130 
		if (isequal(ptr->lft, ptr->rgt))
131 
		{	/* p U p = p */
132 
			ptr = ptr->rgt;
133 
			break;
134 
		}
135 
		if (ptr->lft->ntyp == U_OPER
136 
		&&  isequal(ptr->lft->lft, ptr->rgt))
137 
		{	/* (p U q) U p = (q U p) */
138 
			ptr->lft = ptr->lft->rgt;
139 
			break;
140 
		}
141 
		if (ptr->rgt->ntyp == U_OPER
142 
		&&  ptr->rgt->lft->ntyp == TRUE)
143 
		{	/* p U (T U q)  = (T U q) */
144 
			ptr = ptr->rgt;
145 
			break;
146 
		}
147 
#ifdef NXT
148 
		/* X p U X q == X (p U q) */
149 
		if (ptr->rgt->ntyp == NEXT
150 
		&&  ptr->lft->ntyp == NEXT)
151 
		{	ptr = tl_nn(NEXT,
152 
				tl_nn(U_OPER,
153 
					ptr->lft->lft,
154 
					ptr->rgt->lft), ZN);
155 
		}
156 
#endif
157 
#endif
158 
		break;
159 
	case V_OPER:
160 
#ifndef NO_OPT
161 
		if (ptr->rgt->ntyp == FALSE
162 
		||  ptr->rgt->ntyp == TRUE
163 
		||  ptr->lft->ntyp == TRUE)
164 
		{	ptr = ptr->rgt;
165 
			break;
166 
		}
167 
		if (isequal(ptr->lft, ptr->rgt))
168 
		{	/* p V p = p */
169 
			ptr = ptr->rgt;
170 
			break;
171 
		}
172 
		/* F V (p V q) == F V q */
173 
		if (ptr->lft->ntyp == FALSE
174 
		&&  ptr->rgt->ntyp == V_OPER)
175 
		{	ptr->rgt = ptr->rgt->rgt;
176 
			break;
177 
		}
178 
		/* p V (F V q) == F V q */
179 
		if (ptr->rgt->ntyp == V_OPER
180 
		&&  ptr->rgt->lft->ntyp == FALSE)
181 
		{	ptr->lft = False;
182 
			ptr->rgt = ptr->rgt->rgt;
183 
			break;
184 
		}
185 
#endif
186 
		break;
187 
	case IMPLIES:
188 
#ifndef NO_OPT
189 
		if (isequal(ptr->lft, ptr->rgt))
190 
		{	ptr = True;
191 
			break;
192 
		}
193 
#endif
194 
		ptr = tl_nn(OR, Not(ptr->lft), ptr->rgt);
195 
		ptr = rewrite(ptr);
196 
		break;
197 
	case EQUIV:
198 
#ifndef NO_OPT
199 
		if (isequal(ptr->lft, ptr->rgt))
200 
		{	ptr = True;
201 
			break;
202 
		}
203 
#endif
204 
		a = rewrite(tl_nn(AND,
205 
			dupnode(ptr->lft),
206 
			dupnode(ptr->rgt)));
207 
		b = rewrite(tl_nn(AND,
208 
			Not(ptr->lft),
209 
			Not(ptr->rgt)));
210 
		ptr = tl_nn(OR, a, b);
211 
		ptr = rewrite(ptr);
212 
		break;
213 
	case AND:
214 
#ifndef NO_OPT
215 
		/* p && (q U p) = p */
216 
		if (ptr->rgt->ntyp == U_OPER
217 
		&&  isequal(ptr->rgt->rgt, ptr->lft))
218 
		{	ptr = ptr->lft;
219 
			break;
220 
		}
221 
		if (ptr->lft->ntyp == U_OPER
222 
		&&  isequal(ptr->lft->rgt, ptr->rgt))
223 
		{	ptr = ptr->rgt;
224 
			break;
225 
		}
226 
 
227 
		/* p && (q V p) == q V p */
228 
		if (ptr->rgt->ntyp == V_OPER
229 
		&&  isequal(ptr->rgt->rgt, ptr->lft))
230 
		{	ptr = ptr->rgt;
231 
			break;
232 
		}
233 
		if (ptr->lft->ntyp == V_OPER
234 
		&&  isequal(ptr->lft->rgt, ptr->rgt))
235 
		{	ptr = ptr->lft;
236 
			break;
237 
		}
238 
 
239 
		/* (p U q) && (r U q) = (p && r) U q*/
240 
		if (ptr->rgt->ntyp == U_OPER
241 
		&&  ptr->lft->ntyp == U_OPER
242 
		&&  isequal(ptr->rgt->rgt, ptr->lft->rgt))
243 
		{	ptr = tl_nn(U_OPER,
244 
				tl_nn(AND, ptr->lft->lft, ptr->rgt->lft),
245 
				ptr->lft->rgt);
246 
			break;
247 
		}
248 
 
249 
		/* (p V q) && (p V r) = p V (q && r) */
250 
		if (ptr->rgt->ntyp == V_OPER
251 
		&&  ptr->lft->ntyp == V_OPER
252 
		&&  isequal(ptr->rgt->lft, ptr->lft->lft))
253 
		{	ptr = tl_nn(V_OPER,
254 
				ptr->rgt->lft,
255 
				tl_nn(AND, ptr->lft->rgt, ptr->rgt->rgt));
256 
			break;
257 
		}
258 
#ifdef NXT
259 
		/* X p && X q == X (p && q) */
260 
		if (ptr->rgt->ntyp == NEXT
261 
		&&  ptr->lft->ntyp == NEXT)
262 
		{	ptr = tl_nn(NEXT,
263 
				tl_nn(AND,
264 
					ptr->rgt->lft,
265 
					ptr->lft->lft), ZN);
266 
			break;
267 
		}
268 
#endif
269 
 
270 
		if (isequal(ptr->lft, ptr->rgt)	/* (p && p) == p */
271 
		||  ptr->rgt->ntyp == FALSE	/* (p && F) == F */
272 
		||  ptr->lft->ntyp == TRUE)	/* (T && p) == p */
273 
		{	ptr = ptr->rgt;
274 
			break;
275 
		}
276 
		if (ptr->rgt->ntyp == TRUE	/* (p && T) == p */
277 
		||  ptr->lft->ntyp == FALSE)	/* (F && p) == F */
278 
		{	ptr = ptr->lft;
279 
			break;
280 
		}
281 
 
282 
		/* (p V q) && (r U q) == p V q */
283 
		if (ptr->rgt->ntyp == U_OPER
284 
		&&  ptr->lft->ntyp == V_OPER
285 
		&&  isequal(ptr->lft->rgt, ptr->rgt->rgt))
286 
		{	ptr = ptr->lft;
287 
			break;
288 
		}
289 
#endif
290 
		break;
291 
 
292 
	case OR:
293 
#ifndef NO_OPT
294 
		/* p || (q U p) == q U p */
295 
		if (ptr->rgt->ntyp == U_OPER
296 
		&&  isequal(ptr->rgt->rgt, ptr->lft))
297 
		{	ptr = ptr->rgt;
298 
			break;
299 
		}
300 
 
301 
		/* p || (q V p) == p */
302 
		if (ptr->rgt->ntyp == V_OPER
303 
		&&  isequal(ptr->rgt->rgt, ptr->lft))
304 
		{	ptr = ptr->lft;
305 
			break;
306 
		}
307 
 
308 
		/* (p U q) || (p U r) = p U (q || r) */
309 
		if (ptr->rgt->ntyp == U_OPER
310 
		&&  ptr->lft->ntyp == U_OPER
311 
		&&  isequal(ptr->rgt->lft, ptr->lft->lft))
312 
		{	ptr = tl_nn(U_OPER,
313 
				ptr->rgt->lft,
314 
				tl_nn(OR, ptr->lft->rgt, ptr->rgt->rgt));
315 
			break;
316 
		}
317 
 
318 
		if (isequal(ptr->lft, ptr->rgt)	/* (p || p) == p */
319 
		||  ptr->rgt->ntyp == FALSE	/* (p || F) == p */
320 
		||  ptr->lft->ntyp == TRUE)	/* (T || p) == T */
321 
		{	ptr = ptr->lft;
322 
			break;
323 
		}
324 
		if (ptr->rgt->ntyp == TRUE	/* (p || T) == T */
325 
		||  ptr->lft->ntyp == FALSE)	/* (F || p) == p */
326 
		{	ptr = ptr->rgt;
327 
			break;
328 
		}
329 
 
330 
		/* (p V q) || (r V q) = (p || r) V q */
331 
		if (ptr->rgt->ntyp == V_OPER
332 
		&&  ptr->lft->ntyp == V_OPER
333 
		&&  isequal(ptr->lft->rgt, ptr->rgt->rgt))
334 
		{	ptr = tl_nn(V_OPER,
335 
				tl_nn(OR, ptr->lft->lft, ptr->rgt->lft),
336 
				ptr->rgt->rgt);
337 
			break;
338 
		}
339 
 
340 
		/* (p V q) || (r U q) == r U q */
341 
		if (ptr->rgt->ntyp == U_OPER
342 
		&&  ptr->lft->ntyp == V_OPER
343 
		&&  isequal(ptr->lft->rgt, ptr->rgt->rgt))
344 
		{	ptr = ptr->rgt;
345 
			break;
346 
		}
347 
#endif
348 
		break;
349 
	}
350 
	return ptr;
351 
}
352 
 
353 
static Node *
354 
tl_level(int nr)
355 
{	int i; Node *ptr = ZN;
356 
 
357 
	if (nr < 0)
358 
		return tl_factor();
359 
 
360 
	ptr = tl_level(nr-1);
361 
again:
362 
	for (i = 0; i < 4; i++)
363 
		if (tl_yychar == prec[nr][i])
364 
		{	tl_yychar = tl_yylex();
365 
			ptr = tl_nn(prec[nr][i],
366 
				ptr, tl_level(nr-1));
367 
			ptr = bin_simpler(ptr);
368 
			goto again;
369 
		}
370 
	if (!ptr) tl_yyerror("syntax error");
371 
#if 0
372 
	printf("level %d:	", nr);
373 
	tl_explain(ptr->ntyp);
374 
	printf("\n");
375 
#endif
376 
	return ptr;
377 
}
378 
 
379 
static Node *
380 
tl_formula(void)
381 
{	tl_yychar = tl_yylex();
382 
	return tl_level(1);	/* 2 precedence levels, 1 and 0 */
383 
}
384 
 
385 
void
386 
tl_parse(void)
387 
{	Node *n;
388 
 
389 
	/* tl_verbose = 1; */
390 
	n = tl_formula();
391 
	if (tl_verbose)
392 
	{	printf("formula: ");
393 
		dump(n);
394 
		printf("\n");
395 
	}
396 
	if (tl_Getchar() != -1)
397 
	{	tl_yyerror("syntax error");
398 
		tl_errs++;
399 
		return;
400 
	}
401 
	trans(n);
402 
}