Spot 2.15.1 has been released to fix a compilation issue
reported right after the release of Spot 2.15.
You can find the new release here:
http://www.lre.epita.fr/dload/spot/spot-2.15.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.15.1 (2026-04-25)
Bugs fixes:
- Fix compilation error due to std::result_of being removed from
C++20. (Issue #643.)
- The new path to translate syntactic obligation to deterministic
Büchi automata forgot to mark automata generated from X-free
formulas as stutter-invariant.
New in spot 2.15 (2026-04-24)
Backward-incompatible changes:
- Spot is now built in C++20 mode, so you need at least GCC 10 or
Clang 10 to compile it. There is also an --enable-c++23 option
to configure in case you want to force a build of Spot in C++23
mode.
- Two new operators \forall and \exists have been added to the LTL
syntax in order to support QLTL and QLTLf in the future. (See
below for the limited support at present.) If you have code
working on the AST of formulas, it is likely that you will have to
update it to account for the new op::exists and op::forall
operators.
- The 'ltl2tgta' tool, that was used to build "testing automata"
and print them in dot format, has been removed.
- All the code supporting (generalized) testing automata has been
removed. This code was initially introduced in Spot 1.0, and
received only minimal updates for Spot 2.0; it was poorly
tested/covered.
Maintaining it in Spot does not seem worth the human effort and
CI/CD resources it takes.
- ltlfsynt --translation=dfs-strict-on-the-fly is not supported
anymore. This required specific code that was slower than
--translation=dfs-on-the-fly.
Documentation:
- https://spot.lre.epita.fr/tut91.html is a new page that talks
about the low-level MTBDD operations that have been introduced in
Spot 2.14 and in this release.
Tools:
- Synthesis of syntactic-obligations, and their translation to
deterministic automata just got a lot faster. This mainly
concerns ltl2tgba and ltlsynt. See the notes about spot::mtdswa
below. The improved translation path can be disabled in ltl2tgba
and ltlsynt by passing option -xnew-oblig=0.
This builds upon some new translation presented in a paper
titled "Fast obligation translation and synthesis" to appear
at CAV'26.
- ltlsynt has a new option --obligation-synthesis=no that can be
used to disable MTBDD-based synthesis when the specification is
an obligation. (See the aforementioned CAV'26 paper)
- ltlsynt and ltlfsynt just learned an option --unobservable-ins to
specify a list of input propositions that may appear in the
specification, but that should not be observed by the controller.
This builds upon some technique presented in a paper titled
"On-the-fly LTLf synthesis under partial observability", to appear
at KR'26.
- ltlfilt learned the --unobservable-ins option too. This can be
useful to relabel input/output/unobservable variables using the
--relabel=io option (renamed unobservable variables will start
with u), or to write part files with --save-part-file.
- ltlfilt learned a --satisfiable option to keep only satisfiable
formulas. See the comments on ltl_satisfiable() below.
- genltl's --kr-nlogn=N and --kr-n=N options, introduced in Spot
2.3.1, generate LTL formulas that can only be recognized by a DBA
of doubly-exponential size. Those formulas actually describe
obligation properties, but they are not syntactic obligations.
The new --kr-nlogn-delta1=N and --kr-n-delta1=N options generate
variants of those formulas that are equivalent to the previous
properties, but that both belong to the Δ₁ fragment of LTL (i.e.,
the fact that they are obligation properties can be checked
syntactically.)
- autfilt --given-strategy=... learned "auto-small" and "auto-si",
to implement a loop where the automaton is regularly simplified
with --given-strategy=minato and --given-strategy=relax, returning
the smallest automaton found (with "auto-small"), or the smallest
automaton that is stutter-invariant (with "auto-si"). If
postprocessing options like --small or --deterministic are given,
they will also be applied during this loop.
Library:
- There is a new class called spot::mtdswa to represent
state-based deterministic ω-automata using MTBDDs.
See https://spot.lre.epita.fr/ipynb/mtdswa.html for examples
covering the next three points as well.
- spot::obligation_to_mtdswa() is a new function to translate
syntactic-obligations to a weak spot::mtdswa.
- spot::loding_weak_ranking() and spot::minimize_mtdswa()
are new functions that can be used together to minimize
a weak spot::mtdswa.
- spot::obligation_synthesis() is a new function to synthesize
syntactic-obligation specifications using MTBDDs.
- scc_filter() will now preserve and update any "original-states"
or "degen-levels" property present in the original automaton.
- formula::multop() and its variants (formula::And(),
formula::Concat(), etc.) now accept a two-operand variant instead
of a vector. For instance, instead of formula::And({x, y})
it is now possible to write formula::And(x, y). A vector still
has to be constructed internally; however, the two-argument
syntax is a bit more efficient at inlining arguments when one of
the arguments uses the same n-ary operator.
- atomic propositions are now assigned a unique 0-based identifier,
so that mapping atomic proposition to arbitrary data can easily be
done using an array. See https://www.lre.epita.fr/tut03.html#apid
for some discussion.
- formula::map() will not attempt to recreate nodes that haven't
changed. This saves time.
- ltlf_one_step_sat_rewrite and ltlf_one_step_unsat_rewrite now use
a cache internally. The ltlf_one_step_sat_rewrite_cached and
ltlf_one_step_unsat_rewrite_cached classes make it possible to
reuse the same cache between calls. This is now used by LTLf
synthesis functions to speed up one-step (un)realizability checks.
- spot::ltl_satisfiable() is a new function to test if a formula is
satisfiable. The implementation is currently very simple: after
some cheap preprocessing, the formula is converted to a TGBA that
is then checked for emptiness. It can be improved later.
(Issue #623.)
- Preliminary support for \forall and \exists:
- A formula such as '\forall a, c: a U (b W c)' is stored
as a formula of type op::forall with children [a, c, a U (b W c)].
I.e., the last child is the quantified formula, and previous children
are the atomic proposition to quantify. \exists is handled
similarly.
- The parser will allow these quantification operators at the
top-level of a formula, or right below another quantification
operator.
- spot::collect_aps_with_polarities() and
spot::collect_equivalent_literals() were taught to ignore the
quantifiers when processing formulas.
- spot::print_dot(), spot::print_psl(), and other print functions
learned to print these new operators.
- spot::normalize_quantifier() is a new function used to remove
quantification over variables that are missing from the body.
It also removes variables that have a constant polarity.
- the spot::tl_simplifier uses spot::normalize_quantifier()
For instance:
% ltlfilt --simplify=1 -f '\forall a, c: a U b W c'
Gb
- spot::ltl_to_tgba_fm() now supports existentially quantified LTL
formulas (producing non-deterministic TGBA). The quantification
is performed during the translation, not a posteriori. Universal
quantification is _not_ supported.
- spot::obligation_synthesis() and spot::ltlf_to_mtdfa_for_synthesis()
support both quantifiers, even nested. In particular, universal
quantification is used to implement synthesis with partial
observability.
- spot::ltlf_to_mtdfa (and the ltlf2dfa tool) support both
quantifiers too, even nested.
Bug fixes:
- Let ltlfilt's --save-part-file work even if -q is used. (Issue #632.)
- ltlfsynt --decompose was found to be bogus in tricky cases. It is
disabled (i.e., defaults to "no") in this release, until we find a
fix. (Issue #610)
- The decomposition in the context of LTL synthesis contained an error in the
splitting of implications. The correction did not impact any cases in the
Syntcomp or any of the tests.
- A poorly defined hash function used in tgba_determinize() could
cause that function to throw a "robin_hood::map overflow"
exception. (Issue #631.)
We are happy to announce the release of Spot 2.15.
Notable changes in this release include improvements to the translation
of syntactic-obligation formulas to deterministic automata, improvements
to the synthesis of syntactic-obligation specifications, support for
synthesis of LTL or LTLf under partial observability, support for
quantified LTLf translation, partial support for quantified LTL
translation, and the switch from C++17 to C++20.
A more detailed list of user-visible changes is at the end of this
email.
You can find the new release here:
http://www.lre.epita.fr/dload/spot/spot-2.15.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.15 (2026-04-24)
Backward-incompatible changes:
- Spot is now built in C++20 mode, so you need at least GCC 10 or
Clang 10 to compile it. There is also an --enable-c++23 option
to configure in case you want to force a build of Spot in C++23
mode.
- Two new operators \forall and \exists have been added to the LTL
syntax in order to support QLTL and QLTLf in the future. (See
below for the limited support at present.) If you have code
working on the AST of formulas, it is likely that you will have to
update it to account for the new op::exists and op::forall
operators.
- The 'ltl2tgta' tool, that was used to build "testing automata"
and print them in dot format, has been removed.
- All the code supporting (generalized) testing automata has been
removed. This code was initially introduced in Spot 1.0, and
received only minimal updates for Spot 2.0; it was poorly
tested/covered.
Maintaining it in Spot does not seem worth the human effort and
CI/CD resources it takes.
- ltlfsynt --translation=dfs-strict-on-the-fly is not supported
anymore. This required specific code that was slower than
--translation=dfs-on-the-fly.
Documentation:
- https://spot.lre.epita.fr/tut91.html is a new page that talks
about the low-level MTBDD operations that have been introduced in
Spot 2.14 and in this release.
Tools:
- Synthesis of syntactic-obligations, and their translation to
deterministic automata just got a lot faster. This mainly
concerns ltl2tgba and ltlsynt. See the notes about spot::mtdswa
below. The improved translation path can be disabled in ltl2tgba
and ltlsynt by passing option -xnew-oblig=0.
This builds upon some new translation presented in a paper
titled "Fast obligation translation and synthesis" to appear
at CAV'26.
- ltlsynt has a new option --obligation-synthesis=no that can be
used to disable MTBDD-based synthesis when the specification is
an obligation. (See the aforementioned CAV'26 paper)
- ltlsynt and ltlfsynt just learned an option --unobservable-ins to
specify a list of input propositions that may appear in the
specification, but that should not be observed by the controller.
This builds upon some technique presented in a paper titled
"On-the-fly LTLf synthesis under partial observability", to appear
at KR'26.
- ltlfilt learned the --unobservable-ins option too. This can be
useful to relabel input/output/unobservable variables using the
--relabel=io option (renamed unobservable variables will start
with u), or to write part files with --save-part-file.
- ltlfilt learned a --satisfiable option to keep only satisfiable
formulas. See the comments on ltl_satisfiable() below.
- genltl's --kr-nlogn=N and --kr-n=N options, introduced in Spot
2.3.1, generate LTL formulas that can only be recognized by a DBA
of doubly-exponential size. Those formulas actually describe
obligation properties, but they are not syntactic obligations.
The new --kr-nlogn-delta1=N and --kr-n-delta1=N options generate
variants of those formulas that are equivalent to the previous
properties, but that both belong to the Δ₁ fragment of LTL (i.e.,
the fact that they are obligation properties can be checked
syntactically.)
- autfilt --given-strategy=... learned "auto-small" and "auto-si",
to implement a loop where the automaton is regularly simplified
with --given-strategy=minato and --given-strategy=relax, returning
the smallest automaton found (with "auto-small"), or the smallest
automaton that is stutter-invariant (with "auto-si"). If
postprocessing options like --small or --deterministic are given,
they will also be applied during this loop.
Library:
- There is a new class called spot::mtdswa to represent
state-based deterministic ω-automata using MTBDDs.
See https://spot.lre.epita.fr/ipynb/mtdswa.html for examples
covering the next three points as well.
- spot::obligation_to_mtdswa() is a new function to translate
syntactic-obligations to a weak spot::mtdswa.
- spot::loding_weak_ranking() and spot::minimize_mtdswa()
are new functions that can be used together to minimize
a weak spot::mtdswa.
- spot::obligation_synthesis() is a new function to synthesize
syntactic-obligation specifications using MTBDDs.
- scc_filter() will now preserve and update any "original-states"
or "degen-levels" property present in the original automaton.
- formula::multop() and its variants (formula::And(),
formula::Concat(), etc.) now accept a two-operand variant instead
of a vector. For instance, instead of formula::And({x, y})
it is now possible to write formula::And(x, y). A vector still
has to be constructed internally; however, the two-argument
syntax is a bit more efficient at inlining arguments when one of
the arguments uses the same n-ary operator.
- atomic propositions are now assigned a unique 0-based identifier,
so that mapping atomic proposition to arbitrary data can easily be
done using an array. See https://www.lre.epita.fr/tut03.html#apid
for some discussion.
- formula::map() will not attempt to recreate nodes that haven't
changed. This saves time.
- ltlf_one_step_sat_rewrite and ltlf_one_step_unsat_rewrite now use
a cache internally. The ltlf_one_step_sat_rewrite_cached and
ltlf_one_step_unsat_rewrite_cached classes make it possible to
reuse the same cache between calls. This is now used by LTLf
synthesis functions to speed up one-step (un)realizability checks.
- spot::ltl_satisfiable() is a new function to test if a formula is
satisfiable. The implementation is currently very simple: after
some cheap preprocessing, the formula is converted to a TGBA that
is then checked for emptiness. It can be improved later.
(Issue #623.)
- Preliminary support for \forall and \exists:
- A formula such as '\forall a, c: a U (b W c)' is stored
as a formula of type op::forall with children [a, c, a U (b W c)].
I.e., the last child is the quantified formula, and previous children
are the atomic proposition to quantify. \exists is handled
similarly.
- The parser will allow these quantification operators at the
top-level of a formula, or right below another quantification
operator.
- spot::collect_aps_with_polarities() and
spot::collect_equivalent_literals() were taught to ignore the
quantifiers when processing formulas.
- spot::print_dot(), spot::print_psl(), and other print functions
learned to print these new operators.
- spot::normalize_quantifier() is a new function used to remove
quantification over variables that are missing from the body.
It also removes variables that have a constant polarity.
- the spot::tl_simplifier uses spot::normalize_quantifier()
For instance:
% ltlfilt --simplify=1 -f '\forall a, c: a U b W c'
Gb
- spot::ltl_to_tgba_fm() now supports existentially quantified LTL
formulas (producing non-deterministic TGBA). The quantification
is performed during the translation, not a posteriori. Universal
quantification is _not_ supported.
- spot::obligation_synthesis() and spot::ltlf_to_mtdfa_for_synthesis()
support both quantifiers, even nested. In particular, universal
quantification is used to implement synthesis with partial
observability.
- spot::ltlf_to_mtdfa (and the ltlf2dfa tool) support both
quantifiers too, even nested.
Bug fixes:
- Let ltlfilt's --save-part-file work even if -q is used. (Issue #632.)
- ltlfsynt --decompose was found to be bogus in tricky cases. It is
disabled (i.e., defaults to "no") in this release, until we find a
fix. (Issue #610)
- The decomposition in the context of LTL synthesis contained an error in the
splitting of implications. The correction did not impact any cases in the
Syntcomp or any of the tests.
- A poorly defined hash function used in tgba_determinize() could
cause that function to throw a "robin_hood::map overflow"
exception. (Issue #631.)
New in spot 2.14.5 (2025-01-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.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.
