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