diff --git a/NEWS b/NEWS index d2836f658..4cbfe8128 100644 --- a/NEWS +++ b/NEWS @@ -7,6 +7,17 @@ New in spot 2.9.0.dev (not yet released) ltl2tgba -D -G '(Fa & Fb & Fc & Fd) <-> GFe' now produces a 16-state automaton (instead of 31 in Spot 2.9). + - Option '-x wdba-minize=N' used to accept N=0 (off), or N=1 (on). + It can now take three values: + 0: never attempt this optimization, + 1: always try to determinize and minimize automata as WDBA, + and check (if needed) that the result is correct, + 2: determinize and minimize automata as WDBA only if it is known + beforehand (by cheap syntactic means) that the result will be + correct (e.g., the input formula is a syntactic obligation). + The default is 1 in "--high" mode, 2 in "--medium" mode or in + "--deterministic --low" mode, and 0 in other "--low" modes. + Library: - product_xor() and product_xnor() are two new versions of the diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 90c6eec3d..007e23233 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -152,8 +152,10 @@ abstracted as atomic propositions during the translation to automaton. \ This relabeling can speeds the translation if a few Boolean subformulas \ use a large number of atomic propositions. By default N=4. Setting \ this value to 0 will disable the rewriting.") }, - { DOC("wdba-minimize", "Set to 0 to disable WDBA-minimization. \ -Enabled by default.") }, + { DOC("wdba-minimize", "Set to 0 to disable WDBA-minimization, to 1 to \ +always try it, or 2 to attempt it only on syntactic obligations or on automata \ +that are weak and deterministic. The default is 1 in --high mode, else 2 in \ +--medium or --deterministic modes, else 0 in --low mode.") }, { DOC("tba-det", "Set to 1 to attempt a powerset determinization \ if the TGBA is not already deterministic. Doing so will degeneralize \ the automaton. This is disabled by default, unless sat-minimize is set.") }, diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index e637e3fe8..f9188f0b1 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2010-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -567,6 +567,16 @@ namespace spot return product(min_aut, aut_neg)->is_empty(); } + bool minimize_obligation_garanteed_to_work(const const_twa_graph_ptr& aut_f, + formula f) + { + // WDBA-minimization necessarily work for obligations + return ((f && f.is_syntactic_obligation()) + // Weak deterministic automata are obligations + || (aut_f->prop_weak().is_true() && is_deterministic(aut_f)) + // Guarantee automata are obligations as well. + || is_terminal_automaton(aut_f)); + } twa_graph_ptr minimize_obligation(const const_twa_graph_ptr& aut_f, @@ -580,12 +590,7 @@ namespace spot ("minimize_obligation() does not support alternation"); bool minimization_will_be_correct = false; - // WDBA-minimization necessarily work for obligations - if ((f && f.is_syntactic_obligation()) - // Weak deterministic automata are obligations - || (aut_f->prop_weak() && is_deterministic(aut_f)) - // Guarantee automata are obligations as well. - || is_terminal_automaton(aut_f)) + if (minimize_obligation_garanteed_to_work(aut_f, f)) { minimization_will_be_correct = true; } diff --git a/spot/twaalgos/minimize.hh b/spot/twaalgos/minimize.hh index 9bf1f796b..0b454654a 100644 --- a/spot/twaalgos/minimize.hh +++ b/spot/twaalgos/minimize.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2018, 2019 -// Laboratoire de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009-2016, 2018-2020 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -116,5 +116,23 @@ namespace spot const_twa_graph_ptr aut_neg_f = nullptr, bool reject_bigger = false, const output_aborter* aborter = nullptr); + + /// \brief Whether calling minimize_obligation is sure to work + /// + /// This checks whether \a f is a syntactic obligation, or if \a + /// aut_f obviously corresponds to an obligation (for instance if + /// this is a terminal automaton, or if it is both weak and + /// deterministic). In this case, calling minimize_obligation() + /// should not be a waste of time, as it will return a new + /// automaton. + /// + /// If this function returns false, the input property might still + /// be a pathological obligation. The only way to know is to call + /// minimize_obligation(), but as it is less likely, you might + /// decide to save time. + SPOT_API + bool minimize_obligation_garanteed_to_work(const const_twa_graph_ptr& aut_f, + formula f = nullptr); + /// @} } diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 3d9df7e1f..36d0345bf 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -83,7 +83,7 @@ namespace spot sat_acc_ = opt->get("sat-acc", 0); sat_states_ = opt->get("sat-states", 0); state_based_ = opt->get("state-based", 0); - wdba_minimize_ = opt->get("wdba-minimize", 1); + wdba_minimize_ = opt->get("wdba-minimize", -1); gen_reduce_parity_ = opt->get("gen-reduce-parity", 1); if (sat_acc_ && sat_minimize_ == 0) @@ -371,9 +371,19 @@ namespace spot output_aborter* aborter = (det_max_states_ >= 0 || det_max_edges_ >= 0) ? &aborter_ : nullptr; - // (Small,Low) is the only configuration where we do not run - // WDBA-minimization. - if ((PREF_ != Small || level_ != Low) && wdba_minimize_) + int wdba_minimize = wdba_minimize_; + if (wdba_minimize == -1) + { + if (level_ == High) + wdba_minimize = 1; + else if (level_ == Medium || PREF_ == Deterministic) + wdba_minimize = 2; + else + wdba_minimize = 0; + } + if (wdba_minimize == 2) + wdba_minimize = minimize_obligation_garanteed_to_work(a, f); + if (wdba_minimize) { bool reject_bigger = (PREF_ == Small) && (level_ <= Medium); dba = minimize_obligation(a, f, nullptr, reject_bigger, aborter); diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index 5b739e5b7..3fbd07060 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -253,7 +253,7 @@ namespace spot int sat_states_ = 0; int gen_reduce_parity_ = 1; bool state_based_ = false; - bool wdba_minimize_ = true; + int wdba_minimize_ = -1; }; /// @} } diff --git a/tests/core/genltl.test b/tests/core/genltl.test index 4a85c7c66..271820d8d 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -132,12 +132,12 @@ genltl --kr-n2=1..2 --kr-nlogn=1..2 --kr-n=1..2 --gxf-and=0..3 --fxg-or=0..3 \ --pps-arbiter-standard=2..3 --pps-arbiter-strict=2..3 --format=%F=%L,%f | ltl2tgba --low --det -F-/2 --stats='%<,%s' > out cat >exp<