translate: use compositional suspension on request
This has to be turned on using "-x comp-susp" and other related options documented in spot-x (7). * src/tgbaalgos/translate.hh, src/tgbaalgos/translate.cc: Add support for calling composition-suspension, with optional simulation, WDBA-minimization, and composition. * src/bin/spot-x.cc: Document the new options. * src/bin/man/spot-x.x: Add some bibliography. * src/tgbatest/ltlcross2.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz
parent
88cd376dff
commit
b6d4806dca
5 changed files with 93 additions and 14 deletions
|
|
@ -6,6 +6,23 @@ spot-x \- Common fine-tuning options.
|
|||
.B \-x STRING
|
||||
[DESCRIPTION]
|
||||
.\" Add any additional description here
|
||||
[BIBLIOGRAPHY]
|
||||
.TP
|
||||
1.
|
||||
Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the
|
||||
Powerset Construction for Restricted Classes of
|
||||
ω-Automata. Proceedings of ATVA'07. LNCS 4762.
|
||||
|
||||
Describes the WDBA-minimization algorithm implemented in Spot.
|
||||
.TP
|
||||
2.
|
||||
Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský,
|
||||
Jan Strejček: Compositional Approach to Suspension and Other
|
||||
Improvements to LTL Translation. Proceedings of SPIN'13. LNCS XXXX.
|
||||
|
||||
Describes the compositional suspension, the simulation-based
|
||||
reductions, and the SCC-based simplifications.
|
||||
|
||||
[SEE ALSO]
|
||||
.BR ltl2tgba (1)
|
||||
.BR ltl2tgta (1)
|
||||
|
|
|
|||
|
|
@ -37,6 +37,24 @@ value) is a shorthand for KEY=1, while !KEY is a shorthand for KEY=0.";
|
|||
|
||||
static const argp_option options[] =
|
||||
{
|
||||
{ 0, 0, 0, 0, "Translation options:", 0 },
|
||||
{ DOC("comp-susp", "Set to 1 to enable compositional suspension, \
|
||||
as described in our SPIN'13 paper (see Bibliography below). Set to 2, \
|
||||
to build only the skeleton TGBA without composing it. Set to 0 (the \
|
||||
default) to disable.") },
|
||||
{ DOC("early-susp", "When set to 1, start compositional suspension on \
|
||||
the transitions that enter accepting SCCs, and not only on the transitions \
|
||||
inside accepting SCCs. This option defaults to 0, and is only used when \
|
||||
comp-susp=1.") },
|
||||
{ DOC("skel-simul", "Default to 1. Set to 0 to disable simulation \
|
||||
on the skeleton automaton during compositional suspension. Only used when \
|
||||
comp-susp=1.") },
|
||||
{ DOC("skel-wdba", "Set to 0 to disable WDBA \
|
||||
minimization on the skeleton automaton during compositional suspension. \
|
||||
Set to 1 always WDBA-minimize the skeleton . Set to 2 to keep the WDBA \
|
||||
only if it is smaller than the original skeleton. This option is only \
|
||||
used when comp-susp=1 and default to 1 or 2 depending on whether --small \
|
||||
or --deterministic is specified.") },
|
||||
{ 0, 0, 0, 0, "Postprocessing options:", 0 },
|
||||
{ DOC("scc-filter", "Set to 1 (the default) to enable \
|
||||
SCC-pruning and acceptance simplification at the beginning of \
|
||||
|
|
|
|||
|
|
@ -19,10 +19,28 @@
|
|||
|
||||
#include "translate.hh"
|
||||
#include "ltl2tgba_fm.hh"
|
||||
#include "compsusp.hh"
|
||||
#include "misc/optionmap.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
void translator::setup_opt(const option_map* opt)
|
||||
{
|
||||
comp_susp_ = early_susp_ = skel_wdba_ = skel_simul_ = 0;
|
||||
|
||||
if (!opt)
|
||||
return;
|
||||
|
||||
comp_susp_ = opt->get("comp-susp", 0);
|
||||
if (comp_susp_ == 1)
|
||||
{
|
||||
early_susp_ = opt->get("early-susp", 0);
|
||||
skel_wdba_ = opt->get("skel-wdba", -1);
|
||||
skel_simul_ = opt->get("skel-simul", 1);
|
||||
}
|
||||
}
|
||||
|
||||
void translator::build_simplifier(bdd_dict* dict)
|
||||
{
|
||||
ltl::ltl_simplifier_options options(false, false, false);
|
||||
|
|
@ -53,8 +71,22 @@ namespace spot
|
|||
// natural way (improving the degeneralization).
|
||||
simpl_->clear_as_bdd_cache();
|
||||
|
||||
bool exprop = level_ == spot::postprocessor::High;
|
||||
const tgba* aut = ltl_to_tgba_fm(r, simpl_->get_dict(), exprop);
|
||||
const tgba* aut;
|
||||
if (comp_susp_ > 0)
|
||||
{
|
||||
int skel_wdba = skel_wdba_;
|
||||
if (skel_wdba < 0)
|
||||
skel_wdba = (pref_ == spot::postprocessor::Deterministic) ? 1 : 2;
|
||||
|
||||
aut = compsusp(r, simpl_->get_dict(), skel_wdba == 0,
|
||||
skel_simul_ == 0, early_susp_ != 0,
|
||||
comp_susp_ == 2, skel_wdba == 2, false);
|
||||
}
|
||||
else
|
||||
{
|
||||
bool exprop = level_ == spot::postprocessor::High;
|
||||
aut = ltl_to_tgba_fm(r, simpl_->get_dict(), exprop);
|
||||
}
|
||||
aut = this->postprocessor::run(aut, r);
|
||||
return aut;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -52,18 +52,21 @@ namespace spot
|
|||
: postprocessor(opt), simpl_(simpl), simpl_owned_(0)
|
||||
{
|
||||
assert(simpl);
|
||||
setup_opt(opt);
|
||||
}
|
||||
|
||||
translator(bdd_dict* dict, const option_map* opt = 0)
|
||||
: postprocessor(opt)
|
||||
{
|
||||
build_simplifier(dict);
|
||||
setup_opt(opt);
|
||||
}
|
||||
|
||||
translator(const option_map* opt = 0)
|
||||
: postprocessor(opt)
|
||||
{
|
||||
build_simplifier(0);
|
||||
setup_opt(opt);
|
||||
}
|
||||
|
||||
~translator()
|
||||
|
|
@ -72,8 +75,6 @@ namespace spot
|
|||
delete simpl_owned_;
|
||||
}
|
||||
|
||||
void build_simplifier(bdd_dict* dict);
|
||||
|
||||
typedef postprocessor::output_type output_type;
|
||||
|
||||
void
|
||||
|
|
@ -111,10 +112,17 @@ namespace spot
|
|||
/// the caller.
|
||||
const tgba* run(const ltl::formula** f);
|
||||
|
||||
protected:
|
||||
void setup_opt(const option_map* opt);
|
||||
void build_simplifier(bdd_dict* dict);
|
||||
|
||||
private:
|
||||
ltl::ltl_simplifier* simpl_;
|
||||
ltl::ltl_simplifier* simpl_owned_;
|
||||
int comp_susp_;
|
||||
int early_susp_;
|
||||
int skel_wdba_;
|
||||
int skel_simul_;
|
||||
};
|
||||
/// @}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -24,13 +24,17 @@ ltl2tgba=../../bin/ltl2tgba
|
|||
|
||||
../../bin/randltl -P -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 |
|
||||
../../bin/ltlcross \
|
||||
"$ltl2tgba --lbtt --any --low %f > %T" \
|
||||
"$ltl2tgba --lbtt --any --medium %f > %T" \
|
||||
"$ltl2tgba --lbtt --any --high %f > %T" \
|
||||
"$ltl2tgba --lbtt --deterministic --low %f > %T" \
|
||||
"$ltl2tgba --lbtt --deterministic --medium %f > %T" \
|
||||
"$ltl2tgba --lbtt --deterministic --high %f > %T" \
|
||||
"$ltl2tgba --lbtt --small --low %f > %T" \
|
||||
"$ltl2tgba --lbtt --small --medium %f > %T" \
|
||||
"$ltl2tgba --lbtt --small --high %f > %T" \
|
||||
--json=output.json --csv=output.csv
|
||||
"$ltl2tgba --lbtt --any --low %f > %T" \
|
||||
"$ltl2tgba --lbtt --any --medium %f > %T" \
|
||||
"$ltl2tgba --lbtt --any --high %f > %T" \
|
||||
"$ltl2tgba --lbtt --deterministic --low %f > %T" \
|
||||
"$ltl2tgba --lbtt --deterministic --medium %f > %T" \
|
||||
"$ltl2tgba --lbtt --deterministic --high %f > %T" \
|
||||
"$ltl2tgba --lbtt --small --low %f > %T" \
|
||||
"$ltl2tgba --lbtt --small --medium %f > %T" \
|
||||
"$ltl2tgba --lbtt --small --high %f > %T" \
|
||||
"$ltl2tgba --lbtt -x comp-susp --small %f >%T" \
|
||||
"$ltl2tgba --lbtt -x comp-susp,!skel-wdba --lbtt --small %f >%T" \
|
||||
"$ltl2tgba --lbtt -x comp-susp,early-susp --lbtt --small %f >%T" \
|
||||
"$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --lbtt --small %f >%T" \
|
||||
--json=output.json --csv=output.csv
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue