Це команда lpssuminst, яку можна запустити в постачальнику безкоштовного хостингу OnWorks за допомогою однієї з наших численних безкоштовних робочих станцій, таких як Ubuntu Online, Fedora Online, онлайн емулятор Windows або онлайн емулятор MAC OS
ПРОГРАМА:
ІМ'Я
lpssuminst - створити екземпляр підсумовуваних змінних LPS
СИНТАКСИС
lpssuminst [ВАРІАНТ]... [INFILE [OUTFILE]]
ОПИС
Створіть екземпляр змінних підсумовування лінійної специфікації процесу (LPS) у INFILE
і запишіть результат у OUTFILE. Якщо INFILE відсутній, використовується stdin. Якщо OUTFILE є
немає, використовується стандартний вихід.
ВАРІАНТИ
ВАРІАНТ може бути будь-яке з наступного:
-f, --кінцевий
створювати лише екземпляри змінних, сорти яких є кінцевими
-QNUM, --qlimit=NUM
обмежити перерахування кванторів до NUM змінних. (За замовчуванням NUM=1000, NUM=0 для
необмежений).
-rІМ'Я, --переписувач=ІМ'Я
використовувати стратегію перезапису NAME: 'jitty' jitty rewriting (за замовчуванням) 'jittyc' скомпільовано
jitty переписування 'jittyp' jitty переписування з доказом
-s[ІМ'Я], -- сорти[=ІМ'Я]
виберіть сортування, які потрібно розгорнути (список, розділений комами)
Приклади: Bool; Bool, List(Nat)
-t, --тау
створювати лише екземпляри змінних у доданках tau
-- терміни[=Фото]
додати вимірювання часу до FILE. Вимірювання записуються до стандартної похибки, якщо
FILE не надається
Стандартні опції:
-q, --спокійно
не відображати попереджувальні повідомлення
-v, -багатослівний
відображати короткі проміжні повідомлення
-d, --відлагоджувати
відображати детальні проміжні повідомлення
-- рівень журналу=РІВЕНЬ
відображати проміжні повідомлення до рівня включно
-h, --допомога
відобразити довідкову інформацію
-- версія
відобразити інформацію про версію
Використовуйте lpssuminst онлайн за допомогою служб onworks.net
