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_); }