Blame | Last modification | View Log | RSS feed
/***** 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, state_cnt;
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 *);
void
ini_trans(void)
{
Stack_mx = 0;
Max_Red = 0;
Total = 0;
Mapped = (Mapping *) 0;
Nodes_Set = (Graph *) 0;
Nodes_Stack = (Graph *) 0;
memset(dumpbuf, 0, sizeof(dumpbuf));
Red_cnt = 0;
Lab_cnt = 0;
Base = 0;
Stack_sz = 0;
}
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 char buf[32];
sprintf(buf, "S%d", state_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");
}
}