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