3.2.4 State space options

The following command line options affect the way in which lbtt generates state spaces that are then used in the model checking tests. They correspond to options in the `StateSpaceOptions' section of the configuration file. See also Random state spaces, for more information about the graph generation modes.

`--edgeprobability=PROBABILITY'

This option sets the approximate random edge probability for state spaces. (The option has no effect if the generated state spaces are random or enumerated paths.)

`--enumeratedpath'

This option instructs lbtt to enumerate all paths of a given size as state spaces instead of generating random state spaces for model checking tests. The option also enables lbtt's internal model checking algorithm.

`--randomconnectedgraph'

This option makes lbtt generate random connected graphs as state spaces for model checking tests.

`--randomgraph'

This option makes lbtt generate random graphs as state spaces for model checking tests.

`--randompath'

This option forces lbtt to generate random paths as state spaces. The option also enables lbtt's internal model checking algorithm in the model checking tests.

`--statespacechangeinterval=NUMBER-OF-ROUNDS'

This option sets the frequency (in test rounds) in which new state spaces are generated. A value of 0 forces lbtt to use a fixed state space for all tests.

`--statespacegeneratemode=randomconnectedgraph | randomgraph | randompath | enumeratedpath'

This option can be used instead of one of the four options above to select the state space generation mode.

`--statespacerandomseed=INTEGER'

This option gives a seed value for generating random numbers required by the random state space generation algorithm.

`--statespacesize=INTEGER'

`--statespacesize=MINIMUM-SIZE-MAXIMUM-SIZE'

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

This option can be used to change the size of the generated state spaces.

`--truthprobability=PROBABILITY'

This option sets the probability that lbtt uses for choosing the valuation for each atomic proposition in each state of the randomly generated state spaces. (This option has no effect if using enumerated paths as state spaces.)