Next: , Previous: Translator section, Up: Configuration file


3.1.2 The `GlobalOptions' section

The `GlobalOptions' section includes options that affect the general behavior of lbtt. Options available within this section are (in alphabetical order):

`ComparisonCheck = TRUTH-VALUE'
`ComparisonTest = TRUTH-VALUE'
This option can be used to enable or disable the model checking result cross-comparison test (see Model checking result cross-comparison test). The test is enabled by default.
`ConsistencyCheck = TRUTH-VALUE'
`ConsistencyTest = TRUTH-VALUE'
This option can be used to enable or disable the model checking result consistency check (see Model checking result consistency check). The test is enabled by default.
`Interactive = MODE-LIST'
This option determines when lbtt should pause to wait for user input between test rounds. The MODE-LIST is a comma-separated list of the following modes (with no spaces in between the modes):
`Always'
Pause unconditionally after each test round.
`OnError'
Pause testing only after failed test rounds.
`Never'
Run all tests without interruption.
`OnBreak'
Pause testing when requested by the user (for example, after receiving a break signal from the keyboard). If this mode is not specified, `lbtt' will respond to break signals by aborting.

(Since the first three interactivity modes are mutually exclusive, it does not make sense to combine these modes with each other.) The default mode list consists of the value `Always', that is, testing is paused after every test round, and signalling a break will abort testing.

`IntersectionCheck = TRUTH-VALUE'
`IntersectionTest = TRUTH-VALUE'
This option can be used to enable or disable the Büchi automata intersection emptiness check (see Automata intersection emptiness check). The test is enabled by default.
`ModelCheck = Local | Global'
This option determines whether lbtt should perform model checking with respect to all states of each state space or only with respect to a single state of each state space. This affects the number of tests that lbtt makes during 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). Global model checking (the default) maximizes the number of tests, but may require more time and memory. (Note: This option has no effect if none of the model checking tests is enabled.)
`Rounds = INTEGER'
The `Rounds' option can be used to specify the number of test rounds to run; the default value is 10.
`TranslatorTimeout = TIME-SPECIFICATION'
This option can be used to specify a time limit (in wall-clock time) after which the execution of a translator is aborted if it fails to produce a result within the given limit. A timeout is considered a test failure. The time specification is of the form `[hours]h[minutes]min[seconds]s' where hours, minutes and seconds specify the time limit in the obvious way (time units having value 0 can be omitted). For example, a limit of `1h30min' sets the limit at one hour and thirty minutes.
`Verbosity = INTEGER'
This option sets the verbosity level for output messages. The value can be an integer between 0 and 5 (inclusive). A value of 0 will suppress all messages (and is therefore useful only when storing test results into a log file; see `--logfile' command line option); increasing the value results in more output. The default value is 3.