maria - Modular Reachability Analyzer for high-level Petri nets

maria [options] les...

This manual page documents briey the maria command. More complete documentation is available in the GNU Info format; see below.

maria is a program that analyzes models of concurrent systems, described in its input language that is based on Algebraic System Nets. The formalism was presented by Ekkart Kindler and Hagen Vlzer at ICATPN'98, Flexibility in Algebraic Nets.

Algebraic System Nets is a framework that does not dene any data types or algebraic operations. The data type system and the operations in Maria are designed with high-level programming and specication languages in mind. Despite that, each Maria model has a nite unfolding.

To ensure interoperability with low-level Petri net tools, Maria translates identiers in unfolded nets to strings of alpha-numerical characters and underscores. The lter foldname.pl can be used or adapted to improve the readability of the identiers.

Maria follows the usual GNU command line syntax, with long options starting with two dashes (`-'). A summary of options is included below. For a complete description, see the Info les.

-a limit, --array-limit=limit

Limit the size of array index types to limit possible values. A limit of 0 disables the checks.

-b model, --breadth-first-search=model

Generate the reachability graph of model using breadth-rst search.

-C directory, --compile=directory

Generate C code in directory for evaluating expressions and for the low-level routines of the transition instance analysis algorithm. When this option is used, evaluation errors are reported in a slightly dierent way. The interpreter displays the valuation and expression that caused the rst error in a state; the compiled code displays the number of errors. For performance reasons, the generated code does not check for overow errors when adding items to multi-sets.

-c, --no-compile

The opposite of -C. Evaluate all expressions in the built-in interpreter. This is the default behavior.

-D symbol, --define=symbol

Dene the preprocessor symbol symbol.

-d model, --depth-first-search=model

Generate the reachability graph of model using depth-rst search.

-E interval, --edges=interval

When generating the reachability graph, report the size of the graph after every interval generated edges.

-e string, --execute=string

Execute string.

-g graphle, --graph=graphle

Load a previously generated reachability graph from graphle.rgh.

-H h[,f[,t]], --hashes=h[,f[,t]]

Congure the parameters for probabilistic verication (-P). Allocate t universal hash functions of f elements and corresponding hash tables of h bits each. Both h and f will be rounded up to next suitable values.

-?, -h, --help

Print a summary of the command-line options to Maria and exit.

-I directory, --include=directory

Append directory to the list of directories searched for include les.

-i columns, --width=columns

Set the right margin of the output to columns. The default is 80.

-j processes, --jobs=processes

When checking safety properties (options -L, -M and -P), use this many worker processes to speed up the analysis on a multiprocessor computer. See also -k and -Z.

-k port[/host], --connect=port[/host]

Distribute safety model checking (options -L, -M and -P) in a TCP/IP network. For the server, only port is specied as a 16-bit unsigned integer, usually between 1024 and 65535. For the worker processes, port/host species the port and the address of the server. See also -j.

-L model, --lossless=model

Load model and prepare for analyzing it by constructing a set of reachable states in disk les. See also -M, -P, -j and -k.

-m model, --model=model

Load model and clear its reachability graph.

-M model, --md5-compacted=model

Load model and prepare for analyzing it by constructing an over-approximation of set of reachable states in the main memory. See also -P, -L, -j and -k.

-N cregexp, --name=cregexp

Specify the names allowed in context c as the extended regular expression regexp. The context is identied by the rst character of the parameter string; the succeeding characters constitute the regular expression that allowed names must match.

-n cregexp, --no-name=cregexp

Specify the names not allowed in context c as the extended regular expression regexp.

If both -N and and -n are specied for a context c, then the allowing match takes precedence. For instance, to require that all user dened type names be terminated with _t, specify -nt -Nt'_t$'. The quotes in the latter parameter are required to remove the special meaning from $ in the command line shell you are probably using to invoke Maria.

-P model, --probabilistic=model

Load model and prepare for analyzing it by constructing a set of reachable states in the main memory by using a technique called bitstate hashing.

-p command, --property-translator=command

Specify the command to use for translating property automata. The command should read a formula from the standard input and write a corresponding automaton description to the standard output. The translator lbt is compatible with this option.

-q limit, --quantification-limit=limit

Prevent quantication (multi-set sum) of types having more than limit possible values. A limit of 0 disables the checks.

-U symbol, --undefine=symbol

Undene the preprocessor symbol symbol.

-u [a][f[outle]], --unfold=[a][f[outle]]

Unfold the net using algorithm a and write it in format f to outle. If outle is not specied, dump the unfolded net to the standard output. Possible formats are m (Maria (human-readable), default), l (LoLA), p (PEP), and r (PROD). There are two algorithms: traditional (default) and reduced by constructing a coverable marking (M).

-V, --version

Print the version number of Maria and exit.

-v, --verbose

Display verbose information on dierent stages of the analysis.

-W, --warnings

Enable warnings about suspicious net constructs. This is the default behavior.

-w, --no-warnings

The opposite of -W. Disable all warnings.

-x numberbase, --radix=numberbase

Specify the number base for diagnostic output. Allowed values for numberbase are oct, octal, 8, hex, hexadecimal, 16, dec, decimal and 10. The default is to use decimal numbers.

-Y, --compress-hidden

Reduce the set of reachable states by not storing the successor states of transitions instances for which a hide condition holds. The hidden successors are stored to a separate state set. This option may save memory (-L or -m) or reduce the probability that states are omitted (-M or -P), and it may improve the eciency of parallel analysis (-j or -k), but it may also considerably increase the processor time requirement. The option also works with liveness model checking, but there is no guarantee that the truth values of liveness properties remain unchanged. This option can be combined with -Z.

-y, --no-compress-hidden

The opposite of -Y. This is the default behavior.

-Z, --compress-paths

Reduce the set of reachable states by not storing intermediate states that have at most one successor. This option may save memory (-L or -m) or reduce the probability that states are omitted (-M or -P), and it may improve the eciency of parallel analysis (-j or -k), but it may also considerably increase the processor time requirement. The option also works with liveness model checking, but there is no guarantee that the truth values of liveness properties remain unchanged. This option can be combined with -Y.

-z, --no-compress-paths

The opposite of -Z. This is the default behavior.

lbt(1), maria-vis(1), maria-cso(1).

/usr/share/maria/runtime/*.h

The run-time library for the compilation option

/usr/share/doc/maria/foldname.pl

Script for demangling identiers in unfolded net output

The programs are documented fully by Maria, available via the Info system.

This manual page was written by Marko Mkel <msmakela@tcs.hut.fi>. Maria was written by Marko Mkel, and some algorithms were designed by Kimmo Varpaaniemi, Timo Latvala and Emil Falck. Please see the copyright le in /usr/share/doc/maria for details.