Previous: Format for automata, Up: Interfacing with lbtt


6.4 The lbtt-translate utility

The lbtt source distribution includes a small utility which can be used as a common interface for the following publicly available LTL-to-Büchi translator algorithm implementations:

To use lbtt for testing the LTL-to-Büchi translators included in these tools, you should first install the tool normally by following its installation instructions. Then add the following `Translator' section in lbtt's configuration file:

     Translator
     {
       Name = "[name for the implementation]"
       Path = "[path to lbtt-translate]"
       Parameters = "[implementation selector] [path to executable]"
       Enabled = Yes
     }

where [path to lbtt-translate] contains the complete path and file name of the lbtt-translate tool executable, [implementation selector] is either of the options `--lbt' or `--spin', and [path to executable] is the full path of the tool executable. The names of these executables are usually (assuming a normal installation) lbt and spin, respectively.

Note: These implementations may not have built-in support for all of the LTL formula operators available for generating random LTL formulas with lbtt. See the documentation of each translator for information about which operators are supported, and then change the parameters in lbtt's configuration file accordingly to disable the unsupported operators (or instruct lbtt to read the formulas from an external source by invoking lbtt with the `--formulafile' command line option).

The lbtt-translate utility can also be invoked directly from the shell to translate an LTL formula into a Büchi automaton using either of the above translators. Use the command lbtt-translate --help to see a short summary of available options.