We are happy to announce the release of Spot 1.99.6.

You can find the new release here:

http://www.lrde.epita.fr/dload/spot/spot-1.99.6.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.6 (2015-12-04)

Command-line tools:

* autfilt has two new filters: --is-weak and --is-terminal.

* autfilt has a new transformation: --decompose-strength, implementing the decomposition of our TACAS'13 paper. A demonstration of this feature via the Python bindings can be found at https://spot.lrde.epita.fr/ipynb/decompose.html

* All tools that output HOA files accept a --check=strength option to request automata to be marked as "weak" or "terminal" as appropriate. Without this option, these properties may only be set as a side-effect of running transformations that use this information.

Library:

* Properties of automata (like the "properties:" line of the HOA format) are stored as bits whose interpretation is True=yes, False=maybe. Having getters like "aut->is_deterministic()" or "aut->is_unambiguous()" was confusing, because there are separate functions "is_deterministic(aut)" and "is_unambiguous(aut)" that do actually check the automaton. The getters have been renamed to avoid confusion, and get names more in line with the HOA format.

- twa::has_state_based_acc() -> twa::prop_state_acc() - twa::prop_state_based_acc(bool) -> twa::prop_state_acc(bool) - twa::is_inherently_weak() -> twa::prop_inherently_weak() - twa::is_deterministic() -> twa::prop_deterministic() - twa::is_unambiguous() -> twa::prop_unambiguous() - twa::is_stutter_invariant() -> twa::prop_stutter_invariant() - twa::is_stutter_sensitive() -> twa::prop_stutter_sensitive()

The setters have the same names as the getters, except they take a Boolean argument. This argument used to be optionnal (defaulting to True), but it no longer is.

* Automata now support the "weak" and "terminal" properties in addition to the previously supported "inherently-weak".

* By default the HOA printer tries not to bloat the output with properties that are redundant and probably useless. The HOA printer now has a new option "v" (use "-Hv" from the command line) to output more verbose "properties:". This currently includes outputing "no-univ-branch", outputting "unambiguous" even for automata already tagged as "deterministic", and "inherently-weak" or "weak" even for automata tagged "weak" or "terminal".

* The HOA printer has a new option "k" (use "-Hk" from the command line) to output automata using state labels whenever possible. This is useful to print Kripke structures.

* The dot output will display pair of states when displaying an automaton built as an explicit product. This works in IPython with spot.product() or spot.product_or() and in the shell with autfilt's --product or --product-or options.

* The print_dot() function supports a new option, +N, where N is a positive integer that will be added to all set numbers in the output. This is convenient when displaying two automata before building their product: use +N to shift the displayed sets of the second automaton by the number of acceptance sets N of the first one.

* The sat minimization for DTwA now does a better job at selecting reference automata when the output acceptance is the the same as the input acceptance. This can provide nice speedups when tring to syntethise larged automata with different acceptance conditions.

* Explicit Kripke structures (i.e., stored as explciti graphs) have been rewritten above the graph class, using an interface similar to the twa class. The new class is called kripke_graph. The ad hoc Kripke parser and printer have been removed, because we can now use print_hoa() with the "k" option to print Kripke structure in the HOA format, and furthermore the parse_aut() function now has an option to load such an HOA file as a kripke_graph.

* The HOA parser now accepts identifier, aliases, and headernames containing dots, as this will be allowed in the next version of the HOA format.

* Renamings: is_guarantee_automaton() -> is_terminal_automaton() tgba_run -> twa_run twa_word::print -> operator<< dtgba_sat_synthetize() -> dtwa_sat_synthetize() dtgba_sat_synthetize_dichotomy() -> dtwa_sat_synthetize_dichotomy()

Python:

* Add bindings for is_unambiguous(). * Better interface for sat_minimize().

Bug fixes:

* the HOA parser was ignoring the "unambiguous" property. * --dot=Bb should work like --dot=b, allowing us to disable a B option set via an environment variable.