Spot-announce

Download

spot-announce@lrde.epita.fr

April 2026

1 participants
2 discussions

Spot 2.15.1 has been released
by Alexandre Duret-Lutz 26 Apr '26

26 Apr '26

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

1 0

Spot 2.15 released
by Alexandre Duret-Lutz 24 Apr '26

24 Apr '26

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

1 0