diff --git a/ChangeLog b/ChangeLog index 2643edcfb..07088fa36 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,11 @@ 2003-10-27 Alexandre Duret-Lutz + * src/tgbaalgos/emptinesscheck.cc (connected_component): Split + into ... + (emptiness_check::connected_component, + emptiness_check::connected_component_set): ... these. + * src/tgbaalgos/emptinesscheck.cc: Adjust. + * src/tgbaalgos/emptinesscheck.cc (emptiness_check::h_filt, emptiness_check::~emptiness_check) New methods. (emptiness_check::check): Release all iterators in todo on exit. diff --git a/src/tgbaalgos/emptinesscheck.cc b/src/tgbaalgos/emptinesscheck.cc index 3d21b8ef5..9733ff82e 100644 --- a/src/tgbaalgos/emptinesscheck.cc +++ b/src/tgbaalgos/emptinesscheck.cc @@ -10,16 +10,16 @@ namespace spot typedef std::pair pair_state_iter; typedef std::pair triplet; - connected_component::connected_component(int i) + emptiness_check::connected_component::connected_component(int i) { index = i; condition = bddfalse; } bool - connected_component::has_state(const state* s) const + emptiness_check::connected_component_set::has_state(const state* s) const { - return state_set.find(s) != state_set.end(); + return states.find(s) != states.end(); } @@ -289,10 +289,11 @@ namespace spot int comp_size = root.size(); // Transform the stack of connected component into an array. - connected_component* scc = new connected_component[comp_size]; + connected_component_set* scc = new connected_component_set[comp_size]; for (int j = comp_size - 1; 0 <= j; --j) { - scc[j] = root.top(); + scc[j].index = root.top().index; + scc[j].condition = root.top().condition; root.pop(); } assert(root.empty()); @@ -311,7 +312,7 @@ namespace spot for (j = 1; j < comp_size; ++j) if (index < scc[j].index) break; - scc[j - 1].state_set.insert(i->first); + scc[j - 1].states.insert(i->first); } suffix.push_front(h_filt(aut_->get_init_state())); @@ -398,7 +399,7 @@ namespace spot } void - emptiness_check::complete_cycle(const connected_component& comp_path, + emptiness_check::complete_cycle(const connected_component_set& comp_path, const state* from_state, const state* to_state) { @@ -452,7 +453,7 @@ namespace spot // FIXME: Derecursive this function. void - emptiness_check::accepting_path(const connected_component& comp_path, + emptiness_check::accepting_path(const connected_component_set& comp_path, const state* start_path, bdd to_accept) { hash_type seen_priority; diff --git a/src/tgbaalgos/emptinesscheck.hh b/src/tgbaalgos/emptinesscheck.hh index 8352678b4..80ac7030e 100644 --- a/src/tgbaalgos/emptinesscheck.hh +++ b/src/tgbaalgos/emptinesscheck.hh @@ -11,28 +11,6 @@ namespace spot { - class connected_component - { - // During the Depth path we keep the connected component that we met. - public: - connected_component(int index = -1); - - public: - int index; - /// The bdd condition is the union of all accepting condition of - /// transitions which connect the states of the connected component. - bdd condition; - - typedef Sgi::hash_set set_type; - /// for the counter example we need to know all the states of the - /// component - set_type state_set; - - /// Check if the SCC contains states \a s. - bool has_state(const state* s) const; - }; - /// \brief Check whether the language of an automate is empty. /// /// This is based on the following paper. @@ -73,6 +51,31 @@ namespace spot const tgba* restrict = 0) const; private: + + struct connected_component + { + // During the Depth path we keep the connected component that we met. + public: + connected_component(int index = -1); + + int index; + /// The bdd condition is the union of all accepting condition of + /// transitions which connect the states of the connected component. + bdd condition; + }; + + struct connected_component_set: public connected_component + { + typedef Sgi::hash_set set_type; + /// for the counter example we need to know all the states of the + /// component + set_type states; + + /// Check if the SCC contains states \a s. + bool has_state(const state* s) const; + }; + const tgba* aut_; std::stack root; state_sequence suffix; @@ -98,12 +101,12 @@ namespace spot /// Called by counter_example to find a path which traverses all /// accepting conditions in the accepted SCC. - void accepting_path (const connected_component& comp_path, + void accepting_path (const connected_component_set& comp_path, const state* start_path, bdd to_accept); /// Complete a cycle that caraterise the period of the counter /// example. Append a sequence to the path given by accepting_path. - void complete_cycle(const connected_component& comp_path, + void complete_cycle(const connected_component_set& comp_path, const state* from_state,const state* to_state); }; }