We are happy to announce the release of Spot 2.11.3. This is a
maintenance release that fixes bugs discovered after we released 2.11.2.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.11.3.tar.gz
See https://spot.lre.epita.fr/ for documentation and installation
instructions.
Please direct any feedback to <spot(a)lrde.epita.fr>.
⚠ Note that LRDE (EPITA's Research & Development Laboratory) has been
merged with another entity into something larger that is now called LRE
(EPITA's Research Laboratory). The removal of "development", is nothing
to worry about: we are still continuing to develop Spot as part of our
research. However a consequence is that this release contains a mix of
URLs in "lre.epita.fr" (for services that have already migrated to the
new name) and "lrde.epita.fr". If you find a URL ending in
"lrde.epita.fr" that does not work, please try without the "d".
New in spot 2.11.3 (2022-12-09)
Bug fixes:
- Automata-based implication checks, used to simplify formulas, were
slower than necessary because the translator was configured to
favor determinism unnecessarily. (Issue #521.)
- Automata-based implication checks for f&g and f|g could be
very slow when those n-ary operator had two many arguments.
They have been limited to 16 operands, but this value can be changed
with option -x tls-max-ops=N. (Issue #521 too.)
- Running ltl_to_tgba_fm() with an output_aborter (which is done
during automata-based implication checks) would leak memory on
abort.
- configure --with-pythondir should also redefine pyexecdir,
otherwise, libraries get installed in the wrong place on Debian.
(Issue #512.)
- The HOA parser used to silently declare unused and undefined states
(e.g., when the State: header declare many more states than the body
of the file). It now warns about those.
- 'autfilt -c ...' should display a match count even in presence of
parse errors.
- Calling solve_parity_game() multiple times on the same automaton
used to append the new strategy to the existing one instead of
overwriting it.
We are happy to announce the release of Spot 2.11.2
Spot 2.11.2 fix a couple of issues, and also add a few simple features
that have been requested since 2.11.1.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.11.2.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
Please direct any feedback to <spot(a)lrde.epita.fr>.
⚠ Note that LRDE (EPITA's Research & Development Laboratory) had been
merged with another entity into something larger that is now called
LRE (EPITA's Research Laboratory). The removal of "development", is
nothing to worry about: we are still continuing to develop Spot as
part of our research. However a consequence is that this release
contains a mix of URLs in "lre.epita.fr" (for services that have
already migrated to the new name) and "lrde.epita.fr". If you find a
URL ending in "lrde.epita.fr" that does not work, please try without
the "d".
New in spot 2.11.2 (2022-10-26)
Command-line tools:
- The --stats specifications %s, %e, %t for printing the number of
(reachable) states, edges, and transitions, learned to support
options [r], [u], [a] to indicate if only reachable, unreachable,
or all elements should be counted.
Library:
- spot::reduce_parity() now has a "layered" option to force all
transition in the same parity layer to receive the same color;
like acd_transform() would do.
Bugs fixed:
- Fix pkg-config files containing @LIBSPOT_PTHREAD@ (issue #520)
- spot::relabel_bse() was incorrectly relabeling some dependent
Boolean subexpressions in SERE. (Note that this had no
consequence on automata translated from those SERE.)
We are happy to announce the release of Spot 2.11.1
Spot 2.11 is a major release containing new feature and improvements
implemented over the last 11 months by Florian Rankin, Philipp
Schlehuber-Caissier, Antoine Martin, and myself. A detailled list of
changes is appended to this email.
Spot 2.11.1 fixes a couple of build issues discovered before I had time
to announce 2.11...
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.11.1.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
Please direct any feedback to <spot(a)lrde.epita.fr>.
⚠ Note that LRDE (EPITA's Research & Development Laboratory) had been
merged with another entity into something larger that is now called
LRE (EPITA's Research Laboratory). The removal of "development", is
nothing to worry about: we are still continuing to develop Spot as
part of our research. However a consequence is that this release
contains a mix of URLs in "lre.epita.fr" (for services that have
already migrated to the new name) and "lrde.epita.fr". If you find a
URL ending in "lrde.epita.fr" that does not work, please try without
the "d".
New in spot 2.11.1 (2022-10-10)
Bugs fixed:
- Fix a build issue preventing the update of website (issue #516).
- Fix a compilation error with clang-14 on FreeBSD (issue #515).
New in spot 2.11 (2022-10-08)
Build:
- configure will now diagnose situations where Python bindings will
be installed in a directory that is not part of Python's search
path. A new configure option --with-pythondir can be used to
modify this installation path. (Issue #512)
- A new configure option --enable-pthread enables the compilation of
Spot with -pthread, and render available the parallel version of
some algorithms. If Spot is compiled with -pthread enabled, any
user linking with Spot should also link with the pthread library.
In order to not break existing build setups using Spot, this
option is currently disabled by default in this release. We plan
to turn it on by default in some future release. Third-party
project using Spot may want to start linking with -pthread in
prevision for this change.
Command-line tools:
- autfilt has a new options --aliases=drop|keep to specify
if the HOA printer should attempt to preserve aliases
present in the HOA input. This defaults to "keep".
- autfilt has a new --to-finite option, illustrated on
https://spot.lrde.epita.fr/tut12.html
- ltlfilt has a new --sonf option to produce a formula's Suffix
Operator Normal Form, described in [cimatti.06.fmcad]. The
associated option --sonf-aps allows listing the newly introduced
atomic propositions.
- autcross learned a --language-complemented option to assist in the
case one is testing tools that complement automata. (issue #504).
- ltlsynt has a new option --tlsf that takes the filename of a TLSF
specification and calls syfco (which must be installed) to convert
it into an LTL formula.
- ltlsynt has a new option --from-pgame that takes a parity game in
extended HOA format, as used in the Synthesis Competition.
- ltlsynt has a new option --hide-status to hide the REALIZABLE or
UNREALIZABLE output expected by SYNTCOMP. (This line is
superfluous, because the exit status of ltlsynt already indicate
whether the formula is realizable or not.)
- ltlsynt has a new option --dot to request GraphViz output instead
of most output. This works for displaying Mealy machines, games,
or AIG circuits. See https://spot.lrde.epita.fr/ltlsynt.html for
examples.
- genaut learned the --cyclist-trace-nba and --cyclist-proof-dba
options. Those are used to generate pairs of automata that should
include each other, and are used to show a regression (in speed)
present in Spot 2.10.x and fixed in 2.11.
- genltl learned --eil-gsi to generate a familly a function whose
translation and simplification used to be very slow. In particular
genltl --eil-gsi=23 | ltlfilt --from-ltlf | ltl2tgba
was reported as taking 9 days. This is now instantaneous.
Library:
- The new function suffix_operator_normal_form() implements
transformation of formulas to Suffix Operator Normal Form,
described in [cimatti.06.fmcad].
- "original-classes" is a new named property similar to
"original-states". It maps an each state to an unsigned integer
such that if two classes are in the same class, they are expected
to recognize the same language. The "original-states" should be
prefered property when that integer correspond to some actual
state.
- tgba_determinize() learned to fill the "original-classes" property.
States of the determinized automaton that correspond to the same
subset of states of the original automaton belong to the same
class. Filling this property is only done on demand as it inccurs
a small overhead.
- sbacc() learned to take the "original-classes" property into
account and to preserve it.
- The HOA parser and printer learned to map the synthesis-outputs
property of Spot to the controllable-AP header for the Extended
HOA format used in SyntComp. https://arxiv.org/abs/1912.05793
- The automaton parser learned to parse games in the PGSolver format.
See the bottom of https://spot.lrde.epita.fr/ipynb/games.html for
an example.
- "aliases" is a new named property that is filled by the HOA parser
using the list of aliases declared in the HOA file, and then used
by the HOA printer on a best-effort basis. Aliases can be used to
make HOA files more compact or more readable. But another
possible application is to use aliases to name letters of a 2^AP
alphabet, in applications where using atomic propositions is
inconvenient.
- print_dot() learned option "@" to display aliases, as discussed
above.
- to_finite() is a new function that help interpreting automata
build from LTLf formula using the from_ltlf() function. It replace
the previously suggested method of removing and atomic proposition
and simpifying automata, that failed to deal with states without
successors. See updated https://spot.lrde.epita.fr/tut12.html
- the HOA parser learned to not ignore self-loops labeled with [f]
and to turn any state that have colors but no outgoing transitions
into a state with a [f] self-loop. This helps dealing with
automata containing states without successors, as in the output of
to_finite().
- purge_dead_states() will now also remove edges labeled by false
(except self-loops).
- When parsing formulas with a huge number of operands for an n-ary
operator (for instance 'p1 | p2 | ... | p1000') the LTL parser
would construct that formula two operand at a time, and the
formula constructor for that operator would be responsible for
inlining, sorting, deduplicating, ... all operands at each step.
This resulted in a worst-than-quadratic slowdown. This is now
averted in the parser by delaying the construction of such n-ary
nodes until all children are known.
- complement() used to always turn tautological acceptance conditions
into Büchi. It now only does that if the automaton is modified.
- The zielonka_tree construction was optimized using the same
memoization trick that is used in ACD. Additionally it can now be
run with additional options to abort when the tree as an unwanted
shape, or to turn the tree into a DAG.
- contains() can now take a twa as a second argument, not just a
twa_graph. This allows for instance to do contains(ltl, kripke)
to obtain a simple model checker (that returns true or false,
without counterexample).
- degeneralize() and degeneralize_tba() learned to work on
generalized-co-Büchi as well.
- product() learned that the product of two co-Büchi automata
is a co-Büchi automaton. And product_or() learned that the
"or"-product of two Büchi automata is a Büchi automaton.
- spot::postprocessor has a new extra option "merge-states-min" that
indicates above how many states twa_graph::merge_states() (which
perform a very cheap pass to fuse states with identicall
succesors) should be called before running simulation-based
reductions.
- A new function delay_branching_here(aut) can be used to simplify
some non-deterministic branching. If two transitions (q₁,ℓ,M,q₂)
and (q₁,ℓ,M,q₃) differ only by their destination state, and are
the only incoming transitions of their destination states, then q₂
and q₃ can be merged (taking the union of their outgoing
transitions). This is cheap function is automatically called by
spot::translate() after translation of a formula to GBA, before
further simplification. This was introduced to help with automata
produced from formulas output by "genltl --eil-gsi" (see above).
- spot::postprocessor has new configuration variable branch-post
that can be used to control the use of branching-postponement
(disabled by default) or delayed-branching (see above, enabled by
default). See the spot-x(7) man page for details.
- spot::postprocessor is now using acd_transform() by default when
building parity automata. Setting option "acd=0" will revert
to using "to_parity()" instead.
- to_parity() has been almost entirely rewritten and is a bit
faster.
- When asked to build parity automata, spot::translator is now more
aggressively using LTL decomposition, as done in the Generic
acceptance case before paritizing the result. This results in
much smaller automata in many cases.
- spot::parallel_policy is an object that can be passed to some
algorithm to specify how many threads can be used if Spot has been
compiled with --enable-pthread. Currently, only
twa_graph::merge_states() supports it.
Python bindings:
- The to_str() method of automata can now export a parity game into
the PG-Solver format by passing option 'pg'. See
https://spot.lrde.epita.fr/ipynb/games.html for an example.
Deprectation notice:
- spot::pg_print() has been deprecated in favor of spot::print_pg()
for consistency with the rest of the API.
Bugs fixed:
- calling twa_graph::new_univ_edge(src, begin, end, cond, acc) could
produce unexpected result if begin and end where already pointing
into the universal edge vector, since the later can be
reallocated during that process.
- Printing an alternating automaton with print_dot() using 'u' to
hide true state could produce some incorrect GraphViz output if
the automaton as a true state as part of a universal group.
- Due to an optimization introduces in 2.10 to parse HOA label more
efficiently, the automaton parser could crash when parsing random
input (not HOA) containing '[' (issue #509).
We are happy to announce the release of Spot 2.10.6
This is a maintenance release fixing an couple of bugs
reported or discovered over the last two weeks.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.10.6.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.6 (2022-05-18)
Bugs fixed:
- Fix compilation error on MacOS X.
- Using -Ffile/N to read column N of a CSV file would not reset the
/N specification for the next file.
- make_twa_graph() will now preserve state numbers when copying a
kripke_graph object. As a consequence, print_dot() and
print_hoa() will now use state numbers matching those of the
kripke_graph (issue #505).
- Fix several compilation warning introduced by newer versions
of GCC and Clang.
We are happy to announce the release of Spot 2.10.5
This is a maintenance release fixing an assortment of
minor bugs discovered over the last three months.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.10.5.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions. (The spot web site is not yet updated to point to 2.10.5,
but that should be fixed in the next days.)
Please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.10.5 (2022-05-03)
Bugs fixed:
- reduce_parity() produced incorrect results when applied to
automata with deleted edges.
- An optimization of Zielonka could result in incorrect results
in some cases.
- ltlsynt --print-pg incorrectly solved the game in addition to
printing it.
- ltlsynt would fail if only one of --ins or --outs was set, and
if it was set empty.
- Work around a portability issue in Flex 2.6.4 preventing
compilation on OpenBSD.
- Do not use the seq command in test cases, it is not available
everywhere.
- Do not erase the previous contents of the PYTHONPATH environment
variable when running tests, prepend to it instead.
- Simplify Debian instructions for LTO build to work around newer
libtool version.
- Fix invalid read in digraph::sort_edges_of_(), currently unused in
Spot.
We are happy to announce the release of Spot 2.10.4
This is a maintenance release fixing some very old memory
leaks discovered in the Python bindings.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.10.4.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.4 (2022-02-01)
Bug fixed:
- Fix memory leaks in Python bindings for several iteration objects.
This occured while itering on twa_graph.out(), twa_graph.edges(),
twa_graph.univ_dests(), kripke_graph.out(), kripke_graph.edges(),
mark_t.sets(), scc_info.edges_of(), scc_info.inner_edges_of(), and
on an scc_info instance.
We are happy to announce the release of Spot 2.10.3
This is a maintenance release fixing a few bugs discovered
since the last release.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.10.3.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.3 (2022-01-15)
Bugs fixed:
- On automata where the absence of color is not rejecting
(e.g. co-Büchi) and where the initial state was in a rejecting
SCC, sbacc() could output a superfluous state. (Issue #492)
- Compared to 2.9.8, complement() (and many functions using it) was
slower and produced larger outputs on some automata with more than
32 states due to an optimization of the determinization being
unintentionally disabled.
- The split_2step() function used to create a synthesis game could
complain that it was unable to complement a monitor (Issue #495).
- Work around GraphViz bug #2179 by avoiding unnecessary empty
lines in the acceptance conditions shown in dot.
- Fix a case where generic_accepting_run() incorrectly returns a
cycle around a rejecting self-loop.
- Mealy machines resulting from SAT-based minimization could differ
on architectures with different hash tables implementations.
- org-mode moved to GNU ELPA (Issue #496).
We are happy to announce the release of Spot 2.10.2
This is a maintenance release fixing a few bugs discovered
over the last two weeks.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.10.2.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.2 (2021-12-03)
Bugs fixed:
- twa_graph::purge_dead_states() now also removes edges labeled by
bddfalse.
- only use sched_getcpu() and pthread_setaffinity_np() when they are
available.
- Using ##300 in a SERE will report that the repeatition exceeds the
allowed value using a parse error, not as an exception.
- spot::formula::is_literal() should be const.
We are happy to announce the release of Spot 2.10.1
This is a maintenance release fixing a few bug discovered
right after the release for Spot 2.10 last week.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.10.1.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.1 (2021-11-19)
Build:
- Python 3.5 or later is now required (unless Python bindings are
disabled). Python 3.5 reached end-of-life one year ago, so we
believe support for older versions of Python will not be missed.
Library:
- The sbacc() function now defines the "original-states" property,
allowing to map an output state back to its input.
Bugs fixed:
- Ranged repetition operators from LTL/PSL, like [*a..b],
[->a..b] or even F[a..b] used to store and handle a and b
as 8-bit values without overflow checks. So for instance
{a[*260];b} was silently interpreted as {a[*4];b}
This version still restricts those bounds to 8 bits, but now
diagnose overflow checks while parsing and constructing formulas.
Also the so called "trivial simplification rules" will not be
applied in case they would lead to an overflow. For instance
{a;[*150];[*50];b} is rewritten to {a;[*200];b}
but
{a;[*150];[*150];b} is untouched.
- Fix a compilation error on system with glibc older than 2.18,
where <inttypes.h> does not define some C99 macro by default when
compiled in C++ mode. (Such old libraries are used when compiling
packages for conda-forge, which use CentOS 6 as building environment.)
- Fix a link error of tests/ltsmin/modelcheck not finding BDD functions
on some systems (observed on CentOS 6 again).
- Fix spurious test-suite failures under newer Jupyter
installations. IPykernel 6.0 now captures stdout/stderr from
subprocesses and displays them in the notebook. The spot.ltsmin
code that loads modules compiled with SpinS had to be rewritten to
capture and display the output of SpinS, so that our test-cases
can be reproduced regardless of the IPykernel version. This fix
was easier to do in Python 3.5.
- Fix sevaral minor documentation errors.
We are happy to announce the release of Spot 2.10
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.
