Aceasta este comanda lbt2dot care poate fi rulată în furnizorul de găzduire gratuit OnWorks folosind una dintre multiplele noastre stații de lucru online gratuite, cum ar fi Ubuntu Online, Fedora Online, emulator online Windows sau emulator online MAC OS
PROGRAM:
NUME
lbt - LTL în Büchi Translator
REZUMAT
lbt < formula.txt > automat.txt
lbt2dot < automat.txt > automat.punct
DESCRIERE
Această pagină de manual documentează pe scurt lbt și lbt2dot comenzi. Această pagină de manual a fost
scris pentru distribuția Debian GNU/Linux deoarece programul original nu are un
pagina de manual. În schimb, are documentație în format HTML; Vezi mai jos.
lbt este un filtru care traduce o formulă de logică temporală liniară (LTL) într-o formulă corespunzătoare
automat Büchi generalizat. Traducerea se bazează pe algoritmul lui Gerth, Peled
și Vardi a prezentat la PSTV'95, simplu pe fuga automat verificare of liniar
temporal logică. Nu sunt implementate aproape deloc optimizări, iar automatul generat este
adesea mai mare decât este necesar. Dar, pe de altă parte, ar trebui să fie întotdeauna corect.
Filtrul lbt2dot poate fi folosit pentru a traduce automatele Büchi din lbt format de ieșire la
Formatul GraphViz pentru vizualizare.
EXEMPLU
ecou G p0 | lbt | lbt2dot | dotty -
Utilizați lbt2dot online folosind serviciile onworks.net