diff --git a/NEWS b/NEWS index 55dfa117f..69c4d7479 100644 --- a/NEWS +++ b/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.) diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 698ca22ed..ad3b0ac36 100644 --- a/bin/spot-x.cc +++ b/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 \ diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index c2c6d6ed8..8ba5caa27 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -26,6 +26,7 @@ #include #include #include +#include #include #include @@ -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> 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 m = use_scc ? + std::make_unique(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 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 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(a); return degeneralize_aux(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(a); return degeneralize_aux(a, use_z_lvl, use_cust_acc_orders, - use_lvl_cache, skip_levels, ignaccsl); + use_lvl_cache, skip_levels, ignaccsl, + remove_extra_scc); } } diff --git a/spot/twaalgos/degen.hh b/spot/twaalgos/degen.hh index ac0ce0510..665ff838f 100644 --- a/spot/twaalgos/degen.hh +++ b/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); /// \@} } diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index ca28d2ed8..375f3224e 100644 --- a/spot/twaalgos/postproc.cc +++ b/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_); } diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index 3266fe2a3..f2b0fa635 100644 --- a/spot/twaalgos/postproc.hh +++ b/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; diff --git a/tests/Makefile.am b/tests/Makefile.am index a33a66917..522e76675 100644 --- a/tests/Makefile.am +++ b/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 \ diff --git a/tests/core/degenscc.test b/tests/core/degenscc.test new file mode 100644 index 000000000..47abfc717 --- /dev/null +++ b/tests/core/degenscc.test @@ -0,0 +1,61 @@ +#!/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 . + +. ./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 < 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' diff --git a/tests/core/det.test b/tests/core/det.test index af634876e..c04558a0b 100755 --- a/tests/core/det.test +++ b/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))