3.1.1 The `Translator' section

Each LTL-to-Büchi translator to be tested requires a separate `Translator' section¹ in the configuration file; there must be at least one such section in the file.

The translators are assumed to be accessible through external executable files. Therefore, this section must at a minimum specify the full file name of the executable to run in order to invoke the translator; see Translator interface, for information about the conventions lbtt uses to communicate with the LTL-to-Büchi translators.

Translators specified in the configuration file are given unique integer identifiers in the order they are listed in the file, starting from zero. These numbers can be used when referring to the different translators when using lbtt's internal commands (see Analyzing test results). Alternatively, the translators can be referred to using the names specified in the configuration file.

The following options (in alphabetical order) are available within this section:

`Enabled = TRUTH-VALUE'

This option determines whether the translator should be initially included in or excluded from the tests. The default value is `Yes'. The translator can be enabled or disabled during testing with lbtt's internal commands (see Test control commands).

`Name = STRING'

This option can be used to specify a unique textual identifier for the LTL-to-Büchi translator. lbtt will use this identifier when displaying various messages concerning the implementation; the identifier can also be used to refer to the implementation when working with lbtt's internal commands (see Analyzing test results). (If no name has been explicitly given for the translator, lbtt assigns the translator a name of the form `Algorithm n', where n is the running integer identifier for the translators.)

The identifier `lbtt' is reserved for lbtt's internal model checking algorithm (see Model checking result cross-comparison test).

`Parameters = STRING'

This option can be used to specify any additional parameters that should be passed to the translator executable whenever running it. (The parameter string defaults to the empty string if the option is not used.)

`Path = STRING'

This option must be given a value for each translator specified in the configuration file. The value should be the complete file name of the program which is used to run the translator.