3.1 Configuration file

The configuration file of lbtt contains a list of the LTL-to-Büchi translators to be tested along with other options which affect the way the tests are performed. The configuration file is processed before starting the tests. By default, lbtt will try to read the configuration from the file config in the current working directory; a different file name can be specified with the --configfile=filename command line option.

The configuration file consists of one or more sections, each of which provides a collection of interrelated configuration options. The general format of the configuration file is

     section-name
     {
       option-name = value
       option-name = value
       ...
     }
     
     ...

Section and option names are case-insensitive. Values can be numbers, strings or truth values (`yes' and `no', or equivalently, `true' and `false'). String values are case-sensitive and are subject to common quoting and escaping rules (i.e., string values containing white space should be enclosed in quotes, or the white space characters should be escaped with `\').

Comments can be included by putting a `#' symbol before them; the end of any line containing the `#' character will be ignored when processing the configuration file.

The configuration file must contain at least one `Translator' section specifying an LTL-to-Büchi translator. The other sections are optional and can be used to override the default testing parameters.

• Translator section: Each LTL-to-Büchi translator to be tested requires a separate `Translator' section in the configuration file.
• GlobalOptions section: Options for changing the general behavior of lbtt.
• FormulaOptions section: Options controlling the way random LTL formulas are generated.
• StateSpaceOptions section: Options controlling the way random state spaces are generated.
• Sample configuration file: An example of a configuration file.