diff --git a/NEWS b/NEWS index 88c689bfc..3a2b8316b 100644 --- a/NEWS +++ b/NEWS @@ -164,11 +164,20 @@ New in spot 2.10.6.dev (not yet released) further simplification. This was introduced to help with automata produced from formulas output by "genltl --eil-gsi" (see above). - - spot::postproc has new configuration variable branch-post that + - spot::postprocessor has new configuration variable branch-post that can be used to control the use of branching-postponement (diabled by default) or delayed-branching (see above, enabled by default). See the spot-x(7) man page for details. + - spot::postprocessor is now using acd_transform() by default when + building parity automata. Setting option "acd=0" will revert + to using "to_parity()" instead. + + - When asked to build parity automata, spot::translator is now more + aggressively using LTL decomposition, as done in the Generic + acceptance case before paritizing the result. This results in + much smaller automata in many cases. + - spot::parallel_policy is an object that can be passed to some algorithm to specify how many threads can be used if Spot has been compiled with --enable-pthread. Currently, only diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 908cbb98a..d1a8f96f6 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -80,6 +80,9 @@ only if it is smaller than the original skeleton. This option is only \ used when comp-susp=1 and default to 1 or 2 depending on whether --small \ or --deterministic is specified.") }, { nullptr, 0, nullptr, 0, "Postprocessing options:", 0 }, + { DOC("acd", "Set to 1 (the default) to use paritize automata using \ +the alternatinc cycle decomposition. Set to 0 to use paritization based \ +on latest appearance record variants.") }, { DOC("scc-filter", "Set to 1 (the default) to enable \ SCC-pruning and acceptance simplification at the beginning of \ post-processing. Transitions that are outside of accepting SCC are \ diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 55feeb295..19e3d2b6c 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2021 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -40,6 +40,7 @@ #include #include #include +#include namespace spot { @@ -92,6 +93,7 @@ namespace spot merge_states_min_ = opt->get("merge-states-min", 128); wdba_det_max_ = opt->get("wdba-det-max", 4096); simul_trans_pruning_ = opt->get("simul-trans-pruning", 512); + acd_ = opt->get("acd", 1); if (sat_acc_ && sat_minimize_ == 0) sat_minimize_ = 1; // Dicho. @@ -250,7 +252,8 @@ namespace spot tmp = ensure_ba(tmp); if (want_parity) { - reduce_parity_here(tmp, COLORED_); + if (!acd_was_used_) + reduce_parity_here(tmp, COLORED_); parity_kind kind = parity_kind_any; parity_style style = parity_style_any; if ((type_ & ParityMin) == ParityMin) @@ -295,6 +298,8 @@ namespace spot bool via_gba = (type_ == Buchi) || (type_ == GeneralizedBuchi) || (type_ == Monitor); bool want_parity = type_ & Parity; + acd_was_used_ = false; + if (COLORED_ && !want_parity) throw std::runtime_error("postprocessor: the Colored setting only works " "for parity acceptance"); @@ -340,18 +345,26 @@ namespace spot !(type_ == Generic && PREF_ == Any && level_ == Low)) a = remove_alternation(a); + // If we do want a parity automaton, we can use to_parity(). + // However (1) degeneralization is faster if the input is + // GBA, and (2) if we want a deterministic parity automaton and the + // input is not deterministic, that is useless here. We need + // to determinize it first, and our deterministization + // function only deal with TGBA as input. if ((via_gba || (want_parity && !a->acc().is_parity())) && !a->acc().is_generalized_buchi()) { - // If we do want a parity automaton, we can use to_parity(). - // However (1) degeneralization is better if the input is - // GBA, and (2) if we want a deterministic parity automaton and the - // input is not deterministic, that is useless here. We need - // to determinize it first, and our deterministization - // function only deal with TGBA as input. if (want_parity && (PREF_ != Deterministic || is_deterministic(a))) { - a = to_parity(a); + if (acd_) + { + a = acd_transform(a, COLORED_); + acd_was_used_ = true; + } + else + { + a = to_parity(a); + } } else { diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index 96128c531..f470dcf5b 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -270,6 +270,8 @@ namespace spot int simul_max_ = 4096; int merge_states_min_ = 128; int wdba_det_max_ = 4096; + bool acd_ = false; + bool acd_was_used_; }; /// @} } diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index cd1e2aa63..0f5e86cde 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -137,6 +137,9 @@ namespace spot twa_graph_ptr aut; twa_graph_ptr aut2 = nullptr; + bool split_hard = + type_ == Generic || (type_ & Parity) || type_ == GeneralizedBuchi; + if (ltl_split_ && !r.is_syntactic_obligation()) { formula r2 = r; @@ -146,11 +149,11 @@ namespace spot r2 = r2[0]; ++leading_x; } - if (type_ == Generic || type_ == GeneralizedBuchi) + if (split_hard) { - // F(q|u|f) = q|F(u)|F(f) only for generic acceptance + // F(q|u|f) = q|F(u)|F(f) disabled for GeneralizedBuchi // G(q&e&f) = q&G(e)&G(f) - bool want_u = r2.is({op::F, op::Or}) && (type_ == Generic); + bool want_u = r2.is({op::F, op::Or}) && (type_ != GeneralizedBuchi); if (want_u || r2.is({op::G, op::And})) { std::vector susp; @@ -213,20 +216,19 @@ namespace spot oblg.erase(i, oblg.end()); } + // The only cases where we accept susp and rest to be both + // non-empty is when doing Generic/Parity/TGBA if (!susp.empty()) { - // The only cases where we accept susp and rest to be both - // non-empty is when doing Generic acceptance or TGBA. - if (!rest.empty() - && !(type_ == Generic || type_ == GeneralizedBuchi)) + if (!rest.empty() && !split_hard) { rest.insert(rest.end(), susp.begin(), susp.end()); susp.clear(); } // For Parity, we want to translate all suspendable // formulas at once. - if (rest.empty() && type_ & Parity) - susp = { formula::multop(r2.kind(), susp) }; + //if (rest.empty() && type_ & Parity) + // susp = { formula::multop(r2.kind(), susp) }; } // For TGBA and BA, we only split if there is something to // suspend. diff --git a/tests/core/genltl.test b/tests/core/genltl.test index 71b1ddf77..ce5584a21 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -190,29 +190,29 @@ cat >exp<