Next: Format for automata, Previous: Translator interface, Up: Interfacing with lbtt

`lbtt` passes each LTL formula to each LTL-to-Büchi translator
in a file containing an LTL formula in a prefix notation followed by a
single newline. The precise grammar for the LTL formulas (in a BNF-style
notation) is as follows:

formula::= `t' // ``true'' | `f' // ``false'' | `p'[0---9]+ // atomic proposition with // a nonnegative integer // identifier | `!'spformula// negation | `X'spformula// ``next time'' | `F'spformula// ``finally'' | `G'spformula// ``globally'' | `&'spformulaspformula// conjunction | `|'spformulaspformula// disjunction | `i'spformulaspformula// implication | `e'spformulaspformula// equivalence | `^'spformulaspformula// exclusive or | `U'spformulaspformula// ``(strong) until'' | `V'spformulaspformula// ``(weak) release'' | `W'spformulaspformula// ``weak until'' | `M'spformulaspformula// ``strong release'' | `B'spformulaspformula// ``before''

(The quoted characters denote the characters themselves; `sp` denotes
any nonempty string of white space. Lines containing a // are comments and
are not part of the grammar. All atomic propositions in the formula have a
nonnegative numeric identifier.)

For example, the LTL formula
(in `lbtt`'s infix syntax)

(p0 U p1) -> (<> [] (! p2 <-> p3))

would be expressed in the form

i U p0 p1 F G e ! p2 p3

in an output file.

If your translator does not support all of the above operators, edit
the configuration file (see Configuration file) or use the command
line options (see Command line options) to prevent
`lbtt` from generating random LTL formulas with these operators.