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

postproc: Perform simulation on the BA in --high mode.

* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Do simulation
on the BA produced in --high mode.
* src/bin/spot-x.cc: Document the ba-simul option that can be used
to disable it.
parent ce2bb052
...@@ -67,6 +67,11 @@ number of \"don't care\" transitions considered by the \ ...@@ -67,6 +67,11 @@ number of \"don't care\" transitions considered by the \
\"don't care\"-simulation algorithm. A negative value (the default) \ \"don't care\"-simulation algorithm. A negative value (the default) \
does not enforce any limit. Note that if there are N \"don't care\" \ does not enforce any limit. Note that if there are N \"don't care\" \
transitions, the algorithm may potentially test 2^N configurations.") }, transitions, the algorithm may potentially test 2^N configurations.") },
{ DOC("ba-simul", "Set to 0 to disable simulation-based reductions \
on the Büchi automaton (i.e., after degeneralization has been performed). \
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.") },
{ 0, 0, 0, 0, 0, 0 } { 0, 0, 0, 0, 0, 0 }
}; };
......
...@@ -46,7 +46,7 @@ namespace spot ...@@ -46,7 +46,7 @@ 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), scc_filter_(-1) simul_(-1), scc_filter_(-1), ba_simul_(-1)
{ {
if (opt) if (opt)
{ {
...@@ -56,12 +56,13 @@ namespace spot ...@@ -56,12 +56,13 @@ namespace spot
simul_ = opt->get("simul", -1); simul_ = opt->get("simul", -1);
simul_limit_ = opt->get("simul-limit", -1); simul_limit_ = opt->get("simul-limit", -1);
scc_filter_ = opt->get("scc-filter", -1); scc_filter_ = opt->get("scc-filter", -1);
ba_simul_ = opt->get("ba-simul", -1);
} }
} }
const tgba* postprocessor::do_simul(const tgba* a) const tgba* postprocessor::do_simul(const tgba* a, int opt)
{ {
switch (simul_) switch (opt)
{ {
case 0: case 0:
return a; return a;
...@@ -86,7 +87,14 @@ namespace spot ...@@ -86,7 +87,14 @@ namespace spot
degen_order_, degen_order_,
degen_cache_); degen_cache_);
delete a; delete a;
if (ba_simul_ <= 0)
return d; return d;
const tgba* s = do_simul(d, ba_simul_);
if (s != d)
delete d;
return s;
} }
const tgba* postprocessor::run(const tgba* a, const ltl::formula* f) const tgba* postprocessor::run(const tgba* a, const ltl::formula* f)
...@@ -96,6 +104,8 @@ namespace spot ...@@ -96,6 +104,8 @@ namespace spot
if (simul_ < 0) if (simul_ < 0)
simul_ = (level_ == Low) ? 1 : 3; simul_ = (level_ == Low) ? 1 : 3;
if (ba_simul_ < 0)
ba_simul_ = (level_ == High) ? 3 : 0;
if (scc_filter_ < 0) if (scc_filter_ < 0)
scc_filter_ = 1; scc_filter_ = 1;
...@@ -124,7 +134,7 @@ namespace spot ...@@ -124,7 +134,7 @@ namespace spot
if (pref_ == Any) if (pref_ == Any)
return a; return a;
const tgba* sim = do_simul(a); const tgba* sim = do_simul(a, simul_);
if (a == sim) if (a == sim)
// simulation was disabled. // simulation was disabled.
return a; return a;
...@@ -174,15 +184,19 @@ namespace spot ...@@ -174,15 +184,19 @@ namespace spot
// 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))
{ {
sim = do_simul(a); sim = do_simul(a, simul_);
if (sim != a)
delete 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); sim = do_degen(sim);
} }
else
if (sim != a) {
delete a; delete a;
}
if (wdba && sim) if (wdba && sim)
{ {
......
...@@ -90,7 +90,7 @@ namespace spot ...@@ -90,7 +90,7 @@ namespace spot
const tgba* run(const tgba* input_disown, const ltl::formula* f); const tgba* run(const tgba* input_disown, const ltl::formula* f);
protected: protected:
const tgba* do_simul(const tgba* input); const tgba* do_simul(const tgba* input, int opt);
const tgba* do_degen(const tgba* input); const tgba* do_degen(const tgba* input);
output_type type_; output_type type_;
...@@ -103,6 +103,7 @@ namespace spot ...@@ -103,6 +103,7 @@ namespace spot
int simul_; int simul_;
int simul_limit_; int simul_limit_;
int scc_filter_; int scc_filter_;
int ba_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