We are happy to announce the release of Spot 1.99.5.

You can find the new release at

http://www.lrde.epita.fr/dload/spot/spot-1.99.5.tar.gz

See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to spot@lrde.epita.fr.

As their names suggest, all the 1.99.x versions are intermediate releases before a Spot 2.0 release, expected in 2016. While each of them may fix bugs and bring additional features, the most important part is that they clean up the C++ and Python API. This clean up introduces a lot of backward incompatible changes, and you should expect more C++/Python API changes before the Spot 2.0 release. (The command-line tools are mostly unaffected.)

A list of newsworthy changes introduced by this release is given below.

New in spot 1.99.5 (2015-11-03)

Command-line tools:

* autfilt has gained a --complement option. It currently works only for deterministic automata.

* By default, autfilt does not simplify automata (this has not changed), as if the --low --any options were used. But now, if one of --small, --deterministic, or --any is given, the optimization level automatically defaults to --high (unless specified otherwise). For symmetry, if one of --low, --medium, or --high is given, then the translation intent defaults to --small (unless specified otherwise).

* autfilt, dstar2tgba, ltlcross, and ltldo now trust the (supported) automaton properties declared in any HOA file they read. This can be disabled with option --trust-hoa=no.

* ltlgrind FILENAME[/COL] is now the same as ltlgrind -F FILENAME[/COL] for consistency with ltlfilt.

Library:

* dtgba_complement() was renamed to dtwa_complement(), moved to complement.hh, and its purpose was restricted to just completing the automaton and complementing its acceptance condition. Any further acceptance condition transformation can be done with to_generalized_buchi() or remove_fin().

* The remove_fin() has learnt how to better deal with automata that are declared as weak. This code was previously in dtgba_complement().

* scc_filter_states() has learnt to remove useless acceptance marks that are on transitions between SCCs, while preserving state-based acceptance. The most visible effect is in the output of "ltl2tgba -s XXXa": it used to have 5 accepting states, it now has only one. (Changing removing acceptance of those 4 states has no effect on the language, but it speeds up some algorithms like NDFS-based emptiness checks, as discussed in our Spin'15 paper.)

* The HOA parser will diagnose any version that is not v1, unless it looks like a subversion of v1 and no parse error was detected.

* The way to pass option to the automaton parser has been changed to make it easier to introduce new options. One such new option is "trust_hoa": when true (the default) supported properties declared in HOA files are trusted even if they cannot be easily be verified. Another option "raise_errors" now replaces the method automaton_stream_parser::parse_strict().

* The output of the automaton parser now include the list of parse errors (that does not have to be passed as a parameters) and the input filename (making the output of error messages easier).

* The following renamings make the code more consistent: ltl_simplifier -> tl_simplifier tgba_statistics::transitions -> twa_statistics::edges tgba_sub_statistics::sub_transitions -> twa_sub_statistics::transitions tgba_run -> twa_run reduce_run -> twa_run::reduce replay_tgba_run -> twa_run::replay print_tgba_run -> operator<< tgba_run_to_tgba -> twa_run::as_twa format_parse_aut_errors -> parsed_aut::format_errors twa_succ_iterator::current_state -> twa_succ_iterator::dst twa_succ_iterator::current_condition -> twa_succ_iterator::cond twa_succ_iterator::current_acceptance_conditions -> twa_succ_iterator::acc ta_succ_iterator::current_state -> ta_succ_iterator::dst ta_succ_iterator::current_condition -> ta_succ_iterator::cond ta_succ_iterator::current_acceptance_conditions -> ta_succ_iterator::acc

Python:

* The minimum supported Python version is now 3.3. * Add bindings for complete() and dtwa_complement() * Formulas now have a custom __format__ function. See https://spot.lrde.epita.fr/tut01.html for examples. * The Debian package is now compiled for all Python3 versions supported by Debian, not just the default one. * Automata now have get_name()/set_name() methods. * spot.postprocess(aut, *options), or aut.postprocess(*options) simplify the use of the spot.postprocessor object. (Just like we have spot.translate() on top of spot.translator().) * spot.automata() and spot.automaton() now have additional optional arguments: - timeout: to restrict the runtime of commands that produce automata - trust_hoa: can be set to False to ignore HOA properties that cannot be easily verified - ignore_abort: can be set to False if you do not want to skip automata ended with --ABORT--.

Documentation:

* There is a new page showing how to use spot::postprocessor to convert any type of automaton to Büchi. https://spot.lrde.epita.fr/tut30.html

Bugs fixed:

* Work around some weird exception raised when using the randltlgenerator under Python 3.5. * Recognize "nullptr" formulas as None in Python. * Fix compilation of bench/stutter/ * Handle saturation of formula reference counts. * Fix typo in the Python code for the CGI server. * "randaut -Q0 1" used to segfault. * "ltlgrind -F FILENAME/COL" did not preserve other CSV columns. * "ltlgrind --help" did not document FORMAT. * unabbreviate could easily use forbidden operators. * "autfilt --is-unambiguous" could fail to detect the nonambiguity of some automata with empty languages. * When parsing long tokens (e.g, state labels representing very large strings) the automaton parser could die with "input buffer overflow, can't enlarge buffer because scanner uses REJECT"