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@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.