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
We are happy to announce the release of Spot 2.7.3
This maintenance release contains only bug fixes
and documentation updates.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.7.3.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.3 (2019-04-19)
Bugs fixed:
- When processing CSV files with MSDOS-style \r\n line endings,
--stats would output the \r as part of the %> sequence instead
of ignoring it.
- Fix serious typo in removel_alternation() causing incorrect
output for some VWAA. Bug introduced in Spot 2.6.
Documentation:
- Multiple typos and minor updates.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.7.2
This release contains mostly documentation improvements and some minor
additions to the Python bindings. See below for a detailed list of
user-visible changes.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.7.2.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.2 (2019-03-17)
Python:
- Improved support for explicit Kripke structures. It is now
possible to iterate over a kripke_graph object in a way similar to
twa_graph.
Documentation:
- A new page shows how to create explicit Kripke structures in C++
and Python. See https://spot.lrde.epita.fr/tut52.html
- Another new page shows how to deal with LTLf formulas (i.e., LTL
with finite semantics) and how to translate those.
See https://spot.lrde.epita.fr/tut12.html
Build:
- Work around a spurious null dereference warning when compiling
with --coverage and g++ 8.3.0-3 from Debian unstable.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.7.1
This release contains mostly bug fixes and some minor additions to the
Python bindings. See below for a detailed list of user-visible
changes.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.7.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.7.1 (2019-02-14)
Build
- Work around GCC bug #89303 that causes memory leaks and std::weak_bad_ptr
exceptions when Spot is compiled with the version of g++ 8.2 currently
distributed by Debian unstable (starting with g++ 8.2.0-15).
Python:
- The following methods of spot::bdd_dict are now usable in Python when
fine control over the lifetime of associations between BDD variables
and atomic propositions is needed.
- register_proposition(formula, for_me)
- register_anonymous_variables(count, for_me)
- register_all_propositions_of(other, for_me)
- unregister_all_my_variables(for_me)
- unregister_variable(var, for_me)
- Better support for explicit Kripke structures:
- the kripke_graph type now has Python bindings
- spot.automaton() and spot.automata() now support a want_kripke=True
to return a kripke_graph
See the bottom of https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html
for some examples.
Library:
- Printing Kripke structures via print_hoa() will save state names.
- kripke_graph_ptr objects now honnor any "state-names" property
when formating states.
Bugs fixed:
- The print_dot_psl() function would incorrectly number all but the
first children of commutative n-ary operators: in this case no
numbering was expected.
- std::out_of_range C++ exceptions raised from Python code are now
converted into IndexError Python exceptions (instead of aborting
the program).
- The LTL parser would choke on carriage returns when command-line
tools such as ltlfilt, ltlcross, or ltl2tgba were run on files of
formulas with MS-DOS line endings.
- The core translation for unambiguous automata was incorrectly
tagging some non-weak automata as weak.
- The product_susp() function used to multiply an automaton with a
suspendable automaton could incorrectly build transition-based
automata when multipliying two state-based automata. This caused
ltl2tgba to emit error messages such as: "automaton has
transition-based acceptance despite prop_state_acc()==true".
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.7
Someone recently reported some release-worthy bug, and unfortunately we
do not have time to prepare a 2.6.4 release by cherry-picking the bug
fixes from the development branch. So here is Spot 2.7 instead, with
some minor new features and backward-incompatible changes done over the
last 5 months. See the list below for details.
This release contains contributions by Maximilien Colange, Etienne
Renault, and myself.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.7.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 (2018-12-11)
Command-line tools:
- ltlsynt now has three algorithms for synthesis:
--algo=sd is the historical one. The automaton of the formula
is split to separate inputs and outputs, then
determinized (with Safra construction).
--algo=ds the automaton of the formula is determinized (Safra),
then split to separate inputs and outputs.
--algo=lar translate the formula to a deterministic automaton
with an arbitrary acceptance condition, then turn it
into a parity automaton using LAR, and split it.
In all three cases, the obtained parity game is solved using
Zielonka algorithm. Calude's quasi-polynomial time algorithm has
been dropped as it was not used.
- ltlfilt learned --liveness to match formulas representing liveness
properties.
- the --stats= option of tools producing automata learned how to
tell if an automaton uses universal branching (%u), or more
precisely how many states (%[s]u) or edges (%[e]u) use universal
branching.
Python:
- spot.translate() and spot.postprocess() now take an xargs=
argument similar to the -x option of ltl2tgba and autfilt, making
it easier to fine tune these operations. For instance
ltl2tgba 'GF(a <-> XXa)' --det -x gf-guarantee=0
would be written in Python as
spot.translate('GF(a <-> XXa)', 'det', xargs='gf-guarantee=0')
(Note: those extra options are documented in the spot-x(7) man page.)
- spot.is_generalized_rabin() and spot.is_generalized_streett() now return
a tuple (b, v) where b is a Boolean, and v is the vector of the sizes
of each generalized pair. This is a backward incompatible change.
Library:
- The LTL parser learned syntactic sugar for nested ranges of X
using the X[n], F[n:m], and G[n:m] syntax of TSLF. (These
correspond to the next!, next_e!, and next_a! operators of PSL,
but we do not support those under these names currently.)
X[6]a = XXXXXXa
F[2:4]a = XX(a | X(a | Xa))
G[2:4]a = XX(a & X(a & Xa))
The corresponding constructors (for C++ and Python) are
formula::X(unsigned, formula)
formula::F(unsigned, unsigned, formula)
formula::G(unsigned, unsigned, formula)
- spot::unabbreviate(), used to rewrite away operators such as M or
W, learned to use some shorter rewritings when an argument (e) is
a pure eventuality or (u) is purely universal:
Fe = e
Gu = u
f R u = u
f M e = F(f & e)
f W u = G(f | u)
- The twa_graph class has a new dump_storage_as_dot() method
to show its data structure. This is more conveniently used
as aut.show_storage() in a Jupyter notebook. See
https://spot.lrde.epita.fr/ipynb/twagraph-internals.html
- spot::generic_emptiness_check() is a new function that performs
emptiness checks of twa_graph_ptr (i.e., automata not built
on-the-fly) with an *arbitrary* acceptance condition. Its sister
spot::generic_emptiness_check_scc() can be used to decide the
emptiness of an SCC. This is now used by
twa_graph_ptr::is_empty(), twa_graph_ptr::intersects(), and
scc_info::determine_unknown_acceptance().
- The new function spot::to_parity() translates an automaton with
arbitrary acceptance condition into a parity automaton, based on a
last-appearance record (LAR) construction. (It is used by ltlsynt
but not yet by autfilt or ltl2tgba.)
- The new function is_liveness() and is_liveness_automaton() can be
used to check whether a formula or an automaton represents a
liveness property.
- Two new functions count_univbranch_states() and
count_univbranch_edges() can help measuring the amount of
universal branching in alternating automata.
Bugs fixed:
- translate() would incorrectly mark as stutter-invariant
some automata produced from formulas of the form X(f...)
where f... is syntactically stutter-invariant.
- acc_cond::is_generalized_rabin() and
acc_cond::is_generalized_streett() did not recognize the cases
were a single generalized pair is used.
- The pair of acc_cond::mark_t returned by
acc_code::used_inf_fin_sets(), and the pair (bool,
vector_rs_pairs) by acc_cond::is_rabin_like() and
acc_cond::is_streett_like() were not usable in Python.
- Many object types had __repr__() methods that would return the
same string as __str__(), contrary to Python usage where repr(x)
should try to show how to rebuild x. The following types have
been changed to follow this convention:
spot.acc_code
spot.acc_cond
spot.atomic_prop_set
spot.formula
spot.mark_t
spot.twa_run (__repr__ shows type and address)
spot.twa_word (likewise, but _repr_latex_ used in notebooks)
Note that this you were relying on the fact that Jupyter calls
repr() to display returned values, you may want to call print()
explicitely if you prefer the old representation.
- Fix compilation under Cygwin and Alpine Linux, both choking
on undefined secure_getenv().
We are happy to announce the release of Spot 2.6.3
This is a maintenance release containing only bug fixes.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.6.3.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.6.3 (2018-10-17)
Bugs fixed:
- Running "ltl2tgba -B" on formulas of the type FG(safety) would
unexpectedly use a co-Büchi automaton as an intermediate step.
This in turn caused "ltl2tgba -U -B" to not produce unambiguous
automata.
- ltl2tgba --low now disables the "gf-guarantee" feature, as
documented.
- ltlfilt's --accept-word and --reject-word options were ignored
unless used together.
--
Alexandre Duret-Lutz
