Este es el comando lbt2dot que se puede ejecutar en el proveedor de alojamiento gratuito de OnWorks utilizando una de nuestras múltiples estaciones de trabajo en línea gratuitas, como Ubuntu Online, Fedora Online, emulador en línea de Windows o emulador en línea de MAC OS.
PROGRAMA:
NOMBRE
lbt - Traductor de LTL a Büchi
SINOPSIS
LBT < fórmula.txt > autómata.txt
lbt2punto < autómata.txt > autómata.dot
DESCRIPCIÓN
Esta página de manual documenta brevemente la LBT y lbt2punto comandos. Esta página de manual fue
escrito para la distribución Debian GNU / Linux porque el programa original no tiene una
página de manual. En cambio, tiene documentación en formato HTML; vea abajo.
LBT es un filtro que traduce una fórmula de lógica temporal lineal (LTL) a un correspondiente
autómata Büchi generalizado. La traducción se basa en el algoritmo de Gerth, Peled
y Vardi presentado en PSTV'95, Fácil sobre la marcha y automática verificación of lineal
temporal lógica. Casi no se implementan optimizaciones, y el autómata generado es
a menudo más grande de lo necesario. Pero, por otro lado, siempre debe ser correcto.
El filtro lbt2punto se puede utilizar para traducir autómatas Büchi del LBT formato de salida a
Formato GraphViz para visualización.
EJEMPLO
echo Gp0 | LBT | lbt2punto | punteado -
Use lbt2dot en línea usando los servicios de onworks.net
