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