
We are happy to announce the release of Spot 2.14.2 This is a minor realease that addresses a few bugs and improve the documentation. You can find the new release here: http://www.lre.epita.fr/dload/spot/spot-2.14.2.tar.gz See https://spot.lre.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot@lrde.epita.fr>, or create issues on https://gitlab.lre.epita.fr/spot/spot/-/issues/new New in spot 2.14.2 (2025-09-18) Library: - BuDDy's implementation of bdd_mt_apply1_synthesis() and bdd_mt_apply1_synthesis_with_choice() used by ltlfsynt, got some small improvements resulting in smaller strategies being generated. (Issue #611.) Documentation: - https://www.lre.epita.fr/tlsf.html is a new page discussing how the --tlsf option of ltlsynt/ltlfsynt/ltlf2dfa uses syfco to transform TLSF into LTL/LTLf. - https://www.lre.epita.fr/tut60.html shows two examples of integration with ppLTLTT to handle some pure-past LTL sub-formulas. Bug fixes: - twadfa_to_mtdfa(aut) was not properly registering the atomic proposition of aut into the resulting MTDFA. - The part of the HOA parser responsible for dealing with multiple initial states (a feature of the HOA format that Spot does not support internally) had a bug if the last state of the set of initial state without incoming edges also had no outgoing edges. - spot::mtdfa_strategy_to_mealy() now has an option to produce a strategy that stutter on accepance. This gets rid of the accepting sink, and this is also necessary for the correctness of the produced controller in some decomposition cases. (Issue #610)
participants (1)
-
Alexandre Duret-Lutz