.\"                                      Hey, EMACS: -*- nroff -*-
.\" First parameter, NAME, should be all caps
.\" Second parameter, SECTION, should be 1-8, maybe w/ subsection
.\" other parameters are allowed: see man(7), man(1)
.TH LBT 1 "August 10, 2001"
.\" Please adjust this date whenever revising the manpage.
.\"
.\" Some roff macros, for reference:
.\" .nh        disable hyphenation
.\" .hy        enable hyphenation
.\" .ad l      left justify
.\" .ad b      justify to both left and right margins
.\" .nf        disable filling
.\" .fi        enable filling
.\" .br        insert line break
.\" .sp <n>    insert n+1 empty lines
.\" for manpage-specific macros, see man(7)
.SH NAME
lbt \- LTL to B\(:uchi Translator
.SH SYNOPSIS
.B lbt
.RI "< " formula.txt " > " automaton.txt
.br
.B lbt2dot
.RI "< " automaton.txt " > " automaton.dot
.SH DESCRIPTION
This manual page documents briefly the
.B lbt
and
.B lbt2dot
commands.
This manual page was written for the Debian GNU/Linux distribution
because the original program does not have a manual page.
Instead, it has documentation in HTML format; see below.
.PP
.\" TeX users may be more comfortable with the \fB<whatever>\fP and
.\" \fI<whatever>\fP escape sequences to invode bold face and italics, 
.\" respectively.
\fBlbt\fP is a filter that translates a linear temporal logic (LTL)
formula to a corresponding generalized B\(:uchi automaton.  The
translation is based on the algorithm by Gerth, Peled and Vardi
presented at PSTV'95,
.IR "Simple on-the-fly automatic verification of linear temporal logic".
Hardly any optimizations are implemented, and the generated automaton
is often bigger than necessary.  But on the other hand, it should always
be correct.
.br
The filter \fBlbt2dot\fP can be used to translate Büchi automata from the
\fBlbt\fP output format to GraphViz format for visualization.
.SH EXAMPLE
\fBecho\fP G p0 | \fBlbt\fP | \fBlbt2dot\fP | \fBdotty\fP -
.SH SEE ALSO
.BR dotty (1).
.SH FILES
.TP
.I /usr/share/doc/lbt/html/index.html
The real documentation for LBT.
.SH AUTHOR
This manual page was written by Marko M\(:akel\(:a <msmakela@tcs.hut.fi>,
for the Debian GNU/Linux system (but may be used by others).
The \fBlbt\fP program was written by
.B Mauno R\(:onkk\(:o
and
.B Heikki Tauriainen,
and it was optimized by
.B Marko M\(:akel\(:a,
who also wrote the \fBlbt2dot\fP filter.
Please see the copyright file in
.I /usr/share/doc/lbt
for details.