We are pleased to announce the release of Spot 0.8.

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.

Although this version contains a few new features, this should really be regarded as a maintenance release to fix a series of bugs that have been reported over the last few months.

You can find the new release here:

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

New in spot 0.8 (2011-11-28):

* Major new features: - Spot can read DiVinE models. See iface/dve2/README for details. - The genltl tool can now output 20 different LTL formula families. It also replaces the LTLcounter Perl scripts. - There is a printer and parser for Kripke structures in text format. * Major interface changes: - The destructor of all states is now private. Any code that looks like "delete some_state;" will cause an compile error and should be updated to "some_state->destroy();". This new syntax is supported since version 0.7. - The experimental Nips interface has been removed. * Minor changes: - The dotty_reachable() function has a new option "assume_sba" that can be used for rendering automata with state-based acceptance. In that case, acceptance states are displayed with a double circle. ltl2tgba (both command line and on-line) Use it to display degeneralized automata. - The dotty_reachable() function will also display transition annotations (as returned by the tgba::transitition_annotation()). This can be useful when displaying (small) state spaces. - Identifiers used to name atomic proposition can contain dots. E.g.: X.Y is now an atomic proposition, while it was understood as X&Y in previous versions. - The Doxygen documentation is no longer built as a PDF file. * Internal improvements: - The on-line ltl2tgba CGI script uses a cache to produce faster answers. - Better memory management for the states of explicit automata. Thanks to the aforementioned ->destroy() change, we can avoid cloning explicit states. - tgba_product has learned how to be faster when one of the operands is a Kripke structure (15% speedup). - The reduction rule for "a M b" has been improved: it can be reduced to "a & b" if "a" is a pure eventuallity. - More useless acceptance conditions are removed by SCC simplifications. * Bug fixes: - Safra complementation has been fixed in cases where more than one acceptance conditions where needed to convert the deterministic Streett automaton as a TGBA. - The degeneralization is now idempotent. Previously, degeneralizing an already degeneralized automaton could add some states. - The degeneralization now has a deterministic behavior. Previously it was possible to obtain different output depending on the memory layout. - Spot now outputs neverclaims with fully parenthesized guards. I.e., instead of (!x && y) -> goto S1 it now outputs ((!(x)) && (y)) -> goto S1 This prevents problems when the model defines `x' as #define x flag==0 because !x then evaluated to (!flag)==0 instead of !(flag==0).