D7net Mini Sh3LL v1
| Current File : /var/../bin/../include/../share/doc/usbmuxd/../libksba8/../liblsan0/../maria-doc/html/maria_3.html |
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html401/loose.dtd">
<html>
<!-- Created on March 22, 2020 by texi2html 1.82
texi2html was written by:
Lionel Cons <Lionel.Cons@cern.ch> (original author)
Karl Berry <karl@freefriends.org>
Olaf Bachmann <obachman@mathematik.uni-kl.de>
and many others.
Maintained by: Many creative people.
Send bugs and suggestions to <texi2html-bug@nongnu.org>
-->
<head>
<title>Maria: 2. Reachability Analysis with Maria</title>
<meta name="description" content="Maria: 2. Reachability Analysis with Maria">
<meta name="keywords" content="Maria: 2. Reachability Analysis with Maria">
<meta name="resource-type" content="document">
<meta name="distribution" content="global">
<meta name="Generator" content="texi2html 1.82">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css">
<!--
a.summary-letter {text-decoration: none}
blockquote.smallquotation {font-size: smaller}
pre.display {font-family: serif}
pre.format {font-family: serif}
pre.menu-comment {font-family: serif}
pre.menu-preformatted {font-family: serif}
pre.smalldisplay {font-family: serif; font-size: smaller}
pre.smallexample {font-size: smaller}
pre.smallformat {font-family: serif; font-size: smaller}
pre.smalllisp {font-size: smaller}
span.roman {font-family:serif; font-weight:normal;}
span.sansserif {font-family:sans-serif; font-weight:normal;}
ul.toc {list-style: none}
-->
</style>
</head>
<body lang="en" bgcolor="#FFFFFF" text="#000000" link="#0000FF" vlink="#800080" alink="#FF0000">
<a name="Analysis"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="maria_2.html#Scoping" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Invoking-Maria" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria_2.html#Modeling" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Reachability-Analysis-with-Maria"></a>
<h1 class="chapter">2. Reachability Analysis with Maria</h1>
<a name="index-reachability-analysis"></a>
<p>Determining all interesting behaviors of a concurrent system is done by
computing a graph of all system states reachable from the initial state.
This process is called <em>reachability analysis</em>. Once a (possibly
incomplete) reachability graph has been generated, it can be examined,
and one can verify temporal properties from it.
</p>
<p>It is also possible to verify temporal properties during the generation
of the reachability graph (see section <a href="maria_4.html#Model-Checking">Model Checking Algorithms</a>). This can guide the
search and speed up the analysis, but verifying another temporal
property from the system will usually require the reachability analysis
to be performed again.
</p>
<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Invoking-Maria">2.1 Invoking Maria</a></td><td> </td><td align="left" valign="top"> Starting the reachability analysis
</td></tr>
<tr><td align="left" valign="top"><a href="#Interrupting">2.1.1 Interrupting the Reachability Analysis</a></td><td> </td><td align="left" valign="top"> Interrupting the reachability analysis
</td></tr>
<tr><td align="left" valign="top"><a href="#Maria-Shell">2.2 The Maria Shell</a></td><td> </td><td align="left" valign="top"> Examining the reachability graph interactively
</td></tr>
<tr><td align="left" valign="top"><a href="#Emacs">2.3 Editing Petri Nets with GNU Emacs</a></td><td> </td><td align="left" valign="top"></td></tr>
</table>
<hr size="6">
<a name="Invoking-Maria"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Analysis" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Interrupting" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Analysis" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Invoking-Maria-1"></a>
<h2 class="section">2.1 Invoking Maria</h2>
<a name="index-reachability-graph_002c-generating"></a>
<a name="index-command-line-options_002c-maria"></a>
<a name="index-invoking-maria"></a>
<p>The usual way to invoke Maria is as follows:
</p>
<table><tr><td> </td><td><pre class="example">maria -b <var>model</var>
</pre></td></tr></table>
<p>Here <var>model</var> is the Petri Net file name, which usually ends in
‘<samp>.pn</samp>’. The base name for reachability graph files (see section <a href="maria_6.html#Graph-Files">The Graph Files</a>) is generated by removing the directory name part and the file
name suffix (the last part of the name starting with a period ‘<samp>.</samp>’)
from the Petri Net file name. Three files will be generated using the
base name, with the suffixes ‘<samp>.rgd</samp>’, ‘<samp>.rgs</samp>’, ‘<samp>.rga</samp>’ and
‘<samp>.rgh</samp>’. Thus, ‘<samp>maria -b dining.pn</samp>’ yields ‘<tt>dining.rgd</tt>’,
‘<tt>dining.rgs</tt>’, ‘<tt>dining.rga</tt>’ and ‘<tt>dining.rgh</tt>’, and
‘<samp>maria -d test/order.pn</samp>’ yields ‘<tt>order.rgd</tt>’, ‘<tt>order.rgs</tt>’,
‘<tt>order.rga</tt>’ and ‘<tt>order.rgh</tt>’, in the current directory.
</p>
<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Interrupting">2.1.1 Interrupting the Reachability Analysis</a></td><td> </td><td align="left" valign="top"> Interrupting the reachability analysis
</td></tr>
<tr><td align="left" valign="top"><a href="#Maria-Options">2.1.2 Options</a></td><td> </td><td align="left" valign="top"> All the options described in detail,
in alphabetical order by short options.
</td></tr>
<tr><td align="left" valign="top"><a href="#Maria-Option-Cross-Key">2.1.3 Option Cross Key</a></td><td> </td><td align="left" valign="top"> Alphabetical list of long options.
</td></tr>
</table>
<hr size="6">
<a name="Interrupting"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Invoking-Maria" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Maria-Options" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Invoking-Maria" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Interrupting-the-Reachability-Analysis"></a>
<h3 class="subsection">2.1.1 Interrupting the Reachability Analysis</h3>
<p>Maria traps the interrupt signal (<code>SIGINT</code>), which is usually bound
to <kbd>C-c</kbd>. When it catches the signal, it will stop processing new
states. After Maria has finished with the state it is currently
processing, analyzing all the enabled transition instances and
generating the successor states, it will update the reachability graph
directory and stop the analysis.
</p>
<p>Analyzing and firing enabled transition instances in a state may take a
long time. Be patient or issue a <code>SIGQUIT</code> (normally bound to
<kbd>C-\</kbd>) or a <code>SIGKILL</code> signal to abort the process immediately,
leaving the reachability graph files in an inconsistent state.
</p>
<hr size="6">
<a name="Maria-Options"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Interrupting" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Maria-Option-Cross-Key" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Invoking-Maria" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Options"></a>
<h3 class="subsection">2.1.2 Options</h3>
<p>Maria supports both traditional single-letter options and mnemonic long
option names (if compiled with ‘<samp>getopt_long</samp>’, see section <a href="maria_7.html#Compiling">Compiling Maria</a>).
Long option names are indicated with ‘<samp>--</samp>’ instead of ‘<samp>-</samp>’.
Abbreviations for option names are allowed as long as they are unique.
When a long option takes an argument, like ‘<samp>--include</samp>’, connect the
option name and the argument with ‘<samp>=</samp>’ or provide the argument in
the immediately following command line argument.
</p>
<p>The options are interpreted in the order they are entered on the
command line. In other words, the options for interpreting a model
should be specified before loading the model. For instance,
‘<samp>maria -b dbm.pn -DUNUSED</samp>’ does not make much sense, while
‘<samp>maria -DUNUSED -b dbm.pn</samp>’ does.
</p>
<p>Here is a list of options that can be used with Maria, alphabetized by
short option. It is followed by a cross key alphabetized by long
option.
</p>
<dl compact="compact">
<dt> ‘<samp>-a <var>limit</var></samp>’</dt>
<dt> ‘<samp>--array-limit=<var>limit</var></samp>’</dt>
<dd><p>Limit the size of array index types to <var>limit</var> possible values. A
limit of 0 disables the checks.
</p>
</dd>
<dt> ‘<samp>-b <var>model</var></samp>’</dt>
<dt> ‘<samp>--breadth-first-search=<var>model</var></samp>’</dt>
<dd><p>Generate the reachability graph of <var>model</var> using breadth-first search.
Equivalent to ‘<samp>-m <var>model</var> -e breadth</samp>’.
</p>
</dd>
<dt> ‘<samp>-C <var>directory</var></samp>’</dt>
<dt> ‘<samp>--compile=<var>directory</var></samp>’</dt>
<dd><p>Generate C code in <var>directory</var> for evaluating expressions and for
the low-level routines of the transition instance analysis algorithm
(see section <a href="maria_4.html#Instance-Analysis">Transition Instance Analysis</a>). In order for this option to work, the
program must have been compiled with support for compiled expressions
enabled (see section <a href="maria_7.html#Compiling">Compiling Maria</a>). Also, the compilation script
‘<tt><var>progname</var>-cso</tt>’ must be found in the search path, where
‘<tt><var>progname</var></tt>’ is the name used to invoke the analyzer. It is a
good idea to have a look at the compilation script, and to adjust the
variable definition <code>INCLUDES</code>, so that the required header files
can always be found.
</p>
<p>You may also want to adjust the variables <code>DEFINES</code>, <code>CC</code>,
<code>CFLAGS</code>, <code>LD</code> and <code>LDFLAGS</code> either in the script or in the
environment of the reachability analyzer. For instance, if you are
using Bourne shell or one of its descendants, prefixing the command line
for invoking Maria with ‘<samp>DEFINES="" CFLAGS=""</samp>’ disables all
compiler optimizations for the model being analyzed. This may be useful
if the optimization algorithms of the C compiler would consume too many
resources.
</p>
<p>Applying this option should not affect the behaviour of the model
(i.e. it is a bug if it does). 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.
</p>
</dd>
<dt> ‘<samp>-c</samp>’</dt>
<dt> ‘<samp>--no-compile</samp>’</dt>
<dd><p>The opposite of ‘<samp>-C</samp>’. Evaluate all expressions in the built-in
interpreter. This is the default behavior.
</p>
</dd>
<dt> ‘<samp>-D <var>symbol</var></samp>’</dt>
<dt> ‘<samp>--define=<var>symbol</var></samp>’</dt>
<dd><p>Define the preprocessor symbol <var>symbol</var>. See section <a href="maria_2.html#Conditions">Conditional Processing</a>.
</p>
</dd>
<dt> ‘<samp>-d <var>model</var></samp>’</dt>
<dt> ‘<samp>--depth-first-search=<var>model</var></samp>’</dt>
<dd><p>Generate the reachability graph of <var>model</var> using depth-first search.
Equivalent to ‘<samp>-m <var>model</var> -e depth</samp>’.
</p>
</dd>
<dt> ‘<samp>-E <var>interval</var></samp>’</dt>
<dt> ‘<samp>--edges=<var>interval</var></samp>’</dt>
<dd><p>When generating the reachability graph, report the size of the graph
after every <var>interval</var> generated edges.
</p>
</dd>
<dt> ‘<samp>-e <var>string</var></samp>’</dt>
<dt> ‘<samp>--execute=<var>string</var></samp>’</dt>
<dd><p>Execute <var>string</var>. See section <a href="#Maria-Shell">The Maria Shell</a>.
</p>
</dd>
<dt> ‘<samp>-g <var>graphfile</var></samp>’</dt>
<dt> ‘<samp>--graph=<var>graphfile</var></samp>’</dt>
<dd><p>Load a previously generated reachability graph from
‘<tt><var>graphfile</var>.rgh</tt>’.
</p>
</dd>
<dt> ‘<samp>-H <var>h</var>[,<var>f</var>[,<var>t</var>]]</samp>’</dt>
<dt> ‘<samp>--hashes=<var>h</var>[,<var>f</var>[,<var>t</var>]]</samp>’</dt>
<dd><p>Configure the parameters for lossy verification (‘<samp>-P</samp>’ or
‘<samp>-M</samp>’). For ‘<samp>-P</samp>’, allocate <var>t</var> universal hash functions
of <var>f</var> elements and corresponding hash tables of <var>h</var> bits
each. For ‘<samp>-M</samp>’, allocate a <var>f</var> bytes for all <var>h</var>
elements of the hash table. The value <var>h</var> (and for ‘<samp>-P</samp>’,
also the value <var>f</var>) will be rounded up to suitable values.
</p>
</dd>
<dt> ‘<samp>-?</samp>’</dt>
<dt> ‘<samp>-h</samp>’</dt>
<dt> ‘<samp>--help</samp>’</dt>
<dd><p>Print a summary of the command-line options to Maria and exit.
</p>
</dd>
<dt> ‘<samp>-I <var>directory</var></samp>’</dt>
<dt> ‘<samp>--include=<var>directory</var></samp>’</dt>
<dd><p>Append <var>directory</var> to the list of directories searched for include
files.
</p>
</dd>
<dt> ‘<samp>-i <var>columns</var></samp>’</dt>
<dt> ‘<samp>--width=<var>columns</var></samp>’</dt>
<dd><p>Set the right margin of the output to <var>columns</var>. The default is 80.
</p>
</dd>
<dt> ‘<samp>-j <var>processes</var></samp>’</dt>
<dt> ‘<samp>--jobs=<var>processes</var></samp>’</dt>
<dd><p>When checking safety properties (options ‘<samp>-L</samp>’, ‘<samp>-M</samp>’ and
‘<samp>-P</samp>’), use this many worker processes to speed up the analysis on
a multiprocessor computer. See also ‘<samp>-k</samp>’ and ‘<samp>-Z</samp>’. Note
that on Digital UNIX, this option may not work properly if the
model is generating successor states too fast (especially when using
the ‘<samp>-C</samp>’ option).
</p>
</dd>
<dt> ‘<samp>-k <var>port</var>[/<var>host</var>]</samp>’</dt>
<dt> ‘<samp>--connect=<var>port</var>[/<var>host</var>]</samp>’</dt>
<dd><p>Distribute safety model checking (options ‘<samp>-L</samp>’, ‘<samp>-M</samp>’ and
‘<samp>-P</samp>’) in a TCP/IP network. For the server, only <var>port</var> is
specified as a 16-bit unsigned integer, usually between 1024 and
65535. For the worker processes, <var>port</var>/<var>host</var> specifies the
port and the address of the server. See also ‘<samp>-j</samp>’.
</p>
<p>All processes should use the same command line options, except that on
the server, the ‘<samp>-k</samp>’ switch takes only the <var>port</var> argument, and
the worker processes exit after executing the ‘<samp>breadth</samp>’ or
‘<samp>depth</samp>’ command. To gain best performance, start the server and
one client on the fastest computer of the network.
</p>
<p>Note that when a computer arranges machine words in the big endian byte
order, all computers must be big endian and have the same word length.
Little endian computers interoperate regardless of their word lengths.
</p>
</dd>
<dt> ‘<samp>-L <var>model</var></samp>’</dt>
<dt> ‘<samp>--lossless=<var>model</var></samp>’</dt>
<dd><p>Load <var>model</var> and prepare for analysing it by constructing a set of
reachable states in disk files. See also ‘<samp>-M</samp>’, ‘<samp>-P</samp>’,
‘<samp>-j</samp>’ and ‘<samp>-k</samp>’.
</p>
</dd>
<dt> ‘<samp>-m <var>model</var></samp>’</dt>
<dt> ‘<samp>--model=<var>model</var></samp>’</dt>
<dd><p>Load <var>model</var> and clear its reachability graph. See also ‘<samp>-b</samp>’
and ‘<samp>-d</samp>’.
</p>
</dd>
<dt> ‘<samp>-M <var>model</var></samp>’</dt>
<dt> ‘<samp>--md5-compacted=<var>model</var></samp>’</dt>
<dd><p>Load <var>model</var> and prepare for analysing it by constructing an
overapproximation of the set of reachable states in the main memory
by using a technique called <em>hash compaction</em>. See also ‘<samp>-P</samp>’,
‘<samp>-L</samp>’, ‘<samp>-j</samp>’ and ‘<samp>-k</samp>’.
</p>
</dd>
<dt> ‘<samp>-N <var>c</var><var>regexp</var></samp>’</dt>
<dt> ‘<samp>--name=<var>c</var><var>regexp</var></samp>’</dt>
<dd><p>Specify the names allowed in context <var>c</var> as the extended regular
expression <var>regexp</var>; See <a href="../grep/Regular-Expressions.html#Regular-Expressions">(grep)Regular Expressions</a> section ‘Regular Expressions’ in <cite>GNU GREP Manual</cite>. In order for this option to work,
the program must have been compiled with the POSIX regular expression
library enabled (see section <a href="maria_7.html#Compiling">Compiling Maria</a>). The context is identified by the
first character of the parameter string; the succeeding characters
constitute the regular expression that allowed names must match:
</p><dl compact="compact">
<dt> ‘<samp>P</samp>’</dt>
<dd><p>place name
</p></dd>
<dt> ‘<samp>T</samp>’</dt>
<dd><p>transition name
</p></dd>
<dt> ‘<samp>t</samp>’</dt>
<dd><p>type name
</p></dd>
<dt> ‘<samp>e</samp>’</dt>
<dd><p>name of enumeration constant
</p></dd>
<dt> ‘<samp>c</samp>’</dt>
<dd><p>name of struct or union component
</p></dd>
<dt> ‘<samp>f</samp>’</dt>
<dd><p>function name
</p></dd>
<dt> ‘<samp>p</samp>’</dt>
<dd><p>function parameter name
</p></dd>
<dt> ‘<samp>v</samp>’</dt>
<dd><p>transition variable name
</p></dd>
<dt> ‘<samp>i</samp>’</dt>
<dd><p>iterator variable name
</p></dd>
</dl>
</dd>
<dt> ‘<samp>-n <var>c</var><var>regexp</var></samp>’</dt>
<dt> ‘<samp>--no-name=<var>c</var><var>regexp</var></samp>’</dt>
<dd><p>Specify the names not allowed in context <var>c</var> as the extended regular
expression <var>regexp</var>.
</p>
<p>If both ‘<samp>-N</samp>’ and and ‘<samp>-n</samp>’ are specified for a context <var>c</var>,
then the allowing match takes precedence. For instance, to require that
all user defined type names be terminated with ‘<samp>_t</samp>’, specify
‘<samp>-nt -Nt'_t$'</samp>’. The quotes in the latter parameter are required to
remove the special meaning from ‘<samp>$</samp>’ in the command line shell you
are probably using to invoke Maria.
</p>
</dd>
<dt> ‘<samp>-P <var>model</var></samp>’</dt>
<dt> ‘<samp>--probabilistic=<var>model</var></samp>’</dt>
<dd><p>Load <var>model</var> and prepare for analysing it by constructing an
overapproximation of the set of reachable states in the main memory by
using a technique called <em>bitstate hashing</em>. See also ‘<samp>-M</samp>’,
‘<samp>-L</samp>’, ‘<samp>-j</samp>’ and ‘<samp>-k</samp>’.
</p>
</dd>
<dt> ‘<samp>-p <var>command</var></samp>’</dt>
<dt> ‘<samp>--property-translator=<var>command</var></samp>’</dt>
<dd><p>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 ‘<tt>lbt</tt>’ (available separately) is compatible with this
option.
</p>
</dd>
<dt> ‘<samp>-q <var>limit</var></samp>’</dt>
<dt> ‘<samp>--quantification-limit=<var>limit</var></samp>’</dt>
<dd><p>Prevent quantification (multi-set sum) of types having more than
<var>limit</var> possible values. A limit of 0 disables the checks.
</p>
</dd>
<dt> ‘<samp>-R</samp>’</dt>
<dt> ‘<samp>--modular</samp>’</dt>
<dd><p>Explore the state space in a modular way. See section <a href="maria_2.html#Subnets">Defining Subnets for Modular State Space Exploration</a>.
</p>
</dd>
<dt> ‘<samp>-r</samp>’</dt>
<dt> ‘<samp>--no-modular</samp>’</dt>
<dd><p>Consider only one state space. This is the default.
</p>
</dd>
<dt> ‘<samp>-t <var>limit</var></samp>’</dt>
<dt> ‘<samp>--tolerance=<var>limit</var></samp>’</dt>
<dd><p>Abort the analysis when <var>limit</var> non-fatal errors have been
reported. A limit of 0, the default, allows an infinite number of
errors to occur.
</p>
</dd>
<dt> ‘<samp>-U <var>symbol</var></samp>’</dt>
<dt> ‘<samp>--undefine=<var>symbol</var></samp>’</dt>
<dd><p>Undefine the preprocessor symbol <var>symbol</var>. See section <a href="maria_2.html#Conditions">Conditional Processing</a>.
</p>
</dd>
<dt> ‘<samp>-u [M][<var>f</var>[<var>outfile</var>]]</samp>’</dt>
<dt> ‘<samp>--unfold=[M][<var>f</var>[<var>outfile</var>]]</samp>’</dt>
<dd><p>Unfold the net (optionally reducing it by constructing a
<em>coverable marking</em> (‘<samp>M</samp>’)) and write it in format <var>f</var> to
<var>outfile</var>. If <var>outfile</var> is not specified, dump the unfolded
net to the standard output. Possible formats are ‘<samp>m</samp>’ (Maria
(human-readable), default), ‘<samp>l</samp>’ (LoLA), ‘<samp>p</samp>’ (PEP), and
‘<samp>r</samp>’ (PROD).
</p>
<p>When the PROD output is chosen, <var>outfile</var> must be specified and end
in ‘<samp>.net</samp>’. Since PROD has no low-level input format, the
transitions in the low-level net are grouped to equivalence classes
based on the input and output arc weights. Each equivalence class is
folded to a high-level transition. The translation makes use of tables
that are written to a separate file. If <var>outfile</var> is
‘<tt><var>out</var>.net</tt>’, the tables are written to
‘<tt><var>out</var>.src/tables.c</tt>’.
</p>
</dd>
<dt> ‘<samp>-V</samp>’</dt>
<dt> ‘<samp>--version</samp>’</dt>
<dd><p>Print the version number of Maria and exit.
</p>
</dd>
<dt> ‘<samp>-v</samp>’</dt>
<dt> ‘<samp>--verbose</samp>’</dt>
<dd><p>Display verbose information on different stages of the analysis.
</p>
</dd>
<dt> ‘<samp>-W</samp>’</dt>
<dt> ‘<samp>--warnings</samp>’</dt>
<dd><p>Enable warnings about suspicious net constructs. This is the default
behavior.
</p>
</dd>
<dt> ‘<samp>-w</samp>’</dt>
<dt> ‘<samp>--no-warnings</samp>’</dt>
<dd><p>The opposite of ‘<samp>-W</samp>’. Disable all warnings.
</p>
</dd>
<dt> ‘<samp>-x <var>numberbase</var></samp>’</dt>
<dt> ‘<samp>--radix=<var>numberbase</var></samp>’</dt>
<dd><p>Specify the number base for diagnostic output. Allowed values for
<var>numberbase</var> are ‘<samp>oct</samp>’, ‘<samp>octal</samp>’, ‘<samp>8</samp>’, ‘<samp>hex</samp>’,
‘<samp>hexadecimal</samp>’, ‘<samp>16</samp>’, ‘<samp>dec</samp>’, ‘<samp>decimal</samp>’ and ‘<samp>10</samp>’.
The default is to use decimal numbers.
</p>
</dd>
<dt> ‘<samp>-Y</samp>’</dt>
<dt> ‘<samp>--compress-hidden</samp>’</dt>
<dd><p>Reduce the set of reachable states by not storing the successor states
of transitions instances for which a ‘<samp>hide</samp>’ condition holds. The
hidden successors are stored to a separate state set. This option may
save memory (‘<samp>-L</samp>’ or ‘<samp>-m</samp>’) or reduce the probability that
states are omitted (‘<samp>-M</samp>’ or ‘<samp>-P</samp>’), and it may improve the
efficiency of parallel analysis (‘<samp>-j</samp>’ or ‘<samp>-k</samp>’), 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 ‘<samp>-Z</samp>’.
</p>
</dd>
<dt> ‘<samp>-y</samp>’</dt>
<dt> ‘<samp>--no-compress-hidden</samp>’</dt>
<dd><p>The opposite of ‘<samp>-Y</samp>’. This is the default behavior.
</p>
</dd>
<dt> ‘<samp>-Z</samp>’</dt>
<dt> ‘<samp>--compress-paths</samp>’</dt>
<dd><p>Reduce the set of reachable states by not storing intermediate states
that have at most one successor. This option may save memory
(‘<samp>-L</samp>’ or ‘<samp>-m</samp>’) or reduce the probability that states are
omitted (‘<samp>-M</samp>’ or ‘<samp>-P</samp>’), and it may improve the efficiency of
parallel analysis (‘<samp>-j</samp>’ or ‘<samp>-k</samp>’), 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 ‘<samp>-Y</samp>’.
</p>
</dd>
<dt> ‘<samp>-z</samp>’</dt>
<dt> ‘<samp>--no-compress-paths</samp>’</dt>
<dd><p>The opposite of ‘<samp>-Z</samp>’. This is the default behavior.
</p></dd>
</dl>
<hr size="6">
<a name="Maria-Option-Cross-Key"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Maria-Options" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Maria-Shell" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Invoking-Maria" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Option-Cross-Key"></a>
<h3 class="subsection">2.1.3 Option Cross Key</h3>
<p>Here is a list of options, alphabetized by long option, to help you find
the corresponding short option.
</p>
<table><tr><td> </td><td><pre class="example">--array-limit=<var>limit</var> -a <var>limit</var>
--breadth-first-search=<var>model</var> -b <var>model</var>
--compile=<var>directory</var> -C <var>directory</var>
--compress-hidden -Y
--compress-paths -Z
--connect=<var>port</var>[/<var>host</var>] -k <var>port</var>[/<var>host</var>]
--define=<var>symbol</var> -D <var>symbol</var>
--depth-first-search=<var>model</var> -d <var>model</var>
--edges=<var>interval</var> -E <var>interval</var>
--execute=<var>string</var> -e <var>string</var>
--graph=<var>graphfile</var> -g <var>graphfile</var>
--hashes=<var>h</var>[,<var>f</var>[,<var>t</var>]] -H <var>h</var>[,<var>f</var>[,<var>t</var>]]
--help -h
--include=<var>directory</var> -I <var>directory</var>
--jobs=<var>processes</var> -j <var>processes</var>
--lossless=<var>model</var> -L <var>model</var>
--md5-compacted=<var>model</var> -M <var>model</var>
--model=<var>model</var> -m <var>model</var>
--modular -R
--name=<var>c</var><var>regexp</var> -N <var>c</var><var>regexp</var>
--no-compile -c
--no-compress-hidden -y
--no-compress-paths -z
--no-modular -r
--no-name=<var>c</var><var>regexp</var> -n <var>c</var><var>regexp</var>
--no-warnings -w
--probabilistic=<var>model</var> -P <var>model</var>
--property-translator=<var>command</var> -p <var>command</var>
--quantification-limit=<var>limit</var> -q <var>limit</var>
--radix=<var>numberbase</var> -x <var>numberbase</var>
--tolerance=<var>limit</var> -t <var>limit</var>
--undefine=<var>symbol</var> -U <var>symbol</var>
--unfold=[M][<var>f</var>[<var>outfile</var>]] -u [M][<var>f</var>[<var>outfile</var>]]
--verbose -v
--version -V
--warnings -W
--width=<var>columns</var> -i <var>columns</var>
</pre></td></tr></table>
<hr size="6">
<a name="Maria-Shell"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Maria-Option-Cross-Key" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Line-Editor" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Analysis" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="The-Maria-Shell"></a>
<h2 class="section">2.2 The Maria Shell</h2>
<a name="index-reachability-graph_002c-examining"></a>
<p>The Maria shell can be used to interactively examine the reachability
graph of a model or to check temporal properties in it.
</p>
<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Line-Editor">2.2.1 The Line Editor</a></td><td> </td><td align="left" valign="top"> The command line editor
</td></tr>
<tr><td align="left" valign="top"><a href="#Query-Language">2.2.2 The Query Language</a></td><td> </td><td align="left" valign="top"> The query language
</td></tr>
<tr><td align="left" valign="top"><a href="#Quirks">2.2.3 Some Quirks with the Query Language</a></td><td> </td><td align="left" valign="top"> Some considerations on the preprocessor
</td></tr>
<tr><td align="left" valign="top"><a href="#Visual">2.2.4 Visualizing Graphs and Paths</a></td><td> </td><td align="left" valign="top"> Visualizing the results
</td></tr>
</table>
<hr size="6">
<a name="Line-Editor"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Maria-Shell" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Name-Completion" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Maria-Shell" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="The-Line-Editor"></a>
<h3 class="subsection">2.2.1 The Line Editor</h3>
<a name="index-command-line-interface"></a>
<p>The Maria shell has a command-line driven user interface. When support
for the GNU Readline library has been enabled at compile time
(see section <a href="maria_7.html#Compiling">Compiling Maria</a>), using the command line is pretty comfortable.
Without Readline, you have to cope with the system’s default line
editor, which certainly lacks command line history and completion
features.
</p>
<p>When invoked, Maria will greet you with the prompt ‘<samp>@0$</samp>’, where
‘<samp>0</samp>’ is the number of the current state, or ‘<samp>$</samp>’ if no model has
been loaded. The initial state always has the number zero. Command
lines may be split over multiple physical lines. When there is an
unbalanced single or double quote or a multi-line (C-style) comment, or
when the line ends in a backslash ‘<samp>\</samp>’, Maria will present the
continuation prompt ‘<samp>@<var>n</var>></samp>’. In case of a typing mistake,
<kbd>EOF</kbd> will tell Maria to abort reading continuation lines.
</p>
<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Name-Completion">2.2.1.1 Name Completion</a></td><td> </td><td align="left" valign="top"> Features of the Readline library
</td></tr>
</table>
<hr size="6">
<a name="Name-Completion"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Line-Editor" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Line-Editor" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Name-Completion-1"></a>
<h4 class="subsubsection">2.2.1.1 Name Completion</h4>
<a name="index-Readline"></a>
<a name="index-completion-of-names"></a>
<a name="index-names_002c-completion-of"></a>
<p>This is by no means a complete list of Readline features. See <a href="../readline/Command-Line-Editing.html#Command-Line-Editing">(readline)Command Line Editing</a> section ‘Command Line Editing’ in <cite>GNU Readline Library</cite>,
if you are not familiar with Readline.
</p>
<p>One of the nicest features of the Readline library is context-sensitive
completion of names. The Maria shell completes names of data types
(immediately following the ‘<samp>is</samp>’ keyword), places (following
‘<samp>place</samp>’), transitions (‘<samp>trans</samp>’), and keywords. Let us now
assume that you have generated the reachability graph for the dining
philosopher example (see section <a href="maria_8.html#Dining">Dining Philosophers (‘<tt>dining.pn</tt>’)</a>). The following example illustrates
how the context-sensitive completion of names works.
</p>
<table><tr><td> </td><td><pre class="example"><b>$</b>graph dining<kbd>RET</kbd>
<b>@0$</b>pa<kbd>TAB</kbd>
<b>@0$</b>pa<b>th </b>@29 pl<kbd>TAB</kbd>
<b>@0$</b>path @29 pl<b>ace "</b>f<kbd>TAB</kbd>
<b>@0$</b>path @29 place "f<b>ork" </b>eq<kbd>TAB</kbd>
<b>@0$</b>path @29 place "fork" eq<b>uals </b>em<kbd>TAB</kbd>
<b>@0$</b>path @29 place "fork" equals em<b>pty </b><kbd>RET</kbd>
<b>shortest path from condition to @29 (2 nodes):</b>
</pre><pre class="example"><b>@74:state (</b>
<b> state:</b>
<b> {3,thinking},{1,hungry},{4,hungry},{5,hungry},{2,eating}</b>
<b>)</b>
<b>4 predecessors</b>
<b>1 successor</b>
</pre><pre class="example"><b>transition finish->@29</b>
<b><</b>
<b> p:2</b>
<b>></b>
</pre><pre class="example"><b>@29:state (</b>
<b> fork:</b>
<b> 2,3</b>
<b> state:</b>
<b> {2,thinking},{3,thinking},{1,hungry},{4,hungry},{5,hungry}</b>
<b>)</b>
<b>4 predecessors</b>
<b>3 successors</b>
</pre><pre class="example"><b>@0$</b>exit <kbd>RET</kbd>
</pre></td></tr></table>
<p>Unfortunately backslash-quoted names cannot be completed. This is due
to a limitation of the Readline library, which will only call the
dequoting function if its built-in filename completion function is being
used. This is why the keyword completer adds a double quotation mark
after keywords that are likely to be followed by a name.
</p>
<hr size="6">
<a name="Query-Language"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Name-Completion" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Graph-and-Model" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Maria-Shell" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="The-Query-Language"></a>
<h3 class="subsection">2.2.2 The Query Language</h3>
<a name="index-query-language"></a>
<p>Maria uses a script language in which statements are separated by
semicolons (‘<samp>;</samp>’). See section <a href="#Separating-Statements">Separating Statements</a>, for other
considerations.
</p>
<p>There are commands for moving around in the graph and for evaluating
formulae in different graph nodes. Maria shell commands are reserved
words only in the beginning of a statement: there is no need to quote a
place name ‘<samp>exit</samp>’, for instance.
</p>
<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Graph-and-Model">2.2.2.1 Loading a Model</a></td><td> </td><td align="left" valign="top"> Loading a reachability graph or model
</td></tr>
<tr><td align="left" valign="top"><a href="#Dump">2.2.2.2 Displaying a Model</a></td><td> </td><td align="left" valign="top"> Displaying a model
</td></tr>
<tr><td align="left" valign="top"><a href="#Unfold">2.2.2.3 Unfolding a Model</a></td><td> </td><td align="left" valign="top"> Unfolding a model
</td></tr>
<tr><td align="left" valign="top"><a href="#LSTS">2.2.2.4 Exporting a Labelled State Transition System</a></td><td> </td><td align="left" valign="top"></td></tr>
<tr><td align="left" valign="top"><a href="#Dumpgraph">2.2.2.5 Exporting the Reachability Graph</a></td><td> </td><td align="left" valign="top"> Exporting a reachability graph
</td></tr>
<tr><td align="left" valign="top"><a href="#Depth-and-Breadth">2.2.2.6 Exhaustive Analysis</a></td><td> </td><td align="left" valign="top"> Exhaustive reachability analysis
</td></tr>
<tr><td align="left" valign="top"><a href="#Eval">2.2.2.7 Evaluating Expressions and Formulae</a></td><td> </td><td align="left" valign="top"> Evaluating expressions and formulae
</td></tr>
<tr><td align="left" valign="top"><a href="#Show">2.2.2.8 Displaying Markings</a></td><td> </td><td align="left" valign="top"> Displaying markings
</td></tr>
<tr><td align="left" valign="top"><a href="#Hide">2.2.2.9 Excluding Places from Displayed Markings</a></td><td> </td><td align="left" valign="top"> Omitting places from markings
</td></tr>
<tr><td align="left" valign="top"><a href="#Subnet">2.2.2.10 Selecting the Active Subnet</a></td><td> </td><td align="left" valign="top"> Selecting the active subnet
</td></tr>
<tr><td align="left" valign="top"><a href="#Succ">2.2.2.11 Listing Successor Nodes</a></td><td> </td><td align="left" valign="top"> Listing successor nodes
</td></tr>
<tr><td align="left" valign="top"><a href="#Pred">2.2.2.12 Listing Predecessor Nodes</a></td><td> </td><td align="left" valign="top"> Listing predecessor nodes
</td></tr>
<tr><td align="left" valign="top"><a href="#Go">2.2.2.13 Moving in the Graph</a></td><td> </td><td align="left" valign="top"> Moving between nodes
</td></tr>
<tr><td align="left" valign="top"><a href="#Trans">2.2.2.14 Anonymous Transitions</a></td><td> </td><td align="left" valign="top"> Defining and firing an anonymous transition
</td></tr>
<tr><td align="left" valign="top"><a href="#Function">2.2.2.15 Defining Functions</a></td><td> </td><td align="left" valign="top"> Defining functions
</td></tr>
<tr><td align="left" valign="top"><a href="#Strong">2.2.2.16 Strongly Connected Components</a></td><td> </td><td align="left" valign="top"> Strongly connected components
</td></tr>
<tr><td align="left" valign="top"><a href="#Path">2.2.2.17 Shortest Paths</a></td><td> </td><td align="left" valign="top"> Shortest paths
</td></tr>
<tr><td align="left" valign="top"><a href="#Misc">2.2.2.18 Miscellanous Commands</a></td><td> </td><td align="left" valign="top"> Miscellanous commands
</td></tr>
<tr><td align="left" valign="top"><a href="#Exit">2.2.2.19 Exiting</a></td><td> </td><td align="left" valign="top"></td></tr>
</table>
<hr size="6">
<a name="Graph-and-Model"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Query-Language" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Dump" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Loading-a-Model"></a>
<h4 class="subsubsection">2.2.2.1 Loading a Model</h4>
<a name="index-graph_002c-query-language"></a>
<a name="index-model_002c-query-language"></a>
<table><tr><td> </td><td><pre class="example">statement:
GRAPH name
|
MODEL name
</pre></td></tr></table>
<p>The ‘<samp>graph</samp>’ command loads a previously generated reachability
graph. The supplied name must exclude the ‘<samp>.rgh</samp>’ suffix.
</p>
<p>The ‘<samp>model</samp>’ command loads a Petri net model and initializes its
reachability graph. Be careful with this command; it will delete a
previously generated reachability graph of the model, if one exists in
the current directory.
</p>
<hr size="6">
<a name="Dump"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Graph-and-Model" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Unfold" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Displaying-a-Model"></a>
<h4 class="subsubsection">2.2.2.2 Displaying a Model</h4>
<a name="index-visual_002c-query-language"></a>
<a name="index-dump_002c-query-language"></a>
<table><tr><td> </td><td><pre class="example">statement:
[ VISUAL ] DUMP
</pre></td></tr></table>
<p>The ‘<samp>dump</samp>’ command displays the syntax tree of the current model in
the modelling language. When the ‘<samp>visual</samp>’ prefix is present, the
Petri net will be displayed graphically (see section <a href="#Visual">Visualizing Graphs and Paths</a>). This command
may be useful when trying to find out how Maria expands multi-set
summations (see section <a href="maria_2.html#Multi_002dSets">Operations on Multi-Sets</a>) or quantifications (see section <a href="maria_2.html#Logic">Boolean Logic</a>).
</p>
<hr size="6">
<a name="Unfold"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Dump" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#LSTS" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Unfolding-a-Model"></a>
<h4 class="subsubsection">2.2.2.3 Unfolding a Model</h4>
<a name="index-unfold_002c-query-language"></a>
<table><tr><td> </td><td><pre class="example">statement:
UNFOLD [ name ]
</pre></td></tr></table>
<p>The ‘<samp>unfold</samp>’ command unfolds the currently loaded Petri net model.
The argument takes the same format as the command line option ‘<samp>-u</samp>’
(see section <a href="#Maria-Options">Options</a>).
</p>
<hr size="6">
<a name="LSTS"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Unfold" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Dumpgraph" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Exporting-a-Labelled-State-Transition-System"></a>
<h4 class="subsubsection">2.2.2.4 Exporting a Labelled State Transition System</h4>
<a name="index-lsts_002c-query-language"></a>
<table><tr><td> </td><td><pre class="example">statement:
LSTS [ name ]
</pre></td></tr></table>
<p>Maria is able to export the reachability graph or parts thereof as a
labelled state transition system. The ‘<samp>lsts</samp>’ command specifies a
file name for an LSTS. When the command is invoked without a file name,
any currently open LSTS files are closed and the function cancelled.
</p>
<p>The ‘<samp>lsts</samp>’ command affects exhaustive analysis (see section <a href="#Depth-and-Breadth">Exhaustive Analysis</a>), non-visual path queries (see section <a href="#Path">Shortest Paths</a>) and the representation
of counterexample paths of liveness properties (see section <a href="maria_4.html#Liveness">Checking Liveness Properties</a>).
</p>
<p>In exhaustive analysis, the command should be invoked before any states
have been explored, right after the model has been loaded. When using
the path commands, the ‘<samp>lsts</samp>’ command should be issued right before
generating the counterexample. These measures are necessary, because
for efficiency reasons, the ‘<samp>lsts</samp>’ command has been implemented so
that all generated states and arcs are exported to LSTS files if ones
have been opened. The path query commands export results to LSTS if the
files are open, and close the files immediately after that. It is
impossible to combine several query results into one exported LSTS.
</p>
<p>The LSTS output can be controlled by hiding variables or transition
instances (see section <a href="maria_2.html#Transitions">Transition Definition: ‘<samp>trans</samp>’</a>) and by specifying state propositions
(see section <a href="maria_2.html#Propositions">Specifying State Propositions for LSTS Output</a>).
</p>
<hr size="6">
<a name="Dumpgraph"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#LSTS" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Depth-and-Breadth" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Exporting-the-Reachability-Graph"></a>
<h4 class="subsubsection">2.2.2.5 Exporting the Reachability Graph</h4>
<a name="index-dumpgraph_002c-query-language"></a>
<a name="index-visual_002c-query-language-1"></a>
<table><tr><td> </td><td><pre class="example">statement:
[ VISUAL ] DUMPGRAPH
</pre></td></tr></table>
<p>The command ‘<samp>dumpgraph</samp>’ exports the portion of the reachability
graph that has been generated so far. When the ‘<samp>visual</samp>’ prefix
is present, the reachability graph will be displayed graphically
(see section <a href="#Visual">Visualizing Graphs and Paths</a>). See section <a href="#Depth-and-Breadth">Exhaustive Analysis</a>, for information on
generating the reachability graph.
</p>
<hr size="6">
<a name="Depth-and-Breadth"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Dumpgraph" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Eval" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Exhaustive-Analysis"></a>
<h4 class="subsubsection">2.2.2.6 Exhaustive Analysis</h4>
<a name="index-breadth_002c-query-language"></a>
<a name="index-depth_002c-query-language"></a>
<a name="index-visual_002c-query-language-2"></a>
<table><tr><td> </td><td><pre class="example">statement:
BREADTH [ STATE ]
|
DEPTH [ STATE ]
</pre></td></tr></table>
<p>The commands ‘<samp>breadth</samp>’ and ‘<samp>depth</samp>’ generate all states that
are reachable either from the current state or from a specified state.
This exhaustive search will only be performed if the successors of the
state have not already been generated.
</p>
<table><tr><td> </td><td><pre class="example"><b>$</b>model "dining.pn"
<b>@0$</b>breadth
<b>"dining.pn": 82 states (3..6 bytes), 265 arcs</b>
</pre></td></tr></table>
<p>At the end of the search, the numbers of generated states and events are
reported. The byte range indicates the minimum and maximum lengths of
encoded state representations. This number is affected by modelling
techniques, such as the use of capacity constraints and invariants
(see section <a href="maria_2.html#Places">Place Definition: ‘<samp>place</samp>’</a>), and by not folding places unnecessarily. For this
particular model (see section <a href="maria_8.html#Dining">Dining Philosophers (‘<tt>dining.pn</tt>’)</a>), the maximum length of encoded states
can be reduced from 6 to 4 bytes by splitting the place that holds pairs
of philosophers and their states (thinking, hungry, eating) to three
places, holding a set of those philosophers that are in the state, and
by defining an invariant initialisation expression for the "thinking"
place.
</p>
<p>The ‘<samp>breadth</samp>’ and ‘<samp>depth</samp>’ commands can be also used in
purely state-based safety verification (command-line options
‘<samp>-L</samp>’, ‘<samp>-M</samp>’ and ‘<samp>-P</samp>’), without generating a reachability
graph. If either command is given a safety LTL formula as an
argument, the model contained in the file will be verified against the
property. When the command is preceded by a ‘<samp>visual</samp>’ keyword,
any path that violates the formula will be displayed graphically
(see section <a href="#Visual">Visualizing Graphs and Paths</a>).
</p>
<table><tr><td> </td><td><pre class="example">statement:
[ VISUAL ] BREADTH formula
|
[ VISUAL ] DEPTH formula
</pre></td></tr></table>
<hr size="6">
<a name="Eval"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Depth-and-Breadth" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Show" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Evaluating-Expressions-and-Formulae"></a>
<h4 class="subsubsection">2.2.2.7 Evaluating Expressions and Formulae</h4>
<a name="index-expressions_002c-evaluating"></a>
<a name="index-model-checking"></a>
<a name="index-visual_002c-query-language-3"></a>
<a name="index-eval_002c-query-language"></a>
<table><tr><td> </td><td><pre class="example">statement:
[ VISUAL ] [ EVAL ] [ STATE ] formula
</pre></td></tr></table>
<p>Expressions and formulae can be evaluated either in the current state or
in a given state.
</p>
<table><tr><td> </td><td><pre class="example"><b>@0$</b>place fork
<b>fork:</b>
<b> 1,2,3,4,5</b>
</pre><pre class="example"><b>@0$</b>eval @4 place fork
<b>fork:</b>
<b> 1,2,3,5</b>
</pre></td></tr></table>
<p>When the ‘<samp>visual</samp>’ keyword is present and a temporal formula is
being evaluated, a path violating the formula is displayed graphically
(see section <a href="#Visual">Visualizing Graphs and Paths</a>).
</p>
<hr size="6">
<a name="Show"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Eval" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Hide" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Displaying-Markings"></a>
<h4 class="subsubsection">2.2.2.8 Displaying Markings</h4>
<a name="index-visual_002c-query-language-4"></a>
<a name="index-show_002c-query-language"></a>
<p>With the ‘<samp>show</samp>’ command it is possible to view the marking of a
node in the reachability graph. When a node is not specified, the
current node will be shown.
</p>
<p>The command can also be used to view the nodes in a strongly connected
component (see section <a href="#Strong">Strongly Connected Components</a>). It is possible to specify a Boolean
condition to select a subset of the states in the strongly connected
component to be displayed.
</p>
<table><tr><td> </td><td><pre class="example">statement:
[ VISUAL ] SHOW [ STATE ]
|
[ VISUAL ] [ SHOW ] COMP [ expr ]
|
[ VISUAL ] SHOW STATE STATE ( STATE )*
</pre></td></tr></table>
<p>When the keyword ‘<samp>show</samp>’ is followed by a sequence of at least two
state numbers, Maria displays the sequence of states in the same way as
the ‘<samp>path</samp>’ command does (see section <a href="#Path">Shortest Paths</a>). This command is most
useful with the ‘<samp>visual</samp>’ prefix, since it can be used for
visualizing a previously reported path.
</p>
<table><tr><td> </td><td><pre class="example"><b>@0$</b>show @4
<b>@4:state (</b>
<b> fork:</b>
<b> 1,2,3,5</b>
<b> state:</b>
<b> {1,thinking},{2,thinking},{3,thinking},{5,thinking},{4,hungry}</b>
<b>)</b>
<b>4 predecessors</b>
<b>5 successors</b>
</pre></td></tr></table>
<hr size="6">
<a name="Hide"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Show" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Subnet" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Excluding-Places-from-Displayed-Markings"></a>
<h4 class="subsubsection">2.2.2.9 Excluding Places from Displayed Markings</h4>
<a name="index-hide_002c-query-language"></a>
<p>Petri net models often contain a large number of places whose contents
are of less significance when investigating a particular property of the
model. The ‘<samp>hide</samp>’ command controls which places are displayed by
the ‘<samp>show</samp>’ command (see section <a href="#Show">Displaying Markings</a>) and in the graphical interface
(see section <a href="#Visual">Visualizing Graphs and Paths</a>).
</p>
<table><tr><td> </td><td><pre class="example">statement:
HIDE [ '!' ] [ [ PLACE ] name ( ',' [ PLACE ] name )* ]
</pre></td></tr></table>
<p>When followed by an exclamation point, the command selects places to be
shown (instead of to be hidden). An empty list of place names selects
all places. Typically, one can issue the command ‘<samp>hide</samp>’ followed
by ‘<samp>hide ! <var>placename</var></samp>’ for each place to be shown.
</p>
<hr size="6">
<a name="Subnet"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Hide" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Succ" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Selecting-the-Active-Subnet"></a>
<h4 class="subsubsection">2.2.2.10 Selecting the Active Subnet</h4>
<a name="index-subnet_002c-query-language"></a>
<a name="index-modules-2"></a>
<p>When the model contains subnets (see section <a href="#Subnet">Selecting the Active Subnet</a>) and Maria has been
told to generate a reachability graph and apply modular analysis
(see section <a href="#Invoking-Maria">Invoking Maria</a>), the ‘<samp>subnet</samp>’ command can be used for
navigating in the state spaces of the modules.
</p>
<p>The ‘<samp>subnet</samp>’ command can be used for navigating in the hierarchy
tree in a similar way as the ‘<samp>cd</samp>’ command navigates in the
directory tree. It takes a sequence of subnet identifiers separated
by slashes. The string ‘<samp>..</samp>’ denotes the parent net.
</p>
<p>When invoked without parameters, ‘<samp>subnet</samp>’ selects the root net,
which represents the whole system. If the parameter string starts
with a slash, the tree is selected relative to the root net.
Otherwise, it is selected relative to the currently selected net.
</p>
<p>Nets that have been given a name (see section <a href="#Subnet">Selecting the Active Subnet</a>) can be referred to
by that name. All nets can be referred to by their index number in
the parent net. The subnets are numbered starting from zero.
</p>
<table><tr><td> </td><td><pre class="example">statement:
SUBNET [ [ netid ] ( '/'+ netid )* '/'* ]
</pre><pre class="example">netid: '..' | name | number
</pre></td></tr></table>
<hr size="6">
<a name="Succ"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Subnet" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Pred" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Listing-Successor-Nodes"></a>
<h4 class="subsubsection">2.2.2.11 Listing Successor Nodes</h4>
<a name="index-visual_002c-query-language-5"></a>
<a name="index-succ_002c-query-language"></a>
<a name="index-simulating"></a>
<p>The ‘<samp>succ</samp>’ command lists all successors of a state, or possible
events in the state. If no successors have been generated for the
state, they will be generated on demand. This makes Maria suitable for
simulating or debugging a Petri Net model without generating the
complete reachability graph: to create the interesting part of the
reachability graph, one can keep listing the successors of the states he
is interested in.
</p>
<p>The command can also be used to view the successors of a strongly
connected component (see section <a href="#Strong">Strongly Connected Components</a>).
</p>
<table><tr><td> </td><td><pre class="example">statement:
[ VISUAL ] SUCC [ '!' ] [ STATE ]
|
[ VISUAL ] SUCC COMP
</pre></td></tr></table>
<p>When the ‘<samp>visual</samp>’ keyword is present, the successor states or
components are displayed graphically (see section <a href="#Visual">Visualizing Graphs and Paths</a>).
</p>
<p>When the ‘<samp>succ</samp>’ keyword is followed by an exclamation point
(‘<samp>!</samp>’), Maria will follow the chain of successor states until a
state with several successors is encountered.
</p>
<table><tr><td> </td><td><pre class="example"><b>@0$</b>succ
<b>transition left->@1</b>
<b><</b>
<b> p:1</b>
<b>></b>
</pre><pre class="example"><b>transition left->@2</b>
<b><</b>
<b> p:2</b>
<b>></b>
</pre><pre class="example"><b>transition left->@3</b>
<b><</b>
<b> p:3</b>
<b>></b>
</pre><pre class="example"><b>transition left->@4</b>
<b><</b>
<b> p:4</b>
<b>></b>
</pre><pre class="example"><b>transition left->@5</b>
<b><</b>
<b> p:5</b>
<b>></b>
</pre></td></tr></table>
<hr size="6">
<a name="Pred"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Succ" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Go" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Listing-Predecessor-Nodes"></a>
<h4 class="subsubsection">2.2.2.12 Listing Predecessor Nodes</h4>
<a name="index-visual_002c-query-language-6"></a>
<a name="index-pred_002c-query-language"></a>
<p>The ‘<samp>pred</samp>’ command lists all the generated predecessors of a state,
or all events leading to the state.
</p>
<p>The command can also be used to view the predecessors of a strongly
connected component (see section <a href="#Strong">Strongly Connected Components</a>).
</p>
<table><tr><td> </td><td><pre class="example">statement:
[ VISUAL ] PRED [ '!' ] [ STATE ]
|
[ VISUAL ] PRED COMP
</pre></td></tr></table>
<p>When the ‘<samp>visual</samp>’ keyword is present, the predecessor states or
components are displayed graphically (see section <a href="#Visual">Visualizing Graphs and Paths</a>).
</p>
<p>When the ‘<samp>pred</samp>’ keyword is followed by an exclamation point
(‘<samp>!</samp>’), Maria will follow the chain of predecessor states until a
state with several predecessors is encountered.
</p>
<table><tr><td> </td><td><pre class="example"><b>@0$</b>pred
<b>transition finish<-@20</b>
<b><</b>
<b> p:5</b>
<b>></b>
</pre><pre class="example"><b>transition finish<-@18</b>
<b><</b>
<b> p:4</b>
<b>></b>
</pre><pre class="example"><b>transition finish<-@15</b>
<b><</b>
<b> p:3</b>
<b>></b>
</pre><pre class="example"><b>transition finish<-@11</b>
<b><</b>
<b> p:2</b>
<b>></b>
</pre><pre class="example"><b>transition finish<-@6</b>
<b><</b>
<b> p:1</b>
<b>></b>
</pre></td></tr></table>
<hr size="6">
<a name="Go"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Pred" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Trans" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Moving-in-the-Graph"></a>
<h4 class="subsubsection">2.2.2.13 Moving in the Graph</h4>
<a name="index-go_002c-query-language"></a>
<p>Moving from a state to another is as simple as entering the state
number. To make scripts more readable, you may also use the ‘<samp>go</samp>’
keyword.
</p>
<table><tr><td> </td><td><pre class="example">statement:
[ GO ] STATE
</pre></td></tr></table>
<table><tr><td> </td><td><pre class="example"><b>@0$</b>@4
<b>@4$</b>go @0
<b>@0$</b>
</pre></td></tr></table>
<hr size="6">
<a name="Trans"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Go" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Function" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Anonymous-Transitions"></a>
<h4 class="subsubsection">2.2.2.14 Anonymous Transitions</h4>
<a name="index-trans_002c-query-language"></a>
<p>Sometimes, when modelling a complex system, it may be useful to
specify a different initial state as a starting point for the
analysis. For instance, one might want to slightly modify the marking
of an erroneous state to see how the analysis would proceed from
there.
</p>
<p>In Maria, new states can be computed by entering an anonymous
transition that will be evaluated in a specified state, or in the
current state if no state is specified. No arcs will be added to the
reachability graph. The generated states will be displayed either
textually or graphically.
</p>
<table><tr><td> </td><td><pre class="example">statement:
[ VISUAL ] [ STATE ] TRANS atrans*
</pre><pre class="example">atrans:
'{' [ avar_expr ( delim avar_expr )* [ delim ] ] '}'
|
IN trans_places
|
OUT trans_places
|
GATE expr ( ',' expr )*
</pre><pre class="example">avar_expr:
typereference name
|
typereference name '!' [ '(' expr ')' ]
</pre></td></tr></table>
<table><tr><td> </td><td><pre class="example"><b>@0$</b>trans in { place fork: 1 } out { place fork: 2 }
<b>@82:unprocessed state (</b>
<b> fork:</b>
<b> 2#2,3,4,5</b>
<b> state:</b>
<b> {1,thinking},{2,thinking},{3,thinking},{4,thinking},{5,thinking}</b>
<b>)</b>
<b>@0$</b>
</pre></td></tr></table>
<hr size="6">
<a name="Function"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Trans" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Strong" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Defining-Functions"></a>
<h4 class="subsubsection">2.2.2.15 Defining Functions</h4>
<a name="index-functions_002c-defining-1"></a>
<a name="index-function_002c-query-language"></a>
<p>All the functions defined in the Petri Net are available in the query
tool. It is also possible to define additional functions by using the
‘<samp>function</samp>’ keyword.
</p>
<table><tr><td> </td><td><pre class="example">statement:
FUNCTION function
</pre></td></tr></table>
<table><tr><td> </td><td><pre class="example"><b>@0$</b>function bool assert (bool f) f || fatal
<b>@0$</b>assert (false);
<b><fatalExpression:</b>
<b> fatal</b>
<b>></b>
</pre></td></tr></table>
<p>If there are many function definitions, it is advisable to write them in
a Maria command file, e.g. ‘<tt>dining</tt>’:
</p>
<table><tr><td> </td><td><pre class="example">#!<var>/usr/local/bin/maria</var>
graph dining;
function bool assert (bool f) f || fatal;
</pre></td></tr></table>
<p>The definitions can be loaded in at least three different ways:
</p>
<table><tr><td> </td><td><pre class="example"><b>$</b>maria dining
<b>@0$</b>exit
</pre><pre class="example"><b>$</b>./dining #<span class="roman">the script must be executable</span>
<b>@0$</b>exit
</pre><pre class="example"><b>$</b>maria
<b>$</b>#include "dining"
</pre></td></tr></table>
<hr size="6">
<a name="Strong"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Function" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Path" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Strongly-Connected-Components"></a>
<h4 class="subsubsection">2.2.2.16 Strongly Connected Components</h4>
<a name="index-visual_002c-query-language-7"></a>
<a name="index-strong_002c-query-language"></a>
<a name="index-terminal_002c-query-language"></a>
<a name="index-components_002c-query-language"></a>
<a name="index-strongly-connected-components"></a>
<a name="index-trivial-component"></a>
<a name="index-terminal-component"></a>
<p>A <em>strongly connected component</em> of a directed graph (e.g. a
reachability graph) is a set of nodes that are reachable from each other
by following the arcs. If the reachability graph of a model has only
one strongly connected component, it is guaranteed to be free of
deadlocks, since the initial state is reachable from all states.
</p>
<p>A strongly connected component, or a node of a <em>component graph</em>,
may be <em>trivial</em>, meaning that it contains only one node of the
underlying graph. A <em>terminal component</em> does not have any
successors.
</p>
<p>Maria computes the strongly connected components by starting from a
specified state (by default, the current state) and considering a
transitive closure of its generated successors in the reachability
graph. It is possible to limit the transitive closure by specifying a
condition. States for which the condition does not evaluate to
‘<samp>true</samp>’ are ignored by the search algorithm.
</p>
<p>Once the component graph has been generated, it is possible to list all
its non-trivial terminal components, or all components. Also the
‘<samp>show</samp>’, ‘<samp>succ</samp>’ and ‘<samp>prev</samp>’ commands can be used to examine
the component graph. The ‘<samp>visual</samp>’ keyword selects graphical
display (see section <a href="#Visual">Visualizing Graphs and Paths</a>).
</p>
<table><tr><td> </td><td><pre class="example">statement:
STRONG [ STATE ] [ expr ]
|
TERMINAL
|
[ VISUAL ] COMPONENTS
|
</pre><pre class="example"> [ VISUAL ] [ SHOW ] COMP [ expr ]
|
[ VISUAL ] ( SUCC | PRED ) COMP
</pre></td></tr></table>
<table><tr><td> </td><td><pre class="example"><b>@0$</b>strong
<b>dining: 82 states (3..6 bytes), 265 arcs, 2 components, 1
terminal component</b>
<b>@0$</b>@@0
<b>terminal trivial strongly connected component @@0: @71</b>
<b>@0$</b>pred @@0
<b>@@1</b>
</pre></td></tr></table>
<p>Maria deploys Tarjan’s algorithm for computing strongly connected
components. The algorithm was implemented in Prod by Vesa Hirvisalo and
initially ported to Maria by Emil Falck. His port was rewritten by
Marko Mäkelä to optimize memory usage. The implementation requires
two bits for each node in the reachability graph, and one search stack
whose length is limited by the length of the longest cycle or acyclic
path in the generated reachability graph. Everything else is managed in
disk files.
</p>
<hr size="6">
<a name="Path"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Strong" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Misc" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Shortest-Paths"></a>
<h4 class="subsubsection">2.2.2.17 Shortest Paths</h4>
<a name="index-visual_002c-query-language-8"></a>
<a name="index-path_002c-query-language"></a>
<p>The ‘<samp>path</samp>’ command lets one to find out the shortest path between a
specific state and a set of states.
</p>
<table><tr><td> </td><td><pre class="example">statement:
[ VISUAL ] PATH ( STATE | COMP | expr ) [ STATE ] [ ',' expr ]
|
[ VISUAL ] PATH STATE ( COMP | expr ) [ ',' expr ]
</pre></td></tr></table>
<p>The command takes up to three arguments: the target state, the source
state, and an optional condition that all states on the path must
fulfill. If the source state is omitted, the command finds out the
shortest path to the given target state. Either the source or the
target state must be specified; the other end of the path may be
identified with a state formula or with a strongly connected component
number.
</p>
<p>When the ‘<samp>visual</samp>’ keyword is present, the path is displayed
graphically (see section <a href="#Visual">Visualizing Graphs and Paths</a>).
</p>
<table><tr><td> </td><td><pre class="example"><b>@0$</b>path @6
<b>shortest path from @0 to @6 (3 nodes):</b>
</pre><pre class="example"><b>@0:state (</b>
<b> fork:</b>
<b> 1,2,3,4,5</b>
<b> state:</b>
<b> {1,thinking},{2,thinking},{3,thinking},{4,thinking},{5,thinking}</b>
<b>)</b>
<b>5 predecessors</b>
<b>5 successors</b>
</pre><pre class="example"><b>transition left->@2</b>
<b><</b>
<b> p:2</b>
<b>></b>
</pre><pre class="example"><b>@2:state (</b>
<b> fork:</b>
<b> 1,3,4,5</b>
<b> state:</b>
<b> {1,thinking},{3,thinking},{4,thinking},{5,thinking},{2,hungry}</b>
<b>)</b>
<b>4 predecessors</b>
<b>5 successors</b>
</pre><pre class="example"><b>transition left->@6</b>
<b><</b>
<b> p:1</b>
<b>></b>
</pre><pre class="example"><b>@6:state (</b>
<b> fork:</b>
<b> 3,4,5</b>
<b> state:</b>
<b> {3,thinking},{4,thinking},{5,thinking},{1,hungry},{2,hungry}</b>
<b>)</b>
<b>4 predecessors</b>
<b>4 successors</b>
</pre></td></tr></table>
<p>A third variant of the ‘<samp>path</samp>’ command finds the shortest path from
the current state to a loop. In order to avoid an ambiguity in the
grammar, the loop must consist of at least three states.
</p>
<table><tr><td> </td><td><pre class="example">statement:
[ VISUAL ] PATH STATE STATE STATE ( STATE )* [ ',' expr ]
</pre></td></tr></table>
<p>Maria does not check whether the given states really form a loop; it
just finds the shortest path to any of the specified states so that the
optional condition holds in all states along the path. When the path
enters a state that is not the first (and last) state specified, the
loop is shifted. The result is an acyclic path leading to a cycle,
resembling the shape of the number 6.
</p>
<hr size="6">
<a name="Misc"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Path" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Exit" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Miscellanous-Commands"></a>
<h4 class="subsubsection">2.2.2.18 Miscellanous Commands</h4>
<a name="index-help_002c-query-language"></a>
<a name="index-stats_002c-query-language"></a>
<a name="index-time_002c-query-language"></a>
<a name="index-cd_002c-query-language"></a>
<a name="index-translator_002c-query-language"></a>
<a name="index-compiledir_002c-query-language"></a>
<a name="index-log_002c-query-language"></a>
<a name="index-prompt_002c-query-language"></a>
<p>The ‘<samp>help</samp>’ command displays a short list of all commands. The
‘<samp>stats</samp>’ command displays some statistical information of the graph
being analyzed. The ‘<samp>time</samp>’ command displays timing statistics
since the last invocation of the ‘<samp>time</samp>’ command, or since the time
when the analyzer was started.
</p>
<p>The ‘<samp>cd</samp>’ command can be used to switch the current
directory. Without a parameter, it tries to switch to the directory the
environment variable <code>HOME</code> expands to. The ‘<samp>translator</samp>’
command is used to specify the program for translating temporal logic
formulae into property automata. When the command is invoked without
arguments, the verification of temporal formulae is disabled.
</p>
<p>In order for the ‘<samp>compiledir</samp>’ command to work, Maria must have been
compiled with support for compiled expressions enabled
(see section <a href="maria_7.html#Compiling">Compiling Maria</a>). This command specifies the directory that will be
used for generating executable code from the model. Invoking the
command without arguments disables the code generator.
</p>
<p>The ‘<samp>log</samp>’ command allows the textual output of query language
commands to be redirected to a file, or to the standard error stream
when no file name is specified to the command.
</p>
<p>The ‘<samp>prompt</samp>’ command may be useful when Maria is executed as a
subprocess. When the command is invoked with a non-null character
constant argument, this character will be echoed on its own line
before the command prompt is shown. The plain ‘<samp>prompt</samp>’ command
disables this feature again.
</p>
<table><tr><td> </td><td><pre class="example"> HELP
|
</pre><pre class="example"> STATS
|
</pre><pre class="example"> TIME
|
</pre><pre class="example"> CD [ name ]
|
</pre><pre class="example"> TRANSLATOR [ name ]
|
</pre><pre class="example"> COMPILEDIR [ name ]
|
</pre><pre class="example"> LOG [ name ]
|
</pre><pre class="example"> PROMPT [ 'c' ]
</pre></td></tr></table>
<table><tr><td> </td><td><pre class="example"><b>@0$</b>stats
<b>dining: 82 states (3..4 bytes), 265 arcs</b>
</pre></td></tr></table>
<hr size="6">
<a name="Exit"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Misc" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Quirks" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Language" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Exiting"></a>
<h4 class="subsubsection">2.2.2.19 Exiting</h4>
<a name="index-exit_002c-query-language"></a>
<p>The query tool can be exited either by issuing the command ‘<samp>exit</samp>’
or by typing the end-of-file character <kbd>EOF</kbd> at the command prompt.
</p>
<hr size="6">
<a name="Quirks"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Exit" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Separating-Statements" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Maria-Shell" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Some-Quirks-with-the-Query-Language"></a>
<h3 class="subsection">2.2.3 Some Quirks with the Query Language</h3>
<p>Due to the way the query language and the preprocessor
(see section <a href="maria_2.html#Preprocessor">Preprocessor Directives</a>) have been implemented, there are some things that
are not obvious for the novice user.
</p>
<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Separating-Statements">2.2.3.1 Separating Statements</a></td><td> </td><td align="left" valign="top"> Why is a semicolon mandatory here?
</td></tr>
<tr><td align="left" valign="top"><a href="#Conditional-Processing">2.2.3.2 Conditional Processing in the Editor</a></td><td> </td><td align="left" valign="top"> Using #ifdef on the command line
</td></tr>
</table>
<hr size="6">
<a name="Separating-Statements"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Quirks" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Conditional-Processing" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Quirks" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Separating-Statements-1"></a>
<h4 class="subsubsection">2.2.3.1 Separating Statements</h4>
<p>Maria uses a script language in which statements are separated by
semicolons (‘<samp>;</samp>’). The separator is optional at the end of input.
In the interactive mode, every logical line is parsed separately and
semicolons are only required when issuing multiple commands on one
command line. In script files, semicolons are mandatory between the
statements. Consider the following example:
</p>
<table><tr><td> </td><td><pre class="example">#!<var>/usr/local/bin/maria</var>
graph dining;
function bool eval () false;
eval;
eval
</pre></td></tr></table>
<p>This example will evaluate the function twice. If the semicolon was
omitted, the function would be evaluated only once, since ‘<samp>eval</samp>’
would be treated as a keyword in that case.
</p>
<hr size="6">
<a name="Conditional-Processing"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Separating-Statements" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Visual" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Quirks" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Conditional-Processing-in-the-Editor"></a>
<h4 class="subsubsection">2.2.3.2 Conditional Processing in the Editor</h4>
<a name="index-conditional-processing_002c-interactively"></a>
<p>The line editor of Maria performs simple lexical analysis to find out
whether the line entered is complete. For instance, if the line
contains an unbalanced amount of quotes, a continuation prompt will be
presented and further lines will be read until all quotes and multi-line
comments are balanced or the entry is aborted by typing <kbd>EOF</kbd> at the
beginning of a continuation line.
</p>
<p>However, preprocessor directives for conditional processing are not
detected by the command line interpreter. In case you want to enter
conditional statements (which must span several physical lines)
interactively, you must enter the physical lines as one logical line by
quoting all newline characters but the last one. This can be achieved
on many systems by typing <kbd>C-v C-j</kbd>.
</p>
<hr size="6">
<a name="Visual"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Conditional-Processing" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#GraphViz" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Maria-Shell" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Visualizing-Graphs-and-Paths"></a>
<h3 class="subsection">2.2.4 Visualizing Graphs and Paths</h3>
<a name="index-visual_002c-query-language-9"></a>
<p>Many commands in the query language can be preceded by the ‘<samp>visual</samp>’
keyword. When this keyword is present, the results of the command will
be displayed in a separate visualization process. The visual variant
often displays more information, such as edge attributes (transition
names and valuations) in displayed paths.
</p>
<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#GraphViz">2.2.4.1 GraphViz, the Graph Visualizer</a></td><td> </td><td align="left" valign="top"> The interface to the graph visualizer
</td></tr>
<tr><td align="left" valign="top"><a href="#Visual-Caveats">2.2.4.2 Known Bugs in the Visualizer</a></td><td> </td><td align="left" valign="top"> Exceptional situations in visualization
</td></tr>
</table>
<hr size="6">
<a name="GraphViz"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Visual" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Visual-Caveats" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Visual" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="GraphViz_002c-the-Graph-Visualizer"></a>
<h4 class="subsubsection">2.2.4.1 GraphViz, the Graph Visualizer</h4>
<a name="index-GraphViz"></a>
<a name="index-printing"></a>
<p>In order for this option to work, a software package for drawing graphs
called Graphviz (<a href="http://www.graphviz.org">http://www.graphviz.org</a>) must be installed. The
‘<tt>lefty</tt>’ command, belonging to the package, must be in the search
path, and the script ‘<tt>dotty.lefty</tt>’ must be located either in the
default ‘<tt>lefty</tt>’ search path or in a directory specified in
<code>LEFTYPATH</code>. Also, the visualization script
‘<tt><var>progname</var>-vis</tt>’ must be found in the search path, where
‘<tt><var>progname</var></tt>’ is the name used to invoke the analyzer.
</p>
<p>On the Microsoft Windows platform, Maria does not invoke GraphViz as a
subprocess. Instead, it writes the visualization data to the file
‘<tt>maria-vis.out</tt>’ in the current directory. This file must be
slightly edited before feeding it to the ‘<tt>dotty</tt>’ or ‘<tt>dot</tt>’
programs of GraphViz.
</p>
<p>The visualization program reacts to some keyboard and mouse commands.
Pressing the left or middle mouse button while the mouse pointer is
located on a graph node requests for the successors or predecessors of
the node to be generated. Holding down the right mouse button brings up
a menu whose contents depends on whether the mouse pointer is located
above a node, an edge or somewhere else in the graph. There exist
keyboard short-cuts for most menu entries.
</p>
<p>The visualization program communicates fully asynchronously with Maria
via its standard input and output. It reads commands and graph
descriptions from standard input and writes Maria commands to standard
output. Maria is ready to read and execute these commands whenever it
is sitting in the command prompt waiting for input.
</p>
<p>Maria uses two commands of the visualization program. It issues the
‘<samp>new();</samp>’ command followed by a graph description whenever a query
language command is preprended with a ‘<samp>visual</samp>’ keyword. This
command causes a new graph to be displayed. The ‘<samp>add();</samp>’ command
is issued whenever a query language command is prepended with several
‘<samp>visual</samp>’ keywords. This command causes the visualization program
to merge the immediately following graph description with the last graph
the user has interacted with. The visualization program always issues
query language commands prepended with ‘<samp>visual visual</samp>’, causing the
currently displayed graph to be extended.
</p>
<p>If you want to access the visualization commands generated by Maria, you
can rename the ‘<tt>maria-vis</tt>’ script and replace it with something
like the following script:
</p>
<table><tr><td> </td><td><pre class="example">#!/bin/sh
tee <var>/tmp/maria-vis.out</var> | exec <var>maria-vis-orig</var> "$@"
</pre></td></tr></table>
<p>In order to print a visualized graph, you can save it to a file by
selecting a command in the graphical user interface, and then input this
file to the ‘<tt>dot</tt>’ command. Alternatively, you can use a script
like the above one and extract the graph descriptions from the
intercepted log file. As the ‘<tt>dot</tt>’ command does not directly
support the DIN A4 paper size, you may want to try out one of the
following command lines:
</p>
<table><tr><td> </td><td><pre class="example">dot -Gsize=11.69,8.26 -Gcenter=1 -Gmargin=0 -Grotate=90 -Tps
dot -Gsize=8.26,11.69 -Gcenter=1 -Gmargin=0 -Tps
</pre></td></tr></table>
<p>The former line is for horizontal layouts and the latter is for vertical
layouts. You may want to add ‘<samp>-Grankdir=LR</samp>’ to force left-to-right
layouting of the graph instead of the default top-to-bottom. The
attributes in the graph file override the command line switches.
</p>
<p>Both command lines act as filters, reading the graph description from
standard input and writing the Postscript code to standard output. The
Postscript can be printed directly as such, or embedded in a document,
since it follows the Encapsulated Postscript conventions.
</p>
<hr size="6">
<a name="Visual-Caveats"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#GraphViz" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Emacs" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Visual" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Known-Bugs-in-the-Visualizer"></a>
<h4 class="subsubsection">2.2.4.2 Known Bugs in the Visualizer</h4>
<p>Graphical user interfaces are more challenging to program than plain
textual programs. We have avoided most of the problems by choosing an
external tool that lays out directed graphs. The GraphViz developer
team has been very responsive and nice towards us, even though it has
limited resources.
</p>
<p>Two bugs that may not be fixed soon concern labels in the graph. Some
GraphViz utilities fail if labels are longer than about one thousand
characters. You can use the ‘<samp>hide</samp>’ command (see section <a href="#Hide">Excluding Places from Displayed Markings</a>) to
shorten node labels. Also backslash characters in labels may be handled
incorrectly.
</p>
<p>There are also some known bugs in Maria. Presently, Maria identifies
paths only by state numbers. When a path is displayed graphically,
Maria displays all transitions between each neighboring state along the
path.
</p>
<p>This treatment of transitions may be confusing especially when
displaying counterexample paths (see section <a href="maria_4.html#Liveness">Checking Liveness Properties</a>), since Maria omits
the property automaton states from the counterexample. Effectively, it
projects the product of the reachability graph and the property
automaton on the reachability graph. If there are several enabled
actions between two states, or if fairness constraints are present, the
presented counterexample path may contain extraneous transitions.
</p>
<hr size="6">
<a name="Emacs"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Visual-Caveats" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#pn_002dmode" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Analysis" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Editing-Petri-Nets-with-GNU-Emacs"></a>
<h2 class="section">2.3 Editing Petri Nets with GNU Emacs</h2>
<a name="index-Emacs"></a>
<p>We recommend that you use GNU Emacs for editing Petri Net models.
There is an Emacs major mode for editing Maria Petri Nets. Its main
features are context-sensitive indentation and syntax highlighting. If
you are not familiar with these features of Emacs, it is recommended
that you read the Emacs tutorial (press <kbd>C-h t</kbd>, that is, first hold
down the <kbd>Control</kbd> key, press <kbd>h</kbd>, then release <kbd>Control</kbd>
and press <kbd>t</kbd>) and learn about these features from the on-line help
system of Emacs e.g. with the commands <kbd>C-h i</kbd> (<kbd>M-x info</kbd>)
and <kbd>C-h a</kbd> (<kbd>M-x apropos-command</kbd>).
</p>
<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#pn_002dmode">2.3.1 Installing the Petri Net mode</a></td><td> </td><td align="left" valign="top"></td></tr>
<tr><td align="left" valign="top"><a href="#Highlighting">2.3.2 Syntax Highlighting</a></td><td> </td><td align="left" valign="top"> Syntax highlighting
</td></tr>
<tr><td align="left" valign="top"><a href="#Fine_002dTuning">2.3.3 Customizing Emacs</a></td><td> </td><td align="left" valign="top"> Other things to customize in Emacs
</td></tr>
</table>
<hr size="6">
<a name="pn_002dmode"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Emacs" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Highlighting" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Emacs" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Installing-the-Petri-Net-mode"></a>
<h3 class="subsection">2.3.1 Installing the Petri Net mode</h3>
<a name="index-Petri-Net-mode"></a>
<a name="index-indentation"></a>
<a name="index-syntax-highlighting"></a>
<p>The Petri Net mode ‘<samp>pn-mode</samp>’ has been written for GNU Emacs,
versions 20.3 and 21. It does not work in version 19.34, which lacks
‘<samp>cc-mode</samp>’ and some features of ‘<samp>font-lock-mode</samp>’ the Petri
Net mode requires.
</p>
<p>Installing the Petri Net mode is simple. Just add the name of the
directory containing ‘<tt>pn-mode.el</tt>’ to <var>load-path</var> and do
‘<samp>(require 'pn-mode)</samp>’. To do this, you can add e.g. the following
lines to your ‘<tt>.emacs</tt>’ file.
</p>
<table><tr><td> </td><td><pre class="lisp">(cond ((>= emacs-major-version 20)
(let ((pn-lisp-dir (expand-file-name "<var>~/elisp</var>")))
(cond ((file-readable-p pn-lisp-dir)
(add-to-list 'load-path pn-lisp-dir))
(require 'pn-mode)
(setq pn-font-lock-extra-types
'("token" "\\sw+_t")))))))
</pre></td></tr></table>
<p>In this example, we also set the variable <var>pn-font-lock-extra-types</var>
so that the word ‘<samp>token</samp>’ and all words ending in ‘<samp>_t</samp>’ will be
treated as type names.
</p>
<hr size="6">
<a name="Highlighting"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#pn_002dmode" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Fine_002dTuning" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Emacs" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Syntax-Highlighting"></a>
<h3 class="subsection">2.3.2 Syntax Highlighting</h3>
<a name="index-syntax-highlighting-1"></a>
<p>If you are not familiar with the current syntax highlighting features of
Emacs (‘<samp>font-lock-mode</samp>’), you should read the documentation (using
the Info system and maybe also the <kbd>C-h f</kbd> and <kbd>C-h v</kbd>
commands).
</p>
<p>Adding the following declarations to your ‘<tt>.emacs</tt>’ file will enable
maximum degree of syntax highlighting in all Emacs modes. You may want
to consult the documentation of the variable
<var>font-lock-maximum-decoration</var> if you want to limit the degree of
highlighting in some modes.
</p>
<table><tr><td> </td><td><pre class="lisp">(global-font-lock-mode t)
(setq font-lock-maximum-decoration t)
(turn-on-font-lock)
</pre></td></tr></table>
<hr size="6">
<a name="Fine_002dTuning"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Highlighting" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Emacs" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Customizing-Emacs"></a>
<h3 class="subsection">2.3.3 Customizing Emacs</h3>
<a name="index-Emacs_002c-customizing"></a>
<p>One of the most frequent problems of Emacs newcomers is how to convince
Emacs to use 8-bit characters, as in the character set standardized by
ISO 8859-1, also known as the Latin-1 alphabet. The default 7-bit
character set will suffice for editing Petri Net models. But since this
section is about fine-tuning, here is something for your ‘<tt>.emacs</tt>’
file:
</p>
<table><tr><td> </td><td><pre class="lisp">(standard-display-european t)
(set-input-mode nil nil 'dummy)
(cond ((< emacs-major-version 20)
(require 'iso-syntax))
(t
(setq default-enable-multibyte-characters nil)
(set-language-environment "Latin-1")))
</pre></td></tr></table>
<p>In the following you will see some more definitions from my
‘<tt>.emacs</tt>’ file. Feel free to use any of them. In order for
‘<samp>pn-mode</samp>’ to automatically register the ‘<tt>.pn</tt>’ extension with
‘<samp>speedbar</samp>’, the latter should be loaded first.
</p>
<table><tr><td> </td><td><pre class="lisp">(setq next-line-add-newlines nil);<span class="roman">no accidentally inserted empty lines</span>
(setq make-backup-files nil) ;<span class="roman">unless you like the ‘<samp>~</samp>’ files</span>
(setq mouse-yank-at-point t) ;<span class="roman">for more accurate yanking (pasting)</span>
(setq inhibit-startup-message t) ;<span class="roman">disable the startup message</span>
</pre><pre class="lisp">(if (null window-system)
(menu-bar-mode -1) ;<span class="roman">hide the menu line in text mode</span>
(if (>= emacs-major-version 20)
(speedbar-frame-mode t))) ;<span class="roman">enable speedbar, the navigator</span>
</pre><pre class="lisp">(setq visible-bell t) ;<span class="roman">do not beep---flash instead</span>
(line-number-mode t) ;<span class="roman">show line numbers in the mode line</span>
(column-number-mode t) ;<span class="roman">show column numbers in the mode line</span>
(show-paren-mode t) ;<span class="roman">highlight matching parentheses</span>
(auto-compression-mode t);<span class="roman">transparently (de)compress ‘<samp>.gz</samp>’ files</span>
</pre></td></tr></table>
<hr size="6">
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Analysis" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[<a href="maria_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
<td valign="middle" align="left">[<a href="maria_10.html#Index" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="maria_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<p>
<font size="-1">
This document was generated by <em>root</em> on <em>March 22, 2020</em> using <a href="http://www.nongnu.org/texi2html/"><em>texi2html 1.82</em></a>.
</font>
<br>
</p>
</body>
</html>
AnonSec - 2021 | Recode By D7net