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(a)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.
--
Alexandre Duret-Lutz
