parity: add spot::cleanup_parity_acceptance()

Merge the acceptance sets of a parity acceptance with the same priority
level to simplify this acceptance.

* spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here
* tests/core/parity.cc: Add tests for spot::cleanup_parity_acceptance()

spot/twaalgos/parity.cc

@@ -24,7 +24,6 @@
 #include <utility>
 #include <functional>
 #include <queue>
-#include <spot/twaalgos/hoa.hh>
 
 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<unsigned> 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)
   {

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

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;