Это команда ltscompare, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
ltscompare - сравнить два LTS
СИНТАКСИС
сравнить [ВАРИАНТ] ... [ИНФАЙЛ1] ИНФАЙЛ2
ОПИСАНИЕ
Определите, являются ли помеченные переходные системы (LTS) в INFILE1 и INFILE2
связаны некоторой эквивалентностью или предварительным заказом. Если INFILE1 не указан, используется стандартный ввод.
Форматы ввода определяются содержимым INFILE1 и INFILE2. Параметры --in1
и --in2 можно использовать для принудительного ввода формата ввода INFILE1 и INFILE2 соответственно. В
поддерживаемые форматы:
'aut' для формата Альдебарана (CADP),
'точка' для формата GraphViz (больше не поддерживается в качестве входного формата),
'fsm' для формата конечного автомата, или
'lts' для формата mCRL2 LTS
ДОПОЛНИТЕЛЬНЫЕ УСЛУГИ, НЕ ВКЛЮЧЕННЫЕ В ПАКЕТ
ВАРИАНТ может быть любым из следующих:
-c, --противопример
генерировать трассировки примеров счетчика, если входные lts не эквивалентны
-eИМЯ), - эквивалентность=ИМЯ)
использовать эквивалентное ИМЯ (не допускается в сочетании с -p / - предзаказ): 'none'
идентичность эквивалентности (по умолчанию) 'bisim' сильное бисимарность 'ветвление-бисим'
ветвление двойное сходство 'dpbranching-bisim' расхождение с сохранением ветвления
двойное сходство 'weak-bisim' слабое двойное сходство 'dpweak-bisim' сохранение расхождения
слабое двойное сходство 'sim' сильная симуляционная эквивалентность 'trace' сильная трассировка
эквивалентность 'слабый след' эквивалентность слабого следа
-iФОРМАТ, --в 1=ФОРМАТ
используйте FORMAT как формат для INFILE1 (или stdin)
-jФОРМАТ, --в 2=ФОРМАТ
используйте FORMAT в качестве формата для INFILE2
-pИМЯ, --предзаказ=ИМЯ
использовать предварительный заказ ИМЯ (не допускается в сочетании с эквивалентностью -e / -): 'unknown'
неизвестный предварительный заказ (по умолчанию) 'sim' строгий предварительный заказ моделирования 'трассировка' строгий след
предварительный заказ 'weak-trace' предварительный заказ слабой трассировки
--тау=ACTNAMES
рассматривать действия с именем в списке, разделенном запятыми, ACTNAMES, как внутренние
(тау) действия в дополнение к тем, которые определены как таковые входом
--сроки[=ФАЙЛОВ]
добавить измерения времени в ФАЙЛ. Измерения записываются со стандартной ошибкой, если
ФАЙЛ не предоставлен
Стандартные варианты:
-q, --тихий
не отображать предупреждающие сообщения
-v, --подробный
отображать короткие промежуточные сообщения
-d, --отлаживать
отображать подробные промежуточные сообщения
--лог-уровень=УРОВЕНЬ
отображать промежуточные сообщения до уровня включительно
-h, --Помогите
отображать справочную информацию
--версия
отображать информацию о версии
Используйте ltscompare в Интернете с помощью сервисов onworks.net
