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