diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 8d6147a7e..7a9fa580d 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -91,6 +91,12 @@ 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("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.") }, + { DOC("det-stutter", "Set to 0 to disable optimizations based on \ +the stutter-invariance in the determinization algorithm.") }, { DOC("simul", "Set to 0 to disable simulation-based reductions. \ 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. \ diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 6c1abc328..b75a7ddaf 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -729,7 +729,7 @@ expectations. deterministic TGBA exists. #+NAME: ltl2tgba-fga -#+BEGIN_SRC sh :results verbatim :exports none +#+BEGIN_SRC sh :results verbatim :exports code ltl2tgba "FGa" -D -d.a #+END_SRC @@ -743,7 +743,7 @@ ltl2tgba "FGa" -D -d.a But with =--generic=, =ltl2tgba= will output the following Rabin automaton: #+NAME: ltl2tgba-fga-D -#+BEGIN_SRC sh :results verbatim :exports none +#+BEGIN_SRC sh :results verbatim :exports code ltl2tgba "FGa" -G -D -d.a #+END_SRC @@ -758,6 +758,40 @@ Note that determinization algorithm implemented actually outputs parity acceptance, but =Fin(0)&Inf(1)= can be interpreted either as =Rabin 1= or =parity min odd 2=. + +The [[./man/spot-x.7.html][=spot-x=]](7) man page lists a few =-x= options (=det-scc=, +=det-simul=, =det-stutter=) of the determinization algorithm that are +enable by default, but that you may want to disable for experimental +purpose. + +For instance the following deterministic automaton + +#+NAME: ltl2tgba-det1 +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba "F(a W FGb)" -G -D -d.a +#+END_SRC + +#+BEGIN_SRC dot :file ltl2tgba-det1.png :cmdline -Tpng :var txt=ltl2tgba-det1 :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:ltl2tgba-det1.png]] + +would be larger if SCC-based optimizations were disabled: + +#+NAME: ltl2tgba-det2 +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba "F(a W FGb)" -x '!det-scc' -G -D -d.a +#+END_SRC + +#+BEGIN_SRC dot :file ltl2tgba-det2.png :cmdline -Tpng :var txt=ltl2tgba-det2 :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:ltl2tgba-det2.png]] + * Translating multiple formulas for statistics If multiple formulas are given to =ltl2tgba=, the corresponding diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 9c6ddd421..d674fa1f5 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -53,12 +53,6 @@ namespace spot } postprocessor::postprocessor(const option_map* opt) - : type_(TGBA), pref_(Small), level_(High), - degen_reset_(true), degen_order_(false), degen_cache_(true), - degen_lskip_(true), degen_lowinit_(false), simul_(-1), - scc_filter_(-1), ba_simul_(-1), - tba_determinisation_(false), sat_minimize_(0), sat_acc_(0), - sat_states_(0), state_based_(false), wdba_minimize_(true) { if (opt) { @@ -67,6 +61,9 @@ namespace spot degen_cache_ = opt->get("degen-lcache", 1); degen_lskip_ = opt->get("degen-lskip", 1); degen_lowinit_ = opt->get("degen-lowinit", 0); + det_scc_ = opt->get("det-scc", 1); + det_simul_ = opt->get("det-simul", 1); + det_stutter_ = opt->get("det-stutter", 1); simul_ = opt->get("simul", -1); scc_filter_ = opt->get("scc-filter", -1); ba_simul_ = opt->get("ba-simul", -1); @@ -366,7 +363,8 @@ namespace spot if (PREF_ == Deterministic && type_ == Generic && !dba) { - dba = tgba_determinize(to_generalized_buchi(sim)); + dba = tgba_determinize(to_generalized_buchi(sim), + false, det_scc_, det_simul_, det_stutter_); if (level_ != Low) dba = simulation(dba); sim = nullptr; diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index 0533a3460..76f08c94e 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -172,24 +172,27 @@ namespace spot twa_graph_ptr do_scc_filter(const twa_graph_ptr& a, bool arg); twa_graph_ptr do_scc_filter(const twa_graph_ptr& a); - output_type type_; - int pref_; - optimization_level level_; + output_type type_ = TGBA; + int pref_ = Small; + optimization_level level_ = High; // Fine-tuning options fetched from the option_map. - bool degen_reset_; - bool degen_order_; - int degen_cache_; - bool degen_lskip_; - bool degen_lowinit_; - int simul_; - int scc_filter_; - int ba_simul_; - bool tba_determinisation_; - int sat_minimize_; - int sat_acc_; - int sat_states_; - bool state_based_; - bool wdba_minimize_; + bool degen_reset_ = true; + bool degen_order_ = false; + int degen_cache_ = true; + bool degen_lskip_ = true; + bool degen_lowinit_ = false; + bool det_scc_ = true; + bool det_simul_ = true; + bool det_stutter_ = true; + int simul_ = -1; + int scc_filter_ = -1; + int ba_simul_ = -1; + bool tba_determinisation_ = false; + int sat_minimize_ = 0; + int sat_acc_ = 0; + int sat_states_ = 0; + bool state_based_ = false; + bool wdba_minimize_ = true; }; /// @} }