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
We are happy to announce the release of Spot 2.7.4
This maintenance release contains only some bug fixes.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.7.4.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.4 (2019-04-27)
Bugs fixed:
- separate_sets_here() (and therefore autfilt --separate-sets) could
loop infinitely on some inputs.
- In some situation, ltl2tgba -G could abort with
"direct_simulation() requires separate Inf and Fin sets". This
was fixed by teaching simulation-based reductions how to deal
with such cases.
- The code for detecting syntactically stutter-invariant PSL
formulas was incorrectly handling the ";" operator, causing some
stutter-sensitive formulas to be flagged a stutter-invariant.
--
Alexandre Duret-Lutz
