Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[919] trunk/doc/help
|
From: <koc...@us...> - 2010-09-13 14:23:41
|
Revision: 919
http://scstudio.svn.sourceforge.net/scstudio/?rev=919&view=rev
Author: kocianon
Date: 2010-09-13 14:23:33 +0000 (Mon, 13 Sep 2010)
Log Message:
-----------
converted to xhtml, some redundant files deleted
Modified Paths:
--------------
trunk/doc/help/acyclic/acyclic.html
trunk/doc/help/beautify/beautify.html
trunk/doc/help/boundedness/boundedness.html
trunk/doc/help/deadlock/deadlock.html
trunk/doc/help/fifo/fifo.html
trunk/doc/help/help.css
trunk/doc/help/livelock/livelock.html
trunk/doc/help/localchoice/localchoice.html
trunk/doc/help/membership/membership.html
trunk/doc/help/race/race.html
trunk/doc/help/realizability/realizability.html
trunk/doc/help/recursivity/recursivity.html
trunk/doc/help/time_consistency/time_consistency.html
trunk/doc/help/time_syntax/time_syntax.html
trunk/doc/help/time_tighten/time_tighten.html
trunk/doc/help/time_trace_race/time_race.html
trunk/doc/help/unique_instance/unique_instance.html
Removed Paths:
-------------
trunk/doc/help/beautify/coregion1.png
trunk/doc/help/beautify/coregion2.png
trunk/doc/help/beautify/ordered.png
trunk/doc/help/beautify/unfifo2.png
trunk/doc/help/beautify/unordered.png
trunk/doc/help/boundedness/unbounded.png
trunk/doc/help/deadlock/deadlock.png
trunk/doc/help/livelock/livelock.png
trunk/doc/help/membership/memebership_1.png
trunk/doc/help/membership/memebership_10.png
trunk/doc/help/membership/memebership_11.png
trunk/doc/help/membership/memebership_12.png
trunk/doc/help/membership/memebership_2.png
trunk/doc/help/membership/memebership_3.png
trunk/doc/help/membership/memebership_4.png
trunk/doc/help/membership/memebership_5.png
trunk/doc/help/membership/memebership_6.png
trunk/doc/help/membership/memebership_7.png
trunk/doc/help/membership/memebership_8.png
trunk/doc/help/membership/memebership_9.png
Modified: trunk/doc/help/acyclic/acyclic.html
===================================================================
--- trunk/doc/help/acyclic/acyclic.html 2010-09-13 13:40:13 UTC (rev 918)
+++ trunk/doc/help/acyclic/acyclic.html 2010-09-13 14:23:33 UTC (rev 919)
@@ -1,46 +1,71 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
-<HTML>
-<HEAD>
- <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
- <TITLE>Acyclic property</TITLE>
- <meta name="author" content="Martin Chmelik">
- <LINK href="../help.css" rel="stylesheet" type="text/css"/>
-</HEAD>
-<BODY>
-<H1>Acyclic property</H1>
-<P> ensures that there is no cyclic dependency among events in an BMSC. Such a dependency is erroneous, because it requires to wait with sending a message until it is received. An example of such BMSC design can be seen in the following figure: </P>
+<?xml version="1.0" encoding="utf-8"?>
+<!DOCTYPE html
+ PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd" >
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/cyclic_simple.png" width="250" BORDER="0" ALT="Cyclic BMSC" TITLE="Cyclic BMSC"></li>
- <li class="caption">Cyclic design</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/cyclic_result.png" width="250" BORDER="0" ALT="Cyclic BMSC" TITLE="Cyclic BMSC"></li>
- <li class="caption">Highlighted cyclic dependency</li>
- </ul>
-</li>
-</ul>
-</div>
-
-<p style="clear: both;">
-Sending message <I>m2</I> may not be done until message <I>m1</I> is received, but message <I>m1</I> may not be send until message <I>m2</I> is received.</P>
-SCStudio highlights the cyclic dependency:
-
-A more tricky example of an acyclic design is depicted on the following figure. There is a coregion box on the <I>Instance p</I> which contains send of the message <I>m2</I> and receive of the message <I>m1</I>. From the semantics of coregion it follows that <I>m1, m2</I> are unordered. Thus we can perform first <I>m1</I> and then <I> m2 </I> and there is no cyclic dependency. </p>
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/acyclic.png" width="250" BORDER="0" ALT="Acyclic BMSC" TITLE="Acyclic BMSC"></li>
- <li class="caption">Acyclic design</li>
- </ul>
-</li>
-</ul>
-</div>
-
-</BODY>
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <title>Acyclic property</title>
+ <meta name="author" content="Martin Chmelik" />
+ <link href="../help.css" rel="stylesheet" type="text/css" />
+ </head>
+ <body>
+ <h1>Acyclic property</h1>
+ <p>
+ ensures that there is no cyclic dependency among events in an BMSC. Such a
+ dependency is erroneous, because it requires to wait with sending a
+ message until it is received. An example of such BMSC design can be seen
+ in the following figure:
+ </p>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/cyclic_simple.png" width="250"
+ alt="Cyclic BMSC" title="Cyclic BMSC" />
+ </li>
+ <li class="caption">
+ Cyclic design
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/cyclic_result.png" width="250"
+ alt="Cyclic BMSC" title="Cyclic BMSC" />
+ </li>
+ <li class="caption">
+ Highlighted cyclic dependency
+ </li>
+ </ul>
+ </li>
+ </ul>
+ <p>
+ Sending message <i>m2</i> may not be done until message <i>m1</i>
+ is received, but message <i>m1</i> may not be send until message
+ <i>m2</i> is received.
+ </p>
+ SCStudio highlights the cyclic dependency: A more tricky example of an
+ acyclic design is depicted on the following figure. There is a coregion box
+ on the <i>Instance p</i> which contains send of the message <i>m2</i>
+ and receive of the message <i>m1</i>. From the semantics of
+ coregion it follows that <i>m1, m2</i> are unordered. Thus we can
+ perform first <i>m1</i> and then <i> m2 </i> and there is
+ no cyclic dependency.
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/acyclic.png" width="250"
+ alt="Acyclic BMSC" title="Acyclic BMSC" />
+ </li>
+ <li class="caption">
+ Acyclic design
+ </li>
+ </ul>
+ </li>
+ </ul>
+ </body>
+</html>
Modified: trunk/doc/help/beautify/beautify.html
===================================================================
--- trunk/doc/help/beautify/beautify.html 2010-09-13 13:40:13 UTC (rev 918)
+++ trunk/doc/help/beautify/beautify.html 2010-09-13 14:23:33 UTC (rev 919)
@@ -1,78 +1,114 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
-<HTML>
-<HEAD>
- <TITLE>Beautify documentation</TITLE>
- <LINK href="../help.css" rel="stylesheet" type="text/css"/>
-</HEAD>
-<div>
-<h2>Beautify</h2>
-<P>The main aim of this function is to redraw BMSC to be well-arranged.
-It is accessible via menu <code>Check → Drawing → Beautify</code>.
-</P>
-<h3> Example 1:</h3>
-<P>It changes order of instances to minimize a number of messages
-going from right side to left side and crossing instances with messages.
-Instances are justified to top and have the same length.
-For <a href="../fifo/fifo.html">FIFO</a> and
-<a href="../acyclic/acyclic.html">acyclic</a> BMSC it makes all messages
-horizontal and arranged over instances uniformly from top to down.
-</P>
+<?xml version="1.0" encoding="utf-8"?>
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/unordered.png" width="500" BORDER="0" ALT="Unordered BMSC"></li>
- <li class="caption">Before beautify</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/ordered.png" align="middle" width="350" BORDER="0" ALT="Ordered BMSC"></li>
- <li class="caption">After beautify</li>
- </ul>
-</li>
-</ul>
-</div>
-<p style="clear: both;">
+<!DOCTYPE html
+ PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd" >
-<h3> Example 2:</h3>
-<P>A <a href="../fifo/fifo.html">non-FIFO</a> BMSC is redrawn to
-a form that no messages are going up.</P>
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/unfifo2.png" width="250" BORDER="0" ALT="Ordered non-FIFO BMSC"></li>
- <li class="caption">Acyclic design</li>
- </ul>
-</li>
-</ul>
-</div>
-
-<p style="clear: both;">
-<h3> Example 3:</h3>
-<P>For coregions it changes the order of events to minimize number
-of crossing two messages. After redrawing, messages are jointed with
-coregion in such way that they do not go across coregion body.
-<BR></P>
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li>
- <img src="pictures/coregion1.png" width="250" alt="Crossing messages jointed with coregion"></li>
- <li class="caption">Before beautify</li>
- </ul></li>
-<li>
- <ul>
-
- <li>
- <img src="pictures/coregion2.png" width="250 "alt=""></li>
- <li class="caption">After beautify</li>
- </ul>
-</li>
-</ul>
-</div>
-
-</BODY>
-</HTML>
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <title>
+ Beautify documentation
+ </title>
+ <link href="../help.css" rel="stylesheet" type="text/css" />
+ </head>
+ <body>
+ <h2>
+ Beautify
+ </h2>
+ <p>
+ The main aim of this function is to redraw BMSC to be well-arranged. It
+ is accessible via menu <code>Check → Drawing → Beautify</code>.
+ </p>
+ <h3>
+ Example 1:
+ </h3>
+ <p>
+ It changes order of instances to minimize a number of messages going
+ from right side to left side and crossing instances with messages.
+ Instances are justified to top and have the same length. For <a
+ href="../fifo/fifo.html">FIFO</a> and <a
+ href="../acyclic/acyclic.html">acyclic</a> BMSC it makes all
+ messages horizontal and arranged over instances uniformly from top to
+ down.
+ </p>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/unordered.png" width="500" border="0"
+ alt="Unordered BMSC" />
+ </li>
+ <li class="caption">
+ Before beautify
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/ordered.png" width="350"
+ border="0" alt="Ordered BMSC" />
+ </li>
+ <li class="caption">
+ After beautify
+ </li>
+ </ul>
+ </li>
+ </ul>
+ <p>
+ </p>
+ <h3>
+ Example 2:
+ </h3>
+ <p>
+ A <a href="../fifo/fifo.html">non-FIFO</a> BMSC is redrawn to a
+ form that no messages are going up.
+ </p>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/unfifo2.png" width="250"
+ alt="Ordered non-FIFO BMSC" />
+ </li>
+ <li class="caption">
+ Acyclic design
+ </li>
+ </ul>
+ </li>
+ </ul>
+ <p>
+ </p>
+ <h3>
+ Example 3:
+ </h3>
+ <p>
+ For coregions it changes the order of events to minimize number of
+ crossing two messages. After redrawing, messages are jointed with
+ coregion in such way that they do not go across coregion body.
+ </p>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/coregion1.png" width="250"
+ alt="Crossing messages jointed with coregion" />
+ </li>
+ <li class="caption">
+ Before beautify
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/coregion2.png" width="250 " alt="" />
+ </li>
+ <li class="caption">
+ After beautify
+ </li>
+ </ul>
+ </li>
+ </ul>
+ </body>
+</html>
Deleted: trunk/doc/help/beautify/coregion1.png
===================================================================
(Binary files differ)
Deleted: trunk/doc/help/beautify/coregion2.png
===================================================================
(Binary files differ)
Deleted: trunk/doc/help/beautify/ordered.png
===================================================================
(Binary files differ)
Deleted: trunk/doc/help/beautify/unfifo2.png
===================================================================
(Binary files differ)
Deleted: trunk/doc/help/beautify/unordered.png
===================================================================
(Binary files differ)
Modified: trunk/doc/help/boundedness/boundedness.html
===================================================================
--- trunk/doc/help/boundedness/boundedness.html 2010-09-13 13:40:13 UTC (rev 918)
+++ trunk/doc/help/boundedness/boundedness.html 2010-09-13 14:23:33 UTC (rev 919)
@@ -1,37 +1,72 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
-<HTML>
-<HEAD>
- <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
- <TITLE>Universal Boundedness</TITLE>
- <meta name="author" content="Martin Chmelik">
- <LINK href="../help.css" rel="stylesheet" type="text/css"/>
-</HEAD>
-<BODY>
-<H1>Universal Boundedness</H1>
-<P>is a property of an HMSC. An HMSC is universally bounded if there exists an upper bound on size of communication buffers of all involved processes. Informally, each instance waits for a response before sending the same message again. A dialog is an example of bounded communication. E-mail spam is an example of unbounded communication - actually, it is not rare that an input buffer (mailbox) gets full in this case. </P>
+<?xml version="1.0" encoding="utf-8"?>
-<P>When all the possible executions of an HMSC are finite, then HMSC is universally bounded. Therefore only HMSCs containing a cycle may be unbounded. Every cycle whose repetitive execution may lead to unbounded grow of an input buffer is found and displayed by SCStudio.</P>
-<P>The HMSC on the following picture is unbounded. This is because there is no mechanism for keeping the buffer for messages between <I>X</I> and <I>Y</I> bounded. </P>
+<!DOCTYPE html
+ PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd" >
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/unbounded_hmsc.png" width="200" BORDER="0" ALT="Unbounded HMSC" TITLE="Unbounded HMSC"></li>
- <li class="caption">Unbounded HMSC</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/unbounded_msc.png" width="250" BORDER="0" ALT="MSC A" TITLE="MSC A"></li>
- <li class="caption">MSC A</li>
- </ul>
-</li>
-</ul>
-</div>
-
-<p style="clear: both;">
-
-
-<P>For any bound <I>B</I> of the buffer we can make an execution for which the buffer is not sufficiently large. This execution is for example the one which goes through cycle <I>B+1</I> times, the sending of message is very fast and the receiving is very slow. It is so slow, that in point of time when we have sent all messages we have not received any of them. Thus we have exceeded the bound <I>B</I> for this buffer.</P>
-<p>
-</BODY>
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <title>
+ Universal Boundedness
+ </title>
+ <meta name="author" content="Martin Chmelik" />
+ <link href="../help.css" rel="stylesheet" type="text/css" />
+ </head>
+ <body>
+ <h1>
+ Universal Boundedness
+ </h1>
+ <p>
+ is a property of an HMSC. An HMSC is universally bounded if there exists
+ an upper bound on size of communication buffers of all involved processes.
+ Informally, each instance waits for a response before sending the same
+ message again. A dialog is an example of bounded communication. E-mail
+ spam is an example of unbounded communication - actually, it is not rare
+ that an input buffer (mailbox) gets full in this case.
+ </p>
+ <p>
+ When all the possible executions of an HMSC are finite, then HMSC is
+ universally bounded. Therefore only HMSCs containing a cycle may be
+ unbounded. Every cycle whose repetitive execution may lead to unbounded
+ grow of an input buffer is found and displayed by SCStudio.
+ </p>
+ <p>
+ The HMSC on the following picture is unbounded. This is because there is
+ no mechanism for keeping the buffer for messages between <i>X</i>
+ and <i>Y</i> bounded.
+ </p>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/unbounded_hmsc.png" width="200"
+ alt="Unbounded HMSC" title="Unbounded HMSC" />
+ </li>
+ <li class="caption">
+ Unbounded HMSC
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/unbounded_msc.png" width="250"
+ alt="MSC A" title="MSC A" />
+ </li>
+ <li class="caption">
+ MSC A
+ </li>
+ </ul>
+ </li>
+ </ul>
+ <p>
+ For any bound <i>B</i> of the buffer we can make an execution for
+ which the buffer is not sufficiently large. This execution is for example
+ the one which goes through cycle <i>B+1</i> times, the sending of
+ message is very fast and the receiving is very slow. It is so slow, that
+ in point of time when we have sent all messages we have not received any
+ of them. Thus we have exceeded the bound <i>B</i> for this
+ buffer.
+ </p>
+ </body>
+</html>
Deleted: trunk/doc/help/boundedness/unbounded.png
===================================================================
(Binary files differ)
Modified: trunk/doc/help/deadlock/deadlock.html
===================================================================
--- trunk/doc/help/deadlock/deadlock.html 2010-09-13 13:40:13 UTC (rev 918)
+++ trunk/doc/help/deadlock/deadlock.html 2010-09-13 14:23:33 UTC (rev 919)
@@ -1,31 +1,47 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
-<HTML>
-<HEAD>
- <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
- <TITLE>Deadlock</TITLE>
- <meta name="author" content="Martin Chmelik">
- <LINK href="../help.css" rel="stylesheet" type="text/css"/>
-</HEAD>
-<BODY>
-<H1>Deadlock</H1>
-<P>is a property of a HMSC node. A reachable node is deadlocked if there is no reference node reachable from the node, i.e. after executing the BMSC referenced by a deadlocked node, there is no node to continue with.</P>
+<?xml version="1.0" encoding="utf-8"?>
-<P>
-SCStudio finds all deadlocked nodes in a given HMSC. For each deadlocked node a path from the start node to the node is given as an example of the deadlock.
-</P>
+<!DOCTYPE html
+ PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd" >
-<P>
-On the next picture the node B is clearly a deadlocked node. That is why it is highlighted by SCStudio and given as an example.
-</P>
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/deadlock.png" width="350" BORDER="0" ALT="Typical deadlock" TITLE="Typical deadlock"></li>
- <li class="caption">Typical deadlock</li>
- </ul>
-</li>
-</ul>
-</div>
-
-</BODY>
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <title>
+ Deadlock
+ </title>
+ <meta name="author" content="Martin Chmelik" />
+ <link href="../help.css" rel="stylesheet" type="text/css" />
+ </head>
+ <body>
+ <h1>
+ Deadlock
+ </h1>
+ <p>
+ is a property of a HMSC node. A reachable node is deadlocked if there is
+ no reference node reachable from the node, i.e. after executing the BMSC
+ referenced by a deadlocked node, there is no node to continue with.
+ </p>
+ <p>
+ SCStudio finds all deadlocked nodes in a given HMSC. For each deadlocked
+ node a path from the start node to the node is given as an example of the
+ deadlock.
+ </p>
+ <p>
+ On the next picture the node B is clearly a deadlocked node. That is why
+ it is highlighted by SCStudio and given as an example.
+ </p>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/deadlock.png" width="350"
+ alt="Typical deadlock" title="Typical deadlock" />
+ </li>
+ <li class="caption">
+ Typical deadlock
+ </li>
+ </ul>
+ </li>
+ </ul>
+ </body>
+</html>
Deleted: trunk/doc/help/deadlock/deadlock.png
===================================================================
(Binary files differ)
Modified: trunk/doc/help/fifo/fifo.html
===================================================================
--- trunk/doc/help/fifo/fifo.html 2010-09-13 13:40:13 UTC (rev 918)
+++ trunk/doc/help/fifo/fifo.html 2010-09-13 14:23:33 UTC (rev 919)
@@ -1,116 +1,182 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
-<HTML>
-<HEAD>
- <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
- <TITLE>FIFO</TITLE>
- <meta name="author" content="Martin Chmelik">
- <LINK href="../help.css" rel="stylesheet" type="text/css"/>
-</HEAD>
-<BODY>
-<H1>FIFO (First In, First Out) property</H1>
-<P>is a BMSC property. The property ensures that it is possible
-to implement the desired behavior without deadlocks, that would be
-caused by channel behavior.</P>
+<?xml version="1.0" encoding="utf-8"?>
-<P>
-There are several types of channels and several ways how they can be used in BMSC. Some of the most useful are the following:
-<ul>
-<li> FIFO channel for every pair of instances </li>
-<li> FIFO channel for every pair of instances and labels </li>
-<li> One FIFO channel for every process </li>
-<li> One FIFO channel for all processes </li>
-</ul>
+<!DOCTYPE html
+ PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd" >
-The SCStudio currently supports the first two options. The extension for other options is planned.
-</P>
-
-<H2>Basic Message Sequence Chart</H2>
-<H3>FIFO channel for every pair of instances </H3>
-<P>FIFO property is violated when there are two
-messages, such that they share a common source and destination
-instance and the latter message may arrive before the first one.</p>
-<p> Imagine we have a system in an all-channel FIFO environment which behaves according to a BMSC specification. A process expects the messages to arrive in some order, according to specification, but the messages might have been sent in a different order. A deadlock is reached as there might be a different message in the head of the channel queue.
-</P>
-<P>An example of a non-FIFO design can be seen on the
-next picture. Message <I>m1</I> is sent before <I>m2</I>, but
-instance <I>q</I> receives message <I>m2</I> before <I>m1. </I>Because
-we are having a FIFO channel between instances <I>p</I> and <I>q</I>,
-this is not possible and leads to a deadlock.</P>
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/simple_non_fifo.png" width="250" BORDER="0" ALT="Example of a non-fifo design" TITLE="Example of a non-fifo design"></li>
- <li class="caption">Example of a non-FIFO design</li>
- </ul>
-</li>
-</ul>
-</div>
-<p style="clear: both;">
-
-<h4>Formal definition:</h4>
-<P>BMSC is FIFO if for all receive events <I>c</I>, <I>d</I> and their matching send events
-<I>a, b</I> (<<I>a,c</I>> forms the first message and <<I>b,d</I>> forms the second message) it holds that
-<I>c < d => a < b</I>, where < is the visual order and the two messages belong
-to the same channel.</P>
-<P>On the next picture we can see tricky examples of FIFO BMSCs. They satisfy the FIFO property, because the receive events of both messages are in coregion. This means that the user has specified that the receive events can happen in an arbitrary order. So that if there is any order of these two events in the head of the channel queue, the system will certainly not reach deadlock.</P>
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/fifo1.png" width="250" BORDER="0" ALT="FIFO MSC design" TITLE="FIFO MSC design"></li>
- <li class="caption">Example of a FIFO design</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/fifo2.png" width="250" BORDER="0" ALT="FIFO MSC design" TITLE="FIFO MSC design"></li>
- <li class="caption">Example of a different FIFO design</li>
- </ul>
-</li>
-</ul>
-</div>
-
-<p style="clear: both;">
-
-<P>An example of a non-FIFO design can be seen on the following picture. This is because the <I>Instance q</I> can execute only the receive event of message <I>m1</I> and then the receive event of the message <I>m2</I>. However it is possible (due to coregion), that the message <I>m2</I> is at head of the channel queue of Instance q and message <I>m2</I> is behind it. </P>
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/nonfifo1.png" width="250" BORDER="0" ALT="non-fifo design" TITLE="non-fifo design"></li>
- <li class="caption">Example of a non-FIFO design</li>
- </ul>
-</li>
-</ul>
-</div>
-<p style="clear: both;">
-
-<H3>FIFO channel for every pair of instances and labels</H3>
-<P>In this case we can have more than one FIFO channel between two processes. For every label there is one channel. Everything what has satisfied FIFO property in the previous case, will satisfy the property also in this case. The difference can be seen on the following FIFO example:</P>
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/label_channel_fifo.png" width="250" BORDER="0" ALT="FIFO MSC design" TITLE="FIFO MSC design"></li>
-
- </ul>
-</li>
-</ul>
-</div>
-<p style="clear: both;">
-
-<P>Messages <I>m2</I> and <I>m1</I> are not in the same channel, therefore they may arrive in
-any order.</P>
-<!-- comment
-<H3>One FIFO buffer for every process</H3>
-<P>TODO, wait until implementation is done</P>
-<H3>One FIFO buffer for all processes</H3>
-<P>TODO, wait until implementation is done</P>
--->
-<H2>High-level Message Sequence Chart</H2>
-<P>HMSC satisfies FIFO property for a certain channel
-type, if every BMSC represented by the HMSC satisfies the FIFO property
-for that channel type.</P>
-</BODY>
-</HTML>
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <title>
+ FIFO
+ </title>
+ <meta name="author" content="Martin Chmelik" />
+ <link href="../help.css" rel="stylesheet" type="text/css" />
+ </head>
+ <body>
+ <h1>
+ FIFO (First In, First Out) property
+ </h1>
+ <p>
+ is a BMSC property. The property ensures that it is possible to implement
+ the desired behavior without deadlocks, that would be caused by channel
+ behavior.
+ </p>
+ <p>
+ There are several types of channels and several ways how they can be used
+ in BMSC. Some of the most useful are the following:
+ </p>
+ <ul>
+ <li>
+ FIFO channel for every pair of instances
+ </li>
+ <li>
+ FIFO channel for every pair of instances and labels
+ </li>
+ <li>
+ One FIFO channel for every process
+ </li>
+ <li>
+ One FIFO channel for all processes
+ </li>
+ </ul>
+ The SCStudio currently supports the first two options. The extension for
+ other options is planned.
+ <h2>
+ Basic Message Sequence Chart
+ </h2>
+ <h3>
+ FIFO channel for every pair of instances
+ </h3>
+ <p>
+ FIFO property is violated when there are two messages, such that they
+ share a common source and destination instance and the latter message may
+ arrive before the first one.
+ </p>
+ <p>
+ Imagine we have a system in an all-channel FIFO environment which behaves
+ according to a BMSC specification. A process expects the messages to
+ arrive in some order, according to specification, but the messages might
+ have been sent in a different order. A deadlock is reached as there might
+ be a different message in the head of the channel queue.
+ </p>
+ <p>
+ An example of a non-FIFO design can be seen on the next picture. Message
+ <i>m1</i> is sent before <i>m2</i>, but instance <i>q</i>
+ receives message <i>m2</i> before <i>m1. </i>Because we
+ are having a FIFO channel between instances <i>p</i> and <i>q</i>,
+ this is not possible and leads to a deadlock.
+ </p>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/simple_non_fifo.png" width="250" border="0"
+ alt="Example of a non-fifo design"
+ title="Example of a non-fifo design" />
+ </li>
+ <li class="caption">
+ Example of a non-FIFO design
+ </li>
+ </ul>
+ </li>
+ </ul>
+ <p>
+ </p>
+ <h4>
+ Formal definition:
+ </h4>
+ <p>
+ BMSC is FIFO if for all receive events <i>c</i>, <i>d</i>
+ and their matching send events <i>a, b</i> (<<i>a,c</i>>
+ forms the first message and <<i>b,d</i>> forms the second
+ message) it holds that <i>c < d => a < b</i>, where < is
+ the visual order and the two messages belong to the same channel.
+ </p>
+ <p>
+ On the next picture we can see tricky examples of FIFO BMSCs. They satisfy
+ the FIFO property, because the receive events of both messages are in
+ coregion. This means that the user has specified that the receive events
+ can happen in an arbitrary order. So that if there is any order of these
+ two events in the head of the channel queue, the system will certainly not
+ reach deadlock.
+ </p>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/fifo1.png" width="250" border="0"
+ alt="FIFO MSC design" title="FIFO MSC design" />
+ </li>
+ <li class="caption">
+ Example of a FIFO design
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/fifo2.png" width="250" border="0"
+ alt="FIFO MSC design" title="FIFO MSC design" />
+ </li>
+ <li class="caption">
+ Example of a different FIFO design
+ </li>
+ </ul>
+ </li>
+ </ul>
+ <p>
+ An example of a non-FIFO design can be seen on the following picture. This
+ is because the <i>Instance q</i> can execute only the receive
+ event of message <i>m1</i> and then the receive event of the
+ message <i>m2</i>. However it is possible (due to coregion), that
+ the message <i>m2</i> is at head of the channel queue of Instance
+ q and message <i>m2</i> is behind it.
+ </p>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/nonfifo1.png" width="250" border="0"
+ alt="non-fifo design" title="non-fifo design" />
+ </li>
+ <li class="caption">
+ Example of a non-FIFO design
+ </li>
+ </ul>
+ </li>
+ </ul>
+ <h3>
+ FIFO channel for every pair of instances and labels
+ </h3>
+ <p>
+ In this case we can have more than one FIFO channel between two processes.
+ For every label there is one channel. Everything what has satisfied FIFO
+ property in the previous case, will satisfy the property also in this
+ case. The difference can be seen on the following FIFO example:
+ </p>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/label_channel_fifo.png" width="250" border="0"
+ alt="FIFO MSC design" title="FIFO MSC design" />
+ </li>
+ </ul>
+ </li>
+ </ul>
+ <p>
+ Messages <i>m2</i> and <i>m1</i> are not in the same
+ channel, therefore they may arrive in any order.
+ </p>
+ <!-- comment <H3>One FIFO buffer for every process</H3> <P>TODO, wait until
+ implementation is done</P> <H3>One FIFO buffer for all processes</H3>
+ <P>TODO, wait until implementation is done</P> -->
+ <h2>
+ High-level Message Sequence Chart
+ </h2>
+ <p>
+ HMSC satisfies FIFO property for a certain channel type, if every BMSC
+ represented by the HMSC satisfies the FIFO property for that channel type.
+ </p>
+ </body>
+</html>
Modified: trunk/doc/help/help.css
===================================================================
--- trunk/doc/help/help.css 2010-09-13 13:40:13 UTC (rev 918)
+++ trunk/doc/help/help.css 2010-09-13 14:23:33 UTC (rev 919)
@@ -6,6 +6,7 @@
p {
margin-top: 0em;
margin-bottom: 0.7em;
+ clear: both;
}
h1 {
font-size: 1.4em;
Modified: trunk/doc/help/livelock/livelock.html
===================================================================
--- trunk/doc/help/livelock/livelock.html 2010-09-13 13:40:13 UTC (rev 918)
+++ trunk/doc/help/livelock/livelock.html 2010-09-13 14:23:33 UTC (rev 919)
@@ -1,25 +1,45 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
-<HTML>
-<HEAD>
- <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
- <TITLE>Livelock</TITLE>
- <meta name="author" content="Martin Chmelik">
- <LINK href="../help.css" rel="stylesheet" type="text/css"/>
-</HEAD>
-<BODY>
-<H1>Livelock</H1>
-<P>is a property of an HMSC. An HMSC contains a livelock if there exists a cycle of nodes from which no endnode is reachable. It is required that the cycle contains at least one reference node.</P>
+<?xml version="1.0" encoding="utf-8"?>
-<P>SCStudio finds and displays all such cycles in a given HMSC.</P>
-<P> An example of livelock is depicted on the next picture. It clearly satisfies all conditions for livelock.</P>
+<!DOCTYPE html
+ PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd" >
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/livelock.png" width="450" BORDER="0" ALT="Typical livelock" TITLE="Typical livelock"></li>
- <li class="caption">Typical livelock</li>
- </ul>
-</li>
-</ul>
-</div>
-</BODY>
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <title>
+ Livelock
+ </title>
+ <meta name="author" content="Martin Chmelik" />
+ <link href="../help.css" rel="stylesheet" type="text/css" />
+ </head>
+ <body>
+ <h1>
+ Livelock
+ </h1>
+ <p>
+ is a property of an HMSC. An HMSC contains a livelock if there exists a
+ cycle of nodes from which no endnode is reachable. It is required that the
+ cycle contains at least one reference node.
+ </p>
+ <p>
+ SCStudio finds and displays all such cycles in a given HMSC.
+ </p>
+ <p>
+ An example of livelock is depicted on the next picture. It clearly
+ satisfies all conditions for livelock.
+ </p>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/livelock.png" width="450"
+ alt="Typical livelock" title="Typical livelock" />
+ </li>
+ <li class="caption">
+ Typical livelock
+ </li>
+ </ul>
+ </li>
+ </ul>
+ </body>
+</html>
Deleted: trunk/doc/help/livelock/livelock.png
===================================================================
(Binary files differ)
Modified: trunk/doc/help/localchoice/localchoice.html
===================================================================
--- trunk/doc/help/localchoice/localchoice.html 2010-09-13 13:40:13 UTC (rev 918)
+++ trunk/doc/help/localchoice/localchoice.html 2010-09-13 14:23:33 UTC (rev 919)
@@ -1,62 +1,109 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
-<HTML>
-<HEAD>
- <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
- <TITLE>Non-local choice</TITLE>
- <meta name="author" content="Martin Chmelik">
- <LINK href="../help.css" rel="stylesheet" type="text/css"/>
-</HEAD>
-<BODY>
-<H1>Non-local choice</H1>
-<P>is a property of an HMSC node, that has more than one successor, occurring when multiple different behaviors (branches <I>MSC A</I> or <I>MSC B</I>) are possible and the branches are initiated by different instances (<I>MSC A</I> is initiated by the <I>Instance p</I>, <I>MSC B</I> is initiated by the <I>Instance q</I>). Therefore the resulting behavior of the system may contain a combination of both branches, resulting in a non specified implied behavior. </P>
+<?xml version="1.0" encoding="utf-8"?>
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/simple_nonlocal.png" width="550" BORDER="0" ALT="HMSC specification with a branching node" TITLE="HMSC specification with a branching node"></li>
- <li class="caption">HMSC specification with a branching node</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/simple_nonlocal_MSCA.png" width="200" BORDER="0" ALT="MSC A" TITLE="MSC A"></li>
- <li class="caption">MSC A</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/simple_nonlocal_MSCB.png" width="200" BORDER="0" ALT="MSC B" TITLE="MSC B"></li>
- <li class="caption">MSC B</li>
- </ul>
-</li>
-</ul>
-</div>
+<!DOCTYPE html
+ PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd" >
-<p style="clear: both;">
-
-More formally, a branching node is called a non-local choice if one of the conditions is satisfied:</P>
-<UL>
-<LI> There exists a branch that is initiated by more than one instance.</LI>
-<LI> There exist two branches, such that each is initiated by different instance</LI>.
-</UL>
-
-<P>The result of the check on the previous example marks the non-local choice node with the red color:</P>
-
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/simple_nonlocal_result.png" width="350" BORDER="0" ALT="Result of SCStudio" TITLE="Result of SCStudio"></li>
- <li class="caption">Result of SCStudio</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/simple_nonlocal_implied.png" width="200" BORDER="0" ALT="Implied behavior" TITLE="Implied behavior"></li>
- <li class="caption">Implied behavior</li>
- </ul>
-</li>
-</ul>
-</div>
-</BODY>
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <title>
+ Non-local choice
+ </title>
+ <meta name="author" content="Martin Chmelik" />
+ <link href="../help.css" rel="stylesheet" type="text/css" />
+ </head>
+ <body>
+ <h1>
+ Non-local choice
+ </h1>
+ <p>
+ is a property of an HMSC node, that has more than one successor, occurring
+ when multiple different behaviors (branches <i>MSC A</i> or <i>MSC
+ B</i>) are possible and the branches are initiated by different
+ instances (<i>MSC A</i> is initiated by the <i>Instance p</i>,
+ <i>MSC B</i> is initiated by the <i>Instance q</i>).
+ Therefore the resulting behavior of the system may contain a combination
+ of both branches, resulting in a non specified implied behavior.
+ </p>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/simple_nonlocal.png" width="550" border="0"
+ alt="HMSC specification with a branching node"
+ title="HMSC specification with a branching node" />
+ </li>
+ <li class="caption">
+ HMSC specification with a branching node
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/simple_nonlocal_MSCA.png" width="200"
+ border="0" alt="MSC A" title="MSC A" />
+ </li>
+ <li class="caption">
+ MSC A
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/simple_nonlocal_MSCB.png" width="200"
+ border="0" alt="MSC B" title="MSC B" />
+ </li>
+ <li class="caption">
+ MSC B
+ </li>
+ </ul>
+ </li>
+ </ul>
+ <p>
+ More formally, a branching node is called a non-local choice if one of the
+ conditions is satisfied:
+ </p>
+ <ul>
+ <li>
+ There exists a branch that is initiated by more than one instance.
+ </li>
+ <li>
+ There exist two branches, such that each is initiated by different
+ instance
+ </li>
+ <li>
+ .
+ </li>
+ </ul>
+ <p>
+ The result of the check on the previous example marks the non-local choice
+ node with the red color:
+ </p>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/simple_nonlocal_result.png" width="350"
+ border="0" alt="Result of SCStudio" title="Result of SCStudio" />
+ </li>
+ <li class="caption">
+ Result of SCStudio
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/simple_nonlocal_implied.png" width="200"
+ border="0" alt="Implied behavior" title="Implied behavior" />
+ </li>
+ <li class="caption">
+ Implied behavior
+ </li>
+ </ul>
+ </li>
+ </ul>
+ </body>
+</html>
Modified: trunk/doc/help/membership/membership.html
===================================================================
--- trunk/doc/help/membership/membership.html 2010-09-13 13:40:13 UTC (rev 918)
+++ trunk/doc/help/membership/membership.html 2010-09-13 14:23:33 UTC (rev 919)
@@ -1,135 +1,214 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
-<HTML>
-<HEAD>
- <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
- <TITLE>membership documentation</TITLE>
- <LINK href="../help.css" rel="stylesheet" type="text/css"/>
-</HEAD>
-<BODY LANG="en-US" DIR="LTR" STYLE="border: none; padding: 0in">
-<h1>Membership</FONT></h1>
-<P >The problem of
-membership is deciding whether given BMSC is contained in a given HMSC.
-It is possible to check both untimed and timed cases of BMSCs and
-HMSCs.<BR></P>
-<h3>Example 1:</h3>
+<?xml version="1.0" encoding="utf-8"?>
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/memebership_4.png" width="250" BORDER="0" ALT="Input bMSC" TITLE="Input bMSC"></li>
- <li class="caption">Input BMSC</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_1.png" width="150" BORDER="0" ALT="Input HMSC" TITLE="Input HMSC"></li>
- <li class="caption">Input HMSC</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_2.png" width="250" BORDER="0" ALT="bMSC01" TITLE="bMSC01"></li>
- <li class="caption">bMSC01</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_3.png" width="250" BORDER="0" ALT="bMSC02" TITLE="bMSC02"></li>
- <li class="caption">bMSC02</li>
- </ul>
-</li>
-</ul>
-</div>
+<!DOCTYPE html
+ PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd" >
-<p style="clear: both;">
-In the figure above we
-have specified an input to the membership problem. Every path from the
-initial node to the terminal node in a HMSC represents a BMSC. There is
-only one path in the <i>Input HMSC</i>. The BMSC specified by the path is
-formed from nodes (BMSCs) on the path by the sequential composition
-(putting the BMSCs one after the other and gluing the matching
-process lines). It is easy to see that the <i>Input BMSC</i> is exactly the
-same BMSC represented by the only path in the <i>Input HMSC</i>. The result of
-procedure solving membership problem should be every successful path
-i.e. <i>Input HMSC</i>.</P>
-<P >More formal
-specification of the procedure:</P>
-<P >Input:
-</P>
-<UL>
- <LI><P >BMSC with the timing
- assignment</P>
- <LI><P >MSC with timers
- and time constraints (both HMSC constraints and BMSC
- constraints may be present in an HMSC)</P>
-</UL>
-<P >Output: graph of nodes
-and edges between initial and terminal vertex in the input HMSC
-representing the possible paths in the HMSC. The paths, after
-sequential composition, form a set of BMSCs with time constraints.
-The input BMSC satisfies all the time constraints in every one of the
-BMSCs formed by paths from the start to the end node of the graph.</P>
-<h3>Example 2:</h3>
-
-<div style="margin: 0 auto;">
-<ul class="gallery">
-<li>
- <ul>
- <li><IMG SRC="pictures/memebership_11.png" width="250" BORDER="0" ALT="Input BMSC" TITLE="Input BMSC"></li>
- <li class="caption">Input BMSC</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_5.png" width="450" BORDER="0" ALT="Input HMSC" TITLE="Input HMSC"></li>
- <li class="caption">Input HMSC</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_6.png" width="250" BORDER="0" ALT="bMSC1" TITLE="bMSC1"></li>
- <li class="caption">bMSC1</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_7.png" width="250" BORDER="0" ALT="bMSC2" TITLE="bMSC2"></li>
- <li class="caption">bMSC2</li>
- </ul>
-</li>
-<li>
- <ul>
- <li><IMG SRC="pictures/memebership_8.png" width="250" BORDER="0" ALT="bMSC3" TITLE="bMSC3"></li>
- <li class="caption">bMSC3</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_9.png" width="250" BORDER="0" ALT="bMSC4" TITLE="bMSC4"></li>
- <li class="caption">bMSC4</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_10.png" width="250" BORDER="0" ALT="bMSC5" TITLE="bMSC5"></li>
- <li class="caption">bMSC5</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_12.png" width="350" BORDER="0" ALT="Result HMSC" TITLE="Result HMSC"></li>
- <li class="caption">Result HMSC</li>
- </ul>
-</li>
-</ul>
-</div>
-
-<P style="clear: both;">In the result there are only two paths through the <i>Input HMSC</i>. This is because only these two paths form BMSCs, which are satisfied by the <i>Input BMSC</i>. The path through <i>BMSC4</i> forms BMSC which is not satisfied by the <i>Input BMSC</i>. This is because the difference between send times of messages with caption <I>q</I> is 2, what is not included in time interval [8,9). Also there are only two possible iterations of the cycle containing <i>BMSC2</i>, because there are only two messages with caption <I>q</I> in the <i>Input BMSC</i>.</P>
-</BODY>
-</HTML>
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <title>
+ membership documentation
+ </title>
+ <link href="../help.css" rel="stylesheet" type="text/css" />
+ </head>
+ <body lang="en-US" dir="ltr" style="border: none; padding: 0in">
+ <h1>
+ Membership
+ </h1>
+ <p>
+ The problem of membership is deciding whether given BMSC is contained in a
+ given HMSC. It is possible to check both untimed and timed cases of BMSCs
+ and HMSCs.<br />
+ </p>
+ <h3>
+ Example 1:
+ </h3>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/memebership_4.png" width="250" border="0"
+ alt="Input bMSC" title="Input bMSC" />
+ </li>
+ <li class="caption">
+ Input BMSC
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/memebership_1.png" width="150" border="0"
+ alt="Input HMSC" title="Input HMSC" />
+ </li>
+ <li class="caption">
+ Input HMSC
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/memebership_2.png" width="250" border="0"
+ alt="bMSC01" title="bMSC01" />
+ </li>
+ <li class="caption">
+ bMSC01
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/memebership_3.png" width="250" border="0"
+ alt="bMSC02" title="bMSC02" />
+ </li>
+ <li class="caption">
+ bMSC02
+ </li>
+ </ul>
+ </li>
+ </ul>
+ <p>
+ In the figure above we have specified an input to the membership problem.
+ Every path from the initial node to the terminal node in a HMSC represents
+ a BMSC. There is only one path in the <i>Input HMSC</i>. The BMSC
+ specified by the path is formed from nodes (BMSCs) on the path by the
+ sequential composition (putting the BMSCs one after the other and gluing
+ the matching process lines). It is easy to see that the <i>Input BMSC</i>
+ is exactly the same BMSC represented by the only path in the <i>Input
+ HMSC</i>. The result of procedure solving membership problem should
+ be every successful path i.e. <i>Input HMSC</i>.
+ </p>
+ <p>
+ More formal specification of the procedure:
+ </p>
+ <p>
+ Input:
+ </p>
+ <ul>
+ <li>
+ <p>
+ BMSC with the timing assignment
+ </p>
+ </li>
+ <li>
+ <p>
+ MSC with timers and time constraints (both HMSC constraints and BMSC
+ constraints may be present in an HMSC)
+ </p>
+ </li>
+ </ul>
+ <p>
+ Output: graph of nodes and edges between initial and terminal vertex in
+ the input HMSC representing the possible paths in the HMSC. The paths,
+ after sequential composition, form a set of BMSCs with time constraints.
+ The input BMSC satisfies all the time constraints in every one of the
+ BMSCs formed by paths from the start to the end node of the graph.
+ </p>
+ <h3>
+ Example 2:
+ </h3>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/memebership_11.png" width="250" border="0"
+ alt="Input BMSC" title="Input BMSC" />
+ </li>
+ <li class="caption">
+ Input BMSC
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/memebership_5.png" width="450" border="0"
+ alt="Input HMSC" title="Input HMSC" />
+ </li>
+ <li class="caption">
+ Input HMSC
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/memebership_6.png" width="250" border="0"
+ alt="bMSC1" title="bMSC1" />
+ </li>
+ <li class="caption">
+ bMSC1
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/memebership_7.png" width="250" border="0"
+ alt="bMSC2" title="bMSC2" />
+ </li>
+ <li class="caption">
+ bMSC2
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/memebership_8.png" width="250" border="0"
+ alt="bMSC3" title="bMSC3" />
+ </li>
+ <li class="caption">
+ bMSC3
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/memebership_9.png" width="250" border="0"
+ alt="bMSC4" title="bMSC4" />
+ </li>
+ <li class="caption">
+ bMSC4
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/memebership_10.png" width="250" border="0"
+ alt="bMSC5" title="bMSC5" />
+ </li>
+ <li class="caption">
+ bMSC5
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/memebership_12.png" width="350" border="0"
+ alt="Result HMSC" title="Result HMSC" />
+ </li>
+ <li class="caption">
+ Result HMSC
+ </li>
+ </ul>
+ </li>
+ </ul>
+ <p>
+ In the result there are only two paths through the <i>Input HMSC</i>.
+ This is because only these two paths form BMSCs, which are satisfied by
+ the <i>Input BMSC</i>. The path through <i>BMSC4</i>
+ forms BMSC which is not satisfied by the <i>Input BMSC</i>. This
+ is because the difference between send times of messages with caption <i>q</i>
+ is 2, what is not included in time interval [8,9). Also there are only two
+ possible iterations of the cycle containing <i>BMSC2</i>, because
+ there are only two messages with caption <i>q</i> in the <i>Input
+ BMSC</i>.
+ </p>
+ </body>
+</html>
Deleted: trunk/doc/help/membership/memebership_1.png
===================================================================
(Binary files differ)
Deleted: trunk/doc/help/membership/memebership_10.png
===================================================================
(Binary files differ)
Deleted: trunk/doc/help/membership/memebership_11.png
===================================================================
(Binary files differ)
Deleted: trunk/doc/help/membership/memebership_12.png
===================================================================
(Binary files differ)
Deleted: trunk/doc/help/membership/memebership_2.png
===================================================================
(Binary files differ)
Deleted: trunk/doc/help/membership/memebership_3.png
===================================================================
(Binary files differ)
Deleted: trunk/doc/help/membership/memebership_4.png
===================================================================
(Binary files differ)
Deleted: trunk/doc/help/membership/memebership_5.png
===================================================================
(Binary files differ)
Deleted: trunk/doc/help/membership/memebership_6.png
===================================================================
(Binary files differ)
Deleted: trunk/doc/help/membership/memebership_7.png
===================================================================
(Binary files differ)
Deleted: trunk/doc/help/membership/memebership_8.png
===================================================================
(Binary files differ)
Deleted: trunk/doc/help/membership/memebership_9.png
===================================================================
(Binary files differ)
Modified: trunk/doc/help/race/race.html
===================================================================
--- trunk/doc/help/race/race.html 2010-09-13 13:40:13 UTC (rev 918)
+++ trunk/doc/help/race/race.html 2010-09-13 14:23:33 UTC (rev 919)
@@ -1,64 +1,110 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
-<HTML>
-<HEAD>
- <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
- <TITLE>Race Condition</TITLE>
- <meta name="author" content="Martin Chmelik">
- <LINK href="../help.css" rel="stylesheet" type="text/css"/>
-</HEAD>
-<BODY>
-<H1>Race Condition</H1>
-<P>
-Informally, two events are in race if they are specified by user to perform in some order, but there is a possibility that they can perform in an inverse order.
-Race condition occurs in a BMSC whenever a pair of events is drawn in a particular order but there exists a execution with a different order. If the real implementation is based on the BMSC specification, it may lead to a system failure. Do not mix up race condition with <a href="../fifo/fifo.html">FIFO</a>; race condition is only applicable for BMSCs that satisfy FIFO.</P>
-<P>SCStudio finds all pairs of events in a given BMSC and also in BMSCs referenced by an HMSC. On the next picture there is an example of an BMSC which contains race condition:
+<?xml version="1.0" encoding="utf-8"?>
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul >
- <li><IMG SRC="pictures/easyrace_1.png" width="300" BORDER="0" ALT="Input BMSC" TITLE="Input BMSC"></li>
- <li class="caption">Input BMSC</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/easyrace_2.png" width="300" BORDER="0" ALT="Possible execution" TITLE="Possible execution"></li>
- <li class="caption">Possible execution</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/easyrace_result.png" width="300" BORDER="0" ALT="SCStudio result" TITLE="SCStudio result"></li>
- <li class="caption">SCStudio result</li>
- </ul>
-</li>
-</ul>
-</div>
-<p style="clear: both;">
-The race condition may also occur between events from different BMSC within an HMSC. HMSC contains race if there exists path which contains a race. SCStudio is capable of finding one such occurrence:</P>
+<!DOCTYPE html
+ PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd" >
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/trickyrace_1.png" width="100" BORDER="0" ALT="Input HMSC" TITLE="Input HMSC"></li>
- <li class="caption">Input HMSC with a race</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/trickyrace_2.png" width="300" BORDER="0" ALT="MSC A" TITLE="MSC A"></li>
- <li class="caption">MSC A</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/trickyrace_3.png" width="300" BORDER="0" ALT="MSC B" TITLE="MSC B"></li>
- <li class="caption">MSC B</li>
- </ul>
-</li>
-</ul>
-</div>
-
-</BODY>
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <title>
+ Race Condition
+ </title>
+ <meta name="author" content="Martin Chmelik" />
+ <link href="../help.css" rel="stylesheet" type="text/css" />
+ </head>
+ <body>
+ <h1>
+ Race Condition
+ </h1>
+ <p>
+ Informally, two events are in race if they are specified by user to
+ perform in some order, but there is a possibility that they can perform in
+ an inverse order. Race condition occurs in a BMSC whenever a pair of
+ events is drawn in a particular order but there exists a execution with a
+ different order. If the real implementation is based on the BMSC
+ specification, it may lead to a system failure. Do not mix up race
+ condition with <a href="../fifo/fifo.html">FIFO</a>; race
+ condition is only applicable for BMSCs that satisfy FIFO.
+ </p>
+ <p>
+ SCStudio finds all pairs of events in a given BMSC and also in BMSCs
+ referenced by an HMSC. On the next picture there is an example of an BMSC
+ which contains race condition:
+ </p>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/easyrace_1.png" width="300" border="0"
+ alt="Input BMSC" title="Input BMSC" />
+ </li>
+ <li class="caption">
+ Input BMSC
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/easyrace_2.png" width="300" border="0"
+ alt="Possible execution" title="Possible execution" />
+ </li>
+ <li class="caption">
+ Possible execution
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/easyrace_result.png" width="300" border="0"
+ alt="SCStudio result" title="SCStudio result" />
+ </li>
+ <li class="caption">
+ SCStudio result
+ </li>
+ </ul>
+ </li>
+ </ul>
+ <p>
+ The race condition may also occur between events from different BMSC
+ within an HMSC. HMSC contains race if there exists path which contains a
+ race. SCStudio is capable of finding one such occurrence:
+ </p>
+ <ul class="gallery">
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/trickyrace_1.png" width="100" border="0"
+ alt="Input HMSC" title="Input HMSC" />
+ </li>
+ <li class="caption">
+ Input HMSC with a race
+ </li>
+ </ul>
+ </li>
+ <li>
+ <ul>
+ <li>
+ <img src="pictures/trickyrace_2.png" width="300" border="0"
+ alt="MSC A" title="MSC A" /...
[truncated message content] |
