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
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
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
- `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
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.