Spot-announce

Download

spot-announce@lrde.epita.fr

September 2026

1 participants
1 discussions

Spot 2.16 has been released
by Alexandre Duret-Lutz 03 Sep '26

03 Sep '26

We are happy to announce the release of Spot 2.16 This is a major release introducing two new tools (autdo, autwords), better support for Quantified LTL, more operations for MTBDD-based automata, support for on-the-fly translation in the main LTL translator, support for Moore semantics in ltlsynt, support for terminal semantics with the __SigAlive__ signal in ltlfsynt, and many more (see below). This release contains contributions by Perrine Le Duc, Vladimir Mungiu, Philipp Schlehuber-Caissier, Florian Renkin, and myself. You can find the new release here: http://www.lre.epita.fr/dload/spot/spot-2.16.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 (2026-09-03) Build: - It is now possible to pass a release tarball to "pip install", making it easier to compile and install Spot in a virtual environment for Python. Tools: - autdo is a new tool, similar to ltldo, but for automata: it runs automata through one or more external tools and outputs the results. Its input options are the same as those of autcross, and its output options are the same as those of ltldo (e.g., ability to output the smallest or largest result from multiple tools, changing the output format, killing tools on timeout...). (Issue #466.) - autwords is a new tool that enumerates lasso-shaped words accepted by an ω-automaton. (Issue #642.) - genaut learned a new family of automata --el-empty=k,N. It generates a one-state, empty-language automaton with a complex EL acceptance condition designed to challenge EL emptiness-checking algorithms. - autcross and autdo now recognize "kofola" as a shorthand, appending "%H>%O" when no %-sequence is used in the command. - ltldo's --stats format string now documents the tool name under "%K" instead of "%T", for consistency with autdo and with the autfilt convention (where "%T" is the number of transitions in the input). The old "%T" sequence is still supported by ltldo, but undocumented. - ltlfilt's and randltl's -r/--simplify option now accepts named simplification options such as basics, synt-impl, event-univ, containment-checks, containment-checks-stronger, nenoform-stop-on-boolean, reduce-size-strictly, boolean-to-isop, favor-event-univ, keep-top-xor, and a new unit-propagation. Multiple options can be combined with commas, prefixed with '!' to disable. The historical levels 0-3 remain supported. - ltlfilt learned a --distribute-X option that distributes X and X[!] operators over Boolean connectives. - ltlsynt learned a --semantics=Moore option to synthesize reactive controllers under Moore (output-first) semantics, where the controller's outputs depend only on the history of inputs, not on the current input. This is in addition to the default Mealy (input-first) semantics. (Issue #608.) - ltlfsynt now encodes terminating semantics in AIGER circuits by adding an extra output named __SigAlive__ that is initially true and becomes false after the controller takes its first self-loop (i.e., terminates). The signal name can be changed with --terminating=NAME, and the feature can be disabled with --non-terminating. (Issue #635.) - ltlfsynt now has a --verify option to check that the computed strategy or AIG circuit satisfies the specification. For Mealy machines, the strategy is converted to a Büchi automaton with an explicit termination signal before checking against the negated specification. For AIG circuits, the check is performed using the circuit's transition relation. - ltlsynt learned --print-each-mealy to print each Mealy machine produced for a decomposed specification before AIGER encoding. - ltlf2dfa --translation=compositional now also supports QLTL. (Quantifiers were only supported by --translation=direct before.) Library: - the spot::translator class learned to deal with quantified LTL with arbitrary nesting of quantifiers at the top level. Those quantifications are easier to deal with in the syntactic-obligation fragment; in the general case only a single \exists operator can be handled efficiently, and other situations involve complementing automata. - spot::lasso_enumerator is a new class that lazily enumerates all lasso-shaped accepted runs and words of an ω-automaton, within user-supplied bounds on stem and cycle lengths. (Issue #642.) - spot::bdd_dict::ap_from_var(int var) is a new method that returns the atomic proposition formula associated to a BDD variable number, or nullptr if the variable is not an atomic proposition. This avoids having to access the internal bdd_map directly. (Issue #622.) - BuDDy has a new function called bdd_splitcube(), used to split a cube according to a set of variables. (Issue #644.) - spot::analyze_dependent_output() is a new function that identifies output variables whose values may depend on previous output values. The supporting BuDDy function bdd_have_dependent_var() is also available. (See "On Dependent Variables in Reactive Synthesis" by Akshay et al. TACAS'24) - spot::obligation_to_mtdswa() now also supports \exists and \forall. - improve support for unobservable inputs in ltlsynt. It now works with all translation algorithms (not just SD or DS), and relies on existential quantification performed during the translation, not afterwards. - spot::are_equivalent() now uses product_xor() + is_empty() to test equivalence of two deterministic automata, instead of using two inclusion checks. This is simpler and slightly faster. (Issue #598.) - spot::from_ltlf() has a new overload from_ltlf(f, alive, algo) that accepts an integer algorithm selector. algo=0 selects the original De Giacomo & Vardi (IJCAI'13) reduction to LTL; algo=1 (the new default) selects a new reduction that guarantees the result is a syntactic obligation. The two-argument overload from_ltlf(f, alive) reads the SPOT_FROM_LTLF environment variable to pick the algorithm (defaulting to 1). See also https://arxiv.org/abs/2609.00379 - spot::ltl_to_tgba_fm_otf is a new class that exposes the core Couvreur/FM LTL-to-TGBA translation as an on-the-fly explorer. The existing spot::ltl_to_tgba_fm() has been refactored to use this class. - spot::ltl_satisfiable() (introduced in 2.15) has been rewritten to use the above on-the-fly explorer. Note that this function is used by 'ltlfilt --satisfiable'. (Issue #626.) - spot::distribute_next() is a new function that distributes X and X[!] operators over Boolean connectives in a formula. - spot::unit_propagate() is a new function that simplifies an LTL formula by propagating unit facts through the formula tree in a single top-down pass. See the "Unit Propagation" section of doc/tl/tl.pdf for details. (Issue #606.) - spot::tl_simplifier_options has a new option unit_prop that, when enabled, runs spot::unit_propagate() as a first pass before the usual recursive rewriting. (Issue #606.) - Repetition bounds used by the operators [*i..j], [=i..j], [->i..j], [:*i..j], F[i..j], G[i..j], X[i], X[!][i] etc. are now stored as 16-bit values instead of 8-bit values, allowing bounds up to 65534 (instead of 254). (Issue #485.) - Several functions gained a new 'moore' parameter to support Moore (output-first) semantics in addition to the traditional Mealy (input-first) semantics: spot::split_2step(), spot::apply_strategy(), spot::solved_game_to_mealy(), and spot::alternate_players(). A new spot::synthesis_info::moore field was also added. (Issue #608.) - spot::mealy_machine_to_aig(), spot::mealy_machines_to_aig(), and spot::print_aiger() learned an optional terminating_signal parameter to encode terminating semantics in AIGER circuits. When set, an extra output (named after the given string) is added that is initially true and becomes false after the first self-loop of the Mealy machine. (Issue #635.) - randomize() now preserves more named properties. (Issue #532.) - Boolean operations over mtdswa_ptr have been implemented as product(), product_or(), product_xor(), product_nxor(), product_implies(), complement(). - quantification functions are implemented for weak mtdswa_ptr and for mtdfa_ptr as quantify_exists() and quantify_forall(). - trim() is a new function to remove useless states in mtdswa_ptr and in mtdfa_ptr. - generic_emptiness_check_select_version() now accepts spot216, a new generic emptiness-checking algorithm with improved asymptotic complexity for the relevant acceptance conditions. Deprecation notices: - spot::collect_aps_with_polarities() is deprecated; use spot::collect_apids_with_polarities() instead, it is available since Spot 2.15. Bug fixes: - Acceptance formulas that are too large to be stored internally now cause a std::runtime_error to be thrown, rather than silently producing a corrupt formula. The internal representation has also been changed to use a 24-bit field for the subtree size (up from 16 bits). - The condition to apply the trivial simplification f[*i..j][*k..l] = f[*ik..jl] was not capturing the cases where k=l. - ltlsynt --splittype=fullsym had a bug that could cause unrealizable specifications to be erroneously declared realizable. (Issue #647.) - Fix some incorrect results of ltlsynt in rare cases involving decomposition, polarity-based simplification, and obligation-based synthesis. LedMatrix.tlsf is one such case. (Issue #651.) - random_formula::parse_options() and randltlgenerator() were using strtok() to parse priority strings, which mutates the input buffer and is non-reentrant. This could crash when called with a string literal, and worked only by luck from Python (SWIG's temporary buffer happened to be writable). The parsing has been rewritten to use a non-mutating string_view tokenizer, and the priority parameters now take const char*. Removed functions: - spot::is_bare_word() and spot::quote_unless_bare_word() [misc/bareword.hh]. These functions were never used anywhere in the library or tools. Removed functions (deprecated since Spot 2.9 or earlier): - spot::copy() [twaalgos/copy.hh, deprecated since 2.4]: use spot::make_twa_graph() instead. - spot::dtwa_complement() [twaalgos/complement.hh, deprecated since 2.4]: use spot::dualize() instead. - spot::decompose_strength() [twaalgos/strength.hh, deprecated since 2.4]: use spot::decompose_scc() instead. - spot::twa::prop_deterministic() (setter and getter) [twa/twa.hh, deprecated since 2.4]: use spot::twa::prop_universal() instead. - spot::twa::prop_set(bool, bool, bool, bool, bool) (5-argument form) [twa/twa.hh, deprecated since 2.4]: use the 6-argument form that also takes a "complete" argument. - spot::scc_info::acc() [twaalgos/sccinfo.hh, deprecated since 2.5]: use spot::scc_info::acc_sets_of() instead. - spot::scc_info::used_acc() [twaalgos/sccinfo.hh, deprecated since 2.5]: use spot::scc_info::marks() instead. - spot::scc_info::used_acc_of() [twaalgos/sccinfo.hh, deprecated since 2.5]: use spot::scc_info::marks_of() instead. - spot::acc_cond::mark_t::value_t [twa/acc.hh, deprecated since 2.6]: mark_t no longer relies on unsigned. - spot::acc_cond::mark_t(unsigned) [twa/acc.hh, deprecated since 2.6]: use brace initialization instead (e.g., mark_t{} or mark_t::all()). - spot::acc_cond::mark_t::operator==(unsigned) and operator!=(unsigned) [twa/acc.hh, deprecated since 2.6]: compare mark_t to mark_t, not to unsigned. - spot::twa::intersecting_run(const_twa_ptr, bool) [twa/twa.hh, deprecated since 2.8]: replace a->intersecting_run(b, true) by b->intersecting_run(a). - spot::acc_cond::format(std::ostream&, mark_t) and spot::acc_cond::format(mark_t) [twa/acc.hh, deprecated since 2.8]: use operator<< or mark_t::as_string() instead. - spot::iar() [twaalgos/toparity.hh, deprecated since 2.9]: use spot::to_parity() instead. - spot::iar_maybe() [twaalgos/toparity.hh, deprecated since 2.9]: use spot::to_parity() and spot::acc_cond::is_rabin_like() instead.

1 0