alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

postproc: add an scc-filter option

Browse source 
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add an
scc-filter option.
* src/bin/man/ltl2tgba.x: Document it.
This commit is contained in:
Alexandre Duret-Lutz 2013-02-14 14:35:14 +01:00
parent bc7a2865de
commit a965af711c
3 changed files with 16 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/bin/man/ltl2tgba.x
View file

@ -14,6 +14,14 @@ shorthand for \fIKEY\fR=1, and !\fIKEY\fR is a shorthand for
Supported options are: Supported options are:
.TP .TP
\fBscc\-filter\fR
Set to 1 (the default) to enable SCC-pruning and acceptance
simplification at the beginning of post-processing. Transitions that
are outside of accepting SCC are removed from accepting sets, except
those that enter into an accepting SCC. Set to 2 to remove even these
entering transition from the accepting sets. Set to 0 to disable this
SCC-pruning and acceptance simpification pass.
.TP
\fBdegen\-reset\fR \fBdegen\-reset\fR
If non-zero (the default), the degeneralization algorithm will reset If non-zero (the default), the degeneralization algorithm will reset
its level any time it exits a non-accepting SCC. its level any time it exits a non-accepting SCC.

10
src/tgbaalgos/postproc.cc
View file

@ -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) simul_(-1), scc_filter_(-1)
{ {
if (opt) if (opt)
{ {
@ -55,6 +55,7 @@ namespace spot
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); simul_limit_ = opt->get("simul-limit", -1);
scc_filter_ = opt->get("scc-filter", -1);
} }
} }
@ -95,10 +96,13 @@ namespace spot
if (simul_ < 0) if (simul_ < 0)
simul_ = (level_ == Low) ? 1 : 3; simul_ = (level_ == Low) ? 1 : 3;
if (scc_filter_ < 0)
scc_filter_ = 1;
// Remove useless SCCs. // Remove useless SCCs.
if (scc_filter_ > 0 || type_ == Monitor)
{ {
const tgba* s = scc_filter(a, simul_ > 3); const tgba* s = scc_filter(a, scc_filter_ > 1);
delete a; delete a;
a = s; a = s;
} }
@ -194,7 +198,7 @@ namespace spot
} }
} }
if (sim && type_ == TGBA && level_ == High) if (sim && type_ == TGBA && level_ == High && scc_filter_ != 0)
{ {
const tgba* s = scc_filter(sim, true); const tgba* s = scc_filter(sim, true);
delete sim; delete sim;

1
src/tgbaalgos/postproc.hh
View file

@ -102,6 +102,7 @@ namespace spot
bool degen_cache_; bool degen_cache_;
int simul_; int simul_;
int simul_limit_; int simul_limit_;
int scc_filter_;
}; };
/// @} /// @}
} }