- Spot-announce

Spot 2.14.3 released
by Alexandre Duret-Lutz 11 Nov '25

11 Nov '25

We are happy to announce the release of Spot 2.14.3 This is a maintenance realease that fixes minor compatibility issues and bugs. You can find the new release here: http://www.lre.epita.fr/dload/spot/spot-2.14.3.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.3 (2025-11-11) Bugs fixed: - Spot's Python bindings used to map spot::parse_error exceptions into Python's SyntaxError exception. However, recent ipython versions have a handling of SyntaxError that really assume a SyntaxError in Python, not an error comming from some third-party parser reading some third-party format... That spot::parse_error exceptions are now raised as instances of spot.parse_error. (Issue #617.) - Swig 4.4, released recently, contains a proper fix to Issue #603. However, that new version also requires some update in Spot's code. While this Spot release preserves compatibility with earlier Swig versions, it is the first to be compatible with Swig 4.4. - ltlf2dfa --mtdfa-stats had a bug where if "false" was the only constant used, it would be reported as "true". - ltlf_to_mtdfa_compose() would sometimes keep the name of states even when instructed to discard them. - Fix several "unnecessary virtual specifiers" reported by newer versions of Clang. - Many typos and documentation improvements.

1 0

Spot 2.14.2 released
by Alexandre Duret-Lutz 18 Sep '25

18 Sep '25

We are happy to announce the release of Spot 2.14.2 This is a minor realease that addresses a few bugs and improve the documentation. You can find the new release here: http://www.lre.epita.fr/dload/spot/spot-2.14.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.14.2 (2025-09-18) Library: - BuDDy's implementation of bdd_mt_apply1_synthesis() and bdd_mt_apply1_synthesis_with_choice() used by ltlfsynt, got some small improvements resulting in smaller strategies being generated. (Issue #611.) Documentation: - https://www.lre.epita.fr/tlsf.html is a new page discussing how the --tlsf option of ltlsynt/ltlfsynt/ltlf2dfa uses syfco to transform TLSF into LTL/LTLf. - https://www.lre.epita.fr/tut60.html shows two examples of integration with ppLTLTT to handle some pure-past LTL sub-formulas. Bug fixes: - twadfa_to_mtdfa(aut) was not properly registering the atomic proposition of aut into the resulting MTDFA. - The part of the HOA parser responsible for dealing with multiple initial states (a feature of the HOA format that Spot does not support internally) had a bug if the last state of the set of initial state without incoming edges also had no outgoing edges. - spot::mtdfa_strategy_to_mealy() now has an option to produce a strategy that stutter on accepance. This gets rid of the accepting sink, and this is also necessary for the correctness of the produced controller in some decomposition cases. (Issue #610)

1 0

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

Spot 2.11.4 released
by Alexandre Duret-Lutz 10 Feb '23

10 Feb '23

We are happy to announce the release of Spot 2.11.4 Spot 2.11.4 fix a couple of issues discovered in the last two months. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.11.4.tar.gz See https://spot.lrde.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) had 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 a consequence is that this release contains a mix of URLs in "lre.epita.fr" (for services that have already migrated to the new name) and "lrde.epita.fr". If you find a URL ending in "lrde.epita.fr" that does not work, please try without the "d". New in spot 2.11.4 (2023-02-10) Python: - spot.acd() no longer depends on jQuery for interactivity. Bug fixes: - When merging initial states from state-based automata with multiple initial states (because Spot supports only one), the HOA parser could break state-based acceptance. (Issue #522.) - autfilt --highlight-word refused to work on automata with Fin acceptance for historical reasons, however the code has been perfectly able to handle this for a while. (Issue #523.) - delay_branching_here(), a new optimization of Spot 2.11, had an incorrect handling of states without successors, causing some segfaults. (Issue #524.) - Running delay_branching_here() on state-based automata (this was not done in Spot so far) may require the output to use transition-based acceptance. (Issue #525.) - to_finite(), introduced in 2.11, had a bug that could break the completeness of automata and trigger an exception from the HOA printer. (Issue #526.)

1 0

Spot 2.11.3 released
by Alexandre Duret-Lutz 09 Dec '22

09 Dec '22

We are happy to announce the release of Spot 2.11.3. This is a maintenance release that fixes bugs discovered after we released 2.11.2. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.11.3.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 a consequence is that this release contains a mix of URLs in "lre.epita.fr" (for services that have already migrated to the new name) and "lrde.epita.fr". If you find a URL ending in "lrde.epita.fr" that does not work, please try without the "d". New in spot 2.11.3 (2022-12-09) Bug fixes: - Automata-based implication checks, used to simplify formulas, were slower than necessary because the translator was configured to favor determinism unnecessarily. (Issue #521.) - Automata-based implication checks for f&g and f|g could be very slow when those n-ary operator had two many arguments. They have been limited to 16 operands, but this value can be changed with option -x tls-max-ops=N. (Issue #521 too.) - Running ltl_to_tgba_fm() with an output_aborter (which is done during automata-based implication checks) would leak memory on abort. - configure --with-pythondir should also redefine pyexecdir, otherwise, libraries get installed in the wrong place on Debian. (Issue #512.) - The HOA parser used to silently declare unused and undefined states (e.g., when the State: header declare many more states than the body of the file). It now warns about those. - 'autfilt -c ...' should display a match count even in presence of parse errors. - Calling solve_parity_game() multiple times on the same automaton used to append the new strategy to the existing one instead of overwriting it.

1 0

Spot 2.11.2 has been released
by Alexandre Duret-Lutz 26 Oct '22

26 Oct '22

We are happy to announce the release of Spot 2.11.2 Spot 2.11.2 fix a couple of issues, and also add a few simple features that have been requested since 2.11.1. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.11.2.tar.gz See https://spot.lrde.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) had 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 a consequence is that this release contains a mix of URLs in "lre.epita.fr" (for services that have already migrated to the new name) and "lrde.epita.fr". If you find a URL ending in "lrde.epita.fr" that does not work, please try without the "d". New in spot 2.11.2 (2022-10-26) Command-line tools: - The --stats specifications %s, %e, %t for printing the number of (reachable) states, edges, and transitions, learned to support options [r], [u], [a] to indicate if only reachable, unreachable, or all elements should be counted. Library: - spot::reduce_parity() now has a "layered" option to force all transition in the same parity layer to receive the same color; like acd_transform() would do. Bugs fixed: - Fix pkg-config files containing @LIBSPOT_PTHREAD@ (issue #520) - spot::relabel_bse() was incorrectly relabeling some dependent Boolean subexpressions in SERE. (Note that this had no consequence on automata translated from those SERE.)

1 0

Spot 2.11.1 released
by Alexandre Duret-Lutz 10 Oct '22

10 Oct '22

We are happy to announce the release of Spot 2.11.1 Spot 2.11 is a major release containing new feature and improvements implemented over the last 11 months by Florian Rankin, Philipp Schlehuber-Caissier, Antoine Martin, and myself. A detailled list of changes is appended to this email. Spot 2.11.1 fixes a couple of build issues discovered before I had time to announce 2.11... You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.11.1.tar.gz See https://spot.lrde.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) had 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 a consequence is that this release contains a mix of URLs in "lre.epita.fr" (for services that have already migrated to the new name) and "lrde.epita.fr". If you find a URL ending in "lrde.epita.fr" that does not work, please try without the "d". New in spot 2.11.1 (2022-10-10) Bugs fixed: - Fix a build issue preventing the update of website (issue #516). - Fix a compilation error with clang-14 on FreeBSD (issue #515). New in spot 2.11 (2022-10-08) Build: - configure will now diagnose situations where Python bindings will be installed in a directory that is not part of Python's search path. A new configure option --with-pythondir can be used to modify this installation path. (Issue #512) - A new configure option --enable-pthread enables the compilation of Spot with -pthread, and render available the parallel version of some algorithms. If Spot is compiled with -pthread enabled, any user linking with Spot should also link with the pthread library. In order to not break existing build setups using Spot, this option is currently disabled by default in this release. We plan to turn it on by default in some future release. Third-party project using Spot may want to start linking with -pthread in prevision for this change. Command-line tools: - autfilt has a new options --aliases=drop|keep to specify if the HOA printer should attempt to preserve aliases present in the HOA input. This defaults to "keep". - autfilt has a new --to-finite option, illustrated on https://spot.lrde.epita.fr/tut12.html - ltlfilt has a new --sonf option to produce a formula's Suffix Operator Normal Form, described in [cimatti.06.fmcad]. The associated option --sonf-aps allows listing the newly introduced atomic propositions. - autcross learned a --language-complemented option to assist in the case one is testing tools that complement automata. (issue #504). - ltlsynt has a new option --tlsf that takes the filename of a TLSF specification and calls syfco (which must be installed) to convert it into an LTL formula. - ltlsynt has a new option --from-pgame that takes a parity game in extended HOA format, as used in the Synthesis Competition. - ltlsynt has a new option --hide-status to hide the REALIZABLE or UNREALIZABLE output expected by SYNTCOMP. (This line is superfluous, because the exit status of ltlsynt already indicate whether the formula is realizable or not.) - ltlsynt has a new option --dot to request GraphViz output instead of most output. This works for displaying Mealy machines, games, or AIG circuits. See https://spot.lrde.epita.fr/ltlsynt.html for examples. - genaut learned the --cyclist-trace-nba and --cyclist-proof-dba options. Those are used to generate pairs of automata that should include each other, and are used to show a regression (in speed) present in Spot 2.10.x and fixed in 2.11. - genltl learned --eil-gsi to generate a familly a function whose translation and simplification used to be very slow. In particular genltl --eil-gsi=23 | ltlfilt --from-ltlf | ltl2tgba was reported as taking 9 days. This is now instantaneous. Library: - The new function suffix_operator_normal_form() implements transformation of formulas to Suffix Operator Normal Form, described in [cimatti.06.fmcad]. - "original-classes" is a new named property similar to "original-states". It maps an each state to an unsigned integer such that if two classes are in the same class, they are expected to recognize the same language. The "original-states" should be prefered property when that integer correspond to some actual state. - tgba_determinize() learned to fill the "original-classes" property. States of the determinized automaton that correspond to the same subset of states of the original automaton belong to the same class. Filling this property is only done on demand as it inccurs a small overhead. - sbacc() learned to take the "original-classes" property into account and to preserve it. - The HOA parser and printer learned to map the synthesis-outputs property of Spot to the controllable-AP header for the Extended HOA format used in SyntComp. https://arxiv.org/abs/1912.05793 - The automaton parser learned to parse games in the PGSolver format. See the bottom of https://spot.lrde.epita.fr/ipynb/games.html for an example. - "aliases" is a new named property that is filled by the HOA parser using the list of aliases declared in the HOA file, and then used by the HOA printer on a best-effort basis. Aliases can be used to make HOA files more compact or more readable. But another possible application is to use aliases to name letters of a 2^AP alphabet, in applications where using atomic propositions is inconvenient. - print_dot() learned option "@" to display aliases, as discussed above. - to_finite() is a new function that help interpreting automata build from LTLf formula using the from_ltlf() function. It replace the previously suggested method of removing and atomic proposition and simpifying automata, that failed to deal with states without successors. See updated https://spot.lrde.epita.fr/tut12.html - the HOA parser learned to not ignore self-loops labeled with [f] and to turn any state that have colors but no outgoing transitions into a state with a [f] self-loop. This helps dealing with automata containing states without successors, as in the output of to_finite(). - purge_dead_states() will now also remove edges labeled by false (except self-loops). - When parsing formulas with a huge number of operands for an n-ary operator (for instance 'p1 | p2 | ... | p1000') the LTL parser would construct that formula two operand at a time, and the formula constructor for that operator would be responsible for inlining, sorting, deduplicating, ... all operands at each step. This resulted in a worst-than-quadratic slowdown. This is now averted in the parser by delaying the construction of such n-ary nodes until all children are known. - complement() used to always turn tautological acceptance conditions into Büchi. It now only does that if the automaton is modified. - The zielonka_tree construction was optimized using the same memoization trick that is used in ACD. Additionally it can now be run with additional options to abort when the tree as an unwanted shape, or to turn the tree into a DAG. - contains() can now take a twa as a second argument, not just a twa_graph. This allows for instance to do contains(ltl, kripke) to obtain a simple model checker (that returns true or false, without counterexample). - degeneralize() and degeneralize_tba() learned to work on generalized-co-Büchi as well. - product() learned that the product of two co-Büchi automata is a co-Büchi automaton. And product_or() learned that the "or"-product of two Büchi automata is a Büchi automaton. - spot::postprocessor has a new extra option "merge-states-min" that indicates above how many states twa_graph::merge_states() (which perform a very cheap pass to fuse states with identicall succesors) should be called before running simulation-based reductions. - A new function delay_branching_here(aut) can be used to simplify some non-deterministic branching. If two transitions (q₁,ℓ,M,q₂) and (q₁,ℓ,M,q₃) differ only by their destination state, and are the only incoming transitions of their destination states, then q₂ and q₃ can be merged (taking the union of their outgoing transitions). This is cheap function is automatically called by spot::translate() after translation of a formula to GBA, before further simplification. This was introduced to help with automata produced from formulas output by "genltl --eil-gsi" (see above). - spot::postprocessor has new configuration variable branch-post that can be used to control the use of branching-postponement (disabled by default) or delayed-branching (see above, enabled by default). See the spot-x(7) man page for details. - spot::postprocessor is now using acd_transform() by default when building parity automata. Setting option "acd=0" will revert to using "to_parity()" instead. - to_parity() has been almost entirely rewritten and is a bit faster. - When asked to build parity automata, spot::translator is now more aggressively using LTL decomposition, as done in the Generic acceptance case before paritizing the result. This results in much smaller automata in many cases. - spot::parallel_policy is an object that can be passed to some algorithm to specify how many threads can be used if Spot has been compiled with --enable-pthread. Currently, only twa_graph::merge_states() supports it. Python bindings: - The to_str() method of automata can now export a parity game into the PG-Solver format by passing option 'pg'. See https://spot.lrde.epita.fr/ipynb/games.html for an example. Deprectation notice: - spot::pg_print() has been deprecated in favor of spot::print_pg() for consistency with the rest of the API. Bugs fixed: - calling twa_graph::new_univ_edge(src, begin, end, cond, acc) could produce unexpected result if begin and end where already pointing into the universal edge vector, since the later can be reallocated during that process. - Printing an alternating automaton with print_dot() using 'u' to hide true state could produce some incorrect GraphViz output if the automaton as a true state as part of a universal group. - Due to an optimization introduces in 2.10 to parse HOA label more efficiently, the automaton parser could crash when parsing random input (not HOA) containing '[' (issue #509).

1 0

Spot 2.10.6 released
by Alexandre Duret-Lutz 18 May '22

18 May '22

We are happy to announce the release of Spot 2.10.6 This is a maintenance release fixing an couple of bugs reported or discovered over the last two weeks. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.10.6.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.10.6 (2022-05-18) Bugs fixed: - Fix compilation error on MacOS X. - Using -Ffile/N to read column N of a CSV file would not reset the /N specification for the next file. - make_twa_graph() will now preserve state numbers when copying a kripke_graph object. As a consequence, print_dot() and print_hoa() will now use state numbers matching those of the kripke_graph (issue #505). - Fix several compilation warning introduced by newer versions of GCC and Clang.

1 0

Spot 2.10.5 released
by Alexandre Duret-Lutz 03 May '22

03 May '22

We are happy to announce the release of Spot 2.10.5 This is a maintenance release fixing an assortment of minor bugs discovered over the last three months. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.10.5.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. (The spot web site is not yet updated to point to 2.10.5, but that should be fixed in the next days.) Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.10.5 (2022-05-03) Bugs fixed: - reduce_parity() produced incorrect results when applied to automata with deleted edges. - An optimization of Zielonka could result in incorrect results in some cases. - ltlsynt --print-pg incorrectly solved the game in addition to printing it. - ltlsynt would fail if only one of --ins or --outs was set, and if it was set empty. - Work around a portability issue in Flex 2.6.4 preventing compilation on OpenBSD. - Do not use the seq command in test cases, it is not available everywhere. - Do not erase the previous contents of the PYTHONPATH environment variable when running tests, prepend to it instead. - Simplify Debian instructions for LTO build to work around newer libtool version. - Fix invalid read in digraph::sort_edges_of_(), currently unused in Spot.

1 0

Spot 2.10.4 released
by Alexandre Duret-Lutz 02 Feb '22

02 Feb '22

We are happy to announce the release of Spot 2.10.4 This is a maintenance release fixing some very old memory leaks discovered in the Python bindings. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.10.4.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.10.4 (2022-02-01) Bug fixed: - Fix memory leaks in Python bindings for several iteration objects. This occured while itering on twa_graph.out(), twa_graph.edges(), twa_graph.univ_dests(), kripke_graph.out(), kripke_graph.edges(), mark_t.sets(), scc_info.edges_of(), scc_info.inner_edges_of(), and on an scc_info instance.

1 0

Spot 2.10.3 released
by Alexandre Duret-Lutz 17 Jan '22

17 Jan '22

We are happy to announce the release of Spot 2.10.3 This is a maintenance release fixing a few bugs discovered since the last release. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.10.3.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr> New in spot 2.10.3 (2022-01-15) Bugs fixed: - On automata where the absence of color is not rejecting (e.g. co-Büchi) and where the initial state was in a rejecting SCC, sbacc() could output a superfluous state. (Issue #492) - Compared to 2.9.8, complement() (and many functions using it) was slower and produced larger outputs on some automata with more than 32 states due to an optimization of the determinization being unintentionally disabled. - The split_2step() function used to create a synthesis game could complain that it was unable to complement a monitor (Issue #495). - Work around GraphViz bug #2179 by avoiding unnecessary empty lines in the acceptance conditions shown in dot. - Fix a case where generic_accepting_run() incorrectly returns a cycle around a rejecting self-loop. - Mealy machines resulting from SAT-based minimization could differ on architectures with different hash tables implementations. - org-mode moved to GNU ELPA (Issue #496).

1 0

Spot 2.10.2 released
by Alexandre Duret-Lutz 03 Dec '21

03 Dec '21

We are happy to announce the release of Spot 2.10.2 This is a maintenance release fixing a few bugs discovered over the last two weeks. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.10.2.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.10.2 (2021-12-03) Bugs fixed: - twa_graph::purge_dead_states() now also removes edges labeled by bddfalse. - only use sched_getcpu() and pthread_setaffinity_np() when they are available. - Using ##300 in a SERE will report that the repeatition exceeds the allowed value using a parse error, not as an exception. - spot::formula::is_literal() should be const.

1 0

Spot 2.10.1 released
by Alexandre Duret-Lutz 19 Nov '21

19 Nov '21

We are happy to announce the release of Spot 2.10.1 This is a maintenance release fixing a few bug discovered right after the release for Spot 2.10 last week. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.10.1.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.10.1 (2021-11-19) Build: - Python 3.5 or later is now required (unless Python bindings are disabled). Python 3.5 reached end-of-life one year ago, so we believe support for older versions of Python will not be missed. Library: - The sbacc() function now defines the "original-states" property, allowing to map an output state back to its input. Bugs fixed: - Ranged repetition operators from LTL/PSL, like [*a..b], [->a..b] or even F[a..b] used to store and handle a and b as 8-bit values without overflow checks. So for instance {a[*260];b} was silently interpreted as {a[*4];b} This version still restricts those bounds to 8 bits, but now diagnose overflow checks while parsing and constructing formulas. Also the so called "trivial simplification rules" will not be applied in case they would lead to an overflow. For instance {a;[*150];[*50];b} is rewritten to {a;[*200];b} but {a;[*150];[*150];b} is untouched. - Fix a compilation error on system with glibc older than 2.18, where <inttypes.h> does not define some C99 macro by default when compiled in C++ mode. (Such old libraries are used when compiling packages for conda-forge, which use CentOS 6 as building environment.) - Fix a link error of tests/ltsmin/modelcheck not finding BDD functions on some systems (observed on CentOS 6 again). - Fix spurious test-suite failures under newer Jupyter installations. IPykernel 6.0 now captures stdout/stderr from subprocesses and displays them in the notebook. The spot.ltsmin code that loads modules compiled with SpinS had to be rewritten to capture and display the output of SpinS, so that our test-cases can be reproduced regardless of the IPykernel version. This fix was easier to do in Python 3.5. - Fix sevaral minor documentation errors.

1 0

Spot 2.10 released
by Alexandre Duret-Lutz 14 Nov '21

14 Nov '21

We are happy to announce the release of Spot 2.10 This is a major release that has been under development for 19 months. It contains new features contributed by Jérôme Dubois, Antoine Martin, Étienne Renault, Florian Renkin, Philipp Schlehuber, and myself. A summary of those 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.10.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.10 (2021-11-13) Build: - Spot is now built in C++17 mode, so you need at least GCC 7 or clang 5 to compile it. The current versions of all major linux distributions ship with at least GCC 7.4, so this should not be a problem. There is also an --enable-c++20 option to configure in case you want to force a build of Spot in C++20 mode. Command-line tools: - ltlsynt has been seriously overhauled, while trying to preserve backward compatibility. Below is just a summary of the main user-visible changes. Most of the new options are discussed on https://spot-dev.lrde.epita.fr/ltlsynt.html + ltlsynt now accepts only one of the --ins or --outs options to be given and will deduce the value of the other one. + ltlsynt learned --print-game-hoa to output its internal parity game in the HOA format (with an extension described below). + ltlsynt --aiger option now takes an optional argument indicating how the bdd and states are to be encoded in the aiger output. The option has to be given in the form ite|isop|both[+ud][+dc][+sub0|sub1|sub2] where the first only obligatory argument decides whether "if-then-else" ("ite") or irreducible-sum-of-products ("isop") is to be used. "both" executes both strategies and retains the smaller circuits. The additional options are for fine-tuning. "ud" also encodes the dual of the conditions and retains the smaller circuits. "dc" computes if for some inputs we do not care whether the output is high or low and try to use this information to compute a smaller circuit. "subX" indicates different strategies to find common subexpressions, with "sub0" indicating no extra computations. + ltlsynt learned --verify to check the computed strategy or aiger circuit against the specification. + ltlsynt now has a --decompose=yes|no option to specify if the specification should be decomposed into independent sub-specifications, the controllers of which can then be glued together to satisfy the input specification. (cf. [finkbeiner.21.nfm] in doc/spot.bib) + ltlsynt learned --simplify=no|bisim|bwoa|sat|bisim-sat|bwoa-sat to specifies how to simplify the synthesized controler. - ltl2tgba, autfilt, dstar2tgba, and randaut learned a --buchi option, or -b for short. This outputs Büchi automata without forcing state-based acceptance. The following aliases have also been added for consistency: --gba is an alias for --tgba, because the "t" of --tgba is never forced. --sba is an alias for -B/--ba, because -B really implies -S and that is not clear from --ba. As a consequence of the introduction of --sba, the option --sbacc (an alias for --state-based-acceptance) cannot be abbreviated as --sba anymore. - autfilt learned a --kill-states=NUM[,NUM...] option. - ltlcross, autcross, ltldo have learned shorthands for the commands of Owl 21.0. For instance running ltlcross 'owl-21 ltl2nba' ... is equivalent to running ltlcross '{owl-21 ltl2nba}owl-21 ltl2nba -f %f>%O' ... Library: - Spot now provides convenient functions to create and solve games. (twaalgos/game.hh) and some additional functions for reactive synthesis (twaalgos/synthesis.hh, twaalgos/mealy_machine.hh). - A new class called aig represent an and-inverter-graphs, and is currently used during synthesis. (twaalgos/aiger.hh) - Some new *experimental* classes, called "twacube" and "kripkecube" implement a way to store automata or Kripke structures without using BDDs as labels. Instead they use a structure called cube, that can only encode a conjunction of litterals. Avoiding BDDs (or rather, avoiding the BuDDy library) in the API for automata makes it possible to build multithreaded algorithms. /!\ Currently these classes should be considered as experimental, and their API is very likely to change in a future version. Functions like twacube_to_twa(), twa_to_twacube(), can be used to bridge between automata with BDD labels, and automata with cube labels. In addition to the previous conversion, we implemented various state-of-the-art multi-threaded emptiness-check algorithms: [bloemen.16.ppopp], [bloemen.16.hvc], [evangeslita.12.atva], [renault.13.lpar], [holzmann.11.ieee] (see doc/spot.bib). The mc_instanciator class provides an abstraction for launching, pinning, and stopping threads inside of parallel model-checking algorithms. The class ltsmin_model class, providing support for loading various models that follow ltsmin's PINS interinterface, has been adjusted and can now produce either a kripke instance, or a kripkecube instance. - The postprocessor::set_type() method can now accept options postprocessor::Buchi and postprocessor::GeneralizedBuchi. These syntaxes is more homogeneous with the rest of the supported types. Note that postprocessor::BA and postprocessor::TGBA, while still supported and not yet marked as deprecated, are best avoided in new code. postprocessor::set_type(postprocessor::TGBA) can be replaced by postprocessor::set_type(postprocessor::GeneralizedBuchi) and postprocessor::set_type(postprocessor::BA) by postprocessor::set_type(postprocessor::Buchi) postprocessor::set_pref(postprocessor::Small | postprocessor::SBAcc) Note that the old postprocessor::BA option implied state-based acceptance (and was unique in that way), but the new postprocessor::Buchi specifies Büchi acceptance without requiring state-based acceptance (something that postprocessor did not permit before). - Translations for formulas such as FGp1 & FGp2 &...& FGp32 which used to take ages are now instantaneous. (Issue #412.) - remove_fin() learned to remove more unnecessary edges by using propagate_marks_vector(), both in the general case and in the Rabin-like case. - simplify_acceptance() learned to simplify acceptence formulas of the form Inf(x)&Inf(y) or Fin(x)|Fin(y) when the presence of x always implies that of y. (Issue #406.) - simplifiy_acceptance_here() and propagate_marks_here() learned to use some patterns of the acceptance condition to remove or add (depending on the function) colors on edges. As an example, with a condition such as Inf(0) | Fin(1), an edge labeled by {0,1} can be simplied to {0}, but the oppose rewriting can be useful as well. (Issue #418.) - The parity_game class has been removed, now any twa_graph_ptr that has a "state-player" property is considered to be a game. - the "state-player" property is output by the HOA printer, and read back by the automaton parser, which means that games can be saved and loaded. - print_dot() will display states from player 1 using a diamond shape. - print_dot() learned to display automata that correspond to Mealy machines specifically. - print_dot() has a new option "i" to define id=... attributes for states (S followed by the state number), edges (E followed by the edge number), and SCCs (SCC followed by SCC number). The option "i(graphid)" will also set the id of the graph. These id attributes are useful if an automaton is converted into SVG and one needs to refer to some particular state/edge/SCC with CSS or javascript. See https://spot.lrde.epita.fr/oaut.html#SVG-and-CSS - spot::postproc has new configuration variables that define thresholds to disable some costly operation in order to speedup the processing of large automata. (Those variables are typically modified using the -x option of command-line tools, and are all documented in the spot-x(7) man page.) wdba-det-max Maximum number of additional states allowed in intermediate steps of WDBA-minimization. If the number of additional states reached in the powerset construction or in the followup products exceeds this value, WDBA-minimization is aborted. Defaults to 4096. Set to 0 to disable. This limit is ignored when -D used or when det-max-states is set. simul-max Number of states above which simulation-based reductions are skipped. Defaults to 4096. Set to 0 to disable. This also applies to the simulation-based optimization of the determinization algorithm. simul-trans-pruning For simulation-based reduction, this is the number of equivalence classes above which transition-pruning for non-deterministic automata is disabled. Defaults to 512. Set to 0 to disable. This applies to all simulation-based reduction, as well as to the simulation-based optimization of the determinization algorithm. Simulation-based reduction perform a number of BDD implication checks that is quadratic in the number of classes to implement transition pruning. dpa-simul Set to 0/1 to disable/enable simulation-based reduction performed after running a Safra-like determinization to optain a DPA. By default, it is only disabled with --low or if simul=0. dba-simul Set to 0/1 to disable/enable simulation-based reduction performed after running the powerset-like construction (enabled by option tba-det) to obtain a DBA. By default, it is only disabled with --low or if simul=0. spot::translator additionally honor the following new variables: tls-max-states Maximum number of states of automata involved in automata-based implication checks for formula simplifications. Defaults to 64. exprop When set, this causes the core LTL translation to explicitly iterate over all possible valuations of atomic propositions when considering the successors of a BDD-encoded state, instead of discovering possible successors by rewriting the BDD as a sum of product. This is enabled by default for --high, and disabled by default otherwise. When unambiguous automata are required, this option forced and cannot be disabled. (This feature is not new, but was not tunable before.) - In addition the to above new variables, the default value for ba-simul (controling how degeneralized automata are reduced) and for det-simul (simulation-based optimization of the determinization) is now equal to the default value of simul. This changes allows "-x simul=0" to disable all of "ba-simul", "dba-simul", "dpa-simul", and "det-simul" at once. - tgba_powerset() now takes an extra optional argument to specify a list of accepting sinks states if some are known. Doing so can cut the size of the powerset automaton by 2^|sinks| in favorable cases. - twa_graph::merge_edges() had its two passes swapped. Doing so improves the determinism of some automata. - twa_graph::kill_state(num) is a new method that removes the outgoing edge of some state. It can be used together with purge_dead_states() to remove selected states. - The new functions reduce_direct_sim(), reduce_direct_cosim() and reduce_iterated() (and their state based acceptance version, reduce_direct_sim_sba(), reduce_direct_cosim_sba() and reduce_iterated_sba()), are matrix-based implementation of simulation-based reductions. This new version is faster than the signature-based BDD implementation in most cases, however there are some cases it does not capture yet.. By default, the old one is used. This behavior can be changed by setting SPOT_SIMULATION_REDUCTION environment variable or using the "-x simul-method=..." option (see spot-x(7)). - The automaton parser will now recognize lines of the form #line 10 "filename" that may occur *between* the automata of an input stream to specify that error messages should be emitted as if the next automaton was read from "filename" starting on line 10. (Issue #232) - The automaton parser for HOA is now faster at parsing files where a label is used multiple times (i.e., most automata): it uses a hash table to avoid reconstructing BDDs corresponding to label that have already been parsed. This trick was already used in the never claim parser. - spot::twa_graph::merge_states() will now sort the vector of edges before attempting to detect mergeable states. When merging states with identical outgoing transitions, it will now also consider self-looping transitions has having identical destinations. Additionally, this function now returns the number of states that have been merged (and therefore removed from the automaton). - spot::zielonka_tree and spot::acd are new classes that implement the Zielonka Tree and Alternatic Cycle Decomposition, based on a paper by Casares et al. (ICALP'21). Those structures can be used to paritize any automaton, and more. The graphical rendering of ACD in Jupyter notebooks is Spot's first interactive output. See https://spot.lrde.epita.fr/ipynb/zlktree.html for more. Python: - Bindings for functions related to games. See https://spot.lrde.epita.fr/ipynb/games.html and https://spot.lrde.epita.fr/tut40.html for examples. - Bindings for functions related to synthesis and aig-circuits. See https://spot.lrde.epita.fr/ipynb/synthesis.html - spot::twa::prop_set was previously absent from the Python bindings, making it impossible to call make_twa_graph() for copying a twa. It is now available as spot.twa_prop_set (issue #453). Also for convenience, the twa_graph.__copy__() method, called by copy.copy(), will duplicate a twa_graph (issue #470). Bugs fixed: - tgba_determinize() could create parity automata using more colors than necessary. (Related to issue #298) - There were two corners cases under which sat_minimize() would return the original transition-based automaton when asked to produce state-based output without changing the acceptance condition. Deprecation notices: - twa_graph::defrag_states() and digraph::defrag_states() now take the renaming vector by reference instead of rvalue reference. The old prototype is still supported but will emit a deprecation warning.

1 0

Spot 2.9.8 released (with conda-forge packages for Linux and OSX)
by Alexandre Duret-Lutz 10 Aug '21

10 Aug '21

We are happy to announce the release of Spot 2.9.8. This is a maintenance release that fixes a few bugs reported over the last three months, as well as a few warnings. New since the last version, we are now distributing Spot as a conda package (via conda-forge) for Linux and OSX. Instructions are on https://spot.lrde.epita.fr/install.html You can download the source for the new release directly from: http://www.lrde.epita.fr/dload/spot/spot-2.9.8.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Versions from the 2.9.x branch are the last releases using C++14. We have already switched to C++17 for the development of the next major release. This release is already compatible with C++17, so those using Spot as a library should consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.8 (2021-08-10) Documentation: - Mention the conda-forge package. Bugs fixed: - left->intersacting_run(right) could return a run with incorrect colors (likely not corresponding to any existing transition of left) if left was a weak automaton. (Issue #471) - Fix bitset::operator-() causing issues when Spot was configured with more than 32 colors for instance with --enable-max-sets=64. (Issue #469) - Work around some warnings from newer compilers.

1 0

Spot 2.9.7 released
by Alexandre Duret-Lutz 13 May '21

13 May '21

We are happy to announce the release of Spot 2.9.7. This is a maintenance release that fixes a handful of minor issues. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.7.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that versions from the 2.9.x branch are the last releases using C++14. We have already switched to C++17 for the development of the next major release. This release is already compatible with C++17, so users using Spot as a library should consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.7 (2021-05-12) Bugs fixed: - Some formulas using ->, <->, or xor were not properly detected as purely universal or pure eventualities. - autfilt --keep-states=... could incorrectly mention --mask-acc when diagnosing errors. - Work around GraphViz issue 1931, causing spurious failures in the test suite. - Miscelaneous documentation fixes.

1 0

Spot 2.9.6 released
by Alexandre Duret-Lutz 18 Jan '21

18 Jan '21

We are happy to announce the release of Spot 2.9.6. This is a maintenance release that fixes various issues, including a segmentation fault observed on the latest version of Alpine Linux released last week (however there is no reason why it may not occur elsewhere). It contains patches contributed by Florian Renkin, Jerome Dubois, and myself. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.6.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that versions from the 2.9.x branch are the last releases using C++14. We have already switched to C++17 for the development of the next major release. This release is already compatible with C++17, so tools using Spot as a library should consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.6 (2021-01-18) Build: - Build scripts are now compatible with Autoconf 2.70 (Issue #447) and require at least Autoconf 2.69 (released in 2012). - Debian builds use updated standards. Bugs fixed: - twa_graph::merge_edges() could fail to merge two transitions if the destination transition was the first of the automaton. (Issue #441) - On non-deterministic automata, iterated_simulations() was performing an (unnecessary) second iteration even when the first one failed to reduce the automaton. (Issue #442) - When passed an incomplete automaton as input, tgba_determinize() would sometimes produce a complete automaton but incorrectly mark it as incomplete. (Related to issue #298) - gf_guarantee_to_ba(), used to translate some specific classes of subformulas, could segfault in some condition (Issue #449). - Work around some spurious test suite failures.

1 0

Spot 2.9.5 released
by Alexandre Duret-Lutz 20 Nov '20

20 Nov '20

We are happy to announce the release of Spot 2.9.5 This is maintenance release with fixes for minor issues discovered over the last two months. If you already use 2.9.3 or later, there is no serious reason to upgrade. The release contains contributions from Jérôme Dubois and myself. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.5.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that versions from the 2.9.x branch are the last releases using C++14. We have already switched to C++17 for the development of the next major release. This release is already compatible with C++17, so tools using Spot as a library should consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.5 (2020-11-19) Bugs fixed: - Fix multiple spurious test suite failures on Darwin (Issues #426, #427, #428, #429) or when the Pandas package was not installed. - The filename python/spot/aux.py caused a problem on Windows and has been renamed. Existing "import spot.aux" statements should *not* be updated. (Issue #437) - Fix memory leak in minimize_wdba() when determinization is aborted because an output_aborter is passed. - Distribution used to contain unnecessary large SVG files (Issue #422) -- Alexandre Duret-Lutz

1 0

Spot 2.9.4 released
by Alexandre Duret-Lutz 07 Sep '20

07 Sep '20

We are happy to announce the release of Spot 2.9.4 This is a maintenance release with very minor fixes. (If you already have 2.9.3, there is no real reason to upgrade.) The release contains contributions from Florian Renkin and myself. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.4.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that versions from the 2.9.x branch are the last releases using C++14. We have already switched to C++17 for the development of the next major release. This release is already compatible with C++17, so tools using Spot as a library should consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.4 (2020-09-07) Bugs fixed: - Handle xor and <-> in a more natural way when translating LTL formulas to generic acceptance conditions. - Multiple typos in documentation, --help texts, or error messages. -- Alexandre Duret-Lutz

1 0

Spot 2.9.3 released
by Alexandre Duret-Lutz 22 Jul '20

22 Jul '20

Yes, 2.9.2 was short-lived, as the main issue it was supposed to fix was only half-fixed... You can find the 2.9.3 release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.3.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that versions 2.9.x are likely to be the last releases using C++14. We plan to switch to C++17 for the next major release. The current code-base is already compatible with C++17, so tools using Spot as a library may consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.3 (2020-07-22) Bug fixed: - Completely fix the ltlcross issue mentioned in previous release. New in spot 2.9.2 (2020-07-21) Bugs fixed: - ltlcross --csv=... --product=N with N>0 could output spurious diagnostics claiming that words were rejected when evaluating the automaton on state-space. - spot::scc_info::determine_unknown_acceptance() now also update the result of spot::scc_info::one_accepting_scc(). -- Alexandre Duret-Lutz

1 0

Spot 2.9.2 released
by Alexandre Duret-Lutz 21 Jul '20

21 Jul '20

Spot 2.9.2 has been released. This fixes a bug in ltlcross that was introduced in 2.9 and reported by Salomon Sickert. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.2.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that versions 2.9.x are likely to be the last releases using C++14. We plan to switch to C++17 for the next major release. The current code-base is already compatible with C++17, so tools using Spot as a library may consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.2 (2020-07-21) Bugs fixed: - ltlcross --csv=... --product=N with N>0 could output spurious diagnosics claiming that words were rejected when evaluating the automaton on state-space. - spot::scc_info::determine_unknown_acceptance() now also update the result of spot::scc_info::one_accepting_scc(). -- Alexandre Duret-Lutz

1 0

Spot 2.9.1 released
by Alexandre Duret-Lutz 16 Jul '20

16 Jul '20

We are happy to announce the release of Spot 2.9.1 This is mostly a maintenance release that fixes a couple of bugs discovered since the release of 2.9, as well as some simple portability issues. It also adds some minor features that were part of our SYNTCOMP submission (but not all patches of the SYNTCOMP submission have been merged yet). The release contains contributions from Florian Renkin and myself. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.1.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that versions 2.9.x are likely to be the last releases using C++14. We plan to switch to C++17 for the next major release. The current code-base is already compatible with C++17, so tools using Spot as a library may consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.1 (2020-07-15) Command-line tools: - 'ltl2tgba -G -D' is now better at handling formulas that use '<->' and 'xor' operators at the top level. For instance ltl2tgba -D -G '(Fa & Fb & Fc & Fd) <-> GFe' now produces a 16-state automaton (instead of 31 in Spot 2.9). - Option '-x wdba-minize=N' used to accept N=0 (off), or N=1 (on). It can now take three values: 0: never attempt this optimization, 1: always try to determinize and minimize automata as WDBA, and check (if needed) that the result is correct, 2: determinize and minimize automata as WDBA only if it is known beforehand (by cheap syntactic means) that the result will be correct (e.g., the input formula is a syntactic obligation). The default is 1 in "--high" mode, 2 in "--medium" mode or in "--deterministic --low" mode, and 0 in other "--low" modes. - ltlsynt learned --algo=ps to use the default conversion to deterministic parity automata (the same as ltl2tgba -DP'max odd'). - ltlsynt now has a -x option to fine-tune the translation. See the spot-x(7) man page for detail. Unlike ltl2tgba, ltlsynt defaults to simul=0,ba-simul=0,det-simul=0,tls-impl=1,wdba-minimize=2. Library: - product_xor() and product_xnor() are two new versions of the synchronized product. They only work with operands that are deterministic automata, and build automata whose language are respectively the symmetric difference of the operands, and the complement of that. - tl_simplifier_options::keep_top_xor is a new option to keep Xor and Equiv operator that appear at the top of LTL formulas (maybe below other Boolean or X operators). This is used by the spot::translator class when creating deterministic automata with generic acceptance. - remove_fin() learned a trick to remove some superfluous transitions. Bugs fixed: - Work around undefined behavior reported by clang 10.0.0's UBsan. - spot::twa_sub_statistics was very slow at computing the number of transitions, and could overflow. It is now avoiding some costly loop of BDD operations, and storing the result using at least 64 bits. This affects the output of "ltlcross --csv" and "--stats=%t" for many tools. - simplify_acceptance() missed some patterns it should have been able to simplify. For instance Fin(0)&(Fin(1)|Fin(2)|Fin(4)) should simplify to Fin(1)|Fin(2)|Fin(4) adter adding {1,2,4} to every place where 0 occur, and then the acceptance would be renumbered to Fin(0)|Fin(1)|Fin(2). This is now fixed. - Improve ltldo diagnostics to fix spurious test-suite failure on systems with antique GNU libc. - twa_run::reduce() could reduce accepting runs incorrectly on automata using Fin in their acceptance condition. This caused issues in intersecting_run(), exclusive_run(), intersecting_word(), exclusive_word(), which all call reduce(). - ltlcross used to crash with "Too many acceptance sets used. The limit is 32." when complementing an automaton would require more acceptance sets than supported by Spot. This is now diagnosed with --verbose, but does not prevent ltlcross from continuing. - scc_info::edges_of() and scc_info::inner_edges_of() now correctly honor any filter passed to scc_info. -- Alexandre Duret-Lutz

1 0

Spot 2.9 released
by Alexandre Duret-Lutz 30 Apr '20

30 Apr '20

We are happy to announce the release of Spot 2.9 This is a major release that has been under development for 9 months. It contains new features contributed by from Florian Renkin and myself. A summary of those changes is given at the end of this email. Note that version 2.9 and the following 2.9.x minor releases are likely to be the last releases using C++14. We plan is to switch to C++17 for the next major release. The current code-base is already compatible with C++17, so tools using Spot as a library may consider switching to C++17 already. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9 (2020-04-30) Command-line tools: - When the --check=stutter-sensitive-example option is passed to tools like ltl2tgba, autfilt, genaut, or ltldo, the produced automata are checked for stutter-invariance (as in the --check=stutter-invariant case), additionally a proof of stutter-sensitiveness is provided as two stutter-equivalent words: one accepted, and one rejected. These sample words are printed in the HOA output. % ltl2tgba --check=stutter-sensitive-example Xa | grep word: spot-accepted-word: "!a; cycle{a}" spot-rejected-word: "!a; !a; cycle{a}" - autfilt learned the --partial-degeneralize option, to remove conjunctions of Inf, or disjunctions of Fin that appears in arbitrary conditions. - ltlfilt and autfilt learned a --nth=RANGE (a.k.a. -N) option to select a range of their input formulas or automata (assuming a 1-based numbering). - When running translators, ltlcross will now display {names} when supplied. - ltlcross is now using the generic emptiness check procedure introduced in Spot 2.7, as opposed to removing Fin acceptance before using a classical emptiness check. - ltlcross learned a --save-inclusion-products=FILENAME option. Its use cases are probably quite limited. We use that to generate benchmarks for our generic emptiness check procedure. - ltlsynt --algo=lar uses the new version of to_parity() mentionned below. The old version is available via --algo=lar.old - ltlsynt learned --csv=FILENAME, to record some statistics about the duration of its different phases. - The dot printer is now automatically using rectangles with rounded corners for automata states if one state label have five or more characters. This saves space with very long labels. Use --dot=c, --dot=e, or --dot=E to force the use of Circles, Ellipses, or rEctangles. Library: - Historically, Spot only supports LTL with infinite semantics so it had automatic simplifications reducing X(1) and X(0) to 1 and 0 whenever such formulas are constructed. This caused issues for users of LTLf formulas, where it is important to distinguish a "weak next" (for which X(1)=1 but X(0)!=0) from a "strong next" (for which X(0)=0 but X(1)!=1). To accommodate this, this version introduces a new operator op::strong_X in addition to the existing op::X (whose interpretation is now weak in LTLf). The syntax for the strong next is X[!] as a reference to the PSL syntax (where the strong next is written X!). Trivial simplification rules for X are changed to just X(1) = 1 (and not X(0)=0 anymore) while we have X[!]0 = 0 The X(0)=0 and X[!]1=1 reductions are now preformed during LTL simplification, not automatically. Aside from the from_ltlf() function, the other functions of the library handle X and X[!] in the same way, since there is no difference between X and X[!] over infinite words. Operators F[n:m!] and G[n:m!] are also supported as strong variants of F[n:m] and G[n:m], but those four are only implemented as syntactic sugar. - acc_cond::acc_code::parity(bool, bool, int) was not very readable, as it was unclear to the reader what the boolean argument meant. The following sister functions can now improve readability: parity_max(is_odd, n) = parity(true, is_odd, n) parity_max_odd(n) = parity_max(true, n) parity_max_even(n) = parity_max(false, n) parity_min(is_odd, n) = parity(false, is_odd, n) parity_min_odd(n) = parity_min(true, n) parity_min_even(n) = parity_min(false, n) - partial_degeneralize() is a new function performing partial degeneralization to get rid of conjunctions of Inf terms, or disjunctions of Fin terms in acceptance conditions. - simplify_acceptance_here() and simplify_acceptance() learned to simplify subformulas like Fin(i)&Fin(j) or Inf(i)|Inf(j), or some more complex variants of those. If i is uniquely used in the acceptance condition, these become respectively Fin(i) or Inf(i), and the automaton is adjusted so that i also appears where j appeared. - acc_code::unit_propagation() is a new method for performing unit propagation in acceptance condition. E.g. Fin(0) | (Inf(0) & Inf(1)) becomes Fin(0) | Inf(1). This is now called by simplify_acceptance_here(). - propagate_marks_vector() and propagate_marks_here() are helper functions for propagating marks on the automaton: ignoring self-loops and out-of-SCC transitions, marks common to all the input transitions of a state can be pushed to all its outgoing transitions, and vice-versa. This is repeated until a fix point is reached. propagate_marks_vector() does not modify the automaton and returns a vector of the acc_cond::mark_t that should be on each transition; propagate_marks_here() actually modifies the automaton. - rabin_to_buchi_if_realizable() is a new variant of rabin_to_buchi_maybe() that converts a Rabin-like automaton into a Büchi automaton only if the resulting Büchi automaton can keep the same transition structure (where the ..._maybe() variant would modify the Rabin automaton if needed). - to_parity() has been rewritten. It now combines several strategies for paritizing automata with any acceptance condition. - relabel_bse(), used by ltlfilt --relabel-bool, is now better at dealing with n-ary operators and isolating subsets of operands that can be relabeled as a single term. - print_dot()'s default was changed to use circles for automata with fewer than 10 unamed states, ellipses for automata with up to 1000 unamed states (or named states with up to 4 characters), and rounded rectangles otherwise. Rectangles are also used for automata with acceptance bullets on states. The new "E" option can be used to force rectangles in all situations. - The generic emptiness check has been slightly improved (doing fewer recursive calls in the worst case). Backward-incompatible changes: - iar() and iar_maybe() have been moved from spot/twaalgos/rabin2parity.hh spot/twaalgos/toparity.hh and marked as deprecated, they should be replaced by to_parity(). In case the input is Rabin-like or Streett-like, to_parity() should be at least as good as iar(). - The twa_graph::is_alternating() and digraph::is_alternating() methods, deprecated in Spot 2.3.1 (2017-02-20), have been removed. Bugs fixed: - Relabeling automata could introduce false edges. Those are now removed. - Emptiness checks, and scc_info should now ignore edges labeled with false. - relabel_bse() could incorrectly relabel Boolean subformulas that had some atomic propositions in common. -- Alexandre Duret-Lutz

1 0

Spot 2.8.7 released
by Alexandre Duret-Lutz 13 Mar '20

13 Mar '20

We are happy to announce the release of Spot 2.8.7 This maintenance release contains only bug fixes. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.7.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.8.7 (2019-03-13) Bugs fixed: - Building a product between two complete automata where one operand had false acceptance could create an incomplete automaton incorrectly tagged as complete, causing the print_hoa() function to raise an exception. - autfilt --uniq was not considering differences in acceptance conditions or number of states when discarding automata. - In an automaton with acceptance condition containing some Fin, and whose accepting cycle could be reduced to a self-loop in an otherwise larger SCC, the generation of an accepting run could be wrong. This could in turn cause segfaults or infinite loops while running autcross or autfilt --stats=%w. - The generic emptiness check used a suboptimal selection of "Fin" to remove, not matching the correct line in our ATVA'19 paper. This could cause superfluous recursive calls, however benchmarks have shown the difference to be insignificant in practice. - The sl(), and sl2() functions for computing the "self-loopization" of an automaton, and used for instance in algorithms for computing proof of stutter-sensitiveness (e.g., in our web application), were incorrect when applied on automata with "t" acceptance (or more generaly, any automaton where a cycle without mark is accepting). - ltlcross was not diagnosing write errors associated to options --grind=FILENAME and --save-bogus=FILENAME. -- Alexandre Duret-Lutz

1 0

Spot 2.8.6 released
by Alexandre Duret-Lutz 19 Feb '20

19 Feb '20

We are happy to announce the release of Spot 2.8.6 This maintenance release containing fixes for bug discovered during the development of the future 2.9 release. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.6.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.8.6 (2020-02-19) Bugs fixed: - calling spot.translate() with two conflicting preferences like spot.translate(..., 'det', 'any') triggered a syntax error in the Python code to handle this error. - degeneralize_tba() was incorrectly not honnoring the "skip_level" optimization after creating an accepting transition; as a consequence, some correct output could be larger than necessary (but still correct). - Some formulas with Boolean sub-formulas equivalent to true or false could be translated into automata with false labels. - The HOA printer would incorrectly output the condition 'Fin(1) & Inf(2) & Fin(0)' as 'Fin(0) | Fin(1) & Inf(2)' due to a bug in the is_generalized_rabin() matching function. -- Alexandre Duret-Lutz

1 0

Spot 2.8.5 released
by Alexandre Duret-Lutz 04 Jan '20

04 Jan '20

We are happy to announce the release of Spot 2.8.5 This maintenance release contains only bug fixes. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.5.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.8.5 (2020-01-04) Bugs fixed: - ltl2tgba -B could return automata with "t" acceptance, instead of the expected Inf(0). - twa_graph::merge_edges() (a.k.a. autfilt --merge-transitions) was unaware that merging edges can sometimes transform a non-deterministic automaton into a deterministic one, causing the following unexpected diagnostic: "print_hoa(): automaton is universal despite prop_universal()==false" The kind of non-deterministic automata where this occurs is not naturally produced by any Spot algorithm, but can be found for instance in automata produced by Goal 2015-10-18. -- Alexandre Duret-Lutz

1 0

Spot 2.8.4 has been released
by Alexandre Duret-Lutz 09 Dec '19

09 Dec '19

We are happy to announce the release of Spot 2.8.4 This release contains a fix for a bug affecting complementation of Rabin-like automata. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.4.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.8.4 (2019-12-08) Bugs fixed: - The Rabin-to-Büchi conversion could misbehave when applied to Rabin-like acceptance with where some pairs have missing Inf(.) (e.g. Fin(0)|(Inf(1)&Fin(2))) and when some of the SCCs do not visit the remaining Inf(.). This indirectly caused the complementation algorithm to produce incorrect results on such inputs, causing false positives in ltlcross and autcross. - Work around a small difference between Python 3.7 and 3.8, causing spurious failures of the test suite. -- Alexandre Duret-Lutz

1 0

Spot 2.8.3 released
by Alexandre Duret-Lutz 06 Nov '19

06 Nov '19

We are happy to announce the release of Spot 2.8.3 This release mainly works around an issue in recent GraphViz releases, causing cropped automata in Jupyter notebooks. (If you do not use Spot in Jupyter notebooks, there is little point in updating.) You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.3.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.8.3 (2019-11-06) Build: - Minor portabilities improvements with C++17 deprecations. Python: - Doing "import spot.foo" will now load any spot-extra/foo.py on Python's search path. This can be used to install third-party packages that want to behave as plugins for Spot. - Work around GraphViz bug #1605 in Jupyter notebooks. https://gitlab.com/graphviz/graphviz/issues/1605 -- Alexandre Duret-Lutz

1 0

Spot 2.8.2 released
by Alexandre Duret-Lutz 28 Sep '19

28 Sep '19

We are happy to announce the release of Spot 2.8.2 This release contains many minor fixes; mostly portability issues. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.2.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.8.2 (2019-09-27) Command-line tools: - ltl2tgba and ltldo learned a --negate option. Bugs fixed: - Calling "autfilt --dualize" on an alternating automaton with transition-based acceptance and universal initial states would fail with "set_init_state() called with nonexisting state". - The numbering of nodes in the AIGER output of ltlsynt was architecture dependent. - Various compilation issues. In particular, this release is the first one that can be compiled (and pass tests) on a Raspberry PI. -- Alexandre Duret-Lutz

1 0

Spot 2.8.1 released
by Alexandre Duret-Lutz 18 Jul '19

18 Jul '19

We are happy to announce the release of Spot 2.8.1 This release one important bug fix to ltlcross, and a few other minor addition. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.1.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.8.1 (2019-07-18) Command-line tools: - genltl learned --pps-arbiter-standard and --pps-arbiter-strict. - ltlcross and autcross have learned a new option -q (--quiet) to remain quiet until an error is found. This helps for instance in scenarios where multiple instances of ltlcross/autcross are run in parallel (using "xargs -P" or "GNU Parallel", for instance). See https://spot.lrde.epita.fr/ltlcross.html#parallel for examples. Bugs fixed: - When complement() was called with an output_aborter, it could return an alternating automaton on large automata. This in turn caused ltlcross to emit errors like "remove_alternation() only works with weak alternating automata" or "product() does not support alternating automata". - Work around Emacs bug #34341 when rebuilding documentation on a system with Emacs <26.3, GNU TLS >= 3.6, and without ESS or with an obsolete org-mode installed. -- Alexandre Duret-Lutz

1 0

Spot 2.8 released
by Alexandre Duret-Lutz 10 Jul '19

10 Jul '19

We are happy to announce the release of Spot 2.8 Spot is a library of algorithms for manipulating LTL formulas and omega-automata objects (as commonly used in model checking). This release contains code contributed by Clément Gillard and myself. A detailed list of new features is given at the end of this email. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that since Debian 10 ("Buster") was released a few days ago, the "stable" Debian packages we distribute are now built for Buster. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.8 (2019-07-10) Command-line tools: - autfilt learned --highlight-accepting-run=NUM to highlight some accepting run with color NUM. - ltldo, ltlcross, and autcross are now preferring posix_spawn() over fork()+exec() when available. - ltlcross has new options --determinize-max-states=N and --determinize-max-edges=M to restrict the use of determinization-based complementation to cases where it produces automata with at most N states and M edges. By default determinization is now attempted up to 500 states and 5000 edges. This is an improvement over the previous default where determinization-based complementation was not performed at all, unless -D was specified. - ltlcross will now skip unnecessary cross-checks and consistency-checks (they are unnecessary when all automata could be complemented and statistics were not required). - genaut learned --m-nba=N to generate Max Michel's NBA familly. (NBAs with N+1 states whose determinized have at least N! states.) - Due to some new simplification of parity acceptance, the output of "ltl2tgba -P -D" is now using a minimal number of colors. This means that recurrence properties have an acceptance condition among "Inf(0)", "t", or "f", and persistance properties have an acceptance condition among "Fin(0)", "t", or "f". - ltldo and ltlcross learned shorthands to call the tools ltl2na, ltl2nba, and ltl2ngba from Owl 19.06. Similarly, autcross learned a shorthand for Owl's dra2dpa. Documentation: - https://spot.lrde.epita.fr/tut90.html is a new file that explains the purpose of the spot::bdd_dict object. Library: - Add generic_accepting_run() as a variant of generic_emptiness_check() that returns an accepting run in an automaton with any acceptance condition. - twa::accepting_run() and twa::intersecting_run() now work on automata using Fin in their acceptance condition. - simulation-based reductions have learned a trick that sometimes improve transition-based output when the input is state-based. (The automaton output by 'ltl2tgba -B GFa | autfilt --small' now has 1 state instead of 2 in previous versions. Similarly, 'ltldo ltl2dstar -f 'GFa -> GFb' | autfilt --small' produces 1 state instead of 4.) - simulation-based reductions hae learned another trick to better merge states from transiant SCCs. - acc_cond::top_disjuncts() and acc_cond::top_conjuncts() can be used to split an acceptance condition on the top-level & or |. These methods also exist in acc_cond::acc_code. - minimize_obligation() learned to work on very weak automata even if the formula or negated automaton are not supplied. (This allows "autfilt [-D] --small" to minimize very-weak automata whenever they are found to represent obligation properties.) - There is a new spot::scc_and_mark_filter objet that simplifies the creation of filters to restrict spot::scc_info to some particular SCC while cutting new SCCs on given acceptance sets. This is used by spot::generic_emptiness_check() when processing SCCs recursively, and makes it easier to write similar code in Python. - print_dot has a new option 'g', to hide edge labels. This is helpful to display automata as "graphs", e.g., when illustrating algorithms that do not care about labels. - A new complement() function returns complemented automata with unspecified acceptance condition, allowing different algorithms to be used. The output can be alternating only if the input was alternating. - There is a new class output_aborter that is used to specify upper bounds on the size of automata produced by some algorithms. Several functions have been changed to accept an output_aborter. This includes: * tgba_determinize() * tgba_powerset() * minimize_obligation() * minimize_wdba() * remove_alternation() * product() * the new complement() * the postprocessor class, via the "det-max-state" and "det-max-edges" options. - SVA's first_match operator can now be used in SERE formulas and that is supported by the ltl_to_tgba_fm() translation. See doc/tl/tl.pdf for the semantics. *WARNING* Because this adds a new operator, any code that switches over the spot::op type may need a new case for op::first_match. Furthermore, the output of "randltl --psl" will be different from previous releases. - The parser for SERE learned to recognize the ##n and ##[i:j] operators from SVA. So {##2 a ##0 b[+] ##1 c ##2 e} is another way to write {[*2];a:b[+];c;1;e}. The syntax {a ##[i:j] b} is replaced in different ways depending on the values of i, a, and b. The formula::sugar_delay() function implements this SVA operator in terms of the existing PSL operators. ##[+] and ##[*] are sugar for ##[1:$] and ##[0:$]. - The F[n:m] and G[n:m] operators introduced in Spot 2.7 now support the case where m=$. - spot::relabel_apply() makes it easier to reverse the effect of spot::relabel() or spot::relabel_bse() on formula. - The LTL simplifier learned the following rules: F(G(a | Fb)) = FGa | GFb (if option "favor_event_univ") G(F(a | Gb)) = GFa | FGb (if option "favor_event_univ") F(G(a & Fb) = FGa & GFb (unless option "reduce_size_strictly") G(F(a & Gb)) = GFa & FGb (unless option "reduce_size_strictly") GF(f) = GF(dnf(f)) (unless option "reduce_size_strictly") FG(f) = FG(cnf(f)) (unless option "reduce_size_strictly") (f & g) R h = f R h if h implies g (f & g) M h = f M h if h implies g (f | g) W h = f W h if g implies h (f | g) U h = f U h if g implies h Gf | F(g & eventual) = f W (g & eventual) if !f implies g Ff & G(g | universal) = f M (g | universal) if f implies !g f U (g & eventual) = F(g & eventual) if !f implies g f R (g | universal) = G(g | universal) if f implies !g - cleanup_parity() and colorize_parity() were cleaned up a bit, resulting in fewer colors used in some cases. In particular, colorize_parity() learned that coloring transitiant edges does not require the introduction of a new color. - A new reduce_parity() function implements and generalizes the algorithm for minimizing parity acceptance by Carton and Maceiras (Computing the Rabin index of a parity automaton, 1999). This is a better replacement for cleanup_parity() and colorize_parity(). See https://spot.lrde.epita.fr/ipynb/parity.html for examples. - The postprocessor and translator classes are now using reduce_parity() for further simplifications. - The code for checking recurrence/persistence properties can also use the fact the reduce_parity() with return "Inf(0)" (or "t" or "f") for deterministic automata corresponding to recurrence properties, and "Fin(0)" (or "t" or "f") for persistence properties. This can be altered with the SPOT_PR_CHECK environment variable. Deprecation notices: - The virtual function twa::intersecting_run() no longuer takes a second "from_other" Boolean argument. This is a backward incompatibility only for code that overrides this function in a subclass. For backward compatibility with programs that simply call this function with two argument, a non-virtual version of the function has been introduced and marked as deprecated. - The spot::acc_cond::format() methods have been deprecated. These were used to display acceptance marks, but acceptance marks are unrelated to acceptance conditions, so it's better to simply print marks with operator<< without this extra step. Bugs fixed: - The gf_guarantee_to_ba() is relying on an inplace algorithm that could produce a different number of edges for the same input in two different transition order. - A symmetry-based optimization of the LAR algorithm performed in spot::to_parity() turned out to be incorrect. The optimization has been removed. "ltlsynt --algo=lar" is the only code using this function currently. -- Alexandre Duret-Lutz

1 0

Spot 2.7.5 released
by Alexandre Duret-Lutz 05 Jun '19

05 Jun '19

We are happy to announce the release of Spot 2.7.5 This maintenance release fixing a few minor issues. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.7.5.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.7.5 (2019-06-05) Build: - Although the Python bindings in this release are still done with Swig3.0, the code has been updated to be compatible with Swig4.0. Library: - print_dot will replace labels that have more 2048 characters by a "(label too long)" string. This works around a limitation of GraphViz that aborts when some label exceeds 16k characters, and also helps making large automata more readable. Bugs fixed: - spot::translator was not applying Boolean sub-formula rewritting by default unless a spot::option_map was passed. This caused some C++ code for translating certains formulas to be noticeably slower than the equivalent call to the ltl2tgba binary. - The remove_ap algorithm was preserving the "terminal property" of automata, but it is possible that a non-terminal input produces a terminal output after some propositions are removed. -- Alexandre Duret-Lutz

1 0

Spot 2.7.4 released
by Alexandre Duret-Lutz 27 Apr '19

27 Apr '19

We are happy to announce the release of Spot 2.7.4 This maintenance release contains only some bug fixes. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.7.4.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.7.4 (2019-04-27) Bugs fixed: - separate_sets_here() (and therefore autfilt --separate-sets) could loop infinitely on some inputs. - In some situation, ltl2tgba -G could abort with "direct_simulation() requires separate Inf and Fin sets". This was fixed by teaching simulation-based reductions how to deal with such cases. - The code for detecting syntactically stutter-invariant PSL formulas was incorrectly handling the ";" operator, causing some stutter-sensitive formulas to be flagged a stutter-invariant. -- Alexandre Duret-Lutz

1 0

Spot 2.7.3 released
by Alexandre Duret-Lutz 19 Apr '19

19 Apr '19

We are happy to announce the release of Spot 2.7.3 This maintenance release contains only bug fixes and documentation updates. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.7.3.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.7.3 (2019-04-19) Bugs fixed: - When processing CSV files with MSDOS-style \r\n line endings, --stats would output the \r as part of the %> sequence instead of ignoring it. - Fix serious typo in removel_alternation() causing incorrect output for some VWAA. Bug introduced in Spot 2.6. Documentation: - Multiple typos and minor updates. -- Alexandre Duret-Lutz

1 0

Spot 2.7.2 released
by Alexandre Duret-Lutz 17 Mar '19

17 Mar '19

We are happy to announce the release of Spot 2.7.2 This release contains mostly documentation improvements and some minor additions to the Python bindings. See below for a detailed list of user-visible changes. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.7.2.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.7.2 (2019-03-17) Python: - Improved support for explicit Kripke structures. It is now possible to iterate over a kripke_graph object in a way similar to twa_graph. Documentation: - A new page shows how to create explicit Kripke structures in C++ and Python. See https://spot.lrde.epita.fr/tut52.html - Another new page shows how to deal with LTLf formulas (i.e., LTL with finite semantics) and how to translate those. See https://spot.lrde.epita.fr/tut12.html Build: - Work around a spurious null dereference warning when compiling with --coverage and g++ 8.3.0-3 from Debian unstable. -- Alexandre Duret-Lutz

1 0

Spot 2.7.1 released
by Alexandre Duret-Lutz 14 Feb '19

14 Feb '19

We are happy to announce the release of Spot 2.7.1 This release contains mostly bug fixes and some minor additions to the Python bindings. See below for a detailed list of user-visible changes. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.7.1.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.7.1 (2019-02-14) Build - Work around GCC bug #89303 that causes memory leaks and std::weak_bad_ptr exceptions when Spot is compiled with the version of g++ 8.2 currently distributed by Debian unstable (starting with g++ 8.2.0-15). Python: - The following methods of spot::bdd_dict are now usable in Python when fine control over the lifetime of associations between BDD variables and atomic propositions is needed. - register_proposition(formula, for_me) - register_anonymous_variables(count, for_me) - register_all_propositions_of(other, for_me) - unregister_all_my_variables(for_me) - unregister_variable(var, for_me) - Better support for explicit Kripke structures: - the kripke_graph type now has Python bindings - spot.automaton() and spot.automata() now support a want_kripke=True to return a kripke_graph See the bottom of https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html for some examples. Library: - Printing Kripke structures via print_hoa() will save state names. - kripke_graph_ptr objects now honnor any "state-names" property when formating states. Bugs fixed: - The print_dot_psl() function would incorrectly number all but the first children of commutative n-ary operators: in this case no numbering was expected. - std::out_of_range C++ exceptions raised from Python code are now converted into IndexError Python exceptions (instead of aborting the program). - The LTL parser would choke on carriage returns when command-line tools such as ltlfilt, ltlcross, or ltl2tgba were run on files of formulas with MS-DOS line endings. - The core translation for unambiguous automata was incorrectly tagging some non-weak automata as weak. - The product_susp() function used to multiply an automaton with a suspendable automaton could incorrectly build transition-based automata when multipliying two state-based automata. This caused ltl2tgba to emit error messages such as: "automaton has transition-based acceptance despite prop_state_acc()==true". -- Alexandre Duret-Lutz

1 0

Spot 2.7 released
by Alexandre Duret-Lutz 11 Dec '18

11 Dec '18

We are happy to announce the release of Spot 2.7 Someone recently reported some release-worthy bug, and unfortunately we do not have time to prepare a 2.6.4 release by cherry-picking the bug fixes from the development branch. So here is Spot 2.7 instead, with some minor new features and backward-incompatible changes done over the last 5 months. See the list below for details. This release contains contributions by Maximilien Colange, Etienne Renault, and myself. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.7.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.7 (2018-12-11) Command-line tools: - ltlsynt now has three algorithms for synthesis: --algo=sd is the historical one. The automaton of the formula is split to separate inputs and outputs, then determinized (with Safra construction). --algo=ds the automaton of the formula is determinized (Safra), then split to separate inputs and outputs. --algo=lar translate the formula to a deterministic automaton with an arbitrary acceptance condition, then turn it into a parity automaton using LAR, and split it. In all three cases, the obtained parity game is solved using Zielonka algorithm. Calude's quasi-polynomial time algorithm has been dropped as it was not used. - ltlfilt learned --liveness to match formulas representing liveness properties. - the --stats= option of tools producing automata learned how to tell if an automaton uses universal branching (%u), or more precisely how many states (%[s]u) or edges (%[e]u) use universal branching. Python: - spot.translate() and spot.postprocess() now take an xargs= argument similar to the -x option of ltl2tgba and autfilt, making it easier to fine tune these operations. For instance ltl2tgba 'GF(a <-> XXa)' --det -x gf-guarantee=0 would be written in Python as spot.translate('GF(a <-> XXa)', 'det', xargs='gf-guarantee=0') (Note: those extra options are documented in the spot-x(7) man page.) - spot.is_generalized_rabin() and spot.is_generalized_streett() now return a tuple (b, v) where b is a Boolean, and v is the vector of the sizes of each generalized pair. This is a backward incompatible change. Library: - The LTL parser learned syntactic sugar for nested ranges of X using the X[n], F[n:m], and G[n:m] syntax of TSLF. (These correspond to the next!, next_e!, and next_a! operators of PSL, but we do not support those under these names currently.) X[6]a = XXXXXXa F[2:4]a = XX(a | X(a | Xa)) G[2:4]a = XX(a & X(a & Xa)) The corresponding constructors (for C++ and Python) are formula::X(unsigned, formula) formula::F(unsigned, unsigned, formula) formula::G(unsigned, unsigned, formula) - spot::unabbreviate(), used to rewrite away operators such as M or W, learned to use some shorter rewritings when an argument (e) is a pure eventuality or (u) is purely universal: Fe = e Gu = u f R u = u f M e = F(f & e) f W u = G(f | u) - The twa_graph class has a new dump_storage_as_dot() method to show its data structure. This is more conveniently used as aut.show_storage() in a Jupyter notebook. See https://spot.lrde.epita.fr/ipynb/twagraph-internals.html - spot::generic_emptiness_check() is a new function that performs emptiness checks of twa_graph_ptr (i.e., automata not built on-the-fly) with an *arbitrary* acceptance condition. Its sister spot::generic_emptiness_check_scc() can be used to decide the emptiness of an SCC. This is now used by twa_graph_ptr::is_empty(), twa_graph_ptr::intersects(), and scc_info::determine_unknown_acceptance(). - The new function spot::to_parity() translates an automaton with arbitrary acceptance condition into a parity automaton, based on a last-appearance record (LAR) construction. (It is used by ltlsynt but not yet by autfilt or ltl2tgba.) - The new function is_liveness() and is_liveness_automaton() can be used to check whether a formula or an automaton represents a liveness property. - Two new functions count_univbranch_states() and count_univbranch_edges() can help measuring the amount of universal branching in alternating automata. Bugs fixed: - translate() would incorrectly mark as stutter-invariant some automata produced from formulas of the form X(f...) where f... is syntactically stutter-invariant. - acc_cond::is_generalized_rabin() and acc_cond::is_generalized_streett() did not recognize the cases were a single generalized pair is used. - The pair of acc_cond::mark_t returned by acc_code::used_inf_fin_sets(), and the pair (bool, vector_rs_pairs) by acc_cond::is_rabin_like() and acc_cond::is_streett_like() were not usable in Python. - Many object types had __repr__() methods that would return the same string as __str__(), contrary to Python usage where repr(x) should try to show how to rebuild x. The following types have been changed to follow this convention: spot.acc_code spot.acc_cond spot.atomic_prop_set spot.formula spot.mark_t spot.twa_run (__repr__ shows type and address) spot.twa_word (likewise, but _repr_latex_ used in notebooks) Note that this you were relying on the fact that Jupyter calls repr() to display returned values, you may want to call print() explicitely if you prefer the old representation. - Fix compilation under Cygwin and Alpine Linux, both choking on undefined secure_getenv().

1 0

Spot 2.6.3 released
by Alexandre Duret-Lutz 17 Oct '18

17 Oct '18

We are happy to announce the release of Spot 2.6.3 This is a maintenance release containing only bug fixes. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.6.3.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.6.3 (2018-10-17) Bugs fixed: - Running "ltl2tgba -B" on formulas of the type FG(safety) would unexpectedly use a co-Büchi automaton as an intermediate step. This in turn caused "ltl2tgba -U -B" to not produce unambiguous automata. - ltl2tgba --low now disables the "gf-guarantee" feature, as documented. - ltlfilt's --accept-word and --reject-word options were ignored unless used together. -- Alexandre Duret-Lutz

1 0

Spot 2.6.2
by Alexandre Duret-Lutz 28 Sep '18

28 Sep '18

We are happy to announce the release of Spot 2.6.2 This is a maintenance release containing minor bug fixes. This also removes the source code for the online translator, that has been replaced by a separate (and rewritten) web application. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.6.2.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.6.2 (2018-09-28) Build: - We no longer distribute the Python-based CGI script + javascript code for the online translator. Its replacement has its own repository: https://gitlab.lrde.epita.fr/spot/spot-web-app/ Library: - When states are highlighted with more than 8 colors, print_dot() will add some extra markers to help distinguishing the colors. This helps with the fact that colors 8-15 are lighter versions of colors 0-7, and that higher color numbers cycle into this 16-color palette. Bugs fixed: - exclusive_ap::constrain() (called by autfilt --exclusive-ap=...) would incorrectly copy the "universal" property of the input automaton, causing print_hoa() to fail. - configure --disable-doxygen would actually enable it. - Fix several warnings emited by the development version of GCC. -- Alexandre Duret-Lutz

1 0

Spot 2.6.1 released
by Alexandre Duret-Lutz 04 Aug '18

04 Aug '18

We are happy to announce the release of Spot 2.6.1 This is a maintenance release containing mostly bug fixes. The only exception is the straightforward --suspendable option added to ltlfilt. This release contains code contributed by Etienne Renault, Maximilien Colange, Antoine Martin, and myself. Noteworthy changes are given at the end of this email. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.6.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.6.1 (2018-08-04) Command-line tools: - "ltlfilt --suspendable" is now a synonym for "ltlfilt --universal --eventual". Bugs fixed: - scc_info::split_on_sets() did not correctly register the atomic propositions of the returned automata. - The spot::tl_simplifier class could raise an exception while attempting to reduce formulas containing unsimplified <->, -> or xor, if options nenoform_stop_on_boolean and synt_impl are both set. (This combination of options is not available from command-line tools.) - The spot::contains(a, b) function introduced in 2.6 was testing a⊆b instead of a⊇b as one would expect. Infortunately the documentation was also matching the code, so this is a backward incompatible change, but a short-lived one. - The Python binding of the getter of spot::parsed_formula::f was returning a reference instead of a copy, causing issues if the reference outlasted the parsed_formula struct. -- Alexandre Duret-Lutz

1 0

Spot 2.6 released
by Alexandre Duret-Lutz 04 Jul '18

04 Jul '18

We are happy to announce the release of Spot 2.6. Spot is a library of algorithms for manipulating LTL formulas and omega-automata (objects as commonly used in model checking). This release contains code contributed by Maximilien Colange, Antoine Martin, and myself. A detailed list of new features in this new release is given at the end of this email. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.6.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that the unstable Debian packages and stable RPM packages should be available within 24h. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.6 (2018-07-04) Command-line tools: - autfilt learned --is-colored to filter automata that use exactly one acceptance set per mark or transition. - autfilt learned --has-univ-branching and --has-exist-branching to keep automata that have universal branching, or that make non-deterministic choices. - autcross' tool specifications now have %M replaced by the name of the input automaton. - autcross now aborts if there is any parser diagnostic for the input automata (previous versions would use the input automaton whenever the parser would manage to read something). - ltlcross, ltldo, and autcross learned shorthands to call delag, ltl2dra, ltl2dgra, and nba2dpa. - When autfilt is asked to build a Büchi automaton from of a chain of many products, as in "autfilt -B --product 1.hoa ... --product n.hoa in.hoa" then it will automatically degeneralize the intermediate products to avoid exceeding the number of supported acceptance sets. - genltl learned to generate six new families of LTL formulas: --gf-equiv-xn=RANGE GF(a <-> X^n(a)) --gf-implies-xn=RANGE GF(a -> X^n(a)) --sejk-f=RANGE[,RANGE] f(0,j)=(GFa0 U X^j(b)), f(i,j)=(GFai U G(f(i-1,j))) --sejk-j=RANGE (GFa1&...&GFan) -> (GFb1&...&GFbn) --sejk-k=RANGE (GFa1|FGb1)&...&(GFan|FGbn) --sejk-patterns[=RANGE] φ₁,φ₂,φ₃ from Sikert et al's [CAV'16] paper (range should be included in 1..3) - genltl --ms-example can now take a two-range argument, (as --sejk-f above). Build: - ./configure --enable-max-accsets=N let you specify a maximum number of acceptance sets that Spot should support. The default is still 32, but this limit is no longer hardcoded. Larger values will cost additional memory and time. - We know distribute RPM packages for Fedora 28. See file:///home/adl/git/spot/doc/userdoc/install.html#Fedora Library: - The PSL/LTL simplification routine learned the following: q R Xf = X(q R f) if q is suspendable q U Xf = X(q U f) if q is suspendable {SERE;1} = {1} if {SERE} accepts [*0] {SERE;1} = {SERE} if {SERE} does not accept [*0] - gf_guarantee_to_ba() is a specialized construction for translating formulas of the form GF(guarantee) to BA or DBA, and fg_safety_to_dca() is a specialized construction for translating formulas of the form FG(safety) to DCA. These are generalizations of some constructions proposed by J. Esparza, J. Křentínský, and S. Sickert (LICS'18). These are now used by the main translation routine, and can be disabled by passing -x '!gf-guarantee' to ltl2tgba. For example, here are the size of deterministic transition-based generalized Büchi automata constructed from four GF(guarantee) formulas with two versions of Spot, and converted to other types of deterministic automata by other tools distributed with Owl 18.06. "x(y)" means x states and y acceptance sets. ltl2tgba -D delag ltl2dra 2.5 2.6 18.06 18.06 ------------------------- ----------- ------------- GF(a <-> XXa) 9(1) 4(1) 4(2) 9(4) GF(a <-> XXXa) 27(1) 8(1) 8(2) 25(4) GF(((a & Xb) | XXc) & Xd) 6(1) 4(1) 16(1) 5(2) GF((b | Fa) & (b R Xb)) 6(2) 2(1) 3(4) 3(4) Note that in the above the automata produced by 'ltl2tgba -D' in version 2.5 were not deterministic (because -D is only a preference). They are deterministic in 2.6 and other tools. - spot::product() and spot::product_or() learned to produce an automaton with a simpler acceptance condition if one of the argument is a weak automaton. In this case the resulting acceptance condition is (usually) that of the other argument. - spot::product_susp() and spot::product_or_susp() are new functions for building products between an automaton A and a "suspendable" automaton B. They are also optimized for the case that A is weak. - When 'generic' acceptance is enabled, the translation routine will split the input formula on Boolean operators into components that are syntactically 'obligation', 'suspendable', or 'something else'. Those will be translated separately and combined with product()/product_susp(). This is inspired by the ways things are done in ltl2dstar or delag, and can be disabled by passing option -xltl-split=0, as in ltl2tgba -G -D -xltl-split=0. Here are the sizes of deterministic automata (except for ltl3tela which produces non-deterministic automata) produced with generic acceptance using two versions of ltl2tgba and other tools for reference. ltl2tgba -DG delag ltl3tela 2.5 2.6 18.06 1.1.2 ------------ ------- -------- FGa0&GFb0 2(2) 1(2) 1(2) 1(2) (FGa1&GFb1)|FGa0|GFb0 16(6) 1(4) 1(4) 1(9) (FGa2&GFb2)|((FGa1|GFb1)&FGa0&GFb0) 29(8) 1(6) 1(6) 3(11) FGa0|GFb0 5(4) 1(2) 1(2) 1(5) (FGa1|GFb1)&FGa0&GFb0 8(4) 1(4) 1(4) 1(7) (FGa2|GFb2)&((FGa1&GFb1)|FGa0|GFb0) 497(14) 1(6) 1(6) 1(14) GFa1 <-> GFz 4(6) 1(3) 1(4) 1(7) (GFa1 & GFa2) <-> GFz 8(4) 1(3) 1(6) 3(10) (GFa1 & GFa2 & GFa3) <-> GFz 21(4) 1(4) 1(8) 3(13) GFa1 -> GFz 5(4) 1(2) 1(2) 1(5) (GFa1 & GFa2) -> GFz 12(4) 1(3) 1(3) 1(6) (GFa1 & GFa2 & GFa3) -> GFz 41(4) 1(4) 1(4) 1(7) FG(a|b)|FG(!a|Xb) 4(2) 2(2) 2(2) 2(3) FG(a|b)|FG(!a|Xb)|FG(a|XXb) 21(2) 4(3) 4(3) 4(4) FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb) 170(2) 8(4) 8(4) 8(5) - For 'parity' output, the 'ltl-split' optimization just separates obligation subformulas from the rest, where a determinization is still performed. ltl2tgba -DP ltl3dra ltl2dpa 2.5 2.6 0.2.3 18.06 -------------- ------- ------- FGp0 & (Gp1 | XFp2) 6(2) 4(1) 4(1) 4(2) G!p0 | F(p0 & (!p1 W p2)) 5(2) 4(2) n/a 5(2) (p0 W XXGp0) & GFp1 & FGp2 6(2) 5(2) n/a 6(3) (The above just show a few cases that were improved. There are many cases where ltl2dpa still produces smaller automata.) - The automaton postprocessor will now simplify acceptance conditions more aggressively, calling spot::simplify_acceptance() or spot::cleanup_acceptance() depending on the optimization level. - print_dot(), used to print automata in GraphViz's format, underwent several changes: * option "a", for printing the acceptance condition, is now enabled by default. Option "A", introduced in Spot 2.4, can be used to hide the acceptance condition in case you do not want it. This change of course affects the --dot option of all the command-line tools, as well as the various way to display automata using the Python bindings. * when option "1" is used to hide state names and force the display of state numbers, the actual state names is now moved to the "tooltip" field of the state. The SVG files produced by "dot -Tsvg" will show those as popups. This is also done for state labels of Kripke structures. * the output digraph is now named using the name of the automaton if available, or the empty string otherwise. (Previous versions used to call all digraphs "G".) This name appears as a tooltip in SVG figures when the mouse is over the acceptance condition. * a new option "u" hides "true states" behind "exiting transitions". This can be used to display alternating automata in a way many people expect. * a new option "K" cancels the effect of "k" (which uses state labels whenever possible). This is most useful when one want to force transition-labeling of a Kripke structure, where "k" is usually the default. - spot::twa_graph::merge_states() is a new method that merges states with the exact same outgoing edges. As it performs no reordering of the edges, it is better to call it when you know that the edges in the twa_graph are sorted (e.g. after a call to merge_edges()). - spot::twa_graph::purge_unreachable_states() now takes a function which is called with the new numbering of states. This is useful to update an external structure that references states of the twa that we want to purge. - spot::scc_filter() now automatically turns automata marked as inherently-weak into weak automata with state-based acceptance. The acceptance condition is set to Büchi unless the input had co-Büchi or t acceptance. spot::scc_filter_states() will pass inherently-weak automata to spot::scc_filter(). - spot::cleanup_parity() and spot::cleanup_parity_here() are smarter and now remove from the acceptance condition the parity colors that are not used in the automaton. - spot::contains() and spot::are_equivalent() can be used to check language containement between two automata or formulas. They are most welcome in Python, since we used to redefine them every now and them. Some examples are shown in https://spot.lrde.epita.fr/ipynb/contains.html - aut1->exclusive_word(aut2) is a new method that returns a word accepted by aut1 or aut2 but not both. The exclusive_run() variant will return. This is useful when comparing automata and looking for differences. See also https://spot.lrde.epita.fr/ipynb/contains.html - spot::complement_semidet(aut) is a new function that returns the complement of aut, where aut is a semideterministic automaton. The function uses the NCSB complementation algorithm proposed by F. Blahoudek, M. Heizmann, S. Schewe, J. Strejček, and MH. Tsai (TACAS'16). - spot::remove_alternation() was slightly improved on very-weak alternating automata: the labeling of the outgoing transitions in the resulting TGBA makes it more likely that simulation-based reductions will reduce it. - When applied to automata that are not WDBA-realizable, spot::minimize_wdba() was changed to produce an automaton recognizing a language that includes the original one. As a consequence spot::minimize_obligation() and spot::is_wdba_realizable() now only need one containement check instead of two. - Slightly improved log output for the SAT-based minimization functions. The CSV log files now include an additional column with the size of the reference automaton, and they now have a header line. These log files give more details and are more accurate in the case of incremental SAT-solving. Python: - New spot.jupyter package. This currently contains a function for displaying several arguments side by side in a Jupyter notebook. See https://spot.lrde.epita.fr/ipynb/alternation.html for some examples. - Strings are now implicitely converted into formulas when passed as arguments to functions that expect formulas. Previously this was done only for a few functions. - The Python bindings for sat_minimize() now have display_log and return_log options; these are demonstrated on the new https://spot.lrde.epita.fr/ipynb/satmin.html page. Bugs fixed: - Python *.py and *.so files are now always installed into the same directory. This was an issue on systems like Fedora that separate plateform-specific packages from non-plateform-specific ones. - print_dot() will correctly escape strings containing \n in HTML mode. - The HOA parser will now accept Alias: declarations that occur before AP:. - The option --allow-dups of randltl now works properly. - Converting generalized-co-Büchi to Streett using dnf_to_nca() could produce bogus automata if the input had rejecting SCCs. Deprecation notices: - The type spot::acc_cond::mark_t has been overhauled and uses a custom bit-vector to represent acceptance sets instead of storing everything in a "unsigned int". This change is to accomodate configure's --enable-max-accsets=N option and has several effect: * The following shortcuts are deprecated: acc_cond::mark_t m1 = 0U; acc_cond::mark_t m2 = -1U; instead, use: acc_cond::mark_t m1 = {}; acc_cond::mark_t m2 = acc_cond::mark_t::all(); * acc_cond::mark_t::value_t is deprecated. It is now only defined when --enable-max-accsets=32 (the default) and equal to "unsigned" for backward compatibility reasons. Backward incompatibilities: - Functions spot::parity_product() and spot::parity_product_or() were removed. The code was unused, hard to maintain, and bogus. - The output of print_dot() now include the acceptance condition. Add option "A" (supported since version 2.4) to cancel that. - Because genltl now supports LTL pattern with two argumens, using --format=%L may output two comma-separated integer. This is an issue if you used to produce CSV files using for instance: genltl --format='%F,%L,%f' ... Make sure to quote %L to protect the potential commas: genltl --format='%F,"%L",%f' ... - In Spot 2.5 and prior running "ltl2tgba --generic --det" on some formula would attempt to translate it as deterministic TGBA or determinize it into an automaton with parity acceptance. Version 2.5 introduced --parity to force parity acceptance on the output. This version finally gives --generic some more natural semantics: any acceptance condition can be used. -- Alexandre Duret-Lutz

1 0