Это команда lpsconfcheck, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
lpsconfcheck - отметить сливающиеся тау-слагаемые LPS
СИНТАКСИС
lpsconfcheck [ВАРИАНТ] ... [ИНФАЙЛ [АУТФАЙЛ]]
ОПИСАНИЕ
Проверяет, какие тау-слагаемые mCRL2 LPS в INFILE сливаются, помечает их переименованием.
их в ctau и записать результат в OUTFILE. Если INFILE отсутствует, используется стандартный ввод. Если
OUTFILE нет, используется стандартный вывод.
ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ
ВАРИАНТ может быть любым из следующих:
-a, --отметить все
проверьте слияние тау-слагаемых относительно всех остальных слагаемых, а не
переходя к следующему тау-слагаемому, как только встречается слагаемое, которое
не сливается с текущим тау-слагаемым
-c, --противопример
отображать оценку, для которой условие слияния не выполняется, в случае, если
встретившееся условие не является ни противоречием, ни тавтологией
-g, --generate-инварианты
попытаться доказать, что приведенное условие слияния является инвариантом LPS, в
случай, когда условие слияния не является тавтологией
-o, --индукция
применять индукцию к спискам
-iИНВФАЙЛ, --инвариантный=ИНВФАЙЛ
используйте логическую формулу (выражение данных mCRL2 вида Bool) в INVFILE как
инвариантный
-n, - не проверять
не проверять, выполняется ли инвариант перед проверкой слияния
-m, - без маркировки
не отмечайте сливающиеся тау-слагаемые; поскольку в LPS нет изменений,
в OUTFILE ничего не пишется
-pПРЕФИКС, --print-точка=ПРЕФИКС
сохранить файл .dot полученного BDD на случай, если два слагаемых не могут быть доказаны
сливной; PREFIX будет использоваться как префикс выходных файлов
-QNUM, --qlimit=NUM
ограничить перечисление кванторов до ЧИСЛА переменных. (По умолчанию ЧИСЛО = 1000, ЧИСЛО = 0 для
без ограничений).
-rИМЯ, - пивовар=ИМЯ
использовать стратегию перезаписи NAME: 'jitty' jitty rewriting (по умолчанию) 'jittyc' скомпилирован
jitty rewriting 'jittyp' jitty rewriting с помощью прувера
-zРЕШЕНИЕ, --smt-решатель=РЕШЕНИЕ
используйте SOLVER для удаления несогласованных путей из BDD, используемых внутри (по умолчанию,
исключение пути не применяется): 'cvc' решатель SMT CVC3
-sNUM, --приказ=NUM
исключить или упростить слагаемое только с номером NUM
-tОГРАНИЧЕНИЯ, --лимит времени=ОГРАНИЧЕНИЯ
потратить не более LIMIT секунд на доказательство одной формулы
--сроки[=ФАЙЛОВ]
добавить измерения времени в ФАЙЛ. Измерения записываются со стандартной ошибкой, если
ФАЙЛ не предоставлен
Стандартные варианты:
-q, --тихий
не отображать предупреждающие сообщения
-v, --подробный
отображать короткие промежуточные сообщения
-d, --отлаживать
отображать подробные промежуточные сообщения
--лог-уровень=УРОВЕНЬ
отображать промежуточные сообщения до уровня включительно
-h, --Помогите
отображать справочную информацию
--версия
отображать информацию о версии
Используйте lpsconfcheck онлайн с помощью сервисов onworks.net
