From fbf5ac0ea7933458bf7204866aefe5fef0c62fdd Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 18 Dec 2015 18:14:25 +0100
Subject: [PATCH] acc_cond: get rid of generalized_buchi()

It is already in acc_cond::acc_code::generalized_buchi() along with all
other acceptance condition constructors.

* spot/twa/acc.hh (acc_cond::generalized_buchi): Remove.
* spot/tests/ikwiad.cc, spot/twaalgos/postproc.cc: Adjust.
---
 spot/tests/ikwiad.cc      |  2 +-
 spot/twa/acc.hh           | 12 ++++--------
 spot/twaalgos/postproc.cc |  9 ++++++---
 3 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/spot/tests/ikwiad.cc b/spot/tests/ikwiad.cc
index 2669cbc65..866957614 100644
--- a/spot/tests/ikwiad.cc
+++ b/spot/tests/ikwiad.cc
@@ -1195,7 +1195,7 @@ checked_main(int argc, char** argv)
 	  tm.start("dtwasat");
 	  auto satminimized = dtwa_sat_minimize
 	    (ensure_digraph(a), opt_dtwasat,
-	     spot::acc_cond::generalized_buchi(opt_dtwasat));
+	     spot::acc_cond::acc_code::generalized_buchi(opt_dtwasat));
 	  tm.stop("dtwasat");
 	  if (satminimized)
 	    a = satminimized;
diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh
index d8eca7ba4..22202cc91 100644
--- a/spot/twa/acc.hh
+++ b/spot/twa/acc.hh
@@ -497,12 +497,16 @@ namespace spot
       static acc_code generalized_buchi(unsigned n)
       {
 	acc_cond::mark_t m = (1U << n) - 1;
+	if (n == 8 * sizeof(mark_t::value_t))
+	  m = mark_t(-1U);
 	return inf(m);
       }
 
       static acc_code generalized_co_buchi(unsigned n)
       {
 	acc_cond::mark_t m = (1U << n) - 1;
+	if (n == 8 * sizeof(mark_t::value_t))
+	  m = mark_t(-1U);
 	return fin(m);
       }
 
@@ -1037,14 +1041,6 @@ namespace spot
     // parity acceptance condition.
     bool is_parity(bool& max, bool& odd, bool equiv = false) const;
 
-    static acc_code generalized_buchi(unsigned n)
-    {
-      mark_t m((1U << n) - 1);
-      if (n == 8 * sizeof(mark_t::value_t))
-	m = mark_t(-1U);
-      return acc_code::inf(m);
-    }
-
     // Return (true, m) if there exist some acceptance mark m that
     // does not satisfy the acceptance condition.  Return (false, 0U)
     // otherwise.
diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc
index 0197c602b..c5246195d 100644
--- a/spot/twaalgos/postproc.cc
+++ b/spot/twaalgos/postproc.cc
@@ -414,15 +414,18 @@ namespace spot
 	  {
 	    if (sat_states_ != -1)
 	      res = dtwa_sat_synthetize
-		(res, target_acc, acc_cond::generalized_buchi(target_acc),
+		(res, target_acc,
+		 acc_cond::acc_code::generalized_buchi(target_acc),
 		 sat_states_, state_based_);
 	    else if (sat_minimize_ == 1 || sat_minimize_ == -1)
 	      res = dtwa_sat_minimize
-		(res, target_acc, acc_cond::generalized_buchi(target_acc),
+		(res, target_acc,
+		 acc_cond::acc_code::generalized_buchi(target_acc),
 		 state_based_);
 	    else  // sat_minimize_ == 2
 	      res = dtwa_sat_minimize_dichotomy
-		(res, target_acc, acc_cond::generalized_buchi(target_acc),
+		(res, target_acc,
+		 acc_cond::acc_code::generalized_buchi(target_acc),
 		 state_based_);
 	  }