From fda83b9c51e585da57b4ad54578c6dd0b67bf0b3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 23 Oct 2003 13:05:35 +0000 Subject: [PATCH] * src/tgbaalgos/emptinesscheck.hh (emptiness_check::remove_component, emptiness_check::root_component, emptiness_check::seen_state_num, emptiness_check::suffix): Move in private part. (emptiness_check::arc_accepting, emptiness_check::todo): Move ... * src/tgbaalgos/emptinesscheck.cc (emptiness_check::tgba_emptiness_check): ... as local variables of this function. * src/tgbaalgos/emptinesscheck.hh (emptiness_check::vec_component): Move ... (emptiness_check::counter_example): ... as local variable of this function. * src/tgbaalgos/emptinesscheck.hh (pair_state_iter, triplet): Move ... * src/tgbaalgos/emptinesscheck.cc (pair_state_iter, triplet): ... here. --- src/tgbaalgos/emptinesscheck.hh | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) diff --git a/src/tgbaalgos/emptinesscheck.hh b/src/tgbaalgos/emptinesscheck.hh index 0b32aff83..0f7019049 100644 --- a/src/tgbaalgos/emptinesscheck.hh +++ b/src/tgbaalgos/emptinesscheck.hh @@ -52,15 +52,6 @@ namespace spot typedef std::list cycle_path; public: - /// this function remove all accessible state from a given - /// state. In other words, it removes the strongly connected - /// component that contents this state. - - /// \brief Emptiness check on spot::tgba - void - remove_component(const tgba& aut, seen& state_map, - const spot::state* start_delete); - /// This function returns true if the automata's language is empty, /// and builds a stack of SCC. /// @@ -90,15 +81,20 @@ namespace spot std::ostream& print_result(std::ostream& os, const spot::tgba* aut, const tgba* restrict = 0) const; + private: std::stack arc_accepting; std::stack root_component; seen seen_state_num; state_sequence suffix; cycle_path period; - private: - std::stack todo; - std::vector vec_sequence; + /// \brief Remove a strongly component from the hash. + /// + /// This function remove all accessible state from a given + /// state. In other words, it removes the strongly connected + /// component that contains this state. + void remove_component(const tgba& aut, seen& state_map, + const spot::state* start_delete); /// Called by counter_example to find a path which traverses all /// accepting conditions in the accepted SCC.