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