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

ПРОГРАММА:

ИМЯ

pbes2bool - Создайте BES из PBES и решите его.

СИНТАКСИС

pbes2bool [ВАРИАНТ] ... [ИНФАЙЛ]

ОПИСАНИЕ

Решает (P) BES из INFILE. Если INFILE отсутствует, используется стандартный ввод.

ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ

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

-c, --прилавок
напечатайте в конце дерево, помеченное экземплярами левой части
уравнения; это дерево является показателем того, как pbes2bool пришел к действительности или
недействительность ПБЭС

-eУРОВЕНЬ, --стереть=УРОВЕНЬ
используйте remove level LEVEL для удаления переменных bes 'none' не удалять сгенерированные bes
переменные. Это может привести к чрезмерному использованию памяти. (по умолчанию) 'some' удалить
сгенерированных переменных, которые не используются, за исключением случаев, когда правая часть его
уравнение верно или неверно. Необходимо пересчитать rhss переменных, если
снова встретился, что вполне нормально. 'all' удаляет все переменные bes, которые
больше не используется ни в одном уравнении. Это довольно эффективно с точки зрения памяти, но может быть
очень много времени, так как rhss удаленных переменных bes, возможно, придется
пересчитывается довольно часто.

-H, --хэш-таблицы
использовать хэш-таблицы при замене в уравнениях BES и переводить внутренние
выражения в диаграммы бинарных решений (не рекомендуется из-за производительности)

-iФОРМАТ, --в=ФОРМАТ
использовать формат ввода FORMAT: 'pbes' PBES во внутреннем формате 'pbes_text' PBES в
внутренний текстовый формат 'text' PBES в текстовом (mCRL2) формате 'bes' BES во внутреннем
формат 'bes_text' BES во внутреннем текстовом формате 'cwi' BES в формате CWI 'pgsolver'
BES в формате PGSolver

-oФОРМАТ, --выход=ФОРМАТ
использовать формат вывода FORMAT (эта опция устарела. Используйте инструмент pbes2bes
вместо).

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

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

-zПОИСК, --поиск=ПОИСК
использовать стратегию поиска ПОИСК: "в ширину". Вычислить правую часть
логические переменные в порядке очереди. Это сравнимо с
поиск в ширину. Это хорошо для создания контрпримеров. (дефолт)
'depth-first' Вычислить правую часть логических переменных, где последняя
сгенерированная переменная исследуется в первую очередь. Это соответствует принципу приоритета в глубину.
поиск. Это может существенно превзойти поиск в ширину, когда достоверность
формула определяется после большей глубины. 'b' Краткое обозначение «в ширину».
'd' Сокращение для определения глубины.

-sSTRAT, --стратегия=STRAT
использовать стратегию подстановки STRAT: '0' Вычислить все логические уравнения, которые могут быть
достигнуто из исходного состояния, без оптимизации. Это самые данные
эффективный вариант на сгенерированное уравнение. (по умолчанию) '1' Оптимизировать немедленно
заменяя правые части на уже исследованные переменные, которые истинны
или false при генерации выражения. Это такой же эффективный объем памяти, как 0. '2' В
в дополнение к 1, также замените переменные, которые являются истинными или ложными, в уже
сгенерированная правая часть. Это может означать, что некоторые переменные становятся недоступными.
(например, X0 в X0 и X1, когда X1 становится ложным, предполагая, что X0 не встречается где-либо еще.
Будет сохранено, какие переменные стали недоступными, поскольку они не имеют
для расследования. В зависимости от PBES это может уменьшить размер
генерирует BES существенно, но требует большего объема памяти. '3' дюйма
в дополнение к 2, исследуйте сгенерированные переменные, встречаются ли они в цикле,
таким образом, что они могут быть установлены на истину или ложь, в зависимости от символа фиксированной точки.
Это может существенно увеличить время, необходимое для создания уравнения.

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

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

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

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

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

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

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

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

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

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