1 /***** tl_spin: tl_trans.c *****/
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
8 * Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
9 * presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
15 extern int tl_errs, tl_verbose, tl_terse, newstates, state_cnt;
17 int Stack_mx=0, Max_Red=0, Total=0;
19 static Mapping *Mapped = (Mapping *) 0;
20 static Graph *Nodes_Set = (Graph *) 0;
21 static Graph *Nodes_Stack = (Graph *) 0;
23 static char dumpbuf[4096];
24 static int Red_cnt = 0;
25 static int Lab_cnt = 0;
27 static int Stack_sz = 0;
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 *);
58 Mapped = (Mapping *) 0;
59 Nodes_Set = (Graph *) 0;
60 Nodes_Stack = (Graph *) 0;
62 memset(dumpbuf, 0, sizeof(dumpbuf));
74 for (n1 = g->New; n1; n1 = n1->nxt)
75 { dump(n1); printf(", "); }
77 for (n1 = g->Old; n1; n1 = n1->nxt)
78 { dump(n1); printf(", "); }
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(", "); }
97 printf("\nPush %s, from ", g->name->name);
98 for (z = g->incoming; z; z = z->next)
99 printf("%s, ", z->name);
103 if (Stack_sz > Stack_mx) Stack_mx = Stack_sz;
108 { Graph *g = Nodes_Stack;
110 if (g) Nodes_Stack = g->nxt;
119 { static char buf[32];
120 sprintf(buf, "S%d", state_cnt++);
125 has_clause(int tok, Graph *p, Node *n)
130 return has_clause(tok, p, n->lft) &&
131 has_clause(tok, p, n->rgt);
133 return has_clause(tok, p, n->lft) ||
134 has_clause(tok, p, n->rgt);
137 for (q = p->Other; q; q = q->nxt)
138 { qq = right_linked(q);
139 if (anywhere(tok, n, qq))
153 for (p = Nodes_Set; p; p = p->nxt)
155 && has_clause(AND, p, n))
156 { p->isgrn[p->grncnt++] =
157 (unsigned char) Red_cnt;
161 if (n->ntyp == U_OPER) /* 3.4.0 */
174 for (p = Nodes_Set; p; p = p->nxt)
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;
213 for (p = Nodes_Set; p; p = p->nxt)
214 if (!strcmp(p->name->name, nm))
216 for (m = Mapped; m; m = m->nxt)
217 if (strcmp(m->from, nm) == 0)
220 printf("warning: node %s not found\n", nm);
225 Addout(char *to, char *from)
226 { Graph *p = findgraph(from);
230 s = getsym(tl_lookup(to));
231 s->next = p->outgoing;
244 return only_nxt(n->rgt) && only_nxt(n->lft);
252 dump_cond(Node *pp, Node *r, int first)
256 if (!pp) return frst;
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, " } ");
270 if (q->ntyp == PREDICATE
276 { if (!frst) fprintf(tl_out, " && ");
280 } else if (q->ntyp == OR)
281 { if (!frst) fprintf(tl_out, " && ");
282 fprintf(tl_out, "((");
283 frst = dump_cond(q->lft, r, 1);
286 fprintf(tl_out, ") || (");
288 { if (only_nxt(q->lft))
289 { fprintf(tl_out, "1))");
294 frst = dump_cond(q->rgt, r, 1);
297 { if (only_nxt(q->rgt))
298 fprintf(tl_out, "1");
300 fprintf(tl_out, "0");
304 fprintf(tl_out, "))");
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)
311 frst = dump_cond(q->lft, r, frst);
312 frst = dump_cond(q->rgt, r, frst);
319 choueka(Graph *p, int count)
320 { int j, k, incr_cnt = 0;
322 for (j = count; j <= Max_Red; j++) /* for each acceptance class */
325 /* is state p labeled Grn-j OR not Red-j ? */
327 for (k = 0; k < (int) p->grncnt; k++)
328 if (p->isgrn[k] == j)
336 for (k = 0; k < (int) p->redcnt; k++)
337 if (p->isred[k] == j)
350 set_prefix(char *pref, int count, Graph *r2)
351 { int incr_cnt = 0; /* acceptance class 'count' */
355 sprintf(pref, "accept"); /* new */
356 else if (count >= Max_Red)
357 sprintf(pref, "T0"); /* cycle */
359 { incr_cnt = choueka(r2, count+1);
360 if (incr_cnt + count >= Max_Red)
361 sprintf(pref, "accept"); /* last hop */
363 sprintf(pref, "T%d", count+incr_cnt);
369 fsm_trans(Graph *p, int count, char *curnm)
372 char prefix[128], nwnm[256];
375 addtrans(p, curnm, False, "accept_all");
377 for (s = p->outgoing; s; s = s->next)
378 { r = findgraph(s->name);
381 { (void) set_prefix(prefix, count, r);
382 sprintf(nwnm, "%s_%s", prefix, s->name);
384 strcpy(nwnm, "accept_all");
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]);
393 addtrans(p, curnm, r->Old, nwnm);
403 for (k = 0; k <= Max_Red; k++)
404 for (p = Nodes_Set; p; p = p->nxt)
408 && !strcmp(p->name->name, "init")
413 && strcmp(p->name->name, "init") != 0)
414 strcpy(curnm, "accept_");
416 sprintf(curnm, "T%d_", k);
418 strcat(curnm, p->name->name);
420 fsm_trans(p, k, curnm);
427 { Symbol *p1, *p2, *p3, *d = ZS;
429 for (p1 = s; p1; p1 = p1->next)
430 { for (p3 = d; p3; p3 = p3->next)
431 { if (!strcmp(p3->name, p1->name))
434 if (p3) continue; /* a duplicate */
444 catSlist(Symbol *a, Symbol *b)
445 { Symbol *p1, *p2, *p3, *tmp;
447 /* remove duplicates from b */
448 for (p1 = a; p1; p1 = p1->next)
450 for (p2 = b; p2; p2 = p2->next)
451 { if (strcmp(p1->name, p2->name))
468 /* find end of list */
469 for (p1 = a; p1->next; p1 = p1->next)
478 Symbol *q1, *q2 = ZS;
480 ng(tl_lookup("init"), ZS, ZN, ZN, ZN);
483 { p1->nxt = Nodes_Set;
484 p1->Other = p1->Old = orig;
488 for (g = Nodes_Set; g; g = g->nxt)
489 { for (q1 = g->incoming; q1; q1 = q2)
491 Addout(g->name->name, q1->name);
500 { Node *q, *r, *z = ZN;
502 for (q = p; q; q = q->nxt)
505 z = tl_nn(AND, r, z);
516 { Node *n1, *n2, *lst = ZN, *d = ZN;
518 for (n1 = n; n1; n1 = n1->nxt)
530 ng(Symbol *s, Symbol *in, Node *isnew, Node *isold, Node *next)
531 { Graph *g = (Graph *) tl_emalloc(sizeof(Graph));
534 else g->name = tl_lookup(newname());
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);
548 case PREDICATE: strcat(dumpbuf, n->sym->name);
550 case U_OPER: strcat(dumpbuf, "U");
552 case V_OPER: strcat(dumpbuf, "V");
554 case OR: strcat(dumpbuf, "|");
556 case AND: strcat(dumpbuf, "&");
557 common2: sdump(n->rgt);
558 common1: sdump(n->lft);
561 case NEXT: strcat(dumpbuf, "X");
564 case CEXPR: strcat(dumpbuf, "c_expr {");
566 strcat(dumpbuf, "}");
568 case NOT: strcat(dumpbuf, "!");
570 case TRUE: strcat(dumpbuf, "T");
572 case FALSE: strcat(dumpbuf, "F");
574 default: strcat(dumpbuf, "?");
584 if (n->ntyp == PREDICATE)
589 return tl_lookup(dumpbuf);
594 { Graph *q1; Node *tmp, *n1, *n2;
597 tmp = flatten(g->Old); /* duplicate, collapse, normalize */
598 g->Other = g->Old; /* non normalized full version */
601 g->oldstring = DoDump(g->Old);
603 tmp = flatten(g->Next);
604 g->nxtstring = DoDump(tmp);
606 if (tl_verbose) dump_graph(g);
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");
614 Debug2(" compare nxt to: %s", q1->name->name);
615 Debug2(" [%s]", q1->nxtstring?q1->nxtstring->name:"true");
617 if (q1->oldstring != g->oldstring
618 || q1->nxtstring != g->nxtstring)
619 { Debug(" => different\n");
622 Debug(" => match\n");
625 q1->incoming = catSlist(g->incoming, q1->incoming);
627 /* check if there's anything in g->Other that needs
630 for (n2 = g->Other; n2; n2 = n2->nxt)
631 { for (n1 = q1->Other; n1; n1 = n1->nxt)
635 { Node *n3 = dupnode(n2);
636 /* don't mess up n2->nxt */
641 map = (Mapping *) tl_emalloc(sizeof(Mapping));
642 map->from = g->name->name;
647 for (n1 = g->Other; n1; n1 = n2)
651 for (n1 = g->Old; n1; n1 = n2)
655 for (n1 = g->Next; n1; n1 = n2)
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;
678 { Node *now, *n1, *n2, *nx;
682 { Debug2("\nDone with %s", g->name->name);
683 if (tl_verbose) dump_graph(g);
685 { if (tl_verbose) printf("\tIs Not New\n");
689 { Debug(" Has Next [");
690 for (n1 = g->Next; n1; n1 = n1->nxt)
691 { Dump(n1); Debug(", "); }
694 ng(ZS, getsym(g->name), g->Next, ZN, ZN);
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);
708 if (g->New->ntyp == AND)
713 n2->nxt = g->New->nxt;
715 n1 = n2 = g->New->lft;
718 n2->nxt = g->New->rgt;
720 releasenode(0, g->New);
727 can_release = 0; /* unless it need not go into Old */
729 g->New = g->New->nxt;
732 if (now->ntyp != TRUE)
734 { for (n1 = g->Old; n1->nxt; n1 = n1->nxt)
735 if (isequal(now, n1))
755 if (can_release) releasenode(1, now);
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);
769 nx = getnode(now); /* now also appears in Old */
773 n2->nxt = getnode(now->rgt);
774 n2->nxt->nxt = g->New;
775 g->New = flatten(n2);
777 ng(ZS, g->incoming, n1, g->Old, nx);
781 Assert(now->rgt->nxt == ZN, now->ntyp);
782 Assert(now->lft->nxt == ZN, now->ntyp);
788 nx = getnode(now); /* now also appears in Old */
798 Assert(now->lft != ZN, now->ntyp);
799 nx = dupnode(now->lft);
802 if (can_release) releasenode(0, now);
808 Assert(now->rgt->nxt == ZN, now->ntyp);
809 Assert(now->lft->nxt == ZN, now->ntyp);
818 ng(ZS, g->incoming, n1, g->Old, nx);
819 g->New = flatten(n2);
821 if (can_release) releasenode(1, now);
831 /* 1: ([]p1 && []p2) == [](p1 && p2) */
832 /* 2: (<>p1 || <>p2) == <>(p1 || p2) */
841 p->lft = twocases(p->lft);
842 p->rgt = twocases(p->rgt);
848 p->lft = twocases(p->lft);
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));
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));
879 if (!p || tl_errs) return;
883 if (tl_verbose || tl_terse)
884 { fprintf(tl_out, "\t/* Normlzd: ");
886 fprintf(tl_out, " */\n");
893 ng(ZS, getsym(tl_lookup("init")), p, ZN, ZN);
894 while ((g = Nodes_Stack) != (Graph *) 0)
895 { Nodes_Stack = g->nxt;
902 liveness(flatten(op)); /* was: liveness(op); */
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);