e are pleased to announce the release of Spot 1.0.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 second maintainance release fixes couple of bugs, the most serious being in web interface, and adds two minor new features. You can find the new release here: http://spot.lip6.fr/dl/spot-1.0.2.tar.gz A summary of the changes follows. Please report any issue to <spot(a)lrde.epita.fr>fr>. New in spot 1.0.2 (2013-03-06): * New features: - the on-line ltl2tgba.html interface can output deterministic or non-deterministic monitors. However, and unlike the ltl2tgba command-line tool, it doesn't different output formats. - the class ltl::ltl_simplifier now has an option to rewrite Boolean subformulaes as irredundante-sum-of-product during the simplification of any LTL/PSL formula. The service is also available as a method ltl_simplifier::boolean_to_isop() that applies this rewriting to a Boolean formula and implements a cache. ltlfilt as a new option --boolean-to-isop to try to apply the above rewriting from the command-line: % ltlfilt --boolean-to-isop -f 'GF((a->b)&(b->c))' GF((!a & !b) | (b & c)) This is currently not used anywhere else in the library. * Bug fixes: - 'ltl2tgba --high' is documented to be the same as 'ltl2tgba', but by default ltl2tgba forgot to enable LTL simplifications based on language containment, which --high do enable. There are now enabled by default. - the on-line ltl2tgba.html interface failed to output monitors, testing automata, and generalized testing automata due to two issues with the Python bindings. It also used to display Testing Automaton Options when the desired output was set to Monitor. - bench/ltl2tgba would not work in a VPATH build. - a typo caused some .dir-locals.el configuration parameters to be silently ignored by emacs - improved Doxygen comments for formula_to_bdd, bdd_to_formula, and bdd_dict. - src/tgbatest/ltl2tgba (not to be confused with src/bin/ltl2tgba) would have a memory leak when passed the conflicting option -M and -O. It probably has many other problems. Do not use src/tgbatest/ltl2tgba if you are not writing a test case for Spot. Use src/bin/ltl2tgba instead. -- Alexandre Duret-Lutz