+++ /dev/null
-/***** tl_spin: tl_trans.c *****/
-
-/* Copyright (c) 1995-2003 by Lucent Technologies, Bell Laboratories. */
-/* All Rights Reserved. This software is for educational purposes only. */
-/* No guarantee whatsoever is expressed or implied by the distribution of */
-/* this code. Permission is given to distribute this code provided that */
-/* this introductory message is not removed and no monies are exchanged. */
-/* Software written by Gerard J. Holzmann. For tool documentation see: */
-/* http://spinroot.com/ */
-/* Send all bug-reports and/or questions to: bugs@spinroot.com */
-
-/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
-/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
-
-#include "tl.h"
-
-extern FILE *tl_out;
-extern int tl_errs, tl_verbose, tl_terse, newstates;
-
-int Stack_mx=0, Max_Red=0, Total=0;
-
-static Mapping *Mapped = (Mapping *) 0;
-static Graph *Nodes_Set = (Graph *) 0;
-static Graph *Nodes_Stack = (Graph *) 0;
-
-static char dumpbuf[2048];
-static int Red_cnt = 0;
-static int Lab_cnt = 0;
-static int Base = 0;
-static int Stack_sz = 0;
-
-static Graph *findgraph(char *);
-static Graph *pop_stack(void);
-static Node *Duplicate(Node *);
-static Node *flatten(Node *);
-static Symbol *catSlist(Symbol *, Symbol *);
-static Symbol *dupSlist(Symbol *);
-static char *newname(void);
-static int choueka(Graph *, int);
-static int not_new(Graph *);
-static int set_prefix(char *, int, Graph *);
-static void Addout(char *, char *);
-static void fsm_trans(Graph *, int, char *);
-static void mkbuchi(void);
-static void expand_g(Graph *);
-static void fixinit(Node *);
-static void liveness(Node *);
-static void mk_grn(Node *);
-static void mk_red(Node *);
-static void ng(Symbol *, Symbol *, Node *, Node *, Node *);
-static void push_stack(Graph *);
-static void sdump(Node *);
-
-static void
-dump_graph(Graph *g)
-{ Node *n1;
-
- printf("\n\tnew:\t");
- for (n1 = g->New; n1; n1 = n1->nxt)
- { dump(n1); printf(", "); }
- printf("\n\told:\t");
- for (n1 = g->Old; n1; n1 = n1->nxt)
- { dump(n1); printf(", "); }
- printf("\n\tnxt:\t");
- for (n1 = g->Next; n1; n1 = n1->nxt)
- { dump(n1); printf(", "); }
- printf("\n\tother:\t");
- for (n1 = g->Other; n1; n1 = n1->nxt)
- { dump(n1); printf(", "); }
- printf("\n");
-}
-
-static void
-push_stack(Graph *g)
-{
- if (!g) return;
-
- g->nxt = Nodes_Stack;
- Nodes_Stack = g;
- if (tl_verbose)
- { Symbol *z;
- printf("\nPush %s, from ", g->name->name);
- for (z = g->incoming; z; z = z->next)
- printf("%s, ", z->name);
- dump_graph(g);
- }
- Stack_sz++;
- if (Stack_sz > Stack_mx) Stack_mx = Stack_sz;
-}
-
-static Graph *
-pop_stack(void)
-{ Graph *g = Nodes_Stack;
-
- if (g) Nodes_Stack = g->nxt;
-
- Stack_sz--;
-
- return g;
-}
-
-static char *
-newname(void)
-{ static int cnt = 0;
- static char buf[32];
- sprintf(buf, "S%d", cnt++);
- return buf;
-}
-
-static int
-has_clause(int tok, Graph *p, Node *n)
-{ Node *q, *qq;
-
- switch (n->ntyp) {
- case AND:
- return has_clause(tok, p, n->lft) &&
- has_clause(tok, p, n->rgt);
- case OR:
- return has_clause(tok, p, n->lft) ||
- has_clause(tok, p, n->rgt);
- }
-
- for (q = p->Other; q; q = q->nxt)
- { qq = right_linked(q);
- if (anywhere(tok, n, qq))
- return 1;
- }
- return 0;
-}
-
-static void
-mk_grn(Node *n)
-{ Graph *p;
-
- n = right_linked(n);
-more:
- for (p = Nodes_Set; p; p = p->nxt)
- if (p->outgoing
- && has_clause(AND, p, n))
- { p->isgrn[p->grncnt++] =
- (unsigned char) Red_cnt;
- Lab_cnt++;
- }
-
- if (n->ntyp == U_OPER) /* 3.4.0 */
- { n = n->rgt;
- goto more;
- }
-}
-
-static void
-mk_red(Node *n)
-{ Graph *p;
-
- n = right_linked(n);
- for (p = Nodes_Set; p; p = p->nxt)
- { if (p->outgoing
- && has_clause(0, p, n))
- { if (p->redcnt >= 63)
- Fatal("too many Untils", (char *)0);
- p->isred[p->redcnt++] =
- (unsigned char) Red_cnt;
- Lab_cnt++; Max_Red = Red_cnt;
- } }
-}
-
-static void
-liveness(Node *n)
-{
- if (n)
- switch (n->ntyp) {
-#ifdef NXT
- case NEXT:
- liveness(n->lft);
- break;
-#endif
- case U_OPER:
- Red_cnt++;
- mk_red(n);
- mk_grn(n->rgt);
- /* fall through */
- case V_OPER:
- case OR: case AND:
- liveness(n->lft);
- liveness(n->rgt);
- break;
- }
-}
-
-static Graph *
-findgraph(char *nm)
-{ Graph *p;
- Mapping *m;
-
- for (p = Nodes_Set; p; p = p->nxt)
- if (!strcmp(p->name->name, nm))
- return p;
- for (m = Mapped; m; m = m->nxt)
- if (strcmp(m->from, nm) == 0)
- return m->to;
-
- printf("warning: node %s not found\n", nm);
- return (Graph *) 0;
-}
-
-static void
-Addout(char *to, char *from)
-{ Graph *p = findgraph(from);
- Symbol *s;
-
- if (!p) return;
- s = getsym(tl_lookup(to));
- s->next = p->outgoing;
- p->outgoing = s;
-}
-
-#ifdef NXT
-int
-only_nxt(Node *n)
-{
- switch (n->ntyp) {
- case NEXT:
- return 1;
- case OR:
- case AND:
- return only_nxt(n->rgt) && only_nxt(n->lft);
- default:
- return 0;
- }
-}
-#endif
-
-int
-dump_cond(Node *pp, Node *r, int first)
-{ Node *q;
- int frst = first;
-
- if (!pp) return frst;
-
- q = dupnode(pp);
- q = rewrite(q);
-
- if (q->ntyp == PREDICATE
- || q->ntyp == NOT
-#ifndef NXT
- || q->ntyp == OR
-#endif
- || q->ntyp == FALSE)
- { if (!frst) fprintf(tl_out, " && ");
- dump(q);
- frst = 0;
-#ifdef NXT
- } else if (q->ntyp == OR)
- { if (!frst) fprintf(tl_out, " && ");
- fprintf(tl_out, "((");
- frst = dump_cond(q->lft, r, 1);
-
- if (!frst)
- fprintf(tl_out, ") || (");
- else
- { if (only_nxt(q->lft))
- { fprintf(tl_out, "1))");
- return 0;
- }
- }
-
- frst = dump_cond(q->rgt, r, 1);
-
- if (frst)
- { if (only_nxt(q->rgt))
- fprintf(tl_out, "1");
- else
- fprintf(tl_out, "0");
- frst = 0;
- }
-
- fprintf(tl_out, "))");
-#endif
- } else if (q->ntyp == V_OPER
- && !anywhere(AND, q->rgt, r))
- { frst = dump_cond(q->rgt, r, frst);
- } else if (q->ntyp == AND)
- {
- frst = dump_cond(q->lft, r, frst);
- frst = dump_cond(q->rgt, r, frst);
- }
-
- return frst;
-}
-
-static int
-choueka(Graph *p, int count)
-{ int j, k, incr_cnt = 0;
-
- for (j = count; j <= Max_Red; j++) /* for each acceptance class */
- { int delta = 0;
-
- /* is state p labeled Grn-j OR not Red-j ? */
-
- for (k = 0; k < (int) p->grncnt; k++)
- if (p->isgrn[k] == j)
- { delta = 1;
- break;
- }
- if (delta)
- { incr_cnt++;
- continue;
- }
- for (k = 0; k < (int) p->redcnt; k++)
- if (p->isred[k] == j)
- { delta = 1;
- break;
- }
-
- if (delta) break;
-
- incr_cnt++;
- }
- return incr_cnt;
-}
-
-static int
-set_prefix(char *pref, int count, Graph *r2)
-{ int incr_cnt = 0; /* acceptance class 'count' */
-
- if (Lab_cnt == 0
- || Max_Red == 0)
- sprintf(pref, "accept"); /* new */
- else if (count >= Max_Red)
- sprintf(pref, "T0"); /* cycle */
- else
- { incr_cnt = choueka(r2, count+1);
- if (incr_cnt + count >= Max_Red)
- sprintf(pref, "accept"); /* last hop */
- else
- sprintf(pref, "T%d", count+incr_cnt);
- }
- return incr_cnt;
-}
-
-static void
-fsm_trans(Graph *p, int count, char *curnm)
-{ Graph *r;
- Symbol *s;
- char prefix[128], nwnm[256];
-
- if (!p->outgoing)
- addtrans(p, curnm, False, "accept_all");
-
- for (s = p->outgoing; s; s = s->next)
- { r = findgraph(s->name);
- if (!r) continue;
- if (r->outgoing)
- { (void) set_prefix(prefix, count, r);
- sprintf(nwnm, "%s_%s", prefix, s->name);
- } else
- strcpy(nwnm, "accept_all");
-
- if (tl_verbose)
- { printf("maxred=%d, count=%d, curnm=%s, nwnm=%s ",
- Max_Red, count, curnm, nwnm);
- printf("(greencnt=%d,%d, redcnt=%d,%d)\n",
- r->grncnt, r->isgrn[0],
- r->redcnt, r->isred[0]);
- }
- addtrans(p, curnm, r->Old, nwnm);
- }
-}
-
-static void
-mkbuchi(void)
-{ Graph *p;
- int k;
- char curnm[64];
-
- for (k = 0; k <= Max_Red; k++)
- for (p = Nodes_Set; p; p = p->nxt)
- { if (!p->outgoing)
- continue;
- if (k != 0
- && !strcmp(p->name->name, "init")
- && Max_Red != 0)
- continue;
-
- if (k == Max_Red
- && strcmp(p->name->name, "init") != 0)
- strcpy(curnm, "accept_");
- else
- sprintf(curnm, "T%d_", k);
-
- strcat(curnm, p->name->name);
-
- fsm_trans(p, k, curnm);
- }
- fsm_print();
-}
-
-static Symbol *
-dupSlist(Symbol *s)
-{ Symbol *p1, *p2, *p3, *d = ZS;
-
- for (p1 = s; p1; p1 = p1->next)
- { for (p3 = d; p3; p3 = p3->next)
- { if (!strcmp(p3->name, p1->name))
- break;
- }
- if (p3) continue; /* a duplicate */
-
- p2 = getsym(p1);
- p2->next = d;
- d = p2;
- }
- return d;
-}
-
-static Symbol *
-catSlist(Symbol *a, Symbol *b)
-{ Symbol *p1, *p2, *p3, *tmp;
-
- /* remove duplicates from b */
- for (p1 = a; p1; p1 = p1->next)
- { p3 = ZS;
- for (p2 = b; p2; p2 = p2->next)
- { if (strcmp(p1->name, p2->name))
- { p3 = p2;
- continue;
- }
- tmp = p2->next;
- tfree((void *) p2);
- if (p3)
- p3->next = tmp;
- else
- b = tmp;
- } }
- if (!a) return b;
- if (!b) return a;
- if (!b->next)
- { b->next = a;
- return b;
- }
- /* find end of list */
- for (p1 = a; p1->next; p1 = p1->next)
- ;
- p1->next = b;
- return a;
-}
-
-static void
-fixinit(Node *orig)
-{ Graph *p1, *g;
- Symbol *q1, *q2 = ZS;
-
- ng(tl_lookup("init"), ZS, ZN, ZN, ZN);
- p1 = pop_stack();
- p1->nxt = Nodes_Set;
- p1->Other = p1->Old = orig;
- Nodes_Set = p1;
-
- for (g = Nodes_Set; g; g = g->nxt)
- { for (q1 = g->incoming; q1; q1 = q2)
- { q2 = q1->next;
- Addout(g->name->name, q1->name);
- tfree((void *) q1);
- }
- g->incoming = ZS;
- }
-}
-
-static Node *
-flatten(Node *p)
-{ Node *q, *r, *z = ZN;
-
- for (q = p; q; q = q->nxt)
- { r = dupnode(q);
- if (z)
- z = tl_nn(AND, r, z);
- else
- z = r;
- }
- if (!z) return z;
- z = rewrite(z);
- return z;
-}
-
-static Node *
-Duplicate(Node *n)
-{ Node *n1, *n2, *lst = ZN, *d = ZN;
-
- for (n1 = n; n1; n1 = n1->nxt)
- { n2 = dupnode(n1);
- if (lst)
- { lst->nxt = n2;
- lst = n2;
- } else
- d = lst = n2;
- }
- return d;
-}
-
-static void
-ng(Symbol *s, Symbol *in, Node *isnew, Node *isold, Node *next)
-{ Graph *g = (Graph *) tl_emalloc(sizeof(Graph));
-
- if (s) g->name = s;
- else g->name = tl_lookup(newname());
-
- if (in) g->incoming = dupSlist(in);
- if (isnew) g->New = flatten(isnew);
- if (isold) g->Old = Duplicate(isold);
- if (next) g->Next = flatten(next);
-
- push_stack(g);
-}
-
-static void
-sdump(Node *n)
-{
- switch (n->ntyp) {
- case PREDICATE: strcat(dumpbuf, n->sym->name);
- break;
- case U_OPER: strcat(dumpbuf, "U");
- goto common2;
- case V_OPER: strcat(dumpbuf, "V");
- goto common2;
- case OR: strcat(dumpbuf, "|");
- goto common2;
- case AND: strcat(dumpbuf, "&");
-common2: sdump(n->rgt);
-common1: sdump(n->lft);
- break;
-#ifdef NXT
- case NEXT: strcat(dumpbuf, "X");
- goto common1;
-#endif
- case NOT: strcat(dumpbuf, "!");
- goto common1;
- case TRUE: strcat(dumpbuf, "T");
- break;
- case FALSE: strcat(dumpbuf, "F");
- break;
- default: strcat(dumpbuf, "?");
- break;
- }
-}
-
-Symbol *
-DoDump(Node *n)
-{
- if (!n) return ZS;
-
- if (n->ntyp == PREDICATE)
- return n->sym;
-
- dumpbuf[0] = '\0';
- sdump(n);
- return tl_lookup(dumpbuf);
-}
-
-static int
-not_new(Graph *g)
-{ Graph *q1; Node *tmp, *n1, *n2;
- Mapping *map;
-
- tmp = flatten(g->Old); /* duplicate, collapse, normalize */
- g->Other = g->Old; /* non normalized full version */
- g->Old = tmp;
-
- g->oldstring = DoDump(g->Old);
-
- tmp = flatten(g->Next);
- g->nxtstring = DoDump(tmp);
-
- if (tl_verbose) dump_graph(g);
-
- Debug2("\tformula-old: [%s]\n", g->oldstring?g->oldstring->name:"true");
- Debug2("\tformula-nxt: [%s]\n", g->nxtstring?g->nxtstring->name:"true");
- for (q1 = Nodes_Set; q1; q1 = q1->nxt)
- { Debug2(" compare old to: %s", q1->name->name);
- Debug2(" [%s]", q1->oldstring?q1->oldstring->name:"true");
-
- Debug2(" compare nxt to: %s", q1->name->name);
- Debug2(" [%s]", q1->nxtstring?q1->nxtstring->name:"true");
-
- if (q1->oldstring != g->oldstring
- || q1->nxtstring != g->nxtstring)
- { Debug(" => different\n");
- continue;
- }
- Debug(" => match\n");
-
- if (g->incoming)
- q1->incoming = catSlist(g->incoming, q1->incoming);
-
- /* check if there's anything in g->Other that needs
- adding to q1->Other
- */
- for (n2 = g->Other; n2; n2 = n2->nxt)
- { for (n1 = q1->Other; n1; n1 = n1->nxt)
- if (isequal(n1, n2))
- break;
- if (!n1)
- { Node *n3 = dupnode(n2);
- /* don't mess up n2->nxt */
- n3->nxt = q1->Other;
- q1->Other = n3;
- } }
-
- map = (Mapping *) tl_emalloc(sizeof(Mapping));
- map->from = g->name->name;
- map->to = q1;
- map->nxt = Mapped;
- Mapped = map;
-
- for (n1 = g->Other; n1; n1 = n2)
- { n2 = n1->nxt;
- releasenode(1, n1);
- }
- for (n1 = g->Old; n1; n1 = n2)
- { n2 = n1->nxt;
- releasenode(1, n1);
- }
- for (n1 = g->Next; n1; n1 = n2)
- { n2 = n1->nxt;
- releasenode(1, n1);
- }
- return 1;
- }
-
- if (newstates) tl_verbose=1;
- Debug2(" New Node %s [", g->name->name);
- for (n1 = g->Old; n1; n1 = n1->nxt)
- { Dump(n1); Debug(", "); }
- Debug2("] nr %d\n", Base);
- if (newstates) tl_verbose=0;
-
- Base++;
- g->nxt = Nodes_Set;
- Nodes_Set = g;
-
- return 0;
-}
-
-static void
-expand_g(Graph *g)
-{ Node *now, *n1, *n2, *nx;
- int can_release;
-
- if (!g->New)
- { Debug2("\nDone with %s", g->name->name);
- if (tl_verbose) dump_graph(g);
- if (not_new(g))
- { if (tl_verbose) printf("\tIs Not New\n");
- return;
- }
- if (g->Next)
- { Debug(" Has Next [");
- for (n1 = g->Next; n1; n1 = n1->nxt)
- { Dump(n1); Debug(", "); }
- Debug("]\n");
-
- ng(ZS, getsym(g->name), g->Next, ZN, ZN);
- }
- return;
- }
-
- if (tl_verbose)
- { Symbol *z;
- printf("\nExpand %s, from ", g->name->name);
- for (z = g->incoming; z; z = z->next)
- printf("%s, ", z->name);
- printf("\n\thandle:\t"); Explain(g->New->ntyp);
- dump_graph(g);
- }
-
- if (g->New->ntyp == AND)
- { if (g->New->nxt)
- { n2 = g->New->rgt;
- while (n2->nxt)
- n2 = n2->nxt;
- n2->nxt = g->New->nxt;
- }
- n1 = n2 = g->New->lft;
- while (n2->nxt)
- n2 = n2->nxt;
- n2->nxt = g->New->rgt;
-
- releasenode(0, g->New);
-
- g->New = n1;
- push_stack(g);
- return;
- }
-
- can_release = 0; /* unless it need not go into Old */
- now = g->New;
- g->New = g->New->nxt;
- now->nxt = ZN;
-
- if (now->ntyp != TRUE)
- { if (g->Old)
- { for (n1 = g->Old; n1->nxt; n1 = n1->nxt)
- if (isequal(now, n1))
- { can_release = 1;
- goto out;
- }
- n1->nxt = now;
- } else
- g->Old = now;
- }
-out:
- switch (now->ntyp) {
- case FALSE:
- push_stack(g);
- break;
- case TRUE:
- releasenode(1, now);
- push_stack(g);
- break;
- case PREDICATE:
- case NOT:
- if (can_release) releasenode(1, now);
- push_stack(g);
- break;
- case V_OPER:
- Assert(now->rgt != ZN, now->ntyp);
- Assert(now->lft != ZN, now->ntyp);
- Assert(now->rgt->nxt == ZN, now->ntyp);
- Assert(now->lft->nxt == ZN, now->ntyp);
- n1 = now->rgt;
- n1->nxt = g->New;
-
- if (can_release)
- nx = now;
- else
- nx = getnode(now); /* now also appears in Old */
- nx->nxt = g->Next;
-
- n2 = now->lft;
- n2->nxt = getnode(now->rgt);
- n2->nxt->nxt = g->New;
- g->New = flatten(n2);
- push_stack(g);
- ng(ZS, g->incoming, n1, g->Old, nx);
- break;
-
- case U_OPER:
- Assert(now->rgt->nxt == ZN, now->ntyp);
- Assert(now->lft->nxt == ZN, now->ntyp);
- n1 = now->lft;
-
- if (can_release)
- nx = now;
- else
- nx = getnode(now); /* now also appears in Old */
- nx->nxt = g->Next;
-
- n2 = now->rgt;
- n2->nxt = g->New;
-
- goto common;
-
-#ifdef NXT
- case NEXT:
- Assert(now->lft != ZN, now->ntyp);
- nx = dupnode(now->lft);
- nx->nxt = g->Next;
- g->Next = nx;
- if (can_release) releasenode(0, now);
- push_stack(g);
- break;
-#endif
-
- case OR:
- Assert(now->rgt->nxt == ZN, now->ntyp);
- Assert(now->lft->nxt == ZN, now->ntyp);
- n1 = now->lft;
- nx = g->Next;
-
- n2 = now->rgt;
- n2->nxt = g->New;
-common:
- n1->nxt = g->New;
-
- ng(ZS, g->incoming, n1, g->Old, nx);
- g->New = flatten(n2);
-
- if (can_release) releasenode(1, now);
-
- push_stack(g);
- break;
- }
-}
-
-Node *
-twocases(Node *p)
-{ Node *q;
- /* 1: ([]p1 && []p2) == [](p1 && p2) */
- /* 2: (<>p1 || <>p2) == <>(p1 || p2) */
-
- if (!p) return p;
-
- switch(p->ntyp) {
- case AND:
- case OR:
- case U_OPER:
- case V_OPER:
- p->lft = twocases(p->lft);
- p->rgt = twocases(p->rgt);
- break;
-#ifdef NXT
- case NEXT:
-#endif
- case NOT:
- p->lft = twocases(p->lft);
- break;
-
- default:
- break;
- }
- if (p->ntyp == AND /* 1 */
- && p->lft->ntyp == V_OPER
- && p->lft->lft->ntyp == FALSE
- && p->rgt->ntyp == V_OPER
- && p->rgt->lft->ntyp == FALSE)
- { q = tl_nn(V_OPER, False,
- tl_nn(AND, p->lft->rgt, p->rgt->rgt));
- } else
- if (p->ntyp == OR /* 2 */
- && p->lft->ntyp == U_OPER
- && p->lft->lft->ntyp == TRUE
- && p->rgt->ntyp == U_OPER
- && p->rgt->lft->ntyp == TRUE)
- { q = tl_nn(U_OPER, True,
- tl_nn(OR, p->lft->rgt, p->rgt->rgt));
- } else
- q = p;
- return q;
-}
-
-void
-trans(Node *p)
-{ Node *op;
- Graph *g;
-
- if (!p || tl_errs) return;
-
- p = twocases(p);
-
- if (tl_verbose || tl_terse)
- { fprintf(tl_out, "\t/* Normlzd: ");
- dump(p);
- fprintf(tl_out, " */\n");
- }
- if (tl_terse)
- return;
-
- op = dupnode(p);
-
- ng(ZS, getsym(tl_lookup("init")), p, ZN, ZN);
- while ((g = Nodes_Stack) != (Graph *) 0)
- { Nodes_Stack = g->nxt;
- expand_g(g);
- }
- if (newstates)
- return;
-
- fixinit(p);
- liveness(flatten(op)); /* was: liveness(op); */
-
- mkbuchi();
- if (tl_verbose)
- { printf("/*\n");
- printf(" * %d states in Streett automaton\n", Base);
- printf(" * %d Streett acceptance conditions\n", Max_Red);
- printf(" * %d Buchi states\n", Total);
- printf(" */\n");
- }
-}
projects / lttv.git / blobdiff