We are happy to announce the release of Spot 2.13
This is a major release that comes 10 months after the
release of Spot 2.12. It contains contributions by Philipp
Schlehuber, Florian Renkin, Antoin Martin, and myself.
A list of user-visible changes is given at the end of this email.
You can find the new release here:
http://www.lre.epita.fr/dload/spot/spot-2.13.tar.gz
See https://spot.lre.epita.fr/ for documentation and installation
instructions.
Please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.13 (2025-03-24)
Command-line tools:
- ltlmix is a new tool that generates formulas by combining existing
ones. See https://spot.lre.epita.fr/ltlmix.html for examples.
- (BACKWARD INCOMPATIBILITY) ltlsynt's CSV output has been largely
overhauled, and the output columns have been both renamed (for
consistency) and augmented (with new statistics). The new CSV
output should be more useful when the input specification is
decomposed, in particular, there is a column giving the number of
sub-specifications obtained, and other statistics columns have
names starting with "max_" or "sum_" indicating how said
statistics are updated across sub-specifications.
Additionally, --csv=FILENAME will now save the source filename for
the processed formulas as the first column of the CSV file, and
the "formula" column is no longer output by default to save space.
This "formula" column can be added back with the new option
--csv-with-formula=FILENAME if really needed.
- ltlsynt learned a --part-file option, to specify the partition of
input/output proposition from a *.part file, as used in several
other tools.
- ltlfilt learned a --relabel=io mode, that is useful to shorten
atomic propositions in the context of LTL synthesis. For instance
% ltlfilt -f 'G(req->Fack)&G(go->Fgrant)' --relabel=io --ins=req,go
G(i1 -> Fo0) & G(i0 -> Fo1)
The resulting formulas are now usable by ltlsynt without having to
specify which atomic propositions are input or output, as this can
be inferred from their name. Instead of using --ins/--outs, a
--part-file option can be used as well.
- ltlfilt learned a --save-part-file[=FILENAME] option that can be
used to create partition files suitable for many synthesis tools
(including ltlsynt).
- genltl learned --lily-patterns to generate the example LTL
synthesis specifications from Lily 1.0.2. Those come with input
and output atomic propositions rewriten in the form "iNN" or "oNN",
so they can be fed to ltlsynt directly, as in
% genltl --lily-patterns | ltlsynt -q
- genltl's --pps-arbiter-standard and --pps-arbiter-strict have been
changed to rename variables {r1,r2,...,g1,g2...} as
{i1,i2,...,o1,o2,...} so that these formulas can be fed directly to
ltlsynt.
- autfilt learned --restrict-dead-end-edges, to restricts labels of
edges leading to dead-ends. See the description of
restrict_dead_end_edges_here() below.
- autfilt learned --track-formula=F to label states with formulas
derived from F. (This is more precise on deterministic automata.)
- autfilt learned --mcs[=any|scc] to reorder states according to a
maximum cardinality search. The argument specifies how to break
ties.
- autfilt learned --given-formula, --given-automaton, and
--given-strategy to simplify automata given some knowledge.
This is discussed in the PN'25 paper "Simplifying LTL
Model-Checking Given Prior Knowledge" by Duret-Lutz, Poitrenaud,
and Thierry-Mieg.
- ltlfilt learned --pi1, --sigma1, --delta1, --pi2, --sigma2, and
--delta2 to filter according to classes Π₁,Σ₁,Δ₁,Π₂,Σ₂, and Δ₂.
- ltlfilt learned --to-delta2 to transform an LTL formula into Δ₂.
Library:
- restrict_dead_end_edges_here() can reduce non-determinism (but
not remove it) by restricting the label L of some edge (S)-L->(D)
going to a state D that does not have other successors than
itself. The conditions are detailed in the documentation of
this function.
- spot::postprocessor will now call restrict_dead_end_edges_here()
in its highest setting. This can be fine-tuned with the "rde"
extra option; see the spot-x (7) man page for detail.
- The formula class now keeps track of membership to the Δ₁, Σ₂,
Π₂, and Δ₂ syntactic classes. This can be tested with
formula::is_delta1(), formula::is_sigma2(), formula::is_pi2(),
formula::is_delta2(). See doc/tl/tl.pdf from more discussion.
- spot::to_delta2() implements Δ₂-normalization for LTL formulas,
following "Efficient Normalization of Linear Temporal Logic" by
Esparza et al. (J. ACM, 2024).
- Trivial rewritings (those performed everytime at construction)
were missing the rule "[*0]|f ≡ f" when f already accepts the
empty word. (Issue #545.)
- spot::match_states(A, B) is a new function that returns a vector
V such that V[x] contains all states y such that state (x, y) can
reach an accepting cycle in product(A, B). In particular, if A
and B accept the same language, any word accepted by A from state
x can be accepted in B from some state in V[x].
That function also has a variant spot::match_states(A, f) where f
is an LTL formula. In this case, it returns an array of
formulas. If f represents a superset of the language of A, then
any word accepted by A from state x satisfies V[x]. Related to
Issue #591.
- twa_graph::defrag_states(num) no longer requires num[i]≤i; num
can now describe a permutation of the state numbers.
- spot::maximum_cardinality_search() and
spot::maximum_cardinality_search_reorder_here() are new function
to compute (and apply) an ordering of states based on a maximum
cardinality search.
- a new set of functions spot::update_bounds_given(),
spot::bounds_simplify(), and spot::stutterize_given() implements
simplification of automata based on apriori knowledge.
See https://spot.lre.epita.fr/ipynb/given.html for examples.
Bug fixes:
- "ltlsynt --aiger -q ..." was still printing the realizability
status and the AIG circuit; it now does the job silently as
requested.
- ltlsynt had a minor memory leak.
We are happy to announce the release of Spot 2.12.2
This is a maintenance release fixing a couple of bugs discovered since
our 2.12.1 release. In particular, it fixes a serious bug with
to_finite(), used in some LTLf applications, and another one in the
AIGER encoder used by ltlsynt.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.12.2.tar.gz
See https://spot.lre.epita.fr/ for documentation and installation
instructions.
Please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.12.2 (2025-01-18)
Bug fixes:
- to_finite() was dealing incorrectly with edges that were
both alive and dead. (Issue #596.)
- LaTeX output of the X[!] operator was broken in both
LaTeX and self-contained LaTeX mode. (Issue #597)
- Fix a bug in the AIGER encoding with certain forms of
global-equivalence.
- Work around a spurious test failure with Python 3.13.
We are happy to announce the release of Spot 2.12.1
This is a minor release containing fixes for several unimportant bugs;
if 2.12 already works for you, it is safe to skip this upgrade.
You can find the new release here:
https://www.lre.epita.fr/dload/spot/spot-2.12.tar.gz
See https://spot.lre.epita.fr/ for documentation and installation
instructions.
Please direct any feedback to <spot(a)lrde.epita.fr>, or create an issue
at https://gitlab.lre.epita.fr/spot/spot/-/issues/new
----------
New in spot 2.12.1 (2024-09-23)
Bug fixes:
- Generating random formula without any unary opertors would very
often create formulas much smaller than asked.
- The parity game solver, which internally works on "parity max
odd", but actually accept any type of parity acceptance, could be
confused by games with "parity min" acceptance using transition
with several colors (a rather uncommon situation).
- "ltlsynt ... --print-game --dot=ARGS" was ignoring ARGS.
- Work around various warnings from g++14.
- Improved handling of spot-extra/ directory with newer Swig
versions. Necessary to recompile Seminator 2 with Swig 4.
We are happy to announce the release of Spot 2.12
This is a long-awaited major release containing new features developed
in the last 17 months (since the release of Spot 2.11), as well as fixes
for bugs discovered in the last 9 months (since Spot 2.11.6). Some of
these bug fixes are necessary for Spot to work correctly with newer
versions of Python, GCC, or Jupyter.
This release contains contributions by Philipp Schlehuber, Florian
Renkin, Jonah Romero, Pierre Ganty, and myself.
A list of user-visible 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.12.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). However, it will be a while before
we are able to replace all URLs ending in "lrde.epita.fr" by URLs
ending "lrde.epita.fr", so do not be surprized about the mix of those.
New in spot 2.12 (2024-05-16)
Build:
- When Python bindings are enabled, Spot now requires Python 3.6 or
later. Python 3.6 has reached end-of-life in 2021, but is still
used on CentOS 7 (which will reach end-of-support later in 2024).
Documentation:
- https://spot.lre.epita.fr/tut25.html is a new example showing
how to print an automaton in the "BA format" (used by Rabbit
and other tools).
Command-line tools:
- In places that accept format strings with '%' sequences, like
options --stats, --name, or --output, the new '%l' can now be used
to produce the 0-based serial number of the produced object. This
differs from the existing '%L' that is usually related to the line
number of the input (when that makes sense). For instance to
split a file that contains many automata into one file per
automaton, do
autfilt input.hoa -o output-%l.hoa
- For tools that produce automata, using -Hb or --hoa=b will produce
an HOA file in which aliases are used to form a basis for the
whole set of labels. Those aliases are only used when more than
one atomic proposition is used (otherwise, the atomic proposition
and its negation is already a basis). This can help reduce the
size of large HOA files.
- autfilt learned --separate-edges, to split the labels of
the automaton using a basis of disjoint labels. See
https://spot.lre.epita.fr/tut25.html for some motivation.
- autfilt learned --reduce-acceptance-set/--enlarge-acceptance-set
to heurisitcally remove/add to unnecessary acceptance marks in
Büchi automata. (Issue #570)
- ltlfilt has a new option --relabel-overlapping-bool=abc|pnn that
will replace boolean subformulas by fresh atomic propositions even
if those subformulas share atomic propositions.
- ltlsynt's --ins and --outs options will iterpret any atomic
proposition surrounded by '/' as a regular expression.
For intance with
ltlsynt --ins='/^in/,/env/' --outs=/^out/,/control/' ...
any atomic proposition that starts with 'in' or contains 'env'
will be considered as input, and one that starts with 'out'
or contain 'control' will be considered output.
By default, if neither --ins nor --outs is given, ltlsynt will
behave as if --ins='/^[iI]/' and --outs='/^[oO]/ were used.
- ltlsynt will now check for atomic propositions that always have
the same polarity in the specification. When this happens, these
output APs are replaced by true or false before running the
synthesis pipeline, and the resulting game, Mealy machine, or
Aiger circuit is eventually patched to include that constant
output. This can be disabled with --polarity=no.
- ltlsynt will now check for atomic propositions that are specified
as equivalent. When this is detected, equivalent atomic
propositions are replaced by one representative of their class, to
limit the number of different APs processed by the synthesis
pipeline. The resulting game, Mealy machine, or Aiger circuit is
eventually patched to include the removed APs. This optimization
can be disabled with --global-equivalence=no. As an exception, an
equivalence between input and output signals (such as G(in<->out))
will be ignored if ltlsynt is configured to output a game (because
patching the game a posteriori is cumbersome if the equivalence
concerns different players).
- genaut learned two new familes of automata, --cycle-log-nba and
--cycle-onehot-nba. They both create a cycle of n^2 states that
can be reduced to a cycle of n states using reduction based on
direct simulation.
Library:
- The following new trivial simplifications have been implemented for SEREs:
- f|[+] = [+] if f rejects [*0]
- f|[*] = [*] if f accepts [*0]
- f&&[+] = f if f rejects [*0]
- b:b[*i..j] = b[*max(i,1)..j]
- b[*i..j]:b[*k..l] = b[*max(i,1)+max(k,1)-1, j+l-1]
- The following new trivial simplifications have been implemented
for PSL operators:
- {[*]}[]->0 = 0
- {[*]}<>->1 = 1
- The HOA parser is a bit smarter when merging multiple initial
states into a single initial state (Spot's automaton class
supports only one): it now reuses the edges leaving initial states
without incoming transitions.
- The automaton parser has a new option "drop_false_edges" to
specify whether edges labeled by "false" should be ignored during
parsing. It is enabled by default for backward compatibility.
- spot::bdd_to_cnf_formula() is a new variant of spot::bdd_to_formula()
that converts a BDD into a CNF instead of a DNF.
- spot::relabel_bse() has been improved to better deal with more
cases. For instance '(a & b & c) U (!c & d & e)' is now
correctly reduced as '(p0 & p1) U (!p1 & p2)', and
'((a & !b) | (a->b)) U c' now becomes '1 U c'. (Issue #540.)
- spot::relabel_overlapping_bse() is a new function that will
replace boolean subformulas by fresh atomic propositions even if
those subformulas share atomic propositions.
- spot::translate() has a new -x option "relabel-overlap=M" that
augments the existing "relabel-bool=N". By default, N=4, M=8.
When the formula to translate has more than N atomic propositions,
relabel_bse() is first called to attempt to rename non-overlapping
boolean subexpressions (i.e., no shared atomic proposition) in
order to reduce the number of atomic proposition, a source of
exponential explosion in several places of the translation
pipeline. This relabel-bool optimization exists since Spot 2.4.
The new feature is that if, after relabel-bool, the formula still
has more than M atomic propositions, then spot::translate() now
attempts to relabel boolean subexpressions even if they have
overlapping atomic propositions, in an attempt to reduce the
number of atomic proposition even more. Doing so has the slightly
unfortunate side effect of hindering some simplifications (because
the new atomic propositions hide their interactions), but it
usually incures a large speedup. (See Issue #500, Issue #536.)
For instance on Alexandre's laptop, running
'ltlsynt --tlsf SPIReadManag.tlsf --aiger'
with Spot 2.11.6 used to produce an AIG circuit with 48 nodes in
36 seconds; it now produces an AIG circuit with 53 nodes in only
0.1 second.
- spot::contains_forq() is an implementation of the paper "FORQ-Based
Language Inclusion Formal Testing" (Doveri, Ganty, Mazzocchi;
CAV'22) contributed by Jonah Romero.
- spot::contains() still defaults to the complementation-based
algorithm, however by calling
spot::containment_select_version("forq") or by setting
SPOT_CONTAINMENT_CHECK=forq in the environment, the
spot::contains_forq() implementation will be used instead when
applicable (inclusion between Büchi automata).
The above also impacts autfilt's --included-in option.
- spot::reduce_buchi_acceptance_set_here() and
spot::enlarge_buchi_acceptance_set_here() will heuristically
remove/add unnecessary acceptance marks in Büchi automata.
(Issue #570.)
- Given a twa_word_ptr W and a twa_ptr A both sharing the same
alphabet, one can now write W->intersects(A) or A->intersects(W)
instead of the longuer W->as_automaton()->intersects(A) or
A->intersects(W->as_automaton()).
- spot::scc_info has a new option PROCESS_UNREACHABLE_STATES that
causes it to enumerate even unreachable SCCs.
- spot::realizability_simplifier is a new class that performs the
removal of superfluous APs that is now performed by ltlsynt
(search for --polarity and --global-equivalence above).
- scc_filter used to reduce automata tagged with the inherently-weak
property to weak Büchi automata (unless the acceptance was already
t or co-Büchi). In cases where the input automaton had no
rejecting cycle, the Büchi acceptance was overkill: scc_filter
will now use "t" acceptance. This change may have unexpected
consequences in code paths that assume running scc_filter on a
Büchi automaton will always return a Büchi automaton. For those,
a "keep_one_color" option has been added to scc_filter.
- spot::separate_edges() and spot::edge_separator offers more ways
to split labels. See https://spot.lrde.epita.fr/ipynb/split.html
- ltsmin's interface will now point to README.ltsmin in case an
error is found while running divine or spins.
- spot::is_safety_automaton() was generalized to detect any
automaton for which the acceptance could be changed to "t" without
changing the language. In previous versions this function assumed
weak automata as input, but the documentation did not reflect
this.
- spot::remove_alternation() has a new argument to decide whether it
should raise an exception or return nullptr if it requires more
acceptance sets than supported.
- spot::dualize() learned a trick to be faster on states that have
less outgoing edges than atomic proposition declared on the
automaton. spot::remove_alternation(), spot::tgba_powerset(),
simulation-based reductions, and spot::tgba_determinize() learned
a similar trick, except it isn't applied at the state level but if
the entire automaton uses few distinct labels. These changes may
speed up the processing of automata with many atomic propositions
but few distinct labels. (Issue #566 and issue #568.)
Backward incompatibilities:
- spot::dualize() does not call cleanup_acceptance() anymore. This
change ensures that the dual of a Büchi automaton will always be a
co-Büchi automaton. Previously cleanup_acceptance(), which remove
unused colors from the acceptance, was sometimes able to simplify
co-Büchi to "t", causing surprizes.
- Function minimize_obligation_garanteed_to_work() was renamed to
minimize_obligation_guaranteed_to_work(). We believe this
function is only used by Spot currently.
- Function split_independant_formulas() was renamed to
split_independent_formulas(). We believe this function is only
used by Spot currently.
Python:
- The spot.automata() and spot.automaton() functions now accept a
drop_false_edges=False argument to disable the historical behavior
of ignoring edges labeled by False.
- Calling aut.highlight_state(s, None) or aut.highlight_edge(e,
None) may now be used to remove the highlighting color of some
given state or edge. Use aut.remove_highlight_states() or
aut.remove_highlight_edges() to remove all colors. (Issue #554.)
- Calling aut.get_hight_state(s) or get.highlight_edge(e) will
return the highlight color of that state/edge or None.
- Recent version Jupyter Notebook and Jupyter Lab started to render
SVG elements using <img...> tag to make it easier to copy/paste
those images. This breaks several usages, including the
possibility to have informative tooltips on states and edges (used
in Spot). See the following issues for more details.
https://github.com/jupyter/notebook/issues/7114https://github.com/jupyterlab/jupyterlab/issues/10464
This version of Spot now declares its svg outputs as HTML to
prevent Jypyter from wrapping them is images.
Bugs fixed:
- tgba_determinize()'s use_simulation option would cause it to
segfault on automata with more than 2^16 SCCs, due to overflows in
computations of indices in the reachability matrix for SCCs.
(Issue #541.) This has been fixed by disabling the use_simulation
optimization in this case.
- product_or_susp() and product_susp() would behave incorrectly in
presence of unsatisifable or universal acceptance conditions that
were not f or t. (Part of issue #546.)
- Several algorithms were incorrectly dealing with the "!weak"
property. Because they (rightly) assumed that a weak input would
produce a weak output, they also wrongly assumed that a non-weak
output would produce a non-weak output. Unfortunately removing
states or edges in a non-weak automaton can lead a weak automaton.
The incorrect property lead to issue #546. In addition to fixing
several algorithms, product() and print_hoa() will now raise an
exception if automaton with t or f acceptance is declared !weak.
(This cheap check will not catch all automata incorrectly labeled
by !weak, but helps detects some issues nonetheless.)
- The automaton parser forgot to update the list of highlighted
edges while dropping edges labeled by bddfalse. (issue #548.)
- The comparison operators for acceptance condition (==, !=)
could fail to equate two "t" condition, because we have two ways
to represent "t": the empty condition, or the empty "Inf({})".
- Functions complement() and change_parity() could incorrectly read
or write the unused edge #0. In the case of complement(), writing
that edge was usually harmless. However, in some scenario,
complement could need to stick a ⓪ acceptance mark on edge #0,
then the acceptance condition could be simplified to "t", and
finally change_parity could be confused to find such an accepting
mark in an automaton that declares no colors, and perform some
computation on that color that caused it to crash with a "Too many
acceptance sets used" message. (issue #552)
- The detection of terminal automata used did not exactly
match the definition used in the HOA format. The definition
of a terminal automaton is supposed to be:
1. the automaton is weak
2. its accepting SCCs are complete
3. no accepting cycle can reach a rejecting cycle
However the implementation actually replaced the last point
by the following variant:
3'. no accepting edge can reach a rejecting cycle
This caused issues in automata with t acceptance. Fixing the code
by replacing 3' by 3 this also made the third argument of
is_terminal_automaton(), an optional boolean indicating whether
transition between SCCs should be ignored when computing 3',
completely obsolete. This third argument has been marked as
depreated. (Issue #553)
- twa::defrag_states(), which is called for instance by
purge_dead_state(), did not update the highlight-edges property.
(Issue #555.)
- spot::minimize_obligation will skip attempts to complement very
weak automata when those would require too many acceptance sets.
- acd_transform() was not used by spot::postprocessor unless an
option_map was passed. This was due to some bad default for the
"acd" option: it defaulted to true when an option_map was given,
and to false otherwise. This had no consequences on
ltl2tgba/autfilt were some option_map is always passed, but for
instance the parity automata generated by spot.postprocessor in
Python were not using ACD by default.
- Using spot::postprocessor to produce colored parity automata could
fail to color some transiant edges when the "acd" option was
activated.
- The formula printer incorrectly replaced a SERE like "(!a)[*3];a"
by "a[->]". The latter should only replace "(!a)[*];a".
(Issue #559.)
- The configure script failed to detect the include path for Python 3.12.
(Issue #577.)
- Work around many failures caused by incorrect rounding of floating
point values in the counting of transitions. (Issue #582)
- Some incorrectly escaped strings in Python code were causing
warnings with Python 3.12.
We are happy to announce the release of Spot 2.11.6.
This is a maintenance release containing several fixes for bugs that
have been discovered since 2.11.5. This include a fix for a 20-year old
typo in the modified version of BuDDy that we ship with Spot.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.11.6.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). It will be a while before we are able to
replace all URLs ending in "lrde.epita.fr" by URLs ending
"lre.epita.fr", so do not be surprized about the mix of those.
New in spot 2.11.6 (2023-08-01)
Bug fixes:
- Running command lines such as "autfilt input.hoa -o output-%L.hoa"
where thousands of different filenames can be created failed with
"Too many open files". (Issue #534)
- Using --format=... on a tool that output formulas would force
the output on standard output, even when --output was given.
- Using "randltl -S" did not correctly go through the SERE printer
functions.
- Our copy of BuDDy's bdd_forall() had a 20 year old typo that
caused cache entries from bdd_exist() and bdd_forall() to be
mixed. Spot was safe from this bug because it was only using
bdd_exist(). (Issue #535)
- Work around recent Pandas and GCC changes.
We are happy to announce the release of Spot 2.11.5
Spot 2.11.5 is a maintenance release that fixes a handful of issues that
were discovered or reported over the last two months.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.11.5.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 it will be a while before we are able
to replace all URLs ending in "lrde.epita.fr" by URLs ending
"lrde.epita.fr", so do not be surprized about the mix of those.
New in spot 2.11.5 (2023-04-20)
Bug fixes:
- Fix spurious failure of ltlsynt2.test when Python is not installed
(issue #530).
- Building from the git repository would fail to report a missing
emacs (issue #528).
- Fix exception raised by aut1.intersecting_run(aut2).as_twa()
because the run did not match transitions present in aut1
verbatim. We also changed the behavior of as_twa() to not merge
identical states.
- Fix segfaults occuring in determinization of 1-state terminal
automata.
- Fix incorrect assertion in game solver when the edge vector
contains deleted transitions.
We are happy to announce the release of Spot 2.11.4
Spot 2.11.4 fix a couple of issues discovered in the last two months.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.11.4.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.4 (2023-02-10)
Python:
- spot.acd() no longer depends on jQuery for interactivity.
Bug fixes:
- When merging initial states from state-based automata with
multiple initial states (because Spot supports only one), the HOA
parser could break state-based acceptance. (Issue #522.)
- autfilt --highlight-word refused to work on automata with Fin
acceptance for historical reasons, however the code has been
perfectly able to handle this for a while. (Issue #523.)
- delay_branching_here(), a new optimization of Spot 2.11, had an
incorrect handling of states without successors, causing some
segfaults. (Issue #524.)
- Running delay_branching_here() on state-based automata (this was not
done in Spot so far) may require the output to use transition-based
acceptance. (Issue #525.)
- to_finite(), introduced in 2.11, had a bug that could break the
completeness of automata and trigger an exception from the HOA
printer. (Issue #526.)
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).
