Il s'agit de la commande lbt2dot qui peut être exécutée dans le fournisseur d'hébergement gratuit OnWorks en utilisant l'un de nos multiples postes de travail en ligne gratuits tels que Ubuntu Online, Fedora Online, l'émulateur en ligne Windows ou l'émulateur en ligne MAC OS
PROGRAMME:
Nom
lbt - Traducteur LTL vers Büchi
SYNOPSIS
lbt < formule.txt > automate.txt
lbt2dot < automate.txt > automate.dot
DESCRIPTION
Cette page de manuel documente brièvement les lbt et lbt2dot commandes. Cette page de manuel a été
écrit pour la distribution Debian GNU/Linux car le programme original n'a pas de
page de manuel. Au lieu de cela, il a une documentation au format HTML ; voir ci-dessous.
lbt est un filtre qui traduit une formule de logique temporelle linéaire (LTL) en une formule correspondante
automate de Büchi généralisé. La traduction est basée sur l'algorithme de Gerth, Peled
et Vardi présenté au PSTV'95, Simple à la volée automatique vérification of linéaire
temporel logique. Pratiquement aucune optimisation n'est implémentée, et l'automate généré est
souvent plus grand que nécessaire. Mais d'un autre côté, cela devrait toujours être correct.
Le filtre lbt2dot peut être utilisé pour traduire les automates de Büchi du lbt format de sortie vers
Format GraphViz pour la visualisation.
EXEMPLE
echo Gp0 | lbt | lbt2dot | toqué -
Utilisez lbt2dot en ligne en utilisant les services onworks.net
