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

ltlsynt: make sure the previous Xor optimization actually works

Browse source 
* spot/tl/simplify.hh, spot/tl/simplify.cc,
spot/twaalgos/translate.cc: Update the tl_simplification
options after all preferences have been given.
* bin/ltlsynt.cc: Display the size of the translation output.
* tests/core/ltlsynt.test: Add test case.
This commit is contained in:
Alexandre Duret-Lutz 2020-05-16 19:22:28 +02:00
parent 6ec6150462
commit fc1c17b91c
5 changed files with 48 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

16
spot/twaalgos/translate.cc
View file

@ -106,10 +106,6 @@ namespace spot
throw std::runtime_error
("tls-impl should take a value between 0 and 3");
}
if (comp_susp_ > 0 || (ltl_split_ && type_ == Generic))
options.favor_event_univ = true;
if (type_ == Generic && ltl_split_ && (pref_ & Deterministic))
options.keep_top_xor = true;
simpl_owned_ = simpl_ = new tl_simplifier(options, dict);
}
@ -419,6 +415,18 @@ namespace spot
twa_graph_ptr translator::run(formula* f)
{
if (simpl_owned_)
{
// Modify the options according to set_pref() and set_type().
// We do it for all translation, but really only the first one
// matters.
auto& opt = simpl_owned_->options();
if (comp_susp_ > 0 || (ltl_split_ && type_ == Generic))
opt.favor_event_univ = true;
if (type_ == Generic && ltl_split_ && (pref_ & Deterministic))
opt.keep_top_xor = true;
}
// Do we want to relabel Boolean subformulas?
// If we have a huge formula such as
// (a1 & a2 & ... & an) U (b1 | b2 | ... | bm)