From 5a819e0c93adb92da6ca9c099fbe0e31711521d5 Mon Sep 17 00:00:00 2001
From: Maximilien Colange <colange@lrde.epita.fr>
Date: Fri, 25 May 2018 10:26:03 +0200
Subject: [PATCH] twa_graph: add a method to merge states with same outgoing
 edges

* spot/twa/twagraph.hh, spot/twa/twagraph.cc: here
* NEWS: document it
* tests/core/twagraph.cc, tests/core/tgbagraph.test: test it
---
 NEWS                      |  5 +++++
 spot/twa/twagraph.cc      | 42 +++++++++++++++++++++++++++++++++++++++
 spot/twa/twagraph.hh      |  8 ++++++++
 tests/core/tgbagraph.test | 14 ++++++++++++-
 tests/core/twagraph.cc    | 21 ++++++++++++++++++++
 5 files changed, 89 insertions(+), 1 deletion(-)

diff --git a/NEWS b/NEWS
index 494b62e79..23c15f3d1 100644
--- a/NEWS
+++ b/NEWS
@@ -24,6 +24,11 @@ New in spot 2.5.3.dev  (not yet released)
 
   Library:
 
+  - spot::twa_graph::merge_states() is a new method that merges states
+    with the exact same outgoing edges. As it performs no reordering of
+    the edges, it is better to call it when you know that the edges in
+    the twa_graph are sorted (e.g. after a call to merge_edges()).
+
   - You can now specify to Spot the number of acceptance marks you
     wish to use. This is a compile-time option, accessible through
     option --enable-max-accsets of the configure script. The default
diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc
index d48261a57..25dd762fb 100644
--- a/spot/twa/twagraph.cc
+++ b/spot/twa/twagraph.cc
@@ -231,6 +231,48 @@ namespace spot
     g_.chain_edges_();
   }
 
+  void twa_graph::merge_states()
+  {
+    if (!is_existential())
+      throw std::runtime_error(
+          "twa_graph::merge_states() does not work on alternating automata");
+
+    const unsigned nb_states = num_states();
+    std::vector<unsigned> remap(nb_states, -1U);
+    for (unsigned i = 0; i != nb_states; ++i)
+      {
+        auto out1 = out(i);
+        for (unsigned j = 0; j != i; ++j)
+          {
+            auto out2 = out(j);
+            if (std::equal(out1.begin(), out1.end(), out2.begin(), out2.end(),
+                           [](const edge_storage_t& a,
+                              const edge_storage_t& b)
+                           { return a.dst == b.dst && a.data() == b.data(); }))
+            {
+              remap[i] = j;
+              break;
+            }
+          }
+      }
+
+    for (auto& e: edges())
+      if (remap[e.dst] != -1U)
+        e.dst = remap[e.dst];
+
+    if (remap[get_init_state_number()] != -1U)
+      set_init_state(remap[get_init_state_number()]);
+
+    unsigned st = 0;
+    for (auto& s: remap)
+      if (s == -1U)
+        s = st++;
+      else
+        s = -1U;
+
+    defrag_states(std::move(remap), st);
+  }
+
   void twa_graph::purge_unreachable_states(shift_action* f, void* action_data)
   {
     unsigned num_states = g_.num_states();
diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh
index cbd4a46dd..b2020721f 100644
--- a/spot/twa/twagraph.hh
+++ b/spot/twa/twagraph.hh
@@ -553,6 +553,14 @@ namespace spot
     /// This is already called by merge_edges().
     void merge_univ_dests();
 
+    /// \brief Merge states that can be merged.
+    ///
+    /// This merges states that have the exact same outgoing edges. This method
+    /// compares the successors of states in the order in which they are stored.
+    /// Therefore, it is better to call it when you know that the edges are
+    /// stored, e.g. after a call to merge_edges().
+    void merge_states();
+
     /// \brief Remove all dead states
     ///
     /// Dead states are all the states that cannot be part of
diff --git a/tests/core/tgbagraph.test b/tests/core/tgbagraph.test
index f7a8823ea..5629c95db 100755
--- a/tests/core/tgbagraph.test
+++ b/tests/core/tgbagraph.test
@@ -30,7 +30,7 @@
 
 set -e
 
-run 0 ../tgbagraph | tee stdout
+run 0 ../tgbagraph > stdout
 
 cat >expected <<EOF
 p1
@@ -289,6 +289,18 @@ State: 1
 State: 2
 [t] 0&1
 --END--
+HOA: v1
+States: 1
+Start: 0
+AP: 0
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[t] 0
+--END--
 EOF
 
 diff stdout expected
diff --git a/tests/core/twagraph.cc b/tests/core/twagraph.cc
index b979da6e6..f7a04d60b 100644
--- a/tests/core/twagraph.cc
+++ b/tests/core/twagraph.cc
@@ -158,10 +158,31 @@ static void f4()
   spot::print_hoa(std::cout, tg, "1.1") << '\n';
 }
 
+// Test merge_states()
+static void f5()
+{
+  auto d = spot::make_bdd_dict();
+  auto tg = make_twa_graph(d);
+
+  auto s1 = tg->new_state();
+  auto s2 = tg->new_state();
+  auto s3 = tg->new_state();
+
+  tg->set_init_state(s3);
+  tg->new_edge(s1, s2, bddtrue);
+  tg->new_edge(s2, s2, bddtrue);
+  tg->new_edge(s3, s2, bddtrue);
+
+  tg->merge_states();
+
+  spot::print_hoa(std::cout, tg) << '\n';
+}
+
 int main()
 {
   f1();
   f2();
   f3();
   f4();
+  f5();
 }