Man Linux: Main Page and Category List

NAME

       maria - Modular Reachability Analyzer for high-level Petri nets

SYNOPSIS

       maria [options] les...

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 graphle, --graph=graphle
              Load   a   previously   generated   reachability   graph    from
              graphle.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[outle]], --unfold=[a][f[outle]]
              Unfold  the  net  using  algorithm a and write it in format f to
              outle.  If outle 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