diff --git a/NEWS b/NEWS index 35b7ca790..04d76a96e 100644 --- a/NEWS +++ b/NEWS @@ -129,36 +129,50 @@ New in spot 2.9.6.dev (not yet released) - print_dot() will display states from player 1 using a diamond shape. - - spot::postproc has two extra configuration variables that are meant - to speedup the processing of large automata. + - spot::postproc has new configuration variables that define + thresholds to disable some costly operation in order to speedup + the processing of large automata. (Those variables are typically + modified using the -x option of command-line tools, and are all + documented in the spot-x(7) man page.) - simul-max Number of states above which simulation-based - reductions are skipped. Defaults to 512. Set to 0 - to disable. This also applies to the - simulation-based optimization of the - determinization algorithm. wdba-det-max Maximum number of additional states allowed in - intermediate steps of WDBA-minimization. If the + intermediate steps of WDBA-minimization. If the number of additional states reached in the powerset construction or in the followup products exceeds this value, WDBA-minimization is aborted. - Defaults to 4096. Set to 0 to disable. This limit + Defaults to 4096. Set to 0 to disable. This limit is ignored when -D used or when det-max-states is set. - The reason for disabling simulation-based reduction above 512 - states is that the current implementation uses one BDD variable - per state, and makes a number of BDD operations that is quadratic - in the number of states. Similarly, WDBA-mininimization is used - with --small in the off chance that it might produce a smaller - automaton, but we should not waste too much space and time trying - that. + simul-max Number of states above which simulation-based + reductions are skipped. Defaults to 4096. Set + to 0 to disable. This also applies to the + simulation-based optimization of the + determinization algorithm. + + simul-trans-pruning + For simulation-based reduction, this is the + number of equivalence classes above which + transition-pruning for non-deterministic automata + is disabled. Defaults to 512. Set to 0 to + disable. This applies to all simulation-based + reduction, as well as to the simulation-based + optimization of the determinization algorithm. + Simulation-based reduction perform a number of + BDD implication checks that is quadratic in the + number of classes to implement transition pruning. + + dpa-simul Set to 0/1 to disable/enable simulation-based + reduction performed after running a Safra-like + determinization to optain a DPA. By default, it + is activated at all levels but --low. spot::translator additionally honor the following new variables: tls-max-states Maximum number of states of automata involved in automata-based implication checks for formula simplifications. Defaults to 64. + exprop When set, this causes the core LTL translation to explicitly iterate over all possible valuations of atomic propositions when considering the successors diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 9c310d100..8b3f6ecca 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -123,9 +123,15 @@ will be returned.")}, { 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 \ -the determinization algorithm.") }, +the determinization algorithm. (Do not confuse this with option dpa-simul, \ +which runs a simulation-based reduction after determinization.)") }, { DOC("det-stutter", "Set to 0 to disable optimizations based on \ the stutter-invariance in the determinization algorithm.") }, + { DOC("dpa-simul", "Set to 1 to enable simulation-based reduction after \ +running a Safra-like determinization to obtain a DPA, or 0 to disable. By \ +default is is enabled at all levels except low. (Do not confuse this with \ +option det-simul, which uses a simulation-based optimizations during \ +the determinization.)") }, { DOC("gen-reduce-parity", "When the postprocessor routines are \ configured to output automata with any kind of acceptance condition, \ but they happen to process an automaton with parity acceptance, they \ @@ -156,9 +162,18 @@ Set to 1 to use only direct simulation. Set to 2 to use only reverse \ simulation. Set to 3 to iterate both direct and reverse simulations. \ The default is 3 in --high mode, and 0 otherwise.") }, { DOC("simul-max", "Number of states above which simulation-based \ -reductions are skipped. Defaults to 512. Set to 0 to disable. This also \ -applies to the simulation-based optimization of the determinization \ -algorithm.") }, +reductions are skipped. Defaults to 4096. Set to 0 to disable. This \ +applies to all simulation-based optimization, including thoses of the \ +determinization algorithm.") }, + { DOC("simul-trans-pruning", "Number of equivalence classes above which \ +simulation-based transition-pruning for non-deterministic automata is disabled \ +automata. Defaults to 512. Set to 0 to disable. This applies to all \ +simulation-based reduction, as well as to the simulation-based optimization of \ +the determinization algorithm. Simulation-based reduction perform a number of \ +BDD implication checks that is quadratic in the number of classes to implement \ +transition pruning. The equivalence classes is equal to the number \ +of output states of simulation-based reduction when transition-pruning is \ +disabled, it is just an upper bound otherwise.") }, { DOC("relabel-bool", "If set to a positive integer N, a formula \ with N atomic propositions or more will have its Boolean subformulas \ abstracted as atomic propositions during the translation to automaton. \ diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index 00fe04ee2..3e361a813 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -811,7 +811,8 @@ namespace spot tgba_determinize(const const_twa_graph_ptr& a, bool pretty_print, bool use_scc, bool use_simulation, bool use_stutter, - const output_aborter* aborter) + const output_aborter* aborter, + int trans_pruning) { if (!a->is_existential()) throw std::runtime_error @@ -829,7 +830,7 @@ namespace spot if (use_simulation) { aut_tmp = spot::scc_filter(aut_tmp); - auto aut2 = simulation(aut_tmp, &implications); + auto aut2 = simulation(aut_tmp, &implications, trans_pruning); if (pretty_print) aut2->copy_state_names_from(aut_tmp); aut_tmp = aut2; diff --git a/spot/twaalgos/determinize.hh b/spot/twaalgos/determinize.hh index c588ff9aa..61b69f6fb 100644 --- a/spot/twaalgos/determinize.hh +++ b/spot/twaalgos/determinize.hh @@ -77,11 +77,16 @@ namespace spot /// \param aborter abort the construction if the constructed /// automaton would be too large. Return nullptr /// in this case. + /// + /// \param trans_pruning when \a use_simulation is true, \a trans_pruning + /// is passed to the simulation-based reduction to limit + /// the effect of transition pruning. SPOT_API twa_graph_ptr tgba_determinize(const const_twa_graph_ptr& aut, bool pretty_print = false, bool use_scc = true, bool use_simulation = true, bool use_stutter = true, - const output_aborter* aborter = nullptr); + const output_aborter* aborter = nullptr, + int trans_pruning = -1); } diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 962a79ebf..8011cf285 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -75,6 +75,7 @@ namespace spot det_max_edges_ = opt->get("det-max-edges", -1); simul_ = opt->get("simul", -1); simul_method_ = opt->get("simul-method", -1); + dpa_simul_ = opt->get("dpa-simul", -1); scc_filter_ = opt->get("scc-filter", -1); ba_simul_ = opt->get("ba-simul", -1); tba_determinisation_ = opt->get("tba-det", 0); @@ -86,8 +87,9 @@ namespace spot state_based_ = opt->get("state-based", 0); wdba_minimize_ = opt->get("wdba-minimize", -1); gen_reduce_parity_ = opt->get("gen-reduce-parity", 1); - simul_max_ = opt->get("simul-max", 512); + simul_max_ = opt->get("simul-max", 4096); wdba_det_max_ = opt->get("wdba-det-max", 4096); + simul_trans_pruning_ = opt->get("simul-trans-pruning", 512); if (sat_acc_ && sat_minimize_ == 0) sat_minimize_ = 1; // Dicho. @@ -113,11 +115,10 @@ namespace spot twa_graph_ptr postprocessor::do_simul(const twa_graph_ptr& a, int opt) const { - if (simul_max_ > 0 && static_cast(simul_max_) < a->num_states()) - return a; - if (opt == 0) return a; + if (simul_max_ > 0 && static_cast(simul_max_) < a->num_states()) + return a; static unsigned sim = [&]() { @@ -131,18 +132,18 @@ namespace spot if (sim == 2) opt += 3; - // FIXME: simulation-based reduction how have work-arounds for + // FIXME: simulation-based reduction now have work-arounds for // non-separated sets, so we can probably try them. if (!has_separate_sets(a)) return a; switch (opt) { case 1: - return simulation(a); + return simulation(a, simul_trans_pruning_); case 2: - return cosimulation(a); + return cosimulation(a, simul_trans_pruning_); case 3: - return iterated_simulations(a); + return iterated_simulations(a, simul_trans_pruning_); case 4: return reduce_direct_sim(a); case 5: @@ -150,7 +151,7 @@ namespace spot case 6: return reduce_iterated(a); default: - return iterated_simulations(a); + return iterated_simulations(a, simul_trans_pruning_); } } @@ -166,12 +167,12 @@ namespace spot case 0: return a; case 1: - return simulation_sba(a); + return simulation_sba(a, simul_trans_pruning_); case 2: - return cosimulation_sba(a); + return cosimulation_sba(a, simul_trans_pruning_); case 3: default: - return iterated_simulations_sba(a); + return iterated_simulations_sba(a, simul_trans_pruning_); } } @@ -266,6 +267,8 @@ namespace spot simul_ = (level_ == Low) ? 1 : 3; if (ba_simul_ < 0) ba_simul_ = (level_ == High) ? 3 : 0; + if (dpa_simul_ < 0) + dpa_simul_ = (level_ != Low) ? 1 : 0; if (scc_filter_ < 0) scc_filter_ = 1; if (type_ == BA) @@ -551,14 +554,13 @@ namespace spot det_simul = false; dba = tgba_determinize(tba, false, det_scc_, det_simul, det_stutter_, - aborter); + aborter, simul_trans_pruning_); // Setting det-max-states or det-max-edges may cause tgba_determinize // to fail. + if (dba) { - dba = simplify_acc(dba); - if (level_ != Low) - dba = simulation(dba); + dba = do_simul(simplify_acc(dba), dpa_simul_); sim = nullptr; } } diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index b6e77ffec..fc4ba9413 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -253,6 +253,8 @@ namespace spot int det_max_edges_ = -1; int simul_ = -1; int simul_method_ = -1; + int simul_trans_pruning_ = 512; + int dpa_simul_ = -1; int scc_filter_ = -1; int ba_simul_ = -1; bool tba_determinisation_ = false; @@ -264,7 +266,7 @@ namespace spot int gen_reduce_parity_ = 1; bool state_based_ = false; int wdba_minimize_ = -1; - int simul_max_ = 512; + int simul_max_ = 4096; int wdba_det_max_ = 4096; }; /// @} diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index 066536638..e62762489 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -154,10 +154,12 @@ namespace spot } direct_simulation(const const_twa_graph_ptr& in, + int trans_pruning, std::vector* implications = nullptr) : po_size_(0), all_class_var_(bddtrue), original_(in), + trans_pruning_(trans_pruning), record_implications_(implications) { if (!has_separate_sets(in)) @@ -467,13 +469,18 @@ namespace spot } // Update the partial order. + // + // Do not compute implication between classes if we have more + // classes than trans_pruning_, or if the automaton is + // deterministic (in which case want_implications_ was + // initialized to false). The number of classes should only + // augment, so if we exceed trans_pruning_, it's safe to + // disable want_implications_ for good. - // This loop follows the pattern given by the paper. - // foreach class do - // | foreach class do - // | | update po if needed - // | od - // od + if (want_implications_ + && trans_pruning_ >= 0 + && static_cast(trans_pruning_) < sz) + want_implications_ = false; for (unsigned n = 0; n < sz; ++n) { @@ -773,7 +780,7 @@ namespace spot if (!need_another_pass) return res; - direct_simulation sim(res); + direct_simulation sim(res, trans_pruning_); return sim.run(); } @@ -861,16 +868,16 @@ namespace spot automaton_size stat; const const_twa_graph_ptr original_; - + int trans_pruning_; std::vector* record_implications_; }; template twa_graph_ptr - wrap_simul(Fun f, const Aut& a) + wrap_simul(Fun f, const Aut& a, int trans_pruning) { if (has_separate_sets(a)) - return f(a); + return f(a, trans_pruning); // If the input has acceptance sets common to Fin and Inf, // separate them before doing the simulation, and merge them // back afterwards. Doing will temporarily introduce more sets @@ -879,62 +886,63 @@ namespace spot // automata sharing Fin/Inf sets. auto b = make_twa_graph(a, twa::prop_set::all()); separate_sets_here(b); - return simplify_acceptance_here(f(b)); + return simplify_acceptance_here(f(b, trans_pruning)); } } // End namespace anonymous. twa_graph_ptr - simulation(const const_twa_graph_ptr& t) + simulation(const const_twa_graph_ptr& t, int trans_pruning) { - return wrap_simul([](const const_twa_graph_ptr& t) { - direct_simulation simul(t); - return simul.run(); - }, t); + return wrap_simul([](const const_twa_graph_ptr& t, int trans_pruning) { + direct_simulation simul(t, trans_pruning); + return simul.run(); + }, t, trans_pruning); } twa_graph_ptr simulation(const const_twa_graph_ptr& t, - std::vector* implications) + std::vector* implications, int trans_pruning) { - return wrap_simul([implications](const const_twa_graph_ptr& t) { - direct_simulation simul(t, implications); - return simul.run(); - }, t); + return wrap_simul([implications](const const_twa_graph_ptr& t, + int trans_pruning) { + direct_simulation simul(t, trans_pruning, implications); + return simul.run(); + }, t, trans_pruning); } twa_graph_ptr - simulation_sba(const const_twa_graph_ptr& t) + simulation_sba(const const_twa_graph_ptr& t, int trans_pruning) { - return wrap_simul([](const const_twa_graph_ptr& t) { - direct_simulation simul(t); - return simul.run(); - }, t); + return wrap_simul([](const const_twa_graph_ptr& t, int trans_pruning) { + direct_simulation simul(t, trans_pruning); + return simul.run(); + }, t, trans_pruning); } twa_graph_ptr - cosimulation(const const_twa_graph_ptr& t) + cosimulation(const const_twa_graph_ptr& t, int trans_pruning) { - return wrap_simul([](const const_twa_graph_ptr& t) { - direct_simulation simul(t); - return simul.run(); - }, t); + return wrap_simul([](const const_twa_graph_ptr& t, int trans_pruning) { + direct_simulation simul(t, trans_pruning); + return simul.run(); + }, t, trans_pruning); } twa_graph_ptr - cosimulation_sba(const const_twa_graph_ptr& t) + cosimulation_sba(const const_twa_graph_ptr& t, int trans_pruning) { - return wrap_simul([](const const_twa_graph_ptr& t) { - direct_simulation simul(t); - return simul.run(); - }, t); + return wrap_simul([](const const_twa_graph_ptr& t, int trans_pruning) { + direct_simulation simul(t, trans_pruning); + return simul.run(); + }, t, trans_pruning); } template twa_graph_ptr - iterated_simulations_(const const_twa_graph_ptr& t) + iterated_simulations_(const const_twa_graph_ptr& t, int trans_pruning) { twa_graph_ptr res = nullptr; automaton_size prev; @@ -943,12 +951,12 @@ namespace spot do { prev = next; - direct_simulation simul(res ? res : t); + direct_simulation simul(res ? res : t, trans_pruning); res = simul.run(); if (res->prop_universal()) break; - direct_simulation cosimul(res); + direct_simulation cosimul(res, trans_pruning); res = cosimul.run(); if (Sba) @@ -963,15 +971,15 @@ namespace spot } twa_graph_ptr - iterated_simulations(const const_twa_graph_ptr& t) + iterated_simulations(const const_twa_graph_ptr& t, int trans_pruning) { - return wrap_simul(iterated_simulations_, t); + return wrap_simul(iterated_simulations_, t, trans_pruning); } twa_graph_ptr - iterated_simulations_sba(const const_twa_graph_ptr& t) + iterated_simulations_sba(const const_twa_graph_ptr& t, int trans_pruning) { - return wrap_simul(iterated_simulations_, t); + return wrap_simul(iterated_simulations_, t, trans_pruning); } template diff --git a/spot/twaalgos/simulation.hh b/spot/twaalgos/simulation.hh index d4adc2e4a..3965f10d4 100644 --- a/spot/twaalgos/simulation.hh +++ b/spot/twaalgos/simulation.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2015, 2017, 2019 Laboratoire de Recherche et +// Copyright (C) 2012-2015, 2017, 2019, 2021 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -36,7 +36,8 @@ namespace spot /// described in \cite babiak.13.spin . /// /// Our reconstruction of the quotient automaton based on this - /// suffix-inclusion relation will also improve determinism. + /// suffix-inclusion relation will also improve determinism thanks + /// to a kind of transition-pruning. /// /// We recommend to call scc_filter() to first simplify the /// automaton that should be reduced by simulation. @@ -47,22 +48,33 @@ namespace spot /// acceptance conditions than necessary, and running scc_filter() /// again afterwards will remove these superfluous conditions. /// - /// The resulting automaton has a named property "simulated-states", that is a - /// vector mapping each state of the input to a state of the output. Note that - /// some input states may be mapped to -1, as a by-product of improved - /// determinism. Typically, if the language of q1 is included in the language - /// of q2, only a transition to q2 will be built. + /// + /// The resulting automaton has a named property "simulated-states", + /// that is a vector mapping each state of the input to a state of + /// the output. Note that some input states may be mapped to -1, as + /// a by-product of transition prunning. /// /// \param automaton the automaton to simulate. + /// + /// \param trans_pruning Transition pruning requires a quadratic + /// number of BDD implication checks between all equivalence + /// classes, so it can be costly on large automata. If \a + /// trans_pruning is set to a non-negative integer, only + /// (non-deterministic) automata with more states than trans_pruning + /// will be simplified. + /// /// \return a new automaton which is at worst a copy of the received /// one SPOT_API twa_graph_ptr - simulation(const const_twa_graph_ptr& automaton); + simulation(const const_twa_graph_ptr& automaton, + int trans_pruning = -1); SPOT_API twa_graph_ptr simulation(const const_twa_graph_ptr& automaton, - std::vector* implications); + std::vector* implications, + int trans_pruning = -1); SPOT_API twa_graph_ptr - simulation_sba(const const_twa_graph_ptr& automaton); + simulation_sba(const const_twa_graph_ptr& automaton, + int trans_pruning = -1); /// @} /// @{ @@ -73,7 +85,8 @@ namespace spot /// state can be merged into the latter. \cite babiak.13.spin . /// /// Our reconstruction of the quotient automaton based on this - /// prefix-inclusion relation will also improve codeterminism. + /// prefix-inclusion relation will also improve codeterminism + /// thanks to a kind of transition pruning. /// /// We recommend to call scc_filter() to first simplify the /// automaton that should be reduced by cosimulation. @@ -93,12 +106,22 @@ namespace spot /// codeterminism.) /// /// \param automaton the automaton to simulate. + /// + /// \param trans_pruning Transition pruning requires a quadratic + /// number of BDD implication checks between all equivalence + /// classes, so it can be costly on large automata. If \a + /// trans_pruning is set to a non-negative integer, only + /// (non-deterministic) automata with more states than trans_pruning + /// will be simplified. + /// /// \return a new automaton which is at worst a copy of the received /// one SPOT_API twa_graph_ptr - cosimulation(const const_twa_graph_ptr& automaton); + cosimulation(const const_twa_graph_ptr& automaton, + int trans_pruning = -1); SPOT_API twa_graph_ptr - cosimulation_sba(const const_twa_graph_ptr& automaton); + cosimulation_sba(const const_twa_graph_ptr& automaton, + int trans_pruning = -1); /// @} /// @{ @@ -117,9 +140,11 @@ namespace spot /// \return a new automaton which is at worst a copy of the received /// one SPOT_API twa_graph_ptr - iterated_simulations(const const_twa_graph_ptr& automaton); + iterated_simulations(const const_twa_graph_ptr& automaton, + int trans_pruning = -1); SPOT_API twa_graph_ptr - iterated_simulations_sba(const const_twa_graph_ptr& automaton); + iterated_simulations_sba(const const_twa_graph_ptr& automaton, + int trans_pruning = -1); /// @} /// @{ diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 4cd48ce90..c924a9a1e 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -377,5 +377,7 @@ diff out exp f='Fp0 U XX((p0 & F!p1) | (!p0 & Gp1))' ltlsynt --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err grep 'DPA has 13 states' err +ltlsynt -x dpa-simul=0 --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err +grep 'DPA has 30 states' err ltlsynt --verbose -x wdba-minimize=1 --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err grep 'DPA has 12 states' err diff --git a/tests/core/minusx.test b/tests/core/minusx.test index 2ac9ec155..d7be77ef1 100755 --- a/tests/core/minusx.test +++ b/tests/core/minusx.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016, 2020 Laboratoire de Recherche et Développement de +# Copyright (C) 2016, 2020, 2021 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -39,3 +39,8 @@ grep "autfilt: option 'other' was not used" error f='G(!p0 | (!p2 U (p1 | (!p2 & p3 & X(!p2 U p4)))) | G!p1)' test 4,1 = `ltl2tgba --stats=%s,%d "$f"` test 6,0 = `ltl2tgba -x wdba-det-max=4 --stats=%s,%d "$f"` + +# Make sure simul-max has an effect +f=`genltl --ms-phi-s=2` +test 484 -eq `ltl2tgba -P -D --stats=%s "$f"` +test 484 -lt `ltl2tgba -P -D -x simul-max=512 --stats=%s "$f"` diff --git a/tests/core/sim3.test b/tests/core/sim3.test index 57959174a..c6f6cd638 100755 --- a/tests/core/sim3.test +++ b/tests/core/sim3.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2018, 2019, 2020 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2018-2021 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -150,3 +150,33 @@ State: 6 EOF autfilt --small --low input > output diff expect output + + +cat >input <