1 /***** tl_spin: tl_parse.c *****/
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 */
12 /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
13 /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
17 extern int tl_yylex(void);
18 extern int tl_verbose, tl_errs;
23 static Node *tl_formula(void);
24 static Node *tl_factor(void);
25 static Node *tl_level(int);
27 static int prec[2][4] = {
28 { U_OPER, V_OPER, 0, 0 }, /* left associative */
29 { OR, AND, IMPLIES, EQUIV, }, /* left associative */
40 tl_yyerror("expected ')'");
41 tl_yychar = tl_yylex();
45 tl_yychar = tl_yylex();
46 ptr->lft = tl_factor();
47 ptr = push_negation(ptr);
50 tl_yychar = tl_yylex();
54 if (ptr->ntyp == FALSE
56 break; /* [] false == false */
58 if (ptr->ntyp == V_OPER)
59 { if (ptr->lft->ntyp == FALSE)
60 break; /* [][]p = []p */
62 ptr = ptr->rgt; /* [] (p V q) = [] q */
65 ptr = tl_nn(V_OPER, False, ptr);
69 tl_yychar = tl_yylex();
71 if (ptr->ntyp == TRUE)
72 break; /* X true = true */
73 ptr = tl_nn(NEXT, ptr, ZN);
77 tl_yychar = tl_yylex();
82 || ptr->ntyp == FALSE)
83 break; /* <> true == true */
85 if (ptr->ntyp == U_OPER
86 && ptr->lft->ntyp == TRUE)
87 break; /* <><>p = <>p */
89 if (ptr->ntyp == U_OPER)
90 { /* <> (p U q) = <> q */
95 ptr = tl_nn(U_OPER, True, ptr);
100 tl_yychar = tl_yylex();
105 tl_yychar = tl_yylex();
108 if (!ptr) tl_yyerror("expected predicate");
111 tl_explain(ptr->ntyp);
118 bin_simpler(Node *ptr)
125 if (ptr->rgt->ntyp == TRUE
126 || ptr->rgt->ntyp == FALSE
127 || ptr->lft->ntyp == FALSE)
131 if (isequal(ptr->lft, ptr->rgt))
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;
142 if (ptr->rgt->ntyp == U_OPER
143 && ptr->rgt->lft->ntyp == TRUE)
144 { /* p U (T U q) = (T U q) */
149 /* X p U X q == X (p U q) */
150 if (ptr->rgt->ntyp == NEXT
151 && ptr->lft->ntyp == NEXT)
162 if (ptr->rgt->ntyp == FALSE
163 || ptr->rgt->ntyp == TRUE
164 || ptr->lft->ntyp == TRUE)
168 if (isequal(ptr->lft, ptr->rgt))
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;
179 /* p V (F V q) == F V q */
180 if (ptr->rgt->ntyp == V_OPER
181 && ptr->rgt->lft->ntyp == FALSE)
183 ptr->rgt = ptr->rgt->rgt;
190 if (isequal(ptr->lft, ptr->rgt))
195 ptr = tl_nn(OR, Not(ptr->lft), ptr->rgt);
200 if (isequal(ptr->lft, ptr->rgt))
205 a = rewrite(tl_nn(AND,
208 b = rewrite(tl_nn(AND,
211 ptr = tl_nn(OR, a, b);
216 /* p && (q U p) = p */
217 if (ptr->rgt->ntyp == U_OPER
218 && isequal(ptr->rgt->rgt, ptr->lft))
222 if (ptr->lft->ntyp == U_OPER
223 && isequal(ptr->lft->rgt, ptr->rgt))
228 /* p && (q V p) == q V p */
229 if (ptr->rgt->ntyp == V_OPER
230 && isequal(ptr->rgt->rgt, ptr->lft))
234 if (ptr->lft->ntyp == V_OPER
235 && isequal(ptr->lft->rgt, ptr->rgt))
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),
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,
256 tl_nn(AND, ptr->lft->rgt, ptr->rgt->rgt));
260 /* X p && X q == X (p && q) */
261 if (ptr->rgt->ntyp == NEXT
262 && ptr->lft->ntyp == NEXT)
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 */
277 if (ptr->rgt->ntyp == TRUE /* (p && T) == p */
278 || ptr->lft->ntyp == FALSE) /* (F && p) == F */
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))
295 /* p || (q U p) == q U p */
296 if (ptr->rgt->ntyp == U_OPER
297 && isequal(ptr->rgt->rgt, ptr->lft))
302 /* p || (q V p) == p */
303 if (ptr->rgt->ntyp == V_OPER
304 && isequal(ptr->rgt->rgt, ptr->lft))
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,
315 tl_nn(OR, ptr->lft->rgt, ptr->rgt->rgt));
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 */
325 if (ptr->rgt->ntyp == TRUE /* (p || T) == T */
326 || ptr->lft->ntyp == FALSE) /* (F || p) == p */
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),
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))
356 { int i; Node *ptr = ZN;
361 ptr = tl_level(nr-1);
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);
371 if (!ptr) tl_yyerror("syntax error");
373 printf("level %d: ", nr);
374 tl_explain(ptr->ntyp);
382 { tl_yychar = tl_yylex();
383 return tl_level(1); /* 2 precedence levels, 1 and 0 */
388 { Node *n = tl_formula();
390 { printf("formula: ");
394 if (tl_Getchar() != -1)
395 { tl_yyerror("syntax error");