From Spot 2.0 to Spot 2.10: What’s New?

Spot is a library for LTL and \(\omega \)-automata manipulation, distributed under a GPLv3 license. Its source code is available from https://​spot.​lrde.​epita.​fr/​. We provide packages for some Linux distributions like Debian and Fedora, but other packages can also be found for Conda-Forge [17] (for Linux & Darwin), Arch Linux, FreeBSD...

Spot can be used via three interfaces: a C++17 library, a set of command-line tools that give easy access to many features of the library, and Python bindings, that makes prototyping and interactive work very attractive. Our web site now contains many examples of how to perform some tasks using these three interfaces, and we have a public mailing list for questions.

In our last tool paper [21], Spot 2.0 had just converted from being a library for working on Transition-based Generalized Büchi Automata and had become a library supporting \(\omega \)-automata with arbitrary Emerson-Lei [22, 41] acceptance conditions, as enabled by the development of the HOA format [5].

In the HOA format, transitions can carry multiple colors, and acceptance conditions are expressed as a positive Boolean formulas over atoms like \(\mathsf {Fin}(i)\) or \(\mathsf {Inf}(i)\) that tell if a color should be seen finitely or infinitely often for a run to be accepting. Table 1 gives some examples.

While Spot 2.0 was able to read automata with arbitrary acceptance conditions, not all of its algorithms were able to support such a generality. For instance testing an automaton for emptiness or finding an accepting word, would only work on automata with “\(\mathsf {Fin}\)-less” acceptance conditions. For other conditions, Spot 2.0 would rely on a procedure called remove_fin() to convert automata with arbitrary acceptance conditions into “\(\mathsf {Fin}\)-less” acceptance conditions [9]. This was ultimately fixed by developing a generic emptiness check [6]. Additionally the support for arbitrary acceptance conditions has allowed us to implement many useful algorithms; the most recent being the Alternating Cycle Decomposition [15, 16] a powerful data structure with many applications (conversion to parity acceptance, degeneralization, typeness checks...)¹.

There have been 56 releases of Spot since version 2.0, but only 10 of these are major releases. Releases are numbered 2.x.y where y is updated for minor upgrades that mostly fix bugs, and x is updated for major release that add new features. (The leading 2 would be incremented in case of a serious redesign of the API.) Table 2 summarizes the highlights of the various releases in chronological order. Not appearing in this list are many micro-optimizations and usability improvements that Spot has accumulated over the years.

As it is a library, there are many ways to use Spot. We are mostly aware of such uses via citations². Historical and frequent uses-cases are to use Spot for translating LTL formulas to automata (Winners of the sequential LTL and parallel LTL tracks of RERS’19 challenge [26] both used Spot to translate the properties into automata, many competitors on the Model Checking Contest [28] also use Spot this way), or to use it as a research/development toolbox, since it provides helper tools for generation of random formulas/automata, verification of LTL-to-automata translation, simplifications, syntax conversions, etc. Nowadays, the algorithms for \(\omega \)-automata implemented in Spot are often used as baseline for studying better algorithms [e.g., 25, 32, 18, 33], but we also see some new applications built on top of \(\omega \)-automata algorithms from Spot [e.g., 12, 13].

The projects that have the largest intersections of features with Spot seem to be GOAL [43] and Owl [30]. These are two Java-based frameworks that deal with similar objects and provide a range of algorithms. Owl and Spot share a similar and traditional Unix view of the command-line experience, where multiple commands are expected to be chained with pipes, and they both communicate smoothly via the HOA format [5]. GOAL is centered on a graphical interface in which the user can edit automata, and apply algorithms listed in menu entries. Using GOAL from the command-line is possible by writing short scripts in a custom language.

As far as interfacing goes, the most important feature of Spot is probably that it exposes its algorithms and data structures in Python. Beside being usable as a glue language between various tools, this allows us (1) to leverage Python’s ecosystem and (2) to quickly prototype new algorithms in Python.

In this section and the next three, we focuses on how the storage of automata evolved to support alternation, games, and Mealy machines.

The main automaton class of Spot is called twa_graph and inherits from the twa class. The letters twa stand for Transition-based \(\omega \)-Automaton.

The class twa implements an abstract interface that allows on-the-fly exploration of an automaton similar to what had been present in Spot from the start: essentially, one can query the initial state, and query the transitions leaving any known state. In particular, before exploring the state-space of a twa, it is unknown how many states are reachable. Various subclasses of twa are provided in Spot, for instance to represent the state-space of Promela or Divine models [21]. Users may create subclasses, for instance to create a Kripke structure on-the-fly.³

The class twa_graph, introduced in Spot 2.0, implements an explicit, graph-based, representation of an automaton, in which states and edges are designated by integers. This makes for a much simpler interface⁴ and usually simplifies the data structures used in algorithms (since states and edges can be used as indices in arrays). The data structure is best illustrated by using the show_storage() method of the Python bindings, as shown by Fig. 1. A twa_graph is stored as two C++ vectors: a vector of states, and a vector of edges. For each state, the first vector stores two edge numbers: succ is the first outgoing edge, and succ_tail is the last one. These number are indices into the edge vector, which stores five pieces of information per edge. Four of them are related to the identity of the edge: src, dst, cond, acc are respectively the source, destination, guard, and color sets of the edge. The remaining field, next_succ gives the next outgoing edge, effectively creating a linked list of all edges leaving a given state. There is no edge 0: this value is used as terminator for such lists. Outgoing edges of the same state are not necessarily adjacent in that structure. When a new edge is added to the automaton, it is simply appended to the edge vector, and the succ_tail field of the state is used to update the previous end of the list.

To iterate over successors of state 1 in C++ or Python, one can ignore the above linked list implementation and write one of the following loops:

The twa_graph::out methods simply returns a lightweight temporary object which can be iterated upon using iterators that will follow the linked list. Then the object e is effectively a reference to a column of the edge vector.

As seen on Fig. 1, the automaton additionally stores an initial state (Spot only supports a single initial state), a number of colors (num_sets), an acceptance condition, a list of atomic propositions (Spot only supports alphabets of the form \(2^{ AP }\)), and 10 fields storing structural properties of the automaton.

These property fields have only three possible values: they default to maybe, but can be set to no or yes by algorithms that work on the automaton. They can also be read and written in the HOA format. For instance if prop_universal is set to yes, it means that automaton does not have any existential choice (a.k.a. non-determinism). Spot’s is_deterministic() algorithm can return in constant time if prop_universal is known, otherwise it will inspect the automaton and set that property before returning, so that the next call to is_deterministic() will be instantaneous. Some algorithms know how to take advantage of any hint they get from those properties: for instance the product() of two automata is optimized to use fewer colors when one of the arguments is known to be weak (i.e., in an SCC all transitions have the same colors).

Note that algorithms that modify an automaton in place have to remember to update those properties. This has caused a couple of bugs over the years.

Support for alternating \(\omega \)-automata, as defined in the HOA format, was added to Spot in version 2.3 without introducing a new class. Rather, the twa_graph class was extended to support alternation in such a way that existing algorithms would not require any modification to continue working on automata without universal branching. This was done by reserving the sign bit of the destination state number of each transition to signal universal branching.

Figure 2 shows an example of Alternating automaton (top-left) with co-Büchi acceptance. In many works on alternating automata, it is conventional to not represent accepting sinks, and instead have transition without destination. The top-right picture shows that Spot has a rendering option to hide accepting sinks.

The bottom of the figure shows that the automaton has prop_state_acc set, which means that the automaton is meant to be interpreted as using state-based acceptance. Colors are still stored on edges internally, but all edges leaving a state have the same colors. Seeing that the condition is co-Büchi (\(\mathsf {Fin}(0)\)), the display code automatically switched to the convention of using double-circles for rejecting states.

Destinations with the sign bit set are called universal destination groups and appear as pink in the figure. There are two groups here: ~0 and ~3. The complement of these numbers can be used as indices in the dests vector, that actually store the destination groups. At the given index, one can read the size n of the destination group, followed by the state number of the n destinations.

Algorithms that work on alternating automata need to be able to iterate over all destinations of an edge. The process of checking the sign bit of the destination to decide if its a group, and to iterate on that group is hidden by the univ_dests() method:

Note that this code works on non-universal branches as well: if e.dst is unsigned, univ_dests(e) will simply iterate on that unique value.

Spot has two alternation removal procedures. One is an on-the-fly implementation of the Breakpoint construction [37] which transforms an n-state alternating Büchi automaton into a non-alternating Büchi automaton with at most \(3^n\) states. For very weak alternating automata, it is known that a powerset-based procedure can produce a transition-based generalized Büchi automaton with \(2^n\) states [23]; in fact that algorithm even works on ordered automata [11], i.e., alternating automata where the only rejecting cycles are self-loops. The second alternation removal procedure of Spot is a mix between these two procedures but does not work on the fly: it takes a weak automaton as input, and uses the break-point construction on rejectings SCCs that have more than one state, and uses the powerset construction for other SCCs.

Spot’s automata have a mechanism to attach arbitrary data to automata, called named properties. (This is similar to the notion of attributes in the R language.) An object can be attached to the automaton with:

and later retrieved with:

Spot has grown a list of many such properties over time.⁵ For instance automaton-name stores a string that would be displayed as the name of the automaton. The highlight-edges and highlight-states properties can be used to color edges and states. The state-names is a vector of strings that gives a name to each state, etc. While those examples are mostly related to the graphical rendering of the automata, some algorithms store useful byproducts as properties. For instance the product() algorithm will define a product-states named property that store a vector of pairs of the original states.

These named properties are sometimes used to provide additional semantics to the automaton, for instance to obtain a game or a Mealy machine.

The application of Spot to LTL synthesis was introduced in Spot 2.5 in the form of the ltlsynt tool [35], but the inner workings of this tool were progressively redesigned and publicly exposed until version 2.10.

An automaton can now be turned into a game by attaching the state-player property to it.⁶ Only two-player games are supported, so state-player should be a \(\texttt {std::vector<bool>}\). Currently, Spot has solvers for safety games and for games with parity max odd acceptance, but we plan to at least generalize the latter to any kind of parity condition. Once a game has been solved, it contains two new named properties: state-winner (a \(\texttt {std::vector<bool>}\) indexed by state numbers indicating the player winning in each state), and strategy (a \(\texttt {std::vector<unsigned>}\) that gives for each state the edge that its owner should follow to win).

Figure 3 shows an example of game generated by ltlsynt, and how we can display the winning strategy once the game is solved. The winning strategy can be extracted and converted into a Mealy machine, which is just an automaton that uses the synthesis-output property to specify which atomic propositions belong to the output. Such a Mealy machine can then be encoded into an AND-inverter graph, and saved into the AIGER format [7]. Here L0 represents a latch, i.e., one bit of memory, that stores the previous value of a so that the circuit can output b if and only if a is true in the present and in the previous step.

The Python ecosystem makes it easy to develop web interfaces for convenient access to a subset of features of Spot. For instance Fig. 4 shows screenshots of a web application built using a React frontend, and running Spot on the server. It can transform LTL formulas into automata, can display many properties of a formula (membership to the Manna & Pnueli hierarchy [34], Safety/Liveness classification [2], Rabin and Streett indices [14], stutter-invariance [36]), or simply compare two formulas using a Venn diagram.

This application has been found to be useful for teaching about LTL and its relation with automata, but is also a helpful research tool.

While Spot has been used for many applications, there are two recurrent issues: they are related to the types used for some fields of the edge vector (see Figs. 1–2). By default, the set of colors that labels an edge (the acc field) is stored as a 32-bit bit-vector, the transition label (cond, a formula over \(2^ AP \)), is stored as a BDD identified by a unique 32-bit integer, and the other three fields (src, dst, next_succ) are all 32-bit integers. One edge therefore takes 20 bytes.

While limiting the number of states to 32-bit integers has never been a problem so far, the limit of 32 colors can be hit easily. Spot 2.6 added a compile-time option to enlarge the number of supported colors to any multiple of 32; this evidently has a memory cost (and therefore also a runtime cost) as the acc field will be larger for each edge. However this constraint generally means that all the algorithms we implement try to be “color-efficient”, i.e., to not introduce useless colors. For instance while the product of an automaton with x colors and an automaton with y colors is usually an automaton with \(x+y\) colors, the product() implementation will output fewer colors in presence of a weak automaton.

The use of BDDs as edge labels causes another type of issues. Spot uses a customized version of the BuDDy library, with additional functions, and several optimizations (more compact BDD nodes for better cache friendliness, most operations have been rewritten to be recursion-free). However BuDDy is inherently not thread safe, because of its global unicity table and caches. This prevents us from doing any kind of parallel processing on automata. A long term plan is to introduce a new class twacube that represent an automaton in which edges are cubes (i.e., conjunctions of literals) represented using two bit-vectors. Such a class was experimentally introduced in Spot 2.10 and is currently used in some parallel emptiness check procedures [38].