We are happy to announce the release of Spot 1.99.8. This release includes contributions from Alexandre Lewkowicz, Étienne Renault and myself.

You can find the new release here:

http://www.lrde.epita.fr/dload/spot/spot-1.99.8.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. 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 unfortunately introduces a lot of backward incompatible changes, but the good news is that the largest changes are now over, and the upcoming effort should mainly focus on improving the documentation. If you have some old code compatible with 1.2.6 and want to port it to the upcoming 2.0 version, you may consider working with 1.99.8 already.

A list of newsworthy changes introduced by this release is given below. In addition to that, let me also announce the creation of

http://spot-sandbox.lrde.epita.fr/

a Jupyter installation that is free to use for experimenting with Spot's command-line tools (via an interactive shell) or Python bindings (via IPython notebooks) without having to install Spot.

New in spot 1.99.8 (2016-02-18)

Command-line tools:

* ltl2tgba now also support the --generic option (already supported by ltldo and autfilt) to lift any restriction on the acceptance condition produced. This option now has a short version: -G.

* ltl2tgba and autfilt have learnt how to determinize automata. For this to work, --generic acceptance should be enabled (this is the default for autfilt, but not for ltl2tgba).

"ltl2tgba -G -D" will now always outpout a deterministic automaton. It can be an automaton with transition-based parity acceptance in case Spot could not find a deterministic automaton with (maybe generalized) Büchi acceptance.

"ltl2tgba -D" is unchanged (the --tgba acceptance is the default), and will output a deterministic automaton with (generalized) Büchi acceptance only if one could be found. Otherwise a non-deterministic automaton is output, but this does NOT mean that no deterministic Büchi automaton exist for this formula. It only means Spot could not find it.

"autfilt -D" will determinize any automaton, because --generic acceptance is the default for autfilt.

"autfilt -D --tgba" will behave like "ltl2tgba -D", i.e., it may fail to find a deterministic automaton (even if one exists) and return a nondeterministic automaton.

* "autfilt --complement" now also works for non-deterministic automata but will output a deterministic automaton. "autfilt --complement --tgba" will likely output a nondeterministic TGBA.

* autfilt has a new option, --included-in, to filter automata whose language are included in the language of a given automaton.

* autfilt has a new option, --equivalent-to, to filter automata that are equivalent (language-wise) to a given automaton.

* ltlcross has a new option --determinize to instruct it to complement non-deterministic automata via determinization. This option is not enabled by default as it can potentially be slow and generate large automata. When --determinize is given, option --product=0 is implied, since the tests based on products with random state-space are pointless for deterministic automata.

* ltl2tgba and ltldo now support %< and %> in the string passed to --stats when reading formulas from a CSV file.

* ltlfilt's option --size-min=N, --size-max=N, --bsize-min=N, and --bsize-max=N have been reimplemented as --size=RANGE and --bsize=RANGE. The old names are still supported for backward compatibility, but they are not documented anymore.

* ltlfilt's option --ap=N can now take a RANGE as parameter.

* autfilt now has a --ap=RANGE option to filter automata by number of atomic propositions.

Library:

* Building products with different dictionaries now raise an exception instead of using an assertion that could be disabled.

* The load_ltsmin() function has been split in two. Now you should first call ltsmin_model::load(filename) to create an ltsmin_model, and then call the ltsmin_model::kripke(...) method to create an automaton that can be iterated on the fly. The intermediate object can be queried about the supported variables and their types.

* print_dot() now accepts several new options: - use "<N" to specify a maximum number of states to output. Incomplete states are then marked appropriately. For a quick example, compare ltl2tgba -D 'Ga | Gb | Gc' -d'<3' with ltl2tgba -D 'Ga | Gb | Gc' -d - use "C(color)" to specify the color to use for filling states. - use "#" to display the internal number of each transition - use "k" to use state-based labels when possible. This is similar to the "k" option already supported by print_hoa(), and is useful when printing Kripke structures.

* Option "k" is automatically used by print_dot() and print_hoa() when printing Kripke structures.

* print_dot() also honnor two new automaton properties called "highlight-edges" and "highlight-states". These are used to color a subset of edges or transitions.

* There is a new tgba_determinize() function. Despite its name, it in facts works on transition-based Büchi automaton, and will first degeneralize any automaton with generalized Büchi acceptance.

* The twa_safra_complement class has been removed. Use tgba_determinize() and dtwa_complement() instead.

* The twa::transition_annotation() and twa::compute_support_conditions() methods have been removed.

* The interface for all functions parsing formulas (LTL, PSL, SERE, etc.) has been changed to use an interface similar to the one used for parsing automata. These function now return a parsed_formula object that includes both a formula and a list of syntax errors.

Typically a function written as

spot::formula read(std::string input) { spot::parse_error_list pel; spot::formula f = spot::parse_infix_psl(input, pel); if (spot::format_parse_errors(std::cerr, input, pel)) exit(2); return f; }

should be updated to

spot::formula read(std::string input) { spot::parsed_formula pf = spot::parse_infix_psl(input); if (pf.format_errors(std::cerr)) exit(2); return pf.f; }

Python:

* The ltsmin interface has been binded in Python. It also comes with a %%dve cell magic to edit DiVinE models in the notebook. See https://spot.lrde.epita.fr/ipynb/ltsmin.html for a short example.

* spot.setup() sets de maximum number of states to display in automata to 50 by default, as more states is likely to be unreadable (and slow to process by GraphViz). This can be overridden by calling spot.setup(max_states=N).

* Automata now have methods to color selected states and transitions. See https://spot.lrde.epita.fr/ipynb/highlighting.html for an example.

Documentation:

* There is a new page giving informal illustrations (and extra pointers) for some concepts used in Spot. See https://spot.lrde.epita.fr/concepts.html

Bug fixes:

* Using ltl2tgba -U would fail to output the unambiguous property (regression introduced in 1.99.7) * ltlfilt, autfilt, randltl, and randaut could easily crash when compiled statically (i.e., with configure --disable-shared). * "1 U (a | Fb)" was not always simplified to "F(a | b)". * destroying the operands of an otf_product() before the product itself could crash.