From 8e9c4317067238a7c1b1bb408bda9e7317bdc8d0 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 17 Dec 2014 09:04:28 +0100
Subject: [PATCH] merge transitions: also merge transitions with same
 conditions

* src/tgba/tgbagraph.cc (merge_transition): Do it.
* src/tgbatest/readsave.test: Test it.
* src/bin/autfilt.cc: Fix statistics about the original
automaton when using --stats or --name.
---
 src/bin/autfilt.cc         |   6 +-
 src/tgba/tgbagraph.cc      |  43 +++++++++++
 src/tgbatest/readsave.test | 144 +++++++++++++++++++++++++++++++++++++
 3 files changed, 192 insertions(+), 1 deletion(-)

diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc
index 9e99356ad..4cc8aba3a 100644
--- a/src/bin/autfilt.cc
+++ b/src/bin/autfilt.cc
@@ -502,7 +502,11 @@ namespace
       spot::stopwatch sw;
       sw.start();
 
-      auto aut = haut->aut;
+      // If --stats or --name is used, duplicate the automaton so we
+      // never modify the original automaton (e.g. with
+      // merge_transitions()) and the statistics about it make sense.
+      auto aut = ((format == Stats) || opt_name) ?
+	spot::make_tgba_digraph(haut->aut) : haut->aut;
 
       // Preprocessing.
 
diff --git a/src/tgba/tgbagraph.cc b/src/tgba/tgbagraph.cc
index 9b7abd606..a27016789 100644
--- a/src/tgba/tgbagraph.cc
+++ b/src/tgba/tgbagraph.cc
@@ -80,6 +80,49 @@ namespace spot
     if (++out != tend)
       trans.resize(out);
 
+    tend = out;
+    out = in = 2;
+
+    if (in < tend)
+      {
+	typedef graph_t::trans_storage_t tr_t;
+	g_.sort_transitions_([](const tr_t& lhs, const tr_t& rhs)
+			     {
+			       if (lhs.src < rhs.src)
+				 return true;
+			       if (lhs.src > rhs.src)
+				 return false;
+			       if (lhs.dst < rhs.dst)
+				 return true;
+			       if (lhs.dst > rhs.dst)
+				 return false;
+			       return lhs.cond.id() < rhs.cond.id();
+			       // Do not sort on acceptance, we'll merge
+			       // them.
+			     });
+
+	for (; in < tend; ++in)
+	  {
+	    // Merge transitions with the same source, destination,
+	    // and conditions.  (We test the source last, for the
+	    // same reason as above.)
+	    if (trans[out].dst == trans[in].dst
+		&& trans[out].cond.id() == trans[in].cond.id()
+		&& trans[out].src == trans[in].src)
+	      {
+		trans[out].acc |= trans[in].acc;
+	      }
+	    else
+	      {
+		++out;
+		if (in != out)
+		  trans[out] = trans[in];
+	      }
+	  }
+	if (++out != tend)
+	  trans.resize(out);
+      }
+
     g_.chain_transitions_();
   }
 
diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test
index cb1331c7e..a25ed4b5c 100755
--- a/src/tgbatest/readsave.test
+++ b/src/tgbatest/readsave.test
@@ -126,3 +126,147 @@ cat >expected <<EOF
 <Fb U G!a, 3 states>, 7, 1
 EOF
 diff output expected
+
+
+cat >input <<EOF
+HOA: v1
+States: 10
+Start: 0
+AP: 1 "a"
+acc-name: generalized-Buchi 3
+Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[t] 0 {0}
+[!0] 1 {0}
+[!0] 2 {0}
+[0] 3 {0}
+[0] 3 {0 2}
+[!0] 2 {0 2}
+[!0] 4 {1}
+[!0] 5 {1}
+[!0] 6 {1}
+[!0] 6 {1 2}
+[!0] 7 {1}
+[!0] 8 {1}
+[!0] 9 {1}
+[!0] 9 {1 2}
+[!0] 4 {0 1}
+[!0] 5 {0 1}
+[!0] 6 {0 1}
+[!0] 6 {0 1 2}
+[!0] 7 {0 1}
+[!0] 8 {0 1}
+[!0] 9 {0 1}
+[!0] 9 {0 1 2}
+State: 1
+[0] 3 {0 2}
+State: 2
+[!0] 2 {0 2}
+[!0] 6 {1 2}
+[!0] 9 {1 2}
+[!0] 6 {0 1 2}
+[!0] 9 {0 1 2}
+State: 3
+[!0] 1 {0 2}
+[!0] 2 {0}
+[0] 3 {0 2}
+[!0] 2 {0 2}
+[!0] 5 {1 2}
+[!0] 6 {1}
+[!0] 6 {1 2}
+[!0] 8 {1 2}
+[!0] 9 {1}
+[!0] 9 {1 2}
+[!0] 5 {0 1 2}
+[!0] 6 {0 1}
+[!0] 6 {0 1 2}
+[!0] 8 {0 1 2}
+[!0] 9 {0 1}
+[!0] 9 {0 1 2}
+State: 4
+[!0] 4 {1}
+[!0] 5 {1}
+[!0] 6 {1}
+[!0] 6 {1 2}
+[!0] 7
+[!0] 8
+[!0] 9
+[!0] 9 {2}
+[!0] 7 {1}
+[!0] 8 {1}
+[!0] 9 {1}
+[!0] 9 {1 2}
+State: 5
+State: 6
+[!0] 6 {1 2}
+[!0] 9 {2}
+[!0] 9 {1 2}
+State: 7
+[0] 0 {0}
+[0] 3 {0}
+[0] 3 {0 2}
+State: 8
+[0] 3 {0 2}
+State: 9
+--END--
+EOF
+
+cat >expected <<EOF
+HOA: v1
+name: "63->32 edges, 64->33 transitions"
+States: 10
+Start: 0
+AP: 1 "a"
+acc-name: generalized-Buchi 3
+Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
+properties: trans-labels explicit-labels
+--BODY--
+State: 0
+[t] 0 {0}
+[!0] 1 {0}
+[!0] 2 {0 2}
+[0] 3 {0 2}
+[!0] 4 {0 1}
+[!0] 5 {0 1}
+[!0] 6 {0 1 2}
+[!0] 7 {0 1}
+[!0] 8 {0 1}
+[!0] 9 {0 1 2}
+State: 1 {0 2}
+[0] 3
+State: 2
+[!0] 2 {0 2}
+[!0] 6 {0 1 2}
+[!0] 9 {0 1 2}
+State: 3
+[!0] 1 {0 2}
+[!0] 2 {0 2}
+[0] 3 {0 2}
+[!0] 5 {0 1 2}
+[!0] 6 {0 1 2}
+[!0] 8 {0 1 2}
+[!0] 9 {0 1 2}
+State: 4
+[!0] 4 {1}
+[!0] 5 {1}
+[!0] 6 {1 2}
+[!0] 7 {1}
+[!0] 8 {1}
+[!0] 9 {1 2}
+State: 5
+State: 6 {1 2}
+[!0] 6
+[!0] 9
+State: 7
+[0] 0 {0}
+[0] 3 {0 2}
+State: 8 {0 2}
+[0] 3
+State: 9
+--END--
+EOF
+
+$autfilt --merge -Hm input --name="%E->%e edges, %T->%t transitions" > output
+diff output expected