Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[812] trunk/doc/help
|
From: <lko...@us...> - 2010-05-26 22:02:56
|
Revision: 812
http://scstudio.svn.sourceforge.net/scstudio/?rev=812&view=rev
Author: lkorenciak
Date: 2010-05-26 22:02:50 +0000 (Wed, 26 May 2010)
Log Message:
-----------
fixed few mistakes in help, some statements were reformulated
Modified Paths:
--------------
trunk/doc/help/acyclic/acyclic.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_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
Modified: trunk/doc/help/acyclic/acyclic.html
===================================================================
--- trunk/doc/help/acyclic/acyclic.html 2010-05-24 10:10:00 UTC (rev 811)
+++ trunk/doc/help/acyclic/acyclic.html 2010-05-26 22:02:50 UTC (rev 812)
@@ -13,6 +13,7 @@
<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> 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:</P>
+<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>
<IMG SRC="pictures/acyclic.png" BORDER="0" ALT="Acyclic MSC" TITLE="Acyclic MSC">
</BODY>
Modified: trunk/doc/help/deadlock/deadlock.html
===================================================================
--- trunk/doc/help/deadlock/deadlock.html 2010-05-24 10:10:00 UTC (rev 811)
+++ trunk/doc/help/deadlock/deadlock.html 2010-05-26 22:02:50 UTC (rev 812)
@@ -1,20 +1,20 @@
-<!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 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.
-</P>
-
-<p>
-<img src="deadlock.png" alt="Typical deadlock">
-
-</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>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 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.
+</P>
+
+<p>
+<img src="deadlock.png" alt="Typical deadlock">
+
+</BODY>
Modified: trunk/doc/help/fifo/fifo.html
===================================================================
--- trunk/doc/help/fifo/fifo.html 2010-05-24 10:10:00 UTC (rev 811)
+++ trunk/doc/help/fifo/fifo.html 2010-05-26 22:02:50 UTC (rev 812)
@@ -8,10 +8,9 @@
</HEAD>
<BODY>
<H1>FIFO property</H1>
-<P>FIFO (First In, First Out) is a property of an MSC
-and an HMSC specification. The property ensures that it is possible
-to implement the desired behavior without deadlocks that would be
-caused by attributes of channels.</P>
+<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>
<H2>Basic Message Sequence Chart</H2>
<H3>FIFO channel for every pair of instances </H3>
<P>FIFO property is violated when there are two
@@ -28,7 +27,7 @@
<P>A more formal definition follows:</P>
<P>BMSC is FIFO if for all receive events c, d and their matching send events
-a, b (a,c form one message and b,d form second message) it holds that
+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>
@@ -36,7 +35,7 @@
<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 figure:</P>
+<P>An example of a non-FIFO design can be seen on the following picture:</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>
@@ -51,8 +50,8 @@
<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 certain channel
-type, if every MSC in the HMSC specification satisfies FIFO property
+<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>
</BODY>
</HTML>
Modified: trunk/doc/help/localchoice/localchoice.html
===================================================================
--- trunk/doc/help/localchoice/localchoice.html 2010-05-24 10:10:00 UTC (rev 811)
+++ trunk/doc/help/localchoice/localchoice.html 2010-05-26 22:02:50 UTC (rev 812)
@@ -10,15 +10,15 @@
<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>
<DIV class="gallery vary">
-<table><caption align="bottom">HMSC</caption><tr><td>
+<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">
</tr></td></table>
-<table><caption align="bottom">MSC A</caption><tr><td>
+<table><caption align="bottom"><i>MSC A</i></caption><tr><td>
<IMG SRC="pictures/simple_nonlocal_MSCA.png" BORDER="0" ALT="MSC A" TITLE="MSC A">
</tr></td></table>
-<table><caption align="bottom">MSC B</caption><tr><td>
+<table><caption align="bottom"><i>MSC B</i></caption><tr><td>
<IMG SRC="pictures/simple_nonlocal_MSCB.png" BORDER="0" ALT="MSC B" TITLE="MSC B">
</tr></td></table>
@@ -30,14 +30,14 @@
<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 by red:</P>
+<P>The result of the check on the previous example marks the non-local choice node with the red color:</P>
<DIV class="gallery vary">
-<table><caption align="bottom">Result of SCStudio</caption><tr><td>
+<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">Implied behavior</caption><tr><td>
+<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>
Modified: trunk/doc/help/membership/membership.html
===================================================================
--- trunk/doc/help/membership/membership.html 2010-05-24 10:10:00 UTC (rev 811)
+++ trunk/doc/help/membership/membership.html 2010-05-26 22:02:50 UTC (rev 812)
@@ -8,14 +8,14 @@
<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 given HMSC.
-It is possible to check both untimed and timed cases of bMSCs and
+membership is deciding whether given BMSC is contained in given MSC.
+It is possible to check both untimed and timed cases of BMSCs and
HMSCs.<BR></P>
<P>Example 1:</P>
<DIV class="gallery vary">
-<table><caption align="bottom"><i>Input bMSC</i></caption><tr><td>
+<table><caption align="bottom"><i>Input BMSC</i></caption><tr><td>
<img src="memebership_2.png" border="0" alt="" title="Input bMSC">
</tr></td></table>
@@ -35,35 +35,35 @@
<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
+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
-(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
+formed from nodes (BMSCs) on the path by 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 a procedure:</P>
+specification of the procedure:</P>
<P >Input:
</P>
<UL>
- <LI><P >bMSC with timing
+ <LI><P >BMSC with timing
assignment</P>
- <LI><P >HMSC with timers
- and time interval constraints (both HMSC constraints and bMSC
- constraints)</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 initial to the terminal vertex.</P>
+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>
<P >Example 2:</P>
<DIV class="gallery vary">
-<table><caption align="bottom"><i>Input bMSC</i></caption><tr><td>
+<table><caption align="bottom"><i>Input BMSC</i></caption><tr><td>
<img src="memebership_11.png" border="0" alt="" title="bMSC1">
</tr></td></table>
@@ -97,6 +97,6 @@
</div>
<br clear="all">
-<P >In the result there are only two paths through <i>Input HMSC</i>. This is because only these two paths form bMSCs, which are satisfied by <i>Input bMSC</i>. The path through <i>bMSC4</i> forms bMSC which is not satisfied by <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 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 through <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_consistency/time_consistency.html
===================================================================
--- trunk/doc/help/time_consistency/time_consistency.html 2010-05-24 10:10:00 UTC (rev 811)
+++ trunk/doc/help/time_consistency/time_consistency.html 2010-05-26 22:02:50 UTC (rev 812)
@@ -8,12 +8,12 @@
</HEAD>
<BODY>
<H1>Time Consistency</H1>
-<P>Time consistency is problem of deciding whether introduced time constraints in 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 sapecify too restrictive time constraint and cause that the set of executions which satisfy MSC is empty. The time consistency property checks such situations.
+<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.
<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>
-<P>An example of time inconsistent BMSC is depicted on the next picture.</P>
+<P>An example of a time consistent BMSC is depicted on the next picture.</P>
<img src="pictures/cons1.png" border="0" alt="Time inconsistent BMSC" title="Time inconsistent BMSC">
<H2>High-level MSC</H2>
Modified: trunk/doc/help/time_syntax/time_syntax.html
===================================================================
--- trunk/doc/help/time_syntax/time_syntax.html 2010-05-24 10:10:00 UTC (rev 811)
+++ trunk/doc/help/time_syntax/time_syntax.html 2010-05-26 22:02:50 UTC (rev 812)
@@ -10,20 +10,20 @@
<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>
-<P>The following conditions must hold for every time constraint to suffice correct time constraint algorithm:
+<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 must go through B (and other way around) and it cannot go twice through A (B) without going through node B (A) in between.</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 HTTP Response 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 "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>
<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 exist path which goes twice in a row through the node Connection denied and thus the introduced time constraint also does not satisfy 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 Connection denied 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">
-<P>The last example depicts HMSC where exist path which goes through node A of but does not go through node B. Since there is introduced time constraint restricting these nodes it violates Correct Time Constraint Syntax property.</P>
+<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>
<img src="pictures/syntax2.png" border="0" alt="Example of a wrong time constraint" title="Example of a wrong HMSC time constraint">
</BODY>
</HTML>
Modified: trunk/doc/help/time_tighten/time_tighten.html
===================================================================
--- trunk/doc/help/time_tighten/time_tighten.html 2010-05-24 10:10:00 UTC (rev 811)
+++ trunk/doc/help/time_tighten/time_tighten.html 2010-05-26 22:02:50 UTC (rev 812)
@@ -8,7 +8,7 @@
</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 the values of time constraints which cannot be used due to other more restrictive time constraints.
+<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>
<H3> Basic MSC</H3>
<P>After tighten time algorithm, every constraint contains only values in interval sets for which exists valid time assignment.</p>
Modified: trunk/doc/help/time_trace_race/time_race.html
===================================================================
--- trunk/doc/help/time_trace_race/time_race.html 2010-05-24 10:10:00 UTC (rev 811)
+++ trunk/doc/help/time_trace_race/time_race.html 2010-05-26 22:02:50 UTC (rev 812)
@@ -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 HTTP Request and HTTP Response 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 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>
<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>
@@ -19,9 +19,9 @@
<img src="pictures/race1_2.png" border="0" alt="Time race free BMSC" title="Time race free BMSC">
</tr></td></table>
-<P>BMSC B (or HMSC path p) contains time race if there are two visually ordered events in B (or p), but there exists time assignment which assigns visually preceding event larger time value than the value assigned to subsequent event.</P>
-<P>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 assignment to these events must be included in the interval set of this constraint.</P>
+<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, but which is time race free.</P>
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|