1 /***** tl_spin: tl_parse.c *****/ 2 3 /* Copyright (c) 1995-2000 by Lucent Technologies - Bell Laboratories */ 4 /* All Rights Reserved. This software is for educational purposes only. */ 5 /* Permission is given to distribute this code provided that this intro- */ 6 /* ductory message is not removed and no monies are exchanged. */ 7 /* No guarantee is expressed or implied by the distribution of this code. */ 8 /* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */ 9 /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */ 10 /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */ 11 /* Send bug-reports and/or questions to: gerard@research.bell-labs.com */ 12 13 #include "tl.h" 14 15 extern int tl_yylex(void); 16 extern int tl_verbose; 17 18 int tl_yychar = 0; 19 YYSTYPE tl_yylval; 20 21 static Node *tl_formula(void); 22 static Node *tl_factor(void); 23 static Node *tl_level(int); 24 25 static int prec[2][4] = { 26 { U_OPER, V_OPER, 0, 0 }, /* left associative */ 27 { OR, AND, IMPLIES, EQUIV, }, /* left associative */ 28 }; 29 30 static Node * 31 tl_factor(void) 32 { Node *ptr = ZN; 33 34 switch (tl_yychar) { 35 case '(': 36 ptr = tl_formula(); 37 if (tl_yychar != ')') 38 tl_yyerror("expected ')'"); 39 tl_yychar = tl_yylex(); 40 break; 41 case NOT: 42 ptr = tl_yylval; 43 tl_yychar = tl_yylex(); 44 ptr->lft = tl_factor(); 45 ptr = push_negation(ptr); 46 break; 47 case ALWAYS: 48 tl_yychar = tl_yylex(); 49 50 ptr = tl_factor(); 51 52 if (ptr->ntyp == FALSE 53 || ptr->ntyp == TRUE) 54 break; /* [] false == false */ 55 56 if (ptr->ntyp == V_OPER) 57 { if (ptr->lft->ntyp == FALSE) 58 break; /* [][]p = []p */ 59 60 ptr = ptr->rgt; /* [] (p V q) = [] q */ 61 } 62 63 ptr = tl_nn(V_OPER, False, ptr); 64 break; 65 #ifdef NXT 66 case NEXT: 67 tl_yychar = tl_yylex(); 68 ptr = tl_factor(); 69 if (ptr->ntyp == TRUE) 70 break; /* X true = true */ 71 ptr = tl_nn(NEXT, ptr, ZN); 72 break; 73 #endif 74 case EVENTUALLY: 75 tl_yychar = tl_yylex(); 76 77 ptr = tl_factor(); 78 if (ptr->ntyp == TRUE 79 || ptr->ntyp == FALSE) 80 break; /* <> true == true */ 81 82 if (ptr->ntyp == U_OPER 83 && ptr->lft->ntyp == TRUE) 84 break; /* <><>p = <>p */ 85 86 if (ptr->ntyp == U_OPER) 87 { /* <> (p U q) = <> q */ 88 ptr = ptr->rgt; 89 /* fall thru */ 90 } 91 92 ptr = tl_nn(U_OPER, True, ptr); 93 94 break; 95 case PREDICATE: 96 ptr = tl_yylval; 97 tl_yychar = tl_yylex(); 98 break; 99 case TRUE: 100 case FALSE: 101 ptr = tl_yylval; 102 tl_yychar = tl_yylex(); 103 break; 104 } 105 if (!ptr) tl_yyerror("expected predicate"); 106 #if 0 107 printf("factor: "); 108 tl_explain(ptr->ntyp); 109 printf("\n"); 110 #endif 111 return ptr; 112 } 113 114 static Node * 115 bin_simpler(Node *ptr) 116 { Node *a, *b; 117 118 if (ptr) 119 switch (ptr->ntyp) { 120 case U_OPER: 121 if (ptr->rgt->ntyp == TRUE 122 || ptr->rgt->ntyp == FALSE 123 || ptr->lft->ntyp == FALSE) 124 { ptr = ptr->rgt; 125 break; 126 } 127 if (isequal(ptr->lft, ptr->rgt)) 128 { /* p U p = p */ 129 ptr = ptr->rgt; 130 break; 131 } 132 if (ptr->lft->ntyp == U_OPER 133 && isequal(ptr->lft->lft, ptr->rgt)) 134 { /* (p U q) U p = (q U p) */ 135 ptr->lft = ptr->lft->rgt; 136 break; 137 } 138 if (ptr->rgt->ntyp == U_OPER 139 && ptr->rgt->lft->ntyp == TRUE) 140 { /* p U (T U q) = (T U q) */ 141 ptr = ptr->rgt; 142 break; 143 } 144 #ifdef NXT 145 /* X p U X q == X (p U q) */ 146 if (ptr->rgt->ntyp == NEXT 147 && ptr->lft->ntyp == NEXT) 148 { ptr = tl_nn(NEXT, 149 tl_nn(U_OPER, 150 ptr->lft->lft, 151 ptr->rgt->lft), ZN); 152 } 153 #endif 154 break; 155 case V_OPER: 156 if (ptr->rgt->ntyp == FALSE 157 || ptr->rgt->ntyp == TRUE 158 || ptr->lft->ntyp == TRUE) 159 { ptr = ptr->rgt; 160 break; 161 } 162 if (isequal(ptr->lft, ptr->rgt)) 163 { /* p V p = p */ 164 ptr = ptr->rgt; 165 break; 166 } 167 /* F V (p V q) == F V q */ 168 if (ptr->lft->ntyp == FALSE 169 && ptr->rgt->ntyp == V_OPER) 170 { ptr->rgt = ptr->rgt->rgt; 171 break; 172 } 173 /* p V (F V q) == F V q */ 174 if (ptr->rgt->ntyp == V_OPER 175 && ptr->rgt->lft->ntyp == FALSE) 176 { ptr->lft = False; 177 ptr->rgt = ptr->rgt->rgt; 178 break; 179 } 180 break; 181 case IMPLIES: 182 if (isequal(ptr->lft, ptr->rgt)) 183 { ptr = True; 184 break; 185 } 186 ptr = tl_nn(OR, Not(ptr->lft), ptr->rgt); 187 ptr = rewrite(ptr); 188 break; 189 case EQUIV: 190 if (isequal(ptr->lft, ptr->rgt)) 191 { ptr = True; 192 break; 193 } 194 a = rewrite(tl_nn(AND, 195 dupnode(ptr->lft), 196 dupnode(ptr->rgt))); 197 b = rewrite(tl_nn(AND, 198 Not(ptr->lft), 199 Not(ptr->rgt))); 200 ptr = tl_nn(OR, a, b); 201 ptr = rewrite(ptr); 202 break; 203 case AND: 204 /* p && (q U p) = p */ 205 if (ptr->rgt->ntyp == U_OPER 206 && isequal(ptr->rgt->rgt, ptr->lft)) 207 { ptr = ptr->lft; 208 break; 209 } 210 if (ptr->lft->ntyp == U_OPER 211 && isequal(ptr->lft->rgt, ptr->rgt)) 212 { ptr = ptr->rgt; 213 break; 214 } 215 216 /* p && (q V p) == q V p */ 217 if (ptr->rgt->ntyp == V_OPER 218 && isequal(ptr->rgt->rgt, ptr->lft)) 219 { ptr = ptr->rgt; 220 break; 221 } 222 if (ptr->lft->ntyp == V_OPER 223 && isequal(ptr->lft->rgt, ptr->rgt)) 224 { ptr = ptr->lft; 225 break; 226 } 227 228 /* (p U q) && (r U q) = (p && r) U q*/ 229 if (ptr->rgt->ntyp == U_OPER 230 && ptr->lft->ntyp == U_OPER 231 && isequal(ptr->rgt->rgt, ptr->lft->rgt)) 232 { ptr = tl_nn(U_OPER, 233 tl_nn(AND, ptr->lft->lft, ptr->rgt->lft), 234 ptr->lft->rgt); 235 break; 236 } 237 238 /* (p V q) && (p V r) = p V (q && r) */ 239 if (ptr->rgt->ntyp == V_OPER 240 && ptr->lft->ntyp == V_OPER 241 && isequal(ptr->rgt->lft, ptr->lft->lft)) 242 { ptr = tl_nn(V_OPER, 243 ptr->rgt->lft, 244 tl_nn(AND, ptr->lft->rgt, ptr->rgt->rgt)); 245 break; 246 } 247 #ifdef NXT 248 /* X p && X q == X (p && q) */ 249 if (ptr->rgt->ntyp == NEXT 250 && ptr->lft->ntyp == NEXT) 251 { ptr = tl_nn(NEXT, 252 tl_nn(AND, 253 ptr->rgt->lft, 254 ptr->lft->lft), ZN); 255 break; 256 } 257 #endif 258 259 if (isequal(ptr->lft, ptr->rgt) /* (p && p) == p */ 260 || ptr->rgt->ntyp == FALSE /* (p && F) == F */ 261 || ptr->lft->ntyp == TRUE) /* (T && p) == p */ 262 { ptr = ptr->rgt; 263 break; 264 } 265 if (ptr->rgt->ntyp == TRUE /* (p && T) == p */ 266 || ptr->lft->ntyp == FALSE) /* (F && p) == F */ 267 { ptr = ptr->lft; 268 break; 269 } 270 271 /* (p V q) && (r U q) == p V q */ 272 if (ptr->rgt->ntyp == U_OPER 273 && ptr->lft->ntyp == V_OPER 274 && isequal(ptr->lft->rgt, ptr->rgt->rgt)) 275 { ptr = ptr->lft; 276 break; 277 } 278 break; 279 280 case OR: 281 /* p || (q U p) == q U p */ 282 if (ptr->rgt->ntyp == U_OPER 283 && isequal(ptr->rgt->rgt, ptr->lft)) 284 { ptr = ptr->rgt; 285 break; 286 } 287 288 /* p || (q V p) == p */ 289 if (ptr->rgt->ntyp == V_OPER 290 && isequal(ptr->rgt->rgt, ptr->lft)) 291 { ptr = ptr->lft; 292 break; 293 } 294 295 /* (p U q) || (p U r) = p U (q || r) */ 296 if (ptr->rgt->ntyp == U_OPER 297 && ptr->lft->ntyp == U_OPER 298 && isequal(ptr->rgt->lft, ptr->lft->lft)) 299 { ptr = tl_nn(U_OPER, 300 ptr->rgt->lft, 301 tl_nn(OR, ptr->lft->rgt, ptr->rgt->rgt)); 302 break; 303 } 304 305 if (isequal(ptr->lft, ptr->rgt) /* (p || p) == p */ 306 || ptr->rgt->ntyp == FALSE /* (p || F) == p */ 307 || ptr->lft->ntyp == TRUE) /* (T || p) == T */ 308 { ptr = ptr->lft; 309 break; 310 } 311 if (ptr->rgt->ntyp == TRUE /* (p || T) == T */ 312 || ptr->lft->ntyp == FALSE) /* (F || p) == p */ 313 { ptr = ptr->rgt; 314 break; 315 } 316 317 /* (p V q) || (r V q) = (p || r) V q */ 318 if (ptr->rgt->ntyp == V_OPER 319 && ptr->lft->ntyp == V_OPER 320 && isequal(ptr->lft->rgt, ptr->rgt->rgt)) 321 { ptr = tl_nn(V_OPER, 322 tl_nn(OR, ptr->lft->lft, ptr->rgt->lft), 323 ptr->rgt->rgt); 324 break; 325 } 326 327 /* (p V q) || (r U q) == r U q */ 328 if (ptr->rgt->ntyp == U_OPER 329 && ptr->lft->ntyp == V_OPER 330 && isequal(ptr->lft->rgt, ptr->rgt->rgt)) 331 { ptr = ptr->rgt; 332 break; 333 } 334 335 break; 336 } 337 return ptr; 338 } 339 340 static Node * 341 tl_level(int nr) 342 { int i; Node *ptr = ZN; 343 344 if (nr < 0) 345 return tl_factor(); 346 347 ptr = tl_level(nr-1); 348 again: 349 for (i = 0; i < 4; i++) 350 if (tl_yychar == prec[nr][i]) 351 { tl_yychar = tl_yylex(); 352 ptr = tl_nn(prec[nr][i], 353 ptr, tl_level(nr-1)); 354 ptr = bin_simpler(ptr); 355 goto again; 356 } 357 if (!ptr) tl_yyerror("syntax error"); 358 #if 0 359 printf("level %d: ", nr); 360 tl_explain(ptr->ntyp); 361 printf("\n"); 362 #endif 363 return ptr; 364 } 365 366 static Node * 367 tl_formula(void) 368 { tl_yychar = tl_yylex(); 369 return tl_level(1); /* 2 precedence levels, 1 and 0 */ 370 } 371 372 void 373 tl_parse(void) 374 { Node *n = tl_formula(); 375 if (tl_verbose) 376 { printf("formula: "); 377 dump(n); 378 printf("\n"); 379 } 380 trans(n); 381 } 382