1. Introduction

Spot supplies algorithms to use in the AutomataTheoreticApproachToModelChecking. Spot does not process any high-level formalism directly, rather it works with a special kind of automata that we will call TGBAs from now on.

Since Spot will not grok any high-level formalism, it means another tool must do the job of converting this formalism into a TGBA that represents the state space of the model to check.

There is two main ways to go about this.

• The first is to have a third-party tool build all the state space at once, save the resulting automaton into an file, and then have Spot read this file and check whatever is needed. This is quite easy because the two tools can be run separately. However this requires all the state-space automaton to be loaded in memory.

  (The ability to read automata on-the-fly is on the SpotWishList.)

• The second way is to have that third-party tool build the state-space automaton on-the-fly, as Spot needs it. This requires the two tools to communicate, so it's a harder road; but it comes with several benefits. In this approach, the state-space generator

  tool appears to Spot as a regular TGBA, on which all the algorithms can be applied.

Note that if you use that second approach, you will get the first for free. Indeed, Spot can dump any TGBA into a text file.

2. The state-space file approach

You can use spot::tgba_parse() to load an automaton from a text file in TgbaTextFormat, and then apply any Spot algorithm. So the hardest part of your work will be to output this TgbaTextFormat.

3. Interfacing Spot with third-party tools

3.1. The plot

Suppose we have a tool that is able to process our high-level formalism and generate its state space step by step. Let's call it atool for the sake of a better name.

By generating the state space step by step we essentially mean that

• atool knows the initial state of the model;

• given any accessible state, atool can compute its successor states.

These are the requirement of the TGBAs used in Spot. Almost all Spot algorithms work using such an interface: getting the initial state, browsing down its successors.

So the plan is to have atool masquerade as a TGBA. More precisely, the atool program will be linked to Spot to use its algorithms, be instead of using one of Spot's own implementations of TGBA, it will be pass it an object that responds to the TGBA interface, but that calls atool's internal state-space generation routines to compute the answers.

3.2. Examples

There are at least two such interfaces that you can look at for example.

• The CheckPn example was built as a tutorial to demonstrate how to interface Spot.

• Spot comes with a GreatSPN interface in its iface/gspn/ directory. Beware that this is much more complicated to read and use (see also the SpotGspnHowTo).

3.3. The details

Spot's TGBA interface is implemented by the tgba abstract base class. (It's actually spot::tgba but we will omit these pedantic prefixes for brevity.)

Spot already supplies several implementation of tgba as subclasses. To interface atool, we would just need to create a new subclass of tgba that conforms to its interface and uses atool's machinery to explore the state space. (This subclass can be defined in atool itself although the base class is in the Spot library, that is not a problem.)

Actually subclassing tgba is not enough: this class has a few acquaintance that need to be subclassed too.

Here are the four base classes you may have to subclass when writing an interface.

• state: A state.

• tgba_succ_iterator: An iterator over the successors of a state.

• tgba: A TGBA.

• environment: The set of atomic properties of the system.

Another class related to these interface is the bdd_dict. However there is no reason to change it.

The following section intend to give you an idea of the purpose of each of these classes and how they are related. For a more precise description of the interface they must comply to, please refer to the Doxygen documentation of Spot (in the doc/ directory of the source tree).

3.3.1. The bdd_dict class

BDD formula are used in the TGBA interface to represent the propositional formulae that guard transitions, as well as the set of acceptance conditions of a transition. (Furthermore, they may be used internally by the automata to represent other private details.)

Since these BDD can be shared between automata, BDD variables (at least those used in the interface) must be used consistently amongst automata.

A bdd_dict object maps a BDD variable to its meaning, and vice-versa. It also provides methods to declare new BDD variables.

Each tgba instance must have an associated bdd_dict. Two tgba instances must share the same bdd_dict in order to be used together (for instance in a product). This bdd_dict is expected to be passed as an argument to the constructor of the tgba implementation, and used each time the implementation needs to choose BDD variables.

A bdd_dict distinguishes three kinds of BDD variables:

• atomic propositions are registered with the register_proposition() method. Mapping between BDD and atomic propositions is achieved with the var_map and var_formula_map associative arrays.

• acceptance conditions are registered with the register_acceptance_variable() method. Each acceptance is associated to an LtlFormula, mapping back and forth can be done with acc_map and acc_formula_map.

• anonymous variables are registered with the register_anonymous_variables() method.

Anonymous variables are expected to be used internally in the object that registered them, so they can have different meaning in different automata. Atomic propositions and acceptance conditions, on the other hand, have the same meaning amongst all automata (that share the same bdd_dict).

bdd_dict currently contains obsolete methods and maps related to variables called Now and Next (or even state). Do not use them.

bdd_dict tries to reuse unused BDD variables as much as possible. In order to do this, it maintain a list of all objects (usually automata) that have registered a given variable. It is important to unregister these variables with when the object is destroyed. The methods unregister_all_my_variables() or unregister_variable() can be used for this.

3.3.2. The state class

state is an abstract class to represent a state of an automaton. Each automaton can have its own way to represent a state. For instance an BDD-based automaton would use a BDD to represent a state; another implementation would use a bitstring, etc. Model-checker usually enforce a unique and compact scheme to represent a state, but that is not the case in Spot where reusability is more important. Algorithms are given an abstract interface to manipulate states; choosing how the state is coded is up to the automaton.

Usually each subclass of tgba defines the corresponding subclass of state. The state's minimal interface consists in three methods. compare() orders two states, hash() return a hash key for the state, and clone() duplicate the state. These three methods are required so that states can be used in the StandardTemplateLibrary containers.

All more complex operations must be implemented in the automaton. For instance to print a state you should call the format_state method of the tgba object that created this state. Such operation usually requires the tgba object to look into the state object. So you may want to use friend declaration, or additional access methods in your subclass of state (please prefer the latter).

3.3.3. The tgba_succ_iterator class

The tgba_succ_iterator abstract class represents the set of successors of a state. It is an iterator (see IteratorPattern) on a list of successors that does not necessarily exist beforehand. The idea is to allow successors to be computed on the fly.

tgba_succ_iterator objects are created by the succ_iter() method of tgba instances.

Like in the state hierarchy, each tgba subclass usually has its own subclass of tgba_succ_iterator with varying implementations. Some automata are not able to compute the successors of a state one by one, so they use an implementation of tgba_succ_iterator that is filled with a precomputed list of successors, and simply iterate over that list. Other implementation of tgba_succ_iterator may be smarter and embed just the necessary information to compute the successor states each after each.

The tgba_succ_iterator interface contains two parts. Three methods allow to control the iteration: first(), next(), and done(). These are meant to be used in a loop as follows.

Three other functions are used to query information about the actual successor.

• current_state() returns the current successor state the iterator is pointing to.

• current_condition() returns the condition on the arc going the this successor.

• current_acceptance_conditions() returns the acceptance conditions of that arc.

It should be noted that a tgba_succ_iterator does not publicize the state for which it generates the successors. Some implementation (especially those that perform on-the-fly computation) might need to store this information, but that is in implementation detail.

3.3.4. The tgba class

When deriving this class, you'll have to implement at least the following methods:

• get_init_state(): return the initial state,

• succ_iter(): return an instance of a subclass of tgba_succ_iterator as described above,

• all_acceptance_conditions(): the set of all acceptance conditions for this automata (most likely you will simply have to return bddfalse, because the usual state space do not have any acceptance condition),

• neg_acceptance_conditions(): the conjunction of negated acceptance conditions (simply return bddtrue if no acceptance conditions are used),

• get_dict(): return the dictionary used by this tgba,

• format_state(): format a state for printing,

• compute_support_conditions(): return a formula that is true on a given state, this is an optimization and it is always safe to return bddtrue,

• compute_support_variables(): the list of all variables used on outgoing arcs (presently this methods is called only when building a product with a GreatSPN automaton, so you could also decide to return bddtrue temporarily until the rest of the interface works, and come back to this method latter).

You may need to override project_state() if your automaton is parameterized by another automaton and it makes sense to project a state of the current automaton on the other one.

3.3.5. The environment class

Environments are mostly useful when parsing LtlFormulae (see HowToParseLtlFormulae). They basically declare which atomic property exists.

Spot offers two standard environments, but you may define your own. The default_environment is a unique (declared using the PPR:SingletonPattern) environment that accept all atomic properties and create them on-the-fly. The declarative_environment, on the other hand, will reject any atomic property that has not been previously declared. Such environment is useful when the set of properties of a system is known beforehand, so that the LTL parser can flag unknown atomic properties.

The reason we present the environment class here is that declarative_environment is also used in the GreatSPN interface as a way to know all the properties GreatSPN will have to compute. (declarative_environment::get_prop_map() returns an array of all declared atomic properties.) This is hardly ideal, because the user have to fill a declarative_environment by listing all atomic properties on the command line before the LtlFormula gets parsed; one could expect that the list of properties be derived from the LtlFormula directly. The historical reason why we do not go this way is that an LtlFormula is not always used, for instance if one just wants to print the reachability graph of some system.