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>, 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.
We are happy to announce the release of Spot 2.13.2
This is a maintenance release that fixes a few issues.
You can find the new release here:
http://www.lre.epita.fr/dload/spot/spot-2.13.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.13.2 (2025-06-12)
Bugs fixed:
- compiling from git with a missing Bison would display
a confusing error (Issue #607)
- the Python bindings for iterators generated by Swig are not
working with libc++ when multiple modules are used. (Everything
works with libstdc++.) This caused issues in Mac OS and OpenBSD.
This version implements a workaround until Swig is fixed.
(Issue #603)
- Fix spurious failure of ltlsynt.test on OpenBSD.
- difference_word_forq() could return different words on different
architectures because the code was iterating on hash_map that
can be implemented in different ways.
- remove_univ_otf() had a memory-handling bug, that could cause
use-after-free errors.
