Это команда lbt, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
lbt - переводчик с LTL на Büchi
СИНТАКСИС
фунт < формула.txt > автомат.txt
lbt2dot < автомат.txt > автомат.точка
ОПИСАНИЕ
Эта страница руководства кратко документирует фунт и lbt2dot команды. Эта страница руководства была
написана для дистрибутива Debian GNU / Linux, потому что исходная программа не имеет
страница руководства. Вместо этого у него есть документация в формате HTML; см. ниже.
фунт представляет собой фильтр, который переводит формулу линейной временной логики (LTL) в соответствующий
обобщенный автомат Бюхи. Перевод основан на алгоритме Герта, Пеледа.
и Варди представлены на PSTV'95, просто на лету автоматически проверка of линейный
временной логика. Практически не реализованы какие-либо оптимизации, а сгенерированный автомат
часто больше, чем необходимо. Но с другой стороны, он всегда должен быть правильным.
Фильтр lbt2dot может использоваться для перевода автоматов Бюхи из фунт выходной формат в
Формат GraphViz для визуализации.
ПРИМЕР
эхо г р0 | фунт | lbt2dot | рехнувшийся -
Используйте lbt онлайн с помощью сервисов onworks.net
