.\" Hey, EMACS: -*- nroff -*- .\" First parameter, NAME, should be all caps .\" Second parameter, SECTION, should be 1-8, maybe w/ subsection .\" other parameters are allowed: see man(7), man(1) .TH MARIA 1 "August 5, 2002" .\" Please adjust this date whenever revising the manpage. .\" .\" Some roff macros, for reference: .\" .nh disable hyphenation .\" .hy enable hyphenation .\" .ad l left justify .\" .ad b justify to both left and right margins .\" .nf disable filling .\" .fi enable filling .\" .br insert line break .\" .sp insert n+1 empty lines .\" for manpage-specific macros, see man(7) .SH NAME maria \- Modular Reachability Analyzer for high-level Petri nets .SH SYNOPSIS .B maria .RI [ options ] " \(files" ... .SH DESCRIPTION This manual page documents brie\(fly the .B maria command. More complete documentation is available in the GNU Info format; see below. .PP .\" TeX users may be more comfortable with the \fB\fP and .\" \fI\fP escape sequences to invoke bold face and italics, .\" respectively. \fBmaria\fP 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\(:olzer at ICATPN'98, .IR "Flexibility in Algebraic Nets". .br Algebraic System Nets is a framework that does not de\(fine any data types or algebraic operations. The data type system and the operations in Maria are designed with high-level programming and speci\(fication languages in mind. Despite that, each Maria model has a \(finite unfolding. .br To ensure interoperability with low-level Petri net tools, Maria translates identi\(fiers in unfolded nets to strings of alpha-numerical characters and underscores. The \(filter \fBfoldname.pl\fP can be used or adapted to improve the readability of the identi\(fiers. .SH OPTIONS Maria follows the usual GNU command line syntax, with long options starting with two dashes (`\fB-\fP'). A summary of options is included below. For a complete description, see the Info \(files. .TP .B -a \fIlimit\fP, --array-limit=\fIlimit\fP Limit the size of array index types to \fIlimit\fP possible values. A limit of 0 disables the checks. .TP .B -b \fImodel\fP, --breadth-first-search=\fImodel\fP Generate the reachability graph of \fImodel\fP using breadth-\(first search. .TP .B -C \fIdirectory\fP, --compile=\fIdirectory\fP Generate C code in \fIdirectory\fP 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\(fferent 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 over\(flow errors when adding items to multi-sets. .TP .B -c, --no-compile The opposite of \fB-C\fP. Evaluate all expressions in the built-in interpreter. This is the default behavior. .TP .B -D \fIsymbol\fP, --define=\fIsymbol\fP De\(fine the preprocessor symbol \fIsymbol\fP. .TP .B -d \fImodel\fP, --depth-first-search=\fImodel\fP Generate the reachability graph of \fImodel\fP using depth-\(first search. .TP .B -E \fIinterval\fP, --edges=\fIinterval\fP When generating the reachability graph, report the size of the graph after every \fIinterval\fP generated edges. .TP .B -e \fIstring\fP, --execute=\fIstring\fP Execute \fIstring\fP. .TP .B -g \fIgraph\(file\fP, --graph=\fIgraph\(file\fP Load a previously generated reachability graph from \fIgraph\(file\fP\fB.rgh\fP. .TP .B -H \fIh\fP\fR[\fP,\fIf\fP\fR[\fP,\fIt\fP\fR]]\fP, --hashes=\fIh\fP\fR[\fP,\fIf\fP\fR[\fP,\fIt\fP\fR]]\fP Con\(figure the parameters for probabilistic veri\(fication (\fB-P\fP). Allocate \fIt\fP universal hash functions of \fIf\fP elements and corresponding hash tables of \fIh\fP bits each. Both \fIh\fP and \fIf\fP will be rounded up to next suitable values. .TP .B -?, -h, --help Print a summary of the command-line options to Maria and exit. .TP .B -I \fIdirectory\fP, --include=\fIdirectory\fP Append \fIdirectory\fP to the list of directories searched for include \(files. .TP .B -i \fIcolumns\fP, --width=\fIcolumns\fP Set the right margin of the output to \fIcolumns\fP. The default is 80. .TP .B -j \fIprocesses\fP, --jobs=\fIprocesses\fP When checking safety properties (options \fB-L\fP, \fB-M\fP and \fB-P\fP), use this many worker processes to speed up the analysis on a multiprocessor computer. See also \fB-k\fP and \fB-Z\fP. .TP .B -k \fIport\fP\fR[\fP/\fIhost\fP\fR]\fP, --connect=\fIport\fP\fR[\fP/\fIhost\fP\fR]\fP Distribute safety model checking (options \fB-L\fP, \fB-M\fP and \fB-P\fP) in a TCP/IP network. For the server, only \fIport\fP is speci\(fied as a 16-bit unsigned integer, usually between 1024 and 65535. For the worker processes, \fIport\fP\fB/\fP\fIhost\fP speci\(fies the port and the address of the server. See also \fB-j\fP. .TP .B -L \fImodel\fP, --lossless=\fImodel\fP Load \fImodel\fP and prepare for analyzing it by constructing a set of reachable states in disk \(files. See also \fB-M\fP, \fB-P\fP, \fB-j\fP and \fB-k\fP. .TP .B -m \fImodel\fP, --model=\fImodel\fP Load \fImodel\fP and clear its reachability graph. .TP .B -M \fImodel\fP, --md5-compacted=\fImodel\fP Load \fImodel\fP and prepare for analyzing it by constructing an over-approximation of set of reachable states in the main memory. See also \fB-P\fP, \fB-L\fP, \fB-j\fP and \fB-k\fP. .TP .B -N \fIc\fP\fIregexp\fP, --name=\fIc\fP\fIregexp\fP Specify the names allowed in context \fIc\fP as the extended regular expression \fIregexp\fP. The context is identi\(fied by the \(first character of the parameter string; the succeeding characters constitute the regular expression that allowed names must match. .TP .B -n \fIc\fP\fIregexp\fP, --no-name=\fIc\fP\fIregexp\fP Specify the names not allowed in context \fIc\fP as the extended regular expression \fIregexp\fP. .br If both \fB-N\fP and and \fB-n\fP are speci\(fied for a context \fIc\fP, then the allowing match takes precedence. For instance, to require that all user de\(fined type names be terminated with \fB_t\fP, specify \fB-nt -Nt'_t$'\fP. The quotes in the latter parameter are required to remove the special meaning from \fB$\fP in the command line shell you are probably using to invoke Maria. .TP .B -P \fImodel\fP, --probabilistic=\fImodel\fP Load \fImodel\fP and prepare for analyzing it by constructing a set of reachable states in the main memory by using a technique called \fIbitstate hashing\fP. .TP .B -p \fIcommand\fP, --property-translator=\fIcommand\fP 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 \fBlbt\fP is compatible with this option. .TP .B -q \fIlimit\fP, --quantification-limit=\fIlimit\fP Prevent quanti\(fication (multi-set sum) of types having more than \fIlimit\fP possible values. A limit of 0 disables the checks. .TP .B -U \fIsymbol\fP, --undefine=\fIsymbol\fP Unde\(fine the preprocessor symbol \fIsymbol\fP. .TP .B -u \fR[\fP\fIa\fP\fR][\fP\fIf\fP\fR[\fP\fIout\(file\fP\fR]]\fP, --unfold=\fR[\fP\fIa\fP\fR][\fP\fIf\fP\fR[\fP\fIout\(file\fP\fR]]\fP Unfold the net using algorithm \fIa\fP and write it in format \fIf\fP to \fIout\(file\fP. If \fIout\(file\fP is not speci\(fied, dump the unfolded net to the standard output. Possible formats are \fBm\fP (Maria (human-readable), default), \fBl\fP (LoLA), \fBp\fP (PEP), and \fBr\fP (PROD). There are two algorithms: traditional (default) and reduced by constructing a \fIcoverable marking\fP (\fBM\fP). .TP .B -V, --version Print the version number of Maria and exit. .TP .B -v, --verbose Display verbose information on di\(fferent stages of the analysis. .TP .B -W, --warnings Enable warnings about suspicious net constructs. This is the default behavior. .TP .B -w, --no-warnings The opposite of \fB-W\fP. Disable all warnings. .TP .B -x \fInumberbase\fP, --radix=\fInumberbase\fP Specify the number base for diagnostic output. Allowed values for \fInumberbase\fP are \fBoct\fP, \fBoctal\fP, \fB8\fP, \fBhex\fP, \fBhexadecimal\fP, \fB16\fP, \fBdec\fP, \fBdecimal\fP and \fB10\fP. The default is to use decimal numbers. .TP .B -Y, --compress-hidden Reduce the set of reachable states by not storing the successor states of transitions instances for which a \fBhide\fP condition holds. The hidden successors are stored to a separate state set. This option may save memory (\fB-L\fP or \fB-m\fP) or reduce the probability that states are omitted (\fB-M\fP or \fB-P\fP), and it may improve the e\(Ficiency of parallel analysis (\fB-j\fP or \fB-k\fP), 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 \fB-Z\fP. .TP .B -y, --no-compress-hidden The opposite of \fB-Y\fP. This is the default behavior. .TP .B -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 (\fB-L\fP or \fB-m\fP) or reduce the probability that states are omitted (\fB-M\fP or \fB-P\fP), and it may improve the e\(Ficiency of parallel analysis (\fB-j\fP or \fB-k\fP), 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 \fB-Y\fP. .TP .B -z, --no-compress-paths The opposite of \fB-Z\fP. This is the default behavior. .SH SEE ALSO .BR lbt (1), .BR maria-vis (1), .BR maria-cso (1). .SH FILES .TP .I /usr/share/maria/runtime/*.h The run-time library for the compilation option .TP .I /usr/share/doc/maria/foldname.pl Script for demangling identi\(fiers in unfolded net output .br The programs are documented fully by .IR "Maria" , available via the Info system. .SH AUTHOR This manual page was written by Marko M\(:akel\(:a . Maria was written by .B Marko M\(:akel\(:a, and some algorithms were designed by .B Kimmo Varpaaniemi, .B Timo Latvala and .B Emil Falck. Please see the copyright \(file in .I /usr/share/doc/maria for details.