1. Introduction

This document should give you an idea of how to interface Spot with a third-party tool that can produce a state space.

Spot offers algorithms to use in the AutomataTheoreticApproachToModelChecking, so you can build your own model checker, however it does not process any kind high-level formalism directly. Rather, Spot manipulates a special kind of automata: Transition-based Generalized Automata (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.

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.

A variant of this second approach is to interface the tool not as a TGBA, but as a Kripke structure. In Spot a Kripke structure is just a subclass of a TGBA, so its usage is not different, however Kripke structures have a simpler interface to implement.

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

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, but 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.

Another plan would be to have atool masquerade as a Kripke structure. This works in the same way, because a Kripke structure is just a subclass of a TGBA, but with a smaller interface to implement. For instance a TGBA needs to deal with acceptance conditions while a Kripke structure does not.

The following sections describe the TGBA interface before describing the Kripke structure interface.

3.2. Examples

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

3.3. Details for the TGBA interface

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.

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

The following sections 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 formulae 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). Actually, one seldom wants to build two bdd_dicts: most programs use a single bdd_dict shared by all automata. 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:

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 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 that represents 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 a corresponding subclass of state.

The state's minimal interface consists in four methods:

The first two methods are required so that states can be used in the StandardTemplateLibrary containers.

The clone() and destroy() methods are used for memory management. When a state object is returned to the user (for instance by the tgba::get_init_state() method or by tgba_succ_iterator::current_state() method described below), the user has ownership of the state instance, and should call destroy() once the state is no longer needed.

/!\ States should be released by calling destroy(), not using delete. The default implementation of destroy() is to call delete, so if the states you implement for your automaton are allocated by new, you need not implement destroy(). However, the current interface could also allow you to implement a reference counting scheme, where clone() increments a counter, and destroy() decrements a counter and only releases the state when the counter reaches 0.

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 one by one, on demand.

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.

tgba_succ_iterator* i = automaton->succ_iter(some_state);
for (i->first(); !i->done(); i->next())
  {
     // use i
  }
delete i;

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

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:

Optionally, you may want to implement transition_annotation(). This function takes a tgba_succ_iterator and returns some string denoting the current transition. This can be useful, for instance to name the transition of a Petri Net that is being fired when displaying a counterexample. The default implementation of transition_annotation() returns an empty string.

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. Otherwise, the default implementation of project_state() should suit most cases.

3.3.5. The environment class

Environments are mostly useful when parsing LtlFormulae (see HowToParseLtlFormulae). They basically declare which atomic properties 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 accepts 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 with a precise error message.

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.

3.4. Details for the Kripke structure interface

If atool generates a state-space that has properties on states (not transitions) and does not use acceptance conditions, you should consider implementing the kripke interface.

The kripke class is a subclass of tgba that already implements some of the methods you would have to implement.

Not only is it simpler to implement, but also the product between a kripke and a tgba (representing the property) is more efficient than the product between two tgbas: so the model checking process should be faster.

3.4.1. The kripke class

This class is defined in file kripke/kripke.hh. When implementing a subclass, you only need to implement the following methods:

Three of these methods have already been described in the section describing the tgba class. The only new method is state_condition() that should return a BDD describing value of the atomic propositions on the given state.

The other methods of the tgba interface are provided by this class and need not be redefined.

3.4.2. The kripke_succ_iterator class

This class is a subclass of tgba_succ_iterator class that defines current_acceptance_conditions() and current_condition(), so that you only need to supply an implementation of first(), next(), done(), and the current_state() methods.

InterfacingSpot (last edited 2012-03-19 12:49:56 by AlexandreDuretLutz)

All text is available under the terms of the GNU Free Documentation License, see SpotWikiLicense for details.