We are happy to announce the release of Spot 2.14.5
This is a maintenance realease that fixes a few bugs discovered in the
path month.
You can find the new release here:
http://www.lre.epita.fr/dload/spot/spot-2.14.5.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.5 (2025-12-11)
Bug fixes:
- The code of acc_code::inf_satisfiable was changed to properly match
its documentation. This function was not used and not tested so far,
but it has become needed for the next bug fix.
- The restrict_dead_end_edges_here() function introduced in Spot 2.13
could produce non-equivalent automata when the acceptance condition
involved Fin(x) terms. (Issue #628).
- BuDDy's bdd_free_path(), used in some iterations using paths_of(...) and
variants, was behaving incorrectly when the iteration was aborted.
- Because of an optimization introduced in Spot 2.11 to improve the
parsing of large disjunctions or conjunctions, the LTL parser
could instantiate Boolean subformulas in different order depending
on the architecture's calling convention. This could cause
different ordering of operands when printing formulas, causing
spurious failures in the test suite (e.g. if a test case expects
"α & β" as a result, but gets "β & α" instead).
We are happy to announce the release of Spot 2.14.4
This is a maintenance realease that fixes a few bugs discovered in the
path month. This includes one 11-year old bug in the code that checks
isomorphism between deterministic automata. This could lead to false
positives from `ltlfilt --equivalent-to=...`.
You can find the new release here:
http://www.lre.epita.fr/dload/spot/spot-2.14.4.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.4 (2025-12-17)
Library:
- spot::zielonka_tree was changed to include nodes labeled by {} by
default, otherwise it was hard to distinguish the tree for Inf(0)
(which had an implicit {} node) from the tree for Inf(0)|Fin(0)
(which did not). The old behavior, which is more memory efficient
and still useful in some applications, can be requested by passing
the new option zielonka_tree_options::NO_EMPTY_LAYER.
Additionally, spot::zielonka_tree::empty_layer_is_even() is a new
method that can now be used to distinguish between the above two
trees when the NO_EMPTY_LAYER option is used. (Issue #621.)
Bugs fixed:
- The isomorphism checker for deterministic automata
(spot::are_isomorphic_det) was ignoring colors! (Issue #627.)
- The recent introduction of bdd_mt_quantify_prepare() in BuDDy
caused issues with following calls to operations such as
bdd_restrict(), due to caching issues.
- Multiple typos in --help strings.
- Workarounds for new compiler warnings.
We are happy to announce the release of Spot 2.14.3
This is a maintenance realease that fixes minor compatibility issues
and bugs.
You can find the new release here:
http://www.lre.epita.fr/dload/spot/spot-2.14.3.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.3 (2025-11-11)
Bugs fixed:
- Spot's Python bindings used to map spot::parse_error exceptions
into Python's SyntaxError exception. However, recent ipython
versions have a handling of SyntaxError that really assume a
SyntaxError in Python, not an error comming from some third-party
parser reading some third-party format... That spot::parse_error
exceptions are now raised as instances of spot.parse_error.
(Issue #617.)
- Swig 4.4, released recently, contains a proper fix to Issue #603.
However, that new version also requires some update in Spot's
code. While this Spot release preserves compatibility with earlier
Swig versions, it is the first to be compatible with Swig 4.4.
- ltlf2dfa --mtdfa-stats had a bug where if "false" was the only
constant used, it would be reported as "true".
- ltlf_to_mtdfa_compose() would sometimes keep the name of states
even when instructed to discard them.
- Fix several "unnecessary virtual specifiers" reported by newer
versions of Clang.
- Many typos and documentation improvements.
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)
We are happy to announce the release of Spot 2.14.1
This is a minor realease that addresses a few bugs.
You can find the new release here:
http://www.lre.epita.fr/dload/spot/spot-2.14.1.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.1 (2025-07-21)
Bug fixes:
- print_hoa() will not use state-based output if the input has been
tagged as transition-based (i.e. prop_state_acc() == false). If
only uses state-based output when prop_state_acc() == true, or if
prop_state_acc() == maybe and the automaton is found to be
compatible with a state-based output.
- ltlfsynt's decomposition optimization (which was implemented in
the same way as we did in ltlsynt for LTL) isn't always correct
for LTLf specification. Until we know and implement a better
sufficient condition, this version disables decomposition except
for X-free specifications. (Issue #610.)
- Various documentation fixes.
--
Alexandre Duret-Lutz
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.
We are happy to announce the release of Spot 2.13.1
This is a maintenance release that only fixes minor issues discovered
since the last release and listed at the end of this email. If you do
not have any issue with Spot 2.13, there is no reason to upgrade. It
contains contributions Matthias Volk and myself.
You can find the new release here:
http://www.lre.epita.fr/dload/spot/spot-2.13.1.tar.gz
See https://spot.lre.epita.fr/ for documentation and installation
instructions.
Please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.13.1 (2025-05-21)
Bugs fixed:
- ltlsynt --print-game did not work with --global-equiv=no --polarity=yes.
- Work around a couple of compilation issues with GCC 15 and later.
- Miscelaneous documentation fixes.
We are happy to announce the release of Spot 2.13
This is a major release that comes 10 months after the
release of Spot 2.12. It contains contributions by Philipp
Schlehuber, Florian Renkin, Antoin Martin, and myself.
A list of user-visible changes is given at the end of this email.
You can find the new release here:
http://www.lre.epita.fr/dload/spot/spot-2.13.tar.gz
See https://spot.lre.epita.fr/ for documentation and installation
instructions.
Please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.13 (2025-03-24)
Command-line tools:
- ltlmix is a new tool that generates formulas by combining existing
ones. See https://spot.lre.epita.fr/ltlmix.html for examples.
- (BACKWARD INCOMPATIBILITY) ltlsynt's CSV output has been largely
overhauled, and the output columns have been both renamed (for
consistency) and augmented (with new statistics). The new CSV
output should be more useful when the input specification is
decomposed, in particular, there is a column giving the number of
sub-specifications obtained, and other statistics columns have
names starting with "max_" or "sum_" indicating how said
statistics are updated across sub-specifications.
Additionally, --csv=FILENAME will now save the source filename for
the processed formulas as the first column of the CSV file, and
the "formula" column is no longer output by default to save space.
This "formula" column can be added back with the new option
--csv-with-formula=FILENAME if really needed.
- ltlsynt learned a --part-file option, to specify the partition of
input/output proposition from a *.part file, as used in several
other tools.
- ltlfilt learned a --relabel=io mode, that is useful to shorten
atomic propositions in the context of LTL synthesis. For instance
% ltlfilt -f 'G(req->Fack)&G(go->Fgrant)' --relabel=io --ins=req,go
G(i1 -> Fo0) & G(i0 -> Fo1)
The resulting formulas are now usable by ltlsynt without having to
specify which atomic propositions are input or output, as this can
be inferred from their name. Instead of using --ins/--outs, a
--part-file option can be used as well.
- ltlfilt learned a --save-part-file[=FILENAME] option that can be
used to create partition files suitable for many synthesis tools
(including ltlsynt).
- genltl learned --lily-patterns to generate the example LTL
synthesis specifications from Lily 1.0.2. Those come with input
and output atomic propositions rewriten in the form "iNN" or "oNN",
so they can be fed to ltlsynt directly, as in
% genltl --lily-patterns | ltlsynt -q
- genltl's --pps-arbiter-standard and --pps-arbiter-strict have been
changed to rename variables {r1,r2,...,g1,g2...} as
{i1,i2,...,o1,o2,...} so that these formulas can be fed directly to
ltlsynt.
- autfilt learned --restrict-dead-end-edges, to restricts labels of
edges leading to dead-ends. See the description of
restrict_dead_end_edges_here() below.
- autfilt learned --track-formula=F to label states with formulas
derived from F. (This is more precise on deterministic automata.)
- autfilt learned --mcs[=any|scc] to reorder states according to a
maximum cardinality search. The argument specifies how to break
ties.
- autfilt learned --given-formula, --given-automaton, and
--given-strategy to simplify automata given some knowledge.
This is discussed in the PN'25 paper "Simplifying LTL
Model-Checking Given Prior Knowledge" by Duret-Lutz, Poitrenaud,
and Thierry-Mieg.
- ltlfilt learned --pi1, --sigma1, --delta1, --pi2, --sigma2, and
--delta2 to filter according to classes Π₁,Σ₁,Δ₁,Π₂,Σ₂, and Δ₂.
- ltlfilt learned --to-delta2 to transform an LTL formula into Δ₂.
Library:
- restrict_dead_end_edges_here() can reduce non-determinism (but
not remove it) by restricting the label L of some edge (S)-L->(D)
going to a state D that does not have other successors than
itself. The conditions are detailed in the documentation of
this function.
- spot::postprocessor will now call restrict_dead_end_edges_here()
in its highest setting. This can be fine-tuned with the "rde"
extra option; see the spot-x (7) man page for detail.
- The formula class now keeps track of membership to the Δ₁, Σ₂,
Π₂, and Δ₂ syntactic classes. This can be tested with
formula::is_delta1(), formula::is_sigma2(), formula::is_pi2(),
formula::is_delta2(). See doc/tl/tl.pdf from more discussion.
- spot::to_delta2() implements Δ₂-normalization for LTL formulas,
following "Efficient Normalization of Linear Temporal Logic" by
Esparza et al. (J. ACM, 2024).
- Trivial rewritings (those performed everytime at construction)
were missing the rule "[*0]|f ≡ f" when f already accepts the
empty word. (Issue #545.)
- spot::match_states(A, B) is a new function that returns a vector
V such that V[x] contains all states y such that state (x, y) can
reach an accepting cycle in product(A, B). In particular, if A
and B accept the same language, any word accepted by A from state
x can be accepted in B from some state in V[x].
That function also has a variant spot::match_states(A, f) where f
is an LTL formula. In this case, it returns an array of
formulas. If f represents a superset of the language of A, then
any word accepted by A from state x satisfies V[x]. Related to
Issue #591.
- twa_graph::defrag_states(num) no longer requires num[i]≤i; num
can now describe a permutation of the state numbers.
- spot::maximum_cardinality_search() and
spot::maximum_cardinality_search_reorder_here() are new function
to compute (and apply) an ordering of states based on a maximum
cardinality search.
- a new set of functions spot::update_bounds_given(),
spot::bounds_simplify(), and spot::stutterize_given() implements
simplification of automata based on apriori knowledge.
See https://spot.lre.epita.fr/ipynb/given.html for examples.
Bug fixes:
- "ltlsynt --aiger -q ..." was still printing the realizability
status and the AIG circuit; it now does the job silently as
requested.
- ltlsynt had a minor memory leak.
We are happy to announce the release of Spot 2.12.2
This is a maintenance release fixing a couple of bugs discovered since
our 2.12.1 release. In particular, it fixes a serious bug with
to_finite(), used in some LTLf applications, and another one in the
AIGER encoder used by ltlsynt.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.12.2.tar.gz
See https://spot.lre.epita.fr/ for documentation and installation
instructions.
Please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.12.2 (2025-01-18)
Bug fixes:
- to_finite() was dealing incorrectly with edges that were
both alive and dead. (Issue #596.)
- LaTeX output of the X[!] operator was broken in both
LaTeX and self-contained LaTeX mode. (Issue #597)
- Fix a bug in the AIGER encoding with certain forms of
global-equivalence.
- Work around a spurious test failure with Python 3.13.
