We are happy to announce the release of Spot 2.3.2. This is a maintenance release that only contains minor bug fixes, and minor enhancements, as listed below. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.3.2.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot@lrde.epita.fr>. New in spot 2.3.2 (2017-03-15) Tools: - In tools that output automata, the number of atomic propositions can be output using --stats=%x (output automaton) or --stats=%X (input automaton). Additional options can be passed to list atomic propositions instead of counting them. Tools that output formulas also support --format=%x for this purpose. Python: - The bdd_to_formula(), and to_generalized_buchi() functions can now be called in Python. Documentation: - https://spot.lrde.epita.fr/tut11.html is a new page describing how to build monitors in Shell, Python, or C++. Bugs fixed: - The tests using LTSmin's patched version of divine would fail if the current (non-patched) version of divine was installed. - Because of a typo, the output of --stats='...%P...' was correct only if %p was used as well. - genltl was never meant to have (randomly attributed) short options for --postive and --negative. - a typo in the code for transformating transition-based acceptance to state-based acceptance could cause a superfluous initial state to be output in some cases (the result was still correct). - 'ltl2tgba --any -C -M ...' would not complete automata. - While not incorrect, the HOA properties output by 'ltl2tgba -M' could be 'inherently-weak' or 'terminal', while 'ltl2tgba -M -D' would always report 'weak' automata. Both variants now report the most precise between 'weak' or 'terminal'. - spot::twa_graph::set_univ_init_state() could not be called with an initializer list. - The Python wrappers for spot::twa_graph::state_from_number and spot::twa_graph::state_acc_sets were broken in 2.3. - Instantiating an emptiness check on an automaton with unsupported acceptance condition should throw an exception. This used to be just an assertion, disabled in release builds; the difference matters for the Python bindings. Deprecation notice: - Using --format=%a to print the number of atomic propositions in ltlfilt, genltl, and randltl still works, but it is not documented anymore and should be replaced by the newly-introduced --format=%x for consistency with tools producing automata, where %a means something else. -- Alexandre Duret-Lutz