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@lrde.epita.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