diff --git a/ChangeLog b/ChangeLog index f76af1a55..2b83fb1b1 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2009-05-31 Alexandre Duret-Lutz + + Lift the SCC computation off future_condition_collectors, into + a new tgba_scc class. + + * src/tgba/futurecondcol.cc, src/tgba/futurecondcol.hh: Move + all delegation functions and scc_map into ... + * src/tgba/tgbascc.cc, src/tgba/tgbascc.hh: ... these new files. + 2009-05-28 Alexandre Duret-Lutz Test "ltl2tgba -FC" and plug the memory leaks of scc_map. diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 9f664c58b..322a8e562 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -40,6 +40,7 @@ tgba_HEADERS = \ tgbabddconcreteproduct.hh \ tgbabddcoredata.hh \ tgbabddfactory.hh \ + tgbascc.hh \ tgbaexplicit.hh \ tgbaproduct.hh \ tgbatba.hh \ @@ -58,6 +59,7 @@ libtgba_la_SOURCES = \ tgbabddconcretefactory.cc \ tgbabddconcreteproduct.cc \ tgbabddcoredata.cc \ + tgbascc.cc \ tgbaexplicit.cc \ tgbaproduct.cc \ tgbatba.cc \ diff --git a/src/tgba/futurecondcol.cc b/src/tgba/futurecondcol.cc index 563fadb9a..8bef890fb 100644 --- a/src/tgba/futurecondcol.cc +++ b/src/tgba/futurecondcol.cc @@ -44,12 +44,11 @@ namespace spot future_conditions_collector::future_conditions_collector(const tgba* aut, bool show) - : aut_(aut), scc_map_(aut), show_(show) + : tgba_scc(aut, show), + // Initialize future_conds_ with as much empty + // "cond_set"s as there are SCCs. + future_conds_(scc_map_.scc_count()) { - scc_map_.build_map(); - // Initialize future_conds_ with as much empty "cond_set"s as - // there are SCCs. - future_conds_ = fc_map(scc_map_.scc_count()); // Fill future_conds by recursively visiting the (acyclic) graph // of SCCs. map_builder_(scc_map_.initial()); @@ -68,26 +67,6 @@ namespace spot return future_conds_[s]; } - state* - future_conditions_collector::get_init_state() const - { - return aut_->get_init_state(); - } - - tgba_succ_iterator* - future_conditions_collector::succ_iter(const state* local_state, - const state* global_state, - const tgba* global_automaton) const - { - return aut_->succ_iter(local_state, global_state, global_automaton); - } - - bdd_dict* - future_conditions_collector::get_dict() const - { - return aut_->get_dict(); - } - std::string future_conditions_collector::format_state(const state* state) const { @@ -95,7 +74,7 @@ namespace spot return aut_->format_state(state); std::ostringstream str; - str << aut_->format_state(state); + str << this->tgba_scc::format_state(state); str << "\\n["; const cond_set& c = future_conditions(state); for (cond_set::const_iterator i = c.begin(); i != c.end(); ++i) @@ -107,44 +86,4 @@ namespace spot str << "]"; return str.str(); } - - std::string - future_conditions_collector::transition_annotation - (const tgba_succ_iterator* t) const - { - return aut_->transition_annotation(t); - } - - state* - future_conditions_collector::project_state(const state* s, - const tgba* t) const - { - return aut_->project_state(s, t); - } - - bdd - future_conditions_collector::all_acceptance_conditions() const - { - return aut_->all_acceptance_conditions(); - } - - bdd - future_conditions_collector::neg_acceptance_conditions() const - { - return aut_->neg_acceptance_conditions(); - } - - bdd - future_conditions_collector::compute_support_conditions - (const state* state) const - { - return aut_->support_conditions(state); - } - - bdd - future_conditions_collector::compute_support_variables - (const state* state) const - { - return aut_->support_variables(state); - } } diff --git a/src/tgba/futurecondcol.hh b/src/tgba/futurecondcol.hh index b0aeab524..82669553a 100644 --- a/src/tgba/futurecondcol.hh +++ b/src/tgba/futurecondcol.hh @@ -20,8 +20,7 @@ #ifndef SPOT_TGBA_FUTURECONDCOL_HH # define SPOT_TGBA_FUTURECONDCOL_HH -#include "tgbaexplicit.hh" -#include "tgbaalgos/scc.hh" +#include "tgbascc.hh" namespace spot { @@ -32,10 +31,10 @@ namespace spot /// This class is a spot::tgba wrapper that simply add a new method, /// future_conditions(), to any spot::tgba. /// - /// This new methods returns a set of conditions that can be + /// This new method returns a set of conditions that can be /// seen on a transitions accessible (maybe indirectly) from /// the given state. - class future_conditions_collector : public tgba + class future_conditions_collector : public tgba_scc { public: typedef scc_map::cond_set cond_set; @@ -49,6 +48,7 @@ namespace spot future_conditions_collector(const tgba* aut, bool show = false); virtual ~future_conditions_collector(); + /// Returns the set of future conditions visible after \a s const cond_set& future_conditions(const spot::state* s) const; /// \brief Format a state for output. @@ -58,34 +58,11 @@ namespace spot /// state by future_conditions() in the output string. virtual std::string format_state(const state* state) const; - // The following methods simply delegate their work to the wrapped - // tgba. - - virtual state* get_init_state() const; - virtual tgba_succ_iterator* - succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0) const; - virtual bdd_dict* get_dict() const; - - virtual std::string - transition_annotation(const tgba_succ_iterator* t) const; - virtual state* project_state(const state* s, const tgba* t) const; - virtual bdd all_acceptance_conditions() const; - virtual bdd neg_acceptance_conditions() const; - - virtual bdd compute_support_conditions(const state* state) const; - virtual bdd compute_support_variables(const state* state) const; - - private: + protected: void map_builder_(unsigned s); - const tgba* aut_; // The wrapped TGBA. fc_map future_conds_; // The map of future conditions for each // strongly connected component. - scc_map scc_map_; // SCC informations. - bool show_; // Wether to show future conditions - // in the output of format_state(). }; } diff --git a/src/tgba/tgbascc.cc b/src/tgba/tgbascc.cc new file mode 100644 index 000000000..5981da4bf --- /dev/null +++ b/src/tgba/tgbascc.cc @@ -0,0 +1,113 @@ +// Copyright (C) 2009 Laboratoire de recherche et développement de l'Epita. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include "tgbascc.hh" + +namespace spot +{ + + tgba_scc::tgba_scc(const tgba* aut, bool show) + : aut_(aut), scc_map_(aut), show_(show) + { + scc_map_.build_map(); + } + + tgba_scc::~tgba_scc() + { + } + + unsigned + tgba_scc::scc_of_state(const spot::state* st) const + { + return scc_map_.scc_of_state(st); + } + + state* + tgba_scc::get_init_state() const + { + return aut_->get_init_state(); + } + + tgba_succ_iterator* + tgba_scc::succ_iter(const state* local_state, + const state* global_state, + const tgba* global_automaton) const + { + return aut_->succ_iter(local_state, global_state, global_automaton); + } + + bdd_dict* + tgba_scc::get_dict() const + { + return aut_->get_dict(); + } + + std::string + tgba_scc::format_state(const state* state) const + { + if (!show_) + return aut_->format_state(state); + + std::ostringstream str; + str << aut_->format_state(state); + str << "\\nSCC #" << scc_of_state(state); + return str.str(); + } + + std::string + tgba_scc::transition_annotation + (const tgba_succ_iterator* t) const + { + return aut_->transition_annotation(t); + } + + state* + tgba_scc::project_state(const state* s, + const tgba* t) const + { + return aut_->project_state(s, t); + } + + bdd + tgba_scc::all_acceptance_conditions() const + { + return aut_->all_acceptance_conditions(); + } + + bdd + tgba_scc::neg_acceptance_conditions() const + { + return aut_->neg_acceptance_conditions(); + } + + bdd + tgba_scc::compute_support_conditions + (const state* state) const + { + return aut_->support_conditions(state); + } + + bdd + tgba_scc::compute_support_variables + (const state* state) const + { + return aut_->support_variables(state); + } +} diff --git a/src/tgba/tgbascc.hh b/src/tgba/tgbascc.hh new file mode 100644 index 000000000..4737cad19 --- /dev/null +++ b/src/tgba/tgbascc.hh @@ -0,0 +1,84 @@ +// Copyright (C) 2009 Laboratoire de recherche et développement de l'Epita. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBA_TGBASCC_HH +# define SPOT_TGBA_TGBASCC_HH + +#include "tgba.hh" +#include "tgbaalgos/scc.hh" + +namespace spot +{ + + /// \brief Wrap a tgba to offer information about strongly connected + /// components. + /// \ingroup tgba + /// + /// This class is a spot::tgba wrapper that simply add a new method + /// scc_of_state() to retrieve the number of a SCC a state belongs to. + class tgba_scc : public tgba + { + public: + /// \brief Create a tgba_scc wrapper for \a aut. + /// + /// If \a show is set to true, then the format_state() method will + /// include the SCC number computed for the given state in its + /// output string. + tgba_scc(const tgba* aut, bool show = false); + virtual ~tgba_scc(); + + /// Returns the number of the SCC \a s belongs to. + unsigned scc_of_state(const spot::state* s) const; + + /// \brief Format a state for output. + /// + /// If the constructor was called with \a show set to true, then + /// this method will include the SCC number computed for \a + /// state in the output string. + virtual std::string format_state(const state* state) const; + + // The following methods simply delegate their work to the wrapped + // tgba. + + virtual state* get_init_state() const; + virtual tgba_succ_iterator* + succ_iter(const state* local_state, + const state* global_state = 0, + const tgba* global_automaton = 0) const; + virtual bdd_dict* get_dict() const; + + virtual std::string + transition_annotation(const tgba_succ_iterator* t) const; + virtual state* project_state(const state* s, const tgba* t) const; + virtual bdd all_acceptance_conditions() const; + virtual bdd neg_acceptance_conditions() const; + + virtual bdd compute_support_conditions(const state* state) const; + virtual bdd compute_support_variables(const state* state) const; + + protected: + const tgba* aut_; // The wrapped TGBA. + scc_map scc_map_; // SCC informations. + bool show_; // Wether to show future conditions + // in the output of format_state(). + }; + +} + +#endif // SPOT_TGBA_TGBASCC_HH