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