lps2lts - Интернет в облаке

ПРОГРАММА:

ИМЯ

lps2lts - генерировать LTS из LPS

СИНТАКСИС

лпс2лтс [ВАРИАНТ] ... [ИНФАЙЛ [АУТФАЙЛ]]

ОПИСАНИЕ

Создайте LTS из LPS в INFILE и сохраните результат в OUTFILE. Если INFILE не
поставляется, используется стандартный ввод. Если OUTFILE не указан, LTS не сохраняется.

Если используется перезаписчик jittyc, тогда переменная среды MCRL2_COMPILEREWRITER
(значение по умолчанию: 'mcrl2compilerewriter') определяет сценарий, который компилирует программу перезаписи,
а MCRL2_COMPILEDIR (значение по умолчанию: '.') определяет, где хранятся временные файлы.

Обратите внимание, что lps2lts может доставлять несколько переходов с одной и той же меткой между любой парой
состояния. Если это нежелательно, такие переходы можно убрать, применив сильную
преобразование бисимуляции с использованием, например, инструмента ltsconvert.

Формат OUTFILE определяется его расширением (если он не указан
вариант). Поддерживаемые форматы:

'aut' для формата Альдебарана (CADP),
'точка' для формата GraphViz (больше не поддерживается в качестве входного формата),
'fsm' для формата конечного автомата, или
'lts' для формата mCRL2 LTS Если используется jittyc rewriter, то
Переменная среды MCRL2_COMPILEREWRITER (значение по умолчанию: mcrl2compilerewriter)
определяет сценарий, который компилирует перезаписывающее устройство, и MCRL2_COMPILEDIR (значение по умолчанию:
'.') определяет, где хранятся временные файлы. Обратите внимание, что lps2lts может доставлять несколько
переходы с одинаковой меткой между любой парой состояний. Если это нежелательно, такие
переходы могут быть удалены путем применения сильного редуктона бисимуляции с использованием, например,
инструмент ltsconvert.

ДОПОЛНИТЕЛЬНЫЕ УСЛУГИ, НЕ ВКЛЮЧЕННЫЕ В ПАКЕТ

ВАРИАНТ может быть любым из следующих:

-aИМЕНА, --действие=ИМЕНА
обнаруживать и сообщать о действиях в системе переходов, которые имеют имена действий из
ИМЕНА, список, разделенный запятыми. Это, например, полезно, чтобы найти (или доказать
отсутствие) ошибки действия. Сообщение печатается при каждом появлении одного из
эти названия действий. С флагом -t следы к этим действиям генерируются

-b[NUM], --бит-хеш[=NUM]
использовать битовое хеширование для хранения состояний и хранить не более NUM состояний. Это означает, что
вместо того, чтобы вести полную запись всех посещенных состояний, битовый массив
используется, чтобы указать, был ли ранее виден хэш состояния.
Хотя это означает, что эта опция может привести к тому, что состояния будут ошибочно приняты за другие.
(поскольку они сопоставлены с одним и тем же хешем), может быть полезно исследовать очень большие
LTS, которые иначе не исследовать. Значение по умолчанию для NUM приблизительно равно
2 * 10 ^ 8 (это соответствует примерно 25 МБ памяти)

--кешированный
использовать методы кэширования перечисления для ускорения генерации пространства состояний.

-c[ИМЯ], --согласованность[=ИМЯ]
применить приоритезацию переходов с меткой действия NAME. (когда NAME не
предоставленный (т.е. '-c') приоритет отдается действию 'ctau'. Отдать приоритет
для тау используйте флаг -ctau. Обратите внимание, что если линейный процесс не является тау-конфлюэнтным,
сгенерированное пространство состояний обязательно ветвится аналогично пространству состояний
lps. Используемый алгоритм генерации не требует линейного процесса.
быть тау сходящимся.

-D, - тупик
обнаружение взаимоблокировок (т.е. для каждого тупика печатается сообщение)

-F, - расхождение
обнаружение расхождений (т.е. для каждого состояния с расхождением (= тау-цикл) сообщение
напечатаны). Алгоритм обнаружения расхождений является линейным для каждого состояния, поэтому
исследование пространства состояний становится квадратичным с этой опцией, вызывая состояние
при включении этой опции исследование космоса замедлится.

-yBOOL, --дурачок=BOOL
замените свободные переменные в LPS фиктивными значениями на основе значения BOOL:
«да» (по умолчанию) или «нет»

- трассировка ошибки
если во время исследования произошла ошибка, сохраните трассировку до состояния, которое не могло быть
его начали использовать

--init-tsize=NUM
установить начальный размер внутренних хэш-таблиц (по умолчанию 10000)

-lNUM, --Максимум=NUM
изучить не более NUM состояний

-mИМЕНА, --муножество=ИМЕНА
обнаруживать и сообщать о множественных действиях в системе переходов через NAMES, запятую
разделенный список. Работает как -a, за исключением того, что мульти-действия точно совпадают,
включая параметры данных.

--нет-информации
не добавлять информацию о состоянии в OUTFILE Без этой опции lps2lts добавляет состояние
вектор в LTS. Эта опция приводит к тому, что эта информация отбрасывается и указывает
обозначаются только порядковым номером. Явная информация о состоянии полезна для
целей визуализации, например, но может привести к увеличению OUTFILE
значительно. Обратите внимание, что эта опция неявна при записи в формате AUT.

-oФОРМАТ, --из=ФОРМАТ
сохранить вывод в указанном ФОРМАТЕ

--чернослив
используйте сокращение слагаемых, чтобы ускорить создание пространства состояний.

-QNUM, --qlimit=NUM
ограничить перечисление кванторов до ЧИСЛА переменных. (По умолчанию ЧИСЛО = 1000, ЧИСЛО = 0 для
без ограничений).

-rИМЯ, - пивовар=ИМЯ
использовать стратегию перезаписи NAME: 'jitty' jitty rewriting (по умолчанию) 'jittyc' скомпилирован
jitty rewriting 'jittyp' jitty rewriting с помощью прувера

-sИМЯ, --стратегия=ИМЯ
исследовать пространство состояний с помощью стратегии NAME: 'b', 'width' поиск в ширину
(по умолчанию) 'd', 'глубина' поиск в глубину 'p', 'приоритетный' приоритет одиночный
действия по первому аргументу типа Nat, где только те действия с
выбрано наименьшее значение для этого параметра. Например, если есть действия a(3) и
b(4) a(3) остается и b(4) пропускается. Действия без первого параметра сортировки
Всегда выбираются Nat и групповые действия с более чем одним действием (опция
экспериментальный) 'q', 'rprioritized' определяют приоритет действий по первому аргументу, равному
отсортировать Nat (см. параметр --prioritized) и случайным образом выбрать один из них, чтобы получить
приоритетное случайное моделирование (вариант экспериментальный) 'r', 'random' random
моделирование. Из всех следующих состояний одно выбирается случайным образом независимо от того,
это состояние уже наблюдалось. Следовательно, только случайное моделирование
завершается при обнаружении состояния взаимоблокировки.

- подавить
в подробном режиме не выводить сообщения о ходе выполнения с указанием количества посещенных
состояния и переходы. Для больших пространств состояний количество сообщений о ходе выполнения может
быть довольно ужасным. Эта функция помогает их подавить. Другие подробные сообщения,
например, общее количество исследованных состояний остается видимым.

--сроки[=ФАЙЛОВ]
добавить измерения времени в ФАЙЛ. Измерения записываются со стандартной ошибкой, если
ФАЙЛ не предоставлен

--todo-макс=NUM
хранить не более NUM состояний в списках задач; эта опция актуальна только для
первый поиск, где ЧИСЛО - максимальное количество состояний на уровень, а для глубины
первый поиск, где NUM - максимальная глубина

-t[NUM], --след[=NUM]
Напишите кратчайший путь к каждому состоянию, которое достигается действием ИМЕНА из
опция --action, тупик, обнаруженный с помощью --deadlock, или расхождение
обнаруживается с помощью --divergence к файлу. Будет записано не более NUM трассировок. Если
ЧИСЛО не указано, количество трасс не ограничено.
записанный уникальный файл с расширением .trc (трассировка) будет создан, содержащий
кратчайшая трасса от начального состояния до состояния тупика. Следы могут быть
довольно печатается и конвертируется в другие форматы с помощью tracepp.

-u, --unused-данные
не удаляйте неиспользуемые части спецификации данных

Стандартные варианты:

-q, --тихий
не отображать предупреждающие сообщения

-v, --подробный
отображать короткие промежуточные сообщения

-d, --отлаживать
отображать подробные промежуточные сообщения

--лог-уровень=УРОВЕНЬ
отображать промежуточные сообщения до уровня включительно

-h, --Помогите
отображать справочную информацию

--версия
отображать информацию о версии

Используйте lps2lts онлайн с помощью сервисов onworks.net