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

postproc: add some experimental don't care options

* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add a
"simul-limit" option, and add two new cases to "simul"
for the two don't care simulation
* src/bin/man/ltl2tgba.x: Mention the new options.
parent ca941685
...@@ -30,6 +30,15 @@ order for each SCC it processes. This is currently disabled by default. ...@@ -30,6 +30,15 @@ order for each SCC it processes. This is currently disabled by default.
\fBsimul\fR \fBsimul\fR
Set to 0 to disable simulation-based reductions. Set to 1 to use only 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 direct simulation. Set to 2 to use only reverse simulation. Set to 3
to iterate both direct and reverse simulations. The default is 3, to iterate both direct and reverse simulations. Set to 4 to apply
except when option \fB\-\-low\fR is specified, in which case the only "don't care" direct simulation. Set to 5 to iterate "don't care"
default is 1. direct simulation and reverse simulation. The default is 3, except
when option \fB\-\-low\fR is specified, in which case the default is
1.
.TP
\fBsimul-limit\fR
Can be set to a positive integer to cap the number of "don't care"
transitions considered by the "don't care"-simulation algorithm. A
negative value (the default) does not enforce any limit. Note that if
there are \fIN\fR "don't care" transitions, the algorithm may
potentially test 2^\fIN\fR configurations.
...@@ -54,18 +54,12 @@ namespace spot ...@@ -54,18 +54,12 @@ namespace spot
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); simul_ = opt->get("simul", -1);
simul_limit_ = opt->get("simul-limit", -1);
} }
} }
const tgba* postprocessor::do_simul(const tgba* a) 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_) switch (simul_)
{ {
case 0: case 0:
...@@ -77,6 +71,10 @@ namespace spot ...@@ -77,6 +71,10 @@ namespace spot
case 3: case 3:
default: default:
return iterated_simulations(a); return iterated_simulations(a);
case 4:
return dont_care_simulation(a, simul_limit_);
case 5:
return dont_care_iterated_simulations(a, simul_limit_);
} }
} }
...@@ -95,11 +93,12 @@ namespace spot ...@@ -95,11 +93,12 @@ namespace spot
if (type_ == TGBA && pref_ == Any && level_ == Low) if (type_ == TGBA && pref_ == Any && level_ == Low)
return a; return a;
if (simul_ < 0)
simul_ = (level_ == Low) ? 1 : 3;
// Remove useless SCCs. // Remove useless SCCs.
{ {
const tgba* s = scc_filter(a, false); const tgba* s = scc_filter(a, simul_ > 3);
delete a; delete a;
a = s; a = s;
} }
......
...@@ -101,6 +101,7 @@ namespace spot ...@@ -101,6 +101,7 @@ namespace spot
bool degen_order_; bool degen_order_;
bool degen_cache_; bool degen_cache_;
int simul_; int simul_;
int simul_limit_;
}; };
/// @} /// @}
} }
......
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