[Scstudio-commits] SF.net SVN: scstudio:[820] trunk/doc/help

[<lko...@us...>]

Revision: 820
          http://scstudio.svn.sourceforge.net/scstudio/?rev=820&view=rev
Author:   lkorenciak
Date:     2010-06-17 03:06:31 +0000 (Thu, 17 Jun 2010)

Log Message:
-----------
added few descriptions of pictures in Help, mistakes fixed

Modified Paths:
--------------
    trunk/doc/help/acyclic/acyclic.html
    trunk/doc/help/boundedness/boundedness.html
    trunk/doc/help/deadlock/deadlock.html
    trunk/doc/help/fifo/fifo.html
    trunk/doc/help/localchoice/localchoice.html
    trunk/doc/help/membership/membership.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

Modified: trunk/doc/help/acyclic/acyclic.html
===================================================================
--- trunk/doc/help/acyclic/acyclic.html	2010-06-11 11:36:43 UTC (rev 819)
+++ trunk/doc/help/acyclic/acyclic.html	2010-06-17 03:06:31 UTC (rev 820)
@@ -10,10 +10,10 @@
 <H1>Acyclic property</H1>
 <P> Acyclic property ensures that there is no cyclic dependency among events in an MSC. Such a dependency is erroneous, because it requires to wait with sending a message until it is received. An example of such MSC design can be seen in the following figure:</P>
 <IMG SRC="pictures/cyclic_simple.png"  BORDER="0" ALT="Cyclic MSC" TITLE="Cyclic MSC">
-<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>
+<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 sent until message <I>m2</I> is received.</P>
 <P> SCStudio highlights the cyclic dependency:</P>
 <IMG SRC="pictures/cyclic_result.png"  BORDER="0" ALT="SCStudio result" TITLE="SCStudio result">
-<P> A more tricky example of an acyclic design is depicted on the following figure. There is a coregion box on the Instance p 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> 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>
 <IMG SRC="pictures/acyclic.png" BORDER="0" ALT="Acyclic MSC" TITLE="Acyclic MSC">
 </BODY>

Modified: trunk/doc/help/boundedness/boundedness.html
===================================================================
--- trunk/doc/help/boundedness/boundedness.html	2010-06-11 11:36:43 UTC (rev 819)
+++ trunk/doc/help/boundedness/boundedness.html	2010-06-17 03:06:31 UTC (rev 820)
@@ -11,7 +11,7 @@
 <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>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. 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>
 <img src="unbounded.png" alt="Unbounded HMSC">
 </BODY>

Modified: trunk/doc/help/deadlock/deadlock.html
===================================================================
--- trunk/doc/help/deadlock/deadlock.html	2010-06-11 11:36:43 UTC (rev 819)
+++ trunk/doc/help/deadlock/deadlock.html	2010-06-17 03:06:31 UTC (rev 820)
@@ -11,11 +11,11 @@
 <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 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 an 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. 
+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>
 
 <p>

Modified: trunk/doc/help/fifo/fifo.html
===================================================================
--- trunk/doc/help/fifo/fifo.html	2010-06-11 11:36:43 UTC (rev 819)
+++ trunk/doc/help/fifo/fifo.html	2010-06-17 03:06:31 UTC (rev 820)
@@ -13,7 +13,7 @@
 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:
+There are several types of channels and several ways how they can be used in 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>
@@ -43,16 +43,16 @@
 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: 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>
+<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>
 
 <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. 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>
+<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>
 <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>
-<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 also in this case. The difference can be seen on the following FIFO example:</P>
+<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">
 

Modified: trunk/doc/help/localchoice/localchoice.html
===================================================================
--- trunk/doc/help/localchoice/localchoice.html	2010-06-11 11:36:43 UTC (rev 819)
+++ trunk/doc/help/localchoice/localchoice.html	2010-06-17 03:06:31 UTC (rev 820)
@@ -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 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>
+<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 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-11 11:36:43 UTC (rev 819)
+++ trunk/doc/help/membership/membership.html	2010-06-17 03:06:31 UTC (rev 820)
@@ -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 going through/containing <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 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/time_syntax/time_syntax.html
===================================================================
--- trunk/doc/help/time_syntax/time_syntax.html	2010-06-11 11:36:43 UTC (rev 819)
+++ trunk/doc/help/time_syntax/time_syntax.html	2010-06-17 03:06:31 UTC (rev 820)
@@ -8,7 +8,7 @@
 </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 standard or ambiguous.
+<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>
@@ -16,10 +16,10 @@
 <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 "HTTP Response" (??? or <I>HTTP Response</I>) and HTTP Request messages are not visually ordered. Thus the time constraint does not satisfy the correct time constraint syntax property. </P>
+<P>An example of a time constraint can be seen on the next picture. Receive events of <I>HTTP Response</I> and <I>HTTP Request</I> messages are not visually ordered. Thus the time constraint does not satisfy the correct time constraint syntax property. </P>
 <img src="pictures/syntax3.png"  border="0" alt="Example of a wrong time constraint" title="Example of a wrong BMSC time constraint">
 
-<P>On the next picture we see that there exists path which goes twice in a row through the node Connection denied and thus the introduced time constraint also does not satisfy the correct time constraint syntax property.</P>
+<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>
 
 <img src="pictures/syntax1.png"  border="0" alt="Violation of constraint syntax" title="Violation of constraint syntax property">
 

Modified: trunk/doc/help/time_tighten/time_tighten.html
===================================================================
--- trunk/doc/help/time_tighten/time_tighten.html	2010-06-11 11:36:43 UTC (rev 819)
+++ trunk/doc/help/time_tighten/time_tighten.html	2010-06-17 03:06:31 UTC (rev 820)
@@ -8,13 +8,13 @@
 </HEAD>
 <BODY>
 <H1>Tighten Time</H1>
-<P>The purpose of 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>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 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>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 TODO add comment why it is tightened this way:</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>
 
 
 <table><caption align="bottom"><i>Original BMSC</i></caption><tr><td>
@@ -26,8 +26,16 @@
 </tr></td></table>
 
 <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: TODO add comment why it is tightened this way</P>
+<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>
 
 <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">
@@ -37,8 +45,8 @@
 <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 HMSC B</i></caption><tr><td>
-<img src="pictures/tighten1_3.png"  border="0" alt="Original HMSC B" title="Original BMSC B">
+<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>

Modified: trunk/doc/help/time_trace_race/time_race.html
===================================================================
--- trunk/doc/help/time_trace_race/time_race.html	2010-06-11 11:36:43 UTC (rev 819)
+++ trunk/doc/help/time_trace_race/time_race.html	2010-06-17 03:06:31 UTC (rev 820)
@@ -10,7 +10,7 @@
 <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 next two pictures. In 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. </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>
 <table><caption align="bottom"><i>BMSC with the time race</i></caption><tr><td>
 <img src="pictures/race1_1.png"  border="0" alt="BMSC with the time race" title="BMSC with the time race">
 </tr></td></table>
@@ -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 (between <I>HTTP Request</I> and <I>HTTP Response</I> receive events), 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. Due to time constraints the <I>HTTP Request</I>receive event happens allways before the <I>HTTP Response</I> receive event. </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.