degen: detect superfluous SCCs and remove them

Suggested by Maximilien Colange.

* spot/twaalgos/degen.cc: If the output has more SCC than the input,
detect useless SCCs and remove them.
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/degen.hh: Add support for a degen-remscc option.
* bin/spot-x.cc, NEWS: Document it.
* tests/core/degenscc.test: New file.
* tests/Makefile.am: Add it.
* tests/core/det.test: Lower some expected size (yay!).

NEWS

@@ -96,6 +96,14 @@ New in spot 2.4.0.dev (not yet released)
     transitions on the fly from an alternating Büchi automaton
     using Miyano and Hayashi's breakpoint algorithm.
 
+  - In some cases, spot::degeneralize() would output Büchi automata
+    with more SCCs than its input.  This was hard to notice, because
+    very often simulation-based simplifications remove those extra
+    SCCs.  This situation is now detected by spot::degeneralized() and
+    fixed before returning the automaton.  A new optionnal argument
+    can be passed to disable this behavior (or use -x degen-remscc=0
+    from the command-line).
+
   Deprecation notices:
 
   (These functions still work but compilers emit warnings.)

bin/spot-x.cc

@@ -91,6 +91,9 @@ has an accepting self-loop, then level L is replaced by the accepting \
 level, as it might favor finding accepting cycles earlier.  If \
 degen-lowinit is non-zero, then level L is always used without looking \
 for the presence of an accepting self-loop.") },
+    { DOC("degen-remscc", "If non-zero (the default), make sure the output \
+of the degenalization has as many SCCs as the input, by removing superfluous \
+ones.") },
     { DOC("det-scc", "Set to 0 to disable scc-based optimizations in \
 the determinization algorithm.") },
     { DOC("det-simul", "Set to 0 to disable simulation-based optimizations in \

spot/twaalgos/degen.cc

@@ -26,6 +26,7 @@
 #include <vector>
 #include <algorithm>
 #include <iterator>
+#include <memory>
 #include <spot/twaalgos/sccinfo.hh>
 #include <spot/twa/bddprint.hh>
 
@@ -240,7 +241,8 @@ namespace spot
     twa_graph_ptr
     degeneralize_aux(const const_twa_graph_ptr& a, bool use_z_lvl,
                      bool use_cust_acc_orders, int use_lvl_cache,
-                     bool skip_levels, bool ignaccsl)
+                     bool skip_levels, bool ignaccsl,
+                     bool remove_extra_scc)
     {
       if (!a->acc().is_generalized_buchi())
         throw std::runtime_error
@@ -249,7 +251,10 @@ namespace spot
         throw std::runtime_error
           ("degeneralize() does not support alternation");
 
-      bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl;
+      bool use_scc = (use_lvl_cache
+                      || use_cust_acc_orders
+                      || use_z_lvl
+                      || remove_extra_scc);
 
       bdd_dict_ptr dict = a->get_dict();
 
@@ -305,12 +310,11 @@ namespace spot
       std::vector<std::pair<unsigned, bool>> lvl_cache(a->num_states());
 
       // Compute SCCs in order to use any optimization.
-      scc_info* m = nullptr;
-      if (use_scc)
-        m = new scc_info(a);
+      std::unique_ptr<scc_info> m = use_scc ?
+        std::make_unique<scc_info>(a) : nullptr;
 
       // Cache for common outgoing/incoming acceptances.
-      inout_acc inout(a, m);
+      inout_acc inout(a, m.get());
 
       queue_t todo;
 
@@ -337,7 +341,7 @@ namespace spot
                 if (!skip_levels)
                   break;
               }
-          // There is not accepting level for TBA, let reuse level 0.
+          // There is no accepting level for TBA, let reuse level 0.
           if (!want_sba && s.second == order.size())
             s.second = 0;
         }
@@ -373,9 +377,8 @@ namespace spot
 
           // Level cache stores one encountered level for each state
           // (the value of use_lvl_cache determinates which level
-          // should be remembered).
-          // When entering an SCC first the lvl_cache is checked.
-          // If such state exists level from chache is used.
+          // should be remembered).  This cache is used when
+          // re-entering the SCC.
           if (use_lvl_cache)
             {
               unsigned lvl = ds.second;
@@ -612,10 +615,49 @@ namespace spot
       std::cout << '\n';
       orders.print();
 #endif
-
-      delete m;
-
       res->merge_edges();
+
+      unsigned res_ns = res->num_states();
+      if (!remove_extra_scc || res_ns <= a->num_states())
+        return res;
+
+      scc_info si_res(res);
+      unsigned res_scc_count = si_res.scc_count();
+      if (res_scc_count <= m->scc_count())
+        return res;
+
+      // If we reach this place, we have more SCCs in the output than
+      // in the input.  This means that we have created some redundant
+      // SCCs.  Often, these are trivial SCCs created in front of
+      // their larger sisters, because we did not pick the correct
+      // level when entering the SCC for the first time, and the level
+      // we picked has not been seen again when exploring the SCC.
+      // But it could also be the case that by entering the SCC in two
+      // different ways, we create two clones of the SCC (I haven't
+      // encountered any such case, but I do not want to rule it out
+      // in the code below).
+      //
+      // Now we will iterate over the SCCs in topological order to
+      // remember the "bottomost" SCCs that contain each original
+      // state.  If an original state is duplicated in a higher SCC,
+      // it can be shunted away.  Amen.
+      std::vector<unsigned> bottomost_occurence(a->num_states());
+      {
+        unsigned n = res_scc_count;
+        do
+          for (unsigned s: si_res.states_of(--n))
+            bottomost_occurence[(*orig_states)[s]] = s;
+        while (n);
+      }
+      std::vector<unsigned> retarget(res_ns);
+      for (unsigned n = 0; n < res_ns; ++n)
+        {
+          unsigned other = bottomost_occurence[(*orig_states)[n]];
+          retarget[n] = (si_res.scc_of(n) != si_res.scc_of(other)) ? other : n;
+        }
+      for (auto& e: res->edges())
+        e.dst = retarget[e.dst];
+      res->purge_unreachable_states();
       return res;
     }
   }
@@ -623,7 +665,8 @@ namespace spot
   twa_graph_ptr
   degeneralize(const const_twa_graph_ptr& a,
                bool use_z_lvl, bool use_cust_acc_orders,
-               int use_lvl_cache, bool skip_levels, bool ignaccsl)
+               int use_lvl_cache, bool skip_levels, bool ignaccsl,
+               bool remove_extra_scc)
   {
     // If this already a degeneralized digraph, there is nothing we
     // can improve.
@@ -631,13 +674,15 @@ namespace spot
       return std::const_pointer_cast<twa_graph>(a);
 
     return degeneralize_aux<true>(a, use_z_lvl, use_cust_acc_orders,
-                                  use_lvl_cache, skip_levels, ignaccsl);
+                                  use_lvl_cache, skip_levels, ignaccsl,
+                                  remove_extra_scc);
   }
 
   twa_graph_ptr
   degeneralize_tba(const const_twa_graph_ptr& a,
                    bool use_z_lvl, bool use_cust_acc_orders,
-                   int use_lvl_cache, bool skip_levels, bool ignaccsl)
+                   int use_lvl_cache, bool skip_levels, bool ignaccsl,
+                   bool remove_extra_scc)
   {
     // If this already a degeneralized digraph, there is nothing we
     // can improve.
@@ -645,6 +690,7 @@ namespace spot
       return std::const_pointer_cast<twa_graph>(a);
 
     return degeneralize_aux<false>(a, use_z_lvl, use_cust_acc_orders,
-                                   use_lvl_cache, skip_levels, ignaccsl);
+                                   use_lvl_cache, skip_levels, ignaccsl,
+                                   remove_extra_scc);
   }
 }

spot/twaalgos/degen.hh

@@ -41,7 +41,9 @@ namespace spot
   /// smallest number, 3 to keep the largest level, and 1 to keep the
   /// first level found). If \a ignaccsl is set, we do not directly
   /// jump to the accepting level if the entering state has an
-  /// accepting self-loop.
+  /// accepting self-loop.  If \a remove_extra_scc is set (the default)
+  /// we ensure that the output automaton has as many SCCs as the input
+  /// by removing superfluous SCCs.
   ///
   /// Any of these three options will cause the SCCs of the automaton
   /// \a a to be computed prior to its actual degeneralization.
@@ -65,13 +67,15 @@ namespace spot
                bool use_cust_acc_orders = false,
                int use_lvl_cache = 1,
                bool skip_levels = true,
-               bool ignaccsl = false);
+               bool ignaccsl = false,
+               bool remove_extra_scc = true);
 
   SPOT_API twa_graph_ptr
   degeneralize_tba(const const_twa_graph_ptr& a, bool use_z_lvl = true,
                    bool use_cust_acc_orders = false,
                    int use_lvl_cache = 1,
                    bool skip_levels = true,
-                   bool ignaccsl = false);
+                   bool ignaccsl = false,
+                   bool remove_extra_scc = true);
   /// \@}
 }

spot/twaalgos/postproc.cc

@@ -62,6 +62,7 @@ namespace spot
         degen_cache_ = opt->get("degen-lcache", 1);
         degen_lskip_ = opt->get("degen-lskip", 1);
         degen_lowinit_ = opt->get("degen-lowinit", 0);
+        degen_remscc_ = opt->get("degen-remscc", 1);
         det_scc_ = opt->get("det-scc", 1);
         det_simul_ = opt->get("det-simul", 1);
         det_stutter_ = opt->get("det-stutter", 1);
@@ -142,7 +143,7 @@ namespace spot
     auto d = degeneralize(a,
                           degen_reset_, degen_order_,
                           degen_cache_, degen_lskip_,
-                          degen_lowinit_);
+                          degen_lowinit_, degen_remscc_);
     return do_sba_simul(d, ba_simul_);
   }
 

spot/twaalgos/postproc.hh

@@ -207,6 +207,7 @@ namespace spot
     int degen_cache_ = 1;
     bool degen_lskip_ = true;
     bool degen_lowinit_ = false;
+    bool degen_remscc_ = true;
     bool det_scc_ = true;
     bool det_simul_ = true;
     bool det_stutter_ = true;

tests/Makefile.am

@@ -247,6 +247,7 @@ TESTS_twa = \
   core/degendet.test \
   core/degenid.test \
   core/degenlskip.test \
+  core/degenscc.test \
   core/randomize.test \
   core/lbttparse.test \
   core/scc.test \

tests/core/degenscc.test

+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2017 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+. ./defs
+
+set -e
+
+# This make sure that the degeneralize fonction does not create
+# new SCCs.
+#
+# The following cases were found with
+#
+# % randltl -n -1 3 | ltl2tgba | autfilt --acc-sets=3.. |
+#   autfilt -B --stats='%C,%c,%M' | awk -F, '{ if ($1 < $2) { print $0; } }'
+#
+# before patching degeneralize, but today replacing -B by -Bx'!degen-remscc'
+# should do the same.
+cat >input <<EOF
+p2 & GF(G(p0 & !p1) | (F!p0 & Fp1))
+GF((Fp2 & X((p0 & Gp1) | (!p0 & F!p1))) | (G!p2 & X((p0 & F!p1) | (!p0 & Gp1))))
+GF(p0 | GF((p2 M p1) | (Fp1 & F!p0) | G(p0 & !p1)))
+((Gp2&FG((Gp1&Xp0)|(F!p1&X!p0)))|(F!p2 & GF((Gp1 & X!p0)|(Xp0 & F!p1)))) W !p0
+G(((Fp1 & (p1 W Fp0)) | (G!p1 & (!p1 M G!p0))) M FG!p2)
+Xp0 R F((p0 & FG(Gp2 U p1)) | (!p0 & GF(F!p2 R !p1)))
+GF(p0 & (((p1 & Fp2) | (!p1 & G!p2)) M Gp1))
+G(!p1 | (!p2 & F!p1) | (GFp2 U p0))
+X(p1 | GF((Fp2 & F!p1) | G(p1 & !p2)))
+EOF
+
+# We want to make sure the degeneralized automaton as less SCCs
+# (it can be less if the simulation on the BA is lukier than on the TGBA)
+ltl2tgba < input | autfilt -B --stats=": '%M'; test %C -ge %c" > test.sh
+sh -x -e test.sh
+
+# Make sur that this degen-remscc optimizition is actually doing something.
+# The following test could fail in the future if we improve the translation
+# of some of these formulas.  In that case, regenerate the list of test
+# formula using the command displayed above.
+ltl2tgba < input |
+  autfilt -Bx'!degen-remscc' --stats=": '%M'; test %C -lt %c" > test.sh
+sh -x -e test.sh
+
+# We also want to make sure those degeneralized automata are correct
+ltlcross -F input ltl2tgba 'ltl2tgba -B' 'ltl2tgba %f | autfilt -B > %O'

tests/core/det.test

@@ -41,7 +41,7 @@ cat >formulas <<'EOF'
 1,6,GF!a U Xa
 1,5,(a | G(a M !b)) W Fc
 1,6,Fa W Xb
-1,10,X(a R ((!b & F!c) M X!a))
+1,9,X(a R ((!b & F!c) M X!a))
 1,2,XG!a R Fb
 1,4,GFc | (a & Fb)
 1,6,X(a R (Fb R F!b))