Next: , Previous: Analyzing test results, Up: Top

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:

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.)