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@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.