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


5.1 Command conventions

Commands are entered by typing a command name followed by any parameters for the command and then pressing <ENTER>. The command names are case-sensitive. Each parameter should be separated from the command name and other parameters with white space.

Command names can be abbreviated to the shortest prefix that identifies the command unambiguously (for example, `h' could be used in place of the `help' command).

Some of the commands expect lists of implementation or state identifiers as parameters. The lists can be specified as comma-separated numbers (for example, `8') or intervals (for example, `3-11') with no white space between the commas and the numbers or intervals that belong to the same list. For example, assuming that the state space used in the current test round has at least 23 states, the command `statespace -5,8,14-18,22-' would display information about all state space states with an identifier less than or equal to 5, together with information about state 8, states 14 to 18 (inclusive) and all states with an identifier greater than or equal to 22. The `*' symbol can be used as a shorthand for all identifiers in the available range.

lbtt also recognizes the symbolic names of implementations (defined in the configuration file) in implementation identifier lists. The names can be used in place of the numeric identifiers. Quotes or the escape character (`\') should be used to handle white space in identifiers.

Some of the commands require a formula identifier as a parameter for choosing between a positive and a negative LTL formula. The formula identifier (`+' for positive formula, `-' for negative formula) must follow the command name as the first parameter for the command. If the formula identifier is omitted, the positive formula is assumed.

The output of most commands (excluding the test control commands, see Test control commands) can be redirected or appended to a file by ending the command line with `>filename' or `>>filename', respectively.

Optionally, the output can be handed over to an external program by ending the command line with `| command', where command is the command line used for invoking the external program. For example, the output of the (lbtt's internal) command can be piped to a pager application if the entire output does not fit on the screen by itself. Using the pipe construct without specifying any internal command will simply invoke the external program.