lps2lts - онлайн у хмарі

ПРОГРАМА:

ІМ'Я

lps2lts - генерувати LTS з LPS

СИНТАКСИС

lps2lts [ВАРІАНТ]... [INFILE [OUTFILE]]

ОПИС

Згенеруйте LTS з LPS в INFILE і збережіть результат у OUTFILE. Якщо INFILE ні
надається, використовується stdin. Якщо OUTFILE не надано, LTS не зберігається.

Якщо використовується перезаписувач 'jittyc', тоді змінна середовища MCRL2_COMPILEREWRITER
(значення за замовчуванням: 'mcrl2compilerewriter') визначає сценарій, який компілює перезаписувач,
а MCRL2_COMPILEDIR (значення за замовчуванням: '.') визначає, де зберігаються тимчасові файли.

Зауважте, що lps2lts може надавати кілька переходів з однаковою міткою між будь-якою парою
державах. Якщо це не бажано, такі переходи можна прибрати, застосувавши сильний
бісимуляція редукції, використовуючи, наприклад, інструмент ltsconvert.

Формат OUTFILE визначається його розширенням (якщо воно не вказано в файлі
варіант). Підтримувані формати:

"aut" для формату Aldebaran (CADP),
"точка" для формату GraphViz (більше не підтримується як формат введення),
'fsm' для формату кінцевого автомата, або
'lts' для формату mCRL2 LTS Якщо використовується перезаписувач jittyc, то
Змінна середовища MCRL2_COMPILEREWRITER (значення за замовчуванням: mcrl2compilerewriter)
визначає сценарій, який компілює перезаписувач, і MCRL2_COMPILEDIR (значення за замовчуванням:
'.') визначає, де зберігаються тимчасові файли. Зауважте, що lps2lts може надавати декілька
переходи з однаковою міткою між будь-якою парою станів. Якщо цього не хочеться, то таке
Переходи можна видалити, застосувавши сильну бісимуляційну редукцію за допомогою, наприклад
інструмент ltsconvert.

ВАРІАНТИ

ВАРІАНТ може бути будь-яке з наступного:

-aІМЕНА, --дія=ІМЕНА
виявляти і повідомляти про дії в системі переходів, які мають імена дій від
NAMES, список, розділений комами. Це, наприклад, корисно, щоб знайти (або довести
відсутність) помилки дії. Повідомлення друкується для кожного входження одного з
ці назви дій. З прапорцем -t генеруються сліди до цих дій

-b[NUM], --біт-хеш[=NUM]
використовуйте бітове хешування для збереження станів і зберігайте щонайбільше NUM станів. Це означає що
замість ведення повного запису всіх відвіданих станів, бітовий масив
Використовується, що вказує, чи бачив хеш стану раніше.
Хоча це означає, що ця опція може призвести до того, що штати будуть помилково прийнятий за інші
(оскільки вони зіставлені з одним хешем), може бути корисно досліджувати дуже великі
LTS, які в іншому випадку неможливо дослідити. Значення за замовчуванням для NUM приблизно
2*10^8 (це відповідає приблизно 25 МБ пам'яті)

-кешоване
використовувати методи кешування перерахувань для прискорення генерації простору станів.

-c[ІМ'Я], -- злиття[=ІМ'Я]
застосувати пріоритетність переходів з міткою дії NAME. (якщо немає NAME
наданий (тобто '-c') пріоритет надається дії 'ctau'. Віддавати пріоритет
для tau використовуйте прапор -ctau. Зауважте, що якщо лінійний процес не є тау-конфлюентним,
згенерований простір станів обов'язково розгалужується, подібно до простору станів
lps. Алгоритм генерації, який використовується, не вимагає лінійного процесу
бути тау конвергентним.

-D, --тупик
виявити тупикові блокування (тобто для кожного блокування друкується повідомлення)

-F, -- розбіжність
виявляти розбіжності (тобто для кожного стану з розбіжністю (=тау-петля) є повідомлення
друковані). Алгоритм виявлення розбіжностей є лінійним для кожного стану, отже
дослідження простору станів стає квадратичним з увімкненою цією опцією, викликаючи стан
Якщо ввімкнути цю опцію, дослідження космосу сповільниться.

-yBOOL, -- манекен=BOOL
замінити вільні змінні в LPS фіктивними значеннями на основі значення BOOL:
"так" (за замовчуванням) або "ні"

-- трасування помилок
якщо під час дослідження виникає помилка, збережіть трасування до стану, який не міг бути
розвіданий

--init-size=NUM
встановити початковий розмір внутрішньо використовуваних хеш-таблиць (за замовчуванням 10000)

-lNUM, --макс=NUM
досліджувати щонайбільше NUM штатів

-mІМЕНА, --багатодія=ІМЕНА
виявляти багато дій у системі переходів і повідомляти про них із NAMES, кома-
відокремлений список. Працює як -a, за винятком того, що багато дій точно відповідають,
включаючи параметри даних.

-- немає інформації
не додавати інформацію про стан до OUTFILEБез цієї опції lps2lts додає стан
вектор до LTS. Ця опція спричиняє відкидання цієї інформації та вказівки
позначаються лише порядковим номером. Явна інформація про стан корисна для
наприклад, для цілей візуалізації, але може призвести до зростання OUTFILE
значно. Зауважте, що ця опція неявна під час запису у форматі AUT.

-oФОРМАТ, -- вихід=ФОРМАТ
збережіть результат у зазначеному ФОРМАТІ

-- чорнослив
використовуйте скорочення сум для прискорення генерації простору станів.

-QNUM, --qlimit=NUM
обмежити перерахування кванторів до NUM змінних. (За замовчуванням NUM=1000, NUM=0 для
необмежений).

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

-sІМ'Я, --стратегія=ІМ'Я
досліджуйте простір станів за допомогою стратегії NAME: 'b', 'широта' пошук у ширину
(за замовчуванням) 'd', 'depth' пошук у глибину 'p', 'prioritized' пріоритет один
дії над своїм першим аргументом є типу Nat, де лише ті дії з
вибирається найменше значення для цього параметра. Наприклад, якщо є дії a(3) і
b(4) a(3) залишається і b(4) пропущено. Дії без першого параметра сортування
Завжди вибираються Nat і множення з більш ніж однією дією (опція
експериментальний) 'q', 'приоритезований' визначає пріоритети дій за першим аргументом, який є of
відсортуйте Nat (див. параметр --prioritized) і випадковим чином виберіть один із них, щоб отримати a
пріоритетне випадкове моделювання (опція експериментальна) 'r', 'випадковий' випадковий
моделювання. З усіх наступних станів один вибирається випадковим чином, незалежно від того, чи є
цей стан вже спостерігався. Отже, лише випадкове моделювання
завершується, коли зустрічається стан тупика.

-- придушити
у докладному режимі не друкуйте повідомлення про прогрес із зазначенням кількості відвідувань
стани та переходи. Для великих просторів станів кількість повідомлень про прогрес може
бути досить жахливим. Ця функція допомагає придушити їх. Інші докладні повідомлення,
наприклад, загальна кількість досліджуваних станів, залишаються видимими.

-- терміни[=Фото]
додати вимірювання часу до FILE. Вимірювання записуються до стандартної похибки, якщо
FILE не надається

--todo-max=NUM
зберігати не більше NUM станів у списках справ; ця опція актуальна лише для широти-
перший пошук, де NUM – ​​максимальна кількість станів на рівні, а також глибина
перший пошук, де NUM – ​​максимальна глибина

-t[NUM], --слід[=NUM]
Запишіть найкоротшу трасу для кожного стану, якого досягнуто за допомогою дії NAMES from
параметр --action, це тупик, виявлений за допомогою --deadlock, або розбіжність
виявлено за допомогою --divergence до файлу. Буде записано не більше ніж NUM трас. Якщо
NUM не вказано, кількість трас є необмеженою. Для кожного сліду, яке має бути
буде створений унікальний файл із розширенням .trc (trace), що містить a
найкоротша траса від початкового стану до стану тупикової блокування. Сліди можуть бути
досить надруковано та конвертовано в інші формати за допомогою tracepp.

-u, --невикористані-дані
не видаляйте невикористані частини специфікації даних

Стандартні опції:

-q, --спокійно
не відображати попереджувальні повідомлення

-v, -багатослівний
відображати короткі проміжні повідомлення

-d, --відлагоджувати
відображати детальні проміжні повідомлення

-- рівень журналу=РІВЕНЬ
відображати проміжні повідомлення до рівня включно

-h, --допомога
відобразити довідкову інформацію

-- версія
відобразити інформацію про версію

Використовуйте lps2lts онлайн за допомогою служб onworks.net