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 * 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 52 ptr = tl_factor(); 53 #ifndef NO_OPT 54 if (ptr->ntyp == FALSE 55 || ptr->ntyp == TRUE) 56 break; /* [] false == false */ 57 58 if (ptr->ntyp == V_OPER) 59 { if (ptr->lft->ntyp == FALSE) 60 break; /* [][]p = []p */ 61 62 ptr = ptr->rgt; /* [] (p V q) = [] q */ 63 } 64 #endif 65 ptr = tl_nn(V_OPER, False, ptr); 66 break; 67 #ifdef NXT 68 case NEXT: 69 tl_yychar = tl_yylex(); 70 ptr = tl_factor(); 71 if (ptr->ntyp == TRUE) 72 break; /* X true = true */ 73 ptr = tl_nn(NEXT, ptr, ZN); 74 break; 75 #endif 76 case EVENTUALLY: 77 tl_yychar = tl_yylex(); 78 79 ptr = tl_factor(); 80 #ifndef NO_OPT 81 if (ptr->ntyp == TRUE 82 || ptr->ntyp == FALSE) 83 break; /* <> true == true */ 84 85 if (ptr->ntyp == U_OPER 86 && ptr->lft->ntyp == TRUE) 87 break; /* <><>p = <>p */ 88 89 if (ptr->ntyp == U_OPER) 90 { /* <> (p U q) = <> q */ 91 ptr = ptr->rgt; 92 /* fall thru */ 93 } 94 #endif 95 ptr = tl_nn(U_OPER, True, ptr); 96 97 break; 98 case PREDICATE: 99 ptr = tl_yylval; 100 tl_yychar = tl_yylex(); 101 break; 102 case TRUE: 103 case FALSE: 104 ptr = tl_yylval; 105 tl_yychar = tl_yylex(); 106 break; 107 } 108 if (!ptr) tl_yyerror("expected predicate"); 109 #if 0 110 printf("factor: "); 111 tl_explain(ptr->ntyp); 112 printf("\n"); 113 #endif 114 return ptr; 115 } 116 117 static Node * 118 bin_simpler(Node *ptr) 119 { Node *a, *b; 120 121 if (ptr) 122 switch (ptr->ntyp) { 123 case U_OPER: 124 #ifndef NO_OPT 125 if (ptr->rgt->ntyp == TRUE 126 || ptr->rgt->ntyp == FALSE 127 || ptr->lft->ntyp == FALSE) 128 { ptr = ptr->rgt; 129 break; 130 } 131 if (isequal(ptr->lft, ptr->rgt)) 132 { /* p U p = p */ 133 ptr = ptr->rgt; 134 break; 135 } 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; 140 break; 141 } 142 if (ptr->rgt->ntyp == U_OPER 143 && ptr->rgt->lft->ntyp == TRUE) 144 { /* p U (T U q) = (T U q) */ 145 ptr = ptr->rgt; 146 break; 147 } 148 #ifdef NXT 149 /* X p U X q == X (p U q) */ 150 if (ptr->rgt->ntyp == NEXT 151 && ptr->lft->ntyp == NEXT) 152 { ptr = tl_nn(NEXT, 153 tl_nn(U_OPER, 154 ptr->lft->lft, 155 ptr->rgt->lft), ZN); 156 } 157 #endif 158 #endif 159 break; 160 case V_OPER: 161 #ifndef NO_OPT 162 if (ptr->rgt->ntyp == FALSE 163 || ptr->rgt->ntyp == TRUE 164 || ptr->lft->ntyp == TRUE) 165 { ptr = ptr->rgt; 166 break; 167 } 168 if (isequal(ptr->lft, ptr->rgt)) 169 { /* p V p = p */ 170 ptr = ptr->rgt; 171 break; 172 } 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; 177 break; 178 } 179 /* p V (F V q) == F V q */ 180 if (ptr->rgt->ntyp == V_OPER 181 && ptr->rgt->lft->ntyp == FALSE) 182 { ptr->lft = False; 183 ptr->rgt = ptr->rgt->rgt; 184 break; 185 } 186 #endif 187 break; 188 case IMPLIES: 189 #ifndef NO_OPT 190 if (isequal(ptr->lft, ptr->rgt)) 191 { ptr = True; 192 break; 193 } 194 #endif 195 ptr = tl_nn(OR, Not(ptr->lft), ptr->rgt); 196 ptr = rewrite(ptr); 197 break; 198 case EQUIV: 199 #ifndef NO_OPT 200 if (isequal(ptr->lft, ptr->rgt)) 201 { ptr = True; 202 break; 203 } 204 #endif 205 a = rewrite(tl_nn(AND, 206 dupnode(ptr->lft), 207 dupnode(ptr->rgt))); 208 b = rewrite(tl_nn(AND, 209 Not(ptr->lft), 210 Not(ptr->rgt))); 211 ptr = tl_nn(OR, a, b); 212 ptr = rewrite(ptr); 213 break; 214 case AND: 215 #ifndef NO_OPT 216 /* p && (q U p) = p */ 217 if (ptr->rgt->ntyp == U_OPER 218 && isequal(ptr->rgt->rgt, ptr->lft)) 219 { ptr = ptr->lft; 220 break; 221 } 222 if (ptr->lft->ntyp == U_OPER 223 && isequal(ptr->lft->rgt, ptr->rgt)) 224 { ptr = ptr->rgt; 225 break; 226 } 227 228 /* p && (q V p) == q V p */ 229 if (ptr->rgt->ntyp == V_OPER 230 && isequal(ptr->rgt->rgt, ptr->lft)) 231 { ptr = ptr->rgt; 232 break; 233 } 234 if (ptr->lft->ntyp == V_OPER 235 && isequal(ptr->lft->rgt, ptr->rgt)) 236 { ptr = ptr->lft; 237 break; 238 } 239 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), 246 ptr->lft->rgt); 247 break; 248 } 249 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, 255 ptr->rgt->lft, 256 tl_nn(AND, ptr->lft->rgt, ptr->rgt->rgt)); 257 break; 258 } 259 #ifdef NXT 260 /* X p && X q == X (p && q) */ 261 if (ptr->rgt->ntyp == NEXT 262 && ptr->lft->ntyp == NEXT) 263 { ptr = tl_nn(NEXT, 264 tl_nn(AND, 265 ptr->rgt->lft, 266 ptr->lft->lft), ZN); 267 break; 268 } 269 #endif 270 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 */ 274 { ptr = ptr->rgt; 275 break; 276 } 277 if (ptr->rgt->ntyp == TRUE /* (p && T) == p */ 278 || ptr->lft->ntyp == FALSE) /* (F && p) == F */ 279 { ptr = ptr->lft; 280 break; 281 } 282 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)) 287 { ptr = ptr->lft; 288 break; 289 } 290 #endif 291 break; 292 293 case OR: 294 #ifndef NO_OPT 295 /* p || (q U p) == q U p */ 296 if (ptr->rgt->ntyp == U_OPER 297 && isequal(ptr->rgt->rgt, ptr->lft)) 298 { ptr = ptr->rgt; 299 break; 300 } 301 302 /* p || (q V p) == p */ 303 if (ptr->rgt->ntyp == V_OPER 304 && isequal(ptr->rgt->rgt, ptr->lft)) 305 { ptr = ptr->lft; 306 break; 307 } 308 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, 314 ptr->rgt->lft, 315 tl_nn(OR, ptr->lft->rgt, ptr->rgt->rgt)); 316 break; 317 } 318 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 */ 322 { ptr = ptr->lft; 323 break; 324 } 325 if (ptr->rgt->ntyp == TRUE /* (p || T) == T */ 326 || ptr->lft->ntyp == FALSE) /* (F || p) == p */ 327 { ptr = ptr->rgt; 328 break; 329 } 330 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), 337 ptr->rgt->rgt); 338 break; 339 } 340 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)) 345 { ptr = ptr->rgt; 346 break; 347 } 348 #endif 349 break; 350 } 351 return ptr; 352 } 353 354 static Node * 355 tl_level(int nr) 356 { int i; Node *ptr = ZN; 357 358 if (nr < 0) 359 return tl_factor(); 360 361 ptr = tl_level(nr-1); 362 again: 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); 369 goto again; 370 } 371 if (!ptr) tl_yyerror("syntax error"); 372 #if 0 373 printf("level %d: ", nr); 374 tl_explain(ptr->ntyp); 375 printf("\n"); 376 #endif 377 return ptr; 378 } 379 380 static Node * 381 tl_formula(void) 382 { tl_yychar = tl_yylex(); 383 return tl_level(1); /* 2 precedence levels, 1 and 0 */ 384 } 385 386 void 387 tl_parse(void) 388 { Node *n = tl_formula(); 389 if (tl_verbose) 390 { printf("formula: "); 391 dump(n); 392 printf("\n"); 393 } 394 if (tl_Getchar() != -1) 395 { tl_yyerror("syntax error"); 396 tl_errs++; 397 return; 398 } 399 trans(n); 400 } 401