From 11704d31ebcd7410658b93f22f09a572bdb312c2 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 10 May 2017 16:53:22 +0200
Subject: [PATCH] scc_info: improve split_on_sets

* spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh (split_on_set):
Allow names to be preserved
* python/spot/impl.i: Instantiate std::vector<spot::twa_graph_ptr>.
---
 python/spot/impl.i       |  1 +
 spot/twaalgos/sccinfo.cc | 10 +++++++---
 spot/twaalgos/sccinfo.hh | 20 ++++++++++++--------
 3 files changed, 20 insertions(+), 11 deletions(-)

diff --git a/python/spot/impl.i b/python/spot/impl.i
index 2df195064..fbf311078 100644
--- a/python/spot/impl.i
+++ b/python/spot/impl.i
@@ -577,6 +577,7 @@ def state_is_accepting(self, src) -> "bool":
 %include <spot/twaalgos/sccinfo.hh>
 %template(scc_info_scc_edges) spot::internal::scc_edges<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data> const, spot::internal::keep_all>;
 %template(scc_info_inner_scc_edges) spot::internal::scc_edges<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data> const, spot::internal::keep_inner_scc>;
+%template(vector_twa_graph) std::vector<spot::twa_graph_ptr>;
 %include <spot/twaalgos/strength.hh>
 %include <spot/twaalgos/sccfilter.hh>
 %include <spot/twaalgos/stats.hh>
diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc
index 1323956eb..7dc662b5b 100644
--- a/spot/twaalgos/sccinfo.cc
+++ b/spot/twaalgos/sccinfo.cc
@@ -448,7 +448,8 @@ namespace spot
   }
 
   std::vector<twa_graph_ptr>
-  scc_info::split_on_sets(unsigned scc, acc_cond::mark_t sets) const
+  scc_info::split_on_sets(unsigned scc, acc_cond::mark_t sets,
+                          bool preserve_names) const
   {
     std::vector<twa_graph_ptr> res;
 
@@ -480,7 +481,11 @@ namespace spot
                              },
                              init);
         if (copy->num_edges())
-          res.push_back(copy);
+          {
+            if (preserve_names)
+              copy->copy_state_names_from(aut_);
+            res.push_back(copy);
+          }
       }
     return res;
   }
@@ -564,5 +569,4 @@ namespace spot
 
     return res;
   }
-
 }
diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh
index 92a4b61dd..e4cbca421 100644
--- a/spot/twaalgos/sccinfo.hh
+++ b/spot/twaalgos/sccinfo.hh
@@ -549,14 +549,19 @@ namespace spot
 
     bdd scc_ap_support(unsigned scc) const;
 
-  protected:
-    /// \brief: Remove in 'scc', edges containing any mark in 'sets'.
+    /// \brief Split an SCC into multiple automata separated by some
+    /// acceptance sets.
     ///
-    /// Such a deletion may split the SCC, in which case, the function builds
-    /// and returns more than one automaton representing the specified SCC.
-    std::vector<twa_graph_ptr>
-    split_on_sets(unsigned scc, acc_cond::mark_t sets) const;
-
+    /// Pretend that the transitions of SCC \a scc that belong to any
+    /// of the sets given in \a sets have been removed, and return a
+    /// set of automata necessary to cover all remaining states.
+    ///
+    /// Set \a preserve_names to True if you want to keep the original
+    /// name of each states for display.  (This is a bit slower.)
+    std::vector<twa_graph_ptr> split_on_sets(unsigned scc,
+                                             acc_cond::mark_t sets,
+                                             bool preserve_names = false) const;
+  protected:
     /// \brief: Recursive function used by states_on_acc_cycle_of().
     void
     states_on_acc_cycle_of_rec(unsigned scc,
@@ -573,7 +578,6 @@ namespace spot
     /// acceptance condition.
     std::vector<unsigned>
     states_on_acc_cycle_of(unsigned scc) const;
-
   };