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
