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.

ChangeLog

@@ -1,3 +1,12 @@
+2009-05-31  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	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  <adl@lrde.epita.fr>
 
 	Test "ltl2tgba -FC" and plug the memory leaks of scc_map.

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 \

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);
-  }
 }

src/tgba/futurecondcol.hh

@@ -20,8 +20,7 @@
 #ifndef SPOT_TGBA_FUTURECONDCOL_HH
 # define SPOT_TGBA_FUTURECONDCOL_HH
 
-#include "tgbaexplicit.hh"
+#include "tgbascc.hh"
-#include "tgbaalgos/scc.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
+  protected:
-    // 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:
     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().
   };
 
 }

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 <sstream>
+#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);
+  }
+}

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