3.1.4 The `StateSpaceOptions' section

The `StateSpaceOptions' section defines the parameters that affect the way lbtt generates random state spaces for 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). See also Random state spaces, for more information about the different types of available state spaces and the algorithms used for constructing them. The options available within this section are:

`ChangeInterval = INTEGER'

This option determines how often (in number of test rounds) lbtt should generate a new random state space. A value of 0 forces lbtt to use a fixed state space for all tests. The default behavior is to generate a new state space at the beginning of each test round.

`EdgeProbability = PROBABILITY'

This option sets the approximate probability (between 0.0 and 1.0) of adding a transition from any state x to some other state y when generating random graphs as state spaces. The default value is 0.2. The probability is approximate because lbtt still has to ensure that all states of each generated state spaces have at least one successor, which might require adding extra transitions to the graph. Note: This option has no effect if `GenerateMode' is set to `RandomPath' or `EnumeratedPath'.

`GenerateMode = RandomConnectedGraph | RandomGraph | RandomPath | EnumeratedPath'

This option selects the type of generated state spaces from the four available types. The default value is `RandomConnectedGraph'. See Random state spaces, for more information on the different state space types.

Note: Using the `RandomPath' or the `EnumeratedPath' setting includes lbtt's internal model checking algorithm into the various model checking tests if they are enabled. For more information, see Model checking result cross-comparison test.

`Propositions = INTEGER'

This option sets the number of atomic propositions attached to each state of the generated state spaces. The default value is 5.

Usually this should probably be the same as the maximum number of different atomic propositions in the generated formulas (see FormulaOptions section). If the number of propositions attached to each state of the state spaces is less than the maximum number of different propositions that may occur in the generated formulas, all “extra” propositions in the formulas are considered to be false in every state of the state space.

`RandomSeed = INTEGER'

This option specifies a seed value for generating random numbers required by the random state space generation algorithm. If this option is not present, the seed defaults to 1. See the previous section for how to change the random seed used to initialize the random number generator for the random LTL formula generation algorithm.

`Size = INTEGER'

`Size = MINIMUM-SIZE-MAXIMUM-SIZE'

`Size = MINIMUM-SIZE...MAXIMUM-SIZE'

This option sets the number of states in the generated state spaces. If the size is given as an interval, lbtt either chooses a random size in the interval (including its endpoints) each time a new state space is generated, or, if `GenerateMode' is set to `EnumeratedPath', enumerates all state spaces in the specified range systematically, starting from the minimum size. The default size is 20.

`TruthProbability = PROBABILITY'

Probability (between 0.0 and 1.0) with which each individual atomic proposition has the value `true' in any state of the state space. Note: This option has no effect if `GenerateMode' is set to `EnumeratedPath'. The default value is 0.5.