10 Jul
2019
10 Jul
'19
2 p.m.
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>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