maria - онлайн в хмарі

ПРОГРАМА:

ІМ'Я

maria - модульний аналізатор доступності для високорівневих мереж Петрі

СИНТАКСИС

Марія [опції] файли...

ОПИС

На цій сторінці посібника коротко описано Марія команда. Більш повна документація є
доступний у форматі GNU Info; Дивись нижче.

Марія це програма, яка аналізує моделі паралельних систем, описані в її вхідних даних
мова, яка базується на мережах алгебраїчної системи. Формалізм представив Еккарт
Кіндлер і Хаген Фольцер на ICATPN'98, Гнучкість in Алгебраїчний мережі.
Алгебраїчні системні мережі – це структура, яка не визначає жодних типів даних чи алгебраїки
операції. Система типів даних і операції в Maria розроблені на високому рівні
мови програмування та специфікації на увазі. Незважаючи на це, кожна модель Maria має
кінцеве розгортання.
Щоб забезпечити взаємодію з інструментами мережі Петрі низького рівня, Марія перекладає ідентифікатори в
розгорнуті сітки до рядків буквено-цифрових символів і символів підкреслення. Фільтр
foldname.pl можна використовувати або адаптувати для покращення читабельності ідентифікаторів.

ВАРІАНТИ

Марія дотримується звичайного синтаксису командного рядка GNU з довгими параметрами, які починаються з двох
тире (`-'). Нижче наведено короткий опис варіантів. Повний опис див
інформаційні файли.

-a обмежувати, --array-limit=обмежувати
Обмежте розмір типів індексів масиву до обмежувати можливі значення. Обмеження 0
вимикає перевірки.

-b модель, --ширина-перший-пошук=модель
Створіть графік досяжності модель за допомогою пошуку вшир.

-C каталог, --compile=каталог
Згенеруйте код C у каталог для оцінки виразів і для низького рівня
підпрограми алгоритму аналізу екземпляра переходу. Коли використовується ця опція,
помилки оцінки повідомляються дещо іншим чином. Перекладач
відображає оцінку та вираз, які викликали першу помилку в стані; в
скомпільований код відображає кількість помилок. З міркувань продуктивності,
згенерований код не перевіряє помилки переповнення під час додавання елементів до мультинаборів.

-c, --без компіляції
Протилежне -C. Оцініть усі вирази у вбудованому інтерпретаторі. Це
поведінка за замовчуванням.

-D символ, --визначити=символ
Визначте символ препроцесора символ.

-d модель, --depth-first-search=модель
Створіть графік досяжності модель за допомогою пошуку в глибину.

-E інтервал, --края=інтервал
Під час створення графіка доступності повідомляйте розмір графіка після кожного
інтервал створені ребра.

-e рядок, --виконати=рядок
Виконати рядок.

-g графічний файл, --граф=графічний файл
Завантажте раніше згенерований графік доступності з графічний файл.rgh.

-H h[,f[,t]], --хеші=h[,f[,t]]
Налаштуйте параметри для ймовірнісної перевірки (-P). Виділити t універсальний
хеш-функції f елементів і відповідних хеш-таблиць h біти кожен. Обидва h
та f буде округлено до наступних відповідних значень.

-?, -h, --допомога
Роздрукуйте підсумок параметрів командного рядка для Марії та вийдіть.

-I каталог, --включати=каталог
Додавати каталог до списку каталогів, які шукали для включення файлів.

-i стовпців, --ширина=стовпців
Встановіть для правого поля виведення значення стовпців. За замовчуванням – 80.

-j процеси, --робота=процеси
При перевірці властивостей безпеки (опції -L, -M та -P), використовувати цей багато працівників
процесів для прискорення аналізу на багатопроцесорному комп’ютері. Дивись також -k та
-Z.

-k порт[/господар], --connect=порт[/господар]
Поширте перевірку моделі безпеки (опції -L, -M та -P) у мережі TCP/IP. Для
лише сервер порт задається як 16-розрядне ціле число без знака, зазвичай між
1024 і 65535. Для робочих процесів, порт/господар вказує порт і
адреса сервера. Дивись також -j.

-L модель, --без втрат=модель
Навантаження модель і підготуватися до його аналізу шляхом побудови набору досяжних станів
у дискових файлах. Дивись також -M, -P, -j та -k.

-m модель, --модель=модель
Навантаження модель і очистити його графік досяжності.

-M модель, --md5-compacted=модель
Навантаження модель і підготуйтеся до його аналізу, побудувавши надмірну апроксимацію
набір доступних станів в основній пам'яті. Дивись також -P, -L, -j та -k.

-N cregexp, --ім'я=cregexp
Вкажіть імена, дозволені в контексті c як розширений регулярний вираз RegExp.
Контекст ідентифікується за першим символом рядка параметрів; в
Наступні символи становлять регулярний вираз, який мають дозволені імена
збігатися.

-n cregexp, --no-name=cregexp
Вкажіть імена, які не допускаються в контексті c як розширений регулярний вираз
RegExp.
Якщо обоє -N і і -n вказуються для контексту c, тоді береться відповідність
пріоритет. Наприклад, вимагати, щоб усі визначені користувачем імена типів були
припинено з _t, вкажіть -нт -Nt'_t$'. В останньому параметрі є лапки
необхідно видалити особливе значення з $ в оболонці командного рядка ви перебуваєте
ймовірно, використовував для виклику Марії.

-P модель, --імовірнісний=модель
Навантаження модель і підготуватися до його аналізу шляхом побудови набору досяжних станів
в основній пам’яті за допомогою техніки під назвою стан бітів хешування.

-p команда, --property-translator=команда
Вкажіть команду для перекладу автоматів властивостей. Команда повинна
прочитати формулу зі стандартного введення і записати відповідний автомат
опис до стандартного виходу. Перекладач фунти сумісна з цим
варіант.

-q обмежувати, --quantification-limit=обмежувати
Запобігти кількісному визначенню (суму кількох наборів) типів, які мають більше ніж обмежувати це можливо
цінності. Обмеження 0 вимикає перевірки.

-U символ, --undefine=символ
Скасувати визначення символу препроцесора символ.

-u [a][f[вихідний файл]], --розгорнути=[a][f[вихідний файл]]
Розгорніть сітку за алгоритмом a і запишіть у форматі f до вихідний файл. Якщо вихідний файл
не вказано, скидайте розгорнуту сітку до стандартного виходу. Можливі формати
він має m (Марія (розбірлива), за замовчуванням), l (LoLA), p (PEP), і r (PROD). Там
є два алгоритми: традиційний (за замовчуванням) і зменшений шляхом побудови a покривається
маркування (M).

-V, -- версія
Надрукуйте номер версії Марії та вийдіть.

-v, -багатослівний
Відображати детальну інформацію про різні етапи аналізу.

-W, --попередження
Увімкнути попередження про підозрілі конструкції мережі. Це поведінка за замовчуванням.

-w, --без попереджень
Протилежне -W. Вимкніть усі попередження.

-x числобаза, --radix=числобаза
Вкажіть числову базу для виведення діагностики. Дозволені значення для числобаза він має
жовтень, вісімковий, 8, гекса, шістнадцятковий, 16, грудня, десятковий знак та 10. За замовчуванням використовується
десяткові числа.

-Y, --compress-hidden
Зменшіть набір доступних станів, не зберігаючи наступні стани
екземпляри переходів, для яких a приховувати умова виконується. Приховані наступники є
зберігається в окремому наборі станів. Цей параметр може заощадити пам’ять (-L or -m) або зменшити
ймовірність того, що стани опущені (-M or -P), і це може покращити
ефективність паралельного аналізу (-j or -k), але він також може значно збільшитися
потреба в часі процесора. Опція також працює з моделлю живості
перевірка, але немає гарантії, що істинність значень властивостей живості
залишаються незмінними. Цей варіант можна поєднувати з -Z.

-у, --no-compress-hidden
Протилежне -Y. Це поведінка за замовчуванням.

-Z, --компресійні шляхи
Зменшіть набір доступних станів, не зберігаючи проміжні стани, які мають at
найбільше один наступник. Цей параметр може заощадити пам’ять (-L or -m) або зменшити
ймовірність того, що стани опущені (-M or -P), і це може підвищити ефективність
паралельного аналізу (-j or -k), але це також може значно збільшити
потреба в часі процесора. Опція також працює з перевіркою моделі живості,
але немає гарантії, що істинні значення властивостей живості залишаться
без змін. Цей варіант можна поєднувати з -Y.

-z, --no-compress-paths
Протилежне -Z. Це поведінка за замовчуванням.

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