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(a)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
