123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875 |
- /***** 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[128];
- 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->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:
- 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");
- }
- }
|