Commit fbf5ac0e authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent df1ef302
...@@ -1195,7 +1195,7 @@ checked_main(int argc, char** argv) ...@@ -1195,7 +1195,7 @@ checked_main(int argc, char** argv)
tm.start("dtwasat"); tm.start("dtwasat");
auto satminimized = dtwa_sat_minimize auto satminimized = dtwa_sat_minimize
(ensure_digraph(a), opt_dtwasat, (ensure_digraph(a), opt_dtwasat,
spot::acc_cond::generalized_buchi(opt_dtwasat)); spot::acc_cond::acc_code::generalized_buchi(opt_dtwasat));
tm.stop("dtwasat"); tm.stop("dtwasat");
if (satminimized) if (satminimized)
a = satminimized; a = satminimized;
......
...@@ -497,12 +497,16 @@ namespace spot ...@@ -497,12 +497,16 @@ namespace spot
static acc_code generalized_buchi(unsigned n) static acc_code generalized_buchi(unsigned n)
{ {
acc_cond::mark_t m = (1U << n) - 1; acc_cond::mark_t m = (1U << n) - 1;
if (n == 8 * sizeof(mark_t::value_t))
m = mark_t(-1U);
return inf(m); return inf(m);
} }
static acc_code generalized_co_buchi(unsigned n) static acc_code generalized_co_buchi(unsigned n)
{ {
acc_cond::mark_t m = (1U << n) - 1; acc_cond::mark_t m = (1U << n) - 1;
if (n == 8 * sizeof(mark_t::value_t))
m = mark_t(-1U);
return fin(m); return fin(m);
} }
...@@ -1037,14 +1041,6 @@ namespace spot ...@@ -1037,14 +1041,6 @@ namespace spot
// parity acceptance condition. // parity acceptance condition.
bool is_parity(bool& max, bool& odd, bool equiv = false) const; 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 // Return (true, m) if there exist some acceptance mark m that
// does not satisfy the acceptance condition. Return (false, 0U) // does not satisfy the acceptance condition. Return (false, 0U)
// otherwise. // otherwise.
......
...@@ -414,15 +414,18 @@ namespace spot ...@@ -414,15 +414,18 @@ namespace spot
{ {
if (sat_states_ != -1) if (sat_states_ != -1)
res = dtwa_sat_synthetize 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_); sat_states_, state_based_);
else if (sat_minimize_ == 1 || sat_minimize_ == -1) else if (sat_minimize_ == 1 || sat_minimize_ == -1)
res = dtwa_sat_minimize 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_); state_based_);
else // sat_minimize_ == 2 else // sat_minimize_ == 2
res = dtwa_sat_minimize_dichotomy 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_); state_based_);
} }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment