Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[817] trunk/doc/help
|
From: <lko...@us...> - 2010-06-09 22:45:29
|
Revision: 817
http://scstudio.svn.sourceforge.net/scstudio/?rev=817&view=rev
Author: lkorenciak
Date: 2010-06-09 22:45:23 +0000 (Wed, 09 Jun 2010)
Log Message:
-----------
added few descriptions of pictures in Help
Modified Paths:
--------------
trunk/doc/help/boundedness/boundedness.html
trunk/doc/help/deadlock/deadlock.html
trunk/doc/help/fifo/fifo.html
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/time_consistency/time_consistency.html
trunk/doc/help/time_tighten/time_tighten.html
trunk/doc/help/time_trace_race/time_race.html
Modified: trunk/doc/help/boundedness/boundedness.html
===================================================================
--- trunk/doc/help/boundedness/boundedness.html 2010-06-09 17:11:08 UTC (rev 816)
+++ trunk/doc/help/boundedness/boundedness.html 2010-06-09 22:45:23 UTC (rev 817)
@@ -1,17 +1,17 @@
-<!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 limit 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, the 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>
-<img src="unbounded.png" alt="Unbounded HMSC">
-</BODY>
+<!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 limit 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, the 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>TODO add description of the picture here... </P>
+<p>
+<img src="unbounded.png" alt="Unbounded HMSC">
+</BODY>
Modified: trunk/doc/help/deadlock/deadlock.html
===================================================================
--- trunk/doc/help/deadlock/deadlock.html 2010-06-09 17:11:08 UTC (rev 816)
+++ trunk/doc/help/deadlock/deadlock.html 2010-06-09 22:45:23 UTC (rev 817)
@@ -11,9 +11,13 @@
<P>is a property of an HMSC node. An HMSC node is deadlocked if there is no reference node or end node reachable from the node, i.e. after the execution of the MSC 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 available/suggested/given as example of the deadlock.
+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 example of the deadlock.
</P>
+<P>
+In the next picture the node B is clearly a deadlocked node. That is why it is highlited by SCStudio and given as an example/ to show the deadlock.
+</P>
+
<p>
<img src="deadlock.png" alt="Typical deadlock">
Modified: trunk/doc/help/fifo/fifo.html
===================================================================
--- trunk/doc/help/fifo/fifo.html 2010-06-09 17:11:08 UTC (rev 816)
+++ trunk/doc/help/fifo/fifo.html 2010-06-09 22:45:23 UTC (rev 817)
@@ -10,7 +10,20 @@
<H1>FIFO property</H1>
<P>FIFO (First In, First Out) is a property of an MSC. The property ensures that it is possible
to implement the desired behavior without deadlocks, that would be
-caused by attributes/behavior of channels.</P>
+caused by behavior of channels.</P>
+
+<P>
+There are several types of channels and several ways how they can be used im MSC. 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
@@ -30,12 +43,12 @@
a, b (a,c form the first message and b,d form the second message) it holds that
c < d => a < b, where < is the visual order and the two messages belong
to the same channel.</P>
-<P>Tricky examples of FIFO MSCs:</P>
+<P>Tricky examples of FIFO MSCs: 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 sapecified that the receive events can happen in arbitrary order. So that if we any order of these two events in the head of the channel queue, the system will certainly not reach deadlock.</P>
<img src="pictures/fifo1.png" border="0" alt="FIFO MSC design" title="FIFO MSC design">
<img src="pictures/fifo2.png" border="0" alt="FIFO MSC design" title="FIFO MSC design">
-<P>An example of a non-FIFO design can be seen on the following picture:</P>
+<P>An example of a non-FIFO design can be seen on the following picture. This is because the Instance q can execute only the receive event of message <I>m1</I> first/before/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>
<img src="pictures/nonfifo1.png" border="0" alt="non-FIFO MSC design" title="non-FIFO MSC design">
<H3>FIFO channel for every pair of instances and labels</H3>
@@ -45,13 +58,15 @@
<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/specified by the HMSC satisfies FIFO property
-for that channel type:</P>
+type, if every BMSC represented by the HMSC satisfies the FIFO property
+for that channel type.</P>
</BODY>
</HTML>
Modified: trunk/doc/help/livelock/livelock.html
===================================================================
--- trunk/doc/help/livelock/livelock.html 2010-06-09 17:11:08 UTC (rev 816)
+++ trunk/doc/help/livelock/livelock.html 2010-06-09 22:45:23 UTC (rev 817)
@@ -1,16 +1,16 @@
-<!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><img src="livelock.png" alt="Typical livelock"></P>
-</BODY>
+<!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>
+<P><img src="livelock.png" alt="Typical livelock"></P>
+</BODY>
Modified: trunk/doc/help/localchoice/localchoice.html
===================================================================
--- trunk/doc/help/localchoice/localchoice.html 2010-06-09 17:11:08 UTC (rev 816)
+++ trunk/doc/help/localchoice/localchoice.html 2010-06-09 22:45:23 UTC (rev 817)
@@ -8,7 +8,7 @@
</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 MSC A or MSC B) are possible and the branches are initiated by different instances (MSC A is initiated by instance p, MSC B is initiated by instance q). Therefore the resulting behavior of the system may contain a combination of both branches, resulting in a nonspecified implied behavior. </P>
+<P>is a property of an HMSC node, that has more than one successor, occurring when multiple different behaviors (branches MSC A or MSC B) are possible and the branches are initiated by different instances (MSC A is initiated by the Instance p, MSC B is initiated by the Instance q). Therefore the resulting behavior of the system may contain a combination of both branches, resulting in a nonspecified implied behavior. </P>
<DIV class="gallery vary">
<table><caption align="bottom"><i>HMSC</i></caption><tr><td>
<IMG SRC="pictures/simple_nonlocal.png" BORDER="0" ALT="HMSC specification with a branching node" title="HMSC specification with a branching node">
Modified: trunk/doc/help/membership/membership.html
===================================================================
--- trunk/doc/help/membership/membership.html 2010-06-09 17:11:08 UTC (rev 816)
+++ trunk/doc/help/membership/membership.html 2010-06-09 22:45:23 UTC (rev 817)
@@ -34,13 +34,13 @@
<br clear="all">
<P >In the figure above we
-have specified input to the membership problem. Every path from
-initial node to 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 sequential composition
+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
+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
@@ -48,7 +48,7 @@
<P >Input:
</P>
<UL>
- <LI><P >BMSC with timing
+ <LI><P >BMSC with the timing
assignment</P>
<LI><P >MSC with timers
and time constraints (both HMSC constraints and BMSC
@@ -59,7 +59,7 @@
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.</P>
+BMSCs formed by paths from the start to the end node of the graph.</P>
<P >Example 2:</P>
<DIV class="gallery vary">
@@ -97,6 +97,6 @@
</div>
<br clear="all">
-<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 through <i>bMSC2</i>, because there are only two messages with caption <I>q</I> in the <i>Input BMSC</i>.</P>
+<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 going through/containing <i>BMSC2</i>, because there are only two messages with caption <I>q</I> in the <i>Input BMSC</i>.</P>
</BODY>
</HTML>
\ No newline at end of file
Modified: trunk/doc/help/race/race.html
===================================================================
--- trunk/doc/help/race/race.html 2010-06-09 17:11:08 UTC (rev 816)
+++ trunk/doc/help/race/race.html 2010-06-09 22:45:23 UTC (rev 817)
@@ -1,13 +1,15 @@
-<!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>Race Condition occurs in an MSC if a pair of events is drawn in a particular order but the events may occur in the other order during an execution of the MSC. If the real implementation is based on the drawing, it may lead to a system failure. Please don't mix up race condition with <a href="../fifo/fifo.html">FIFO</a>; race condition is only applicable for MSCs that satisfy FIFO.</P>
-<P>SCStudio currently finds all such pairs of events in a given BMSC and also in BMSCs referenced by a HMSC. The race condition may also occur between events from different BMSC. SCStudio is capable of finding one such occurence.</P>
-</BODY>
+<!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>Race Condition occurs in an MSC if a pair of events is drawn in a particular order but the events may occur in the other order during an execution of the MSC. If the real implementation is based on the drawing, it may lead to a system failure. Please don't mix up race condition with <a href="../fifo/fifo.html">FIFO</a>; race condition is only applicable for MSCs that satisfy FIFO.</P>
+<P>SCStudio currently finds all such pairs of events in a given BMSC and also in BMSCs referenced by a HMSC. The race condition may also occur between events from different BMSC. SCStudio is capable of finding one such occurence.</P>
+
+<P>On the next picture there is an example of an BMSC which contains race condition. The receive events of messages ... but it is possibele that...</P>
+</BODY>
Modified: trunk/doc/help/time_consistency/time_consistency.html
===================================================================
--- trunk/doc/help/time_consistency/time_consistency.html 2010-06-09 17:11:08 UTC (rev 816)
+++ trunk/doc/help/time_consistency/time_consistency.html 2010-06-09 22:45:23 UTC (rev 817)
@@ -9,7 +9,7 @@
<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 constraint and cause that the set of executions/behaviors which satisfy MSC is empty. The time consistency property checks such situations.
+<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 which satisfy MSC is empty. The time consistency property checks such situations.
<H2>Basic Message Sequence Chart</H2>
<P>Time consistent property is violated for BMSC B when there is no 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 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>
@@ -19,7 +19,7 @@
<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.</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>
<img src="pictures/cons2.png" border="0" alt="Time inconsistent HMSC" title="Time inconsistent HMSC">
Modified: trunk/doc/help/time_tighten/time_tighten.html
===================================================================
--- trunk/doc/help/time_tighten/time_tighten.html 2010-06-09 17:11:08 UTC (rev 816)
+++ trunk/doc/help/time_tighten/time_tighten.html 2010-06-09 22:45:23 UTC (rev 817)
@@ -14,7 +14,7 @@
<P>After 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 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:</P>
+<P>An example of the tighten time algorithm on a BMSC TODO add comment why it is tightened this way:</P>
<table><caption align="bottom"><i>Original BMSC</i></caption><tr><td>
@@ -27,7 +27,7 @@
<H3> High-level MSC</H3>
<P>After 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 the end node.</p>
-<P>An example of the tighten time algorithm on a HMSC:</P>
+<P>An example of the tighten time algorithm on a HMSC: TODO add comment why it is tightened this way</P>
<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">
Modified: trunk/doc/help/time_trace_race/time_race.html
===================================================================
--- trunk/doc/help/time_trace_race/time_race.html 2010-06-09 17:11:08 UTC (rev 816)
+++ trunk/doc/help/time_trace_race/time_race.html 2010-06-09 22:45:23 UTC (rev 817)
@@ -23,7 +23,7 @@
<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, but which is time race free.</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.</P>
<table><caption align="bottom"><i>BMSC B</i></caption><tr><td>
<img src="pictures/race2_1.png" border="0" alt="Example of time race free HMSC" title="Example of time race free HMSC">
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
