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
ini_trans(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
dump_graph(Graph * g)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
push_stack(Graph * g)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 *
pop_stack(void)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 *
newname(void)121 newname(void)
122 { static char buf[32];
123 sprintf(buf, "S%d", state_cnt++);
124 return buf;
125 }
126
127 static int
has_clause(int tok,Graph * p,Node * n)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
mk_grn(Node * n)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
mk_red(Node * n)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
liveness(Node * n)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 *
findgraph(char * nm)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
Addout(char * to,char * from)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
only_nxt(Node * n)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
dump_cond(Node * pp,Node * r,int first)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
choueka(Graph * p,int count)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
set_prefix(char * pref,int count,Graph * r2)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
fsm_trans(Graph * p,int count,char * curnm)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
mkbuchi(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 *
dupSlist(Symbol * s)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 *
catSlist(Symbol * a,Symbol * b)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
fixinit(Node * orig)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 *
flatten(Node * p)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 *
Duplicate(Node * n)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
ng(Symbol * s,Symbol * in,Node * isnew,Node * isold,Node * next)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
sdump(Node * n)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 *
DoDump(Node * n)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
not_new(Graph * g)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
expand_g(Graph * g)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 *
twocases(Node * p)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
trans(Node * p)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