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