From 5d143cc1f83228870f8b9b98f602c36ee4b0a8b3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment=20Gillard?= <clement.gillard@epita.fr>
Date: Thu, 16 Feb 2017 15:35:01 +0100
Subject: [PATCH] decompose_scc: factor autfilt into decompose_acc_scc

Put what is done by `autfilt` in a new function, `decompose_acc_scc`.

* bin/autfilt.cc: Move code from here...
* spot/twaalgos/strength.cc, spot/twaalgos/strength.hh: To here.
* tests/python/decompose_scc.py: Test python binding.
---
 bin/autfilt.cc                | 15 +----------
 spot/twaalgos/strength.cc     | 19 ++++++++++++++
 spot/twaalgos/strength.hh     | 10 +++++++
 tests/python/decompose_scc.py | 49 +++++++++++++++++++++++++++++++++++
 4 files changed, 79 insertions(+), 14 deletions(-)

diff --git a/bin/autfilt.cc b/bin/autfilt.cc
index a48871867..84998b4da 100644
--- a/bin/autfilt.cc
+++ b/bin/autfilt.cc
@@ -1197,20 +1197,7 @@ namespace
 
       if (opt_decompose_scc != -1)
         {
-          spot::scc_info si(aut);
-          unsigned scc_num = 0;
-
-          for (; scc_num < si.scc_count(); ++scc_num)
-            {
-              if (si.is_accepting_scc(scc_num))
-                {
-                  if (!opt_decompose_scc)
-                    break;
-                  --opt_decompose_scc;
-                }
-            }
-
-          aut = decompose_scc(si, scc_num);
+          aut = decompose_acc_scc(aut, opt_decompose_scc);
           if (!aut)
             return 0;
         }
diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc
index 82ea1140c..7c3428eef 100644
--- a/spot/twaalgos/strength.cc
+++ b/spot/twaalgos/strength.cc
@@ -391,4 +391,23 @@ namespace spot
 
     return res;
   }
+
+  twa_graph_ptr
+  decompose_acc_scc(const const_twa_graph_ptr& aut, int scc_index)
+  {
+    scc_info si(aut);
+    unsigned scc_num = 0;
+
+    for (; scc_num < si.scc_count(); ++scc_num)
+      {
+        if (si.is_accepting_scc(scc_num))
+          {
+            if (!scc_index)
+              break;
+            --scc_index;
+          }
+      }
+
+    return decompose_scc(si, scc_num);
+  }
 }
diff --git a/spot/twaalgos/strength.hh b/spot/twaalgos/strength.hh
index 1f5b8713f..0c4762551 100644
--- a/spot/twaalgos/strength.hh
+++ b/spot/twaalgos/strength.hh
@@ -181,4 +181,14 @@ namespace spot
   /// \param scc_num the index in the map of the SCC to keep
   SPOT_API twa_graph_ptr
   decompose_scc(scc_info& sm, unsigned scc_num);
+
+  /// \brief Extract a sub-automaton of an accepting SCC
+  ///
+  /// This algorithm returns a subautomaton that contains the `scc_index'th
+  /// accepting SCC, plus any upstream SCC (but adjusted not to be accepting).
+  ///
+  /// \param aut the automaton to decompose
+  /// \param scc_index the ID of the accepting SCC to keep
+  SPOT_API twa_graph_ptr
+  decompose_acc_scc(const const_twa_graph_ptr& aut, int scc_index);
 }
diff --git a/tests/python/decompose_scc.py b/tests/python/decompose_scc.py
index a0bae10d4..a92669979 100644
--- a/tests/python/decompose_scc.py
+++ b/tests/python/decompose_scc.py
@@ -49,3 +49,52 @@ except ValueError:
     pass
 else:
     raise AssertionError
+
+assert (spot.decompose_acc_scc(aut, 1).to_str('hoa', '1.1') == """HOA: v1.1
+States: 4
+Start: 0
+AP: 3 "b" "a" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[!1&!2] 0
+[1&!2] 1
+[2] 2
+State: 1
+[!1&!2] 0
+[1&!2] 1
+[!1&2] 2
+[1&2] 3
+State: 2 {0}
+[t] 2
+State: 3
+[!1] 2
+[1] 3
+--END--""")
+
+assert (spot.decompose_acc_scc(aut, 2).to_str('hoa', '1.1') == """HOA: v1.1
+States: 2
+Start: 0
+AP: 3 "b" "a" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc !complete
+properties: deterministic
+--BODY--
+State: 0
+[!1&!2] 0 {0}
+[1&!2] 1
+State: 1
+[!1&!2] 0 {0}
+[1&!2] 1
+--END--""")
+
+try:
+    spot.decompose_acc_scc(aut, 3)
+except ValueError:
+    pass
+else:
+    raise AssertionError
-- 
GitLab