876 lines
16 KiB
C
876 lines
16 KiB
C
/***** 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");
|
|
}
|
|
}
|