This is the command lbt2dot that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator
PROGRAM:
NAME
lbt - LTL to Büchi Translator
SYNOPSIS
lbt < formula.txt > automaton.txt
lbt2dot < automaton.txt > automaton.dot
DESCRIPTION
This manual page documents briefly the lbt and 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.
lbt is a filter that translates a linear temporal logic (LTL) formula to a corresponding
generalized Büchi automaton. The translation is based on the algorithm by Gerth, Peled
and Vardi presented at PSTV'95, 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.
The filter lbt2dot can be used to translate Büchi automata from the lbt output format to
GraphViz format for visualization.
EXAMPLE
echo G p0 | lbt | lbt2dot | dotty -
Use lbt2dot online using onworks.net services
