We are happy to announce the release of Spot 2.16.1
This is a maintenance releases fixings several bugs that have been
reported since the release of 2.16. (But these bugs are actually much
older.)
This release contains contributions by Ondřej Lengál and myself.
You can find the new release here:
http://www.lre.epita.fr/dload/spot/spot-2.16.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/-/works_item/new
New in spot 2.16.1 (2026-10-16)
Bug fixes:
- is_generalized_rabin() and is_generalized_streett() could fail on
acceptance formulas that use the maximum number of colors
supported by Spot.
- writing to files using `-o PATTERN.out` will now flush after each
formula or automaton is output. This ensure that the file can be
properly read even if the tool hasn't yet closed it (because it
might append to it later).
- Some algorithms that temporarily override the acceptance condition
of an automaton (via scc_and_mark_filter) could lower the number
of acceptance sets declared by that automaton when restoring its
acceptance condition, if the highest sets occurred only on edges.
For instance, autfilt --is-inherently-weak, --is-semi-deterministic,
or --is-unambiguous could output automata that use undeclared
acceptance sets, and that could not be parsed back. (Issue #655.)
- autfilt --track-formula could crash on exit when Spot was built
with static libraries, because the formula it kept in a global
variable was destroyed after the table of atomic propositions.
(Issue #656.)
- When called with acc_clean and propagate_col disabled,
to_parity() could produce an automaton with a different language
if some edges of its input carried acceptance sets that are not
used by the acceptance condition. It also read past the end of
an internal array in that case. (Issue #657.)
- to_parity() failed an assertion in try_parity_prefix() when the
SCCs left after removing a parity prefix produced no colored
edge. The code following that assertion was already correct in
that case, but only by relying on unsigned wrap-around.
(Issue #658.)
- to_parity() failed an assertion when no edge of its output
received a color although its input had edges, which happens
when all cycles of the input are rejecting (e.g., with acceptance
"f"). Such automata are now converted into automata with
acceptance "f". (Issue #659.)
- Improve speed of syntactic implication checks. (Issue #660.)
- Translation from LTL to automata with generic acceptance
conditions (e.g., with `ltl2tgba G -D`) could produce an incorrect
automaton on formula involving <-> or xor, with a safety formula
in one operand, and some non-obligation formula on the other one.
(Issue #662.)
