We are pleased to announce the release of Spot 0.7. Spot is a model-checking library developed collaboratively by LRDE and LIP6. It provides algorithms and data structures to implement the automata-theoretic approach for LTL model checking. Highlights in this release include some speed improvements, and a minimization of WDBA (weak deterministic Büchi automata). The online translator has also been rewritten. You can find the new release here: http://spot.lip6.fr/dl/spot-0.7.tar.gz New in spot 0.7 (2011-02-01): * Spot is now able to read an automaton expressed as a Spin neverclaim. * The "experimental" Kripke structure introduced in Spot 0.5 has been rewritten, and is no longer experimental. We have a developement version of checkpn using it, and it should be released shortly after Spot 0.7. * The function to_spin_string(), that outputs an LTL formula using Spin's syntax, now takes an optional argument to request parentheses at all levels. * src/ltltest/genltl is a new tool that generates some interesting families of LTL formulae, for testing purpose. * bench/ltlclasses/ uses the above tool to conduct the same benchmark as in the DepCoS'09 paper by Cichoń et al. The resulting benchmark completes in 12min, while it tooks days (or exhausted the memory) when the paper was written (they used Spot 0.4). * Degeneralization has again been improved in two ways: - It will merge degeneralized transitions that can be merged. - It uses a cache to speed up the improvement introduced in 0.6. * An implementation of Dax et al.'s paper for minimizing obligation formulae has been integrated. Use ltl2tgba -Rm to enable this optimization from the command-line; it will have no effect if the property is not an obligation. * bench/wdba/ conducts a benchmark similar to the one on Dax's webpage, comparing the size of the automata expressing obligation formula before and after minimization. See bench/wdba/README for results. * Using similar code, Spot can now construct deterministic monitors. * New ltl2tgba options: -XN: read an input automaton as a neverclaim. -C, -CR: Compute (and display) a counterexample after running the emptiness check. With -CR, the counterexample will be replayed on the automaton to ensure it is correct (previous version would always compute a replay a counterexample when emptiness-check was enabled) -ks: traverse the automaton to compute its number of states and transitions (this is faster than -k which will also count SCCs and paths). -M: Build a deterministic monitor. -O: Tell whether a formula represents a safety, guarantee, or obligation property. -Rm: Minimize automata representing obligation properties. * The on-line tool to translate LTL formulae into automata has been rewritten and is now at http://spot.lip6.fr/ltl2tgba.html It requires a javascript-enabled browser. * Bug fixes: - Location of the errors messages in the TGBA parser where inaccurate. - Various warning fixes for different versions of GCC and Clang. - The neverclaim output with ltl2tgba -N or -NN used to ignore any automaton simplification performed after degeneralization. - The formula simplification based on universality and eventuality had a quadratic run-time. -- Alexandre Duret-Lutz