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