maria - Интернет в облаке

ПРОГРАММА:

ИМЯ

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

СИНТАКСИС

maria [кредита] файлов...

ОПИСАНИЕ

Эта страница руководства кратко документирует maria команда. Более полная документация есть
доступен в формате GNU Info; см. ниже.

maria это программа, которая анализирует модели параллельных систем, описанные во входных данных
язык, основанный на сетях алгебраических систем. Формализм представил Эккарт.
Киндлер и Хаген Фельцер на ICATPN'98, Трансформируемость in алгебраическая Сети.
Algebraic System Nets - это структура, которая не определяет никаких типов данных или алгебраических
операции. Система типов данных и операции в Maria разработаны на высоком уровне.
в виду языки программирования и спецификаций. Несмотря на это, у каждой модели Марии есть
конечное развертывание.
Чтобы обеспечить взаимодействие с низкоуровневыми инструментами сетей Петри, Мария переводит идентификаторы в
развернутые сети в строки буквенно-цифровых символов и знаков подчеркивания. Фильтр
имя_фолда.pl могут использоваться или адаптироваться для улучшения читаемости идентификаторов.

ДОПОЛНИТЕЛЬНЫЕ УСЛУГИ, НЕ ВКЛЮЧЕННЫЕ В ПАКЕТ

Мария следует обычному синтаксису командной строки GNU с длинными параметрами, начинающимися с двух
тире (`-'). Сводка опций приведена ниже. Полное описание см.
Информационные файлы.

-a предел, --array-limit =предел
Ограничьте размер типов индекса массива до предел возможные значения. Предел 0
отключает проверки.

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

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

-с, --no-компилировать
Противоположно -C. Оцените все выражения во встроенном интерпретаторе. Это
поведение по умолчанию.

-D символ, --define =символ
Определите символ препроцессора символ.

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

-E интервал, --edges =интервал
При создании графика достижимости сообщайте размер графика после каждого
интервал сгенерированные ребра.

-e string, --execute =string
Выполнить string.

-g файл графа, --graph =файл графа
Загрузите ранее созданный график достижимости из файл графа.rgh.

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

- ?, -час, --Помогите
Распечатайте сводку параметров командной строки для Марии и выйдите.

-I каталог, --include =каталог
присоединять каталог в список каталогов, в которых выполняется поиск включаемых файлов.

-i столбцы, --width =столбцы
Установите для правого поля вывода значение столбцы. По умолчанию 80.

-j Процессы, --jobs =Процессы
При проверке свойств безопасности (параметры -L, -M и -P), используйте это много рабочих
процессы для ускорения анализа на многопроцессорном компьютере. Смотрите также -k и
-Z.

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

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

-m модель, --model =модель
нагрузка модель и очистите его график достижимости.

-M модель, --md5-уплотненный =модель
нагрузка модель и подготовиться к его анализу, построив чрезмерное приближение
набор достижимых состояний в основной памяти. Смотрите также -P, -L, -j и -k.

-N Cregexp, --name =Cregexp
Укажите имена, разрешенные в контексте c как расширенное регулярное выражение RegExp.
Контекст идентифицируется первым символом строки параметра; в
следующие символы составляют регулярное выражение, разрешенные имена должны
совпадать.

-n Cregexp, --no-name =Cregexp
Укажите имена, недопустимые в контексте c как расширенное регулярное выражение
RegExp.
Если оба -N и и -n указаны для контекста c, то разрешающее совпадение занимает
приоритет. Например, чтобы потребовать, чтобы все пользовательские имена типов были
прекращается с _t, указывать -нт -Nt'_t $ '. Кавычки в последнем параметре равны
требуется для удаления специального значения из $ в оболочке командной строки вы
вероятно, используется для вызова Марии.

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

-p команду, --property-translator =команду
Укажите команду, которая будет использоваться для преобразования автоматов свойств. Команда должна
прочитать формулу со стандартного ввода и написать соответствующий автомат
описание к стандартному выводу. Переводчик фунт совместим с этим
опцию.

-q предел, --quantification-limit =предел
Предотвратить количественное определение (сумма множественных наборов) типов, имеющих более предел возможное
ценности. Предел 0 отключает проверки.

-U символ, --undefine =символ
Отменить определение символа препроцессора символ.

-u [a][f[Outfile]], --unfold =[a][f[Outfile]]
Разверните сеть с помощью алгоритма a и напишите в формате f в Outfile. Если Outfile
не указан, вывести развернутую сеть на стандартный вывод. Возможные форматы
Он m (Мария (читается человеком), по умолчанию), l (ЛоЛА), p (PEP) и r (ПРОД). Там
два алгоритма: традиционный (по умолчанию) и сокращенный путем построения покладистый
маркировка (M).

-В, --версия
Выведите номер версии Марии и выйдите.

-в, --подробный
Отображение подробной информации на разных этапах анализа.

-В, - предупреждения
Включить предупреждения о подозрительных сетевых конструкциях. Это поведение по умолчанию.

-ш, - без предупреждений
Противоположно -W. Отключить все предупреждения.

-x база номеров, --radix =база номеров
Укажите базу номеров для диагностического вывода. Допустимые значения для база номеров Он
октябрь, восьмеричный, 8, шестнадцатеричный, шестнадцатеричный, 16, декабрь, десятичная дробь и 10. По умолчанию используется
десятичные числа.

-Ю, -сжать-скрытый
Уменьшите набор достижимых состояний, не сохраняя последующие состояния
переходы экземпляров, для которых скрывать условие выполняется. Скрытые преемники
хранится в отдельном наборе состояний. Эта опция может сэкономить память (-L or -m) или уменьшить
вероятность пропуска состояний (-M or -P), и это может улучшить
эффективность параллельного анализа (-j or -k), но может и значительно увеличить
требования к процессорному времени. Опция также работает с моделью живучести.
проверки, но нет гарантии, что истинные значения свойств живучести
оставаться без изменений. Этот вариант можно комбинировать с -Z.

-у, --no-сжатие-скрытый
Противоположно -Y. Это поведение по умолчанию.

-З, --compress-пути
Сократите набор достижимых состояний, не сохраняя промежуточные состояния, которые имеют
у большинства один преемник. Эта опция может сэкономить память (-L or -m) или уменьшить
вероятность того, что состояния пропущены (-M or -P), и это может повысить эффективность
параллельного анализа (-j or -k), но это также может значительно увеличить
требования к процессорному времени. Опция также работает с проверкой живучести модели,
но нет гарантии, что истинные значения свойств живучести останутся
без изменений. Этот вариант можно комбинировать с -Y.

-з, --no-compress-пути
Противоположно -Z. Это поведение по умолчанию.

Используйте maria в Интернете с помощью сервисов onworks.net