Commit b066c6f3 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

postproc: add fine-tuning options for determinization

* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh:
Add options det-scc, det-simul, det-stutter.
* bin/spot-x.cc: Document them.
* doc/org/ltl2tgba.org: Illustrate one of them and link
to the spot-x man page.
parent 8feab7e2
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // 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 \ ...@@ -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 \ level, as it might favor finding accepting cycles earlier. If \
degen-lowinit is non-zero, then level L is always used without looking \ degen-lowinit is non-zero, then level L is always used without looking \
for the presence of an accepting self-loop.") }, 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. \ { 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 \ 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. \ simulation. Set to 3 to iterate both direct and reverse simulations. \
......
...@@ -729,7 +729,7 @@ expectations. ...@@ -729,7 +729,7 @@ expectations.
deterministic TGBA exists. deterministic TGBA exists.
#+NAME: ltl2tgba-fga #+NAME: ltl2tgba-fga
#+BEGIN_SRC sh :results verbatim :exports none #+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba "FGa" -D -d.a ltl2tgba "FGa" -D -d.a
#+END_SRC #+END_SRC
...@@ -743,7 +743,7 @@ ltl2tgba "FGa" -D -d.a ...@@ -743,7 +743,7 @@ ltl2tgba "FGa" -D -d.a
But with =--generic=, =ltl2tgba= will output the following Rabin automaton: But with =--generic=, =ltl2tgba= will output the following Rabin automaton:
#+NAME: ltl2tgba-fga-D #+NAME: ltl2tgba-fga-D
#+BEGIN_SRC sh :results verbatim :exports none #+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba "FGa" -G -D -d.a ltl2tgba "FGa" -G -D -d.a
#+END_SRC #+END_SRC
...@@ -758,6 +758,40 @@ Note that determinization algorithm implemented actually outputs ...@@ -758,6 +758,40 @@ Note that determinization algorithm implemented actually outputs
parity acceptance, but =Fin(0)&Inf(1)= can be interpreted either as parity acceptance, but =Fin(0)&Inf(1)= can be interpreted either as
=Rabin 1= or =parity min odd 2=. =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 * Translating multiple formulas for statistics
If multiple formulas are given to =ltl2tgba=, the corresponding If multiple formulas are given to =ltl2tgba=, the corresponding
......
...@@ -53,12 +53,6 @@ namespace spot ...@@ -53,12 +53,6 @@ namespace spot
} }
postprocessor::postprocessor(const option_map* opt) 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) if (opt)
{ {
...@@ -67,6 +61,9 @@ namespace spot ...@@ -67,6 +61,9 @@ namespace spot
degen_cache_ = opt->get("degen-lcache", 1); degen_cache_ = opt->get("degen-lcache", 1);
degen_lskip_ = opt->get("degen-lskip", 1); degen_lskip_ = opt->get("degen-lskip", 1);
degen_lowinit_ = opt->get("degen-lowinit", 0); 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); simul_ = opt->get("simul", -1);
scc_filter_ = opt->get("scc-filter", -1); scc_filter_ = opt->get("scc-filter", -1);
ba_simul_ = opt->get("ba-simul", -1); ba_simul_ = opt->get("ba-simul", -1);
...@@ -366,7 +363,8 @@ namespace spot ...@@ -366,7 +363,8 @@ namespace spot
if (PREF_ == Deterministic && type_ == Generic && !dba) 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) if (level_ != Low)
dba = simulation(dba); dba = simulation(dba);
sim = nullptr; sim = nullptr;
......
...@@ -172,24 +172,27 @@ namespace spot ...@@ -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, bool arg);
twa_graph_ptr do_scc_filter(const twa_graph_ptr& a); twa_graph_ptr do_scc_filter(const twa_graph_ptr& a);
output_type type_; output_type type_ = TGBA;
int pref_; int pref_ = Small;
optimization_level level_; optimization_level level_ = High;
// Fine-tuning options fetched from the option_map. // Fine-tuning options fetched from the option_map.
bool degen_reset_; bool degen_reset_ = true;
bool degen_order_; bool degen_order_ = false;
int degen_cache_; int degen_cache_ = true;
bool degen_lskip_; bool degen_lskip_ = true;
bool degen_lowinit_; bool degen_lowinit_ = false;
int simul_; bool det_scc_ = true;
int scc_filter_; bool det_simul_ = true;
int ba_simul_; bool det_stutter_ = true;
bool tba_determinisation_; int simul_ = -1;
int sat_minimize_; int scc_filter_ = -1;
int sat_acc_; int ba_simul_ = -1;
int sat_states_; bool tba_determinisation_ = false;
bool state_based_; int sat_minimize_ = 0;
bool wdba_minimize_; int sat_acc_ = 0;
int sat_states_ = 0;
bool state_based_ = false;
bool wdba_minimize_ = true;
}; };
/// @} /// @}
} }
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment