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".