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.
