We are happy to announce the release of Spot 2.9
This is a major release that has been under development for 9 months.
It contains new features contributed by from Florian Renkin and
myself. A summary of those changes is given at the end of this email.
Note that version 2.9 and the following 2.9.x minor releases are
likely to be the last releases using C++14. We plan is to switch to
C++17 for the next major release. The current code-base is already
compatible with C++17, so tools using Spot as a library may consider
switching to C++17 already.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.9.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.9 (2020-04-30)
Command-line tools:
- When the --check=stutter-sensitive-example option is passed to
tools like ltl2tgba, autfilt, genaut, or ltldo, the produced
automata are checked for stutter-invariance (as in the
--check=stutter-invariant case), additionally a proof of
stutter-sensitiveness is provided as two stutter-equivalent words:
one accepted, and one rejected. These sample words are printed in
the HOA output.
% ltl2tgba --check=stutter-sensitive-example Xa | grep word:
spot-accepted-word: "!a; cycle{a}"
spot-rejected-word: "!a; !a; cycle{a}"
- autfilt learned the --partial-degeneralize option, to remove
conjunctions of Inf, or disjunctions of Fin that appears in
arbitrary conditions.
- ltlfilt and autfilt learned a --nth=RANGE (a.k.a. -N) option to
select a range of their input formulas or automata (assuming a
1-based numbering).
- When running translators, ltlcross will now display {names} when
supplied.
- ltlcross is now using the generic emptiness check procedure
introduced in Spot 2.7, as opposed to removing Fin acceptance
before using a classical emptiness check.
- ltlcross learned a --save-inclusion-products=FILENAME option. Its
use cases are probably quite limited. We use that to generate
benchmarks for our generic emptiness check procedure.
- ltlsynt --algo=lar uses the new version of to_parity() mentionned
below. The old version is available via --algo=lar.old
- ltlsynt learned --csv=FILENAME, to record some statistics about
the duration of its different phases.
- The dot printer is now automatically using rectangles with rounded
corners for automata states if one state label have five or more
characters. This saves space with very long labels. Use --dot=c,
--dot=e, or --dot=E to force the use of Circles, Ellipses, or
rEctangles.
Library:
- Historically, Spot only supports LTL with infinite semantics
so it had automatic simplifications reducing X(1) and X(0) to
1 and 0 whenever such formulas are constructed. This
caused issues for users of LTLf formulas, where it is important
to distinguish a "weak next" (for which X(1)=1 but X(0)!=0) from
a "strong next" (for which X(0)=0 but X(1)!=1).
To accommodate this, this version introduces a new operator
op::strong_X in addition to the existing op::X (whose
interpretation is now weak in LTLf). The syntax for the strong
next is X[!] as a reference to the PSL syntax (where the strong
next is written X!).
Trivial simplification rules for X are changed to just
X(1) = 1 (and not X(0)=0 anymore)
while we have
X[!]0 = 0
The X(0)=0 and X[!]1=1 reductions are now preformed during LTL
simplification, not automatically. Aside from the from_ltlf()
function, the other functions of the library handle X and X[!] in
the same way, since there is no difference between X and X[!] over
infinite words.
Operators F[n:m!] and G[n:m!] are also supported as strong
variants of F[n:m] and G[n:m], but those four are only implemented
as syntactic sugar.
- acc_cond::acc_code::parity(bool, bool, int) was not very readable,
as it was unclear to the reader what the boolean argument meant.
The following sister functions can now improve readability:
parity_max(is_odd, n) = parity(true, is_odd, n)
parity_max_odd(n) = parity_max(true, n)
parity_max_even(n) = parity_max(false, n)
parity_min(is_odd, n) = parity(false, is_odd, n)
parity_min_odd(n) = parity_min(true, n)
parity_min_even(n) = parity_min(false, n)
- partial_degeneralize() is a new function performing partial
degeneralization to get rid of conjunctions of Inf terms, or
disjunctions of Fin terms in acceptance conditions.
- simplify_acceptance_here() and simplify_acceptance() learned to
simplify subformulas like Fin(i)&Fin(j) or Inf(i)|Inf(j), or some
more complex variants of those. If i is uniquely used in the
acceptance condition, these become respectively Fin(i) or Inf(i),
and the automaton is adjusted so that i also appears where j
appeared.
- acc_code::unit_propagation() is a new method for performing unit
propagation in acceptance condition. E.g. Fin(0) | (Inf(0) &
Inf(1)) becomes Fin(0) | Inf(1). This is now called by
simplify_acceptance_here().
- propagate_marks_vector() and propagate_marks_here() are helper
functions for propagating marks on the automaton: ignoring
self-loops and out-of-SCC transitions, marks common to all the
input transitions of a state can be pushed to all its outgoing
transitions, and vice-versa. This is repeated until a fix point
is reached. propagate_marks_vector() does not modify the
automaton and returns a vector of the acc_cond::mark_t that should
be on each transition; propagate_marks_here() actually modifies
the automaton.
- rabin_to_buchi_if_realizable() is a new variant of
rabin_to_buchi_maybe() that converts a Rabin-like automaton into a
Büchi automaton only if the resulting Büchi automaton can keep the
same transition structure (where the ..._maybe() variant would
modify the Rabin automaton if needed).
- to_parity() has been rewritten. It now combines several strategies
for paritizing automata with any acceptance condition.
- relabel_bse(), used by ltlfilt --relabel-bool, is now better at
dealing with n-ary operators and isolating subsets of operands
that can be relabeled as a single term.
- print_dot()'s default was changed to use circles for automata with
fewer than 10 unamed states, ellipses for automata with up to 1000
unamed states (or named states with up to 4 characters), and
rounded rectangles otherwise. Rectangles are also used for
automata with acceptance bullets on states. The new "E" option
can be used to force rectangles in all situations.
- The generic emptiness check has been slightly improved (doing
fewer recursive calls in the worst case).
Backward-incompatible changes:
- iar() and iar_maybe() have been moved from
spot/twaalgos/rabin2parity.hh spot/twaalgos/toparity.hh and marked
as deprecated, they should be replaced by to_parity(). In case
the input is Rabin-like or Streett-like, to_parity() should be at
least as good as iar().
- The twa_graph::is_alternating() and digraph::is_alternating() methods,
deprecated in Spot 2.3.1 (2017-02-20), have been removed.
Bugs fixed:
- Relabeling automata could introduce false edges. Those are now
removed.
- Emptiness checks, and scc_info should now ignore edges labeled
with false.
- relabel_bse() could incorrectly relabel Boolean subformulas that
had some atomic propositions in common.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.8.7
This maintenance release contains only bug fixes.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.8.7.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.8.7 (2019-03-13)
Bugs fixed:
- Building a product between two complete automata where one operand
had false acceptance could create an incomplete automaton
incorrectly tagged as complete, causing the print_hoa() function
to raise an exception.
- autfilt --uniq was not considering differences in acceptance
conditions or number of states when discarding automata.
- In an automaton with acceptance condition containing some Fin, and
whose accepting cycle could be reduced to a self-loop in an
otherwise larger SCC, the generation of an accepting run could be
wrong. This could in turn cause segfaults or infinite loops while
running autcross or autfilt --stats=%w.
- The generic emptiness check used a suboptimal selection of "Fin"
to remove, not matching the correct line in our ATVA'19 paper.
This could cause superfluous recursive calls, however benchmarks
have shown the difference to be insignificant in practice.
- The sl(), and sl2() functions for computing the "self-loopization"
of an automaton, and used for instance in algorithms for computing
proof of stutter-sensitiveness (e.g., in our web application),
were incorrect when applied on automata with "t" acceptance (or
more generaly, any automaton where a cycle without mark is
accepting).
- ltlcross was not diagnosing write errors associated to
options --grind=FILENAME and --save-bogus=FILENAME.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.8.6
This maintenance release containing fixes for bug discovered
during the development of the future 2.9 release.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.8.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.8.6 (2020-02-19)
Bugs fixed:
- calling spot.translate() with two conflicting preferences like
spot.translate(..., 'det', 'any') triggered a syntax error in the
Python code to handle this error.
- degeneralize_tba() was incorrectly not honnoring the "skip_level"
optimization after creating an accepting transition; as a
consequence, some correct output could be larger than necessary
(but still correct).
- Some formulas with Boolean sub-formulas equivalent to true or
false could be translated into automata with false labels.
- The HOA printer would incorrectly output the condition
'Fin(1) & Inf(2) & Fin(0)' as 'Fin(0) | Fin(1) & Inf(2)'
due to a bug in the is_generalized_rabin() matching function.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.8.5
This maintenance release contains only bug fixes.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.8.5.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.8.5 (2020-01-04)
Bugs fixed:
- ltl2tgba -B could return automata with "t" acceptance, instead
of the expected Inf(0).
- twa_graph::merge_edges() (a.k.a. autfilt --merge-transitions) was
unaware that merging edges can sometimes transform a
non-deterministic automaton into a deterministic one, causing the
following unexpected diagnostic:
"print_hoa(): automaton is universal despite prop_universal()==false"
The kind of non-deterministic automata where this occurs is not
naturally produced by any Spot algorithm, but can be found for
instance in automata produced by Goal 2015-10-18.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.8.4
This release contains a fix for a bug affecting complementation of
Rabin-like automata.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.8.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.8.4 (2019-12-08)
Bugs fixed:
- The Rabin-to-Büchi conversion could misbehave when applied to
Rabin-like acceptance with where some pairs have missing Inf(.)
(e.g. Fin(0)|(Inf(1)&Fin(2))) and when some of the SCCs do not
visit the remaining Inf(.). This indirectly caused the
complementation algorithm to produce incorrect results on such
inputs, causing false positives in ltlcross and autcross.
- Work around a small difference between Python 3.7 and 3.8, causing
spurious failures of the test suite.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.8.3
This release mainly works around an issue in recent GraphViz releases,
causing cropped automata in Jupyter notebooks. (If you do not use Spot
in Jupyter notebooks, there is little point in updating.)
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.8.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.8.3 (2019-11-06)
Build:
- Minor portabilities improvements with C++17 deprecations.
Python:
- Doing "import spot.foo" will now load any spot-extra/foo.py on
Python's search path. This can be used to install third-party
packages that want to behave as plugins for Spot.
- Work around GraphViz bug #1605 in Jupyter notebooks.
https://gitlab.com/graphviz/graphviz/issues/1605
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.8.2
This release contains many minor fixes; mostly portability issues.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.8.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.8.2 (2019-09-27)
Command-line tools:
- ltl2tgba and ltldo learned a --negate option.
Bugs fixed:
- Calling "autfilt --dualize" on an alternating automaton with
transition-based acceptance and universal initial states would
fail with "set_init_state() called with nonexisting state".
- The numbering of nodes in the AIGER output of ltlsynt was
architecture dependent.
- Various compilation issues. In particular, this release is the
first one that can be compiled (and pass tests) on a Raspberry PI.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.8.1
This release one important bug fix to ltlcross, and a few other minor
addition.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.8.1.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.8.1 (2019-07-18)
Command-line tools:
- genltl learned --pps-arbiter-standard and --pps-arbiter-strict.
- ltlcross and autcross have learned a new option -q (--quiet) to
remain quiet until an error is found. This helps for instance in
scenarios where multiple instances of ltlcross/autcross are run in
parallel (using "xargs -P" or "GNU Parallel", for instance). See
https://spot.lrde.epita.fr/ltlcross.html#parallel for examples.
Bugs fixed:
- When complement() was called with an output_aborter, it could
return an alternating automaton on large automata. This in turn
caused ltlcross to emit errors like "remove_alternation() only
works with weak alternating automata" or "product() does not
support alternating automata".
- Work around Emacs bug #34341 when rebuilding documentation on a
system with Emacs <26.3, GNU TLS >= 3.6, and without ESS or with
an obsolete org-mode installed.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.8
Spot is a library of algorithms for manipulating LTL formulas and
omega-automata objects (as commonly used in model checking).
This release contains code contributed by Clément Gillard and myself.
A detailed list of new features is given at the end of this email.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.8.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
Note that since Debian 10 ("Buster") was released a few days ago, the
"stable" Debian packages we distribute are now built for Buster.
As always, please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.8 (2019-07-10)
Command-line tools:
- autfilt learned --highlight-accepting-run=NUM to highlight some
accepting run with color NUM.
- ltldo, ltlcross, and autcross are now preferring posix_spawn()
over fork()+exec() when available.
- ltlcross has new options --determinize-max-states=N and
--determinize-max-edges=M to restrict the use of
determinization-based complementation to cases where it produces
automata with at most N states and M edges. By default
determinization is now attempted up to 500 states and 5000
edges. This is an improvement over the previous default where
determinization-based complementation was not performed at all,
unless -D was specified.
- ltlcross will now skip unnecessary cross-checks and
consistency-checks (they are unnecessary when all automata
could be complemented and statistics were not required).
- genaut learned --m-nba=N to generate Max Michel's NBA familly.
(NBAs with N+1 states whose determinized have at least N! states.)
- Due to some new simplification of parity acceptance, the output of
"ltl2tgba -P -D" is now using a minimal number of colors. This
means that recurrence properties have an acceptance condition
among "Inf(0)", "t", or "f", and persistance properties have an
acceptance condition among "Fin(0)", "t", or "f".
- ltldo and ltlcross learned shorthands to call the tools ltl2na,
ltl2nba, and ltl2ngba from Owl 19.06. Similarly, autcross learned
a shorthand for Owl's dra2dpa.
Documentation:
- https://spot.lrde.epita.fr/tut90.html is a new file that explains
the purpose of the spot::bdd_dict object.
Library:
- Add generic_accepting_run() as a variant of generic_emptiness_check() that
returns an accepting run in an automaton with any acceptance condition.
- twa::accepting_run() and twa::intersecting_run() now work on
automata using Fin in their acceptance condition.
- simulation-based reductions have learned a trick that sometimes
improve transition-based output when the input is state-based.
(The automaton output by 'ltl2tgba -B GFa | autfilt --small' now
has 1 state instead of 2 in previous versions. Similarly,
'ltldo ltl2dstar -f 'GFa -> GFb' | autfilt --small' produces 1
state instead of 4.)
- simulation-based reductions hae learned another trick to better
merge states from transiant SCCs.
- acc_cond::top_disjuncts() and acc_cond::top_conjuncts() can be
used to split an acceptance condition on the top-level & or |.
These methods also exist in acc_cond::acc_code.
- minimize_obligation() learned to work on very weak automata even
if the formula or negated automaton are not supplied. (This
allows "autfilt [-D] --small" to minimize very-weak automata
whenever they are found to represent obligation properties.)
- There is a new spot::scc_and_mark_filter objet that simplifies the
creation of filters to restrict spot::scc_info to some particular
SCC while cutting new SCCs on given acceptance sets. This is used
by spot::generic_emptiness_check() when processing SCCs
recursively, and makes it easier to write similar code in Python.
- print_dot has a new option 'g', to hide edge labels. This is
helpful to display automata as "graphs", e.g., when illustrating
algorithms that do not care about labels.
- A new complement() function returns complemented automata with
unspecified acceptance condition, allowing different algorithms to
be used. The output can be alternating only if the input was
alternating.
- There is a new class output_aborter that is used to specify
upper bounds on the size of automata produced by some algorithms.
Several functions have been changed to accept an output_aborter.
This includes:
* tgba_determinize()
* tgba_powerset()
* minimize_obligation()
* minimize_wdba()
* remove_alternation()
* product()
* the new complement()
* the postprocessor class, via the "det-max-state" and
"det-max-edges" options.
- SVA's first_match operator can now be used in SERE formulas and
that is supported by the ltl_to_tgba_fm() translation. See
doc/tl/tl.pdf for the semantics. *WARNING* Because this adds a
new operator, any code that switches over the spot::op type may
need a new case for op::first_match. Furthermore, the output of
"randltl --psl" will be different from previous releases.
- The parser for SERE learned to recognize the ##n and ##[i:j]
operators from SVA. So {##2 a ##0 b[+] ##1 c ##2 e} is another
way to write {[*2];a:b[+];c;1;e}. The syntax {a ##[i:j] b} is
replaced in different ways depending on the values of i, a, and b.
The formula::sugar_delay() function implements this SVA operator in
terms of the existing PSL operators. ##[+] and ##[*] are sugar
for ##[1:$] and ##[0:$].
- The F[n:m] and G[n:m] operators introduced in Spot 2.7 now
support the case where m=$.
- spot::relabel_apply() makes it easier to reverse the effect
of spot::relabel() or spot::relabel_bse() on formula.
- The LTL simplifier learned the following rules:
F(G(a | Fb)) = FGa | GFb (if option "favor_event_univ")
G(F(a | Gb)) = GFa | FGb (if option "favor_event_univ")
F(G(a & Fb) = FGa & GFb (unless option "reduce_size_strictly")
G(F(a & Gb)) = GFa & FGb (unless option "reduce_size_strictly")
GF(f) = GF(dnf(f)) (unless option "reduce_size_strictly")
FG(f) = FG(cnf(f)) (unless option "reduce_size_strictly")
(f & g) R h = f R h if h implies g
(f & g) M h = f M h if h implies g
(f | g) W h = f W h if g implies h
(f | g) U h = f U h if g implies h
Gf | F(g & eventual) = f W (g & eventual) if !f implies g
Ff & G(g | universal) = f M (g | universal) if f implies !g
f U (g & eventual) = F(g & eventual) if !f implies g
f R (g | universal) = G(g | universal) if f implies !g
- cleanup_parity() and colorize_parity() were cleaned up a bit,
resulting in fewer colors used in some cases. In particular,
colorize_parity() learned that coloring transitiant edges does not
require the introduction of a new color.
- A new reduce_parity() function implements and generalizes the
algorithm for minimizing parity acceptance by Carton and Maceiras
(Computing the Rabin index of a parity automaton, 1999). This is
a better replacement for cleanup_parity() and colorize_parity().
See https://spot.lrde.epita.fr/ipynb/parity.html for examples.
- The postprocessor and translator classes are now using
reduce_parity() for further simplifications.
- The code for checking recurrence/persistence properties can also
use the fact the reduce_parity() with return "Inf(0)" (or "t" or
"f") for deterministic automata corresponding to recurrence
properties, and "Fin(0)" (or "t" or "f") for persistence
properties. This can be altered with the SPOT_PR_CHECK
environment variable.
Deprecation notices:
- The virtual function twa::intersecting_run() no longuer takes a
second "from_other" Boolean argument. This is a backward
incompatibility only for code that overrides this function in a
subclass. For backward compatibility with programs that simply
call this function with two argument, a non-virtual version of the
function has been introduced and marked as deprecated.
- The spot::acc_cond::format() methods have been deprecated. These
were used to display acceptance marks, but acceptance marks are
unrelated to acceptance conditions, so it's better to simply print
marks with operator<< without this extra step.
Bugs fixed:
- The gf_guarantee_to_ba() is relying on an inplace algorithm that
could produce a different number of edges for the same input in
two different transition order.
- A symmetry-based optimization of the LAR algorithm performed in
spot::to_parity() turned out to be incorrect. The optimization
has been removed. "ltlsynt --algo=lar" is the only code using
this function currently.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.7.5
This maintenance release fixing a few minor issues.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.7.5.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.5 (2019-06-05)
Build:
- Although the Python bindings in this release are still done with
Swig3.0, the code has been updated to be compatible with Swig4.0.
Library:
- print_dot will replace labels that have more 2048 characters by a
"(label too long)" string. This works around a limitation of
GraphViz that aborts when some label exceeds 16k characters, and
also helps making large automata more readable.
Bugs fixed:
- spot::translator was not applying Boolean sub-formula rewritting
by default unless a spot::option_map was passed. This caused some
C++ code for translating certains formulas to be noticeably slower
than the equivalent call to the ltl2tgba binary.
- The remove_ap algorithm was preserving the "terminal property" of
automata, but it is possible that a non-terminal input produces a
terminal output after some propositions are removed.
--
Alexandre Duret-Lutz
