From e945beb607a0f675b454df700c6c74331493acc0 Mon Sep 17 00:00:00 2001
From: Maximilien Colange <colange@lrde.epita.fr>
Date: Wed, 21 Feb 2018 16:21:43 +0100
Subject: [PATCH] Improve cleanup_parity

* spot/twaalgos/parity.cc: cleanup_parity and cleanup_parity_here are
  now better at finding useless parity colors
* tests/python/parity.py: test it
* NEWS: document the change
---
 NEWS                    |  6 ++++-
 spot/twaalgos/parity.cc | 58 +++++++++++++++++++++++++++++++++++------
 tests/python/parity.py  | 51 ++++++++++++++++++++++++++++++++++++
 3 files changed, 106 insertions(+), 9 deletions(-)

diff --git a/NEWS b/NEWS
index 698898030..c6dd244df 100644
--- a/NEWS
+++ b/NEWS
@@ -1,6 +1,10 @@
 New in spot 2.5.1.dev (not yet released)
 
-  Nothing yet.
+  Library:
+
+  - cleanup_parity() and cleanup_parity_here() are smarter and now
+    remove from the acceptance condition the parity colors that are
+    not used in the automaton.
 
 New in spot 2.5.1 (2018-02-20)
 
diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc
index 81b67024b..d30e30940 100644
--- a/spot/twaalgos/parity.cc
+++ b/spot/twaalgos/parity.cc
@@ -177,6 +177,7 @@ namespace spot
     auto used_in_aut = acc_cond::mark_t();
     for (auto& t: aut->edges())
       {
+        // leave only one color on each transition
         if (current_max)
           {
             auto maxset = t.acc.max_set();
@@ -187,16 +188,45 @@ namespace spot
           {
             t.acc = t.acc.lowest();
           }
+        // recall colors used in the automaton
         used_in_aut |= t.acc;
       }
+
+    // remove from the acceptance condition the unused one (starting from the
+    // least significant)
+    auto useful = used_in_aut;
+    int useful_min = 0;
+    int useful_max = num_sets-1;
+    if (!current_max)
+      {
+        int n = num_sets-1;
+        while (n >= 0 && !useful.has(n))
+          {
+            if (n > 0)
+              useful.clear(n-1);
+            n -= 2;
+          }
+        useful_max = n;
+      }
+    else
+      {
+        unsigned n = 0;
+        while (n < num_sets && !useful.has(n))
+          {
+            useful.clear(n+1);
+            n += 2;
+          }
+        useful_min = n;
+      }
     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);
+      if (keep_style && useful_min <= useful_max)
+        {
+          useful.set(useful_min);
+          useful.set(useful_max);
+        }
 
       // Fill the vector shift with the new acceptance sets
       std::vector<unsigned> shift(num_sets);
@@ -204,7 +234,7 @@ namespace spot
       bool change_style = false;
       unsigned new_index = 0;
       for (auto i = 0U; i < num_sets; ++i)
-        if (used_in_aut.has(i))
+        if (useful.has(i))
           {
             if (prev_used == -1)
               change_style = i % 2 != 0;
@@ -217,16 +247,28 @@ namespace spot
       // Update all the transitions with the vector shift
       for (auto& t: aut->edges())
         {
+          t.acc &= useful;
           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 (!useful)
+        {
+          new_num_sets = 0;
+          if (current_max)
+            change_style = false;
+          else
+            change_style = num_sets % 2 == 1;
+        }
+
       if (new_num_sets < num_sets)
         {
-          auto new_acc = acc_cond::acc_code::parity(current_max,
-                                                    current_odd != change_style,
-                                                    new_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);
         }
     }
diff --git a/tests/python/parity.py b/tests/python/parity.py
index b1ede2f44..ee73e7dcb 100644
--- a/tests/python/parity.py
+++ b/tests/python/parity.py
@@ -37,3 +37,54 @@ except RuntimeError as e:
     assert 'input should have parity acceptance' in str(e)
 else:
     exit(2)
+
+a = spot.automaton("""
+HOA: v1
+States: 1
+Start: 0
+AP: 1 "a"
+Acceptance: 2 Fin(0) & Inf(1)
+--BODY--
+State: 0
+[t] 0 {0}
+--END--
+""")
+spot.cleanup_parity_here(a)
+assert a.to_str() == """HOA: v1
+States: 1
+Start: 0
+AP: 1 "a"
+acc-name: none
+Acceptance: 0 f
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[t] 0
+--END--"""
+
+a = spot.automaton("""
+HOA: v1
+States: 1
+Start: 0
+AP: 1 "a"
+Acceptance: 2 Fin(0) | Inf(1)
+--BODY--
+State: 0
+[t] 0 {1}
+--END--
+""")
+spot.cleanup_parity_here(a)
+assert a.to_str() == """HOA: v1
+States: 1
+Start: 0
+AP: 1 "a"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[t] 0
+--END--"""
+