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

postproc: add a "simul" option to select the simulation algorithm

* src/tgbaalgos/postproc.hh, src/tgbaalgos/postproc.cc: Honor the
"simul" option in the option_map.
(do_simul, do_degen): New method to wrap the algorithms that may be
altered via option_map.
* src/bin/man/ltl2tgba.x (simul): Document this option.
parent c46891ed
...@@ -26,3 +26,10 @@ it should reuse that level. The "lcache" stands for "level cache". ...@@ -26,3 +26,10 @@ it should reuse that level. The "lcache" stands for "level cache".
\fBdegen\-order\fR \fBdegen\-order\fR
If non-zero, the degeneralization algorithm will compute one degeneralization If non-zero, the degeneralization algorithm will compute one degeneralization
order for each SCC it processes. This is currently disabled by default. order for each SCC it processes. This is currently disabled by default.
.TP
\fBsimul\fR
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. The default is 3,
except when option \fB\-\-low\fR is specified, in which case the
default is 1.
...@@ -45,21 +45,58 @@ namespace spot ...@@ -45,21 +45,58 @@ namespace spot
postprocessor::postprocessor(const option_map* opt) postprocessor::postprocessor(const option_map* opt)
: type_(TGBA), pref_(Small), level_(High), : type_(TGBA), pref_(Small), level_(High),
degen_reset(true), degen_order(false), degen_cache(true) degen_reset_(true), degen_order_(false), degen_cache_(true),
simul_(-1)
{ {
if (opt) if (opt)
{ {
degen_order = opt->get("degen-order", 0); degen_order_ = opt->get("degen-order", 0);
degen_reset = opt->get("degen-reset", 1); degen_reset_ = opt->get("degen-reset", 1);
degen_cache = opt->get("degen-lcache", 1); degen_cache_ = opt->get("degen-lcache", 1);
simul_ = opt->get("simul", -1);
} }
} }
const tgba* postprocessor::do_simul(const tgba* a)
{
// supported values for simul_:
// 1 => direct simulation
// 2 => reverse-simulation only
// 3 => both simulations, iterated
if (simul_ < 0)
simul_ = (level_ == Low) ? 1 : 3;
switch (simul_)
{
case 0:
return a;
case 1:
return simulation(a);
case 2:
return cosimulation(a);
case 3:
default:
return iterated_simulations(a);
}
}
const tgba* postprocessor::do_degen(const tgba* a)
{
const tgba* d = degeneralize(a,
degen_reset_,
degen_order_,
degen_cache_);
delete a;
return d;
}
const tgba* postprocessor::run(const tgba* a, const ltl::formula* f) const tgba* postprocessor::run(const tgba* a, const ltl::formula* f)
{ {
if (type_ == TGBA && pref_ == Any && level_ == Low) if (type_ == TGBA && pref_ == Any && level_ == Low)
return a; return a;
// Remove useless SCCs. // Remove useless SCCs.
{ {
const tgba* s = scc_filter(a, false); const tgba* s = scc_filter(a, false);
...@@ -84,11 +121,10 @@ namespace spot ...@@ -84,11 +121,10 @@ namespace spot
if (pref_ == Any) if (pref_ == Any)
return a; return a;
const tgba* sim; const tgba* sim = do_simul(a);
if (level_ == Low) if (a == sim)
sim = simulation(a); // simulation was disabled.
else return a;
sim = iterated_simulations(a);
if (level_ != High) if (level_ != High)
{ {
delete a; delete a;
...@@ -113,14 +149,7 @@ namespace spot ...@@ -113,14 +149,7 @@ namespace spot
if (pref_ == Any) if (pref_ == Any)
{ {
if (type_ == BA) if (type_ == BA)
{ a = do_degen(a);
const tgba* d = degeneralize(a,
degen_reset,
degen_order,
degen_cache);
delete a;
a = d;
}
return a; return a;
} }
...@@ -135,30 +164,21 @@ namespace spot ...@@ -135,30 +164,21 @@ namespace spot
wdba = minimize_obligation(a, f, 0, reject_bigger); wdba = minimize_obligation(a, f, 0, reject_bigger);
if (wdba == a) // Minimization failed. if (wdba == a) // Minimization failed.
wdba = 0; wdba = 0;
// The WDBA is a BA, so no degeneralization required. // The WDBA is a BA, so no degeneralization is required.
} }
// Run a simulation when wdba failed (or was not run), or // Run a simulation when wdba failed (or was not run), or
// at hard levels if we want a small output. // at hard levels if we want a small output.
if (!wdba || (level_ == High && pref_ == Small)) if (!wdba || (level_ == High && pref_ == Small))
{ {
if (level_ == Low) sim = do_simul(a);
sim = simulation(a);
else
sim = iterated_simulations(a);
// Degeneralize the result of the simulation if needed. // Degeneralize the result of the simulation if needed.
if (type_ == BA) if (type_ == BA)
{ sim = do_degen(sim);
const tgba* d = degeneralize(sim,
degen_reset,
degen_order,
degen_cache);
delete sim;
sim = d;
}
} }
if (sim != a)
delete a; delete a;
if (wdba && sim) if (wdba && sim)
......
...@@ -90,13 +90,17 @@ namespace spot ...@@ -90,13 +90,17 @@ namespace spot
const tgba* run(const tgba* input_disown, const ltl::formula* f); const tgba* run(const tgba* input_disown, const ltl::formula* f);
private: private:
const tgba* do_simul(const tgba* input);
const tgba* do_degen(const tgba* input);
output_type type_; output_type type_;
output_pref pref_; output_pref pref_;
optimization_level level_; optimization_level level_;
// Fine-tuning degeneralization options. // Fine-tuning options fetched from the option_map.
bool degen_reset; bool degen_reset_;
bool degen_order; bool degen_order_;
bool degen_cache; bool degen_cache_;
int simul_;
}; };
/// @} /// @}
} }
......
Markdown is supported
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