diff --git a/ChangeLog b/ChangeLog index ed7f69123..c2869ca09 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,9 @@ 2004-11-24 Alexandre Duret-Lutz + * 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/Makefile.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Add them. diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index b5d8bf6da..383cf8161 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -20,8 +20,7 @@ // 02111-1307, USA. #include "ce.hh" -#include "tgba/bddprint.hh" -#include +#include "tgbaalgos/bfssteps.hh" namespace spot { @@ -75,115 +74,63 @@ namespace spot numbered_state_heap::state_index_p spi = ecs_->h->index(ecs_->aut->get_init_state()); 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 // first SCC, the starting state is the initial state of the // automaton. The destination state is the closest state // from the next SCC. This destination state becomes the // starting state when building a path through the next SCC. + const state* start = spi.first; 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 todo; - // Record the father of each state, while performing the BFS. - typedef std::map father_map; - father_map father; - - // Initial state of the BFS. - const state* start = run_->prefix.back().s; - todo.push_back(start); - - while (!todo.empty()) + struct scc_bfs: bfs_steps + { + explicit_connected_component** scc; + int k; + bool in_next; + scc_bfs(const tgba* a, explicit_connected_component** scc, int k) + : bfs_steps(a), scc(scc), k(k) { - const state* src = todo.front(); - todo.pop_front(); - tgba_succ_iterator* i = ecs_->aut->succ_iter(src); - - for (i->first(); !i->done(); i->next()) - { - const state* dest = i->current_state(); - - // Are we leaving this SCC? - const state* h_dest = scc[k]->has_state(dest); - if (!h_dest) - { - // If we have found a state in the next SCC. - // Unwind the path and populate RUN_->PREFIX. - h_dest = scc[k+1]->has_state(dest); - if (h_dest) - { - tgba_run::steps seq; - - // The condition and acceptance conditions - // for the transition leaving H_DEST will - // be overwritten later when we know them. - - 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); - t = father[t.s]; - } - assert(!run_->prefix.empty()); - // 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()) - { - todo.push_back(h_dest); - tgba_run::step s = { src, - i->current_condition(), - i->current_acceptance_conditions() }; - father[h_dest] = s; - } - } - delete i; } + + virtual const state* + filter(const state* s) + { + const state* h_s = scc[k]->has_state(s); + if (!h_s) + { + h_s = scc[k+1]->has_state(s); + in_next = true; + if (!h_s) + delete s; + } + else + { + in_next = false; + } + return h_s; + } + + virtual bool + match(tgba_run::step&, const state*) + { + return in_next; + } + + + } b(ecs_->aut, scc, k); + + start = b.search(start, run_->prefix); } - accepting_cycle(scc[comp_size - 1], run_->prefix.back().s, + accepting_cycle(scc[comp_size - 1], start, scc[comp_size - 1]->condition); - run_->prefix.pop_back(); // this state belongs to the cycle. for (int j = comp_size - 1; 0 <= j; --j) delete scc[j]; 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_; } @@ -218,76 +165,45 @@ namespace spot const state* substart = start; do { - // Records backlinks to parent state during the BFS. - // (This also stores the propositions of this link.) - std::map father; - - // BFS queue. - std::deque todo; - - // Initial state. - todo.push_back(substart); - - while (!todo.empty()) + struct scc_bfs: bfs_steps + { + const explicit_connected_component* scc; + bool in_next; + bdd& acc_to_traverse; + 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* src = todo.front(); - todo.pop_front(); - tgba_succ_iterator* i = ecs_->aut->succ_iter(src); - for (i->first(); !i->done(); i->next()) - { - 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(); - bdd acc = i->current_acceptance_conditions(); - tgba_run::step s = { src, cond, acc }; - - // If this new step diminish the number of acceptance - // conditions, record the path so far and start a new - // BFS for the remaining acceptance conditions. - // - // 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 - || (acc_to_traverse == bddfalse - && h_dest == start)) - { - acc_to_traverse = less_acc; - - tgba_run::steps p; - - while (s.s != substart) - { - p.push_front(s); - s = father[s.s]; - } - p.push_front(s); - 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 - // for unvisited states. - if (father.find(h_dest) == father.end()) - { - todo.push_back(h_dest); - father[h_dest] = s; - } - } - delete i; } + + virtual const state* + filter(const state* s) + { + const state* h_s = scc->has_state(s); + if (!h_s) + delete s; + return h_s; + } + + virtual bool + match(tgba_run::step& st, const state* s) + { + bdd less_acc = acc_to_traverse - st.acc; + if (less_acc != acc_to_traverse + || (acc_to_traverse == bddfalse + && s == start)) + { + acc_to_traverse = less_acc; + return true; + } + return false; + } + + } b(ecs_->aut, scc, acc_to_traverse, start); + + substart = b.search(substart, run_->cycle); } while (acc_to_traverse != bddfalse || substart != start); }