26 Aug
2015
26 Aug
'15
3:04 p.m.
We are pleased to announce the release of Spot 1.99.3.
This maintenance release fixes several bugs, and finally merges some
of the important code that was duplicated between the handling of
automata in ltl2dstar's format, and automata in the HOA format.
http://www.lrde.epita.fr/dload/spot/spot-1.99.3.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions. Please direct any feedback to <spot(a)lrde.epita.fr>fr>.
New in spot 1.99.3 (2015-08-26)
* The CGI script for LTL translation offers a HOA download link
for each generated automaton.
* The html documentation now includes a HTML copies of the man
pages, and HTML copies of the Python notebooks.
* scc_filter(aut, true) does not remove Fin marks from rejecting
SCCs, but it now does remove Fin marks from transitions between
SCCs.
* All the unabbreviation functions (unabbreviate_ltl(),
unabbreviate_logic(), unabbreviate_wm()) have been merged into a
single unabbreviate() function that takes a string representing
the list of operators to remove among "eFGiMRW^" where 'e',
'i',
and '^' stand respectively for <->, ->, and xor.
This feature is also available via ltlfilt --unabbreviate.
* In LTL formulas, atomic propositions specified using double-quotes
can now include \" and \\. (This is more consistent with the HOA
format, which already allows that.)
* All the conversion routines that were written specifically for
ltl2dstar's output format (DRA->BA & DRA->TGBA) have been ported
to the new TωA structure supporting the HOA format. The DRA->TGBA
conversion was reimplemented in the previous release, and the
DRA->BA conversion has been reimplemented in this release (but it
is still restricted to state-based acceptance). All these
conversions are called automatically by to_generalized_buchi()
or remove_fin() so there should be no need to call them directly.
As a consequence:
- "autfilt --remove-fin" or "autfilt -B" is better at converting
state-based Rabin automata: it will produce a DBA if the input is
deterministic and DBA-realizable, but will preserve as much
determinism as possible otherwise.
- a lot of obsolete code that was here only to support the old
conversion routines has been removed. (The number of lines
removed by this release is twice the number of lines added.)
- ltlcross now uses automata in ltl2dstar's format directly,
without converting them to Büchi (this makes the statistics
reported in CSV files more relevant).
- ltlcross no longer outputs additional columns about the size
of the input automaton in the case ltl2dstar's format is used.
- ltldo uses results in ltl2dstar's format directly, without
converting them to Büchi.
- dstar2tgba has been greatly simplified and now uses the
same output routines as all the other tools that output
automata. This implies a few minor semantic changes, for
instance --stats=%A used to output the number of acceptance
*pairs* in the input automaton, while it now outputs the
number of acceptance sets like in all the other tools.
* Bugs fixed
- Some acceptance conditions like Fin(0)|Fin(1)|Fin(2)&Inf(3)
were not detected as generalized-Rabin.
- Unknown arguments for print_hoa() (i.e., option -H in command-line
tools) are now diagnosed.
- The CGI script for LTL translation now forces transition-based
acceptance on WDBA-minimized automata when TGBA is requested.
- ltlgrind --help output had some options documented twice, or
in the wrong place.
- The man page for ltlcross had obsolete examples.
- When outputting atomic propositions in double quotes, the
escaping routine used by the two styles of LaTeX output was
slightly wrong. For instance ^ was incorrectly escaped, and
the double quotes where not always properly rendered.
- A spurious assertion was triggered by streett_to_generalized_buchi(),
but only when compiled in DEBUG mode.
- LTL formula rewritten in Spin's syntax no longer have their ->
and <-> rewritten away.
- Fix some warnings reported by the development version of GCC 6.
- The spot.translate() function of the Python binding had a typo
preventing the use of 'low'/'medium'/'high' as argument.
- Fix spurious failure of uniq.test under different locales.
- ltlcross now recovers from out-of-memory errors during
state-space products.
- bitvect.test was failing on 32bit architectures with
assertions enabled because of a bug in the test case.
--
Alexandre Duret-Lutz