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@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