sys/src/cmd/spin/tl_trans.c

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