From 9909699c630783ba76cf50c547b8c0dde02f4271 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 21 May 2014 14:53:03 +0200
Subject: [PATCH] implement scc_filter_states for tgba_digraph

* src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/sccfilter.hh (scc_filter_states): New overload taking
a tgba_digraph and some scc_info.
---
 src/tgbaalgos/sccfilter.cc | 53 +++++++++++++++++++++++++++++++++++++-
 src/tgbaalgos/sccfilter.hh | 14 ++++++++--
 2 files changed, 64 insertions(+), 3 deletions(-)

diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc
index 0be2216f8..9efab7da9 100644
--- a/src/tgbaalgos/sccfilter.cc
+++ b/src/tgbaalgos/sccfilter.cc
@@ -17,10 +17,11 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-#include "sccfilter.hh"
 #include "tgba/tgbaexplicit.hh"
+#include "sccfilter.hh"
 #include "reachiter.hh"
 #include "tgbaalgos/scc.hh"
+#include "tgbaalgos/sccinfo.hh"
 
 namespace spot
 {
@@ -555,6 +556,10 @@ namespace spot
 
   tgba* scc_filter_states(const tgba* aut, scc_map* given_sm)
   {
+    const tgba_digraph* autg = dynamic_cast<const tgba_digraph*>(aut);
+    if (autg && !given_sm)
+      return scc_filter_states(autg, nullptr);
+
     scc_map* sm = given_sm;
     if (!sm)
       {
@@ -604,4 +609,50 @@ namespace spot
     return ret;
   }
 
+  tgba_digraph* scc_filter_states(const tgba_digraph* aut, scc_info* given_si)
+  {
+    // Compute scc_info if not supplied.
+    scc_info* si = given_si;
+    if (!si)
+      si = new scc_info(aut);
+
+    // Renumber all useful states.
+    unsigned in_n = aut->num_states(); // Number of input states.
+    unsigned out_n = 0;		       // Number of output states.
+    std::vector<unsigned> inout; // Associate old states to new ones.
+    inout.reserve(in_n);
+    for (unsigned i = 0; i < in_n; ++i)
+      if (si->is_useful_state(i))
+	inout.push_back(out_n++);
+      else
+	inout.push_back(-1U);
+
+    // scc_info is not useful anymore.
+    if (!given_si)
+      delete si;
+
+    bdd_dict* bd = aut->get_dict();
+    tgba_digraph* filtered = new tgba_digraph(bd);
+    bd->register_all_variables_of(aut, filtered);
+    filtered->copy_acceptance_conditions_of(aut);
+    const tgba_digraph::graph_t& ing = aut->get_graph();
+    tgba_digraph::graph_t& outg = filtered->get_graph();
+    outg.new_states(out_n);
+    for (unsigned isrc = 0; isrc < in_n; ++isrc)
+      {
+	unsigned osrc = inout[isrc];
+	if (osrc >= out_n)
+	  continue;
+	for (auto& t: ing.out(isrc))
+	  {
+	    unsigned odst = inout[t.dst];
+	    if (odst >= out_n)
+	      continue;
+	    outg.new_transition(osrc, odst, t.cond, t.acc);
+	  }
+      }
+    filtered->set_init_state(aut->get_init_state_number());
+    return filtered;
+  }
+
 }
diff --git a/src/tgbaalgos/sccfilter.hh b/src/tgbaalgos/sccfilter.hh
index 60910642d..e24b424d3 100644
--- a/src/tgbaalgos/sccfilter.hh
+++ b/src/tgbaalgos/sccfilter.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et
+// Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche et
 // Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -20,11 +20,16 @@
 #ifndef SPOT_TGBAALGOS_SCCFILTER_HH
 # define SPOT_TGBAALGOS_SCCFILTER_HH
 
-#include "tgba/tgba.hh"
+#include "misc/common.hh"
+#include <bdd.h>
 
 namespace spot
 {
   class scc_map;
+  class tgba;
+  class tgba_digraph;
+  class scc_info;
+
 
   /// \brief Prune unaccepting SCCs and remove superfluous acceptance
   /// conditions.
@@ -75,8 +80,13 @@ namespace spot
   /// Especially, if the input TGBA has the SBA property, (i.e.,
   /// transitions leaving accepting states are all marked as
   /// accepting), then the output TGBA will also have that property.
+  /// @{
   SPOT_API tgba*
   scc_filter_states(const tgba* aut, scc_map* given_sm = 0);
+
+  SPOT_API tgba_digraph*
+  scc_filter_states(const tgba_digraph* aut, scc_info* given_si = 0);
+  /// @}
 }
 
 #endif // SPOT_TGBAALGOS_SCC_HH