maria - Modular Reachability Analyzer for high-level Petri nets
maria [options] les...
This manual page documents brieﬂy 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 deﬁne any data types
or algebraic operations. The data type system and the operations in
Maria are designed with high-level programming and speciﬁcation
languages in mind. Despite that, each Maria model has a ﬁnite
To ensure interoperability with low-level Petri net tools, Maria
translates identiﬁers 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 identiﬁers.
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
-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 diﬀerent 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
overﬂow errors when adding items to multi-sets.
The opposite of -C. Evaluate all expressions in the built-in
interpreter. This is the default behavior.
-D symbol, --define=symbol
Deﬁne the preprocessor symbol symbol.
-d model, --depth-first-search=model
Generate the reachability graph of model using depth-ﬁrst
-E interval, --edges=interval
When generating the reachability graph, report the size of the
graph after every interval generated edges.
-e string, --execute=string
-g graphle, --graph=graphle
Load a previously generated reachability graph from
-H h[,f[,t]], --hashes=h[,f[,t]]
Conﬁgure the parameters for probabilistic veriﬁcation (-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
-i columns, --width=columns
Set the right margin of the output to columns. The default is
-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 speciﬁed as a
16-bit unsigned integer, usually between 1024 and 65535. For
the worker processes, port/host speciﬁes 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 identiﬁed 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 speciﬁed for a context c, then the
allowing match takes precedence. For instance, to require that
all user deﬁned 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
-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 quantiﬁcation (multi-set sum) of types having more than
limit possible values. A limit of 0 disables the checks.
-U symbol, --undefine=symbol
Undeﬁne 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 speciﬁed, 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).
Print the version number of Maria and exit.
Display verbose information on diﬀerent stages of the analysis.
Enable warnings about suspicious net constructs. This is the
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.
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 eﬃciency 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.
The opposite of -Y. This is the default behavior.
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 eﬃciency 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.
The opposite of -Z. This is the default behavior.
lbt(1), maria-vis(1), maria-cso(1).
The run-time library for the compilation option
Script for demangling identiﬁers in unfolded net output
The programs are documented fully by Maria, available via the
This manual page was written by Marko Mäkelä <email@example.com>.
Maria was written by Marko Mäkelä, 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.
August 5, 2002