Never say "never": here is yet another bug fix release for Spot 1.2.
The most important fix is for a simplification rule for some unlikely
PSL pattern. Then we have some improved compatibilities with some
newer versions of the tools we use in the build, some fixes to the HOA
format (as output by ltl2tgba --hoaf) that the current development
version of Spot 2.0 is able to read, and some improved errors checks
for ltlcross.
You can download the new release here:
http://spot.lip6.fr/dl/spot-1.2.6.tar.gz
New in spot 1.2.6 (2014-12-06)
* New features:
- ltlcross --verbose is a new option to see what is being done
* Bug fixes:
- Remove one incorrect simplification rule for PSL discovered
via checks on random formulaes. (The bug was very unlikely
to trigger on non-random formulas, because it requires a SERE
with an entire subexpression that is unsatisfiable.)
- When the automaton resulting from the translation of a positive
formula is deterministic, ltlcross will compute its complement
to perform additional checks against other translations of the
positive formula. The same procedure should be performed with
automata obtained from negated formulas, but because of a typo
this was not the case.
- the neverclaim parser will now diagnose redefinitions of
state labels.
- the acceptance specification in the HOA format output have been
adjusted to match recent changes in the format specifications.
- atomic propositions are correctly escaped in the HOA output.
- the build rules for documentation have been made compatible with
version 8.0 of Org-mode. (This was only a problem if you build
from the git repository, or if you want to edit the
documentation.)
- recent to changes to libstd++ (as shipped by g++ 4.9.2) have
demonstrated that the order of transitions output by the
LTL->TGBA translation used to be dependent on the implementation
of the STL. This is now fixed.
- some developpement version of libstd++ had a bug (PR 63698) in
the assignment of std::set, and that was triggered in two places
in Spot. The workaround (not assigning sets) is actually more
efficient, so we can consider it as a bug fix, even though
libstd++ has also been fixed.
- all parsers would report wrong line numbers while processing
files with DOS style newlines.
- add support for SWIG 3.0.
--
Alexandre Duret-Lutz
