Ubuntu Manpage: maria - Modular Reachability Analyzer for high-level Petri nets

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.

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