MARIA(1)						      General Commands Manual							  MARIA(1)

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 Volzer 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 unfold-
       ing.
       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  algo-
	      rithm.   When  this option is used, evaluation errors are reported in a slightly different way.  The interpreter displays the valua-
	      tion and expression that caused the first error in a state; the compiled code displays the number of errors.  For  performance  rea-
	      sons, 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  algo-
	      rithms: 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 Makela <msmakela@tcs.hut.fi>.  Maria was written by Marko Makela, 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.

								  August 5, 2002							  MARIA(1)