6 Interfacing with lbtt

The output generated by lbtt consists of textual messages and an optional error log file (see `--logfile' command line option). The format of the output messages is determined by the verbosity mode; for more information, see Interpreting the output. In addition, lbtt returns one of the following three values as its exit status upon normal termination:

• 0: lbtt exited successfully; no errors were detected during testing.
• 1: lbtt exited successfully; errors were detected during testing.
• 2: An error was found when reading the program configuration or when processing the command line options.
• 3: lbtt exited due to an unrecoverable internal error.

The rest of this chapter gives the details on how to use lbtt for testing LTL-to-Büchi translation algorithm implementations that are not supported by the basic distribution. (See The lbtt-translate utility for information on how to connect several publicly available LTL-to-Büchi translator implementations to lbtt.)

• Translator interface: lbtt's requirements for an LTL-to-Büchi translator.
• Format for LTL formulas: How lbtt passes LTL formulas to the translators.
• Format for automata: How lbtt expects the translators to present their output.
• The lbtt-translate utility: An interface for two LTL-to-Büchi translators.