We are pleased to announce the release of Spot 0.9.2.

Spot is a model-checking library developed collaboratively by LRDE and LIP6. It provides algorithms and data structures to implement the automata-theoretic approach to LTL model checking.

This maintenance release includes minor bug fixes and speed improvements, and adds an interface to ltl3ba on the online translator.

You can find the new release here:

http://spot.lip6.fr/dl/spot-0.9.2.tar.gz

A more detailed list of new features follows.

New in spot 0.9.2 (2012-07-02):

* New features to the web interface. - It can run ltl3ba (Babiak et al., TACAS'12) where available. - "a loading logo" is displayed when result is not instantaneous. * Speed improvements: - The unicity hash table of BuDDy has been separated separated node table for better cache-friendliness. The resulting speedup is around 5% on BDD-intensive algorithms. - A new BDD operation, called bdd_implies() has been added to BuDDy to check wether one BDD implies another. This benefits mostly the simulation and degeneralization algorithms of Spot. - A new offline implementation of the degeneralization (which had always been performed on-the-fly so far) available. This especially helps the Safra complementation. * Bug fixes: - The CGI script running for ltl2tgba.html will correctly timeout after 30s when Spot's translation takes more time. - Applying WDBA-minimization on an automaton generated by the Couvreur/LaCIM translator could lead to an incorrect automaton due to a bug in the definition of product with symbolic automata. - The Makefile.am of BuDDy, LBTT, and Spot have been adjusted to accomodate Automake 1.12 (while still working with 1.11). - Better error recovery when parsing broken LTL formulae. - Fix errors and warnings reported by clang 3.1 and the upcoming g++ 4.8.