diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc index eb835fac6..af1c8585a 100644 --- a/spot/twaalgos/parity.cc +++ b/spot/twaalgos/parity.cc @@ -24,7 +24,6 @@ #include #include #include -#include namespace spot { @@ -147,6 +146,93 @@ namespace spot return aut; } + twa_graph_ptr + cleanup_parity(const const_twa_graph_ptr& aut, bool keep_style) + { + auto result = make_twa_graph(aut, twa::prop_set::all()); + return cleanup_parity_here(result, keep_style); + } + + twa_graph_ptr + cleanup_parity_here(twa_graph_ptr aut, bool keep_style) + { + bool current_max; + bool current_odd; + if (!aut->acc().is_parity(current_max, current_odd, true)) + throw new std::invalid_argument("cleanup_parity: input " + "must have a parity acceptance."); + auto num_sets = aut->num_sets(); + if (num_sets == 0) + return aut; + + // Compute all the used sets + auto used_in_aut = acc_cond::mark_t(); + for (auto& t: aut->edges()) + { + if (current_max) + { + auto maxset = t.acc.max_set(); + if (maxset) + t.acc = acc_cond::mark_t{maxset - 1}; + } + else + { + t.acc = t.acc.lowest(); + } + used_in_aut |= t.acc; + } + if (used_in_aut) + { + // Never remove the least significant acceptance set, and mark the + // acceptance set 0 to keep the style if needed. + if (current_max || keep_style) + used_in_aut.set(0); + if (!current_max) + used_in_aut.set(num_sets - 1); + + // Fill the vector shift with the new acceptance sets + std::vector shift(num_sets); + int prev_used = -1; + bool change_style = false; + unsigned new_index = 0; + for (auto i = 0U; i < num_sets; ++i) + if (used_in_aut.has(i)) + { + if (prev_used == -1) + change_style = i % 2 != 0; + else if ((i + prev_used) % 2 != 0) + ++new_index; + shift[i] = new_index; + prev_used = i; + } + + // Update all the transitions with the vector shift + for (auto& t: aut->edges()) + { + auto maxset = t.acc.max_set(); + if (maxset) + t.acc = acc_cond::mark_t{shift[maxset - 1]}; + } + auto new_num_sets = new_index + 1; + if (new_num_sets < num_sets) + { + auto new_acc = acc_cond::acc_code::parity(current_max, + current_odd != change_style, + new_num_sets); + aut->set_acceptance(new_num_sets, new_acc); + } + } + else + { + if ((current_max && current_odd) + || (!current_max && current_odd != (num_sets % 2 == 0))) + aut->set_acceptance(0, acc_cond::acc_code::t()); + else + aut->set_acceptance(0, acc_cond::acc_code::f()); + } + return aut; + } + twa_graph_ptr colorize_parity(const const_twa_graph_ptr& aut, bool keep_style) { diff --git a/spot/twaalgos/parity.hh b/spot/twaalgos/parity.hh index df04af9fe..34b0c3a6d 100644 --- a/spot/twaalgos/parity.hh +++ b/spot/twaalgos/parity.hh @@ -88,6 +88,27 @@ namespace spot change_parity_here(twa_graph_ptr aut, parity_kind kind, parity_style style); /// @} + /// \brief Remove useless acceptance sets of an automaton with parity + /// acceptance + /// + /// If two sets with the same parity are separated by unused sets, then these + /// two sets are merged. The input must be an automaton with a parity + /// acceptance, otherwise an invalid_argument exception is thrown. + /// + /// \param aut the input automaton + /// + /// \param keep_style whether the style of the parity acc is kept. + /// + /// \return the automaton without useless acceptance sets. + /// @{ + SPOT_API twa_graph_ptr + cleanup_parity(const const_twa_graph_ptr& aut, + bool keep_style = false); + + SPOT_API twa_graph_ptr + cleanup_parity_here(twa_graph_ptr aut, bool keep_style = false); + /// @} + /// \brief Colorize an automaton with parity acceptance /// /// An automaton is said colored iff all the transitions belong to exactly one diff --git a/tests/core/parity.cc b/tests/core/parity.cc index 0c7e2904b..5e5194c4a 100644 --- a/tests/core/parity.cc +++ b/tests/core/parity.cc @@ -365,6 +365,21 @@ int main() is_max, is_odd, acc_num_sets) && "change_parity: wrong acceptance."); } + // Check cleanup_parity + for (auto keep_style: { true, false }) + { + auto output = spot::cleanup_parity(aut, keep_style); + assert(is_almost_colored(output) + && "cleanup_parity: too many acc on a transition."); + assert(are_equiv(aut, output) + && "cleanup_parity: not equivalent."); + auto target_kind = to_parity_kind(is_max); + auto target_style = keep_style ? to_parity_style(is_odd) + : spot::parity_style_any; + assert(is_right_parity(output, target_kind, target_style, + is_max, is_odd, acc_num_sets) + && "cleanup_parity: wrong acceptance."); + } } } return 0;