Eror Page

D7net Mini Sh3LL v1
OFF | cURL : OFF | WGET : ON | Perl : ON | Python : OFF
Directory (0755) : /libx32/../share/snapd/../locale/ia/../../doc/info/../libroken18-heimdal/../usbmuxd/../liberror-perl/../grub2-common/../libjpeg8/../php7.4-mysql/../gnupg/../python3-apt/../netplan.io/../wget/../libcurl3-gnutls/../libthai-data/../python3-six/../screen/../maria/../libxaw7/../libmnl0/../netplan/../gdisk/../systemd-sysv/../grep/../udisks2/../libacl1/../libxmlb1/../libperl5.30/../automake/../libmpfr6/../libssl1.1/../btrfs-progs/../usbutils/../tcpdump/../libsemanage1/../libdrm2/../gcc/../libselinux1/../bzip2/../mtr-tiny/../iw/../apport/../accountsservice/../bolt/../liblzma5/../finalrd/../libldap-common/../cpp/../tpm-udev/../hostname/../libnuma1/../jsonlint/../ed/../nano/../maria-doc/html/
Home	☍ Command	☍ Upload File	☍Info Server	☍ Buat File	☍ Mass deface	☍ Jumping	☍ Config	☍ Symlink	☍ About
Current File : //libx32/../share/snapd/../locale/ia/../../doc/info/../libroken18-heimdal/../usbmuxd/../liberror-perl/../grub2-common/../libjpeg8/../php7.4-mysql/../gnupg/../python3-apt/../netplan.io/../wget/../libcurl3-gnutls/../libthai-data/../python3-six/../screen/../maria/../libxaw7/../libmnl0/../netplan/../gdisk/../systemd-sysv/../grep/../udisks2/../libacl1/../libxmlb1/../libperl5.30/../automake/../libmpfr6/../libssl1.1/../btrfs-progs/../usbutils/../tcpdump/../libsemanage1/../libdrm2/../gcc/../libselinux1/../bzip2/../mtr-tiny/../iw/../apport/../accountsservice/../bolt/../liblzma5/../finalrd/../libldap-common/../cpp/../tpm-udev/../hostname/../libnuma1/../jsonlint/../ed/../nano/../maria-doc/html/maria_5.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: A. The Grammar</title>

<meta name="description" content="Maria: A. The Grammar">
<meta name="keywords" content="Maria: A. The Grammar">
<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="Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="maria_4.html#Liveness" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Terminal-Symbols" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" title="Beginning of this chapter or previous chapter"> &lt;&lt; </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_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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-Grammar"></a>
<h1 class="appendix">A. The Grammar</h1>
<a name="index-grammar_002c-summary"></a>

<p>This appendix presents the grammar of the Maria languages using a
Bison-like Backus-Naur Form (see <a href="../bison/Language-and-Grammar.html#Language-and-Grammar">(bison)Language and Grammar</a> section &lsquo;Languages and Context-Free Grammars&rsquo; in <cite>The GNU Bison Manual</cite>) with
the following extensions inspired by regular expressions
(see <a href="../flex/Patterns.html#Patterns">(flex)Patterns</a> section &lsquo;Patterns&rsquo; in <cite>The Flex Manual</cite>):
</p>
<ol>
<li> Square brackets (&lsquo;<samp>[]</samp>&rsquo;) indicate optional symbols
</li><li> Asterisk (&lsquo;<samp>*</samp>&rsquo;) denotes any amount repetition (0 or more instances)
</li><li> Parentheses (&lsquo;<samp>()</samp>&rsquo;) are used for grouping grammar symbols
</li></ol>

<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Terminal-Symbols">A.1 Terminal Symbols</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">            Terminal symbols used in the grammars
</td></tr>
<tr><td align="left" valign="top"><a href="#Net-Grammar">A.2 The Net Description Language</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">                 The net description language
</td></tr>
<tr><td align="left" valign="top"><a href="#Query-Grammar">A.3 The Query Language</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">               The query language
</td></tr>
<tr><td align="left" valign="top"><a href="#Expression-Grammar">A.4 Formulae and Expressions</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top"></td></tr>
</table>

<hr size="6">
<a name="Terminal-Symbols"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Net-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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="Terminal-Symbols-1"></a>
<h2 class="section">A.1 Terminal Symbols</h2>

<p>By convention, terminal symbols are written in all-uppercase letters or
as character strings enclosed in single quotation marks, and
non-terminal symbols are written in all-lowercase letters.  The
non-trivial terminal symbols used in the grammar are as follows.
</p>
<dl compact="compact">
<dt> &lsquo;<samp>NUMBER</samp>&rsquo;</dt>
<dd><p>decimal (&lsquo;<samp>[1-9][0-9]*</samp>&rsquo;), octal (&lsquo;<samp>0[0-7]*</samp>&rsquo;)
or hexadecimal (&lsquo;<samp>0x[0-9a-fA-F]+</samp>&rsquo;)
</p></dd>
<dt> &lsquo;<samp>CHARACTER</samp>&rsquo;</dt>
<dd><p>&lsquo;<samp>'<var>c</var>'</samp>&rsquo;: <a href="maria_2.html#Character-Constants">Character Constants</a>
</p></dd>
<dt> &lsquo;<samp>STATE</samp>&rsquo;</dt>
<dd><p>number of a state in the reachability graph:
&lsquo;<samp>@[1-9][0-9]*</samp>&rsquo;, &lsquo;<samp>@0[0-7]*</samp>&rsquo; or &lsquo;<samp>@0x[0-9a-fA-F]+</samp>&rsquo;
</p></dd>
<dt> &lsquo;<samp>COMP</samp>&rsquo;</dt>
<dd><p>number of a strongly connected component of (part of) the reachability graph
&lsquo;<samp>@@[1-9][0-9]*</samp>&rsquo;, &lsquo;<samp>@@0[0-7]*</samp>&rsquo; or &lsquo;<samp>@@0x[0-9a-fA-F]+</samp>&rsquo;
</p></dd>
<dt> &lsquo;<samp>name</samp>&rsquo;</dt>
<dd><p>&lsquo;<samp>[a-zA-Z_][0-9a-zA-Z_]*|&quot;<var>c</var>*&quot;</samp>&rsquo;: <a href="maria_2.html#Identifiers">Identifiers</a>
</p></dd>
</dl>

<p>Reserved words are not listed in the above table.  For instance, the
symbol &lsquo;<samp>PLACE</samp>&rsquo; stands for the keyword &lsquo;<samp>place</samp>&rsquo;.
</p>
<p>In addition, there are a few low-level grammar rules that are almost
like terminal symbols in their nature:
</p><table><tr><td>&nbsp;</td><td><pre class="example">delim:
        ','
        |
        ';'
</pre></td></tr></table>

<hr size="6">
<a name="Net-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Terminal-Symbols" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Type-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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-Net-Description-Language"></a>
<h2 class="section">A.2 The Net Description Language</h2>

<table><tr><td>&nbsp;</td><td><pre class="example">net:
        ( netcomponent ';' )*
</pre><pre class="example">netcomponent:
        type
        |
        function
        |
        place
        |
        transition
        |
        verify
        |
        fairness
        |
        proposition
        |
        subnet
</pre><pre class="example">subnet:
        SUBNET [ name ] '{' net '}'
</pre></td></tr></table>

<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Type-Grammar">A.2.1 Type</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">                Data type definitions
</td></tr>
<tr><td align="left" valign="top"><a href="#Constraint-Grammar">A.2.1.1 Constraint</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">          Constraints of data types
</td></tr>
<tr><td align="left" valign="top"><a href="#Function-Grammar">A.2.2 Function</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">            Function definitions
</td></tr>
<tr><td align="left" valign="top"><a href="#Place-Grammar">A.2.3 Place</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">               Place definitions
</td></tr>
<tr><td align="left" valign="top"><a href="#Transition-Grammar">A.2.4 Transition</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">          Transition definitions
</td></tr>
<tr><td align="left" valign="top"><a href="#Assertion-Grammar">A.2.5 State Properties</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">           State properties
</td></tr>
</table>

<hr size="6">
<a name="Type-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Net-Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Constraint-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Net-Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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="Type"></a>
<h3 class="subsection">A.2.1 Type</h3>

<table><tr><td>&nbsp;</td><td><pre class="example">type:
        TYPEDEF typedefinition name
</pre><pre class="example">typedefinition:
        ENUM '{' enum_item ( delim enum_item )* '}'
        |
        STRUCT '{' [ comp_list ] '}'
        |
        UNION '{' comp_list '}'
        |
        ID '[' number ']'
        |
        typereference
        |
        typedefinition constraint
        |
        typedefinition '[' typedefinition ']'
        |
        typedefinition '[' QUEUE number ']'
        |
        typedefinition '[' STACK number ']'
</pre><pre class="example">typereference:
        name
</pre><pre class="example">enum_item:
        name [ [ '=' ] number ]
</pre><pre class="example">comp_list:
        comp ( delim comp )* [ delim ]
comp:
        typedefinition name
</pre><pre class="example">number:
        expr
</pre></td></tr></table>

<hr size="6">
<a name="Constraint-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Type-Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Function-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Type-Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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="Constraint"></a>
<h4 class="subsubsection">A.2.1.1 Constraint</h4>

<table><tr><td>&nbsp;</td><td><pre class="example">constraint:
        '(' range ( delim range )* ')'
</pre><pre class="example">range:
        value
        |
        '..' value
        |
        value '..' value
        |
        value '..'
</pre><pre class="example">value:
        expr
</pre></td></tr></table>

<hr size="6">
<a name="Function-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Constraint-Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Place-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Net-Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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="Function-1"></a>
<h3 class="subsection">A.2.2 Function</h3>

<table><tr><td>&nbsp;</td><td><pre class="example">function:
        typereference name eq formula
        |
        typereference name '(' param_list ')' formula
</pre><pre class="example">eq:     '=' | '()'
</pre><pre class="example">param_list:
        [ param_list_item ( delim param_list_item )* ]
param_list_item:
        typereference name
</pre></td></tr></table>

<hr size="6">
<a name="Place-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Function-Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Transition-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Net-Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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="Place"></a>
<h3 class="subsection">A.2.3 Place</h3>

<table><tr><td>&nbsp;</td><td><pre class="example">place:
        PLACE name constraint* typedefinition
        [ CONST ] [ ':' marking_list ]
</pre></td></tr></table>

<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Constraint-Grammar">A.2.1.1 Constraint</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">          &lsquo;<samp>constraint</samp>&rsquo;
</td></tr>
<tr><td align="left" valign="top"><a href="#Type-Grammar">A.2.1 Type</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">                &lsquo;<samp>typedefinition</samp>&rsquo;
</td></tr>
<tr><td align="left" valign="top"><a href="#Expression-Grammar">A.4 Formulae and Expressions</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">          &lsquo;<samp>marking_list</samp>&rsquo;
</td></tr>
</table>

<hr size="6">
<a name="Transition-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Place-Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Assertion-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Net-Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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="Transition"></a>
<h3 class="subsection">A.2.4 Transition</h3>

<table><tr><td>&nbsp;</td><td><pre class="example">transition:
        TRANS [ ':' ] name [ '!' ] trans*
</pre><pre class="example">trans:
        '{' [ var_expr ( delim var_expr )* [ delim ] ] '}'
        |
        IN trans_places
        |
        OUT trans_places
        |
        GATE expr ( ',' expr )*
</pre><pre class="example">        |
        HIDE expr
</pre><pre class="example">        |
        STRONGLY_FAIR expr
        |
        WEAKLY_FAIR expr
        |
        ENABLED expr
</pre><pre class="example">        |
        ':' [ TRANS ] name
        |
        NUMBER
</pre><pre class="example">var_expr:
        [ HIDE ] typereference name
        |
        [ HIDE ] typereference name '!' [ '(' expr ')' ]
        |
        function
</pre><pre class="example">trans_places:
        '{' place_marking ( ';' place_marking )* '}'
place_marking:
        [ PLACE ] name ':' marking_list
</pre></td></tr></table>

<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Type-Grammar">A.2.1 Type</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">                &lsquo;<samp>typedefinition</samp>&rsquo;
</td></tr>
<tr><td align="left" valign="top"><a href="#Function-Grammar">A.2.2 Function</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">            &lsquo;<samp>function</samp>&rsquo;
</td></tr>
<tr><td align="left" valign="top"><a href="#Expression-Grammar">A.4 Formulae and Expressions</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">          &lsquo;<samp>expr</samp>&rsquo;, &lsquo;<samp>marking_list</samp>&rsquo;
</td></tr>
</table>

<hr size="6">
<a name="Assertion-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Transition-Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Net-Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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="State-Properties"></a>
<h3 class="subsection">A.2.5 State Properties</h3>

<table><tr><td>&nbsp;</td><td><pre class="example">verify:
        REJECT expr
        |
        DEADLOCK expr
</pre><pre class="example">fairness:
        STRONGLY_FAIR qual_expr ( ',' qual_expr )*
        |
        WEAKLY_FAIR qual_expr ( ',' qual_expr )*
        |
        ENABLED qual_expr ( ',' qual_expr )*
</pre><pre class="example">proposition:
        PROP name ':' expr
</pre></td></tr></table>

<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Expression-Grammar">A.4 Formulae and Expressions</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">          &lsquo;<samp>marking_list</samp>&rsquo;, &lsquo;<samp>formula</samp>&rsquo;
</td></tr>
</table>

<hr size="6">
<a name="Query-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Assertion-Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Expression-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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-1"></a>
<h2 class="section">A.3 The Query Language</h2>
<a name="index-query-language-1"></a>

<p>Keywords of the query language are reserved words only in the beginning
of a statement.  For instance, &lsquo;<samp>eval eval</samp>&rsquo; will try to evaluate the
symbol &lsquo;<samp>eval</samp>&rsquo; in the current state.
</p>
<table><tr><td>&nbsp;</td><td><pre class="example">script:
        [ statement ( ';' statement )* [ ';' ] ]
</pre><pre class="example">statement:
        MODEL name
        |
        GRAPH name
        |
        [ VISUAL ] DUMP
        |
        UNFOLD name
        |
        LSTS [ name ]
        |
        [ VISUAL ] DUMPGRAPH
        |
        ( BREADTH | DEPTH ) [ STATE ]
        |
        [ VISUAL ] ( BREADTH | DEPTH ) formula
        |
</pre><pre class="example">        [ VISUAL ] [ EVAL ] [ STATE ] formula
        |
        [ VISUAL ] SHOW [ STATE ]
        |
        [ VISUAL ] SHOW STATE STATE ( STATE )*
        |
        HIDE [ '!' ] [ [ PLACE ] name ( ',' [ PLACE ] name )* ]
        |
        [ VISUAL ] ( SUCC | PRED ) [ '!' ] [ STATE ]
        |
        [ GO ] STATE
        |
        [ 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><pre class="example">statement:
        STRONG [ STATE ] [expr]
        |
        TERMINAL
        |
        [ VISUAL ] COMPONENTS
        |
        [ VISUAL ] ( SUCC | PRED ) COMP
        |
        [ VISUAL ] [ SHOW ] COMP [ expr ]
        |
</pre><pre class="example">        [ VISUAL ] PATH ( STATE | COMP | expr ) [ STATE ] [ ',' expr ]
        |
        [ VISUAL ] PATH STATE ( COMP | expr ) [ ',' expr ]
        |
        [ VISUAL ] PATH STATE STATE STATE ( STATE )* [ ',' expr ]
</pre><pre class="example">        FUNCTION function
        |
</pre><pre class="example">        STATS
        |
</pre><pre class="example">        TIME
        |
</pre><pre class="example">        CD [ name ]
        |
        TRANSLATOR [ name ]
        |
        COMPILEDIR [ name ]
        |
        LOG [ name ]
        |
</pre><pre class="example">        PROMPT [ 'c' ]
        |
</pre><pre class="example">        HELP
        |
        EXIT
</pre></td></tr></table>

<hr size="6">
<a name="Expression-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Query-Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Literal-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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="Formulae-and-Expressions"></a>
<h2 class="section">A.4 Formulae and Expressions</h2>

<table><tr><td>&nbsp;</td><td><pre class="example">expr:
        formula
</pre><pre class="example">marking:
        formula
marking_list:
        marking ( ',' marking )*
</pre></td></tr></table>

<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Literal-Grammar">A.4.1 Literals</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top"></td></tr>
<tr><td align="left" valign="top"><a href="#Function-Call-Grammar">A.4.2 Functions</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">       Function calls
</td></tr>
<tr><td align="left" valign="top"><a href="#Basic-Formulae-Grammar">A.4.3 Basic Formulae</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">      Syntax for basic formulae
</td></tr>
<tr><td align="left" valign="top"><a href="#Union-Grammar">A.4.4 Typecasting and Union Values</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">               Syntax related with unions and type casting
</td></tr>
<tr><td align="left" valign="top"><a href="#Iterating-Grammar">A.4.5 Non-Determinism and Quantification</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">           Non-determinism and quantification
</td></tr>
<tr><td align="left" valign="top"><a href="#Multi_002dSet-Grammar">A.4.6 Multi-Set Operations</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">           Multi-set operations
</td></tr>
<tr><td align="left" valign="top"><a href="#Temporal-Grammar">A.4.7 Temporal Logic</a></td><td>&nbsp;&nbsp;</td><td align="left" valign="top">            Temporal logic
</td></tr>
</table>

<hr size="6">
<a name="Literal-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Expression-Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Function-Call-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Expression-Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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="Literals-2"></a>
<h3 class="subsection">A.4.1 Literals</h3>
<a name="index-true"></a>
<a name="index-false"></a>
<a name="index-undefined"></a>
<a name="index-fatal"></a>
<a name="index-_0023_002c-unary"></a>
<a name="index-_003c_002c-unary"></a>
<a name="index-_003e_002c-unary"></a>

<table><tr><td>&nbsp;</td><td><pre class="example">formula:
        TRUE | FALSE
        |
        NUMBER
        |
        CHARACTER
        |
        UNDEFINED | FATAL
        |
        '#' typereference
        |
        '&lt;' typereference | '&gt;' typereference
        |
        name
</pre></td></tr></table>

<hr size="6">
<a name="Function-Call-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Literal-Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Basic-Formulae-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Expression-Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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="Functions-1"></a>
<h3 class="subsection">A.4.2 Functions</h3>

<table><tr><td>&nbsp;</td><td><pre class="example">formula:
        name '()'
        |
        name '(' arg_list ')'
arg_list:
        [ formula ( ',' formula )* ]
</pre></td></tr></table>

<hr size="6">
<a name="Basic-Formulae-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Function-Call-Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Union-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Expression-Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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="Basic-Formulae"></a>
<h3 class="subsection">A.4.3 Basic Formulae</h3>

<table><tr><td>&nbsp;</td><td><pre class="example">formula:
        '(' formula ')'
        |
        ATOM formula
        |
</pre><pre class="example">        formula '&lt;' formula
        |
        formula '==' formula
        |
        formula '&gt;' formula
        |
        formula '&gt;=' formula
        |
        formula '!=' formula
        |
        formula '&lt;=' formula
        |
</pre><pre class="example">        '-' formula
        |
        formula '+' formula
        |
        formula '-' formula
        |
        formula '/' formula
        |
        formula '*' formula
        |
        formula '%' formula
        |
</pre><pre class="example">        '|' formula | '+' formula
        |
        '*' formula
        |
        '/' formula | '%' formula
        |
        '~' formula
        |
</pre><pre class="example">        formula '&lt;&lt;' formula
        |
        formula '&gt;&gt;' formula
        |
        formula '&amp;' formula
        |
        formula '^' formula
        |
        formula '|' formula
        |
</pre><pre class="example">        formula '?' formula ( ':' formula )*
        |
</pre><pre class="example">        '{' [ name ':' ] [ expr ] ( ',' [ name ':' ] [ expr ] )* '}'
        |
        formula '.' name
        |
        formula '.' '{' name expr '}'
        |
        formula '[' formula ']'
        |
        formula '.' '{' '[' expr ']' expr '}'
        |
</pre><pre class="example">        '!' formula
        |
        formula '&amp;&amp;' formula
        |
        formula '^^' formula
        |
        formula '||' formula
        |
        formula '&lt;=&gt;' formula
        |
        formula '=&gt;' formula
</pre></td></tr></table>

<hr size="6">
<a name="Union-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Basic-Formulae-Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Iterating-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Expression-Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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="Typecasting-and-Union-Values"></a>
<h3 class="subsection">A.4.4 Typecasting and Union Values</h3>

<table><tr><td>&nbsp;</td><td><pre class="example">formula:
        IS typereference formula
        |
        name '=' formula
        |
        formula IS name
</pre></td></tr></table>

<hr size="6">
<a name="Iterating-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Union-Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Multi_002dSet-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Expression-Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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="Non_002dDeterminism-and-Quantification"></a>
<h3 class="subsection">A.4.5 Non-Determinism and Quantification</h3>

<table><tr><td>&nbsp;</td><td><pre class="example">formula:
        typereference [ name ] '!' [ '(' expr ')' ]
        |
        typereference name [ '(' expr ')' ] ':' formula
        |
        typereference name [ '(' expr ')' ] '&amp;&amp;' formula
        |
        typereference name [ '(' expr ')' ] '||' formula
        |
        '.' name [ name ]
        |
        ':' name [ name ]
</pre></td></tr></table>

<hr size="6">
<a name="Multi_002dSet-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Iterating-Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Temporal-Grammar" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Expression-Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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="Multi_002dSet-Operations"></a>
<h3 class="subsection">A.4.6 Multi-Set Operations</h3>

<table><tr><td>&nbsp;</td><td><pre class="example">formula:
        EMPTY
        |
        '(' marking_list ')'
        |
        formula '#' marking
        |
        PLACE name
        |
</pre><pre class="example">        marking SUBSET marking
        |
        marking INTERSECT marking
        |
        marking MINUS marking
        |
        marking UNION marking
        |
        marking EQUALS marking
        |
</pre><pre class="example">        CARDINALITY marking
        |
        MAX marking
        |
        MIN marking
        |
</pre><pre class="example">        SUBSET name '{' marking_list '}' expr
        |
        MAP name '{' marking_list '}' expr
        |
        MAP name '#' name '{' marking_list '}' marking
</pre></td></tr></table>

<hr size="6">
<a name="Temporal-Grammar"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Multi_002dSet-Grammar" title="Previous section in reading order"> &lt; </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next section in reading order"> &gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="#Expression-Grammar" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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="Temporal-Logic-1"></a>
<h3 class="subsection">A.4.7 Temporal Logic</h3>

<table><tr><td>&nbsp;</td><td><pre class="example">        '&lt;&gt;' formula
        |
        '[]' formula
        |
        '()' formula
        |
        formula UNTIL formula
        |
        formula RELEASE formula
</pre><pre class="example">qual_expr:
        TRANS name [ ':' expr ]
        |
        '(' qual_expr ')'
        |
</pre><pre class="example">        '!' qual_expr
        |
</pre><pre class="example">        qual_expr '&amp;&amp;' qual_expr
        |
</pre><pre class="example">        qual_expr '^^' qual_expr
        |
</pre><pre class="example">        qual_expr '||' qual_expr
        |
</pre><pre class="example">        qual_expr '&lt;=&gt;' qual_expr
        |
        qual_expr '=&gt;' qual_expr
</pre></td></tr></table>

<hr size="6">
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next chapter"> &gt;&gt; </a>]</td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </td>
<td valign="middle" align="left"> &nbsp; </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