1 /***** tl_spin: tl_buchi.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_verbose, tl_clutter, Total, Max_Red; 18 19 FILE *tl_out; /* if standalone: = stdout; */ 20 21 typedef struct Transition { 22 Symbol *name; 23 Node *cond; 24 int redundant, merged, marked; 25 struct Transition *nxt; 26 } Transition; 27 28 typedef struct State { 29 Symbol *name; 30 Transition *trans; 31 Graph *colors; 32 unsigned char redundant; 33 unsigned char accepting; 34 unsigned char reachable; 35 struct State *nxt; 36 } State; 37 38 static State *never = (State *) 0; 39 static int hitsall; 40 41 static int 42 sametrans(Transition *s, Transition *t) 43 { 44 if (strcmp(s->name->name, t->name->name) != 0) 45 return 0; 46 return isequal(s->cond, t->cond); 47 } 48 49 static Node * 50 Prune(Node *p) 51 { 52 if (p) 53 switch (p->ntyp) { 54 case PREDICATE: 55 case NOT: 56 case FALSE: 57 case TRUE: 58 #ifdef NXT 59 case NEXT: 60 #endif 61 return p; 62 case OR: 63 p->lft = Prune(p->lft); 64 if (!p->lft) 65 { releasenode(1, p->rgt); 66 return ZN; 67 } 68 p->rgt = Prune(p->rgt); 69 if (!p->rgt) 70 { releasenode(1, p->lft); 71 return ZN; 72 } 73 return p; 74 case AND: 75 p->lft = Prune(p->lft); 76 if (!p->lft) 77 return Prune(p->rgt); 78 p->rgt = Prune(p->rgt); 79 if (!p->rgt) 80 return p->lft; 81 return p; 82 } 83 releasenode(1, p); 84 return ZN; 85 } 86 87 static State * 88 findstate(char *nm) 89 { State *b; 90 for (b = never; b; b = b->nxt) 91 if (!strcmp(b->name->name, nm)) 92 return b; 93 if (strcmp(nm, "accept_all")) 94 { if (strncmp(nm, "accept", 6)) 95 { int i; char altnm[64]; 96 for (i = 0; i < 64; i++) 97 if (nm[i] == '_') 98 break; 99 if (i >= 64) 100 Fatal("name too long %s", nm); 101 sprintf(altnm, "accept%s", &nm[i]); 102 return findstate(altnm); 103 } 104 /* Fatal("buchi: no state %s", nm); */ 105 } 106 return (State *) 0; 107 } 108 109 static void 110 Dfs(State *b) 111 { Transition *t; 112 113 if (!b || b->reachable) return; 114 b->reachable = 1; 115 116 if (b->redundant) 117 printf("/* redundant state %s */\n", 118 b->name->name); 119 for (t = b->trans; t; t = t->nxt) 120 { if (!t->redundant) 121 { Dfs(findstate(t->name->name)); 122 if (!hitsall 123 && strcmp(t->name->name, "accept_all") == 0) 124 hitsall = 1; 125 } 126 } 127 } 128 129 void 130 retarget(char *from, char *to) 131 { State *b; 132 Transition *t; 133 Symbol *To = tl_lookup(to); 134 135 if (tl_verbose) printf("replace %s with %s\n", from, to); 136 137 for (b = never; b; b = b->nxt) 138 { if (!strcmp(b->name->name, from)) 139 b->redundant = 1; 140 else 141 for (t = b->trans; t; t = t->nxt) 142 { if (!strcmp(t->name->name, from)) 143 t->name = To; 144 } } 145 } 146 147 #ifdef NXT 148 static Node * 149 nonxt(Node *n) 150 { 151 switch (n->ntyp) { 152 case U_OPER: 153 case V_OPER: 154 case NEXT: 155 return ZN; 156 case OR: 157 n->lft = nonxt(n->lft); 158 n->rgt = nonxt(n->rgt); 159 if (!n->lft || !n->rgt) 160 return True; 161 return n; 162 case AND: 163 n->lft = nonxt(n->lft); 164 n->rgt = nonxt(n->rgt); 165 if (!n->lft) 166 { if (!n->rgt) 167 n = ZN; 168 else 169 n = n->rgt; 170 } else if (!n->rgt) 171 n = n->lft; 172 return n; 173 } 174 return n; 175 } 176 #endif 177 178 static Node * 179 combination(Node *s, Node *t) 180 { Node *nc; 181 #ifdef NXT 182 Node *a = nonxt(s); 183 Node *b = nonxt(t); 184 185 if (tl_verbose) 186 { printf("\tnonxtA: "); dump(a); 187 printf("\n\tnonxtB: "); dump(b); 188 printf("\n"); 189 } 190 /* if there's only a X(f), its equivalent to true */ 191 if (!a || !b) 192 nc = True; 193 else 194 nc = tl_nn(OR, a, b); 195 #else 196 nc = tl_nn(OR, s, t); 197 #endif 198 if (tl_verbose) 199 { printf("\tcombo: "); dump(nc); 200 printf("\n"); 201 } 202 return nc; 203 } 204 205 Node * 206 unclutter(Node *n, char *snm) 207 { Node *t, *s, *v, *u; 208 Symbol *w; 209 210 /* check only simple cases like !q && q */ 211 for (t = n; t; t = t->rgt) 212 { if (t->rgt) 213 { if (t->ntyp != AND || !t->lft) 214 return n; 215 if (t->lft->ntyp != PREDICATE 216 #ifdef NXT 217 && t->lft->ntyp != NEXT 218 #endif 219 && t->lft->ntyp != NOT) 220 return n; 221 } else 222 { if (t->ntyp != PREDICATE 223 #ifdef NXT 224 && t->ntyp != NEXT 225 #endif 226 && t->ntyp != NOT) 227 return n; 228 } 229 } 230 231 for (t = n; t; t = t->rgt) 232 { if (t->rgt) 233 v = t->lft; 234 else 235 v = t; 236 if (v->ntyp == NOT 237 && v->lft->ntyp == PREDICATE) 238 { w = v->lft->sym; 239 for (s = n; s; s = s->rgt) 240 { if (s == t) continue; 241 if (s->rgt) 242 u = s->lft; 243 else 244 u = s; 245 if (u->ntyp == PREDICATE 246 && strcmp(u->sym->name, w->name) == 0) 247 { if (tl_verbose) 248 { printf("BINGO %s:\t", snm); 249 dump(n); 250 printf("\n"); 251 } 252 return False; 253 } 254 } 255 } } 256 return n; 257 } 258 259 static void 260 clutter(void) 261 { State *p; 262 Transition *s; 263 264 for (p = never; p; p = p->nxt) 265 for (s = p->trans; s; s = s->nxt) 266 { s->cond = unclutter(s->cond, p->name->name); 267 if (s->cond 268 && s->cond->ntyp == FALSE) 269 { if (s != p->trans 270 || s->nxt) 271 s->redundant = 1; 272 } 273 } 274 } 275 276 static void 277 showtrans(State *a) 278 { Transition *s; 279 280 for (s = a->trans; s; s = s->nxt) 281 { printf("%s ", s->name?s->name->name:"-"); 282 dump(s->cond); 283 printf(" %d %d %d\n", s->redundant, s->merged, s->marked); 284 } 285 } 286 287 static int 288 mergetrans(void) 289 { State *b; 290 Transition *s, *t; 291 Node *nc; int cnt = 0; 292 293 for (b = never; b; b = b->nxt) 294 { if (!b->reachable) continue; 295 296 for (s = b->trans; s; s = s->nxt) 297 { if (s->redundant) continue; 298 299 for (t = s->nxt; t; t = t->nxt) 300 if (!t->redundant 301 && !strcmp(s->name->name, t->name->name)) 302 { if (tl_verbose) 303 { printf("===\nstate %s, trans to %s redundant\n", 304 b->name->name, s->name->name); 305 showtrans(b); 306 printf(" conditions "); 307 dump(s->cond); printf(" <-> "); 308 dump(t->cond); printf("\n"); 309 } 310 311 if (!s->cond) /* same as T */ 312 { releasenode(1, t->cond); /* T or t */ 313 nc = True; 314 } else if (!t->cond) 315 { releasenode(1, s->cond); 316 nc = True; 317 } else 318 { nc = combination(s->cond, t->cond); 319 } 320 t->cond = rewrite(nc); 321 t->merged = 1; 322 s->redundant = 1; 323 cnt++; 324 break; 325 } } } 326 return cnt; 327 } 328 329 static int 330 all_trans_match(State *a, State *b) 331 { Transition *s, *t; 332 int found, result = 0; 333 334 if (a->accepting != b->accepting) 335 goto done; 336 337 for (s = a->trans; s; s = s->nxt) 338 { if (s->redundant) continue; 339 found = 0; 340 for (t = b->trans; t; t = t->nxt) 341 { if (t->redundant) continue; 342 if (sametrans(s, t)) 343 { found = 1; 344 t->marked = 1; 345 break; 346 } } 347 if (!found) 348 goto done; 349 } 350 for (s = b->trans; s; s = s->nxt) 351 { if (s->redundant || s->marked) continue; 352 found = 0; 353 for (t = a->trans; t; t = t->nxt) 354 { if (t->redundant) continue; 355 if (sametrans(s, t)) 356 { found = 1; 357 break; 358 } } 359 if (!found) 360 goto done; 361 } 362 result = 1; 363 done: 364 for (s = b->trans; s; s = s->nxt) 365 s->marked = 0; 366 return result; 367 } 368 369 #ifndef NO_OPT 370 #define BUCKY 371 #endif 372 373 #ifdef BUCKY 374 static int 375 all_bucky(State *a, State *b) 376 { Transition *s, *t; 377 int found, result = 0; 378 379 for (s = a->trans; s; s = s->nxt) 380 { if (s->redundant) continue; 381 found = 0; 382 for (t = b->trans; t; t = t->nxt) 383 { if (t->redundant) continue; 384 385 if (isequal(s->cond, t->cond)) 386 { if (strcmp(s->name->name, b->name->name) == 0 387 && strcmp(t->name->name, a->name->name) == 0) 388 { found = 1; /* they point to each other */ 389 t->marked = 1; 390 break; 391 } 392 if (strcmp(s->name->name, t->name->name) == 0 393 && strcmp(s->name->name, "accept_all") == 0) 394 { found = 1; 395 t->marked = 1; 396 break; 397 /* same exit from which there is no return */ 398 } 399 } 400 } 401 if (!found) 402 goto done; 403 } 404 for (s = b->trans; s; s = s->nxt) 405 { if (s->redundant || s->marked) continue; 406 found = 0; 407 for (t = a->trans; t; t = t->nxt) 408 { if (t->redundant) continue; 409 410 if (isequal(s->cond, t->cond)) 411 { if (strcmp(s->name->name, a->name->name) == 0 412 && strcmp(t->name->name, b->name->name) == 0) 413 { found = 1; 414 t->marked = 1; 415 break; 416 } 417 if (strcmp(s->name->name, t->name->name) == 0 418 && strcmp(s->name->name, "accept_all") == 0) 419 { found = 1; 420 t->marked = 1; 421 break; 422 } 423 } 424 } 425 if (!found) 426 goto done; 427 } 428 result = 1; 429 done: 430 for (s = b->trans; s; s = s->nxt) 431 s->marked = 0; 432 return result; 433 } 434 435 static int 436 buckyballs(void) 437 { State *a, *b, *c, *d; 438 int m, cnt=0; 439 440 do { 441 m = 0; cnt++; 442 for (a = never; a; a = a->nxt) 443 { if (!a->reachable) continue; 444 445 if (a->redundant) continue; 446 447 for (b = a->nxt; b; b = b->nxt) 448 { if (!b->reachable) continue; 449 450 if (b->redundant) continue; 451 452 if (all_bucky(a, b)) 453 { m++; 454 if (tl_verbose) 455 { printf("%s bucky match %s\n", 456 a->name->name, b->name->name); 457 } 458 459 if (a->accepting && !b->accepting) 460 { if (strcmp(b->name->name, "T0_init") == 0) 461 { c = a; d = b; 462 b->accepting = 1; 463 } else 464 { c = b; d = a; 465 } 466 } else 467 { c = a; d = b; 468 } 469 470 retarget(c->name->name, d->name->name); 471 if (!strncmp(c->name->name, "accept", 6) 472 && Max_Red == 0) 473 { char buf[64]; 474 sprintf(buf, "T0%s", &(c->name->name[6])); 475 retarget(buf, d->name->name); 476 } 477 break; 478 } 479 } } 480 } while (m && cnt < 10); 481 return cnt-1; 482 } 483 #endif 484 485 static int 486 mergestates(int v) 487 { State *a, *b; 488 int m, cnt=0; 489 490 if (tl_verbose) 491 return 0; 492 493 do { 494 m = 0; cnt++; 495 for (a = never; a; a = a->nxt) 496 { if (v && !a->reachable) continue; 497 498 if (a->redundant) continue; /* 3.3.10 */ 499 500 for (b = a->nxt; b; b = b->nxt) 501 { if (v && !b->reachable) continue; 502 503 if (b->redundant) continue; /* 3.3.10 */ 504 505 if (all_trans_match(a, b)) 506 { m++; 507 if (tl_verbose) 508 { printf("%d: state %s equals state %s\n", 509 cnt, a->name->name, b->name->name); 510 showtrans(a); 511 printf("==\n"); 512 showtrans(b); 513 } 514 retarget(a->name->name, b->name->name); 515 if (!strncmp(a->name->name, "accept", 6) 516 && Max_Red == 0) 517 { char buf[64]; 518 sprintf(buf, "T0%s", &(a->name->name[6])); 519 retarget(buf, b->name->name); 520 } 521 break; 522 } 523 #if 0 524 else if (tl_verbose) 525 { printf("\n%d: state %s differs from state %s [%d,%d]\n", 526 cnt, a->name->name, b->name->name, 527 a->accepting, b->accepting); 528 showtrans(a); 529 printf("==\n"); 530 showtrans(b); 531 printf("\n"); 532 } 533 #endif 534 } } 535 } while (m && cnt < 10); 536 return cnt-1; 537 } 538 539 static int tcnt; 540 541 static void 542 rev_trans(Transition *t) /* print transitions in reverse order... */ 543 { 544 if (!t) return; 545 rev_trans(t->nxt); 546 547 if (t->redundant && !tl_verbose) return; 548 fprintf(tl_out, "\t:: ("); 549 if (dump_cond(t->cond, t->cond, 1)) 550 fprintf(tl_out, "1"); 551 fprintf(tl_out, ") -> goto %s\n", t->name->name); 552 tcnt++; 553 } 554 555 static void 556 printstate(State *b) 557 { 558 if (!b || (!tl_verbose && !b->reachable)) return; 559 560 b->reachable = 0; /* print only once */ 561 fprintf(tl_out, "%s:\n", b->name->name); 562 563 if (tl_verbose) 564 { fprintf(tl_out, " /* "); 565 dump(b->colors->Other); 566 fprintf(tl_out, " */\n"); 567 } 568 569 if (strncmp(b->name->name, "accept", 6) == 0 570 && Max_Red == 0) 571 fprintf(tl_out, "T0%s:\n", &(b->name->name[6])); 572 573 fprintf(tl_out, "\tif\n"); 574 tcnt = 0; 575 rev_trans(b->trans); 576 if (!tcnt) fprintf(tl_out, "\t:: false\n"); 577 fprintf(tl_out, "\tfi;\n"); 578 Total++; 579 } 580 581 void 582 addtrans(Graph *col, char *from, Node *op, char *to) 583 { State *b; 584 Transition *t; 585 586 t = (Transition *) tl_emalloc(sizeof(Transition)); 587 t->name = tl_lookup(to); 588 t->cond = Prune(dupnode(op)); 589 590 if (tl_verbose) 591 { printf("\n%s <<\t", from); dump(op); 592 printf("\n\t"); dump(t->cond); 593 printf(">> %s\n", t->name->name); 594 } 595 if (t->cond) t->cond = rewrite(t->cond); 596 597 for (b = never; b; b = b->nxt) 598 if (!strcmp(b->name->name, from)) 599 { t->nxt = b->trans; 600 b->trans = t; 601 return; 602 } 603 b = (State *) tl_emalloc(sizeof(State)); 604 b->name = tl_lookup(from); 605 b->colors = col; 606 b->trans = t; 607 if (!strncmp(from, "accept", 6)) 608 b->accepting = 1; 609 b->nxt = never; 610 never = b; 611 } 612 613 static void 614 clr_reach(void) 615 { State *p; 616 for (p = never; p; p = p->nxt) 617 p->reachable = 0; 618 hitsall = 0; 619 } 620 621 void 622 fsm_print(void) 623 { State *b; int cnt1, cnt2=0; 624 extern void put_uform(void); 625 626 if (tl_clutter) clutter(); 627 628 b = findstate("T0_init"); 629 if (Max_Red == 0) 630 b->accepting = 1; 631 632 mergestates(0); 633 b = findstate("T0_init"); 634 635 fprintf(tl_out, "never { /* "); 636 put_uform(); 637 fprintf(tl_out, " */\n"); 638 639 do { 640 clr_reach(); 641 Dfs(b); 642 cnt1 = mergetrans(); 643 cnt2 = mergestates(1); 644 if (tl_verbose) 645 printf("/* >>%d,%d<< */\n", cnt1, cnt2); 646 } while (cnt2 > 0); 647 648 #ifdef BUCKY 649 buckyballs(); 650 clr_reach(); 651 Dfs(b); 652 #endif 653 if (b && b->accepting) 654 fprintf(tl_out, "accept_init:\n"); 655 656 if (!b && !never) 657 { fprintf(tl_out, " 0 /* false */;\n"); 658 } else 659 { printstate(b); /* init state must be first */ 660 for (b = never; b; b = b->nxt) 661 printstate(b); 662 } 663 if (hitsall) 664 fprintf(tl_out, "accept_all:\n skip\n"); 665 fprintf(tl_out, "}\n"); 666 } 667