diff --git a/ChangeLog b/ChangeLog index a646a300b..2643edcfb 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,12 @@ 2003-10-27 Alexandre Duret-Lutz + * src/tgbaalgos/emptinesscheck.cc (emptiness_check::h_filt, + emptiness_check::~emptiness_check) New methods. + (emptiness_check::check): Release all iterators in todo on exit. + (emptiness_check::counter_example): Rewrite the BFS logic. + * src/tgbaalgos/emptinesscheck.hh (emptiness_check::h_filt, + emptiness_check::~emptiness_check): New methods. + * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::~tgba_tba_proxy_succ_iterator): Delete the proxied iterator. diff --git a/src/tgbaalgos/emptinesscheck.cc b/src/tgbaalgos/emptinesscheck.cc index 507f5acab..3d21b8ef5 100644 --- a/src/tgbaalgos/emptinesscheck.cc +++ b/src/tgbaalgos/emptinesscheck.cc @@ -28,6 +28,29 @@ namespace spot { } + emptiness_check::~emptiness_check() + { + // Free keys in H. + hash_type::iterator i = h.begin(); + while (i != h.end()) + { + // Advance the iterator before deleting the key. + const state* s = i->first; + ++i; + delete s; + } + } + + const state* + emptiness_check::h_filt(const state* s) const + { + hash_type::const_iterator i = h.find(s); + assert(i != h.end()); + if (s != i->first) + delete s; + return i->first; + } + void emptiness_check::remove_component(const state* from) { @@ -200,8 +223,16 @@ namespace spot root.top().condition |= acc; if (root.top().condition == aut_->all_accepting_conditions()) - // We have found an accepting SCC. - return false; + { + // We have found an accepting SCC. + // Release all iterators in TODO. + while (!todo.empty()) + { + delete todo.top().second; + todo.pop(); + } + return false; + } } // This automaton recognize no word. return true; @@ -254,6 +285,7 @@ namespace spot emptiness_check::counter_example() { assert(!root.empty()); + assert(suffix.empty()); int comp_size = root.size(); // Transform the stack of connected component into an array. @@ -282,102 +314,87 @@ namespace spot scc[j - 1].state_set.insert(i->first); } - // seqs[i] is a sequence between SCC i and SCC i+1. - state_sequence* seqs = new state_sequence[comp_size - 1]; - // FIFO for the breadth-first search. - std::deque todo; + suffix.push_front(h_filt(aut_->get_init_state())); - // Record the father of each state, while performing the BFS. - typedef std::map father_map; - father_map father; - - state_sequence seq; - - state* start_state = aut_->get_init_state(); - if (comp_size != 1) + // 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 though the next SCC. + for (int k = 0; k < comp_size - 1; ++k) { - tgba_succ_iterator* i = aut_->succ_iter(start_state); - todo.push_back(pair_state_iter(start_state, i)); + // FIFO for the breadth-first search. + // (we are looking for the closest state in the next SCC.) + std::deque todo; - for (int k = 0; k < comp_size - 1; ++k) + // 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 = suffix.back(); + { + tgba_succ_iterator* i = aut_->succ_iter(start); + todo.push_back(pair_state_iter(start, i)); + } + + while (!todo.empty()) { - // We build a path trought all SCC in the stack: a - // possible prefix for a counter example. - while (!todo.empty()) - { - pair_state_iter started_from = todo.front(); - todo.pop_front(); + const state* src = todo.front().first; + tgba_succ_iterator* i = todo.front().second; + todo.pop_front(); - for (started_from.second->first(); - !started_from.second->done(); - started_from.second->next()) + for (i->first(); !i->done(); i->next()) + { + const state* dest = i->current_state(); + + // Are we leaving this SCC? + if (!scc[k].has_state(dest)) { - const state* curr_state = - started_from.second->current_state(); - if (scc[k+1].has_state(curr_state)) + // If we have found a state in the next SCC. + // Unwind the path and populate SUFFIX. + if (scc[k+1].has_state(dest)) { - const state* curr_father = started_from.first; - seq.push_front(curr_state); - seq.push_front(curr_father); - hash_type::iterator i_2 = h.find(curr_father); - assert(i_2 != h.end()); - while (scc[k].index < i_2->second) + state_sequence seq; + + seq.push_front(h_filt(dest)); + while (src->compare(start)) { - assert(i_2->second != 1); - assert(father.find(curr_father) != father.end()); - const state* f = father[curr_father]; - seq.push_front(f); - curr_father = f; - i_2 = h.find(curr_father); - assert(i_2 != h.end()); + seq.push_front(src); + src = father[src]; + } + // Append SEQ to SUFFIX. + suffix.splice(suffix.end(), seq); + // Exit this BFS for this SCC. + while (!todo.empty()) + { + delete todo.front().second; + todo.pop_front(); } - seqs[k] = seq; - seq.clear(); - todo.clear(); break; } - else - { - if (scc[k].has_state(curr_state)) - { - father_map::iterator i_path = - father.find(curr_state); - hash_type::iterator i_seen = h.find(curr_state); + // Restrict the BFS to state inside the SCC. + delete dest; + continue; + } - if (i_seen != h.end() - && i_seen->second > 0 - && i_path == father.end()) - { - todo. - push_back(pair_state_iter(curr_state, - aut_->succ_iter(curr_state))); - father[curr_state] = started_from.first; - } - } - } + dest = h_filt(dest); + if (father.find(dest) == father.end()) + { + todo.push_back(pair_state_iter(dest, + aut_->succ_iter(dest))); + father[dest] = src; } } - assert(!seqs[k].empty()); - todo. - push_back(pair_state_iter(seqs[k].back(), - aut_->succ_iter(seqs[k].back()))); + delete i; } } - else - { - suffix.push_front(start_state); - } - for (int n_ = 0; n_ < comp_size - 1; ++n_) - for (state_sequence::iterator it = seqs[n_].begin(); - it != seqs[n_].end(); ++it) - suffix.push_back(*it); - suffix.unique(); + accepting_path(scc[comp_size - 1], suffix.back(), scc[comp_size - 1].condition); delete[] scc; - delete[] seqs; } void diff --git a/src/tgbaalgos/emptinesscheck.hh b/src/tgbaalgos/emptinesscheck.hh index e039f7651..8352678b4 100644 --- a/src/tgbaalgos/emptinesscheck.hh +++ b/src/tgbaalgos/emptinesscheck.hh @@ -60,6 +60,7 @@ namespace spot typedef std::list cycle_path; public: emptiness_check(const tgba* a); + ~emptiness_check(); /// This function returns true if the automata's language is empty, /// and builds a stack of SCC. @@ -81,6 +82,13 @@ namespace spot state_ptr_hash, state_ptr_equal> hash_type; hash_type h; ///< Map of visited states. + /// \brief Return a state which is equal to \a s, but is in \c h, + /// and free \a s if it is different. Doing so simplify memory + /// management, because we don't have to track which state need + /// to be kept or deallocated: all key in \c h should last for + /// the whole life of the emptiness_check. + const state* h_filt(const state* s) const; + /// \brief Remove a strongly component from the hash. /// /// This function remove all accessible state from a given