3.2.2 Global options
The following list presents the options that can be used to override the
values specified in the `GlobalOptions' section of the configuration
file.
- `--comparisontest[=yes | no]'
- `--nocomparisontest'
- These options enable or disable the model checking result cross-comparison
test (see Model checking result cross-comparison test).
- `--consistencytest[=yes | no]'
- `--noconsistencytest'
- These options enable or disable the model checking result consistency check
(see Model checking result consistency check).
- `--disable=IMPLEMENTATION-ID[,IMPLEMENTATION-ID...]'
- This option can be used to exclude some implementations from the tests by
specifying a comma-separated list of implementation names or their numeric
identifiers. (The implementations are numbered in the order in which they
appear in the configuration file, starting from zero. Use the
`--showconfig' option, see Special options, to obtain a list of the
implementations specified in the configuration file, together with their
identifiers.)
- `--enable=IMPLEMENTATION-ID[,IMPLEMENTATION-ID...]'
- This option can be used to include implementations into the tests (in the
case they are initially disabled in the configuration file).
- `--globalmodelcheck'
- This option instructs lbtt to perform model checking globally
(with respect to all states of each random state space) in the model
checking result cross-comparison test and the model checking result
consistency check. Using a global check increases the number of possible
tests.
- `--interactive[=MODE-LIST]'
- `--pause[=MODE-LIST]'
- These options can be used to override whether lbtt should pause
between test rounds to wait for user input. The optional MODE-LIST is a
comma-separated list of interactivity modes (`Always', `OnError',
`Never', `OnBreak') with no spaces in between
(see Interactivity modes, for the mode descriptions). If omitted, the
mode list defaults to `Always'.
- `--intersectiontest[=yes | no]'
- `--nointersectiontest'
- These options enable or disable the Büchi automata intersection emptiness
check (see Automata intersection emptiness check).
- `--localmodelcheck'
- This option instructs lbtt to perform model checking only with
respect to a single state of each random state space in the model checking
result cross-comparison test and the model checking result consistency
check.
- `--modelcheck=global | local'
- This option can be used to select the model checking mode.
- `--pause[=MODE-LIST]'
- See `--interactive'.
- `--rounds=NUMBER-OF-ROUNDS'
- This option can be used to override the number of test rounds to run.
- `--translatortimeout=TIME-SPECIFICATION'
- This option can be used to override the running time limit (in wall-clock
time) for translators (see Timeouts, for more information).
- `--verbosity=INTEGER'
- This option sets the verbosity of output messages. The value must be
between 0 and 5 (inclusive).