ltl2ba-nix/buchi.c
2010-11-29 17:39:18 +01:00

653 lines
19 KiB
C

/***** ltl2ba : buchi.c *****/
/* Written by Denis Oddoux, LIAFA, France */
/* Copyright (c) 2001 Denis Oddoux */
/* Modified by Paul Gastin, LSV, France */
/* Copyright (c) 2007 Paul Gastin */
/* */
/* This program is free software; you can redistribute it and/or modify */
/* it under the terms of the GNU General Public License as published by */
/* the Free Software Foundation; either version 2 of the License, or */
/* (at your option) any later version. */
/* */
/* This program is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
/* GNU General Public License for more details. */
/* */
/* You should have received a copy of the GNU General Public License */
/* along with this program; if not, write to the Free Software */
/* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/
/* */
/* Based on the translation algorithm by Gastin and Oddoux, */
/* presented at the 13th International Conference on Computer Aided */
/* Verification, CAV 2001, Paris, France. */
/* Proceedings - LNCS 2102, pp. 53-65 */
/* */
/* Send bug-reports and/or questions to Paul Gastin */
/* http://www.lsv.ens-cachan.fr/~gastin */
#include "ltl2ba.h"
/********************************************************************\
|* Structures and shared variables *|
\********************************************************************/
extern GState **init, *gstates;
extern struct rusage tr_debut, tr_fin;
extern struct timeval t_diff;
extern int tl_verbose, tl_stats, tl_simp_diff, tl_simp_fly, tl_simp_scc,
init_size, *final;
extern void put_uform(void);
extern FILE *tl_out;
BState *bstack, *bstates, *bremoved;
BScc *scc_stack;
int accept, bstate_count = 0, btrans_count = 0, rank;
/********************************************************************\
|* Simplification of the generalized Buchi automaton *|
\********************************************************************/
void free_bstate(BState *s) /* frees a state and its transitions */
{
free_btrans(s->trans->nxt, s->trans, 1);
tfree(s);
}
BState *remove_bstate(BState *s, BState *s1) /* removes a state */
{
BState *prv = s->prv;
s->prv->nxt = s->nxt;
s->nxt->prv = s->prv;
free_btrans(s->trans->nxt, s->trans, 0);
s->trans = (BTrans *)0;
s->nxt = bremoved->nxt;
bremoved->nxt = s;
s->prv = s1;
for(s1 = bremoved->nxt; s1 != bremoved; s1 = s1->nxt)
if(s1->prv == s)
s1->prv = s->prv;
return prv;
}
void copy_btrans(BTrans *from, BTrans *to) {
to->to = from->to;
copy_set(from->pos, to->pos, 1);
copy_set(from->neg, to->neg, 1);
}
int simplify_btrans() /* simplifies the transitions */
{
BState *s;
BTrans *t, *t1;
int changed = 0;
if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut);
for (s = bstates->nxt; s != bstates; s = s->nxt)
for (t = s->trans->nxt; t != s->trans;) {
t1 = s->trans->nxt;
copy_btrans(t, s->trans);
while((t == t1) || (t->to != t1->to) ||
!included_set(t1->pos, t->pos, 1) ||
!included_set(t1->neg, t->neg, 1))
t1 = t1->nxt;
if(t1 != s->trans) {
BTrans *free = t->nxt;
t->to = free->to;
copy_set(free->pos, t->pos, 1);
copy_set(free->neg, t->neg, 1);
t->nxt = free->nxt;
if(free == s->trans) s->trans = t;
free_btrans(free, 0, 0);
changed++;
}
else
t = t->nxt;
}
if(tl_stats) {
getrusage(RUSAGE_SELF, &tr_fin);
timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
fprintf(tl_out, "\nSimplification of the Buchi automaton - transitions: %lli.%06is",
(long long int)t_diff.tv_sec, t_diff.tv_usec);
fprintf(tl_out, "\n%i transitions removed\n", changed);
}
return changed;
}
int same_btrans(BTrans *s, BTrans *t) /* returns 1 if the transitions are identical */
{
return((s->to == t->to) &&
same_sets(s->pos, t->pos, 1) &&
same_sets(s->neg, t->neg, 1));
}
void remove_btrans(BState *to)
{ /* redirects transitions before removing a state from the automaton */
BState *s;
BTrans *t;
for (s = bstates->nxt; s != bstates; s = s->nxt)
for (t = s->trans->nxt; t != s->trans; t = t->nxt)
if (t->to == to) { /* transition to a state with no transitions */
BTrans *free = t->nxt;
t->to = free->to;
copy_set(free->pos, t->pos, 1);
copy_set(free->neg, t->neg, 1);
t->nxt = free->nxt;
if(free == s->trans) s->trans = t;
free_btrans(free, 0, 0);
}
}
void retarget_all_btrans()
{ /* redirects transitions before removing a state from the automaton */
BState *s;
BTrans *t;
for (s = bstates->nxt; s != bstates; s = s->nxt)
for (t = s->trans->nxt; t != s->trans; t = t->nxt)
if (!t->to->trans) { /* t->to has been removed */
t->to = t->to->prv;
if(!t->to) { /* t->to has no transitions */
BTrans *free = t->nxt;
t->to = free->to;
copy_set(free->pos, t->pos, 1);
copy_set(free->neg, t->neg, 1);
t->nxt = free->nxt;
if(free == s->trans) s->trans = t;
free_btrans(free, 0, 0);
}
}
while(bremoved->nxt != bremoved) { /* clean the 'removed' list */
s = bremoved->nxt;
bremoved->nxt = bremoved->nxt->nxt;
tfree(s);
}
}
int all_btrans_match(BState *a, BState *b) /* decides if the states are equivalent */
{
BTrans *s, *t;
if (((a->final == accept) || (b->final == accept)) &&
(a->final + b->final != 2 * accept) &&
a->incoming >=0 && b->incoming >=0)
return 0; /* the states have to be both final or both non final */
for (s = a->trans->nxt; s != a->trans; s = s->nxt) {
/* all transitions from a appear in b */
copy_btrans(s, b->trans);
t = b->trans->nxt;
while(!same_btrans(s, t))
t = t->nxt;
if(t == b->trans) return 0;
}
for (s = b->trans->nxt; s != b->trans; s = s->nxt) {
/* all transitions from b appear in a */
copy_btrans(s, a->trans);
t = a->trans->nxt;
while(!same_btrans(s, t))
t = t->nxt;
if(t == a->trans) return 0;
}
return 1;
}
int simplify_bstates() /* eliminates redundant states */
{
BState *s, *s1;
int changed = 0;
if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut);
for (s = bstates->nxt; s != bstates; s = s->nxt) {
if(s->trans == s->trans->nxt) { /* s has no transitions */
s = remove_bstate(s, (BState *)0);
changed++;
continue;
}
bstates->trans = s->trans;
bstates->final = s->final;
s1 = s->nxt;
while(!all_btrans_match(s, s1))
s1 = s1->nxt;
if(s1 != bstates) { /* s and s1 are equivalent */
if(s1->incoming == -1)
s1->final = s->final; /* get the good final condition */
s = remove_bstate(s, s1);
changed++;
}
}
retarget_all_btrans();
if(tl_stats) {
getrusage(RUSAGE_SELF, &tr_fin);
timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
fprintf(tl_out, "\nSimplification of the Buchi automaton - states: %lli.%06is",
(long long int)t_diff.tv_sec, t_diff.tv_usec);
fprintf(tl_out, "\n%i states removed\n", changed);
}
return changed;
}
int bdfs(BState *s) {
BTrans *t;
BScc *c;
BScc *scc = (BScc *)tl_emalloc(sizeof(BScc));
scc->bstate = s;
scc->rank = rank;
scc->theta = rank++;
scc->nxt = scc_stack;
scc_stack = scc;
s->incoming = 1;
for (t = s->trans->nxt; t != s->trans; t = t->nxt) {
if (t->to->incoming == 0) {
int result = bdfs(t->to);
scc->theta = min(scc->theta, result);
}
else {
for(c = scc_stack->nxt; c != 0; c = c->nxt)
if(c->bstate == t->to) {
scc->theta = min(scc->theta, c->rank);
break;
}
}
}
if(scc->rank == scc->theta) {
if(scc_stack == scc) { /* s is alone in a scc */
s->incoming = -1;
for (t = s->trans->nxt; t != s->trans; t = t->nxt)
if (t->to == s)
s->incoming = 1;
}
scc_stack = scc->nxt;
}
return scc->theta;
}
void simplify_bscc() {
BState *s;
rank = 1;
scc_stack = 0;
if(bstates == bstates->nxt) return;
for(s = bstates->nxt; s != bstates; s = s->nxt)
s->incoming = 0; /* state color = white */
bdfs(bstates->prv);
for(s = bstates->nxt; s != bstates; s = s->nxt)
if(s->incoming == 0)
remove_bstate(s, 0);
}
/********************************************************************\
|* Generation of the Buchi automaton *|
\********************************************************************/
BState *find_bstate(GState **state, int final, BState *s)
{ /* finds the corresponding state, or creates it */
if((s->gstate == *state) && (s->final == final)) return s; /* same state */
s = bstack->nxt; /* in the stack */
bstack->gstate = *state;
bstack->final = final;
while(!(s->gstate == *state) || !(s->final == final))
s = s->nxt;
if(s != bstack) return s;
s = bstates->nxt; /* in the solved states */
bstates->gstate = *state;
bstates->final = final;
while(!(s->gstate == *state) || !(s->final == final))
s = s->nxt;
if(s != bstates) return s;
s = bremoved->nxt; /* in the removed states */
bremoved->gstate = *state;
bremoved->final = final;
while(!(s->gstate == *state) || !(s->final == final))
s = s->nxt;
if(s != bremoved) return s;
s = (BState *)tl_emalloc(sizeof(BState)); /* creates a new state */
s->gstate = *state;
s->id = (*state)->id;
s->incoming = 0;
s->final = final;
s->trans = emalloc_btrans(); /* sentinel */
s->trans->nxt = s->trans;
s->nxt = bstack->nxt;
bstack->nxt = s;
return s;
}
int next_final(int *set, int fin) /* computes the 'final' value */
{
if((fin != accept) && in_set(set, final[fin + 1]))
return next_final(set, fin + 1);
return fin;
}
void make_btrans(BState *s) /* creates all the transitions from a state */
{
int state_trans = 0;
GTrans *t;
BTrans *t1;
BState *s1;
if(s->gstate->trans)
for(t = s->gstate->trans->nxt; t != s->gstate->trans; t = t->nxt) {
int fin = next_final(t->final, (s->final == accept) ? 0 : s->final);
BState *to = find_bstate(&t->to, fin, s);
for(t1 = s->trans->nxt; t1 != s->trans;) {
if(tl_simp_fly &&
(to == t1->to) &&
included_set(t->pos, t1->pos, 1) &&
included_set(t->neg, t1->neg, 1)) { /* t1 is redondant */
BTrans *free = t1->nxt;
t1->to->incoming--;
t1->to = free->to;
copy_set(free->pos, t1->pos, 1);
copy_set(free->neg, t1->neg, 1);
t1->nxt = free->nxt;
if(free == s->trans) s->trans = t1;
free_btrans(free, 0, 0);
state_trans--;
}
else if(tl_simp_fly &&
(t1->to == to ) &&
included_set(t1->pos, t->pos, 1) &&
included_set(t1->neg, t->neg, 1)) /* t is redondant */
break;
else
t1 = t1->nxt;
}
if(t1 == s->trans) {
BTrans *trans = emalloc_btrans();
trans->to = to;
trans->to->incoming++;
copy_set(t->pos, trans->pos, 1);
copy_set(t->neg, trans->neg, 1);
trans->nxt = s->trans->nxt;
s->trans->nxt = trans;
state_trans++;
}
}
if(tl_simp_fly) {
if(s->trans == s->trans->nxt) { /* s has no transitions */
free_btrans(s->trans->nxt, s->trans, 1);
s->trans = (BTrans *)0;
s->prv = (BState *)0;
s->nxt = bremoved->nxt;
bremoved->nxt = s;
for(s1 = bremoved->nxt; s1 != bremoved; s1 = s1->nxt)
if(s1->prv == s)
s1->prv = (BState *)0;
return;
}
bstates->trans = s->trans;
bstates->final = s->final;
s1 = bstates->nxt;
while(!all_btrans_match(s, s1))
s1 = s1->nxt;
if(s1 != bstates) { /* s and s1 are equivalent */
free_btrans(s->trans->nxt, s->trans, 1);
s->trans = (BTrans *)0;
s->prv = s1;
s->nxt = bremoved->nxt;
bremoved->nxt = s;
for(s1 = bremoved->nxt; s1 != bremoved; s1 = s1->nxt)
if(s1->prv == s)
s1->prv = s->prv;
return;
}
}
s->nxt = bstates->nxt; /* adds the current state to 'bstates' */
s->prv = bstates;
s->nxt->prv = s;
bstates->nxt = s;
btrans_count += state_trans;
bstate_count++;
}
/********************************************************************\
|* Display of the Buchi automaton *|
\********************************************************************/
void print_buchi(BState *s) /* dumps the Buchi automaton */
{
BTrans *t;
if(s == bstates) return;
print_buchi(s->nxt); /* begins with the last state */
fprintf(tl_out, "state ");
if(s->id == -1)
fprintf(tl_out, "init");
else {
if(s->final == accept)
fprintf(tl_out, "accept");
else
fprintf(tl_out, "T%i", s->final);
fprintf(tl_out, "_%i", s->id);
}
fprintf(tl_out, "\n");
for(t = s->trans->nxt; t != s->trans; t = t->nxt) {
if (empty_set(t->pos, 1) && empty_set(t->neg, 1))
fprintf(tl_out, "1");
print_set(t->pos, 1);
if (!empty_set(t->pos, 1) && !empty_set(t->neg, 1)) fprintf(tl_out, " & ");
print_set(t->neg, 2);
fprintf(tl_out, " -> ");
if(t->to->id == -1)
fprintf(tl_out, "init\n");
else {
if(t->to->final == accept)
fprintf(tl_out, "accept");
else
fprintf(tl_out, "T%i", t->to->final);
fprintf(tl_out, "_%i\n", t->to->id);
}
}
}
void print_spin_buchi() {
BTrans *t;
BState *s;
int accept_all = 0;
if(bstates->nxt == bstates) { /* empty automaton */
fprintf(tl_out, "never { /* ");
put_uform();
fprintf(tl_out, " */\n");
fprintf(tl_out, "T0_init:\n");
fprintf(tl_out, "\tfalse;\n");
fprintf(tl_out, "}\n");
return;
}
if(bstates->nxt->nxt == bstates && bstates->nxt->id == 0) { /* true */
fprintf(tl_out, "never { /* ");
put_uform();
fprintf(tl_out, " */\n");
fprintf(tl_out, "accept_init:\n");
fprintf(tl_out, "\tif\n");
fprintf(tl_out, "\t:: (1) -> goto accept_init\n");
fprintf(tl_out, "\tfi;\n");
fprintf(tl_out, "}\n");
return;
}
fprintf(tl_out, "never { /* ");
put_uform();
fprintf(tl_out, " */\n");
for(s = bstates->prv; s != bstates; s = s->prv) {
if(s->id == 0) { /* accept_all at the end */
accept_all = 1;
continue;
}
if(s->final == accept)
fprintf(tl_out, "accept_");
else fprintf(tl_out, "T%i_", s->final);
if(s->id == -1)
fprintf(tl_out, "init:\n");
else fprintf(tl_out, "S%i:\n", s->id);
if(s->trans->nxt == s->trans) {
fprintf(tl_out, "\tfalse;\n");
continue;
}
fprintf(tl_out, "\tif\n");
for(t = s->trans->nxt; t != s->trans; t = t->nxt) {
BTrans *t1;
fprintf(tl_out, "\t:: (");
spin_print_set(t->pos, t->neg);
for(t1 = t; t1->nxt != s->trans; )
if (t1->nxt->to->id == t->to->id &&
t1->nxt->to->final == t->to->final) {
fprintf(tl_out, ") || (");
spin_print_set(t1->nxt->pos, t1->nxt->neg);
t1->nxt = t1->nxt->nxt;
}
else t1 = t1->nxt;
fprintf(tl_out, ") -> goto ");
if(t->to->final == accept)
fprintf(tl_out, "accept_");
else fprintf(tl_out, "T%i_", t->to->final);
if(t->to->id == 0)
fprintf(tl_out, "all\n");
else if(t->to->id == -1)
fprintf(tl_out, "init\n");
else fprintf(tl_out, "S%i\n", t->to->id);
}
fprintf(tl_out, "\tfi;\n");
}
if(accept_all) {
fprintf(tl_out, "accept_all:\n");
fprintf(tl_out, "\tskip\n");
}
fprintf(tl_out, "}\n");
}
/********************************************************************\
|* Main method *|
\********************************************************************/
void mk_buchi()
{/* generates a Buchi automaton from the generalized Buchi automaton */
int i;
BState *s = (BState *)tl_emalloc(sizeof(BState));
GTrans *t;
BTrans *t1;
accept = final[0] - 1;
if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut);
bstack = (BState *)tl_emalloc(sizeof(BState)); /* sentinel */
bstack->nxt = bstack;
bremoved = (BState *)tl_emalloc(sizeof(BState)); /* sentinel */
bremoved->nxt = bremoved;
bstates = (BState *)tl_emalloc(sizeof(BState)); /* sentinel */
bstates->nxt = s;
bstates->prv = s;
s->nxt = bstates; /* creates (unique) inital state */
s->prv = bstates;
s->id = -1;
s->incoming = 1;
s->final = 0;
s->gstate = 0;
s->trans = emalloc_btrans(); /* sentinel */
s->trans->nxt = s->trans;
for(i = 0; i < init_size; i++)
if(init[i])
for(t = init[i]->trans->nxt; t != init[i]->trans; t = t->nxt) {
int fin = next_final(t->final, 0);
BState *to = find_bstate(&t->to, fin, s);
for(t1 = s->trans->nxt; t1 != s->trans;) {
if(tl_simp_fly &&
(to == t1->to) &&
included_set(t->pos, t1->pos, 1) &&
included_set(t->neg, t1->neg, 1)) { /* t1 is redondant */
BTrans *free = t1->nxt;
t1->to->incoming--;
t1->to = free->to;
copy_set(free->pos, t1->pos, 1);
copy_set(free->neg, t1->neg, 1);
t1->nxt = free->nxt;
if(free == s->trans) s->trans = t1;
free_btrans(free, 0, 0);
}
else if(tl_simp_fly &&
(t1->to == to ) &&
included_set(t1->pos, t->pos, 1) &&
included_set(t1->neg, t->neg, 1)) /* t is redondant */
break;
else
t1 = t1->nxt;
}
if(t1 == s->trans) {
BTrans *trans = emalloc_btrans();
trans->to = to;
trans->to->incoming++;
copy_set(t->pos, trans->pos, 1);
copy_set(t->neg, trans->neg, 1);
trans->nxt = s->trans->nxt;
s->trans->nxt = trans;
}
}
while(bstack->nxt != bstack) { /* solves all states in the stack until it is empty */
s = bstack->nxt;
bstack->nxt = bstack->nxt->nxt;
if(!s->incoming) {
free_bstate(s);
continue;
}
make_btrans(s);
}
retarget_all_btrans();
if(tl_stats) {
getrusage(RUSAGE_SELF, &tr_fin);
timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
fprintf(tl_out, "\nBuilding the Buchi automaton : %lli.%06is",
(long long int)t_diff.tv_sec, t_diff.tv_usec);
fprintf(tl_out, "\n%i states, %i transitions\n", bstate_count, btrans_count);
}
if(tl_verbose) {
fprintf(tl_out, "\nBuchi automaton before simplification\n");
print_buchi(bstates->nxt);
if(bstates == bstates->nxt)
fprintf(tl_out, "empty automaton, refuses all words\n");
}
if(tl_simp_diff) {
simplify_btrans();
if(tl_simp_scc) simplify_bscc();
while(simplify_bstates()) { /* simplifies as much as possible */
simplify_btrans();
if(tl_simp_scc) simplify_bscc();
}
if(tl_verbose) {
fprintf(tl_out, "\nBuchi automaton after simplification\n");
print_buchi(bstates->nxt);
if(bstates == bstates->nxt)
fprintf(tl_out, "empty automaton, refuses all words\n");
fprintf(tl_out, "\n");
}
}
print_spin_buchi();
}