2.1.2 Random state spaces

State spaces are needed as input for tests only in the model checking result cross comparison test (see Model checking result cross-comparison test) and the model checking result consistency check (see Model checking result consistency check). The state spaces are directed labeled graphs, each node of which is labeled with a randomly chosen set of atomic propositions (the propositions that hold in the state corresponding to the graph node). In addition, each state of the state space always has at least one successor.

lbtt provides three different random state space generation algorithms that differ in the structure of the generated state spaces. The common parameters for each of these algorithms are:

• Number of states in the state space.
• Maximum number of different atomic propositions allowed in the label of any state of the state space.
• The probability with which each atomic proposition should hold in a state of the state space (which is, for simplicity, common to all atomic propositions).

The different types of random state spaces that can be generated are:

1. Random connected graphs. These state spaces are guaranteed to have at least one state such that every other state of the state space is reachable from this state. In addition to the three above parameters, the behavior of the algorithm generating these state spaces can be adjusted by specifying a probability which approximates the density of the graph, i.e., the probability that there is a directed edge from a state x to another state y, where x and y are any two states in the state space. For more details, see Algorithm for generating connected graphs.
2. Random graphs. These state spaces are constructed simply by taking all pairs (x, y) of states in the state space and connecting state x to state y with a user-specified probability that approximates the graph density.
3. Random paths. A random path is simply a non-branching sequence of states, where the last state of the sequence is connected to a randomly chosen state earlier in the sequence.

lbtt also includes a state space generation algorithm which systematically enumerates all “paths” (see above) of a given size with a given number of atomic propositions in each state. If |S| is the number of states in the path and |AP| is the number of atomic propositions in each state of the path, it is easy to see that the number of different paths having these parameters is

|S| * 2^(|S| * |AP|),

a number which grows exponentially in the product of the two parameters. Obviously, this makes the exhaustive enumeration of all paths of a given size practicable only for very small values of |S| and |AP|.

In practice, testing should be started using only very small state spaces (say, with only 10–50 states and a small density) regardless of the particular algorithm chosen for generating the state spaces. The size of the state spaces can then be increased if lbtt's memory consumption and the time spent running the tests stay within acceptable limits.