Це команда ltsconvert, яку можна запустити в постачальнику безкоштовного хостингу OnWorks за допомогою однієї з наших численних безкоштовних робочих станцій, таких як Ubuntu Online, Fedora Online, онлайн-емулятор Windows або онлайн-емулятор MAC OS.
ПРОГРАМА:
ІМ'Я
ltsconvert - конвертувати та за бажанням мінімізувати LTS
СИНТАКСИС
ltsconvert [ВАРІАНТ]... [INFILE [OUTFILE]]
ОПИС
Перетворіть позначену систему переходу (LTS) з INFILE на OUTFILE у запитаному
формат після застосування вибраного методу мінімізації (за замовчуванням немає). Якщо OUTFILE є
не надається, використовується стандартний вихід. Якщо INFILE не надано, використовується stdin.
Формат виведення визначається розширенням OUTFILE, тоді як формат введення – це
визначається змістом INFILE. Для примусового введення можна використовувати параметри --in та --out
і вихідні формати. Підтримувані формати:
"aut" для формату Aldebaran (CADP),
"точка" для формату GraphViz (більше не підтримується як формат введення),
'fsm' для формату кінцевого автомата, або
'lts' для формату mCRL2 LTS (за замовчуванням)
ВАРІАНТИ
ВАРІАНТ може бути будь-яке з наступного:
-D, --визначити
визначити LTS
-eІМ'Я, --еквівалентність=ІМ'Я
генерувати еквівалентний LTS, зберігаючи еквівалентність NAME: 'none' identity
еквівалентність (за замовчуванням) 'bisim' сильна двоподібність 'bisim-sig' сильна бісимічність
використання уточнення сигнатури 'branching-bisim' branching bisimilarity 'branching-
bisim-sig' розгалуження біподібності з використанням уточнення сигнатури 'dpbranching-bisim'
дивергенція, що зберігає розгалуження, біподібність 'dpbranching-bisim-sig' розбіжність
збереження двоподібності розгалуження з використанням уточнення сигнатури 'weak-bisim' слабкий
біподібність 'weak-bisim-sig' слабка двоподібність з використанням уточнення підпису 'dpweak-
бісимська дивергенція із збереженням слабкої бісхожості 'dpweak-bisim-sig' дивергенція
збереження слабкої біподібності за допомогою сильного моделювання 'sim' уточнення сигнатур
еквівалентність 'trace' сильна еквівалентність сліду 'weak-trace' слабка еквівалентність сліду
«тау-зірка» тау-зірка зменшення
-iФОРМАТ, --в=ФОРМАТ
використовуйте FORMAT як формат введення
-lФото, --lps=Фото
використовувати FILE як LPS, з якого було згенеровано вхідний LTS; це може знадобитися
зберігати правильні назви параметрів станів при збереженні у форматі fsm і до
конвертувати не-mCRL2 LTS в mCRL2 LTS
--недосяжність
не виконуйте перевірку доступності на вхідному LTS
-n, --не-держави
пропускати інформацію про стан під час збереження у форматі точки
-oФОРМАТ, -- вихід=ФОРМАТ
використовуйте FORMAT як вихідний формат
--тау=ІМЕНИ
вважати дії з іменем у списку ACTNAMES, розділених комами, внутрішніми
(tau) дії на додаток до тих, які визначені як такі за допомогою введення
-- терміни[=Фото]
додати вимірювання часу до FILE. Вимірювання записуються до стандартної похибки, якщо
FILE не надається
Стандартні опції:
-q, --спокійно
не відображати попереджувальні повідомлення
-v, -багатослівний
відображати короткі проміжні повідомлення
-d, --відлагоджувати
відображати детальні проміжні повідомлення
-- рівень журналу=РІВЕНЬ
відображати проміжні повідомлення до рівня включно
-h, --допомога
відобразити довідкову інформацію
-- версія
відобразити інформацію про версію
Використовуйте ltsconvert онлайн за допомогою служб onworks.net
