1 /***** tl_spin: tl_parse.c *****/
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
8 * Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
9 * presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
14 extern int tl_yylex(void);
15 extern int tl_verbose, tl_errs;
20 static Node *tl_formula(void);
21 static Node *tl_factor(void);
22 static Node *tl_level(int);
24 static int prec[2][4] = {
25 { U_OPER, V_OPER, 0, 0 }, /* left associative */
26 { OR, AND, IMPLIES, EQUIV, }, /* left associative */
37 tl_yyerror("expected ')'");
38 tl_yychar = tl_yylex();
42 tl_yychar = tl_yylex();
43 ptr->lft = tl_factor();
45 { fatal("malformed expression", (char *) 0);
47 ptr = push_negation(ptr);
50 tl_yychar = tl_yylex();
53 if (ptr->ntyp == FALSE
55 break; /* [] false == false */
57 if (ptr->ntyp == V_OPER)
58 { if (ptr->lft->ntyp == FALSE)
59 break; /* [][]p = []p */
61 ptr = ptr->rgt; /* [] (p V q) = [] q */
64 ptr = tl_nn(V_OPER, False, ptr);
68 tl_yychar = tl_yylex();
70 if (ptr->ntyp == TRUE)
71 break; /* X true = true */
72 ptr = tl_nn(NEXT, ptr, ZN);
76 tl_yychar = tl_yylex();
78 if (ptr->ntyp != PREDICATE)
79 { tl_yyerror("expected {...} after c_expr");
81 ptr = tl_nn(CEXPR, ptr, ZN);
84 tl_yychar = tl_yylex();
89 || ptr->ntyp == FALSE)
90 break; /* <> true == true */
92 if (ptr->ntyp == U_OPER
93 && ptr->lft->ntyp == TRUE)
94 break; /* <><>p = <>p */
96 if (ptr->ntyp == U_OPER)
97 { /* <> (p U q) = <> q */
102 ptr = tl_nn(U_OPER, True, ptr);
107 tl_yychar = tl_yylex();
112 tl_yychar = tl_yylex();
115 if (!ptr) tl_yyerror("expected predicate");
118 tl_explain(ptr->ntyp);
125 bin_simpler(Node *ptr)
132 if (ptr->rgt->ntyp == TRUE
133 || ptr->rgt->ntyp == FALSE
134 || ptr->lft->ntyp == FALSE)
138 if (isequal(ptr->lft, ptr->rgt))
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;
149 if (ptr->rgt->ntyp == U_OPER
150 && ptr->rgt->lft->ntyp == TRUE)
151 { /* p U (T U q) = (T U q) */
156 /* X p U X q == X (p U q) */
157 if (ptr->rgt->ntyp == NEXT
158 && ptr->lft->ntyp == NEXT)
169 if (ptr->rgt->ntyp == FALSE
170 || ptr->rgt->ntyp == TRUE
171 || ptr->lft->ntyp == TRUE)
175 if (isequal(ptr->lft, ptr->rgt))
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;
186 /* p V (F V q) == F V q */
187 if (ptr->rgt->ntyp == V_OPER
188 && ptr->rgt->lft->ntyp == FALSE)
190 ptr->rgt = ptr->rgt->rgt;
197 if (isequal(ptr->lft, ptr->rgt))
202 ptr = tl_nn(OR, Not(ptr->lft), ptr->rgt);
207 if (isequal(ptr->lft, ptr->rgt))
212 a = rewrite(tl_nn(AND,
215 b = rewrite(tl_nn(AND,
218 ptr = tl_nn(OR, a, b);
223 /* p && (q U p) = p */
224 if (ptr->rgt->ntyp == U_OPER
225 && isequal(ptr->rgt->rgt, ptr->lft))
229 if (ptr->lft->ntyp == U_OPER
230 && isequal(ptr->lft->rgt, ptr->rgt))
235 /* p && (q V p) == q V p */
236 if (ptr->rgt->ntyp == V_OPER
237 && isequal(ptr->rgt->rgt, ptr->lft))
241 if (ptr->lft->ntyp == V_OPER
242 && isequal(ptr->lft->rgt, ptr->rgt))
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),
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,
263 tl_nn(AND, ptr->lft->rgt, ptr->rgt->rgt));
267 /* X p && X q == X (p && q) */
268 if (ptr->rgt->ntyp == NEXT
269 && ptr->lft->ntyp == NEXT)
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 */
284 if (ptr->rgt->ntyp == TRUE /* (p && T) == p */
285 || ptr->lft->ntyp == FALSE) /* (F && p) == F */
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))
302 /* p || (q U p) == q U p */
303 if (ptr->rgt->ntyp == U_OPER
304 && isequal(ptr->rgt->rgt, ptr->lft))
309 /* p || (q V p) == p */
310 if (ptr->rgt->ntyp == V_OPER
311 && isequal(ptr->rgt->rgt, ptr->lft))
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,
322 tl_nn(OR, ptr->lft->rgt, ptr->rgt->rgt));
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 */
332 if (ptr->rgt->ntyp == TRUE /* (p || T) == T */
333 || ptr->lft->ntyp == FALSE) /* (F || p) == p */
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),
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))
363 { int i; Node *ptr = ZN;
368 ptr = tl_level(nr-1);
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);
378 if (!ptr) tl_yyerror("syntax error");
380 printf("level %d: ", nr);
381 tl_explain(ptr->ntyp);
389 { tl_yychar = tl_yylex();
390 return tl_level(1); /* 2 precedence levels, 1 and 0 */
397 /* tl_verbose = 1; */
400 { printf("formula: ");
404 if (tl_Getchar() != -1)
405 { tl_yyerror("syntax error");