1 /***** tl_spin: tl_trans.c *****/
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 */
12 /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
13 /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
18 extern int tl_errs, tl_verbose, tl_terse, newstates;
20 int Stack_mx=0, Max_Red=0, Total=0;
22 static Mapping *Mapped = (Mapping *) 0;
23 static Graph *Nodes_Set = (Graph *) 0;
24 static Graph *Nodes_Stack = (Graph *) 0;
26 static char dumpbuf[2048];
27 static int Red_cnt = 0;
28 static int Lab_cnt = 0;
30 static int Stack_sz = 0;
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 *);
59 for (n1 = g->New; n1; n1 = n1->nxt)
60 { dump(n1); printf(", "); }
62 for (n1 = g->Old; n1; n1 = n1->nxt)
63 { dump(n1); printf(", "); }
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(", "); }
82 printf("\nPush %s, from ", g->name->name);
83 for (z = g->incoming; z; z = z->next)
84 printf("%s, ", z->name);
88 if (Stack_sz > Stack_mx) Stack_mx = Stack_sz;
93 { Graph *g = Nodes_Stack;
95 if (g) Nodes_Stack = g->nxt;
104 { static int cnt = 0;
106 sprintf(buf, "S%d", cnt++);
111 has_clause(int tok, Graph *p, Node *n)
116 return has_clause(tok, p, n->lft) &&
117 has_clause(tok, p, n->rgt);
119 return has_clause(tok, p, n->lft) ||
120 has_clause(tok, p, n->rgt);
123 for (q = p->Other; q; q = q->nxt)
124 { qq = right_linked(q);
125 if (anywhere(tok, n, qq))
137 for (p = Nodes_Set; p; p = p->nxt)
139 && has_clause(AND, p, n))
140 { p->isgrn[p->grncnt++] =
141 (unsigned char) Red_cnt;
145 if (n->ntyp == U_OPER) /* 3.4.0 */
156 for (p = Nodes_Set; p; p = p->nxt)
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;
195 for (p = Nodes_Set; p; p = p->nxt)
196 if (!strcmp(p->name->name, nm))
198 for (m = Mapped; m; m = m->nxt)
199 if (strcmp(m->from, nm) == 0)
202 printf("warning: node %s not found\n", nm);
207 Addout(char *to, char *from)
208 { Graph *p = findgraph(from);
212 s = getsym(tl_lookup(to));
213 s->next = p->outgoing;
226 return only_nxt(n->rgt) && only_nxt(n->lft);
234 dump_cond(Node *pp, Node *r, int first)
238 if (!pp) return frst;
243 if (q->ntyp == PREDICATE
249 { if (!frst) fprintf(tl_out, " && ");
253 } else if (q->ntyp == OR)
254 { if (!frst) fprintf(tl_out, " && ");
255 fprintf(tl_out, "((");
256 frst = dump_cond(q->lft, r, 1);
259 fprintf(tl_out, ") || (");
261 { if (only_nxt(q->lft))
262 { fprintf(tl_out, "1))");
267 frst = dump_cond(q->rgt, r, 1);
270 { if (only_nxt(q->rgt))
271 fprintf(tl_out, "1");
273 fprintf(tl_out, "0");
277 fprintf(tl_out, "))");
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)
284 frst = dump_cond(q->lft, r, frst);
285 frst = dump_cond(q->rgt, r, frst);
292 choueka(Graph *p, int count)
293 { int j, k, incr_cnt = 0;
295 for (j = count; j <= Max_Red; j++) /* for each acceptance class */
298 /* is state p labeled Grn-j OR not Red-j ? */
300 for (k = 0; k < (int) p->grncnt; k++)
301 if (p->isgrn[k] == j)
309 for (k = 0; k < (int) p->redcnt; k++)
310 if (p->isred[k] == j)
323 set_prefix(char *pref, int count, Graph *r2)
324 { int incr_cnt = 0; /* acceptance class 'count' */
328 sprintf(pref, "accept"); /* new */
329 else if (count >= Max_Red)
330 sprintf(pref, "T0"); /* cycle */
332 { incr_cnt = choueka(r2, count+1);
333 if (incr_cnt + count >= Max_Red)
334 sprintf(pref, "accept"); /* last hop */
336 sprintf(pref, "T%d", count+incr_cnt);
342 fsm_trans(Graph *p, int count, char *curnm)
345 char prefix[128], nwnm[128];
348 addtrans(p, curnm, False, "accept_all");
350 for (s = p->outgoing; s; s = s->next)
351 { r = findgraph(s->name);
354 { (void) set_prefix(prefix, count, r);
355 sprintf(nwnm, "%s_%s", prefix, s->name);
357 strcpy(nwnm, "accept_all");
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]);
366 addtrans(p, curnm, r->Old, nwnm);
376 for (k = 0; k <= Max_Red; k++)
377 for (p = Nodes_Set; p; p = p->nxt)
381 && !strcmp(p->name->name, "init")
386 && strcmp(p->name->name, "init") != 0)
387 strcpy(curnm, "accept_");
389 sprintf(curnm, "T%d_", k);
391 strcat(curnm, p->name->name);
393 fsm_trans(p, k, curnm);
400 { Symbol *p1, *p2, *p3, *d = ZS;
402 for (p1 = s; p1; p1 = p1->next)
403 { for (p3 = d; p3; p3 = p3->next)
404 { if (!strcmp(p3->name, p1->name))
407 if (p3) continue; /* a duplicate */
417 catSlist(Symbol *a, Symbol *b)
418 { Symbol *p1, *p2, *p3, *tmp;
420 /* remove duplicates from b */
421 for (p1 = a; p1; p1 = p1->next)
423 for (p2 = b; p2; p2 = p2->next)
424 { if (strcmp(p1->name, p2->name))
441 /* find end of list */
442 for (p1 = a; p1->next; p1 = p1->next)
451 Symbol *q1, *q2 = ZS;
453 ng(tl_lookup("init"), ZS, ZN, ZN, ZN);
456 p1->Other = p1->Old = orig;
459 for (g = Nodes_Set; g; g = g->nxt)
460 { for (q1 = g->incoming; q1; q1 = q2)
462 Addout(g->name->name, q1->name);
471 { Node *q, *r, *z = ZN;
473 for (q = p; q; q = q->nxt)
476 z = tl_nn(AND, r, z);
487 { Node *n1, *n2, *lst = ZN, *d = ZN;
489 for (n1 = n; n1; n1 = n1->nxt)
501 ng(Symbol *s, Symbol *in, Node *isnew, Node *isold, Node *next)
502 { Graph *g = (Graph *) tl_emalloc(sizeof(Graph));
505 else g->name = tl_lookup(newname());
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);
519 case PREDICATE: strcat(dumpbuf, n->sym->name);
521 case U_OPER: strcat(dumpbuf, "U");
523 case V_OPER: strcat(dumpbuf, "V");
525 case OR: strcat(dumpbuf, "|");
527 case AND: strcat(dumpbuf, "&");
528 common2: sdump(n->rgt);
529 common1: sdump(n->lft);
532 case NEXT: strcat(dumpbuf, "X");
535 case NOT: strcat(dumpbuf, "!");
537 case TRUE: strcat(dumpbuf, "T");
539 case FALSE: strcat(dumpbuf, "F");
541 default: strcat(dumpbuf, "?");
551 if (n->ntyp == PREDICATE)
556 return tl_lookup(dumpbuf);
561 { Graph *q1; Node *tmp, *n1, *n2;
564 tmp = flatten(g->Old); /* duplicate, collapse, normalize */
565 g->Other = g->Old; /* non normalized full version */
568 g->oldstring = DoDump(g->Old);
570 tmp = flatten(g->Next);
571 g->nxtstring = DoDump(tmp);
573 if (tl_verbose) dump_graph(g);
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");
581 Debug2(" compare nxt to: %s", q1->name->name);
582 Debug2(" [%s]", q1->nxtstring?q1->nxtstring->name:"true");
584 if (q1->oldstring != g->oldstring
585 || q1->nxtstring != g->nxtstring)
586 { Debug(" => different\n");
589 Debug(" => match\n");
592 q1->incoming = catSlist(g->incoming, q1->incoming);
594 /* check if there's anything in g->Other that needs
597 for (n2 = g->Other; n2; n2 = n2->nxt)
598 { for (n1 = q1->Other; n1; n1 = n1->nxt)
602 { Node *n3 = dupnode(n2);
603 /* don't mess up n2->nxt */
608 map = (Mapping *) tl_emalloc(sizeof(Mapping));
609 map->from = g->name->name;
614 for (n1 = g->Other; n1; n1 = n2)
618 for (n1 = g->Old; n1; n1 = n2)
622 for (n1 = g->Next; n1; n1 = n2)
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;
645 { Node *now, *n1, *n2, *nx;
649 { Debug2("\nDone with %s", g->name->name);
650 if (tl_verbose) dump_graph(g);
652 { if (tl_verbose) printf("\tIs Not New\n");
656 { Debug(" Has Next [");
657 for (n1 = g->Next; n1; n1 = n1->nxt)
658 { Dump(n1); Debug(", "); }
661 ng(ZS, getsym(g->name), g->Next, ZN, ZN);
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);
675 if (g->New->ntyp == AND)
680 n2->nxt = g->New->nxt;
682 n1 = n2 = g->New->lft;
685 n2->nxt = g->New->rgt;
687 releasenode(0, g->New);
694 can_release = 0; /* unless it need not go into Old */
696 g->New = g->New->nxt;
699 if (now->ntyp != TRUE)
701 { for (n1 = g->Old; n1->nxt; n1 = n1->nxt)
702 if (isequal(now, n1))
721 if (can_release) releasenode(1, now);
725 Assert(now->rgt->nxt == ZN, now->ntyp);
726 Assert(now->lft->nxt == ZN, now->ntyp);
733 nx = getnode(now); /* now also appears in Old */
737 n2->nxt = getnode(now->rgt);
738 n2->nxt->nxt = g->New;
739 g->New = flatten(n2);
741 ng(ZS, g->incoming, n1, g->Old, nx);
745 Assert(now->rgt->nxt == ZN, now->ntyp);
746 Assert(now->lft->nxt == ZN, now->ntyp);
752 nx = getnode(now); /* now also appears in Old */
762 nx = dupnode(now->lft);
765 if (can_release) releasenode(0, now);
771 Assert(now->rgt->nxt == ZN, now->ntyp);
772 Assert(now->lft->nxt == ZN, now->ntyp);
781 ng(ZS, g->incoming, n1, g->Old, nx);
782 g->New = flatten(n2);
784 if (can_release) releasenode(1, now);
794 /* 1: ([]p1 && []p2) == [](p1 && p2) */
795 /* 2: (<>p1 || <>p2) == <>(p1 || p2) */
804 p->lft = twocases(p->lft);
805 p->rgt = twocases(p->rgt);
811 p->lft = twocases(p->lft);
817 if (p->ntyp == AND /* 1 */
818 && p->lft->ntyp == V_OPER
819 && p->lft->lft->ntyp == FALSE
820 && p->rgt->ntyp == V_OPER
821 && p->rgt->lft->ntyp == FALSE)
822 { q = tl_nn(V_OPER, False,
823 tl_nn(AND, p->lft->rgt, p->rgt->rgt));
825 if (p->ntyp == OR /* 2 */
826 && p->lft->ntyp == U_OPER
827 && p->lft->lft->ntyp == TRUE
828 && p->rgt->ntyp == U_OPER
829 && p->rgt->lft->ntyp == TRUE)
830 { q = tl_nn(U_OPER, True,
831 tl_nn(OR, p->lft->rgt, p->rgt->rgt));
842 if (!p || tl_errs) return;
846 if (tl_verbose || tl_terse)
847 { fprintf(tl_out, "\t/* Normlzd: ");
849 fprintf(tl_out, " */\n");
856 ng(ZS, getsym(tl_lookup("init")), p, ZN, ZN);
857 while ((g = Nodes_Stack) != (Graph *) 0)
858 { Nodes_Stack = g->nxt;
865 liveness(flatten(op)); /* was: liveness(op); */
870 printf(" * %d states in Streett automaton\n", Base);
871 printf(" * %d Streett acceptance conditions\n", Max_Red);
872 printf(" * %d Buchi states\n", Total);