Spot 2.14 released - Spot-announce

26 Jun 2025


      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@lrde.epita.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.