alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run,

Browse source 
couvreur99_check_result::accepting_cycle): Rewrite the BFSs using
the bfs_steps class.
This commit is contained in:
Alexandre Duret-Lutz 2004-11-24 15:36:56 +00:00
parent 2b74398a62
commit c1fd4d1138
2 changed files with 80 additions and 160 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,5 +1,9 @@
2004-11-24 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-11-24 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run,
couvreur99_check_result::accepting_cycle): Rewrite the BFSs using
the bfs_steps class.
* src/tgbaalgos/bfssteps.hh, src/tgbaalgos/bfssteps.cc: New files. * src/tgbaalgos/bfssteps.hh, src/tgbaalgos/bfssteps.cc: New files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them. libtgbaalgos_la_SOURCES): Add them.

200
src/tgbaalgos/gtec/ce.cc
View file

@ -20,8 +20,7 @@
// 02111-1307, USA. // 02111-1307, USA.
#include "ce.hh" #include "ce.hh"
#include "tgba/bddprint.hh" #include "tgbaalgos/bfssteps.hh"
#include <map>
namespace spot namespace spot
{ {
@ -75,115 +74,63 @@ namespace spot
numbered_state_heap::state_index_p spi = numbered_state_heap::state_index_p spi =
ecs_->h->index(ecs_->aut->get_init_state()); ecs_->h->index(ecs_->aut->get_init_state());
assert(spi.first); assert(spi.first);
// This incomplete starting step will be overwritten later.
tgba_run::step s = { spi.first, bddtrue, bddfalse };
run_->prefix.push_front(s);
// We build a path trough each SCC in the stack. For the // We build a path trough each SCC in the stack. For the
// first SCC, the starting state is the initial state of the // first SCC, the starting state is the initial state of the
// automaton. The destination state is the closest state // automaton. The destination state is the closest state
// from the next SCC. This destination state becomes the // from the next SCC. This destination state becomes the
// starting state when building a path through the next SCC. // starting state when building a path through the next SCC.
const state* start = spi.first;
for (int k = 0; k < comp_size - 1; ++k) for (int k = 0; k < comp_size - 1; ++k)
{ {
// FIFO for the breadth-first search.
// (we are looking for the closest state in the next SCC.)
std::deque<const state*> todo;
// Record the father of each state, while performing the BFS. struct scc_bfs: bfs_steps
typedef std::map<const state*, tgba_run::step,
state_ptr_less_than> father_map;
father_map father;
// Initial state of the BFS.
const state* start = run_->prefix.back().s;
todo.push_back(start);
while (!todo.empty())
{ {
const state* src = todo.front(); explicit_connected_component** scc;
todo.pop_front(); int k;
tgba_succ_iterator* i = ecs_->aut->succ_iter(src); bool in_next;
scc_bfs(const tgba* a, explicit_connected_component** scc, int k)
for (i->first(); !i->done(); i->next()) : bfs_steps(a), scc(scc), k(k)
{ {
const state* dest = i->current_state(); }
// Are we leaving this SCC? virtual const state*
const state* h_dest = scc[k]->has_state(dest); filter(const state* s)
if (!h_dest)
{ {
// If we have found a state in the next SCC. const state* h_s = scc[k]->has_state(s);
// Unwind the path and populate RUN_->PREFIX. if (!h_s)
h_dest = scc[k+1]->has_state(dest);
if (h_dest)
{ {
tgba_run::steps seq; h_s = scc[k+1]->has_state(s);
in_next = true;
// The condition and acceptance conditions if (!h_s)
// for the transition leaving H_DEST will delete s;
// be overwritten later when we know them. }
else
tgba_run::step s = { h_dest, bddtrue, bddfalse };
seq.push_front(s);
// Now unwind our track until we reach START.
tgba_run::step t =
{ src,
i->current_condition(),
i->current_acceptance_conditions() };
while (t.s->compare(start))
{ {
seq.push_front(t); in_next = false;
t = father[t.s];
} }
assert(!run_->prefix.empty()); return h_s;
// Overwrite the incomplete starting step.
run_->prefix.back() = t;
// Append SEQ to RUN_->PREFIX.
run_->prefix.splice(run_->prefix.end(), seq);
// Exit this BFS for this SCC.
todo.clear();
break;
}
// Restrict the BFS to state inside the SCC.
delete dest;
continue;
} }
if (father.find(h_dest) == father.end()) virtual bool
match(tgba_run::step&, const state*)
{ {
todo.push_back(h_dest); return in_next;
tgba_run::step s = { src,
i->current_condition(),
i->current_acceptance_conditions() };
father[h_dest] = s;
}
}
delete i;
}
} }
accepting_cycle(scc[comp_size - 1], run_->prefix.back().s,
} b(ecs_->aut, scc, k);
start = b.search(start, run_->prefix);
}
accepting_cycle(scc[comp_size - 1], start,
scc[comp_size - 1]->condition); scc[comp_size - 1]->condition);
run_->prefix.pop_back(); // this state belongs to the cycle.
for (int j = comp_size - 1; 0 <= j; --j) for (int j = comp_size - 1; 0 <= j; --j)
delete scc[j]; delete scc[j];
delete[] scc; delete[] scc;
// Clone every state in the run before returning it. (We didn't
// do that before in the algorithm, because it's easier to follow
// if every state manipulated is the instance in the hash table.)
for (tgba_run::steps::iterator i = run_->prefix.begin();
i != run_->prefix.end(); ++i)
i->s = i->s->clone();
for (tgba_run::steps::iterator i = run_->cycle.begin();
i != run_->cycle.end(); ++i)
i->s = i->s->clone();
return run_; return run_;
} }
@ -218,76 +165,45 @@ namespace spot
const state* substart = start; const state* substart = start;
do do
{ {
// Records backlinks to parent state during the BFS. struct scc_bfs: bfs_steps
// (This also stores the propositions of this link.)
std::map<const state*, tgba_run::step, state_ptr_less_than> father;
// BFS queue.
std::deque<const state*> todo;
// Initial state.
todo.push_back(substart);
while (!todo.empty())
{ {
const state* src = todo.front(); const explicit_connected_component* scc;
todo.pop_front(); bool in_next;
tgba_succ_iterator* i = ecs_->aut->succ_iter(src); bdd& acc_to_traverse;
for (i->first(); !i->done(); i->next()) const state* start;
scc_bfs(const tgba* a, const explicit_connected_component* scc,
bdd& acc_to_traverse, const state* start)
: bfs_steps(a), scc(scc), acc_to_traverse(acc_to_traverse),
start(start)
{ {
const state* dest = i->current_state();
// Do not escape this SCC
const state* h_dest = scc->has_state(dest);
if (!h_dest)
{
delete dest;
continue;
} }
bdd cond = i->current_condition(); virtual const state*
bdd acc = i->current_acceptance_conditions(); filter(const state* s)
tgba_run::step s = { src, cond, acc }; {
const state* h_s = scc->has_state(s);
if (!h_s)
delete s;
return h_s;
}
// If this new step diminish the number of acceptance virtual bool
// conditions, record the path so far and start a new match(tgba_run::step& st, const state* s)
// BFS for the remaining acceptance conditions. {
// bdd less_acc = acc_to_traverse - st.acc;
// If we have already collected all acceptance conditions,
// we stop if we cycle back to the start of the cycle.
bdd less_acc = acc_to_traverse - acc;
if (less_acc != acc_to_traverse if (less_acc != acc_to_traverse
|| (acc_to_traverse == bddfalse || (acc_to_traverse == bddfalse
&& h_dest == start)) && s == start))
{ {
acc_to_traverse = less_acc; acc_to_traverse = less_acc;
return true;
tgba_run::steps p;
while (s.s != substart)
{
p.push_front(s);
s = father[s.s];
} }
p.push_front(s); return false;
run_->cycle.splice(run_->cycle.end(), p);
// Exit this BFS, and start a new one at h_dest.
todo.clear();
substart = h_dest;
break;
} }
// Common case: record backlinks and continue BFS } b(ecs_->aut, scc, acc_to_traverse, start);
// for unvisited states.
if (father.find(h_dest) == father.end()) substart = b.search(substart, run_->cycle);
{
todo.push_back(h_dest);
father[h_dest] = s;
}
}
delete i;
}
} }
while (acc_to_traverse != bddfalse || substart != start); while (acc_to_traverse != bddfalse || substart != start);
} }