We are happy to announce the release of Spot 2.5.
Spot is a library of algorithms for manipulating LTL formulas and
omega-automata (objects as commonly used in model checking).
A detailed list of new features in this new release is given at the end
of this email. The main features of this release are algorithms for
working with parity acceptance, new functions to convert to co-Büchi
when possible, a new tool for LTL synthesis, and some speedup
of our determinization algorithm.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.5.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
(Note that due to some technical issues on our side, it might
be a few days before the packages for Debian *unstable*
are updated.)
This release contains code contributed by Alexandre Gbaguidi Aïsse,
Thibaud Michaud, Laurent Xu, Maximilien Colange, Etienne Renault,
and myself.
As always, please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.5 (2018-01-20)
Build:
- We no longer distribute the doxygen-generated documentation in
the tarball of Spot to save space. This documentation is still
available online at https://spot.lrde.epita.fr/doxygen/. If you
want to build a local copy you can configure Spot with
--enable-doxygen, or simply run "cd doc && make doc".
- All the images that illustrate the documentation have been
converted to SVG, to save space and improve quality.
Tools:
- ltlsynt is a new tool for synthesizing a controller from LTL/PSL
specifications.
- ltlcross learned --reference=COMMANDFMT to specify a translator
that should be trusted. Doing so makes it possible to reduce the
number of tests to be performed, as all other translators will be
compared to the reference's output when available. Multiple
reference can be given; in that case other tools are compared
against the smallest reference automaton.
- autcross, ltlcross, and ltldo learned --fail-on-timeout.
- ltl2tgba, autfilt, and dstar2tgba have some new '--parity' and
'--colored-parity' options to force parity acceptance on the
output. Different styles can be requested using for instance
--parity='min odd' or --parity='max even'.
- ltl2tgba, autfilt, and dstar2tgba have some new '--cobuchi' option
to force co-Büchi acceptance on the output. Beware: if the input
language is not co-Büchi realizable the output automaton will
recognize a superset of the input. Currently, the output is
always state-based.
- genltl learned to generate six new families of formulas, taken from
the SYNTCOMP competition on reactive synthesis, and from from
Müller & Sickert's GandALF'17 paper:
--gf-equiv=RANGE (GFa1 & GFa2 & ... & GFan) <-> GFz
--gf-implies=RANGE (GFa1 & GFa2 & ... & GFan) -> GFz
--ms-example=RANGE GF(a1&X(a2&X(a3&...)))&F(b1&F(b2&F(b3&...)))
--ms-phi-h=RANGE FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|...
--ms-phi-r=RANGE (FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...))
--ms-phi-s=RANGE (FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...))
- autfilt learned --streett-like to convert automata with DNF
acceptance into automata with Streett-like acceptance.
- autfilt learned --acceptance-is=ACC to filter automata by
acceptance condition. ACC can be the name of some acceptance
class (e.g. Büchi, Fin-less, Streett-like) or a precise acceptance
formula in the HOA syntax.
- ltldo learned to limit the number of automata it outputs using -n.
- ltlfilt learned to measure wall-time using --format=%r, and
cpu-time with --format=%R.
- The --format=%g option of tools that output automata used to
print the acceptance condition as a *formula* in the HOA format.
This %g may now take optional arguments to print the acceptance
*name* in different formats. For instance
... | autfilt -o '%[s]g.hoa'
will separate a stream of automata into different files named
by their acceptance name (Buchi, co-Buchi, Streett, etc.) or
"other" if no name is known for the acceptance condition.
- Tools that produce formulas now support --format=%[OP]n to
display the nesting depth of operator OP.
- The new -x tls-impl=N option allows to fine-tune the
implication-based simplification rules of ltl2tgba. See the
spot-x(7) man page for details.
- All tools learned to check the SPOT_OOM_ABORT environment
variable. This is only useful for debuging out-of-memory
conditions. See the spot-x(7) man page for details.
New functions in the library:
- spot::iar() and spot::iar_maybe() use index appearance records (IAR)
to translate Rabin-like automata into equivalent parity automaton.
This translation preserves determinism and is especially useful when
the input automaton is deterministic.
- spot::print_aiger() encodes an automaton as an AIGER circuit, as
required by the SYNTCOMP competition. It relies on a new named
property "synthesis outputs" that describes which atomic
propositions are to be encoded as outputs of the circuits.
- spot::dnf_to_streett() converts any automaton with a DNF
acceptance condition into a Streett-like automaton.
- spot::nsa_to_nca(), spot::dfn_to_nca(), spot::dfn_to_dca(), and
spot::nsa_to_dca(), convert automata with DNF or Streett-like
acceptance into deterministic or non-deterministic co-Büchi
automata. spot::to_dca() and spot::to_nca() dispatch between
these four functions. The language of produced automaton includes
the original language, but may be larger if the original automaton
is not co-Büchi realizable. Based on Boker & Kupferman FOSSACS'11
paper. Currently only supports state-based output.
- spot::scc_info::states_on_acc_cycle_of() returns all states
visited by any accepting cycle of the specified SCC. It only
works on automata with Streett-like acceptance.
- spot::is_recurrence(), spot::is_persistence(), and
spot::is_obligation() test if a formula is a recurrence,
persistance or obligation. The SPOT_PR_CHECK and SPOT_O_CHECK
environment variables can be used to select between multiple
implementations of these functions (see the spot-x(7) man page).
- spot::is_colored() checks if an automaton is colored
(i.e., every transition belongs to exactly one acceptance set).
- spot::change_parity() converts between different parity acceptance
conditions.
- spot::colorize_parity() transforms an automaton with parity
acceptance into a colored automaton (which is often what people
working with parity automata expect).
- spot::cleanup_parity_acceptance() simplifies a parity acceptance
condition.
- spot::parity_product() and spot::parity_product_or() are
specialized (but expensive) products that preserve parity
acceptance.
- spot::remove_univ_otf() removes universal transitions on the fly
from an alternating Büchi automaton using Miyano and Hayashi's
breakpoint algorithm.
- spot::stutter_invariant_states(),
spot::stutter_invariant_letters(),
spot::highlight_stutter_invariant_states(), ... These functions
help study a stutter-sensitive automaton and detect the subset of
states that are stutter-invariant. See
https://spot.lrde.epita.fr/ipynb/stutter-inv.html for examples.
- spot::acc_cond::name(fmt) is a new method that names well-known
acceptance conditions. The fmt parameter specifies the format to
use for that name (e.g. to the style used in HOA, or that used by
print_dot()).
- spot::formula::is_leaf() method can be used to detect formulas
without children (atomic propositions, or constants).
- spot::nesting_depth() computes the nesting depth of any LTL
operator.
- spot::check_determinism() sets both prop_semi_deterministic()
and prop_universal() appropriately.
Improvements to existing functions in the library:
- spot::tgba_determinize() has been heavily rewritten and
optimized. The algorithm has (almost) not changed, but it is
much faster now. It also features an optimization for
stutter-invariant automata that may produce slightly smaller
automata.
- spot::scc_info now takes an optional argument to disable some
features that are expensive and not always necessary. By
default scc_info tracks the list of all states that belong to an
SCC (you may now ask it not to), tracks the successor SCCs of
each SCC (that can but turned off), and explores all SCCs of the
automaton (you may request to stop on the first SCC that is
found accepting).
- In some cases, spot::degeneralize() would output Büchi automata
with more SCCs than its input. This was hard to notice, because
very often simulation-based simplifications remove those extra
SCCs. This situation is now detected by spot::degeneralized()
and fixed before returning the automaton. A new optional
argument can be passed to disable this behavior (or use -x
degen-remscc=0 from the command-line).
- The functions for detecting stutter-invariant formulas or
automata have been overhauled. Their interface changed
slightly. They are now fully documented.
- spot::postprocessor::set_type() can now request different forms
of parity acceptance as output. However currently the
conversions are not very smart: if the input does not already
have parity acceptance, it will simply be degeneralized or
determinized.
- spot::postprocessor::set_type() can now request co-Büchi
acceptance as output. This calls the aforementioned to_nca() or
to_dca() functions.
- spot::remove_fin() will now call simplify_acceptance(),
introduced in 2.4, before attempting its different Fin-removal
strategies.
- spot::simplify_acceptance() was already merging identical
acceptance sets, and detecting complementary sets i and j to
perform the following simplifications
Fin(i) & Inf(j) = Fin(i)
Fin(i) | Inf(j) = Inf(i)
It now additionally applies the following rules (again assuming i
and j are complementary):
Fin(i) & Fin(j) = f Inf(i) | Inf(j) = t
Fin(i) & Inf(i) = f Fin(i) | Inf(i) = t
- spot::formula::map(fun) and spot::formula::traverse(fun) will
accept additionnal arguments and pass them to fun(). See
https://spot.lrde.epita.fr/tut03.html for some examples.
Python-specific changes:
- The "product-states" property of automata is now accessible via
spot.twa.get_product_states() and spot.twa.set_product_states().
- twa_word instances can be displayed as SVG pictures, with one
signal per atomic proposition. For some examples, see the use of
the show() method in https://spot.lrde.epita.fr/ipynb/word.html
- The test suite is now using v4 of the Jupyter Notebook format.
- The function rabin_is_buchi_realizable() as its name suggests checks
if a rabin aut. is Büchi realizable. It is heavily based on
tra_to_tba() algorithm.
Deprecation notices:
(These functions still work but compilers emit warnings.)
- spot::scc_info::used_acc(), spot::scc_info::used_acc_of() and
spot::scc_info::acc() are deprecated. They have been renamed
spot::scc_info::marks(), spot::scc_info::marks_of() and
spot::scc_info::acc_sets_of() respectively for clarity.
Backward incompatible changes:
- The spot::closure(), spot::sl2(), spot::is_stutter_invariant()
functions no longer take && arguments. The former two have
spot::closure_inplace() and spot::sl2_inplace() variants. These
functions also do not take a list of atomic propositions as an
argument anymore.
- The spot::bmrand() and spot::prand() functions have been removed.
They were not used at all in Spot, and it is not Spot's objective
to provide such random functions.
- The spot::bdd_dict::register_all_propositions_of() function has
been removed. This low-level function was not used anywhere in
Spot anymore, since it's better to use spot::twa::copy_ap_of().
Bugs fixed:
- spot::simplify_acceptance() could produce incorrect output if the
first edge of the automaton was the only one with no acceptance
set. In spot 2.4.x this function was only used by autfilt
--simplify-acceptance; in 2.5 it is now used in remove_fin().
- spot::streett_to_generalized_buchi() could generate incorrect
automata with empty language if some Fin set did not intersect all
accepting SCCs (in other words, the fix from 2.4.1 was incorrect).
- ltlcross could crash when calling remove_fin() on an automaton
with 32 acceptance sets that would need an additional set.
- the down_cast() helper function used in severaly headers of Spot
was not in the spot namespace, and caused issues with some
configurations of GCC.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.4.4
This is a maintenance release containing fixes for two serious bugs
reported by František Blahoudek.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.4.4.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
New in spot 2.4.4 (2017-12-25)
Bugs fixed:
- The generic to_generalized_buchi() function would fail if the
Fin-less & CNF version of the acceptance condition had several
unit clauses.
- If the automaton passed to sbacc() was incomplete or
non-deterministic because of some unreachable states, then it was
possible that the output would marked similarly while it was in
fact complete or deterministic.
Merry Christmas,
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.4.3
This is a maintenance release containing only minor bug fixes and
documentation changes.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.4.3.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
New in spot 2.4.3 (2017-12-19)
Bugs fixed:
- couvreur99_new() leaked memory when processing TωA that allocate
states.
- Some mismatched placement-new/delete reported by ASAN were fixed.
- Static compilation was broken on MinGW.
- Execution of Jupyter notebooks from the testsuite failed with
recent versions of Python.
- Fix some warnings triggered by the development version of g++.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.4.2
This is a maintenance release containing only minor bug fixes and
documentation changes.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.4.2.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
New in spot 2.4.2 (2017-11-07)
Tools:
- ltlcross and ltldo support ltl3tela, the new name of ltl3hoa.
Bugs fixed:
- Automata produced by "genaut --ks-nca=N" were incorrectly marked
as not complete.
- Fix some cases for which the highest setting of formulas
simplification would produce worse results than lower settings.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.4.1
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.4.1.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
This release contains patches contributed by Maximilien Colange,
Florian Perlié-Long, Alexandre Gbaguidi Aïsse, and myself.
As always, please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.4.1 (2017-10-05)
Bugs fixed:
- The formula class failed to build {a->c[*]} although it is
allowed by our grammar.
- spot::scc_info::determine_unknown_acceptance() incorrectly
considered some rejecting SCC as accepting.
- spot::streett_to_generalized_buchi() could generate automata with
empty language if some Fin set did not intersect all accepting
SCCs. As a consequence, some Streett-like automata were
considered empty even though they were not. Also, the same
function could crash on input that had a Streett-like acceptance
not using all declared sets.
- The twa_graph::merge_edges() function relied on BDD IDs to sort
edges. This in turn caused some algorithms (like the
degeneralization) to produce slighltly different (but still correct)
outputs depending on the BDD operations performed before.
- spot::simulation() could incorrectly flag an automaton as
non-deterministic.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.4.
Spot is a library of algorithms for manipulating LTL formulas and
omega-automata (objects as commonly used in model checking).
A detailed list of new features in this new release is given at the end
of this email. You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.4.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
This release contains code contributed by Clément Gillard, Etienne
Renault, Henrich Lauko, Maximilien Colange, Thomas Medioni and myself.
As always, please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.4 (2017-09-06)
Build:
- Spot is now built in C++14 mode, so you need at least GCC 5 or
clang 3.4. The current version of all major linux distributions
ship with at least GCC 6, which defaults to C++14, so this should
not be a problem. In *this* release of Spot, most of the header
files are still C++11 compatible, so you should be able to include
Spot in a C++11 project in case you do not yet want to upgrade.
There is also an --enable-c++17 option to configure in case you
want to force a build of Spot in C++17 mode.
Tools:
- genaut is a new binary that produces families of automata defined
in the literature (in the same way as we have genltl for LTL
formulas).
- autcross is a new binary that compares the output of tools
transforming automata (in the same way as we have ltlcross for
LTL translators).
- genltl learned two generate two new families of formulas:
--fxg-or=RANGE F(p0 | XG(p1 | XG(p2 | ... XG(pn))))
--gxf-and=RANGE G(p0 & XF(p1 & XF(p2 & ... XF(pn))))
The later is a generalization of --eh-pattern=9, for which a
single state TGBA always exists (but previous version of Spot
would build larger automata).
- autfilt learned to build the union (--sum) or the intersection
(--sum-and) of two languages by putting two automata side-by-side
and fiddling with the initial states. This complements the already
implemented intersection (--product) and union (--product-or),
both based on a product.
- autfilt learned to complement any alternating automaton with
option --dualize. (See spot::dualize() below.)
- autfilt learned --split-edges to convert labels that are Boolean
formulas into labels that are min-terms. (See spot::split_edges()
below.)
- autfilt learned --simplify-acceptance to simplify some acceptance
conditions. (See spot::simplify_acceptance() below.)
- autfilt --decompote-strength has been renamed to --decompose-scc
because it can now extract the subautomaton leading to an SCC
specified by number. (The old name is still kept as an alias.)
- The --stats=%c option of tools producing automata can now be
restricted to count complete SCCs, using %[c]c.
- Tools producing automata have a --stats=... option, and tools
producing formulas have a --format=... option. These two options
work similarly, the use of different names is just historical.
Starting with this release, all tools that recognize one of these
two options also accept the other one as an alias.
Library:
- A new library, libspotgen, gathers all functions used to generate
families of automata or LTL formulas, used by genltl and genaut.
- spot::sum() and spot::sum_and() implements the union and the
intersection of two automata by putting them side-by-side and
using non-deterministim or universal branching on the initial
state.
- twa objects have a new property: prop_complete(). This obviously
acts as a cache for the is_complete() function.
- spot::dualize() complements any alternating automaton. Since
the dual of a deterministic automaton is still deterministic, the
function spot::dtwa_complement() has been deprecated and simply
calls spot::dualize().
- spot::decompose_strength() was extended and renamed to
spot::decompose_scc() as it can now also extract a subautomaton
leading to a particular SCC. A demonstration of this feature via
the Python bindings can be found at
https://spot.lrde.epita.fr/ipynb/decompose.html
- The print_dot() function will now display names for well known
acceptance conditions under the formula when option 'a' is used.
We plan to enable 'a' by default in a future release, so a new
option 'A' has been added to hide the acceptance condition.
- The print_dot() function has a new experimental option 'x' to
output labels are LaTeX formulas. This is meant to be used in
conjunction with the dot2tex tool. See
https://spot.lrde.epita.fr/oaut.html#dot2tex
- A new named property for automata called "original-states" can be
used to record the origin of a state before transformation. It is
currently defined by the degeneralization algorithms, and by
transform_accessible() and algorithms based on it (like
remove_ap::strip(), decompose_scc()). This is realy meant as an
aid for writing algorithms that need this mapping, but it can also
be used to debug these algorithms: the "original-states"
information is displayed by the dot printer when the 'd' option is
passed. For instance in
% ltl2tgba 'GF(a <-> Fb)' --dot=s
% ltl2tgba 'GF(a <-> Fb)' | autfilt -B --dot=ds
the second command outputs an automaton with states that show
references to the first one.
- A new named property for automata called "degen-levels" keeps track
of the level of a state in a degeneralization. This information
complements the one carried in "original-states".
- A new named property for automata called "simulated-states" can be
used to record the origin of a state through simulation. The
behavior is similar to "original-states" above. Determinization
takes advantage of this in its pretty print.
- The new function spot::acc_cond::is_streett_like() checks whether
an acceptance condition is conjunction of disjunctive clauses
containing at most one Inf and at most one Fin. It builds a
vector of pairs to use if we want to assume the automaton has
Streett acceptance. The dual function is
spot::acc_cond::is_rabin_like() works similarly.
- The degeneralize() function has learned to consider acceptance
marks common to all edges comming to a state to select its initial
level. A similar trick was already used in sbacc(), and saves a
few states in some cases.
- There is a new spot::split_edges() function that transforms edges
(labeled by Boolean formulas over atomic propositions) into
transitions (labeled by conjunctions where each atomic proposition
appear either positive or negative). This can be used to
preprocess automata before feeding them to algorithms or tools
that expect transitions labeled by letters.
- spot::scc_info has two new methods to easily iterate over the
edges of an SCC: edges_of() and inner_edges_of().
- spot::scc_info can now be passed a filter function to ignore
or cut some edges.
- spot::scc_info now keeps track of acceptance sets that are common
to all edges in an SCC. These can be retrieved using
scc_info::common_sets_of(scc), and they are used by scc_info to
classify some SCCs as rejecting more easily.
- The new function acc_code::remove() removes all the given
acceptance sets from the acceptance condition.
- It is now possible to change an automaton acceptance condition
directly by calling twa::set_acceptance().
- spot::cleanup_acceptance_here now takes an additional boolean
parameter specifying whether to strip useless marks from the
automaton. This parameter is defaulted to true, in order to
keep this modification backward-compatible.
- The new function spot::simplify_acceptance() is able to perform
some simplifications on an acceptance condition, and might lead
to the removal of some acceptance sets.
- The function spot::streett_to_generalized_buchi() is now able to
work on automata with Streett-like acceptance.
- The function for converting deterministic Rabin automata to
deterministic Büchi automata (when possible), internal to the
remove_fin() procedure, has been updated to work with
transition-based acceptance and with Rabin-like acceptance.
- spot::relabel_here() was used on automata to rename atomic
propositions, it can now replace atomic propositions by Boolean
subformula. This makes it possible to use relabeling maps
produced by relabel_bse() on formulas.
- twa_graph::copy_state_names_from() can be used to copy the state
names from another automaton, honoring "original-states" if
present.
- Building automata for LTL formula with a large number N of atomic
propositions can be costly, because several loops and
data-structures are exponential in N. However a formula like
((a & b & c) | (d & e & f)) U ((d & e & f) | (g & h & i))
can be translated more efficiently by first building an automaton
for (p0 | p1) U (p1 | p2), and then substituting p0, p1, p2 by the
appropriate Boolean formula. Such a trick is now attempted
for translation of formulas with 4 atomic propositions or
more (this threshold can be changed, see -x relabel-bool=N in
the spot-x(7) man page).
- The LTL simplification routines learned that an LTL formula like
G(a & XF(b & XFc & Fd) can be simplified to G(a & Fb & Fc & Fd),
and dually F(a | XG(b | XGc | Gd)) = F(a | Gb | Gc | Gd).
When working with SERE, the simplification of "expr[*0..1]" was
improved. E.g. {{a[*]|b}[*0..1]} becomes {a[*]|b} instead of
{{a[+]|b}[*0..1]}.
- The new function spot::to_weak_alternating() is able to take an
input automaton with generalized Büchi/co-Büchi acceptance and
convert it to a weak alternating automaton.
- spot::sbacc() is can now also convert alternating automata
to state-based acceptance.
- spot::sbacc() and spot::degeneralize() learned to merge
accepting sinks.
- If the SPOT_BDD_TRACE environment variable is set, statistics
about BDD garbage collection and table resizing are shown.
- The & and | operators for acceptannce conditions have been changed
slightly to be more symmetrical. In older versions, operator &
would move Fin() terms to the front, but that is not the case
anymore. Also operator & was already grouping all Inf() terms
(for efficiency reasons), in this version operator | is
symmetrically grouping all Fin() terms.
- The automaton parser is now reentrant, making it possible to
process automata from different streams at the same time (i.e.,
using multiple spot::automaton_stream_parser instances at once).
- The print_hoa() and parse_automaton() functions have been updated
to recognize the "exist-branch" property of the non-released HOA
v1.1, as well as the new meaning of property "deterministic". (In
HOA v1 "properties: deterministic" means that the automaton has no
existential branching; in HOA v1.1 it disallows universal
branching as well.) The meaning of "deterministic" in Spot has
been adjusted to these new semantics, see "Backward-incompatible
changes" below.
- The parser for HOA now recognizes and verifies correct use of the
"univ-branch" property. This is known to be a problem with option
-H1 of ltl3ba 1.1.2 and ltl3dra 0.2.4, so the environment variable
SPOT_HOA_TOLERANT can be set to disable the diagnostic.
Python:
- The 'spot.gen' package exports the functions from libspotgen.
See https://spot.lrde.epita.fr/ipynb/gen.html for examples.
Bugs fixed:
- When the remove_fin() function was called on some automaton with
Inf-less acceptance involving at least one disjunction (e.g.,
generalized co-Büchi), it would sometimes output an automaton with
transition-based acceptance but marked as state-based.
- The complete() function could complete an empty co-Büchi automaton
into an automaton accepting everything.
Backward-incompatible changes:
- spot::acc_cond::mark_t::operator bool() has been marked as
explicit. The implicit converion to bool (and, via bool, to int)
was a source of bugs.
- spot::twa_graph::set_init_state(const state*) has been removed.
It was never used. You always want to use
spot::twa_graph::set_init_state(unsigned) in practice.
- The previous implementation of spot::is_deterministic() has been
renamed to spot::is_universal(). The new version of
spot::is_deterministic() requires the automaton to be both
universal and existential. This should not make any difference in
existing code unless you work with the recently added support for
alternating automata.
- spot::acc_cond::mark_t::sets() now returns an internal iterable
object instead of an std::vector<unsigned>.
- The color palette optionally used by print_dot() has been extended
from 9 to 16 colors. While the first 8 colors are similar, they
are a bit more saturated now.
Deprecation notices:
(These functions still work but compilers emit warnings.)
- spot::decompose_strength() is deprecated, it has been renamed
to spot::decompose_scc().
- spot::dtwa_complement() is deprecated. Prefer the more generic
spot::dualize() instead.
- The spot::twa::prop_deterministic() methods have been renamed to
spot::twa::prop_universal() for consistency with the change to
is_deterministic() listed above. We have kept
spot::twa::prop_deterministic() as a deprecated synonym for
spot::twa::prop_universal() to help backward compatibility.
- The spot::copy() function is deprecated. Use
spot::make_twa_graph() instead.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.3.5
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.3.5.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
Furthermore, as Debian 9 "Stretch" was recently released, the stable
Debian packages we distribute (see
http://www.lrde.epita.fr/install.html) are now built for Stretch.
As always, please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.3.5 (2017-06-22)
Bugs fixed:
- We have fixed new cases where translating multiple formulas in a
single ltl2tgba run could produce automata different from those
produced by individual runs.
- The print_dot() function had a couple of issues when printing
alternating automata: in particular, when using flag 's' (display
SCC) or 'y' (split universal destination by colors) universal
edges could be connected to undefined states.
- Using --stats=%s or --stats=%s or --stats=%t could take an
unnecessary long time on automata with many atomic propositions,
due to a typo. Furthermore, %s/%e/%t/%E/%T were printing
a number of reachable states/edges/transitions, but %S was
incorrectly counting all states even unreachable.
- Our verson of BuDDy had an incorrect optimization for the
biimp operator.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.3.4
This is a maintenance release that only contains bug fixes
(listed below), and also corrects some minor build issues and
typos.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.3.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.3.4 (2017-05-11)
Bugs fixed:
- The transformation to state-based acceptance (spot::sbacc()) was
incorrect on automata where the empty acceptance mark is accepting.
- The --help output of randaut and ltl2tgba was showing an
unsupported %b stat.
- ltldo and ltlcross could leave temporary files behind when
aborting on error.
- The LTL simplifcation rule that turns F(f)|q into F(f|q)
when q is a subformula that is both eventual and universal
was documented but not applied in some forgotten cases.
- Because of some caching inside of ltl2tgba, translating multiple
formula in single ltl2tgba run could produce automata different
from those produced by individual runs.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.3.3.
This is a maintenance release that only contains minor bug fixes, and
minor enhancements, as listed below. This release contains
contributions from Thomas Medioni, Maximilien Colange, and myself.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.3.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.3.3 (2017-04-11)
Tools:
- ltldo and ltlcross learned shorthands to talk to ltl2da, ltl2dpa,
and ltl2ldba (from Owl) without needing to specify %f>%O.
- genltl learned --spec-patterns as an alias for --dac-patterns; it
also learned two new sets of LTL formulas under --hkrss-patterns
(a.k.a. --liberouter-patterns) and --p-patterns
(a.k.a. --beem-patterns).
Bugs fixed:
- In "lenient" mode the formula parser would fail to recover from a
missing closing brace.
- The output of 'genltl --r-left=1 --r-right=1 --format=%F' had
typos.
- 'ltl2tgba Fa | autfilt --complement' would incorrectly claim that
the output is "terminal" because dtwa_complement() failed to reset
that property.
- spot::twa_graph::purge_unreachable_states() was misbehaving on
alternating automata.
- In bench/stutter/ the .cc files were not compiling due to warnings
being caught as errors.
- The code in charge of detecting DBA-type Rabin automata is
actually written to handle a slightly larger class of acceptance
conditions (e.g., Fin(0)|(Fin(1)&Inf(2))), however it failed to
correctly detect DBA-typeness in some of these non-Rabin
acceptance.
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.3.2.
This is a maintenance release that only contains minor bug fixes, and
minor enhancements, as listed below.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.3.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.3.2 (2017-03-15)
Tools:
- In tools that output automata, the number of atomic propositions
can be output using --stats=%x (output automaton) or --stats=%X
(input automaton). Additional options can be passed to list
atomic propositions instead of counting them. Tools that output
formulas also support --format=%x for this purpose.
Python:
- The bdd_to_formula(), and to_generalized_buchi() functions can now
be called in Python.
Documentation:
- https://spot.lrde.epita.fr/tut11.html is a new page describing
how to build monitors in Shell, Python, or C++.
Bugs fixed:
- The tests using LTSmin's patched version of divine would fail
if the current (non-patched) version of divine was installed.
- Because of a typo, the output of --stats='...%P...' was correct
only if %p was used as well.
- genltl was never meant to have (randomly attributed) short
options for --postive and --negative.
- a typo in the code for transformating transition-based acceptance
to state-based acceptance could cause a superfluous initial state
to be output in some cases (the result was still correct).
- 'ltl2tgba --any -C -M ...' would not complete automata.
- While not incorrect, the HOA properties output by 'ltl2tgba -M'
could be 'inherently-weak' or 'terminal', while 'ltl2tgba -M -D'
would always report 'weak' automata. Both variants now report the
most precise between 'weak' or 'terminal'.
- spot::twa_graph::set_univ_init_state() could not be called with
an initializer list.
- The Python wrappers for spot::twa_graph::state_from_number and
spot::twa_graph::state_acc_sets were broken in 2.3.
- Instantiating an emptiness check on an automaton with unsupported
acceptance condition should throw an exception. This used to be
just an assertion, disabled in release builds; the difference
matters for the Python bindings.
Deprecation notice:
- Using --format=%a to print the number of atomic propositions in
ltlfilt, genltl, and randltl still works, but it is not documented
anymore and should be replaced by the newly-introduced --format=%x
for consistency with tools producing automata, where %a means
something else.
--
Alexandre Duret-Lutz
