From d795955aaa72d5bb8bf8a951e29b493155c193d8 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 7 Apr 2017 23:25:37 +0200
Subject: [PATCH] cleanacc: add an option to not strip sets

also consider sets that appear everywhere

* spot/twaalgos/cleanacc.cc, spot/twaalgos/cleanacc.hh: Here.
---
 NEWS                      |  5 +++++
 spot/twaalgos/cleanacc.cc | 34 ++++++++++++++++++++++++----------
 spot/twaalgos/cleanacc.hh | 11 +++++++----
 3 files changed, 36 insertions(+), 14 deletions(-)

diff --git a/NEWS b/NEWS
index b6ece1a41..4419d4ecd 100644
--- a/NEWS
+++ b/NEWS
@@ -99,6 +99,11 @@ New in spot 2.3.4.dev (not yet released)
   - It is now possible to change an automaton acceptance condition
     directly by calling twa::set_acceptance().
 
+  - spot::cleanup_acceptance_here now takes an additional boolean
+    parameter specifying whether to strip useless marks from the
+    automaton.  This parameter is defaulted to true, in order to
+    keep this modification backward-compatible.
+
   Python:
 
   - The 'spot.gen' package exports the functions from libspotgen.
diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc
index 1b1277d89..7f2c1d577 100644
--- a/spot/twaalgos/cleanacc.cc
+++ b/spot/twaalgos/cleanacc.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015 Laboratoire de Recherche et Développement
+// Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -21,36 +21,50 @@
 
 namespace spot
 {
-  twa_graph_ptr cleanup_acceptance_here(twa_graph_ptr aut)
+  twa_graph_ptr cleanup_acceptance_here(twa_graph_ptr aut, bool strip)
   {
     auto& acc = aut->acc();
     if (acc.num_sets() == 0)
       return aut;
 
-    auto& c = aut->get_acceptance();
+    auto c = aut->get_acceptance();
     acc_cond::mark_t used_in_cond = c.used_sets();
 
     acc_cond::mark_t used_in_aut = 0U;
+    acc_cond::mark_t used_on_all_edges = used_in_cond;
     for (auto& t: aut->edges())
-      used_in_aut |= t.acc;
+      {
+        used_in_aut |= t.acc;
+        used_on_all_edges &= t.acc;
+      }
 
     auto useful = used_in_aut & used_in_cond;
+    auto useless = strip ? acc.comp(useful) : (used_in_cond - used_in_aut);
 
-    auto useless = acc.comp(useful);
+    useless |= used_on_all_edges;
 
     if (!useless)
       return aut;
 
     // Remove useless marks from the automaton
-    for (auto& t: aut->edges())
-      t.acc = t.acc.strip(useless);
+    if (strip)
+      for (auto& t: aut->edges())
+        t.acc = t.acc.strip(useless);
+
+    // if x appears on all edges, then
+    //   Fin(x) = false and Inf(x) = true
+    if (used_on_all_edges)
+      c = c.remove(used_on_all_edges, false);
 
     // Remove useless marks from the acceptance condition
-    aut->set_acceptance(useful.count(), c.strip(useless, true));
+    if (strip)
+      aut->set_acceptance(useful.count(), c.strip(useless, true));
+    else
+      aut->set_acceptance(aut->num_sets(), c.remove(useless, true));
 
     // This may in turn cause even more set to be unused, because of
-    // some simplifications, so do it again.
-    return cleanup_acceptance_here(aut);
+    // some simplifications in the acceptance condition, so do it again.
+    return cleanup_acceptance_here(aut, strip);
   }
 
   twa_graph_ptr cleanup_acceptance(const_twa_graph_ptr aut)
diff --git a/spot/twaalgos/cleanacc.hh b/spot/twaalgos/cleanacc.hh
index af38c34fb..8af0e8248 100644
--- a/spot/twaalgos/cleanacc.hh
+++ b/spot/twaalgos/cleanacc.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015 Laboratoire de Recherche et Développement
+// Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -24,11 +24,14 @@
 namespace spot
 {
   /// \brief Remove useless acceptance sets
-  /// @{
+  ///
+  /// If \a strip is true (the default), the remaining acceptance set
+  /// numbers will be shifted down to reduce maximal number of
+  /// acceptance sets used.
   SPOT_API twa_graph_ptr
-  cleanup_acceptance_here(twa_graph_ptr aut);
+  cleanup_acceptance_here(twa_graph_ptr aut, bool strip = true);
 
+  /// \brief Remove useless acceptance sets
   SPOT_API twa_graph_ptr
   cleanup_acceptance(const_twa_graph_ptr aut);
-  /// @}
 }