We are happy to announce the release of Spot 2.10
Spot is a C++17 for LTL and ω-automata manipulation, with
applications to model checking and reactive synthesis.
This is a major release that has been under development for 19 months.
It contains new features contributed by Jérôme Dubois, Antoine Martin,
Étienne Renault, Florian Renkin, Philipp Schlehuber, and myself.
A summary of those changes is given at the end of this email.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.10.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
Please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.10 (2021-11-13)
Build:
- Spot is now built in C++17 mode, so you need at least GCC 7 or
clang 5 to compile it. The current versions of all major linux
distributions ship with at least GCC 7.4, so this should not be a
problem. There is also an --enable-c++20 option to configure in
case you want to force a build of Spot in C++20 mode.
Command-line tools:
- ltlsynt has been seriously overhauled, while trying to
preserve backward compatibility. Below is just a summary
of the main user-visible changes. Most of the new options
are discussed on https://spot-dev.lrde.epita.fr/ltlsynt.html
+ ltlsynt now accepts only one of the --ins or --outs options to
be given and will deduce the value of the other one.
+ ltlsynt learned --print-game-hoa to output its internal parity
game in the HOA format (with an extension described below).
+ ltlsynt --aiger option now takes an optional argument indicating
how the bdd and states are to be encoded in the aiger output.
The option has to be given in the form
ite|isop|both[+ud][+dc][+sub0|sub1|sub2] where the first only
obligatory argument decides whether "if-then-else" ("ite") or
irreducible-sum-of-products ("isop") is to be used. "both"
executes both strategies and retains the smaller circuits. The
additional options are for fine-tuning. "ud" also encodes the
dual of the conditions and retains the smaller circuits. "dc"
computes if for some inputs we do not care whether the output is
high or low and try to use this information to compute a smaller
circuit. "subX" indicates different strategies to find common
subexpressions, with "sub0" indicating no extra computations.
+ ltlsynt learned --verify to check the computed strategy or aiger
circuit against the specification.
+ ltlsynt now has a --decompose=yes|no option to specify if
the specification should be decomposed into independent
sub-specifications, the controllers of which can then be glued
together to satisfy the input specification.
(cf. [finkbeiner.21.nfm] in doc/spot.bib)
+ ltlsynt learned --simplify=no|bisim|bwoa|sat|bisim-sat|bwoa-sat
to specifies how to simplify the synthesized controler.
- ltl2tgba, autfilt, dstar2tgba, and randaut learned a --buchi
option, or -b for short. This outputs Büchi automata without
forcing state-based acceptance.
The following aliases have also been added for consistency:
--gba is an alias for --tgba, because the "t" of --tgba is
never forced.
--sba is an alias for -B/--ba, because -B really
implies -S and that is not clear from --ba.
As a consequence of the introduction of --sba, the option
--sbacc (an alias for --state-based-acceptance) cannot be
abbreviated as --sba anymore.
- autfilt learned a --kill-states=NUM[,NUM...] option.
- ltlcross, autcross, ltldo have learned shorthands for
the commands of Owl 21.0. For instance running
ltlcross 'owl-21 ltl2nba' ...
is equivalent to running
ltlcross '{owl-21 ltl2nba}owl-21 ltl2nba -f %f>%O' ...
Library:
- Spot now provides convenient functions to create and solve games.
(twaalgos/game.hh) and some additional functions for reactive
synthesis (twaalgos/synthesis.hh, twaalgos/mealy_machine.hh).
- A new class called aig represent an and-inverter-graphs, and is
currently used during synthesis. (twaalgos/aiger.hh)
- Some new *experimental* classes, called "twacube" and "kripkecube"
implement a way to store automata or Kripke structures without
using BDDs as labels. Instead they use a structure called cube,
that can only encode a conjunction of litterals. Avoiding BDDs
(or rather, avoiding the BuDDy library) in the API for automata
makes it possible to build multithreaded algorithms.
/!\ Currently these classes should be considered as experimental,
and their API is very likely to change in a future version.
Functions like twacube_to_twa(), twa_to_twacube(), can be used
to bridge between automata with BDD labels, and automata with
cube labels.
In addition to the previous conversion, we implemented various
state-of-the-art multi-threaded emptiness-check algorithms:
[bloemen.16.ppopp], [bloemen.16.hvc], [evangeslita.12.atva],
[renault.13.lpar], [holzmann.11.ieee] (see doc/spot.bib).
The mc_instanciator class provides an abstraction for launching,
pinning, and stopping threads inside of parallel model-checking
algorithms.
The class ltsmin_model class, providing support for loading
various models that follow ltsmin's PINS interinterface, has
been adjusted and can now produce either a kripke instance, or
a kripkecube instance.
- The postprocessor::set_type() method can now accept
options postprocessor::Buchi and postprocessor::GeneralizedBuchi.
These syntaxes is more homogeneous with the rest of the supported
types. Note that postprocessor::BA and postprocessor::TGBA, while
still supported and not yet marked as deprecated, are best avoided
in new code.
postprocessor::set_type(postprocessor::TGBA)
can be replaced by
postprocessor::set_type(postprocessor::GeneralizedBuchi)
and
postprocessor::set_type(postprocessor::BA)
by
postprocessor::set_type(postprocessor::Buchi)
postprocessor::set_pref(postprocessor::Small
| postprocessor::SBAcc)
Note that the old postprocessor::BA option implied state-based
acceptance (and was unique in that way), but the new
postprocessor::Buchi specifies Büchi acceptance without requiring
state-based acceptance (something that postprocessor did not
permit before).
- Translations for formulas such as FGp1 & FGp2 &...& FGp32 which
used to take ages are now instantaneous. (Issue #412.)
- remove_fin() learned to remove more unnecessary edges by using
propagate_marks_vector(), both in the general case and in the
Rabin-like case.
- simplify_acceptance() learned to simplify acceptence formulas of
the form Inf(x)&Inf(y) or Fin(x)|Fin(y) when the presence of x
always implies that of y. (Issue #406.)
- simplifiy_acceptance_here() and propagate_marks_here() learned to
use some patterns of the acceptance condition to remove or add
(depending on the function) colors on edges. As an example, with
a condition such as Inf(0) | Fin(1), an edge labeled by {0,1} can
be simplied to {0}, but the oppose rewriting can be useful as
well. (Issue #418.)
- The parity_game class has been removed, now any twa_graph_ptr that
has a "state-player" property is considered to be a game.
- the "state-player" property is output by the HOA printer, and read
back by the automaton parser, which means that games can be saved
and loaded.
- print_dot() will display states from player 1 using a diamond
shape.
- print_dot() learned to display automata that correspond to Mealy
machines specifically.
- print_dot() has a new option "i" to define id=... attributes for
states (S followed by the state number), edges (E followed by the
edge number), and SCCs (SCC followed by SCC number). The option
"i(graphid)" will also set the id of the graph. These id
attributes are useful if an automaton is converted into SVG and
one needs to refer to some particular state/edge/SCC with CSS or
javascript. See https://spot.lrde.epita.fr/oaut.html#SVG-and-CSS
- spot::postproc has new configuration variables that define
thresholds to disable some costly operation in order to speedup
the processing of large automata. (Those variables are typically
modified using the -x option of command-line tools, and are all
documented in the spot-x(7) man page.)
wdba-det-max Maximum number of additional states allowed in
intermediate steps of WDBA-minimization. If the
number of additional states reached in the
powerset construction or in the followup products
exceeds this value, WDBA-minimization is aborted.
Defaults to 4096. Set to 0 to disable. This limit
is ignored when -D used or when det-max-states is
set.
simul-max Number of states above which simulation-based
reductions are skipped. Defaults to 4096. Set
to 0 to disable. This also applies to the
simulation-based optimization of the
determinization algorithm.
simul-trans-pruning
For simulation-based reduction, this is the
number of equivalence classes above which
transition-pruning for non-deterministic automata
is disabled. Defaults to 512. Set to 0 to
disable. This applies to all simulation-based
reduction, as well as to the simulation-based
optimization of the determinization algorithm.
Simulation-based reduction perform a number of
BDD implication checks that is quadratic in the
number of classes to implement transition pruning.
dpa-simul Set to 0/1 to disable/enable simulation-based
reduction performed after running a Safra-like
determinization to optain a DPA. By default, it is
only disabled with --low or if simul=0.
dba-simul Set to 0/1 to disable/enable simulation-based
reduction performed after running the
powerset-like construction (enabled by option
tba-det) to obtain a DBA. By default, it is
only disabled with --low or if simul=0.
spot::translator additionally honor the following new variables:
tls-max-states Maximum number of states of automata involved in
automata-based implication checks for formula
simplifications. Defaults to 64.
exprop When set, this causes the core LTL translation to
explicitly iterate over all possible valuations of
atomic propositions when considering the successors
of a BDD-encoded state, instead of discovering
possible successors by rewriting the BDD as a sum of
product. This is enabled by default for --high,
and disabled by default otherwise. When unambiguous
automata are required, this option forced and
cannot be disabled. (This feature is not new, but
was not tunable before.)
- In addition the to above new variables, the default value for
ba-simul (controling how degeneralized automata are reduced) and
for det-simul (simulation-based optimization of the
determinization) is now equal to the default value of simul. This
changes allows "-x simul=0" to disable all of "ba-simul",
"dba-simul", "dpa-simul", and "det-simul" at once.
- tgba_powerset() now takes an extra optional argument to specify a
list of accepting sinks states if some are known. Doing so can
cut the size of the powerset automaton by 2^|sinks| in favorable
cases.
- twa_graph::merge_edges() had its two passes swapped. Doing so
improves the determinism of some automata.
- twa_graph::kill_state(num) is a new method that removes the
outgoing edge of some state. It can be used together with
purge_dead_states() to remove selected states.
- The new functions reduce_direct_sim(), reduce_direct_cosim() and
reduce_iterated() (and their state based acceptance version,
reduce_direct_sim_sba(), reduce_direct_cosim_sba() and
reduce_iterated_sba()), are matrix-based implementation of
simulation-based reductions. This new version is faster
than the signature-based BDD implementation in most cases,
however there are some cases it does not capture yet.. By
default, the old one is used. This behavior can be changed by
setting SPOT_SIMULATION_REDUCTION environment variable or using
the "-x simul-method=..." option (see spot-x(7)).
- The automaton parser will now recognize lines of the form
#line 10 "filename"
that may occur *between* the automata of an input stream to specify
that error messages should be emitted as if the next automaton
was read from "filename" starting on line 10. (Issue #232)
- The automaton parser for HOA is now faster at parsing files where
a label is used multiple times (i.e., most automata): it uses a
hash table to avoid reconstructing BDDs corresponding to label
that have already been parsed. This trick was already used in the
never claim parser.
- spot::twa_graph::merge_states() will now sort the vector of edges
before attempting to detect mergeable states. When merging states
with identical outgoing transitions, it will now also consider
self-looping transitions has having identical destinations.
Additionally, this function now returns the number of states that
have been merged (and therefore removed from the automaton).
- spot::zielonka_tree and spot::acd are new classes that implement the
Zielonka Tree and Alternatic Cycle Decomposition, based on a paper
by Casares et al. (ICALP'21). Those structures can be used to
paritize any automaton, and more. The graphical rendering of ACD
in Jupyter notebooks is Spot's first interactive output. See
https://spot.lrde.epita.fr/ipynb/zlktree.html for more.
Python:
- Bindings for functions related to games.
See https://spot.lrde.epita.fr/ipynb/games.html and
https://spot.lrde.epita.fr/tut40.html for examples.
- Bindings for functions related to synthesis and aig-circuits.
See https://spot.lrde.epita.fr/ipynb/synthesis.html
- spot::twa::prop_set was previously absent from the Python
bindings, making it impossible to call make_twa_graph() for copying
a twa. It is now available as spot.twa_prop_set (issue #453).
Also for convenience, the twa_graph.__copy__() method, called by
copy.copy(), will duplicate a twa_graph (issue #470).
Bugs fixed:
- tgba_determinize() could create parity automata using more colors
than necessary. (Related to issue #298)
- There were two corners cases under which sat_minimize() would
return the original transition-based automaton when asked to
produce state-based output without changing the acceptance
condition.
Deprecation notices:
- twa_graph::defrag_states() and digraph::defrag_states() now take
the renaming vector by reference instead of rvalue reference. The
old prototype is still supported but will emit a deprecation
warning.
