1 /***** tl_spin: tl_trans.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 FILE *tl_out; 18 extern int tl_errs, tl_verbose, tl_terse, newstates; 19 20 int Stack_mx=0, Max_Red=0, Total=0; 21 22 static Mapping *Mapped = (Mapping *) 0; 23 static Graph *Nodes_Set = (Graph *) 0; 24 static Graph *Nodes_Stack = (Graph *) 0; 25 26 static char dumpbuf[2048]; 27 static int Red_cnt = 0; 28 static int Lab_cnt = 0; 29 static int Base = 0; 30 static int Stack_sz = 0; 31 32 static Graph *findgraph(char *); 33 static Graph *pop_stack(void); 34 static Node *Duplicate(Node *); 35 static Node *flatten(Node *); 36 static Symbol *catSlist(Symbol *, Symbol *); 37 static Symbol *dupSlist(Symbol *); 38 static char *newname(void); 39 static int choueka(Graph *, int); 40 static int not_new(Graph *); 41 static int set_prefix(char *, int, Graph *); 42 static void Addout(char *, char *); 43 static void fsm_trans(Graph *, int, char *); 44 static void mkbuchi(void); 45 static void expand_g(Graph *); 46 static void fixinit(Node *); 47 static void liveness(Node *); 48 static void mk_grn(Node *); 49 static void mk_red(Node *); 50 static void ng(Symbol *, Symbol *, Node *, Node *, Node *); 51 static void push_stack(Graph *); 52 static void sdump(Node *); 53 54 static void 55 dump_graph(Graph *g) 56 { Node *n1; 57 58 printf("\n\tnew:\t"); 59 for (n1 = g->New; n1; n1 = n1->nxt) 60 { dump(n1); printf(", "); } 61 printf("\n\told:\t"); 62 for (n1 = g->Old; n1; n1 = n1->nxt) 63 { dump(n1); printf(", "); } 64 printf("\n\tnxt:\t"); 65 for (n1 = g->Next; n1; n1 = n1->nxt) 66 { dump(n1); printf(", "); } 67 printf("\n\tother:\t"); 68 for (n1 = g->Other; n1; n1 = n1->nxt) 69 { dump(n1); printf(", "); } 70 printf("\n"); 71 } 72 73 static void 74 push_stack(Graph *g) 75 { 76 if (!g) return; 77 78 g->nxt = Nodes_Stack; 79 Nodes_Stack = g; 80 if (tl_verbose) 81 { Symbol *z; 82 printf("\nPush %s, from ", g->name->name); 83 for (z = g->incoming; z; z = z->next) 84 printf("%s, ", z->name); 85 dump_graph(g); 86 } 87 Stack_sz++; 88 if (Stack_sz > Stack_mx) Stack_mx = Stack_sz; 89 } 90 91 static Graph * 92 pop_stack(void) 93 { Graph *g = Nodes_Stack; 94 95 if (g) Nodes_Stack = g->nxt; 96 97 Stack_sz--; 98 99 return g; 100 } 101 102 static char * 103 newname(void) 104 { static int cnt = 0; 105 static char buf[32]; 106 sprintf(buf, "S%d", cnt++); 107 return buf; 108 } 109 110 static int 111 has_clause(int tok, Graph *p, Node *n) 112 { Node *q, *qq; 113 114 switch (n->ntyp) { 115 case AND: 116 return has_clause(tok, p, n->lft) && 117 has_clause(tok, p, n->rgt); 118 case OR: 119 return has_clause(tok, p, n->lft) || 120 has_clause(tok, p, n->rgt); 121 } 122 123 for (q = p->Other; q; q = q->nxt) 124 { qq = right_linked(q); 125 if (anywhere(tok, n, qq)) 126 return 1; 127 } 128 return 0; 129 } 130 131 static void 132 mk_grn(Node *n) 133 { Graph *p; 134 135 n = right_linked(n); 136 more: 137 for (p = Nodes_Set; p; p = p->nxt) 138 if (p->outgoing 139 && has_clause(AND, p, n)) 140 { p->isgrn[p->grncnt++] = 141 (unsigned char) Red_cnt; 142 Lab_cnt++; 143 } 144 145 if (n->ntyp == U_OPER) /* 3.4.0 */ 146 { n = n->rgt; 147 goto more; 148 } 149 } 150 151 static void 152 mk_red(Node *n) 153 { Graph *p; 154 155 n = right_linked(n); 156 for (p = Nodes_Set; p; p = p->nxt) 157 { if (p->outgoing 158 && has_clause(0, p, n)) 159 { if (p->redcnt >= 63) 160 Fatal("too many Untils", (char *)0); 161 p->isred[p->redcnt++] = 162 (unsigned char) Red_cnt; 163 Lab_cnt++; Max_Red = Red_cnt; 164 } } 165 } 166 167 static void 168 liveness(Node *n) 169 { 170 if (n) 171 switch (n->ntyp) { 172 #ifdef NXT 173 case NEXT: 174 liveness(n->lft); 175 break; 176 #endif 177 case U_OPER: 178 Red_cnt++; 179 mk_red(n); 180 mk_grn(n->rgt); 181 /* fall through */ 182 case V_OPER: 183 case OR: case AND: 184 liveness(n->lft); 185 liveness(n->rgt); 186 break; 187 } 188 } 189 190 static Graph * 191 findgraph(char *nm) 192 { Graph *p; 193 Mapping *m; 194 195 for (p = Nodes_Set; p; p = p->nxt) 196 if (!strcmp(p->name->name, nm)) 197 return p; 198 for (m = Mapped; m; m = m->nxt) 199 if (strcmp(m->from, nm) == 0) 200 return m->to; 201 202 printf("warning: node %s not found\n", nm); 203 return (Graph *) 0; 204 } 205 206 static void 207 Addout(char *to, char *from) 208 { Graph *p = findgraph(from); 209 Symbol *s; 210 211 if (!p) return; 212 s = getsym(tl_lookup(to)); 213 s->next = p->outgoing; 214 p->outgoing = s; 215 } 216 217 #ifdef NXT 218 int 219 only_nxt(Node *n) 220 { 221 switch (n->ntyp) { 222 case NEXT: 223 return 1; 224 case OR: 225 case AND: 226 return only_nxt(n->rgt) && only_nxt(n->lft); 227 default: 228 return 0; 229 } 230 } 231 #endif 232 233 int 234 dump_cond(Node *pp, Node *r, int first) 235 { Node *q; 236 int frst = first; 237 238 if (!pp) return frst; 239 240 q = dupnode(pp); 241 q = rewrite(q); 242 243 if (q->ntyp == PREDICATE 244 || q->ntyp == NOT 245 #ifndef NXT 246 || q->ntyp == OR 247 #endif 248 || q->ntyp == FALSE) 249 { if (!frst) fprintf(tl_out, " && "); 250 dump(q); 251 frst = 0; 252 #ifdef NXT 253 } else if (q->ntyp == OR) 254 { if (!frst) fprintf(tl_out, " && "); 255 fprintf(tl_out, "(("); 256 frst = dump_cond(q->lft, r, 1); 257 258 if (!frst) 259 fprintf(tl_out, ") || ("); 260 else 261 { if (only_nxt(q->lft)) 262 { fprintf(tl_out, "1))"); 263 return 0; 264 } 265 } 266 267 frst = dump_cond(q->rgt, r, 1); 268 269 if (frst) 270 { if (only_nxt(q->rgt)) 271 fprintf(tl_out, "1"); 272 else 273 fprintf(tl_out, "0"); 274 frst = 0; 275 } 276 277 fprintf(tl_out, "))"); 278 #endif 279 } else if (q->ntyp == V_OPER 280 && !anywhere(AND, q->rgt, r)) 281 { frst = dump_cond(q->rgt, r, frst); 282 } else if (q->ntyp == AND) 283 { 284 frst = dump_cond(q->lft, r, frst); 285 frst = dump_cond(q->rgt, r, frst); 286 } 287 288 return frst; 289 } 290 291 static int 292 choueka(Graph *p, int count) 293 { int j, k, incr_cnt = 0; 294 295 for (j = count; j <= Max_Red; j++) /* for each acceptance class */ 296 { int delta = 0; 297 298 /* is state p labeled Grn-j OR not Red-j ? */ 299 300 for (k = 0; k < (int) p->grncnt; k++) 301 if (p->isgrn[k] == j) 302 { delta = 1; 303 break; 304 } 305 if (delta) 306 { incr_cnt++; 307 continue; 308 } 309 for (k = 0; k < (int) p->redcnt; k++) 310 if (p->isred[k] == j) 311 { delta = 1; 312 break; 313 } 314 315 if (delta) break; 316 317 incr_cnt++; 318 } 319 return incr_cnt; 320 } 321 322 static int 323 set_prefix(char *pref, int count, Graph *r2) 324 { int incr_cnt = 0; /* acceptance class 'count' */ 325 326 if (Lab_cnt == 0 327 || Max_Red == 0) 328 sprintf(pref, "accept"); /* new */ 329 else if (count >= Max_Red) 330 sprintf(pref, "T0"); /* cycle */ 331 else 332 { incr_cnt = choueka(r2, count+1); 333 if (incr_cnt + count >= Max_Red) 334 sprintf(pref, "accept"); /* last hop */ 335 else 336 sprintf(pref, "T%d", count+incr_cnt); 337 } 338 return incr_cnt; 339 } 340 341 static void 342 fsm_trans(Graph *p, int count, char *curnm) 343 { Graph *r; 344 Symbol *s; 345 char prefix[128], nwnm[128]; 346 347 if (!p->outgoing) 348 addtrans(p, curnm, False, "accept_all"); 349 350 for (s = p->outgoing; s; s = s->next) 351 { r = findgraph(s->name); 352 if (!r) continue; 353 if (r->outgoing) 354 { (void) set_prefix(prefix, count, r); 355 sprintf(nwnm, "%s_%s", prefix, s->name); 356 } else 357 strcpy(nwnm, "accept_all"); 358 359 if (tl_verbose) 360 { printf("maxred=%d, count=%d, curnm=%s, nwnm=%s ", 361 Max_Red, count, curnm, nwnm); 362 printf("(greencnt=%d,%d, redcnt=%d,%d)\n", 363 r->grncnt, r->isgrn[0], 364 r->redcnt, r->isred[0]); 365 } 366 addtrans(p, curnm, r->Old, nwnm); 367 } 368 } 369 370 static void 371 mkbuchi(void) 372 { Graph *p; 373 int k; 374 char curnm[64]; 375 376 for (k = 0; k <= Max_Red; k++) 377 for (p = Nodes_Set; p; p = p->nxt) 378 { if (!p->outgoing) 379 continue; 380 if (k != 0 381 && !strcmp(p->name->name, "init") 382 && Max_Red != 0) 383 continue; 384 385 if (k == Max_Red 386 && strcmp(p->name->name, "init") != 0) 387 strcpy(curnm, "accept_"); 388 else 389 sprintf(curnm, "T%d_", k); 390 391 strcat(curnm, p->name->name); 392 393 fsm_trans(p, k, curnm); 394 } 395 fsm_print(); 396 } 397 398 static Symbol * 399 dupSlist(Symbol *s) 400 { Symbol *p1, *p2, *p3, *d = ZS; 401 402 for (p1 = s; p1; p1 = p1->next) 403 { for (p3 = d; p3; p3 = p3->next) 404 { if (!strcmp(p3->name, p1->name)) 405 break; 406 } 407 if (p3) continue; /* a duplicate */ 408 409 p2 = getsym(p1); 410 p2->next = d; 411 d = p2; 412 } 413 return d; 414 } 415 416 static Symbol * 417 catSlist(Symbol *a, Symbol *b) 418 { Symbol *p1, *p2, *p3, *tmp; 419 420 /* remove duplicates from b */ 421 for (p1 = a; p1; p1 = p1->next) 422 { p3 = ZS; 423 for (p2 = b; p2; p2 = p2->next) 424 { if (strcmp(p1->name, p2->name)) 425 { p3 = p2; 426 continue; 427 } 428 tmp = p2->next; 429 tfree((void *) p2); 430 if (p3) 431 p3->next = tmp; 432 else 433 b = tmp; 434 } } 435 if (!a) return b; 436 if (!b) return a; 437 if (!b->next) 438 { b->next = a; 439 return b; 440 } 441 /* find end of list */ 442 for (p1 = a; p1->next; p1 = p1->next) 443 ; 444 p1->next = b; 445 return a; 446 } 447 448 static void 449 fixinit(Node *orig) 450 { Graph *p1, *g; 451 Symbol *q1, *q2 = ZS; 452 453 ng(tl_lookup("init"), ZS, ZN, ZN, ZN); 454 p1 = pop_stack(); 455 p1->nxt = Nodes_Set; 456 p1->Other = p1->Old = orig; 457 Nodes_Set = p1; 458 459 for (g = Nodes_Set; g; g = g->nxt) 460 { for (q1 = g->incoming; q1; q1 = q2) 461 { q2 = q1->next; 462 Addout(g->name->name, q1->name); 463 tfree((void *) q1); 464 } 465 g->incoming = ZS; 466 } 467 } 468 469 static Node * 470 flatten(Node *p) 471 { Node *q, *r, *z = ZN; 472 473 for (q = p; q; q = q->nxt) 474 { r = dupnode(q); 475 if (z) 476 z = tl_nn(AND, r, z); 477 else 478 z = r; 479 } 480 if (!z) return z; 481 z = rewrite(z); 482 return z; 483 } 484 485 static Node * 486 Duplicate(Node *n) 487 { Node *n1, *n2, *lst = ZN, *d = ZN; 488 489 for (n1 = n; n1; n1 = n1->nxt) 490 { n2 = dupnode(n1); 491 if (lst) 492 { lst->nxt = n2; 493 lst = n2; 494 } else 495 d = lst = n2; 496 } 497 return d; 498 } 499 500 static void 501 ng(Symbol *s, Symbol *in, Node *isnew, Node *isold, Node *next) 502 { Graph *g = (Graph *) tl_emalloc(sizeof(Graph)); 503 504 if (s) g->name = s; 505 else g->name = tl_lookup(newname()); 506 507 if (in) g->incoming = dupSlist(in); 508 if (isnew) g->New = flatten(isnew); 509 if (isold) g->Old = Duplicate(isold); 510 if (next) g->Next = flatten(next); 511 512 push_stack(g); 513 } 514 515 static void 516 sdump(Node *n) 517 { 518 switch (n->ntyp) { 519 case PREDICATE: strcat(dumpbuf, n->sym->name); 520 break; 521 case U_OPER: strcat(dumpbuf, "U"); 522 goto common2; 523 case V_OPER: strcat(dumpbuf, "V"); 524 goto common2; 525 case OR: strcat(dumpbuf, "|"); 526 goto common2; 527 case AND: strcat(dumpbuf, "&"); 528 common2: sdump(n->rgt); 529 common1: sdump(n->lft); 530 break; 531 #ifdef NXT 532 case NEXT: strcat(dumpbuf, "X"); 533 goto common1; 534 #endif 535 case NOT: strcat(dumpbuf, "!"); 536 goto common1; 537 case TRUE: strcat(dumpbuf, "T"); 538 break; 539 case FALSE: strcat(dumpbuf, "F"); 540 break; 541 default: strcat(dumpbuf, "?"); 542 break; 543 } 544 } 545 546 Symbol * 547 DoDump(Node *n) 548 { 549 if (!n) return ZS; 550 551 if (n->ntyp == PREDICATE) 552 return n->sym; 553 554 dumpbuf[0] = '\0'; 555 sdump(n); 556 return tl_lookup(dumpbuf); 557 } 558 559 static int 560 not_new(Graph *g) 561 { Graph *q1; Node *tmp, *n1, *n2; 562 Mapping *map; 563 564 tmp = flatten(g->Old); /* duplicate, collapse, normalize */ 565 g->Other = g->Old; /* non normalized full version */ 566 g->Old = tmp; 567 568 g->oldstring = DoDump(g->Old); 569 570 tmp = flatten(g->Next); 571 g->nxtstring = DoDump(tmp); 572 573 if (tl_verbose) dump_graph(g); 574 575 Debug2("\tformula-old: [%s]\n", g->oldstring?g->oldstring->name:"true"); 576 Debug2("\tformula-nxt: [%s]\n", g->nxtstring?g->nxtstring->name:"true"); 577 for (q1 = Nodes_Set; q1; q1 = q1->nxt) 578 { Debug2(" compare old to: %s", q1->name->name); 579 Debug2(" [%s]", q1->oldstring?q1->oldstring->name:"true"); 580 581 Debug2(" compare nxt to: %s", q1->name->name); 582 Debug2(" [%s]", q1->nxtstring?q1->nxtstring->name:"true"); 583 584 if (q1->oldstring != g->oldstring 585 || q1->nxtstring != g->nxtstring) 586 { Debug(" => different\n"); 587 continue; 588 } 589 Debug(" => match\n"); 590 591 if (g->incoming) 592 q1->incoming = catSlist(g->incoming, q1->incoming); 593 594 /* check if there's anything in g->Other that needs 595 adding to q1->Other 596 */ 597 for (n2 = g->Other; n2; n2 = n2->nxt) 598 { for (n1 = q1->Other; n1; n1 = n1->nxt) 599 if (isequal(n1, n2)) 600 break; 601 if (!n1) 602 { Node *n3 = dupnode(n2); 603 /* don't mess up n2->nxt */ 604 n3->nxt = q1->Other; 605 q1->Other = n3; 606 } } 607 608 map = (Mapping *) tl_emalloc(sizeof(Mapping)); 609 map->from = g->name->name; 610 map->to = q1; 611 map->nxt = Mapped; 612 Mapped = map; 613 614 for (n1 = g->Other; n1; n1 = n2) 615 { n2 = n1->nxt; 616 releasenode(1, n1); 617 } 618 for (n1 = g->Old; n1; n1 = n2) 619 { n2 = n1->nxt; 620 releasenode(1, n1); 621 } 622 for (n1 = g->Next; n1; n1 = n2) 623 { n2 = n1->nxt; 624 releasenode(1, n1); 625 } 626 return 1; 627 } 628 629 if (newstates) tl_verbose=1; 630 Debug2(" New Node %s [", g->name->name); 631 for (n1 = g->Old; n1; n1 = n1->nxt) 632 { Dump(n1); Debug(", "); } 633 Debug2("] nr %d\n", Base); 634 if (newstates) tl_verbose=0; 635 636 Base++; 637 g->nxt = Nodes_Set; 638 Nodes_Set = g; 639 640 return 0; 641 } 642 643 static void 644 expand_g(Graph *g) 645 { Node *now, *n1, *n2, *nx; 646 int can_release; 647 648 if (!g->New) 649 { Debug2("\nDone with %s", g->name->name); 650 if (tl_verbose) dump_graph(g); 651 if (not_new(g)) 652 { if (tl_verbose) printf("\tIs Not New\n"); 653 return; 654 } 655 if (g->Next) 656 { Debug(" Has Next ["); 657 for (n1 = g->Next; n1; n1 = n1->nxt) 658 { Dump(n1); Debug(", "); } 659 Debug("]\n"); 660 661 ng(ZS, getsym(g->name), g->Next, ZN, ZN); 662 } 663 return; 664 } 665 666 if (tl_verbose) 667 { Symbol *z; 668 printf("\nExpand %s, from ", g->name->name); 669 for (z = g->incoming; z; z = z->next) 670 printf("%s, ", z->name); 671 printf("\n\thandle:\t"); Explain(g->New->ntyp); 672 dump_graph(g); 673 } 674 675 if (g->New->ntyp == AND) 676 { if (g->New->nxt) 677 { n2 = g->New->rgt; 678 while (n2->nxt) 679 n2 = n2->nxt; 680 n2->nxt = g->New->nxt; 681 } 682 n1 = n2 = g->New->lft; 683 while (n2->nxt) 684 n2 = n2->nxt; 685 n2->nxt = g->New->rgt; 686 687 releasenode(0, g->New); 688 689 g->New = n1; 690 push_stack(g); 691 return; 692 } 693 694 can_release = 0; /* unless it need not go into Old */ 695 now = g->New; 696 g->New = g->New->nxt; 697 now->nxt = ZN; 698 699 if (now->ntyp != TRUE) 700 { if (g->Old) 701 { for (n1 = g->Old; n1->nxt; n1 = n1->nxt) 702 if (isequal(now, n1)) 703 { can_release = 1; 704 goto out; 705 } 706 n1->nxt = now; 707 } else 708 g->Old = now; 709 } 710 out: 711 switch (now->ntyp) { 712 case FALSE: 713 push_stack(g); 714 break; 715 case TRUE: 716 releasenode(1, now); 717 push_stack(g); 718 break; 719 case PREDICATE: 720 case NOT: 721 if (can_release) releasenode(1, now); 722 push_stack(g); 723 break; 724 case V_OPER: 725 Assert(now->rgt->nxt == ZN, now->ntyp); 726 Assert(now->lft->nxt == ZN, now->ntyp); 727 n1 = now->rgt; 728 n1->nxt = g->New; 729 730 if (can_release) 731 nx = now; 732 else 733 nx = getnode(now); /* now also appears in Old */ 734 nx->nxt = g->Next; 735 736 n2 = now->lft; 737 n2->nxt = getnode(now->rgt); 738 n2->nxt->nxt = g->New; 739 g->New = flatten(n2); 740 push_stack(g); 741 ng(ZS, g->incoming, n1, g->Old, nx); 742 break; 743 744 case U_OPER: 745 Assert(now->rgt->nxt == ZN, now->ntyp); 746 Assert(now->lft->nxt == ZN, now->ntyp); 747 n1 = now->lft; 748 749 if (can_release) 750 nx = now; 751 else 752 nx = getnode(now); /* now also appears in Old */ 753 nx->nxt = g->Next; 754 755 n2 = now->rgt; 756 n2->nxt = g->New; 757 758 goto common; 759 760 #ifdef NXT 761 case NEXT: 762 nx = dupnode(now->lft); 763 nx->nxt = g->Next; 764 g->Next = nx; 765 if (can_release) releasenode(0, now); 766 push_stack(g); 767 break; 768 #endif 769 770 case OR: 771 Assert(now->rgt->nxt == ZN, now->ntyp); 772 Assert(now->lft->nxt == ZN, now->ntyp); 773 n1 = now->lft; 774 nx = g->Next; 775 776 n2 = now->rgt; 777 n2->nxt = g->New; 778 common: 779 n1->nxt = g->New; 780 781 ng(ZS, g->incoming, n1, g->Old, nx); 782 g->New = flatten(n2); 783 784 if (can_release) releasenode(1, now); 785 786 push_stack(g); 787 break; 788 } 789 } 790 791 Node * 792 twocases(Node *p) 793 { Node *q; 794 /* 1: ([]p1 && []p2) == [](p1 && p2) */ 795 /* 2: (<>p1 || <>p2) == <>(p1 || p2) */ 796 797 if (!p) return p; 798 799 switch(p->ntyp) { 800 case AND: 801 case OR: 802 case U_OPER: 803 case V_OPER: 804 p->lft = twocases(p->lft); 805 p->rgt = twocases(p->rgt); 806 break; 807 #ifdef NXT 808 case NEXT: 809 #endif 810 case NOT: 811 p->lft = twocases(p->lft); 812 break; 813 814 default: 815 break; 816 } 817 if (p->ntyp == AND /* 1 */ 818 && p->lft->ntyp == V_OPER 819 && p->lft->lft->ntyp == FALSE 820 && p->rgt->ntyp == V_OPER 821 && p->rgt->lft->ntyp == FALSE) 822 { q = tl_nn(V_OPER, False, 823 tl_nn(AND, p->lft->rgt, p->rgt->rgt)); 824 } else 825 if (p->ntyp == OR /* 2 */ 826 && p->lft->ntyp == U_OPER 827 && p->lft->lft->ntyp == TRUE 828 && p->rgt->ntyp == U_OPER 829 && p->rgt->lft->ntyp == TRUE) 830 { q = tl_nn(U_OPER, True, 831 tl_nn(OR, p->lft->rgt, p->rgt->rgt)); 832 } else 833 q = p; 834 return q; 835 } 836 837 void 838 trans(Node *p) 839 { Node *op; 840 Graph *g; 841 842 if (!p || tl_errs) return; 843 844 p = twocases(p); 845 846 if (tl_verbose || tl_terse) 847 { fprintf(tl_out, "\t/* Normlzd: "); 848 dump(p); 849 fprintf(tl_out, " */\n"); 850 } 851 if (tl_terse) 852 return; 853 854 op = dupnode(p); 855 856 ng(ZS, getsym(tl_lookup("init")), p, ZN, ZN); 857 while ((g = Nodes_Stack) != (Graph *) 0) 858 { Nodes_Stack = g->nxt; 859 expand_g(g); 860 } 861 if (newstates) 862 return; 863 864 fixinit(p); 865 liveness(flatten(op)); /* was: liveness(op); */ 866 867 mkbuchi(); 868 if (tl_verbose) 869 { printf("/*\n"); 870 printf(" * %d states in Streett automaton\n", Base); 871 printf(" * %d Streett acceptance conditions\n", Max_Red); 872 printf(" * %d Buchi states\n", Total); 873 printf(" */\n"); 874 } 875 } 876