We are happy to announce the release of Spot 2.14 This is a major release that includes two new tools related to LTLf and developed over the past 8 months. You can find the new release here: http://www.lre.epita.fr/dload/spot/spot-2.14.tar.gz See https://spot.lre.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>fr>, or create issues on https://gitlab.lre.epita.fr/spot/spot/-/issues/new New in spot 2.14 (2025-06-26) Build: - When Python bindings are enabled, Spot now requires Python 3.8 or later. Python 3.8 is already quite old: it reached end-of-life in 2024. Python 3.8 was used for instance in Ubuntu 20.04, where you can install this version of Spot. Command-line tools: - ltlf2dfa is a new tool that converts LTLf to MTDFA, i.e., DFA represented with multi-terminal BDDs. See https://spot.lre.epita.fr/ltlf2dfs.html for some examples. - ltlfsynt is a new tool that solves the reactive synthesis for LTLf specification, using a reachability game interpreted oveer MTDFA. See https://spot.lre.epita.fr/ltlfsynt.html The output of --realizability has been compared to several other tools on benchmarks from the synthesis competition (which all use Moore semantics) in addition to some custom specifications (with Moore and Mealy semantics) in our test suite. The production of a Mealy machine representing the controller has been implemented, but it hasn't received a lot of testing so far, it should be regarded as very experimental. For more information about ltlf2dfa and ltlfsynt, refer to the paper "Engineering an LTLf Synthesis Tool" to be presented at CIAA'25. - genltl learned four new options: --tv-counter-mealy=N, --tv-double-counters-mealy=N, --tv-nim-mealy=N,M, --chomp-mealy=N,M. These are scalable LTLf specifications that can be used directly with ltlfsynt. The first three options are taken from the literature; Chomp is an original familly that has been submitted as a new model to SyntComp'25. - ltlf2tgba learned an --ltlf option. This currently implements the very slow approach of going from LTLf->LTL->DBA->DFA. ltlf2dfa is way faster. - Tools that take a "--tlsf FILENAME" option (ltlsynt, ltlfsynt, and ltlf2dfa currently) will now accept arguments of the form FILENAME/VAR1=VAL1,VAR2=VAL2... to override parameters defined in the TLSF file. E.g.: ltlsynt --tlsf arbiter.tlsf/n=3 Library: - spot::mtdfa is a new class implementing a DFA using Multi-Terminal BDDs. The data structure is similar to what can be found in Mona. This comes with convenient rendering routines for use in Jupyter notebook. - spot::ltlf_to_mtdfa() and spot::ltlf_to_mtdfa_compose() are new functions that converts a LTLf formula into an MTDFA, using either a direct translation, or a compositional one. - spot::minimize_mtdfa() is a minimization function for MTDFA. See https://spot.lre.epita.fr/ipynb/ltlf2dfa.html for some illustrations. - spot::product_or(), spot::product_and(), spot::product_xor(), etc. have been overloaded to implement those operations on MTDFAs as well. - spot::backprop_graph is a new class implementing what's needed to run a linear backpropagation for solving reachability games. This allows solving the game on-the-fly, as it is constructed. See https://spot.lre.epita.fr/ipynb/backprop.html for examples. - spot::ltlf_to_mtdfa_for_synthesis() is a new function that performs LTLf synthesis. - spot::translator learned output_type::Finite to request translation to Finite automata.