We are happy to announce the release of Spot 2.7
Someone recently reported some release-worthy bug, and unfortunately we
do not have time to prepare a 2.6.4 release by cherry-picking the bug
fixes from the development branch. So here is Spot 2.7 instead, with
some minor new features and backward-incompatible changes done over the
last 5 months. See the list below for details.
This release contains contributions by Maximilien Colange, Etienne
Renault, and myself.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.7.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
As always, please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.7 (2018-12-11)
Command-line tools:
- ltlsynt now has three algorithms for synthesis:
--algo=sd is the historical one. The automaton of the formula
is split to separate inputs and outputs, then
determinized (with Safra construction).
--algo=ds the automaton of the formula is determinized (Safra),
then split to separate inputs and outputs.
--algo=lar translate the formula to a deterministic automaton
with an arbitrary acceptance condition, then turn it
into a parity automaton using LAR, and split it.
In all three cases, the obtained parity game is solved using
Zielonka algorithm. Calude's quasi-polynomial time algorithm has
been dropped as it was not used.
- ltlfilt learned --liveness to match formulas representing liveness
properties.
- the --stats= option of tools producing automata learned how to
tell if an automaton uses universal branching (%u), or more
precisely how many states (%[s]u) or edges (%[e]u) use universal
branching.
Python:
- spot.translate() and spot.postprocess() now take an xargs=
argument similar to the -x option of ltl2tgba and autfilt, making
it easier to fine tune these operations. For instance
ltl2tgba 'GF(a <-> XXa)' --det -x gf-guarantee=0
would be written in Python as
spot.translate('GF(a <-> XXa)', 'det', xargs='gf-guarantee=0')
(Note: those extra options are documented in the spot-x(7) man page.)
- spot.is_generalized_rabin() and spot.is_generalized_streett() now return
a tuple (b, v) where b is a Boolean, and v is the vector of the sizes
of each generalized pair. This is a backward incompatible change.
Library:
- The LTL parser learned syntactic sugar for nested ranges of X
using the X[n], F[n:m], and G[n:m] syntax of TSLF. (These
correspond to the next!, next_e!, and next_a! operators of PSL,
but we do not support those under these names currently.)
X[6]a = XXXXXXa
F[2:4]a = XX(a | X(a | Xa))
G[2:4]a = XX(a & X(a & Xa))
The corresponding constructors (for C++ and Python) are
formula::X(unsigned, formula)
formula::F(unsigned, unsigned, formula)
formula::G(unsigned, unsigned, formula)
- spot::unabbreviate(), used to rewrite away operators such as M or
W, learned to use some shorter rewritings when an argument (e) is
a pure eventuality or (u) is purely universal:
Fe = e
Gu = u
f R u = u
f M e = F(f & e)
f W u = G(f | u)
- The twa_graph class has a new dump_storage_as_dot() method
to show its data structure. This is more conveniently used
as aut.show_storage() in a Jupyter notebook. See
https://spot.lrde.epita.fr/ipynb/twagraph-internals.html
- spot::generic_emptiness_check() is a new function that performs
emptiness checks of twa_graph_ptr (i.e., automata not built
on-the-fly) with an *arbitrary* acceptance condition. Its sister
spot::generic_emptiness_check_scc() can be used to decide the
emptiness of an SCC. This is now used by
twa_graph_ptr::is_empty(), twa_graph_ptr::intersects(), and
scc_info::determine_unknown_acceptance().
- The new function spot::to_parity() translates an automaton with
arbitrary acceptance condition into a parity automaton, based on a
last-appearance record (LAR) construction. (It is used by ltlsynt
but not yet by autfilt or ltl2tgba.)
- The new function is_liveness() and is_liveness_automaton() can be
used to check whether a formula or an automaton represents a
liveness property.
- Two new functions count_univbranch_states() and
count_univbranch_edges() can help measuring the amount of
universal branching in alternating automata.
Bugs fixed:
- translate() would incorrectly mark as stutter-invariant
some automata produced from formulas of the form X(f...)
where f... is syntactically stutter-invariant.
- acc_cond::is_generalized_rabin() and
acc_cond::is_generalized_streett() did not recognize the cases
were a single generalized pair is used.
- The pair of acc_cond::mark_t returned by
acc_code::used_inf_fin_sets(), and the pair (bool,
vector_rs_pairs) by acc_cond::is_rabin_like() and
acc_cond::is_streett_like() were not usable in Python.
- Many object types had __repr__() methods that would return the
same string as __str__(), contrary to Python usage where repr(x)
should try to show how to rebuild x. The following types have
been changed to follow this convention:
spot.acc_code
spot.acc_cond
spot.atomic_prop_set
spot.formula
spot.mark_t
spot.twa_run (__repr__ shows type and address)
spot.twa_word (likewise, but _repr_latex_ used in notebooks)
Note that this you were relying on the fact that Jupyter calls
repr() to display returned values, you may want to call print()
explicitely if you prefer the old representation.
- Fix compilation under Cygwin and Alpine Linux, both choking
on undefined secure_getenv().
