Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[878] trunk/doc/help
|
From: <ag...@us...> - 2010-09-07 10:14:32
|
Revision: 878
http://scstudio.svn.sourceforge.net/scstudio/?rev=878&view=rev
Author: agmy
Date: 2010-09-07 10:14:23 +0000 (Tue, 07 Sep 2010)
Log Message:
-----------
help, remove ~files
Removed 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/frontend/shortcuts.html~
trunk/doc/help/livelock/livelock.html~
trunk/doc/help/localchoice/localchoice.html~
trunk/doc/help/membership/membership.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~
Deleted: trunk/doc/help/acyclic/acyclic.html~
===================================================================
--- trunk/doc/help/acyclic/acyclic.html~ 2010-09-07 09:03:38 UTC (rev 877)
+++ trunk/doc/help/acyclic/acyclic.html~ 2010-09-07 10:14:23 UTC (rev 878)
@@ -1,46 +0,0 @@
-<!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>
-
-
-<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>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>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><li>
- <ul>
- <li><IMG SRC="pictures/acyclic.png" width="250" BORDER="0" ALT="Acyclic BMSC" TITLE="Acyclic BMSC"></li>
- <li>Acyclic design</li>
- </ul>
-</li>
-</ul>
-</div>
-
-</BODY>
Deleted: trunk/doc/help/beautify/beautify.html~
===================================================================
--- trunk/doc/help/beautify/beautify.html~ 2010-09-07 09:03:38 UTC (rev 877)
+++ trunk/doc/help/beautify/beautify.html~ 2010-09-07 10:14:23 UTC (rev 878)
@@ -1,78 +0,0 @@
-<!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>
-
-<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>Before beautify</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/ordered.png" align="middle" " width="350" BORDER="0" ALT="Ordered BMSC"></li>
- <li>After beautify</li>
- </ul>
-</li>
-</ul>
-</div>
-<p style="clear: both;">
-
-<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>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>Before beautify</li>
- </ul></li>
-<li>
- <ul>
-
- <li>
- <img src="pictures/coregion2.png" width="250 "alt=""></li>
- <li>After beautify</li>
- </ul>
-</li>
-</ul>
-</div>
-
-</BODY>
-</HTML>
Deleted: trunk/doc/help/boundedness/boundedness.html~
===================================================================
--- trunk/doc/help/boundedness/boundedness.html~ 2010-09-07 09:03:38 UTC (rev 877)
+++ trunk/doc/help/boundedness/boundedness.html~ 2010-09-07 10:14:23 UTC (rev 878)
@@ -1,37 +0,0 @@
-<!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 dialogue 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>
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/unbounded_hmsc.png" width="250" BORDER="0" ALT="Unbounded HMSC" TITLE="Unbounded HMSC"></li>
- <li>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>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>
Deleted: trunk/doc/help/deadlock/deadlock.html~
===================================================================
--- trunk/doc/help/deadlock/deadlock.html~ 2010-09-07 09:03:38 UTC (rev 877)
+++ trunk/doc/help/deadlock/deadlock.html~ 2010-09-07 10:14:23 UTC (rev 878)
@@ -1,31 +0,0 @@
-<!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>
-
-<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 highlited 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="250" BORDER="0" ALT="Typical deadlock" TITLE="Typical deadlock"></li>
- <li>Typical deadlock</li>
- </ul>
-</li>
-</ul>
-</div>
-
-</BODY>
Deleted: trunk/doc/help/fifo/fifo.html~
===================================================================
--- trunk/doc/help/fifo/fifo.html~ 2010-09-07 09:03:38 UTC (rev 877)
+++ trunk/doc/help/fifo/fifo.html~ 2010-09-07 10:14:23 UTC (rev 878)
@@ -1,107 +0,0 @@
-<!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>
-
-<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>
-
-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>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>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>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 messege <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>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>
-
-<img src="pictures/label_channel_fifo.png" border="0" alt="FIFO MSC design" title="FIFO MSC design">
-
-<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>
Deleted: trunk/doc/help/frontend/shortcuts.html~
===================================================================
--- trunk/doc/help/frontend/shortcuts.html~ 2010-09-07 09:03:38 UTC (rev 877)
+++ trunk/doc/help/frontend/shortcuts.html~ 2010-09-07 10:14:23 UTC (rev 878)
@@ -1,21 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
-<html>
-<head>
-<title>SCStudio Visio addon keyboard accelerators</title>
-<link href="../help.css" rel="stylesheet" type="text/css">
-</head>
-<body>
-<h1>Visio addon keyboard accelerators</h1>
-<p>The following keyboard accelerators are defined by SCStudio Visio addon:</p>
-<table>
-<col width="100"> <col>
-<tr><td><code>Ctrl+Alt+I</code></td><td><a href="shape-selection.html">Select all instances</a></td></tr>
-<tr><td><code>Ctrl+Alt+M</code></td><td><a href="shape-selection.html">Select all message</a></td></tr>
-<tr><td><code>Ctrl+Alt+F</code></td><td><a href="automatic-drawing.html#add_instances">Add instances</a></td></tr>
-<tr><td><code>Ctrl+Alt+S</code></td><td><a href="automatic-drawing.html#message_sequence">Message sequence</a></td></tr>
-<tr><td><code>Ctrl+Alt+E</code></td><td><a href="message-numbering.html">Message Numbering</a></td></tr>
-<tr><td><code>Ctrl+Alt+D</code></td><td><a href="message-numbering.html">Delete message numbering</a></td></tr>
-</table>
-
-</body>
-</html>
Deleted: trunk/doc/help/livelock/livelock.html~
===================================================================
--- trunk/doc/help/livelock/livelock.html~ 2010-09-07 09:03:38 UTC (rev 877)
+++ trunk/doc/help/livelock/livelock.html~ 2010-09-07 10:14:23 UTC (rev 878)
@@ -1,25 +0,0 @@
-<!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>
-
-<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>
-
-<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>Typical livelock</li>
- </ul>
-</li>
-</ul>
-</div>
-</BODY>
Deleted: trunk/doc/help/localchoice/localchoice.html~
===================================================================
--- trunk/doc/help/localchoice/localchoice.html~ 2010-09-07 09:03:38 UTC (rev 877)
+++ trunk/doc/help/localchoice/localchoice.html~ 2010-09-07 10:14:23 UTC (rev 878)
@@ -1,72 +0,0 @@
-<!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 nonspecified implied behavior. </P>
-
-<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>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>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>MSC B</li>
- </ul>
-</li>
-</ul>
-</div>
-
-<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>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>Implied behavior</li>
- </ul>
-</li>
-</ul>
-</div>
-
-
-<DIV class="gallery vary">
-<table><caption align="bottom"><i>Result of SCStudio</i></caption><tr><td>
-<IMG SRC="pictures/simple_nonlocal_result.png" BORDER="0" ALT="Result of SCStudio" TITLE="Result of SCStudio">
-</tr></td></table>
-<DIV class="gallery vary">
-<table><caption align="bottom"><i>Implied behavior</i></caption><tr><td>
-<IMG SRC="pictures/simple_nonlocal_implied.png" BORDER="0" ALT="Implied behavior" TITLE="Implied behavior">
-</tr></td></table>
-</BODY>
Deleted: trunk/doc/help/membership/membership.html~
===================================================================
--- trunk/doc/help/membership/membership.html~ 2010-09-07 09:03:38 UTC (rev 877)
+++ trunk/doc/help/membership/membership.html~ 2010-09-07 10:14:23 UTC (rev 878)
@@ -1,135 +0,0 @@
-<!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>
-
-<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>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>Input HMSC</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_2.png" width="250" BORDER="0" ALT="bMSC01" TITLE="bMSC01"></li>
- <li>bMSC01</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_3.png" width="250" BORDER="0" ALT="bMSC02" TITLE="bMSC02"></li>
- <li>bMSC02</li>
- </ul>
-</li>
-</ul>
-</div>
-
-<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>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>Input HMSC</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_6.png" width="250" BORDER="0" ALT="bMSC1" TITLE="bMSC1"></li>
- <li>bMSC1</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_7.png" width="250" BORDER="0" ALT="bMSC2" TITLE="bMSC2"></li>
- <li>bMSC2</li>
- </ul>
-</li>
-<li>
- <ul>
- <li><IMG SRC="pictures/memebership_8.png" width="250" BORDER="0" ALT="bMSC3" TITLE="bMSC3"></li>
- <li>bMSC3</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_9.png" width="250" BORDER="0" ALT="bMSC4" TITLE="bMSC4"></li>
- <li>bMSC4</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_10.png" width="250" BORDER="0" ALT="bMSC5" TITLE="bMSC5"></li>
- <li>bMSC5</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/memebership_12.png" width="450" BORDER="0" ALT="Result HMSC" TITLE="Result HMSC"></li>
- <li>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>
Deleted: trunk/doc/help/time_consistency/time_consistency.html~
===================================================================
--- trunk/doc/help/time_consistency/time_consistency.html~ 2010-09-07 09:03:38 UTC (rev 877)
+++ trunk/doc/help/time_consistency/time_consistency.html~ 2010-09-07 10:14:23 UTC (rev 878)
@@ -1,44 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
-<HTML>
-<HEAD>
- <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
- <TITLE>Time Consistency</TITLE>
- <meta name="author" content="Martin Chmelik">
- <LINK href="../help.css" rel="stylesheet" type="text/css"/>
-</HEAD>
-<BODY>
-<H1>Time Consistency</H1>
-<P>Time consistency is a problem of deciding whether introduced time constraints in a given MSC are in conflict. MSC is time consistent if it is without such conflicting time constraints.</P>
-<p> The motivation for time consitency is following. It can easily happen that user can specify too restrictive time constraints and cause that the set of behaviors is empty. The time consistency property checks such situations.
-<H2>Basic Message Sequence Chart</H2>
-<P>Time consistent property is violated for BMSC <I>B</I> when there is no valid time assignment for B.</P>
-<P>The time assignment for BMSC (resp. HMSC path) is an assignment of time value to every event, such that it satisfies all constraints in a given BMSC (resp. HMSC path). I.e. for every constraint which restricts two events, the difference of values assigned by assignment to these events must be included in the interval set of this constraint.</P>
-<P>An example of a time consistent BMSC is depicted on the next picture.</P>
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/cons1.png" width="250" BORDER="0" ALT="Time inconsistent BMSC" TITLE="Time inconsistent BMSC"></li>
- <li>Time inconsistent BMSC</li>
- </ul>
-</li>
-</ul>
-</div>
-<p style="clear: both;">
-<H2>High-level MSC</H2>
-
-<P>HMSC violates time consistent property if exists path from start node to end node for which there is no time assignment.</P>
-<P>An example of time inconsistent HMSC is depicted on the next picture. The inconsistency follows from the fact that the two inner constraints are too short compared to the outer constraint. That is why it is not possible for the events in the HMSC to satisfy all constraints.</P>
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/cons2.png" width="250" BORDER="0" ALT="Time inconsistent HMSC" TITLE="Time inconsistent HMSC"></li>
- <li>Time inconsistent HMSC</li>
- </ul>
-</li>
-</ul>
-</div>
-
-</BODY>
-</HTML>
Deleted: trunk/doc/help/time_syntax/time_syntax.html~
===================================================================
--- trunk/doc/help/time_syntax/time_syntax.html~ 2010-09-07 09:03:38 UTC (rev 877)
+++ trunk/doc/help/time_syntax/time_syntax.html~ 2010-09-07 10:14:23 UTC (rev 878)
@@ -1,61 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
-<HTML>
-<HEAD>
- <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
- <TITLE>Correct Time Constraint Syntax</TITLE>
- <meta name="author" content="Lubos Korenciak">
- <LINK href="../help.css" rel="stylesheet" type="text/css"/>
-</HEAD>
-<BODY>
-<H1>Correct Time Constraint Syntax</H1>
-<P>The correct time constraint syntax algorithm is used for checking whether introduced time constraints are correct to use in SCStudio. The main motivation for such test is to rule out time constraints which are either not allowed by the standard or ambiguous.
-</P>
-<P>The following conditions must hold for every time constraint to suffice correct time constraint syntax algorithm:
-<ul>
-<li>if the constraint is in BMSC it has to restrict events which are visually ordered </li>
-<li>if the constraint is in HMSC and it restricts nodes A and B, every path going through A (resp. B) must go through B (resp. A) and it cannot go twice through A (resp. B) without going through node B (resp. A) in between.</li>
-</ul> </p>
-
-<P>An example of a time constraint can be seen on the next picture. Receive events of <I>HTTP Response</I> and send event <I>HTTP Request</I> messages are not visually ordered. Thus the time constraint does not satisfy the correct time constraint syntax property. </P>
-
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/syntax3.png" width="350" BORDER="0" ALT="Example of a wrong time constraint" TITLE="Example of a wrong time constraint"></li>
- <li>Example of a wrong time constraint</li>
- </ul>
-</li>
-</ul>
-</div>
-<p style="clear: both;">
-
-
-<P>On the next picture we see that there exists path which goes twice in a row through the node <I>Connection denied</I> and thus the introduced time constraint also does not satisfy the correct time constraint syntax property.</P>
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/syntax1.png" width="250" BORDER="0" ALT="Violation of constraint syntax" TITLE="Violation of constraint syntax"></li>
- <li>Violation of constraint syntax</li>
- </ul></li>
-</ul>
-</div>
-
-<p style="clear: both;">
-
-<P>The last example depicts a HMSC where exists path which goes through the node A of but does not go through the node B. Since there is introduced time constraint restricting these nodes, it violates the correct time constraint syntax property.</P>
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/syntax2.png" width="350" BORDER="0" ALT="Example of a wrong time constraint" TITLE="Example of a wrong time constraint"></li>
- <li>Example of a wrong time constraint</li>
- </ul></li>
-</ul>
-</div>
-
-<p style="clear: both;">
-
-</BODY>
-</HTML>
Deleted: trunk/doc/help/time_tighten/time_tighten.html~
===================================================================
--- trunk/doc/help/time_tighten/time_tighten.html~ 2010-09-07 09:03:38 UTC (rev 877)
+++ trunk/doc/help/time_tighten/time_tighten.html~ 2010-09-07 10:14:23 UTC (rev 878)
@@ -1,102 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
-<HTML>
-<HEAD>
- <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
- <TITLE>Tighten Time</TITLE>
- <meta name="author" content="Lubos Korenciak">
- <LINK href="../help.css" rel="stylesheet" type="text/css"/>
-</HEAD>
-<BODY>
-<H1>Tighten Time</H1>
-<P>The purpose of the tighten time algorithm is to shorten interval sets of time constraints to minimal possible values. It deletes every value of time constraints which cannot be used due to other more restrictive time constraints.
-</P>
-<H3> Basic MSC</H3>
-<P>After the tighten time algorithm, every constraint contains only values in interval sets for which exists valid time assignment.</p>
-<P>The time assignment for BMSC (resp. HMSC path) is an assignment of time value to every event such that it satisfies all constraints in given BMSC (resp. HMSC path). I.e. for every constraint which restricts two events, the difference of values assigned by the assignment to these events must be included in the interval set of this constraint.</P>
-
-<P>An example of the tighten time algorithm on a BMSC is shown on the next picture. The time constraint which contains value (0,10) has to be changed to [5,10) because the communication turnover takes at least 5 time units.</P>
-
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/tighten2_1.png" width="350" BORDER="0" ALT="Original BMSC" TITLE="Original BMSC"></li>
- <li>Original BMSC</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/tighten2_2.png" width="350" BORDER="0" ALT="Tightened BMSC" TITLE="Tightened BMSC"></li>
- <li>Tightened BMSC</li>
- </ul>
-</li>
-</ul>
-</div>
-
-<p style="clear: both;">
-
-<H3> High-level MSC</H3>
-<P>After the tighten time algorithm, every constraint contains only values in interval sets for which exists valid time assignment for some path from the start node to an end node.</p>
-<P>An example of the tighten time algorithm on a HMSC is shown on the next picture. The constraints change because of the following reasons:
-<ul>
-<li> the constraint on the node <I> B </I> changes because of the <i>Original BMSC B</i> </li>
-<li> the lower bound of the constraint between the nodes <I>A</I> and <I>B</I> changes to 8 because the lower bound of the first path is 9 and the lower bound of the second path is 8</li>
-<li> the <i>Original BMSC A</i> tightens to the <i>Tightened BMSC A</i> because of the both constraints on the nodes <I> A </I> (the upper bound is derived from the constraint containing [3,5] and the lower bound from the constraint containing [2,8]) </li>
-<li> the upper bound of the HMSC constraint originally containing [3,5] is tightened to 5 (not included) because the candidates for the upper bound is the lower value from upper bound 5 (from the original constraint) and the value derived from constraints containing, (8,10], (3,4] and [2,8]. We have to compute the upper bound candidate from the values of the time intervals. Since we can stay at least 3 (not included) time units in the first node <I> A </I> and at least 2 time units in the node <I>B</I> and we can stay at most 10 time units in the whole execution we get that we can stay at most 10 - 3 - 2 = 5 (not included) time units in second node <I> A </I>. Thus the original constraint (with the value [3,5]) will contain [3,5) after the execution of the tightening algorithm.</li>
-<li> the upper bound of the constraint containing originally [2,8] tightens to 4 (not included), bacause the possible upper bound for this constraint derived from the first path is 10 - 4 - 3 = 3 (not included) and from the second path it is 10 - 3 - 3 = 4 (not included). </li>
-</ul>
-</P>
-
-<h4> Before:</h4>
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/tighten1_1.png" width="350" BORDER="0" ALT="Original HMSC" TITLE="Original HMSC"></li>
- <li>Original HMSC</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/tighten1_2.png" width="250" BORDER="0" ALT="Original BMSC A" TITLE="Original BMSC A"></li>
- <li>Original BMSC A</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/tighten1_3.png" width="250" BORDER="0" ALT="Original BMSC B" TITLE="Original BMSC B"></li>
- <li>Original BMSC B</li>
- </ul>
-</li>
-
-</ul>
-</div>
-
-<p style="clear: both;">
-
-<table><caption align="bottom"><i>Original HMSC</i></caption><tr><td>
-<img src="pictures/tighten1_1.png" border="0" alt="Original HMSC" title="Original HMSC">
-</tr></td></table>
-
-<table><caption align="bottom"><i>Original BMSC A</i></caption><tr><td>
-<img src="pictures/tighten1_2.png" border="0" alt="Original BMSC A" title="Original BMSC A">
-</tr></td></table>
-
-<table><caption align="bottom"><i>Original BMSC B</i></caption><tr><td>
-<img src="pictures/tighten1_3.png" border="0" alt="Original BMSC B" title="Original BMSC B">
-</tr></td></table>
-
-<table><caption align="bottom"><i>Tightened HMSC</i></caption><tr><td>
-<img src="pictures/tighten1_4.png" border="0" alt="Tightened HMSC" title="Tightened HMSC">
-</tr></td></table>
-
-<table><caption align="bottom"><i>Tightened BMSC A</i></caption><tr><td>
-<img src="pictures/tighten1_5.png" border="0" alt="Tightened BMSC A" title="Tightened BMSC A">
-</tr></td></table>
-
-<table><caption align="bottom"><i>Tightened BMSC B</i></caption><tr><td>
-<img src="pictures/tighten1_6.png" border="0" alt="Tightened BMSC B" title="Tightened BMSC B">
-</tr></td></table>
-
-</BODY>
-</HTML>
Deleted: trunk/doc/help/time_trace_race/time_race.html~
===================================================================
--- trunk/doc/help/time_trace_race/time_race.html~ 2010-09-07 09:03:38 UTC (rev 877)
+++ trunk/doc/help/time_trace_race/time_race.html~ 2010-09-07 10:14:23 UTC (rev 878)
@@ -1,66 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
-<HTML>
-<HEAD>
- <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
- <TITLE>Time Race</TITLE>
- <meta name="author" content="Lubos Korenciak">
- <LINK href="../help.css" rel="stylesheet" type="text/css"/>
-</HEAD>
-<BODY>
-<H1>Time Race</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 inverse order.</P>
-<P> The introduction of time constraints can eliminate some race conditions. For example consider the next two pictures. On the first one there is a time race between <I>HTTP Request</I> and <I>HTTP Response</I> receive events. However on the second one the added time constraint caused that the BMSC is time race free (the receive event of <I>HTTP Request</I> surely happens after the <I>HTTP Response</I> receive event). </P>
-
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/race1_1.png" width="350" BORDER="0" ALT="BMSC with the time race" TITLE="BMSC with the time race"></li>
- <li>BMSC with the time race</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/race1_2.png" width="350" BORDER="0" ALT="Time race free BMSC" TITLE="Time race free BMSC"></li>
- <li>Time race free BMSC</li>
- </ul>
-</li>
-</ul>
-</div>
-
-<p style="clear: both;">
-
-<P>BMSC B (resp. HMSC path p) contains time race if there are two visually ordered events in B (resp. p), but there exists time assignment which assigns the visually preceding event larger time value than the value assigned to the subsequent event.</P>
-<P>An HMSC contains time race if there exists path which contains time race. </P>
-<P>The time assignment for BMSC (resp. HMSC path) is an assignment of time value to every event such that it satisfies all constraints in given BMSC (resp. HMSC path). I.e. for every constraint which restricts two events, the difference of values assigned by the assignment to these events must be included in the interval set of this constraint.</P>
-<P>Time Race algortihm checks the same as the <a href="../race/race.html">race checker</a>, but takes into account also time constraints.</P>
-<P>The next example shows HMSC which contains race condition (between <I>HTTP Request</I> and <I>HTTP Response</I> receive events), but which is time race free. Due to time constraints the <I>HTTP Request</I>receive event happens allways before the <I>HTTP Response</I> receive event. </P>
-
-<div style="margin: 0 auto;">
-<ul class="gallery"><li>
- <ul>
- <li><IMG SRC="pictures/race2_1.png" width="250" BORDER="0" ALT="Example of time race free HMSC" TITLE="Example of time race free HMSC"></li>
- <li>Example of time race free HMSC</li>
- </ul></li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/race2_2.png" width="250" BORDER="0" ALT="BMSC A" TITLE="BMSC A"></li>
- <li>BMSC A</li>
- </ul>
-</li>
-<li>
- <ul>
-
- <li><IMG SRC="pictures/race2_3.png" width="250" BORDER="0" ALT="BMSC B" TITLE="BMSC B"></li>
- <li>BMSC B</li>
- </ul>
-</li>
-</ul>
-</div>
-
-<p style="clear: both;">
-
-</BODY>
-</HTML>
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
