NAME¶
maria - Modular Reachability Analyzer for high-level Petri nets
SYNOPSIS¶
maria [
options]
files...
DESCRIPTION¶
This manual page documents briefly 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 Völzer at ICATPN'98,
Flexibility in Algebraic Nets.
Algebraic System Nets is a framework that does not define any data types
or algebraic operations. The data type system and the operations in Maria are
designed with high-level programming and specification languages in
mind. Despite that, each Maria model has a finite unfolding.
To ensure interoperability with low-level Petri net tools, Maria translates
identifiers in unfolded nets to strings of alpha-numerical characters
and underscores. The filter
foldname.pl can be used or adapted to
improve the readability of the identifiers.
OPTIONS¶
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 files.
- -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-first 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 different way. The interpreter displays the
valuation and expression that caused the first error in a state; the
compiled code displays the number of errors. For performance reasons, the
generated code does not check for overflow 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
- Define the preprocessor symbol symbol.
- -d model,
--depth-first-search=model
- Generate the reachability graph of model using
depth-first 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 graphfile,
--graph=graphfile
- Load a previously generated reachability graph from
graphfile .rgh.
- -H h[,f[,t]],
--hashes=h[,f[,t]]
- Configure the parameters for probabilistic
verification ( -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 files.
- -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 specified as a 16-bit unsigned integer, usually
between 1024 and 65535. For the worker processes,
port/host specifies 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 files. 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 identified
by the first 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 specified for a context
c, then the allowing match takes precedence. For instance, to
require that all user defined 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 quantification (multi-set sum) of types
having more than limit possible values. A limit of 0 disables the
checks.
- -U symbol, --undefine=symbol
- Undefine the preprocessor symbol symbol.
- -u [a][f[outfile]],
--unfold=[ a][f[outfile]]
- Unfold the net using algorithm a and write it in
format f to outfile. If outfile is not
specified, 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 different 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 efficiency 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 efficiency
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.
SEE ALSO¶
lbt(1),
maria-vis(1),
maria-cso(1).
FILES¶
- /usr/share/maria/runtime/*.h
- The run-time library for the compilation option
- /usr/share/doc/maria/foldname.pl
- Script for demangling identifiers in unfolded net
output
The programs are documented fully by Maria, available via the Info
system.
AUTHOR¶
This manual page was written by Marko Mäkelä
<msmakela@tcs.hut.fi>. Maria was written by
Marko
Mäkelä, and some algorithms were designed by
Kimmo
Varpaaniemi, Timo Latvala and
Emil Falck. Please see the
copyright file in
/usr/share/doc/maria for details.