We are happy to announce the release of Spot 2.9.4
This is a maintenance release with very minor fixes.
(If you already have 2.9.3, there is no real reason to upgrade.)
The release contains contributions from Florian Renkin and myself.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.9.4.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
Note that versions from the 2.9.x branch are the last releases using
C++14. We have already switched to C++17 for the development of the
next major release. This release is already compatible with C++17, so
tools using Spot as a library should consider switching to C++17
already.
Please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.9.4 (2020-09-07)
Bugs fixed:
- Handle xor and <-> in a more natural way when translating
LTL formulas to generic acceptance conditions.
- Multiple typos in documentation, --help texts, or error messages.
--
Alexandre Duret-Lutz
Yes, 2.9.2 was short-lived, as the main issue it was supposed to fix
was only half-fixed...
You can find the 2.9.3 release here:
http://www.lrde.epita.fr/dload/spot/spot-2.9.3.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
Note that versions 2.9.x are likely to be the last releases using
C++14. We plan 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.
Please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.9.3 (2020-07-22)
Bug fixed:
- Completely fix the ltlcross issue mentioned in previous release.
New in spot 2.9.2 (2020-07-21)
Bugs fixed:
- ltlcross --csv=... --product=N with N>0 could output spurious
diagnostics claiming that words were rejected when evaluating
the automaton on state-space.
- spot::scc_info::determine_unknown_acceptance() now also update the
result of spot::scc_info::one_accepting_scc().
--
Alexandre Duret-Lutz
Spot 2.9.2 has been released.
This fixes a bug in ltlcross that was introduced in 2.9 and
reported by Salomon Sickert.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.9.2.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
Note that versions 2.9.x are likely to be the last releases using
C++14. We plan 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.
Please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.9.2 (2020-07-21)
Bugs fixed:
- ltlcross --csv=... --product=N with N>0 could output spurious
diagnosics claiming that words were rejected when evaluating
the automaton on state-space.
- spot::scc_info::determine_unknown_acceptance() now also update the
result of spot::scc_info::one_accepting_scc().
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.9.1
This is mostly a maintenance release that fixes a couple of bugs
discovered since the release of 2.9, as well as some simple
portability issues. It also adds some minor features that were part
of our SYNTCOMP submission (but not all patches of the SYNTCOMP
submission have been merged yet).
The release contains contributions from Florian Renkin and myself.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.9.1.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
Note that versions 2.9.x are likely to be the last releases using
C++14. We plan 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.
Please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.9.1 (2020-07-15)
Command-line tools:
- 'ltl2tgba -G -D' is now better at handling formulas that use
'<->' and 'xor' operators at the top level. For instance
ltl2tgba -D -G '(Fa & Fb & Fc & Fd) <-> GFe'
now produces a 16-state automaton (instead of 31 in Spot 2.9).
- Option '-x wdba-minize=N' used to accept N=0 (off), or N=1 (on).
It can now take three values:
0: never attempt this optimization,
1: always try to determinize and minimize automata as WDBA,
and check (if needed) that the result is correct,
2: determinize and minimize automata as WDBA only if it is known
beforehand (by cheap syntactic means) that the result will be
correct (e.g., the input formula is a syntactic obligation).
The default is 1 in "--high" mode, 2 in "--medium" mode or in
"--deterministic --low" mode, and 0 in other "--low" modes.
- ltlsynt learned --algo=ps to use the default conversion to
deterministic parity automata (the same as ltl2tgba -DP'max odd').
- ltlsynt now has a -x option to fine-tune the translation. See the
spot-x(7) man page for detail. Unlike ltl2tgba, ltlsynt defaults
to simul=0,ba-simul=0,det-simul=0,tls-impl=1,wdba-minimize=2.
Library:
- product_xor() and product_xnor() are two new versions of the
synchronized product. They only work with operands that are
deterministic automata, and build automata whose language are
respectively the symmetric difference of the operands, and the
complement of that.
- tl_simplifier_options::keep_top_xor is a new option to keep Xor
and Equiv operator that appear at the top of LTL formulas (maybe
below other Boolean or X operators). This is used by the
spot::translator class when creating deterministic automata with
generic acceptance.
- remove_fin() learned a trick to remove some superfluous
transitions.
Bugs fixed:
- Work around undefined behavior reported by clang 10.0.0's UBsan.
- spot::twa_sub_statistics was very slow at computing the number of
transitions, and could overflow. It is now avoiding some costly
loop of BDD operations, and storing the result using at least 64
bits. This affects the output of "ltlcross --csv" and
"--stats=%t" for many tools.
- simplify_acceptance() missed some patterns it should have been
able to simplify. For instance Fin(0)&(Fin(1)|Fin(2)|Fin(4))
should simplify to Fin(1)|Fin(2)|Fin(4) adter adding {1,2,4} to
every place where 0 occur, and then the acceptance would be
renumbered to Fin(0)|Fin(1)|Fin(2). This is now fixed.
- Improve ltldo diagnostics to fix spurious test-suite failure on
systems with antique GNU libc.
- twa_run::reduce() could reduce accepting runs incorrectly on
automata using Fin in their acceptance condition. This caused
issues in intersecting_run(), exclusive_run(),
intersecting_word(), exclusive_word(), which all call reduce().
- ltlcross used to crash with "Too many acceptance sets used. The
limit is 32." when complementing an automaton would require more
acceptance sets than supported by Spot. This is now diagnosed
with --verbose, but does not prevent ltlcross from continuing.
- scc_info::edges_of() and scc_info::inner_edges_of() now correctly
honor any filter passed to scc_info.
--
Alexandre Duret-Lutz
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
