D7net Mini Sh3LL v1
| Current File : //libx32/../sbin/../share/doc/usbmuxd/../libip4tc2/../maria-doc/html/maria_1.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: Introduction</title>
<meta name="description" content="Maria: Introduction">
<meta name="keywords" content="Maria: Introduction">
<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="Introduction"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="maria.html#Top" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="maria_2.html#Modeling" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[ << ]</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_2.html#Modeling" 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="Introduction-1"></a>
<h1 class="unnumbered">Introduction</h1>
<p><em>Maria</em>, or <em>Modular Reachability Analyzer</em>, is a reachability
analyzer for Algebraic System Nets. It will generate reachability
graphs for Algebraic System Nets, detect deadlocks and check properties
expressed using temporal logic formulae.
</p>
<p>Maria is remotely based on Prod, a reachability analyzer for
Proposition/Transition Nets developed earlier at the Laboratory for
Theoretical Computer Science. Its data type system and expression
syntax are heavily inspired by the C programming language. In order to
understand this manual, you should be familiar with the basic concepts
of Petri Nets and also have some knowledge in C.
</p>
<p>Maria was written by Marko Mäkelä in a research project at the
Helsinki University of Technology in the Laboratory for Theoretical
Computer Science. The project is financed by the National Technology
Agency of Finland (TEKES), Nokia Research Center, Nokia Networks, the
Helsinki Telephone Corporation and the Finnish Rail Administration.
</p>
<p>Many of the ideas implemented in Maria were brought up in discussions
among the laboratory staff. Ideas expressed by Dr. Kimmo Varpaaniemi,
Dr. Nisse Husberg, Keijo Heljanko and Tommi Junttila have influenced
the design. Dr. Varpaaniemi sketched the first version of the
unification algorithm (see section <a href="maria_4.html#Unification">The Unification Algorithm</a>), and he helped in debugging
by stressing the analyzer with quite obscure examples. Also Simo Blom,
who was the first one to use the analyzer for something real, reported
some bugs, which have now been fixed.
</p>
<p>The model-checking functionality (see section <a href="maria_4.html#Model-Checking">Model Checking Algorithms</a>) is based on
the ideas of Keijo Heljanko and others, and the algorithms were
initially implemented by Timo Latvala.
</p>
<p>This edition corresponds to version 1.3.5 of Maria.
</p>
<hr size="6">
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[ << ]</td>
<td valign="middle" align="left">[<a href="maria_2.html#Modeling" 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