Next: Sample configuration file, Previous: FormulaOptions section, Up: Configuration file

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.