Commit 2ac37ad5 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* NEWS: Summarize recent changes.

parent 01843379
2010-12-12 Alexandre Duret-Lutz <>
* NEWS: Summarize recent changes.
2010-12-11 Alexandre Duret-Lutz <>
Merge transitions in tgba_tba_proxy.
New in spot 0.6a:
Nothing yet.
* Spot is now able to read an automaton expressed as a Spin neverclaim.
* The "experimental" Kripke structure introduced in Spot 0.5 has
been rewritten, and is no longer experimental. We have a
developement version of checkpn using it, and it should be
released shortly after Spot 0.7.
* The function to_spin_string(), used to output an LTL formula using
Spin's syntax, now takes an optional argument to request full
* src/ltltest/genltl is a new tool that generates some interesting
families of LTL formulae, for testing purpose.
* 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
completes in 12min, while it tooks days (or crashed) when the paper
was written (using Spot 0.4).
* Degeneralization has again been improved in two ways:
- It will merge the degeneralized transitions that can be merged.
- It uses a cache to speed up the improvement introduced in 0.6.
* New ltl2tgba options:
-XN: read an input automaton as a neverclaim.
-C, -CR: Compute (and display) a counterexample after running the
emptiness check. With -CR, the counterexample will be
replayed on the automaton to ensure it is correct
(previous version would always compute a replay a
counterexample when emptiness-check was enabled)
-ks: traverse the automaton to compute its number of states and
transitions (this is faster than -k whichi will also count
SCCs and paths).
* Bug fixes:
- Location of the errors messages in the TGBA parser where inaccurate.
- Various warning fixes for different versions of GCC and Clang.
- The neverclaim output with ltl2tgba -N or -NN used to ignore any
automaton simplification performed after degeneralization.
- The formula simplification based on universality and eventuallity
had a quadratic run-time.
New in spot 0.6 (16-04-2010):
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment