From f5965966e96b1a9f198129c95afecca9949b580d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 17 Sep 2020 20:49:23 +0200 Subject: [PATCH] translator: add tls-max-states option This restricts the time spent in translating sub-formulas for implication tests by limiting the associated automata to 64 states by default. Doing so this does worsen any test case, and actually remove all calls the BuDDy's GC in bdd.test. * spot/twaalgos/translate.cc, spot/twaalgos/translate.hh, spot/tl/simplify.cc, spot/tl/simplify.hh, spot/tl/contain.hh, spot/tl/contain.cc, spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/ltl2tgba_fm.hh: Add support for the option or its constraint via an output_aborter. * bin/spot-x.cc, NEWS: Document it. * tests/core/bdd.test: Adjust and augment test case. --- NEWS | 7 +++++++ bin/spot-x.cc | 3 +++ spot/tl/contain.cc | 18 +++++++++++++++--- spot/tl/contain.hh | 7 +++++-- spot/tl/simplify.cc | 3 ++- spot/tl/simplify.hh | 3 +++ spot/twaalgos/ltl2tgba_fm.cc | 10 +++++++++- spot/twaalgos/ltl2tgba_fm.hh | 10 ++++++++-- spot/twaalgos/translate.cc | 3 +++ spot/twaalgos/translate.hh | 3 ++- tests/core/bdd.test | 10 +++++++++- 11 files changed, 66 insertions(+), 11 deletions(-) diff --git a/NEWS b/NEWS index 261418295..c540aec68 100644 --- a/NEWS +++ b/NEWS @@ -104,6 +104,13 @@ New in spot 2.9.4.dev (not yet released) automaton, but we should not waste too much space and time trying that. + spot::translator additionally honor the following new variable: + + tls-max-states Maximum number of states of automata involved in + automata-based implication checks for formula + simplifications. Defaults to 64. + + Python: - Bindings for functions related to parity games. diff --git a/bin/spot-x.cc b/bin/spot-x.cc index ce15fed27..2f74bf167 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -44,6 +44,9 @@ static const argp_option options[] = (2) additionally allows automata-based implication checks, (3) enables \ more rules based on automata-based implication checks. The default value \ depends on the --low, --medium, or --high settings.") }, + { DOC("tls-max-states", + "Maximum number of states of automata involved in automata-based \ +implication checks for formula simplifications. Defaults to 64.") }, { nullptr, 0, nullptr, 0, "Translation options:", 0 }, { DOC("ltl-split", "Set to 0 to disable the translation of automata \ as product or sum of subformulas.") }, diff --git a/spot/tl/contain.cc b/spot/tl/contain.cc index a6cb12806..858afc52d 100644 --- a/spot/tl/contain.cc +++ b/spot/tl/contain.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009-2012, 2014-2016, 2018, 2019 Laboratoire de Recherche +// Copyright (C) 2009-2012, 2014-2016, 2018-2020 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -52,12 +52,15 @@ namespace spot language_containment_checker::language_containment_checker (bdd_dict_ptr dict, bool exprop, bool symb_merge, - bool branching_postponement, bool fair_loop_approx) + bool branching_postponement, bool fair_loop_approx, + unsigned max_states) : dict_(dict), exprop_(exprop), symb_merge_(symb_merge), branching_postponement_(branching_postponement), fair_loop_approx_(fair_loop_approx), translated_(new trans_map_) { + if (max_states) + aborter_ = std::make_unique(max_states); } language_containment_checker::~language_containment_checker() @@ -104,7 +107,11 @@ namespace spot return false; trim_common_Xs(l, g); record_* rl = register_formula_(l); + if (!rl->translation) + return false; record_* rg = register_formula_(g); + if (!rg->translation) + return false; return incompatible_(rl, rg); } @@ -139,7 +146,11 @@ namespace spot if (l == g) return true; record_* rl = register_formula_(l); + if (!rl->translation) + return false; record_* rg = register_formula_(g); + if (!rg->translation) + return false; if (isomorphism_checker::are_isomorphic(rl->translation, rg->translation)) return true; return contained(l, g) && contained(g, l); @@ -153,7 +164,8 @@ namespace spot return &i->second; auto e = ltl_to_tgba_fm(f, dict_, exprop_, symb_merge_, - branching_postponement_, fair_loop_approx_); + branching_postponement_, fair_loop_approx_, + nullptr, nullptr, false, aborter_.get()); return &translated_->emplace(f, std::move(e)).first->second; } } diff --git a/spot/tl/contain.hh b/spot/tl/contain.hh index 20fa714fd..28d83172f 100644 --- a/spot/tl/contain.hh +++ b/spot/tl/contain.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011-2016, 2019 Laboratoire de Recherche +// Copyright (C) 2011-2016, 2019, 2020 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -24,6 +24,7 @@ #include #include +#include namespace spot { @@ -41,7 +42,8 @@ namespace spot bool exprop = false, bool symb_merge = true, bool branching_postponement = false, - bool fair_loop_approx = false); + bool fair_loop_approx = false, + unsigned max_states = 0U); ~language_containment_checker(); @@ -72,5 +74,6 @@ namespace spot /* Translation Maps */ trans_map_* translated_; tl_simplifier_cache* c_; + std::unique_ptr aborter_ = nullptr; }; } diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index 2848c3e9e..1a7f179b3 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -70,7 +70,8 @@ namespace spot tl_simplifier_cache(const bdd_dict_ptr& d, const tl_simplifier_options& opt) - : dict(d), options(opt), lcc(d, true, true, false, false) + : dict(d), options(opt), + lcc(d, true, true, false, false, opt.containment_max_states) { options.containment_checks |= options.containment_checks_stronger; options.event_univ |= options.favor_event_univ; diff --git a/spot/tl/simplify.hh b/spot/tl/simplify.hh index 7ecde7498..e5838544d 100644 --- a/spot/tl/simplify.hh +++ b/spot/tl/simplify.hh @@ -93,6 +93,9 @@ namespace spot // &,|, and X operators. Only rewrite Xor and Equiv under // temporal operators. bool keep_top_xor; + // If greater than 0, bound the number of states used by automata + // in containment checks. + unsigned containment_max_states = 0; }; // fwd declaration to hide technical details. diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index 33019fe22..c560bc2e3 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -1947,7 +1947,8 @@ namespace spot ltl_to_tgba_fm(formula f2, const bdd_dict_ptr& dict, bool exprop, bool symb_merge, bool branching_postponement, bool fair_loop_approx, const atomic_prop_set* unobs, - tl_simplifier* simplifier, bool unambiguous) + tl_simplifier* simplifier, bool unambiguous, + const output_aborter* aborter) { tl_simplifier* s = simplifier; @@ -2051,6 +2052,13 @@ namespace spot dest_map dests; while (!formulae_to_translate.empty()) { + if (aborter && aborter->too_large(a)) + { + if (!simplifier) + delete s; + return nullptr; + } + // Pick one formula. formula now = *formulae_to_translate.begin(); formulae_to_translate.erase(formulae_to_translate.begin()); diff --git a/spot/twaalgos/ltl2tgba_fm.hh b/spot/twaalgos/ltl2tgba_fm.hh index 76a5a15b9..8c1827490 100644 --- a/spot/twaalgos/ltl2tgba_fm.hh +++ b/spot/twaalgos/ltl2tgba_fm.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2017, 2019 Laboratoire de +// Copyright (C) 2010-2015, 2017, 2019-2020 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -26,6 +26,7 @@ #include #include #include +#include namespace spot { @@ -73,6 +74,10 @@ namespace spot /// \param unambiguous When true, unambigous TGBA will be produced /// using the trick described in \cite benedikt.13.tacas . /// + /// \param aborter When given, aborts the construction whenever the + /// constructed automaton would become larger than specified by the + /// output_aborter. + /// /// \return A spot::twa_graph that recognizes the language of \a f. SPOT_API twa_graph_ptr ltl_to_tgba_fm(formula f, const bdd_dict_ptr& dict, @@ -81,5 +86,6 @@ namespace spot bool fair_loop_approx = false, const atomic_prop_set* unobs = nullptr, tl_simplifier* simplifier = nullptr, - bool unambiguous = false); + bool unambiguous = false, + const output_aborter* aborter = nullptr); } diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 4415a6439..dcdcb8175 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -60,11 +60,14 @@ namespace spot gf_guarantee_set_ = true; } ltl_split_ = opt->get("ltl-split", 1); + int tls_max_states = opt->get("tls-max-states", 64); + tls_max_states_ = std::max(0, tls_max_states); } void translator::build_simplifier(const bdd_dict_ptr& dict) { tl_simplifier_options options(false, false, false); + options.containment_max_states = tls_max_states_; switch (level_) { case High: diff --git a/spot/twaalgos/translate.hh b/spot/twaalgos/translate.hh index db65348dd..344cae3ba 100644 --- a/spot/twaalgos/translate.hh +++ b/spot/twaalgos/translate.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2018, 2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -154,6 +154,7 @@ namespace spot bool gf_guarantee_ = true; bool gf_guarantee_set_ = false; bool ltl_split_; + unsigned tls_max_states_ = 0; const option_map* opt_; }; /// @} diff --git a/tests/core/bdd.test b/tests/core/bdd.test index e70216a11..ba2e11232 100755 --- a/tests/core/bdd.test +++ b/tests/core/bdd.test @@ -23,7 +23,8 @@ set -e # Make sure that setting the SPOT_BDD_TRACE envvar actually does # something. -genltl --kr-nlogn=2 | SPOT_BDD_TRACE=1 ltl2tgba -D >out 2>err +genltl --kr-nlogn=2 | + SPOT_BDD_TRACE=1 ltl2tgba -x tls-max-states=0 -D >out 2>err cat err grep spot: out && exit 1 grep 'spot: BDD package initialized' err @@ -34,3 +35,10 @@ test 11 = `grep -c 'spot: BDD GC' err` # Minimal size for this automaton. # See also https://www.lrde.epita.fr/dload/spot/mochart10-fixes.pdf test "147,207" = `autfilt --stats=%s,%e out` + +# With the default value of tls-max-states, no GC is needed +genltl --kr-nlogn=2 | SPOT_BDD_TRACE=1 ltl2tgba -D --stats=%s,%e >out 2>err +cat err +grep 'spot: BDD package initialized' err +test 0 = `grep -c 'spot: BDD GC' err` +test "147,207" = `cat out`