From 0ede968760cd63b7496c345656447740538a42e9 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 16 Apr 2015 00:10:56 +0200
Subject: [PATCH] sat-minimize: allow different acceptances as input and output

* src/twaalgos/dtgbasat.cc (sat_minimize): Use any arbitrary
acceptance condition passed via the "acc" option.
* src/twa/acc.hh (mark_t::max_set): New method.
* src/tests/satmin2.test: Add two test cases with DRA as input
and DSA as output.
---
 src/tests/satmin2.test   | 48 ++++++++++++++++++++++++++++++++++++++++
 src/twa/acc.hh           | 15 +++++++++++++
 src/twaalgos/dtgbasat.cc | 28 ++++++++++++++++++++---
 3 files changed, 88 insertions(+), 3 deletions(-)

diff --git a/src/tests/satmin2.test b/src/tests/satmin2.test
index b8a0cacaf..ec271896c 100755
--- a/src/tests/satmin2.test
+++ b/src/tests/satmin2.test
@@ -24,6 +24,8 @@ set -e
 # Skip if $SATSOLVE is not installed.
 (${SATSOLVER-glucose} --help >/dev/null 2>&1) || exit 77
 
+autfilt=../../bin/autfilt
+ltlfilt=../../bin/ltlfilt
 
 # This is a counterexample for one of the optimization idea we had for
 # the SAT-based minimization.
@@ -63,3 +65,49 @@ diff output expected
 ../../bin/ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" -H >out
 grep 'properties:.*state-acc' out
 grep 'properties:.*deterministic' out
+
+
+# DRA produced by ltl2dstar for GFp0 -> GFp1
+cat >test.hoa <<EOF
+HOA: v1
+States: 4
+properties: implicit-labels trans-labels no-univ-branch deterministic complete
+acc-name: Rabin 2
+Acceptance: 4 (Fin(0)&Inf(1))|(Fin(2)&Inf(3))
+Start: 0
+AP: 2 "p0" "p1"
+--BODY--
+State: 0 {0}
+1
+0
+3
+2
+State: 1 {1}
+1
+0
+3
+2
+State: 2 {0 3}
+1
+0
+3
+2
+State: 3 {1 3}
+1
+0
+3
+2
+--END--
+EOF
+
+# Let's try to find a smaller transition-based Streett automaton We
+# easily really check the expected automaton, because different SAT
+# solver (even different versions of glucose) can return different
+# automata.
+$autfilt -H --sat-minimize='acc="Fin(0)|Inf(1)"' test.hoa --stats=%s >output
+test `cat output` = 1
+
+# How about a state-based DSA?
+$autfilt -H --sat-minimize='state-based,acc="Fin(0)|Inf(1)"' test.hoa \
+	 --stats=%s > output
+test `cat output` = 3
diff --git a/src/twa/acc.hh b/src/twa/acc.hh
index 1645d8e03..5ed2907f3 100644
--- a/src/twa/acc.hh
+++ b/src/twa/acc.hh
@@ -197,6 +197,21 @@ namespace spot
 #endif
       }
 
+      // Return the number of the highest set used plus one.
+      // So if no set is used, this returns 0,
+      // but if the sets {1,3,8} are used, this returns 9.
+      unsigned max_set() const
+      {
+	auto i = id;
+	int res = 0;
+	while (i)
+	  {
+	    ++res;
+	    i >>= 1;
+	  }
+	return res;
+      }
+
       // Remove n bits that where set
       mark_t& remove_some(unsigned n)
       {
diff --git a/src/twaalgos/dtgbasat.cc b/src/twaalgos/dtgbasat.cc
index 32b37b6ba..57760ec3f 100644
--- a/src/twaalgos/dtgbasat.cc
+++ b/src/twaalgos/dtgbasat.cc
@@ -1033,12 +1033,34 @@ namespace spot
     bool dicho = om.get("dichotomy", 0);
     int states = om.get("states", -1);
     int nacc = om.get("gba", -1);
+    auto accstr = om.get_str("acc");
+
+    if (nacc != -1 && !accstr.empty())
+      throw std::runtime_error("options 'gba' and 'acc' cannot "
+			       "be both passed to sat_minimize()");
 
     acc_cond::acc_code target_acc = a->get_acceptance();
-    if (nacc != -1)
-      target_acc = acc_cond::generalized_buchi(nacc);
+    if (!accstr.empty())
+      {
+	target_acc = parse_acc_code(accstr.c_str());
+	// Just in case we were given something like
+	//  Fin(1) | Inf(3)
+	// Rewrite it as
+	//  Fin(0) | Inf(1)
+	// without holes in the set numbers
+	acc_cond::mark_t used = target_acc.used_sets();
+	acc_cond a(used.max_set());
+	target_acc = target_acc.strip(a.comp(used), true);
+	nacc = used.count();
+      }
+    else if (nacc != -1)
+      {
+	target_acc = acc_cond::generalized_buchi(nacc);
+      }
     else
-      nacc = a->acc().num_sets();
+      {
+	nacc = a->acc().num_sets();
+      }
 
     bool target_is_buchi =
       (nacc == 1 && target_acc.size() == 2 &&