Dies ist der Befehl lbt2dot, der im kostenlosen OnWorks-Hosting-Provider über eine unserer zahlreichen kostenlosen Online-Workstations wie Ubuntu Online, Fedora Online, Windows-Online-Emulator oder MAC OS-Online-Emulator ausgeführt werden kann
PROGRAMM:
NAME/FUNKTION
lbt - LTL zu Büchi Übersetzer
ZUSAMMENFASSUNG
LBT < formel.txt > automat.txt
lbt2dot < automat.txt > automat.dot
BESCHREIBUNG
Diese Handbuchseite dokumentiert kurz die LBT und lbt2dot Befehle. Diese Handbuchseite war
für die Debian GNU/Linux-Distribution geschrieben, da das Originalprogramm kein a
Handbuchseite. Stattdessen verfügt es über eine Dokumentation im HTML-Format; siehe unten.
LBT ist ein Filter, der eine lineare zeitliche Logik (LTL)-Formel in eine entsprechende
verallgemeinerter Büchi-Automat. Die Übersetzung basiert auf dem Algorithmus von Gerth, Peled
und Vardi auf PSTV'95 präsentiert, Einfacher on-the-fly maschinell Überprüfung of linear
temporäre Logik. Es werden kaum Optimierungen durchgeführt und der generierte Automat ist
oft größer als nötig. Aber andererseits sollte es immer richtig sein.
Der Filter lbt2dot kann verwendet werden, um Büchi-Automaten aus dem zu übersetzen LBT Ausgabeformat zu
GraphViz-Format zur Visualisierung.
BEISPIEL
Echo Gp0 | LBT | lbt2dot | Dotty -
Verwenden Sie lbt2dot online mit den onworks.net-Diensten
