Spot-announce

spot-announce@lrde.epita.fr

1 participants
110 discussions

Spot 2.14.1 released
by Alexandre Duret-Lutz 21 Jul '25

21 Jul '25

We are happy to announce the release of Spot 2.14.1 This is a minor realease that addresses a few bugs. You can find the new release here: http://www.lre.epita.fr/dload/spot/spot-2.14.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.14.1 (2025-07-21) Bug fixes: - print_hoa() will not use state-based output if the input has been tagged as transition-based (i.e. prop_state_acc() == false). If only uses state-based output when prop_state_acc() == true, or if prop_state_acc() == maybe and the automaton is found to be compatible with a state-based output. - ltlfsynt's decomposition optimization (which was implemented in the same way as we did in ltlsynt for LTL) isn't always correct for LTLf specification. Until we know and implement a better sufficient condition, this version disables decomposition except for X-free specifications. (Issue #610.) - Various documentation fixes. -- Alexandre Duret-Lutz

1 0

Spot 2.14 released
by Alexandre Duret-Lutz 26 Jun '25

26 Jun '25

We are happy to announce the release of Spot 2.14 This is a major release that includes two new tools related to LTLf and developed over the past 8 months. You can find the new release here: http://www.lre.epita.fr/dload/spot/spot-2.14.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.14 (2025-06-26) Build: - When Python bindings are enabled, Spot now requires Python 3.8 or later. Python 3.8 is already quite old: it reached end-of-life in 2024. Python 3.8 was used for instance in Ubuntu 20.04, where you can install this version of Spot. Command-line tools: - ltlf2dfa is a new tool that converts LTLf to MTDFA, i.e., DFA represented with multi-terminal BDDs. See https://spot.lre.epita.fr/ltlf2dfs.html for some examples. - ltlfsynt is a new tool that solves the reactive synthesis for LTLf specification, using a reachability game interpreted oveer MTDFA. See https://spot.lre.epita.fr/ltlfsynt.html The output of --realizability has been compared to several other tools on benchmarks from the synthesis competition (which all use Moore semantics) in addition to some custom specifications (with Moore and Mealy semantics) in our test suite. The production of a Mealy machine representing the controller has been implemented, but it hasn't received a lot of testing so far, it should be regarded as very experimental. For more information about ltlf2dfa and ltlfsynt, refer to the paper "Engineering an LTLf Synthesis Tool" to be presented at CIAA'25. - genltl learned four new options: --tv-counter-mealy=N, --tv-double-counters-mealy=N, --tv-nim-mealy=N,M, --chomp-mealy=N,M. These are scalable LTLf specifications that can be used directly with ltlfsynt. The first three options are taken from the literature; Chomp is an original familly that has been submitted as a new model to SyntComp'25. - ltlf2tgba learned an --ltlf option. This currently implements the very slow approach of going from LTLf->LTL->DBA->DFA. ltlf2dfa is way faster. - Tools that take a "--tlsf FILENAME" option (ltlsynt, ltlfsynt, and ltlf2dfa currently) will now accept arguments of the form FILENAME/VAR1=VAL1,VAR2=VAL2... to override parameters defined in the TLSF file. E.g.: ltlsynt --tlsf arbiter.tlsf/n=3 Library: - spot::mtdfa is a new class implementing a DFA using Multi-Terminal BDDs. The data structure is similar to what can be found in Mona. This comes with convenient rendering routines for use in Jupyter notebook. - spot::ltlf_to_mtdfa() and spot::ltlf_to_mtdfa_compose() are new functions that converts a LTLf formula into an MTDFA, using either a direct translation, or a compositional one. - spot::minimize_mtdfa() is a minimization function for MTDFA. See https://spot.lre.epita.fr/ipynb/ltlf2dfa.html for some illustrations. - spot::product_or(), spot::product_and(), spot::product_xor(), etc. have been overloaded to implement those operations on MTDFAs as well. - spot::backprop_graph is a new class implementing what's needed to run a linear backpropagation for solving reachability games. This allows solving the game on-the-fly, as it is constructed. See https://spot.lre.epita.fr/ipynb/backprop.html for examples. - spot::ltlf_to_mtdfa_for_synthesis() is a new function that performs LTLf synthesis. - spot::translator learned output_type::Finite to request translation to Finite automata.

1 0

Spot 2.13.2 released
by Alexandre Duret-Lutz 12 Jun '25

12 Jun '25

We are happy to announce the release of Spot 2.13.2 This is a maintenance release that fixes a few issues. You can find the new release here: http://www.lre.epita.fr/dload/spot/spot-2.13.2.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.13.2 (2025-06-12) Bugs fixed: - compiling from git with a missing Bison would display a confusing error (Issue #607) - the Python bindings for iterators generated by Swig are not working with libc++ when multiple modules are used. (Everything works with libstdc++.) This caused issues in Mac OS and OpenBSD. This version implements a workaround until Swig is fixed. (Issue #603) - Fix spurious failure of ltlsynt.test on OpenBSD. - difference_word_forq() could return different words on different architectures because the code was iterating on hash_map that can be implemented in different ways. - remove_univ_otf() had a memory-handling bug, that could cause use-after-free errors.

1 0

Spot 2.13.1
by Alexandre Duret-Lutz 22 May '25

22 May '25

We are happy to announce the release of Spot 2.13.1 This is a maintenance release that only fixes minor issues discovered since the last release and listed at the end of this email. If you do not have any issue with Spot 2.13, there is no reason to upgrade. It contains contributions Matthias Volk and myself. You can find the new release here: http://www.lre.epita.fr/dload/spot/spot-2.13.1.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.1 (2025-05-21) Bugs fixed: - ltlsynt --print-game did not work with --global-equiv=no --polarity=yes. - Work around a couple of compilation issues with GCC 15 and later. - Miscelaneous documentation fixes.

1 0

Spot 2.13 released
by Alexandre Duret-Lutz 24 Mar '25

24 Mar '25

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.

1 0

Spot 2.12.2 released
by Alexandre Duret-Lutz 18 Jan '25

18 Jan '25

We are happy to announce the release of Spot 2.12.2 This is a maintenance release fixing a couple of bugs discovered since our 2.12.1 release. In particular, it fixes a serious bug with to_finite(), used in some LTLf applications, and another one in the AIGER encoder used by ltlsynt. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.12.2.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.12.2 (2025-01-18) Bug fixes: - to_finite() was dealing incorrectly with edges that were both alive and dead. (Issue #596.) - LaTeX output of the X[!] operator was broken in both LaTeX and self-contained LaTeX mode. (Issue #597) - Fix a bug in the AIGER encoding with certain forms of global-equivalence. - Work around a spurious test failure with Python 3.13.

1 0

Spot 2.12.1 released
by Alexandre Duret-Lutz 23 Sep '24

23 Sep '24

We are happy to announce the release of Spot 2.12.1 This is a minor release containing fixes for several unimportant bugs; if 2.12 already works for you, it is safe to skip this upgrade. You can find the new release here: https://www.lre.epita.fr/dload/spot/spot-2.12.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 an issue at https://gitlab.lre.epita.fr/spot/spot/-/issues/new ---------- New in spot 2.12.1 (2024-09-23) Bug fixes: - Generating random formula without any unary opertors would very often create formulas much smaller than asked. - The parity game solver, which internally works on "parity max odd", but actually accept any type of parity acceptance, could be confused by games with "parity min" acceptance using transition with several colors (a rather uncommon situation). - "ltlsynt ... --print-game --dot=ARGS" was ignoring ARGS. - Work around various warnings from g++14. - Improved handling of spot-extra/ directory with newer Swig versions. Necessary to recompile Seminator 2 with Swig 4.

1 0

Spot 2.12 has been released
by Alexandre Duret-Lutz 16 May '24

16 May '24

We are happy to announce the release of Spot 2.12 This is a long-awaited major release containing new features developed in the last 17 months (since the release of Spot 2.11), as well as fixes for bugs discovered in the last 9 months (since Spot 2.11.6). Some of these bug fixes are necessary for Spot to work correctly with newer versions of Python, GCC, or Jupyter. This release contains contributions by Philipp Schlehuber, Florian Renkin, Jonah Romero, Pierre Ganty, 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.lrde.epita.fr/dload/spot/spot-2.12.tar.gz See https://spot.lre.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. ⚠ Note that LRDE (EPITA's Research & Development Laboratory) has been merged with another entity into something larger that is now called LRE (EPITA's Research Laboratory). However, it will be a while before we are able to replace all URLs ending in "lrde.epita.fr" by URLs ending "lrde.epita.fr", so do not be surprized about the mix of those. New in spot 2.12 (2024-05-16) Build: - When Python bindings are enabled, Spot now requires Python 3.6 or later. Python 3.6 has reached end-of-life in 2021, but is still used on CentOS 7 (which will reach end-of-support later in 2024). Documentation: - https://spot.lre.epita.fr/tut25.html is a new example showing how to print an automaton in the "BA format" (used by Rabbit and other tools). Command-line tools: - In places that accept format strings with '%' sequences, like options --stats, --name, or --output, the new '%l' can now be used to produce the 0-based serial number of the produced object. This differs from the existing '%L' that is usually related to the line number of the input (when that makes sense). For instance to split a file that contains many automata into one file per automaton, do autfilt input.hoa -o output-%l.hoa - For tools that produce automata, using -Hb or --hoa=b will produce an HOA file in which aliases are used to form a basis for the whole set of labels. Those aliases are only used when more than one atomic proposition is used (otherwise, the atomic proposition and its negation is already a basis). This can help reduce the size of large HOA files. - autfilt learned --separate-edges, to split the labels of the automaton using a basis of disjoint labels. See https://spot.lre.epita.fr/tut25.html for some motivation. - autfilt learned --reduce-acceptance-set/--enlarge-acceptance-set to heurisitcally remove/add to unnecessary acceptance marks in Büchi automata. (Issue #570) - ltlfilt has a new option --relabel-overlapping-bool=abc|pnn that will replace boolean subformulas by fresh atomic propositions even if those subformulas share atomic propositions. - ltlsynt's --ins and --outs options will iterpret any atomic proposition surrounded by '/' as a regular expression. For intance with ltlsynt --ins='/^in/,/env/' --outs=/^out/,/control/' ... any atomic proposition that starts with 'in' or contains 'env' will be considered as input, and one that starts with 'out' or contain 'control' will be considered output. By default, if neither --ins nor --outs is given, ltlsynt will behave as if --ins='/^[iI]/' and --outs='/^[oO]/ were used. - ltlsynt will now check for atomic propositions that always have the same polarity in the specification. When this happens, these output APs are replaced by true or false before running the synthesis pipeline, and the resulting game, Mealy machine, or Aiger circuit is eventually patched to include that constant output. This can be disabled with --polarity=no. - ltlsynt will now check for atomic propositions that are specified as equivalent. When this is detected, equivalent atomic propositions are replaced by one representative of their class, to limit the number of different APs processed by the synthesis pipeline. The resulting game, Mealy machine, or Aiger circuit is eventually patched to include the removed APs. This optimization can be disabled with --global-equivalence=no. As an exception, an equivalence between input and output signals (such as G(in<->out)) will be ignored if ltlsynt is configured to output a game (because patching the game a posteriori is cumbersome if the equivalence concerns different players). - genaut learned two new familes of automata, --cycle-log-nba and --cycle-onehot-nba. They both create a cycle of n^2 states that can be reduced to a cycle of n states using reduction based on direct simulation. Library: - The following new trivial simplifications have been implemented for SEREs: - f|[+] = [+] if f rejects [*0] - f|[*] = [*] if f accepts [*0] - f&&[+] = f if f rejects [*0] - b:b[*i..j] = b[*max(i,1)..j] - b[*i..j]:b[*k..l] = b[*max(i,1)+max(k,1)-1, j+l-1] - The following new trivial simplifications have been implemented for PSL operators: - {[*]}[]->0 = 0 - {[*]}<>->1 = 1 - The HOA parser is a bit smarter when merging multiple initial states into a single initial state (Spot's automaton class supports only one): it now reuses the edges leaving initial states without incoming transitions. - The automaton parser has a new option "drop_false_edges" to specify whether edges labeled by "false" should be ignored during parsing. It is enabled by default for backward compatibility. - spot::bdd_to_cnf_formula() is a new variant of spot::bdd_to_formula() that converts a BDD into a CNF instead of a DNF. - spot::relabel_bse() has been improved to better deal with more cases. For instance '(a & b & c) U (!c & d & e)' is now correctly reduced as '(p0 & p1) U (!p1 & p2)', and '((a & !b) | (a->b)) U c' now becomes '1 U c'. (Issue #540.) - spot::relabel_overlapping_bse() is a new function that will replace boolean subformulas by fresh atomic propositions even if those subformulas share atomic propositions. - spot::translate() has a new -x option "relabel-overlap=M" that augments the existing "relabel-bool=N". By default, N=4, M=8. When the formula to translate has more than N atomic propositions, relabel_bse() is first called to attempt to rename non-overlapping boolean subexpressions (i.e., no shared atomic proposition) in order to reduce the number of atomic proposition, a source of exponential explosion in several places of the translation pipeline. This relabel-bool optimization exists since Spot 2.4. The new feature is that if, after relabel-bool, the formula still has more than M atomic propositions, then spot::translate() now attempts to relabel boolean subexpressions even if they have overlapping atomic propositions, in an attempt to reduce the number of atomic proposition even more. Doing so has the slightly unfortunate side effect of hindering some simplifications (because the new atomic propositions hide their interactions), but it usually incures a large speedup. (See Issue #500, Issue #536.) For instance on Alexandre's laptop, running 'ltlsynt --tlsf SPIReadManag.tlsf --aiger' with Spot 2.11.6 used to produce an AIG circuit with 48 nodes in 36 seconds; it now produces an AIG circuit with 53 nodes in only 0.1 second. - spot::contains_forq() is an implementation of the paper "FORQ-Based Language Inclusion Formal Testing" (Doveri, Ganty, Mazzocchi; CAV'22) contributed by Jonah Romero. - spot::contains() still defaults to the complementation-based algorithm, however by calling spot::containment_select_version("forq") or by setting SPOT_CONTAINMENT_CHECK=forq in the environment, the spot::contains_forq() implementation will be used instead when applicable (inclusion between Büchi automata). The above also impacts autfilt's --included-in option. - spot::reduce_buchi_acceptance_set_here() and spot::enlarge_buchi_acceptance_set_here() will heuristically remove/add unnecessary acceptance marks in Büchi automata. (Issue #570.) - Given a twa_word_ptr W and a twa_ptr A both sharing the same alphabet, one can now write W->intersects(A) or A->intersects(W) instead of the longuer W->as_automaton()->intersects(A) or A->intersects(W->as_automaton()). - spot::scc_info has a new option PROCESS_UNREACHABLE_STATES that causes it to enumerate even unreachable SCCs. - spot::realizability_simplifier is a new class that performs the removal of superfluous APs that is now performed by ltlsynt (search for --polarity and --global-equivalence above). - scc_filter used to reduce automata tagged with the inherently-weak property to weak Büchi automata (unless the acceptance was already t or co-Büchi). In cases where the input automaton had no rejecting cycle, the Büchi acceptance was overkill: scc_filter will now use "t" acceptance. This change may have unexpected consequences in code paths that assume running scc_filter on a Büchi automaton will always return a Büchi automaton. For those, a "keep_one_color" option has been added to scc_filter. - spot::separate_edges() and spot::edge_separator offers more ways to split labels. See https://spot.lrde.epita.fr/ipynb/split.html - ltsmin's interface will now point to README.ltsmin in case an error is found while running divine or spins. - spot::is_safety_automaton() was generalized to detect any automaton for which the acceptance could be changed to "t" without changing the language. In previous versions this function assumed weak automata as input, but the documentation did not reflect this. - spot::remove_alternation() has a new argument to decide whether it should raise an exception or return nullptr if it requires more acceptance sets than supported. - spot::dualize() learned a trick to be faster on states that have less outgoing edges than atomic proposition declared on the automaton. spot::remove_alternation(), spot::tgba_powerset(), simulation-based reductions, and spot::tgba_determinize() learned a similar trick, except it isn't applied at the state level but if the entire automaton uses few distinct labels. These changes may speed up the processing of automata with many atomic propositions but few distinct labels. (Issue #566 and issue #568.) Backward incompatibilities: - spot::dualize() does not call cleanup_acceptance() anymore. This change ensures that the dual of a Büchi automaton will always be a co-Büchi automaton. Previously cleanup_acceptance(), which remove unused colors from the acceptance, was sometimes able to simplify co-Büchi to "t", causing surprizes. - Function minimize_obligation_garanteed_to_work() was renamed to minimize_obligation_guaranteed_to_work(). We believe this function is only used by Spot currently. - Function split_independant_formulas() was renamed to split_independent_formulas(). We believe this function is only used by Spot currently. Python: - The spot.automata() and spot.automaton() functions now accept a drop_false_edges=False argument to disable the historical behavior of ignoring edges labeled by False. - Calling aut.highlight_state(s, None) or aut.highlight_edge(e, None) may now be used to remove the highlighting color of some given state or edge. Use aut.remove_highlight_states() or aut.remove_highlight_edges() to remove all colors. (Issue #554.) - Calling aut.get_hight_state(s) or get.highlight_edge(e) will return the highlight color of that state/edge or None. - Recent version Jupyter Notebook and Jupyter Lab started to render SVG elements using <img...> tag to make it easier to copy/paste those images. This breaks several usages, including the possibility to have informative tooltips on states and edges (used in Spot). See the following issues for more details. https://github.com/jupyter/notebook/issues/7114 https://github.com/jupyterlab/jupyterlab/issues/10464 This version of Spot now declares its svg outputs as HTML to prevent Jypyter from wrapping them is images. Bugs fixed: - tgba_determinize()'s use_simulation option would cause it to segfault on automata with more than 2^16 SCCs, due to overflows in computations of indices in the reachability matrix for SCCs. (Issue #541.) This has been fixed by disabling the use_simulation optimization in this case. - product_or_susp() and product_susp() would behave incorrectly in presence of unsatisifable or universal acceptance conditions that were not f or t. (Part of issue #546.) - Several algorithms were incorrectly dealing with the "!weak" property. Because they (rightly) assumed that a weak input would produce a weak output, they also wrongly assumed that a non-weak output would produce a non-weak output. Unfortunately removing states or edges in a non-weak automaton can lead a weak automaton. The incorrect property lead to issue #546. In addition to fixing several algorithms, product() and print_hoa() will now raise an exception if automaton with t or f acceptance is declared !weak. (This cheap check will not catch all automata incorrectly labeled by !weak, but helps detects some issues nonetheless.) - The automaton parser forgot to update the list of highlighted edges while dropping edges labeled by bddfalse. (issue #548.) - The comparison operators for acceptance condition (==, !=) could fail to equate two "t" condition, because we have two ways to represent "t": the empty condition, or the empty "Inf({})". - Functions complement() and change_parity() could incorrectly read or write the unused edge #0. In the case of complement(), writing that edge was usually harmless. However, in some scenario, complement could need to stick a ⓪ acceptance mark on edge #0, then the acceptance condition could be simplified to "t", and finally change_parity could be confused to find such an accepting mark in an automaton that declares no colors, and perform some computation on that color that caused it to crash with a "Too many acceptance sets used" message. (issue #552) - The detection of terminal automata used did not exactly match the definition used in the HOA format. The definition of a terminal automaton is supposed to be: 1. the automaton is weak 2. its accepting SCCs are complete 3. no accepting cycle can reach a rejecting cycle However the implementation actually replaced the last point by the following variant: 3'. no accepting edge can reach a rejecting cycle This caused issues in automata with t acceptance. Fixing the code by replacing 3' by 3 this also made the third argument of is_terminal_automaton(), an optional boolean indicating whether transition between SCCs should be ignored when computing 3', completely obsolete. This third argument has been marked as depreated. (Issue #553) - twa::defrag_states(), which is called for instance by purge_dead_state(), did not update the highlight-edges property. (Issue #555.) - spot::minimize_obligation will skip attempts to complement very weak automata when those would require too many acceptance sets. - acd_transform() was not used by spot::postprocessor unless an option_map was passed. This was due to some bad default for the "acd" option: it defaulted to true when an option_map was given, and to false otherwise. This had no consequences on ltl2tgba/autfilt were some option_map is always passed, but for instance the parity automata generated by spot.postprocessor in Python were not using ACD by default. - Using spot::postprocessor to produce colored parity automata could fail to color some transiant edges when the "acd" option was activated. - The formula printer incorrectly replaced a SERE like "(!a)[*3];a" by "a[->]". The latter should only replace "(!a)[*];a". (Issue #559.) - The configure script failed to detect the include path for Python 3.12. (Issue #577.) - Work around many failures caused by incorrect rounding of floating point values in the counting of transitions. (Issue #582) - Some incorrectly escaped strings in Python code were causing warnings with Python 3.12.

1 0

Spot 2.11.6 released
by Alexandre Duret-Lutz 02 Aug '23

02 Aug '23

We are happy to announce the release of Spot 2.11.6. This is a maintenance release containing several fixes for bugs that have been discovered since 2.11.5. This include a fix for a 20-year old typo in the modified version of BuDDy that we ship with Spot. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.11.6.tar.gz See https://spot.lre.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. ⚠ Note that LRDE (EPITA's Research & Development Laboratory) has been merged with another entity into something larger that is now called LRE (EPITA's Research Laboratory). It will be a while before we are able to replace all URLs ending in "lrde.epita.fr" by URLs ending "lre.epita.fr", so do not be surprized about the mix of those. New in spot 2.11.6 (2023-08-01) Bug fixes: - Running command lines such as "autfilt input.hoa -o output-%L.hoa" where thousands of different filenames can be created failed with "Too many open files". (Issue #534) - Using --format=... on a tool that output formulas would force the output on standard output, even when --output was given. - Using "randltl -S" did not correctly go through the SERE printer functions. - Our copy of BuDDy's bdd_forall() had a 20 year old typo that caused cache entries from bdd_exist() and bdd_forall() to be mixed. Spot was safe from this bug because it was only using bdd_exist(). (Issue #535) - Work around recent Pandas and GCC changes.

1 0

Spot 2.11.5 released
by Alexandre Duret-Lutz 20 Apr '23

20 Apr '23

We are happy to announce the release of Spot 2.11.5 Spot 2.11.5 is a maintenance release that fixes a handful of issues that were discovered or reported over the last two months. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.11.5.tar.gz See https://spot.lre.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. ⚠ Note that LRDE (EPITA's Research & Development Laboratory) has been merged with another entity into something larger that is now called LRE (EPITA's Research Laboratory). The removal of "development", is nothing to worry about: we are still continuing to develop Spot as part of our research. However it will be a while before we are able to replace all URLs ending in "lrde.epita.fr" by URLs ending "lrde.epita.fr", so do not be surprized about the mix of those. New in spot 2.11.5 (2023-04-20) Bug fixes: - Fix spurious failure of ltlsynt2.test when Python is not installed (issue #530). - Building from the git repository would fail to report a missing emacs (issue #528). - Fix exception raised by aut1.intersecting_run(aut2).as_twa() because the run did not match transitions present in aut1 verbatim. We also changed the behavior of as_twa() to not merge identical states. - Fix segfaults occuring in determinization of 1-state terminal automata. - Fix incorrect assertion in game solver when the edge vector contains deleted transitions.

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot-announce