cleanacc: add an option to not strip sets

also consider sets that appear everywhere

* spot/twaalgos/cleanacc.cc, spot/twaalgos/cleanacc.hh: Here.

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.

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_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
+    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
+    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.
+    // some simplifications in the acceptance condition, so do it again.
-    return cleanup_acceptance_here(aut);
+    return cleanup_acceptance_here(aut, strip);
   }
 
   twa_graph_ptr cleanup_acceptance(const_twa_graph_ptr aut)

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);
-  /// @}
 }