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