/usr/share/doc/maria-doc/html/maria_4.html is in maria-doc 1.3.5-4.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html401/loose.dtd">
<html>
<!-- Created on May 14, 2011 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>May 14, 2011</em> using <a href="http://www.nongnu.org/texi2html/"><em>texi2html 1.82</em></a>.
</font>
<br>
</p>
</body>
</html>
|