We are happy to announce the release of Spot 2.7.1 This release contains mostly bug fixes and some minor additions to the Python bindings. See below for a detailed list of user-visible changes. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.7.1.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.7.1 (2019-02-14) Build - Work around GCC bug #89303 that causes memory leaks and std::weak_bad_ptr exceptions when Spot is compiled with the version of g++ 8.2 currently distributed by Debian unstable (starting with g++ 8.2.0-15). Python: - The following methods of spot::bdd_dict are now usable in Python when fine control over the lifetime of associations between BDD variables and atomic propositions is needed. - register_proposition(formula, for_me) - register_anonymous_variables(count, for_me) - register_all_propositions_of(other, for_me) - unregister_all_my_variables(for_me) - unregister_variable(var, for_me) - Better support for explicit Kripke structures: - the kripke_graph type now has Python bindings - spot.automaton() and spot.automata() now support a want_kripke=True to return a kripke_graph See the bottom of https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html for some examples. Library: - Printing Kripke structures via print_hoa() will save state names. - kripke_graph_ptr objects now honnor any "state-names" property when formating states. Bugs fixed: - The print_dot_psl() function would incorrectly number all but the first children of commutative n-ary operators: in this case no numbering was expected. - std::out_of_range C++ exceptions raised from Python code are now converted into IndexError Python exceptions (instead of aborting the program). - The LTL parser would choke on carriage returns when command-line tools such as ltlfilt, ltlcross, or ltl2tgba were run on files of formulas with MS-DOS line endings. - The core translation for unambiguous automata was incorrectly tagging some non-weak automata as weak. - The product_susp() function used to multiply an automaton with a suspendable automaton could incorrectly build transition-based automata when multipliying two state-based automata. This caused ltl2tgba to emit error messages such as: "automaton has transition-based acceptance despite prop_state_acc()==true". -- Alexandre Duret-Lutz