D7net Mini Sh3LL v1
| Current File : //libx32/../sbin/../share/doc/usbmuxd/../libip4tc2/../maria-doc/html/maria_4.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: 3. Algorithms used in Maria</title>
<meta name="description" content="Maria: 3. Algorithms used in Maria">
<meta name="keywords" content="Maria: 3. Algorithms used in 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="Algorithms"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="maria_3.html#Fine_002dTuning" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Unification" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="maria_3.html#Analysis" 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_5.html#Grammar" 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="Algorithms-used-in-Maria"></a>
<h1 class="chapter">3. Algorithms used in Maria</h1>
<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Unification">3.1 The Unification Algorithm</a></td><td> </td><td align="left" valign="top"> Finding enabled transition instances
</td></tr>
<tr><td align="left" valign="top"><a href="#Model-Checking">3.2 Model Checking Algorithms</a></td><td> </td><td align="left" valign="top"> Checking temporal properties
</td></tr>
</table>
<hr size="6">
<a name="Unification"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Algorithms" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Unification-Concepts" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Algorithms" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Algorithms" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_5.html#Grammar" 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-Unification-Algorithm"></a>
<h2 class="section">3.1 The Unification Algorithm</h2>
<a name="index-unification"></a>
<p>Enabled transition instances are sought in a process called
<em>unification</em>.
</p>
<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Unification-Concepts">3.1.1 Concepts</a></td><td> </td><td align="left" valign="top"> Concepts related to unification
</td></tr>
<tr><td align="left" valign="top"><a href="#Quantification">3.1.2 Expanding Quantifications</a></td><td> </td><td align="left" valign="top"> Expanding multi-set sums
</td></tr>
<tr><td align="left" valign="top"><a href="#Binding">3.1.3 Matching Concrete and Formal Tokens</a></td><td> </td><td align="left" valign="top"> Matching concrete tokens with formal ones
</td></tr>
<tr><td align="left" valign="top"><a href="#Lvalues">3.1.4 Finding Assignment Candidates</a></td><td> </td><td align="left" valign="top"> Finding assignment candidates
</td></tr>
<tr><td align="left" valign="top"><a href="#Instance-Analysis">3.1.5 Transition Instance Analysis</a></td><td> </td><td align="left" valign="top"> The core of the unification algorithm
</td></tr>
</table>
<hr size="6">
<a name="Unification-Concepts"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Unification" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Quantification" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Algorithms" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Unification" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_5.html#Grammar" 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="Concepts"></a>
<h3 class="subsection">3.1.1 Concepts</h3>
<a name="index-concepts_002c-unification"></a>
<p>There are some concepts related to the unification process that may be
somewhat unclear, even though you know the basics of high level Petri
Nets.
</p>
<dl compact="compact">
<dt> <em>input arc</em></dt>
<dd><p>An arc leading from a place to a transition, labelled with a multi-set
expression evaluating to the tokens that are to be removed from the place
when the transition fires
</p></dd>
<dt> <em>output arc</em></dt>
<dd><p>An arc leading from a transition to a place, labelled with a multi-set
expression evaluating to the tokens that are to be inserted to the place
when the transition fires
</p></dd>
<dt> <em>variable</em></dt>
<dd><p>A named and strictly typed entity that may be assigned a value
</p></dd>
<dt> <em>output variable</em></dt>
<dd><p>A variable occurring only on output arcs of a transition; the value will
be picked non-deterministically at the end of the unification process
</p></dd>
<dt> <em>input variable</em></dt>
<dd><p>A variable occurring on the input arcs of a transition
</p></dd>
<dt> <em>valuation</em></dt>
<dt> <em>binding</em></dt>
<dd><p>A binding of values to variables
</p></dd>
<dt> <em>expression</em></dt>
<dd><p>A formula that evaluates to a value; expressions in net descriptions do
not contain temporal logic operators or other set operations than multi-set
summing
</p></dd>
<dt> <em>arc expression</em></dt>
<dd><p>A multi-set valued expression occurring on an input or output arc
</p></dd>
<dt> <em>gate</em></dt>
<dt> <em>gate expression</em></dt>
<dd><p>A condition for the valuation of the input variables; if omitted, it is
treated as identically true
</p></dd>
<dt> <em>token</em></dt>
<dd><p>an entity having a value; moved between places by the firing of transitions
</p></dd>
<dt> <em>concrete token</em></dt>
<dd><p>a token contained in a place
</p></dd>
<dt> <em>abstract token</em></dt>
<dd><p>an item of an arc expression
</p></dd>
<dt> <em>lvalue</em></dt>
<dd><p>Left-hand-side value of an assignment; a data object (in our case, an
input variable) that is assigned to
</p></dd>
<dt> <em>rvalue</em></dt>
<dd><p>Right-hand-side value of an assignment, evaluating to the value that will
be assigned to the lvalue
</p></dd>
</dl>
<hr size="6">
<a name="Quantification"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Unification-Concepts" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Binding" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Algorithms" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Unification" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_5.html#Grammar" 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="Expanding-Quantifications"></a>
<h3 class="subsection">3.1.2 Expanding Quantifications</h3>
<a name="index-quantification_002c-expanding"></a>
<p>Arc expressions may contain multi-set sums (see section <a href="maria_2.html#Multi_002dSets">Operations on Multi-Sets</a>) or
universal or existential quantification with fixed or variable bounds.
They are expanded at parsing time. Consider the following net
description:
</p>
<table><tr><td> </td><td><pre class="example">place p bool: false, true;
place r bool: 2#(2#false, true);
trans t in {
place p: p;
place r: bool s: (s, bool t (p): s && t);
};
</pre></td></tr></table>
<p>The arc expression is expanded as follows:
</p><table><tr><td> </td><td><pre class="example">trans t in {
place p: p;
place r: false, true, (p?3:0)#false, (p?1:0)#true;
};
</pre></td></tr></table>
<hr size="6">
<a name="Binding"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Quantification" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Lvalues" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Algorithms" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Unification" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_5.html#Grammar" 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="Matching-Concrete-and-Formal-Tokens"></a>
<h3 class="subsection">3.1.3 Matching Concrete and Formal Tokens</h3>
<a name="index-tokens_002c-formal-and-concrete"></a>
<a name="index-assignments"></a>
<p>The Petri Net formalism does not have the concept of assignment as known
in programming languages. Also, expressions may not have any
side-effects. The only way a Petri system can change its state is
through the firing of an enabled transition.
</p>
<p>Assignments in the high level Petri Net formalism are implicit. In
order for a high-level transition to be enabled, its variables must be
bound to suitable values. Values for input variables will be found by
matching concrete tokens in places with abstract ones on input arc
expressions.
</p>
<p>For each abstract token with known multiplicity, all concrete tokens in
the input place that have not been associated with other abstract tokens
will be considered. If the tokens are compatible (given the valuation
generated so far, each component of the abstract token evaluates to the
corresponding component of the concrete token or is undefined), a
quantity of the concrete token will be associated with the abstract
token. For instance, if the place contains ‘<samp>3#true,2#false</samp>’ and
the abstract token is ‘<samp>2#x</samp>’, the unification algorithm will
associate 2 of the 3 ‘<samp>true</samp>’ tokens or all the ‘<samp>false</samp>’ tokens
with the abstract token.
</p>
<p>If the abstract token contains assignment candidates (see section <a href="#Lvalues">Finding Assignment Candidates</a>),
the valuation will be extended. Continuing our example, the variable
‘<samp>x</samp>’ in the abstract token ‘<samp>2#x</samp>’ is an lvalue, and it can be
assigned the corresponding value of the concrete token, in this case
‘<samp>true</samp>’ or ‘<samp>false</samp>’.
</p>
<hr size="6">
<a name="Lvalues"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Binding" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Instance-Analysis" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Algorithms" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Unification" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_5.html#Grammar" 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="Finding-Assignment-Candidates"></a>
<h3 class="subsection">3.1.4 Finding Assignment Candidates</h3>
<a name="index-lvalue"></a>
<a name="index-assignments-1"></a>
<p>Assignment candidates, or left-hand-side values of assignments
(<em>lvalues</em>), are expressions that can be assigned to. In Maria,
they are variables or array variables indexed by a known index. Lvalues
must occur either as such (an abstract token is an lvalue) or in
components of structured expressions.
</p>
<p>For example, the abstract token ‘<samp>42#{x,{y+1,z},+t}</samp>’ has two
lvalues, the variables ‘<samp>x</samp>’ and ‘<samp>z</samp>’. The abstract token
‘<samp>x#y</samp>’ has one lvalue, ‘<samp>y</samp>’; the token cannot be matched with a
concrete one until the value of ‘<samp>x</samp>’ is known. The token ‘<samp>|x</samp>’
does not have any lvalues.
</p>
<hr size="6">
<a name="Instance-Analysis"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Lvalues" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Model-Checking" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Algorithms" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Unification" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_5.html#Grammar" 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-Instance-Analysis"></a>
<h3 class="subsection">3.1.5 Transition Instance Analysis</h3>
<a name="index-transitions_002c-instance-analysis"></a>
<a name="index-unification-stack"></a>
<p>A preprocessor sorts the input arcs of each transition in such a way
that they can be processed in one pass. Static analysis finds out for
each input arc the set of variables that are assigned a value based on
the token assigned to the arc expression.
</p>
<p>Tokens are assigned to input arcs by a depth-first search algorithm. If
no variables are unified from an arc, the arc is "constant" under the
assignment gathered so far. In this case, the corresponding input place
is searched for the token the arc evaluates to. Otherwise, the arc is
matched with each token in the input place, one at a time, and the
assignment is augmented in such a way that evaluating the arc expression
under the augmented (but still incomplete) assignment can yield the
token picked from the input place.
</p>
<p>In general, the less variables there are in the arc inscriptions and the
less tokens in the input places, the faster the instance analysis can be
completed.
</p>
<hr size="6">
<a name="Model-Checking"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Instance-Analysis" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Safety" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Algorithms" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Algorithms" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_5.html#Grammar" 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="Model-Checking-Algorithms"></a>
<h2 class="section">3.2 Model Checking Algorithms</h2>
<p>The on-the-fly model checker in Maria verifies properties expressed in
temporal logic by computing a product of a property automaton (which
corresponds to a formula) and the reachability graph interpreted as an
automaton.
</p>
<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Safety">3.2.1 Checking Safety Properties</a></td><td> </td><td align="left" valign="top"> Safety properties
</td></tr>
<tr><td align="left" valign="top"><a href="#Liveness">3.2.2 Checking Liveness Properties</a></td><td> </td><td align="left" valign="top"> Liveness properties
</td></tr>
</table>
<hr size="6">
<a name="Safety"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Model-Checking" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="#Liveness" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Algorithms" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Model-Checking" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_5.html#Grammar" 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="Checking-Safety-Properties"></a>
<h3 class="subsection">3.2.1 Checking Safety Properties</h3>
<a name="index-model-checking_002c-safety"></a>
<p>Safety properties can be specified with ‘<samp>deadlock</samp>’ and
‘<samp>reject</samp>’ conditions (see section <a href="maria_2.html#Assertions">Verifying Safety Properties</a>), as well as with so-called
safe LTL formulae that can be translated to automata on finite words.
Also some built-in features of the modelling language, such as capacity
constraints, marking-dependent initialization expressions, and checks
for expression evaluation errors, can be viewed as safety checking.
</p>
<p>While exploring the reachable state space, Maria reports all violations
of safety properties and may abort the analysis in case of a fatal
violation.
</p>
<p>Safety properties can be verified without constructing a reachability
graph; it is sufficient to construct the set of reachable states. The
command line options ‘<samp>-M</samp>’, ‘<samp>-P</samp>’ and ‘<samp>-L</samp>’ are more
efficient than ‘<samp>-m</samp>’, and the search can be distributed on
multiple processors.
</p>
<hr size="6">
<a name="Liveness"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Safety" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="maria_5.html#Grammar" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="#Algorithms" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="#Model-Checking" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="maria_5.html#Grammar" 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="Checking-Liveness-Properties"></a>
<h3 class="subsection">3.2.2 Checking Liveness Properties</h3>
<a name="index-model-checking_002c-liveness"></a>
<p>Currently, the ‘<samp>eval</samp>’ command (see section <a href="maria_3.html#Eval">Evaluating Expressions and Formulae</a>) supports LTL formulae
on state properties. It is possible to examine counterexamples (paths
violating the property being verified), and the algorithm respects both
weak and strong fairness conditions.
</p>
<hr size="6">
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#Algorithms" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="maria_5.html#Grammar" 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