6.1 Requirements for translator executables

lbtt assumes each tested LTL-to-Büchi translator to be accessible by running an executable file which should read in an LTL formula from a file, convert it into a Büchi automaton and then write the automaton into another file. For this purpose, the executable should support the following command line interface:

     path-to-program parameters input-file output-file

where path-to-program is the full name (and location) of the executable, parameters are any optional parameters that might be needed for running the executable, and input-file and output-file are two file names. The translator executable should read its input (an LTL formula) from input-file and write its output (a Büchi automaton) into output-file (without removing the input file); see Format for LTL formulas and Format for automata for a description on how these files should be formatted.

The translator executable should always create an output file and then return with a zero exit status in case no errors occur during the translation. lbtt interprets a missing output file or a nonzero exit status as an error and will not in this case try to run any tests, even if an automaton were successfully saved in an output file.

To start testing the translator, add a new `Translator' section for it into lbtt's configuration file (see Configuration file), for example

     Translator
     {
       Name = "LTL-to-Büchi translator"
       Path = /home/lbtt-user/bin/ltl-to-buchi-translator
       Parameters = "-x -y -z"
       Enabled = Yes
     }