We are happy to announce the release of Spot 2.1.2.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.1.2.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
Spot 2.1.2 contains a handful of bug fixes and a couple of minor
improvements, as listed below. These changes were contributed by
Étienne Renault, Alexandre Gbaguidi Aïsse, and myself.
As always, please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.1.2 (2014-10-14)
Command-line tools:
* genltl learned 5 new families of formulas
(--tv-f1, --tv-f2, --tv-g1, --tv-g2, --tv-uu)
defined in Tabakov & Vardi's RV'10 paper.
* ltlcross's --csv and --json output was changed to not include
information about the ambiguity or strength of the automata by
default. Computing those can be costly and not needed by
every user, so it should now be requested explicitely using
options --strength and --ambiguous.
Library:
* New LTL simplification rule:
- GF(f & q) = G(F(f) & q) if q is
purely universal and a pure eventuality. In particular
GF(f & GF(g)) now ultimately simplifies to G(F(f) & F(g)).
Bug fixes:
* Fix spurious uninitialized read reported by valgrind when
is_Kleene_star() is compiled by clang++.
* Using "ltlfilt some-large-file --some-costly-filter" could take
to a lot of time before displaying the first results, because the
output of ltlfilt is buffered: the buffer had to fill up before
being flushed. The issue did not manifest when the input is
standard input, because of the C++ feature that reading std::cin
should flush std::cout; however it was well visible when reading
from files. Flushing is now done more regularly.
* Fix compilation warnings when -Wimplicit-fallthrough it enabled.
* Fix python errors on Darwin when using methods from the spot module
inside of the spot.ltsmin submodule.
* Fix ltlcross crash when combining --no-check with --verbose.
* Adjust paths and options used in bench/dtgbasat/ to match the
changes introduced in Spot 2.0.
--
Alexandre Duret-Lutz
