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 *
tl_factor(void)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 *
bin_simpler(Node * ptr)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 *
tl_level(int nr)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 *
tl_formula(void)380 tl_formula(void)
381 { tl_yychar = tl_yylex();
382 return tl_level(1); /* 2 precedence levels, 1 and 0 */
383 }
384
385 void
tl_parse(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 }
403