Это команда ltsconvert, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
ltsconvert - конвертировать и, при необходимости, минимизировать LTS
СИНТАКСИС
лтсконвертировать [ВАРИАНТ] ... [ИНФАЙЛ [АУТФАЙЛ]]
ОПИСАНИЕ
Преобразуйте помеченную систему перехода (LTS) из INFILE в OUTFILE в запрошенном
формат после применения выбранного метода минимизации (по умолчанию отсутствует). Если OUTFILE
не поставляется, используется стандартный вывод. Если INFILE не указан, используется стандартный ввод.
Формат вывода определяется расширением OUTFILE, тогда как формат ввода
определяется содержанием INFILE. Параметры --in и --out могут использоваться для принудительного ввода
и форматы вывода. Поддерживаемые форматы:
'aut' для формата Альдебарана (CADP),
'точка' для формата GraphViz (больше не поддерживается в качестве входного формата),
'fsm' для формата конечного автомата, или
lts для формата mCRL2 LTS (по умолчанию)
ДОПОЛНИТЕЛЬНЫЕ УСЛУГИ, НЕ ВКЛЮЧЕННЫЕ В ПАКЕТ
ВАРИАНТ может быть любым из следующих:
-D, - определить
детерминировать LTS
-eИМЯ, - эквивалентность=ИМЯ
генерировать эквивалентный LTS, сохраняя эквивалентность NAME: 'none' идентичность
эквивалентность (по умолчанию) 'bisim' сильное двойное сходство 'bisim-sig' сильное двойное сходство
с использованием уточнения сигнатуры 'ветвление-бисим' ветвление двойное сходство 'ветвление-
bisim-sig 'ветвление двойного сходства с использованием уточнения сигнатуры' dpbranching-bisim '
дивергенция с сохранением ветвления бисхожесть дивергенция dpbranching-bisim-sig
сохранение двойного сходства ветвления с помощью уточнения сигнатуры 'weak-bisim' weak
двойное сходство 'weak-bisim-sig' слабое двойное сходство с использованием уточнения сигнатуры 'dpweak-
bisim 'дивергенция, сохраняющая слабое бисхожесть' дивергенция dpweak-bisim-sig '
сохранение слабого двойного сходства с использованием уточнения сигнатуры 'sim' сильное моделирование
эквивалентность 'след' эквивалентность сильного следа 'слабая трасса' эквивалентность слабого следа
'tau-star' сокращение tau star
-iФОРМАТ, --в=ФОРМАТ
используйте FORMAT в качестве формата ввода
-lФАЙЛОВ, --lps=ФАЙЛОВ
используйте ФАЙЛ в качестве LPS, из которого был сгенерирован входной LTS; это может понадобиться для
сохранять правильные имена параметров состояний при сохранении в формате fsm и в
конвертировать не-mCRL2 LTS в mCRL2 LTS
- нет досягаемости
не выполнять проверку достижимости на входе LTS
-n, --государственный
исключить информацию о состоянии при сохранении в формате точки
-oФОРМАТ, --из=ФОРМАТ
используйте FORMAT в качестве выходного формата
--тау=ACTNAMES
рассматривать действия с именем в списке, разделенном запятыми, ACTNAMES, как внутренние
(тау) действия в дополнение к тем, которые определены как таковые входом
--сроки[=ФАЙЛОВ]
добавить измерения времени в ФАЙЛ. Измерения записываются со стандартной ошибкой, если
ФАЙЛ не предоставлен
Стандартные варианты:
-q, --тихий
не отображать предупреждающие сообщения
-v, --подробный
отображать короткие промежуточные сообщения
-d, --отлаживать
отображать подробные промежуточные сообщения
--лог-уровень=УРОВЕНЬ
отображать промежуточные сообщения до уровня включительно
-h, --Помогите
отображать справочную информацию
--версия
отображать информацию о версии
Используйте ltsconvert онлайн с помощью сервисов onworks.net
