Provided by: maria_1.3.5-4_amd64 bug

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.

                                          August 5, 2002                                 MARIA(1)