trunk/verif/Spin/Src5.1.6/tl_trans.c

   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[256];
 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 != ZN, now->ntyp);
 726                 Assert(now->lft != ZN, now->ntyp);
 727                 Assert(now->rgt->nxt == ZN, now->ntyp);
 728                 Assert(now->lft->nxt == ZN, now->ntyp);
 729                 n1 = now->rgt;
 730                 n1->nxt = g->New;
 731
 732                 if (can_release)
 733                         nx = now;
 734                 else
 735                         nx = getnode(now); /* now also appears in Old */
 736                 nx->nxt = g->Next;
 737
 738                 n2 = now->lft;
 739                 n2->nxt = getnode(now->rgt);
 740                 n2->nxt->nxt = g->New;
 741                 g->New = flatten(n2);
 742                 push_stack(g);
 743                 ng(ZS, g->incoming, n1, g->Old, nx);
 744                 break;
 745
 746         case U_OPER:
 747                 Assert(now->rgt->nxt == ZN, now->ntyp);
 748                 Assert(now->lft->nxt == ZN, now->ntyp);
 749                 n1 = now->lft;
 750
 751                 if (can_release)
 752                         nx = now;
 753                 else
 754                         nx = getnode(now); /* now also appears in Old */
 755                 nx->nxt = g->Next;
 756
 757                 n2 = now->rgt;
 758                 n2->nxt = g->New;
 759
 760                 goto common;
 761
 762 #ifdef NXT
 763         case NEXT:
 764                 Assert(now->lft != ZN, now->ntyp);
 765                 nx = dupnode(now->lft);
 766                 nx->nxt = g->Next;
 767                 g->Next = nx;
 768                 if (can_release) releasenode(0, now);
 769                 push_stack(g);
 770                 break;
 771 #endif
 772
 773         case OR:
 774                 Assert(now->rgt->nxt == ZN, now->ntyp);
 775                 Assert(now->lft->nxt == ZN, now->ntyp);
 776                 n1 = now->lft;
 777                 nx = g->Next;
 778
 779                 n2 = now->rgt;
 780                 n2->nxt = g->New;
 781 common:
 782                 n1->nxt = g->New;
 783
 784                 ng(ZS, g->incoming, n1, g->Old, nx);
 785                 g->New = flatten(n2);
 786
 787                 if (can_release) releasenode(1, now);
 788
 789                 push_stack(g);
 790                 break;
 791         }
 792 }
 793
 794 Node *
 795 twocases(Node *p)
 796 {       Node *q;
 797         /* 1: ([]p1 && []p2) == [](p1 && p2) */
 798         /* 2: (<>p1 || <>p2) == <>(p1 || p2) */
 799
 800         if (!p) return p;
 801
 802         switch(p->ntyp) {
 803         case AND:
 804         case OR:
 805         case U_OPER:
 806         case V_OPER:
 807                 p->lft = twocases(p->lft);
 808                 p->rgt = twocases(p->rgt);
 809                 break;
 810 #ifdef NXT
 811         case NEXT:
 812 #endif
 813         case NOT:
 814                 p->lft = twocases(p->lft);
 815                 break;
 816
 817         default:
 818                 break;
 819         }
 820         if (p->ntyp == AND      /* 1 */
 821         &&  p->lft->ntyp == V_OPER
 822         &&  p->lft->lft->ntyp == FALSE
 823         &&  p->rgt->ntyp == V_OPER
 824         &&  p->rgt->lft->ntyp == FALSE)
 825         {       q = tl_nn(V_OPER, False,
 826                         tl_nn(AND, p->lft->rgt, p->rgt->rgt));
 827         } else
 828         if (p->ntyp == OR       /* 2 */
 829         &&  p->lft->ntyp == U_OPER
 830         &&  p->lft->lft->ntyp == TRUE
 831         &&  p->rgt->ntyp == U_OPER
 832         &&  p->rgt->lft->ntyp == TRUE)
 833         {       q = tl_nn(U_OPER, True,
 834                         tl_nn(OR, p->lft->rgt, p->rgt->rgt));
 835         } else
 836                 q = p;
 837         return q;
 838 }
 839
 840 void
 841 trans(Node *p)
 842 {       Node    *op;
 843         Graph   *g;
 844
 845         if (!p || tl_errs) return;
 846
 847         p = twocases(p);
 848
 849         if (tl_verbose || tl_terse)
 850         {       fprintf(tl_out, "\t/* Normlzd: ");
 851                 dump(p);
 852                 fprintf(tl_out, " */\n");
 853         }
 854         if (tl_terse)
 855                 return;
 856
 857         op = dupnode(p);
 858
 859         ng(ZS, getsym(tl_lookup("init")), p, ZN, ZN);
 860         while ((g = Nodes_Stack) != (Graph *) 0)
 861         {       Nodes_Stack = g->nxt;
 862                 expand_g(g);
 863         }
 864         if (newstates)
 865                 return;
 866
 867         fixinit(p);
 868         liveness(flatten(op));  /* was: liveness(op); */
 869
 870         mkbuchi();
 871         if (tl_verbose)
 872         {       printf("/*\n");
 873                 printf(" * %d states in Streett automaton\n", Base);
 874                 printf(" * %d Streett acceptance conditions\n", Max_Red);
 875                 printf(" * %d Buchi states\n", Total);
 876                 printf(" */\n");
 877         }
 878 }