Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[910] trunk/doc/help
|
From: <ag...@us...> - 2010-09-10 13:07:33
|
Revision: 910
http://scstudio.svn.sourceforge.net/scstudio/?rev=910&view=rev
Author: agmy
Date: 2010-09-10 13:07:27 +0000 (Fri, 10 Sep 2010)
Log Message:
-----------
Help improvements
Modified Paths:
--------------
trunk/doc/help/algorithms.html
trunk/doc/help/boundedness/boundedness.html
trunk/doc/help/deadlock/deadlock.html
trunk/doc/help/fifo/fifo.html
trunk/doc/help/frontend/automatic-drawing.html
trunk/doc/help/frontend/message-snapping.html
trunk/doc/help/localchoice/localchoice.html
trunk/doc/help/race/race.html
trunk/doc/help/time_consistency/pictures/cons1.png
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/algorithms.html
===================================================================
--- trunk/doc/help/algorithms.html 2010-09-10 11:22:47 UTC (rev 909)
+++ trunk/doc/help/algorithms.html 2010-09-10 13:07:27 UTC (rev 910)
@@ -8,31 +8,45 @@
The following verification algorithms are supported:
<ul>
<li><a href="acyclic/acyclic.html">Acyclic property</a></li>
-<li><a href="fifo/fifo.html">FIFO property</a></li>
-<li><a href="race/race.html">Race Condition</a></li>
-<li><a href="time_syntax/time_syntax.html">Correct Time Constraint Syntax</a></li>
-<li><a href="unique_instance/unique_instance.html">Unique instance names</a></li>
<li><a href="boundedness/boundedness.html">Universal Boundedness</a></li>
<li><a href="deadlock/deadlock.html">Deadlock</a></li>
+<li><a href="fifo/fifo.html">FIFO</a></li>
<li><a href="livelock/livelock.html">Livelock</a></li>
+<li><a href="localchoice/localchoice.html">Nonlocal Choice</a></li>
<li><a href="membership/membership.html">Membership</a></li>
-<li><a href="localchoice/localchoice.html">Nonlocal Choice</a></li>
-<li><a href="realizability/realizability.html">Strong Realizablilty</a></li>
+<li><a href="race/race.html">Race Condition</a></li>
+<li><a href="realizability/realizability.html">Strong Realizability</a></li>
<li><a href="recursivity/recursivity.html">Non-recursivity</li>
<li><a href="time_consistency/time_consistency.html">Time Consistency</a></li>
+<li><a href="time_syntax/time_syntax.html">Correct Time Constraint Syntax</a></li>
<li><a href="time_trace_race/time_race.html">Time Race</a></li>
+<li><a href="unique_instance/unique_instance.html">Unique instance names</a></li>
+</ul>
+
+<h1>Transformers</h1>
+<ul>
+<li><a href="beautify/beautify.html">Beautify</a></li>
<li><a href="time_tighten/time_tighten.html">Tighten Time</a></li>
-<li><a href="time_syntax/time_syntax.html">Correct Time Constraint Syntax</a></li>
</ul>
<h1>Frontend</h1>
+
+<p>Currently, the SCStudio frontend is accessible as a Microsoft Visio addon.
+Thus, Microsoft Visio 2003 or 2007 must be installed prior to installing
+SCStudio.</p>
+<p>When an MSC document is opened, the Sequence Chart Studio toolbar and menu Check
+are available:</p>
+<img class="big" src="frontend/pictures/frontend.png" alt="SCStudio toolbar and menu in MS Visio">
+
+<p>SCStudio functions extending Visio are divided into the following categories:</p>
<ul>
-<li><a href="beautify/beautify.html">Beautify</a></li>
<li><a href="frontend/automatic-drawing.html">Automatic drawing</a></li>
<li><a href="frontend/message-numbering.html">Message numbering</a></li>
<li><a href="frontend/message-snapping.html">Message snapping</a></li>
<li><a href="frontend/shape-selection.html">Shape selection</a></li>
-<li><a href="frontend/shortcuts.html">Shortcuts</a></li>
</ul>
-</body>
+
+<p>Many SCStudio functions define their own keyboard accelerators.
+See the <a href="frontend/shortcuts.html">keyboard accelerators</a> section to
+list all of them.</p></body>
</html>
Modified: trunk/doc/help/boundedness/boundedness.html
===================================================================
--- trunk/doc/help/boundedness/boundedness.html 2010-09-10 11:22:47 UTC (rev 909)
+++ trunk/doc/help/boundedness/boundedness.html 2010-09-10 13:07:27 UTC (rev 910)
@@ -8,7 +8,7 @@
</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>is a property of an HMSC. An HMSC is universally bounded if there exists an upper bound on size of communication buffers of all involved processes. Informally, each instance waits for a response before sending the same message again. A dialog is an example of bounded communication. E-mail spam is an example of unbounded communication - actually, it is not rare that an input buffer (mailbox) gets full in this case. </P>
<P>When all the possible executions of an HMSC are finite, then HMSC is universally bounded. Therefore only HMSCs containing a cycle may be unbounded. Every cycle whose repetitive execution may lead to unbounded grow of an input buffer is found and displayed by SCStudio.</P>
<P>The HMSC on the following picture is unbounded. This is because there is no mechanism for keeping the buffer for messages between <I>X</I> and <I>Y</I> bounded. </P>
Modified: trunk/doc/help/deadlock/deadlock.html
===================================================================
--- trunk/doc/help/deadlock/deadlock.html 2010-09-10 11:22:47 UTC (rev 909)
+++ trunk/doc/help/deadlock/deadlock.html 2010-09-10 13:07:27 UTC (rev 910)
@@ -15,7 +15,7 @@
</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.
+On the next picture the node B is clearly a deadlocked node. That is why it is highlighted by SCStudio and given as an example.
</P>
<div style="margin: 0 auto;">
Modified: trunk/doc/help/fifo/fifo.html
===================================================================
--- trunk/doc/help/fifo/fifo.html 2010-09-10 11:22:47 UTC (rev 909)
+++ trunk/doc/help/fifo/fifo.html 2010-09-10 13:07:27 UTC (rev 910)
@@ -73,7 +73,7 @@
<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>
+<P>An example of a non-FIFO design can be seen on the following picture. This is because the <I>Instance q</I> can execute only the receive event of message <I>m1</I> and then the receive event of the message <I>m2</I>. However it is possible (due to coregion), that the message <I>m2</I> is at head of the channel queue of Instance q and message <I>m2</I> is behind it. </P>
<div style="margin: 0 auto;">
<ul class="gallery"><li>
Modified: trunk/doc/help/frontend/automatic-drawing.html
===================================================================
--- trunk/doc/help/frontend/automatic-drawing.html 2010-09-10 11:22:47 UTC (rev 909)
+++ trunk/doc/help/frontend/automatic-drawing.html 2010-09-10 13:07:27 UTC (rev 910)
@@ -34,7 +34,7 @@
<h2 id="message_sequence">Message Sequence</h2>
<p>The Message Sequence function draws a sequence of messages among selected instances.
The basic usage is that when one instance sends a message, which is received and
-resent by several other instances and finally received by the last instance, as ilustrated
+resent by several other instances and finally received by the last instance, as illustrated
in the following picture.</p>
<img src="pictures/message_sequence.png" alt="Message Sequence example">
<p>The Message Sequence function is accessible via menu
Modified: trunk/doc/help/frontend/message-snapping.html
===================================================================
--- trunk/doc/help/frontend/message-snapping.html 2010-09-10 11:22:47 UTC (rev 909)
+++ trunk/doc/help/frontend/message-snapping.html 2010-09-10 13:07:27 UTC (rev 910)
@@ -23,7 +23,7 @@
<p>
When the message is already dropped on the page, user can still use snapping. As the message is moved, it automatically snaps to the nearest instance(s) (if exists). Since the message can be oblique, three types of snapping are provided:<br><br>
<code>straighten</code><br>
- - the message is straigten on the current location of the mouse cursor and snapped to instance(s).<br>
+ - the message is straighten on the current location of the mouse cursor and snapped to instance(s).<br>
<code>preserve vertical distance between send - receive</code><br>
- endpoint(s) of the message are horizontally stretched and snapped to the nearest instance(s).<br>
<code>preserve slope</code><br>
Modified: trunk/doc/help/localchoice/localchoice.html
===================================================================
--- trunk/doc/help/localchoice/localchoice.html 2010-09-10 11:22:47 UTC (rev 909)
+++ trunk/doc/help/localchoice/localchoice.html 2010-09-10 13:07:27 UTC (rev 910)
@@ -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 <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>
+<P>is a property of an HMSC node, that has more than one successor, occurring when multiple different behaviors (branches <I>MSC A</I> or <I>MSC B</I>) are possible and the branches are initiated by different instances (<I>MSC A</I> is initiated by the <I>Instance p</I>, <I>MSC B</I> is initiated by the <I>Instance q</I>). Therefore the resulting behavior of the system may contain a combination of both branches, resulting in a non specified implied behavior. </P>
<div style="margin: 0 auto;">
<ul class="gallery"><li>
Modified: trunk/doc/help/race/race.html
===================================================================
--- trunk/doc/help/race/race.html 2010-09-10 11:22:47 UTC (rev 909)
+++ trunk/doc/help/race/race.html 2010-09-10 13:07:27 UTC (rev 910)
@@ -36,7 +36,7 @@
</ul>
</div>
<p style="clear: both;">
-The race condition may also occur between events from different BMSC within an HMSC. HMSC contains race if there exists path which contains a race. SCStudio is capable of finding one such occurence:</P>
+The race condition may also occur between events from different BMSC within an HMSC. HMSC contains race if there exists path which contains a race. SCStudio is capable of finding one such occurrence:</P>
<div style="margin: 0 auto;">
<ul class="gallery"><li>
Modified: trunk/doc/help/time_consistency/pictures/cons1.png
===================================================================
(Binary files differ)
Modified: trunk/doc/help/time_consistency/time_consistency.html
===================================================================
--- trunk/doc/help/time_consistency/time_consistency.html 2010-09-10 11:22:47 UTC (rev 909)
+++ trunk/doc/help/time_consistency/time_consistency.html 2010-09-10 13:07:27 UTC (rev 910)
@@ -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 constraints and cause that the set of behaviors is empty. The time consistency property checks such situations.
+<p> The motivation for time consistency 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>
Modified: trunk/doc/help/time_tighten/time_tighten.html
===================================================================
--- trunk/doc/help/time_tighten/time_tighten.html 2010-09-10 11:22:47 UTC (rev 909)
+++ trunk/doc/help/time_tighten/time_tighten.html 2010-09-10 13:07:27 UTC (rev 910)
@@ -43,7 +43,7 @@
<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>
+<li> the upper bound of the constraint containing originally [2,8] tightens to 4 (not included), because 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>
Modified: trunk/doc/help/time_trace_race/time_race.html
===================================================================
--- trunk/doc/help/time_trace_race/time_race.html 2010-09-10 11:22:47 UTC (rev 909)
+++ trunk/doc/help/time_trace_race/time_race.html 2010-09-10 13:07:27 UTC (rev 910)
@@ -33,8 +33,8 @@
<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>
+<P>Time Race algorithm 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 always before the <I>HTTP Response</I> receive event. </P>
<div style="margin: 0 auto;">
<ul class="gallery"><li>
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
