D7net Mini Sh3LL v1
| Current File : //../../usr/share/pam/../base-passwd/../dbus-1/../doc/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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Terminal-Symbols" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria_4.html#Algorithms" 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_6.html#Graph-Files" 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-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 ‘Languages and Context-Free Grammars’ 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 ‘Patterns’ in <cite>The Flex Manual</cite>):
</p>
<ol>
<li> Square brackets (‘<samp>[]</samp>’) indicate optional symbols
</li><li> Asterisk (‘<samp>*</samp>’) denotes any amount repetition (0 or more instances)
</li><li> Parentheses (‘<samp>()</samp>’) 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> </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> </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> </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> </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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Net-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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="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> ‘<samp>NUMBER</samp>’</dt>
<dd><p>decimal (‘<samp>[1-9][0-9]*</samp>’), octal (‘<samp>0[0-7]*</samp>’)
or hexadecimal (‘<samp>0x[0-9a-fA-F]+</samp>’)
</p></dd>
<dt> ‘<samp>CHARACTER</samp>’</dt>
<dd><p>‘<samp>'<var>c</var>'</samp>’: <a href="maria_2.html#Character-Constants">Character Constants</a>
</p></dd>
<dt> ‘<samp>STATE</samp>’</dt>
<dd><p>number of a state in the reachability graph:
‘<samp>@[1-9][0-9]*</samp>’, ‘<samp>@0[0-7]*</samp>’ or ‘<samp>@0x[0-9a-fA-F]+</samp>’
</p></dd>
<dt> ‘<samp>COMP</samp>’</dt>
<dd><p>number of a strongly connected component of (part of) the reachability graph
‘<samp>@@[1-9][0-9]*</samp>’, ‘<samp>@@0[0-7]*</samp>’ or ‘<samp>@@0x[0-9a-fA-F]+</samp>’
</p></dd>
<dt> ‘<samp>name</samp>’</dt>
<dd><p>‘<samp>[a-zA-Z_][0-9a-zA-Z_]*|"<var>c</var>*"</samp>’: <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 ‘<samp>PLACE</samp>’ stands for the keyword ‘<samp>place</samp>’.
</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> </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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Type-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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-Net-Description-Language"></a>
<h2 class="section">A.2 The Net Description Language</h2>
<table><tr><td> </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> </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> </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> </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> </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> </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> </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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Constraint-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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="Type"></a>
<h3 class="subsection">A.2.1 Type</h3>
<table><tr><td> </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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Function-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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="Constraint"></a>
<h4 class="subsubsection">A.2.1.1 Constraint</h4>
<table><tr><td> </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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Place-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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="Function-1"></a>
<h3 class="subsection">A.2.2 Function</h3>
<table><tr><td> </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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Transition-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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="Place"></a>
<h3 class="subsection">A.2.3 Place</h3>
<table><tr><td> </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> </td><td align="left" valign="top"> ‘<samp>constraint</samp>’
</td></tr>
<tr><td align="left" valign="top"><a href="#Type-Grammar">A.2.1 Type</a></td><td> </td><td align="left" valign="top"> ‘<samp>typedefinition</samp>’
</td></tr>
<tr><td align="left" valign="top"><a href="#Expression-Grammar">A.4 Formulae and Expressions</a></td><td> </td><td align="left" valign="top"> ‘<samp>marking_list</samp>’
</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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Assertion-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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="Transition"></a>
<h3 class="subsection">A.2.4 Transition</h3>
<table><tr><td> </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> </td><td align="left" valign="top"> ‘<samp>typedefinition</samp>’
</td></tr>
<tr><td align="left" valign="top"><a href="#Function-Grammar">A.2.2 Function</a></td><td> </td><td align="left" valign="top"> ‘<samp>function</samp>’
</td></tr>
<tr><td align="left" valign="top"><a href="#Expression-Grammar">A.4 Formulae and Expressions</a></td><td> </td><td align="left" valign="top"> ‘<samp>expr</samp>’, ‘<samp>marking_list</samp>’
</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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Query-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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="State-Properties"></a>
<h3 class="subsection">A.2.5 State Properties</h3>
<table><tr><td> </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> </td><td align="left" valign="top"> ‘<samp>marking_list</samp>’, ‘<samp>formula</samp>’
</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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Expression-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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-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, ‘<samp>eval eval</samp>’ will try to evaluate the
symbol ‘<samp>eval</samp>’ in the current state.
</p>
<table><tr><td> </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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Literal-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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="Formulae-and-Expressions"></a>
<h2 class="section">A.4 Formulae and Expressions</h2>
<table><tr><td> </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> </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> </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> </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> </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> </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> </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> </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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Function-Call-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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="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> </td><td><pre class="example">formula:
TRUE | FALSE
|
NUMBER
|
CHARACTER
|
UNDEFINED | FATAL
|
'#' typereference
|
'<' typereference | '>' 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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Basic-Formulae-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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="Functions-1"></a>
<h3 class="subsection">A.4.2 Functions</h3>
<table><tr><td> </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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Union-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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="Basic-Formulae"></a>
<h3 class="subsection">A.4.3 Basic Formulae</h3>
<table><tr><td> </td><td><pre class="example">formula:
'(' formula ')'
|
ATOM formula
|
</pre><pre class="example"> formula '<' formula
|
formula '==' formula
|
formula '>' formula
|
formula '>=' formula
|
formula '!=' formula
|
formula '<=' 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 '<<' formula
|
formula '>>' formula
|
formula '&' 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 '&&' formula
|
formula '^^' formula
|
formula '||' formula
|
formula '<=>' formula
|
formula '=>' 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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Iterating-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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="Typecasting-and-Union-Values"></a>
<h3 class="subsection">A.4.4 Typecasting and Union Values</h3>
<table><tr><td> </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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Multi_002dSet-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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="Non_002dDeterminism-and-Quantification"></a>
<h3 class="subsection">A.4.5 Non-Determinism and Quantification</h3>
<table><tr><td> </td><td><pre class="example">formula:
typereference [ name ] '!' [ '(' expr ')' ]
|
typereference name [ '(' expr ')' ] ':' formula
|
typereference name [ '(' expr ')' ] '&&' 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"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Temporal-Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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="Multi_002dSet-Operations"></a>
<h3 class="subsection">A.4.6 Multi-Set Operations</h3>
<table><tr><td> </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"> < </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Grammar" title="Beginning of this chapter or previous chapter"> << </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"> >> </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="Temporal-Logic-1"></a>
<h3 class="subsection">A.4.7 Temporal Logic</h3>
<table><tr><td> </td><td><pre class="example"> '<>' 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 '&&' qual_expr
|
</pre><pre class="example"> qual_expr '^^' qual_expr
|
</pre><pre class="example"> qual_expr '||' qual_expr
|
</pre><pre class="example"> qual_expr '<=>' qual_expr
|
qual_expr '=>' 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"> << </a>]</td>
<td valign="middle" align="left">[<a href="maria_6.html#Graph-Files" 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