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

* NEWS: Update the news about minimization.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2010-12-13 19:28:48 +01:00
parent d72a2f0a31
commit aadef1fd87
2 changed files with 18 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2010-12-13 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* NEWS: Update the news about minimization.
2010-11-26 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-11-26 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Speed up wdba.test, it was too slow for our buildfarm. Speed up wdba.test, it was too slow for our buildfarm.

21
NEWS
View file

@ -6,34 +6,41 @@ New in spot 0.6a:
developement version of checkpn using it, and it should be developement version of checkpn using it, and it should be
released shortly after Spot 0.7. released shortly after Spot 0.7.
* The function to_spin_string(), used to output an LTL formula using * The function to_spin_string(), used to output an LTL formula using
Spin's syntax, now takes an optional argument to request full Spin's syntax, now takes an optional argument to request full
parenthesis. parenthesis.
* src/ltltest/genltl is a new tool that generates some interesting * src/ltltest/genltl is a new tool that generates some interesting
families of LTL formulae, for testing purpose. families of LTL formulae, for testing purpose.
* bench/ltlclasses/ uses the above tool to conduct the same benchmark * bench/ltlclasses/ uses the above tool to conduct the same benchmark
as in the DepCoS'09 paper by Cichón et al. The resulting benchmark as in the DepCoS'09 paper by Cichón et al. The resulting benchmark
completes in 12min, while it tooks days (or crashed) when the paper completes in 12min, while it tooks days (or crashed) when the paper
was written (using Spot 0.4). was written (using Spot 0.4).
* Degeneralization has again been improved in two ways: * Degeneralization has again been improved in two ways:
- It will merge the degeneralized transitions that can be merged. - It will merge the degeneralized transitions that can be merged.
- It uses a cache to speed up the improvement introduced in 0.6. - It uses a cache to speed up the improvement introduced in 0.6.
* An implementation of Dax et al.'s paper for minimizing obligation
formulae has been integrated. Use ltl2tgba -Rm to enable this
optimization; it will have no effect if the property is not an
obligation.
* New ltl2tgba options: * New ltl2tgba options:
-XN: read an input automaton as a neverclaim. -XN: read an input automaton as a neverclaim.
-C, -CR: Compute (and display) a counterexample after running the -C, -CR: Compute (and display) a counterexample after running the
emptiness check. With -CR, the counterexample will be emptiness check. With -CR, the counterexample will be
replayed on the automaton to ensure it is correct replayed on the automaton to ensure it is correct
(previous version would always compute a replay a (previous version would always compute a replay a
counterexample when emptiness-check was enabled) counterexample when emptiness-check was enabled)
-ks: traverse the automaton to compute its number of states and -ks: traverse the automaton to compute its number of states and
transitions (this is faster than -k whichi will also count transitions (this is faster than -k whichi will also count
SCCs and paths). SCCs and paths).
-Rn: Minimize automata for obligation formulae.
-M: Build a deterministic monitor.
-O: Tell whether an automaton is a safety automaton.
* Bug fixes: * Bug fixes:
- Location of the errors messages in the TGBA parser where inaccurate. - Location of the errors messages in the TGBA parser where inaccurate.
- Various warning fixes for different versions of GCC and Clang. - Various warning fixes for different versions of GCC and Clang.
- The neverclaim output with ltl2tgba -N or -NN used to ignore any - The neverclaim output with ltl2tgba -N or -NN used to ignore any
automaton simplification performed after degeneralization. automaton simplification performed after degeneralization.
- The formula simplification based on universality and eventuallity - The formula simplification based on universality and eventuallity
had a quadratic run-time. had a quadratic run-time.
New in spot 0.6 (16-04-2010): New in spot 0.6 (16-04-2010):