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 &lt;spot(a)lrde.epita.fr&gt;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