15 Mar
2017
15 Mar
'17
1:29 p.m.
We are happy to announce the release of Spot 2.3.2.
This is a maintenance release that only contains minor bug fixes, and
minor enhancements, as listed below.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.3.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>fr>.
New in spot 2.3.2 (2017-03-15)
Tools:
- In tools that output automata, the number of atomic propositions
can be output using --stats=%x (output automaton) or --stats=%X
(input automaton). Additional options can be passed to list
atomic propositions instead of counting them. Tools that output
formulas also support --format=%x for this purpose.
Python:
- The bdd_to_formula(), and to_generalized_buchi() functions can now
be called in Python.
Documentation:
- https://spot.lrde.epita.fr/tut11.html is a new page describing
how to build monitors in Shell, Python, or C++.
Bugs fixed:
- The tests using LTSmin's patched version of divine would fail
if the current (non-patched) version of divine was installed.
- Because of a typo, the output of --stats='...%P...' was correct
only if %p was used as well.
- genltl was never meant to have (randomly attributed) short
options for --postive and --negative.
- a typo in the code for transformating transition-based acceptance
to state-based acceptance could cause a superfluous initial state
to be output in some cases (the result was still correct).
- 'ltl2tgba --any -C -M ...' would not complete automata.
- While not incorrect, the HOA properties output by 'ltl2tgba -M'
could be 'inherently-weak' or 'terminal', while 'ltl2tgba -M
-D'
would always report 'weak' automata. Both variants now report the
most precise between 'weak' or 'terminal'.
- spot::twa_graph::set_univ_init_state() could not be called with
an initializer list.
- The Python wrappers for spot::twa_graph::state_from_number and
spot::twa_graph::state_acc_sets were broken in 2.3.
- Instantiating an emptiness check on an automaton with unsupported
acceptance condition should throw an exception. This used to be
just an assertion, disabled in release builds; the difference
matters for the Python bindings.
Deprecation notice:
- Using --format=%a to print the number of atomic propositions in
ltlfilt, genltl, and randltl still works, but it is not documented
anymore and should be replaced by the newly-introduced --format=%x
for consistency with tools producing automata, where %a means
something else.
--
Alexandre Duret-Lutz