4 Dec
2015
4 Dec
'15
12:03 p.m.
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(a)lrde.epita.fr>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.
--
Alexandre Duret-Lutz