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