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");
This page took 0.055084 seconds and 5 git commands to generate.