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