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

translate: reset the LTL simplifier on set_level().

Browse source 
Fix an issue reported by Tomáš Babiak, who noticed that he could not
manage to have ltl2tgba process `genltl --go-theta=N` efficiently for
larger values of N.

* spot/twaalgos/translate.hh (set_level): Reset any owned LTL simplifier
whenever the optimization level is changed.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2016-10-25 13:53:28 +02:00
parent 4be7065b81
commit ce63c30c0b
2 changed files with 13 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
NEWS
View file

@ -18,6 +18,13 @@ New in spot 2.1.2.dev (not yet released)
this halves the run time of this halves the run time of
genltl --rv-counter=10 | ltl2tgba genltl --rv-counter=10 | ltl2tgba
Bugs:
* ltl2tgba was alway using the highest settings for the LTL
simplifier, ignoring the --low and --medium options. Now
genltl --go-theta=12 | ltl2tgba --low --any
is instantaneous as it should be.
New in spot 2.1.2 (2016-10-14) New in spot 2.1.2 (2016-10-14)
Command-line tools: Command-line tools:

6
spot/twaalgos/translate.hh
View file

@ -96,6 +96,12 @@ namespace spot
set_level(optimization_level level) set_level(optimization_level level)
{ {
level_ = level; level_ = level;
if (simpl_owned_)
{
auto d = simpl_owned_->get_dict();
delete simpl_owned_;
build_simplifier(d);
}
} }
/// \brief Convert \a f into an automaton. /// \brief Convert \a f into an automaton.