16 Jul
2020
16 Jul
'20
10:34 a.m.
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>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