Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[1282] trunk/doc/help
|
From: <lko...@us...> - 2012-01-13 12:10:50
|
Revision: 1282
http://scstudio.svn.sourceforge.net/scstudio/?rev=1282&view=rev
Author: lkorenciak
Date: 2012-01-13 12:10:41 +0000 (Fri, 13 Jan 2012)
Log Message:
-----------
fixed help of scstudio
Modified 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/automatic_drawing.html
trunk/doc/help/frontend/message_numbering.html
trunk/doc/help/frontend/settings.html
trunk/doc/help/frontend/shape_selection.html
trunk/doc/help/index.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/realizability/realizability.html
trunk/doc/help/recursivity/recursivity.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
trunk/doc/help/unique_instance/unique_instance.html
Modified: trunk/doc/help/acyclic/acyclic.html
===================================================================
--- trunk/doc/help/acyclic/acyclic.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/acyclic/acyclic.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -114,7 +114,7 @@
<div class="content">
<h1>Acyclic property</h1>
<p>
- ensures that there is no cyclic dependency among events in an BMSC. Such a
+ ensures that there is no cyclic dependency among events in a 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:
@@ -122,24 +122,28 @@
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/cyclic_simple.vsd">
<li>
- <img src="pictures/cyclic_simple.png" width="250"
+ <img src="pictures/cyclic_simple.png" width="250" border="0"
alt="Cyclic BMSC" title="Cyclic BMSC" />
</li>
<li class="caption">
Cyclic design
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="pictures/cyclic_result.vsd">
<li>
- <img src="pictures/cyclic_result.png" width="250"
+ <img src="pictures/cyclic_result.png" width="250" border="0"
alt="Cyclic BMSC" title="Cyclic BMSC" />
</li>
<li class="caption">
Highlighted cyclic dependency
</li>
+ </a>
</ul>
</li>
</ul>
@@ -149,7 +153,7 @@
<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
+ acyclic design is depicted in 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
@@ -158,13 +162,15 @@
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/acyclic.vsd">
<li>
- <img src="pictures/acyclic.png" width="250"
+ <img src="pictures/acyclic.png" width="250" border="0"
alt="Acyclic BMSC" title="Acyclic BMSC" />
</li>
<li class="caption">
Acyclic design
</li>
+ </a>
</ul>
</li>
</ul>
Modified: trunk/doc/help/beautify/beautify.html
===================================================================
--- trunk/doc/help/beautify/beautify.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/beautify/beautify.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -118,20 +118,20 @@
</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> or by using
+ is accessible via menu <code>Check -> Drawing -> Beautify</code> or by using
hotkey <code>Crtl + Alt + B</code>.
- </p>
- <h3>
- Setting of parameteres
- </h3>
- <p>
- The parameters respected by <code>Beautify</code> can be changed via menu
- <code>Check->Options->Beautify</code>.
- </p>
- <p>
- By pressing <code>General</code> the dialog with options concerning customization of instances
- will be shown:
- </p>
+ </p>
+ <h3>
+ Setting of parameteres
+ </h3>
+ <p>
+ The parameters respected by <code>Beautify</code> can be changed via menu
+ <code>Check->Options->Beautify</code>.
+ </p>
+ <p>
+ By pressing <code>General</code> the dialog with options concerning customization of instances
+ will be shown:
+ </p>
<ul class="gallery">
<li>
<ul>
@@ -140,17 +140,17 @@
alt="General Dialog" />
</li>
</ul>
- </li>
- </ul>
- <p>
- Via <code>General</code>, is possible to set distances between elements, instances length,
- width of instances head, foot and coregions, length of lost and found message and slope
- of messages.
- </p>
- <p>
- By pressing <code>Additional</code> the dialog used for setting of permutation of instances,
- spacing between instances and placement of leftmost instance will be shown:
- </p>
+ </li>
+ </ul>
+ <p>
+ Via <code>General</code>, is possible to set distances between elements, length of instances,
+ width of instance heads, foots and coregions, length of lost and found messages and slope
+ of messages.
+ </p>
+ <p>
+ By pressing <code>Additional</code> the dialog used for setting of permutation of instances,
+ spacing between instances and placement of leftmost instance will be shown:
+ </p>
<ul class="gallery">
<li>
<ul>
@@ -159,18 +159,18 @@
alt="General Dialog" />
</li>
</ul>
- </li>
- </ul>
- <p>
+ </li>
+ </ul>
+ <p>
</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
+ from right side to left side and to minimize the crossings of instances
+ with messages. Instances are aligned 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.
@@ -178,6 +178,7 @@
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/unordered.vsd">
<li>
<img src="pictures/unordered.png" width="500" border="0"
alt="Unordered BMSC" />
@@ -185,10 +186,12 @@
<li class="caption">
Before beautify
</li>
- </ul>
+ </a>
+ </ul>
</li>
<li>
<ul>
+ <a href="pictures/ordered.vsd">
<li>
<img src="pictures/ordered.png" width="350"
border="0" alt="Ordered BMSC" />
@@ -196,6 +199,7 @@
<li class="caption">
After beautify
</li>
+ </a>
</ul>
</li>
</ul>
@@ -211,13 +215,15 @@
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/unfifo2.vsd">
<li>
- <img src="pictures/unfifo2.png" width="250"
+ <img src="pictures/unfifo2.png" width="250" border="0"
alt="Ordered non-FIFO BMSC" />
</li>
<li class="caption">
Acyclic design
</li>
+ </a>
</ul>
</li>
</ul>
@@ -228,43 +234,47 @@
</h3>
<p>
For coregions it changes the order of events to minimize number of
- crossing two messages. After redrawing, messages are jointed with
+ crossings of two messages. After redrawing, messages are joined with
coregion in such way that they do not go across coregion body.
</p>
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/coregion1.vsd">
<li>
- <img src="pictures/coregion1.png" width="250"
+ <img src="pictures/coregion1.png" width="250" border="0"
alt="Crossing messages jointed with coregion" />
</li>
<li class="caption">
Before beautify
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="pictures/coregion2.vsd">
<li>
- <img src="pictures/coregion2.png" width="250 " alt="" />
+ <img src="pictures/coregion2.png" width="250 " border="0" alt="" />
</li>
<li class="caption">
After beautify
</li>
+ </a>
</ul>
</li>
- </ul>
- <p>
- </p>
- <h3>
- Current implementation:
- </h3>
- <p>
- In the current implementation the following features are not supported and therefore may cause
- some inaccuracies: actions, conditions, ordering lines, ordering sides, ordering arrows. Some other
- are not in the final version of implementation: time interval, directed interval and absolute time
- and has to be sometimes redrawn by the user.
+ </ul>
+ <p>
</p>
+ <h3>
+ Current implementation:
+ </h3>
+ <p>
+ In the current implementation the following features are not supported and therefore may cause
+ some inaccuracies: actions, conditions, ordering lines, ordering sides, ordering arrows. Few other
+ features are not in the final version of implementation: time interval, directed interval and
+ absolute time and has to be sometimes redrawn by the user.
+ </p>
</div>
</body>
</html>
Modified: trunk/doc/help/boundedness/boundedness.html
===================================================================
--- trunk/doc/help/boundedness/boundedness.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/boundedness/boundedness.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -132,31 +132,35 @@
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
+ The HMSC in 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>
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/unbounded.vsd">
<li>
- <img src="pictures/unbounded_hmsc.png" width="200"
+ <img src="pictures/unbounded_hmsc.png" width="200" border="0"
alt="Unbounded HMSC" title="Unbounded HMSC" />
</li>
<li class="caption">
Unbounded HMSC
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="pictures/unbounded.vsd">
<li>
- <img src="pictures/unbounded_msc.png" width="250"
+ <img src="pictures/unbounded_msc.png" width="250" border="0"
alt="MSC A" title="MSC A" />
</li>
<li class="caption">
MSC A
</li>
+ </a>
</ul>
</li>
</ul>
Modified: trunk/doc/help/deadlock/deadlock.html
===================================================================
--- trunk/doc/help/deadlock/deadlock.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/deadlock/deadlock.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -118,7 +118,7 @@
Deadlock
</h1>
<p>
- is a property of a HMSC node. A reachable node is deadlocked if there is
+ is a property of an 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>
@@ -128,19 +128,21 @@
deadlock.
</p>
<p>
- On the next picture the node B is clearly a deadlocked node. That is why
+ In 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>
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/deadlock.vsd">
<li>
- <img src="pictures/deadlock.png" width="350"
+ <img src="pictures/deadlock.png" width="351" border="0"
alt="Typical deadlock" title="Typical deadlock" />
</li>
<li class="caption">
Typical deadlock
</li>
+ </a>
</ul>
</li>
</ul>
Modified: trunk/doc/help/fifo/fifo.html
===================================================================
--- trunk/doc/help/fifo/fifo.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/fifo/fifo.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -134,10 +134,10 @@
FIFO channel for every pair of instances and labels
</li>
<li>
- One FIFO channel for every process
+ one FIFO channel for every process
</li>
<li>
- One FIFO channel for all processes
+ one FIFO channel for all processes
</li>
</ul>
The SCStudio currently supports the first two options. The extension for
@@ -161,7 +161,7 @@
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
+ An example of a non-FIFO design can be seen in 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>,
@@ -170,6 +170,7 @@
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/simple_non_fifo.vsd">
<li>
<img src="pictures/simple_non_fifo.png" width="250" border="0"
alt="Example of a non-fifo design"
@@ -178,6 +179,7 @@
<li class="caption">
Example of a non-FIFO design
</li>
+ </a>
</ul>
</li>
</ul>
@@ -194,7 +196,7 @@
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
+ In 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
@@ -204,29 +206,33 @@
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/fifo1.vsd">
<li>
- <img src="pictures/fifo1.png" width="250" border="0"
+ <img src="pictures/fifo1.png" height="348" border="0"
alt="FIFO MSC design" title="FIFO MSC design" />
</li>
<li class="caption">
Example of a FIFO design
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="pictures/fifo2.vsd">
<li>
- <img src="pictures/fifo2.png" width="250" border="0"
+ <img src="pictures/fifo2.png" height="348" border="0"
alt="FIFO MSC design" title="FIFO MSC design" />
</li>
<li class="caption">
Example of a different FIFO design
</li>
+ </a>
</ul>
</li>
</ul>
<p>
- An example of a non-FIFO design can be seen on the following picture. This
+ An example of a non-FIFO design can be seen in 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
@@ -236,6 +242,7 @@
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/nonfifo1.vsd">
<li>
<img src="pictures/nonfifo1.png" width="250" border="0"
alt="non-fifo design" title="non-fifo design" />
@@ -243,6 +250,7 @@
<li class="caption">
Example of a non-FIFO design
</li>
+ </a>
</ul>
</li>
</ul>
@@ -253,15 +261,17 @@
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:
+ case. The difference can be seen in the following FIFO example:
</p>
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/label_channel_fifo.vsd">
<li>
<img src="pictures/label_channel_fifo.png" width="250" border="0"
alt="FIFO MSC design" title="FIFO MSC design" />
</li>
+ </a>
</ul>
</li>
</ul>
Modified: trunk/doc/help/frontend/automatic_drawing.html
===================================================================
--- trunk/doc/help/frontend/automatic_drawing.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/frontend/automatic_drawing.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -162,7 +162,7 @@
</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,
+ instances. The basic usage is that one instance sends a message,
which is received and resent by several other instances and finally
received by the last instance, as illustrated in the following picture.
</p>
@@ -177,15 +177,15 @@
<img class="big" src="pictures/message_sequence_options.png"
alt="Message Sequence options dialog" />
<p>
- The first option in the dialog determines the direction of the sequence.
- For each direction, a separate message label may be specified in the Left
- and Right Message Captions input boxes. Uni- and bidirectional message
- sequences are supported.
+ The first option in the dialog determines the direction of the sequence.
+ Uni- and bidirectional message sequences are supported. For each direction,
+ a separate message label may be specified in the Left and Right Message
+ Captions input boxes.
</p>
<p>
- Starting Y-position determines the instances, among which the sequence is
- to be drawn. The initial set of instances is taken according to current
- selection:
+ Starting Y-position helps to determine the instances, among which the
+ sequence is to be drawn. The initial set of instances is taken according
+ to current selection:
</p>
<ul>
<li>
@@ -200,10 +200,11 @@
</li>
</ul>
From all of these instances, the leftmost and the rightmost instances are
- recognized as the first and last instance in the message sequence. Between
- these two, all other instances crossing an imaginary horizontal line at
- height equal to Starting Y-position are qualified for the message sequence.
- (During the options dialog, these two instances are marked with red color.)
+ recognized as the first and last instance in the message sequence. (During
+ the options dialog, these two instances are marked with red color.) Between
+ these two instances, all other instances crossing an imaginary horizontal
+ line at height equal to Starting Y-position are qualified for the message
+ sequence.
<p>
The Starting Y-position has a default value of mouse position, so the most
comfortable way of invoking Message Sequence is using the context-menu on
@@ -212,7 +213,7 @@
</p>
<p>
The next two input boxes, Vertical space between messages and Vertical
- space between left and right sequence define the vertical space between to
+ space between left and right sequence define the vertical space between the
subsequent messages on the same instance.
</p>
<p>
Modified: trunk/doc/help/frontend/message_numbering.html
===================================================================
--- trunk/doc/help/frontend/message_numbering.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/frontend/message_numbering.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -113,10 +113,10 @@
<div class="content">
<h1>Element Numbering</h1>
<p>Element Numbering allows users to enumerate all types of message shapes (left, right, lost, found), conditions and actions.<br>
-You can enumerate all element on the active page (if no element are selected) or the selection.<br>
+You can enumerate all elements on the active page (if no elements are selected) or in the current selection.<br>
</p>
-<h2>Enable Element Numbering</h2>
+<h2>Enable element numbering</h2>
<p>By pressing Element Numbering button <img src="pictures/icon_message_enumeration.png" alt="Element Numbering">, via menu <code>SCStudio → Drawing → Element Numbering → Add Numbering</code> or by using hotkey <Code>Ctrl+Alt+E</Code> the dialog with options will be shown:</p>
<p>
@@ -124,9 +124,9 @@
</p>
<p>You can choose:<br>
-- specific numbering type (numbers, letters, capital letters, romans)<br>
-- starting index (1-9999 for number, letters and capital letters and 1-3999 for romans)<br>
-- and additional string following the index such as ".", "-", … (max 4 chars). A space between the index and the message label is added automatically.<br>
+- specific numbering type (numbers, letters, capital letters, roman numbers),<br>
+- starting index (1-9999 for number, letters and capital letters and 1-3999 for roman numbers),<br>
+- and additional string following the index such as ".", "-", … (0 to 4 characters). A space between the index and the message label is added automatically.<br>
</p>
<p>
@@ -134,11 +134,11 @@
Already numbered elements will be overwritten by new numbering.
</p>
-<h2>Disable Element Numbering</h2>
+<h2>Disable element numbering</h2>
<p>Numbering can be deleted by pressing Delete numbering button <img src="pictures/icon_message_enumeration_disable.png" alt="Disable Element Numbering"> on the toolbar, via menu <code>SCStudio → Drawing → Element Numbering → Delete numbering</code> or by using hotkey <Code>Ctrl+Alt+D.</Code></p>
<p>
-Using <code>Delete numbering</code> on selection causes other messages indexes will be recomputed. <br>
+Using <code>Delete numbering</code> on selection causes recomputation of other message indexes. <br>
If no selection is used all numbering indexes will be deleted.
</p>
@@ -161,14 +161,14 @@
</p>
<p>
-<code>automatic numbering new elements</code><br>
+<code>automatic numbering of new elements</code><br>
- sets whether auto numbering is enabled, otherwise all other options are disabled.<br><br>
-<code>as nearest element</code><br>
+<code>as the nearest element</code><br>
- new messages will be numbered according to the group of the closest message on the active page. All message indexes in the current group will be recounted. If the closest message isn't numbered, new one won't be either. <br>
-<code>as nearest numbered element</code><br>
+<code>as the nearest numbered element</code><br>
- new elements will be numbered according to the closest <b>numbered</b> element on the active page. If there are no numbered elements on the active page you can choose between: <br><br>
<code>don't number</code><br>
- - don't number new elements if there are no numbered elements on the page.<br>
+ - don't number new elements if there are no numbered elements on the page,<br>
<code>use numbering style</code><br>
- use specific numbering style if there are no numbered elements on the page.<br>
</p>
Modified: trunk/doc/help/frontend/settings.html
===================================================================
--- trunk/doc/help/frontend/settings.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/frontend/settings.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -156,7 +156,7 @@
  - the message is straightened 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
+   - endpoint(s) of the message are horizontally moved and snapped
to the nearest instance(s).<br /> <code>preserve slope</code><br />
  - the message stays obliqued as it was. The endpoint(s) will
be prolonged to the nearest instance(s).<br />
@@ -167,7 +167,7 @@
<ul>
<li>Multiple message snapping is not implemented.</li>
<li>Lost and Found messages are snapped only at one endpoint.</li>
- <li>Messages can be snapped only to the instances lines. Instance's head and end
+ <li>Messages can be snapped only to the instance lines. Instance head and end
symbols are ignored.</li>
</ul>
@@ -188,6 +188,52 @@
<a href="./../beautify/beautify.html">separate page</a>.
</p>
+ <h2>Verfication</h2>
+ <p>
+ In the Verification section can user specify which verification algorithms will
+ be executed when either verify button <img src="pictures/icon_check.png"
+ alt="Select instances button" /> is pressed, or Ctrl + Alt + C shortcut is used
+ or in menu <code>SCStudio → Verify</code> is selected. Please note that it
+ is possible that some algorothm may be executed even it is not ticked. This is
+ because of the fact that some algorithms can be executed if the input MSC
+ satisfies some properties. These properties are checked by verification algorithms
+ and thus they have to be executed before execution of ticked algorithm.
+ </p>
+ <p>
+ Prior the execution of verification user can specify type of channels used in MSC
+ document. The choice of channels can effect results of some verification algorithms
+ e.g. FIFO checker or Race condition checker. There are several types of channels
+ and several ways how they can be used in BMSC. Some of the most useful are the
+ following:
+ </p>
+ <ul>
+ <li>
+ FIFO channel for every pair of instances- <code>Sender-Receiver Pair</code>,
+ </li>
+ <li>
+ FIFO channel for every pair of instances and labels- <code>Sender-Receiver-Message Pair</code>,
+ </li>
+ <li>
+ one FIFO channel for every process,
+ </li>
+ <li>
+ one FIFO channel for all processes.
+ </li>
+ </ul>
+ <p>
+ The SCStudio currently supports the first two options. The extension for
+ other options is planned.
+ </p>
+ <p>
+ User can specify which outputs of algorithms will be displayed in the
+ verification report in the <code> Display </code> menu .
+ </p>
+ <h2>Simulation</h2>
+ <p>
+ Simulation and its configuration is described on a
+ <a href="./../montecarlo/montecarlo.html">separate page</a>.
+ </p>
+
</div>
</body>
</html>
Modified: trunk/doc/help/frontend/shape_selection.html
===================================================================
--- trunk/doc/help/frontend/shape_selection.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/frontend/shape_selection.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -114,7 +114,7 @@
</div>
<div class="content">
<h1>
- Shape Selection
+ Shape selection
</h1>
<p>
On top of standard Visio functions for selecting shapes (such as <code>Ctrl+A</code>
Modified: trunk/doc/help/index.html
===================================================================
--- trunk/doc/help/index.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/index.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -123,13 +123,13 @@
<ul>
- <li>Draw basic MSC: line instances, messages, coregions, general ordering, time constraints and measurements</li>
- <li>Draw HMSC: references, conditions, connections</li>
- <li>Export and import the ITU-T Z.120 textual format (.mpr)</li>
- <li>Perform graphical syntax verification</li>
- <li>Execute verification algorithms: detect deadlock/livelock, detect cycles, race conditions and universal boundedness</li>
- <li>Determine probability distribution of time constraints using Monte Carlo simulation</li>
- <li>Develop proprietary stencils and verification/export modules</li>
+ <li>draw basic MSC: line instances, messages, coregions, general ordering, time constraints and measurements,</li>
+ <li>draw HMSC: references, conditions, connections,</li>
+ <li>export and import the ITU-T Z.120 textual format (.mpr),</li>
+ <li>perform graphical syntax verification,</li>
+ <li>execute verification algorithms: detect deadlock/livelock, detect cycles, race conditions and universal boundedness,</li>
+ <li>determine probability distribution of time constraints using Monte Carlo simulation,</li>
+ <li>develop proprietary stencils and verification/export modules.</li>
</ul>
<img src="pictures/scstudio.png" alt="SCStudio screenshot" title="SCStudio screenshot"/>
Modified: trunk/doc/help/livelock/livelock.html
===================================================================
--- trunk/doc/help/livelock/livelock.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/livelock/livelock.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -126,19 +126,21 @@
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
+ An example of livelock is depicted in the next picture. It clearly
satisfies all conditions for livelock.
</p>
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/livelock.vsd">
<li>
- <img src="pictures/livelock.png" width="450"
+ <img src="pictures/livelock.png" width="447" border="0"
alt="Typical livelock" title="Typical livelock" />
</li>
<li class="caption">
Typical livelock
</li>
+ </a>
</ul>
</li>
</ul>
Modified: trunk/doc/help/localchoice/localchoice.html
===================================================================
--- trunk/doc/help/localchoice/localchoice.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/localchoice/localchoice.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -129,6 +129,7 @@
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/simple_nonlocal.vsd">
<li>
<img src="pictures/simple_nonlocal.png" width="550" border="0"
alt="HMSC specification with a branching node"
@@ -137,10 +138,12 @@
<li class="caption">
HMSC specification with a branching node
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="pictures/simple_nonlocal.vsd">
<li>
<img src="pictures/simple_nonlocal_MSCA.png" width="200"
border="0" alt="MSC A" title="MSC A" />
@@ -148,10 +151,12 @@
<li class="caption">
MSC A
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="pictures/simple_nonlocal.vsd">
<li>
<img src="pictures/simple_nonlocal_MSCB.png" width="200"
border="0" alt="MSC B" title="MSC B" />
@@ -159,6 +164,7 @@
<li class="caption">
MSC B
</li>
+ </a>
</ul>
</li>
</ul>
@@ -168,15 +174,12 @@
</p>
<ul>
<li>
- There exists a branch that is initiated by more than one instance.
+ 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
+ there exist two branches, such that each is initiated by different
+ instance.
</li>
- <li>
- .
- </li>
</ul>
<p>
The result of the check on the previous example marks the non-local choice
@@ -185,6 +188,7 @@
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/simple_nonlocal_result.vsd">
<li>
<img src="pictures/simple_nonlocal_result.png" width="350"
border="0" alt="Result of SCStudio" title="Result of SCStudio" />
@@ -192,10 +196,12 @@
<li class="caption">
Result of SCStudio
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="pictures/simple_nonlocal.vsd">
<li>
<img src="pictures/simple_nonlocal_implied.png" width="200"
border="0" alt="Implied behavior" title="Implied behavior" />
@@ -203,6 +209,7 @@
<li class="caption">
Implied behavior
</li>
+ </a>
</ul>
</li>
</ul>
Modified: trunk/doc/help/membership/membership.html
===================================================================
--- trunk/doc/help/membership/membership.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/membership/membership.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -114,14 +114,15 @@
</div>
<div class="content">
<h1>
- Find Flow Algorithm
+ Find Flow algorithm
</h1>
<p>
The Find Flow problem is deciding whether given flow (BMSC) is contained in a
- given specification (BMSC or HMSC with nesting level 1, means each node represents BMSC).
+ given specification (BMSC or HMSC with nesting level 1). HMSC with nesting level
+ 1 is property HMSC that each reference node in HMSC represents BMSC).
</p>
<p>
- <h2>More formal specification of the procedure:</h2>
+ <h2>More formal specification of the algorithm</h2>
</p>
<p>
Input:
@@ -205,17 +206,17 @@
</li>
<li>
- flow: can contain only one type of time constraint (absolute or relative)
+ flow: can contain only one type of time constraints (absolute or relative)
</li>
</ul>
</p>
- <b>WARNING:</b> If the specification contains the same message ordering in different paths, the algorithm checks time constrains only from one path.
+ <b>WARNING:</b> if the specification contains the same message ordering in different paths, the algorithm checks time constrains only from one path.
<p>
- <h2>Specified instances checking [optional]</h2>
+ <h2>Checking of specified instances [optional]</h2>
</p>
<p>
- The Find Flow algorithm supports mode where a user specifies which instances are supposed to be checked. In this mode the algorithm checks only message orderings on chosen instances (time constraints are not checked).
+ The Find Flow algorithm supports mode where a user specifies which instances should be checked. In this mode the algorithm checks only message orderings on chosen instances (time constraints are not checked).
</p>
<hr/>
@@ -227,9 +228,20 @@
<h3>
Example 1 - specification: HMSC, flow: BMSC:
</h3>
+ <p>
+ In the figures below a <i>specification</i>, which is one of input MSCs to the Find Flow algorithm, is depicted.
+ In HMSC, every path from the initial node to the terminal node describes a scenario, which could be represented by a BMSC.
+ </p>
+
+ <p>
+ The BMSC represented by the path consists of nodes (BMSCs) on the path which are
+ sequentially composed (putting the BMSCs one after the other and gluing the matching process lines).
+ In this case, there are two paths (BMSC01.BMSC02, BMSC01.BMSC03).
+ </p>
<ul class="gallery">
<li>
<ul>
+ <a href="Example_1_spec.vsd">
<li>
<img src="pictures/memebership_15.png" width="380" border="0"
alt="HMSC specification" title="HMSC specification" />
@@ -237,10 +249,12 @@
<li class="caption">
HMSC specification
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="Example_1_spec.vsd">
<li>
<img src="pictures/memebership_14.png" width="280" border="0"
alt="BMSC BMSC01" title="BMSC01" />
@@ -248,10 +262,12 @@
<li class="caption">
BMSC BMSC01
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="Example_1_spec.vsd">
<li>
<img src="pictures/memebership_16.png" width="280" border="0"
alt="BMSC BMSC02" title="BMSC02" />
@@ -259,10 +275,12 @@
<li class="caption">
BMSC BMSC02
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="Example_1_spec.vsd">
<li>
<img src="pictures/memebership_13.png" width="280" border="0"
alt="BMSC BMSC03" title="BMSC03" />
@@ -270,23 +288,19 @@
<li class="caption">
BMSC BMSC03
</li>
+ </a>
</ul>
</li>
</ul>
<p>
- In the figures above a <i>specification</i>, which is one of input MSCs to the Find Flow algorithm, is depicted.
- In HMSC, every path from the initial node to the terminal node describes a scenario, which could be represented by a BMSC.
+ Next parameter for the Find Flow algorithm is an MSC flow which we depicted below. It is easy to see that the <i>BMSC flow</i>
+ is exactly the same as the BMSC represented by the path BMSC01.BMSC02 in the <i>specification</i>.
</p>
- <p>
- The BMSC specified by the path consists of nodes (BMSCs) on the path which are
- sequentially composed (putting the BMSCs one after the other and gluing the matching process lines).
- In this case, there are two paths (BMSC01.BMSC02, BMSC01.BMSC03).
- </p>
-
<ul class="gallery">
<li>
<ul>
+ <a href="Example_1_flow.vsd">
<li>
<img src="pictures/memebership_17.png" width="280" border="0"
alt="BMSC g flow" title="BMSC flow" />
@@ -294,20 +308,18 @@
<li class="caption">
BMSC flow
</li>
+ </a>
</ul>
</li>
</ul>
- <p>
- Next parameter for the Find Flow algorithm is an MSC flow which we depicted above. It is easy to see that the <i>BMSC flow</i>
- is exactly the same as the BMSC represented by the path BMSC01.BMSC02 in the <i>specification</i>.
- </p>
<p>
- The result of the Find Flow algorithm is depicted below. Because the flow corresponds with the specification, the algorithm returns the same HMSC as the specification with additional information. HMSC has marked a path which scenario corresponds with the flow and to each node it connects information how many times the node was included to the scenario.
+ The result of the Find Flow algorithm is depicted below. Because the flow corresponds with one scenario of the specification, the algorithm returns the same HMSC as the specification with additional information. The HMSC contains marked path which scenario that corresponds with the flow and node is liked to information about how many times the node was included in the scenario.
<ul class="gallery">
<li>
<ul>
+ <a href="Example_1_result.vsd">
<li>
<img src="pictures/memebership_18.png" width="650" border="0"
alt="BMSC g flow" title="Result of the Find Flow algorithm" />
@@ -315,6 +327,7 @@
<li class="caption">
Result of the Find Flow algorithm
</li>
+ </a>
</ul>
</li>
</ul>
@@ -325,9 +338,13 @@
<h3>
Example 2 - specification: BMSC, flow: BMSC
</h3>
+ <p>
+ In the figure below we have specified input diagrams to the Find Flow algorithm. It is clear that the diagrams are not the same. <i>Flow </i> diagram does not contain a message from the specification, on the other hand, it contains an extra message. The result of the algorithm is depicted below where the red message is an extra one and the green message is missing in the <i>flow</i> diagram.
+ </p>
<ul class="gallery">
<li>
<ul>
+ <a href="Example_2_spec.vsd">
<li>
<img src="pictures/example_2_spec.png" width="280" border="0"
alt="BMSC specification" title="BMSC specification" />
@@ -335,10 +352,12 @@
<li class="caption">
BMSC specification
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="Example_2_flow.vsd">
<li>
<img src="pictures/example_2_flow.png" width="280" border="0"
alt="BMSC flow" title="BMSC flow" />
@@ -346,15 +365,15 @@
<li class="caption">
BMSC flow
</li>
+ </a>
</ul>
</li>
</ul>
- <p>
- In the figure above we have specified input diagrams to the Find Flow algorithm. In the first look, it is clear that the diagrams are not the same. <i>Flow </i> diagram does not contain a message from the specification, on the other hand, it contains an extra message. The result of the algorithm is depicted below where the red message is an extra and the green message is missing in the <i>flow</i> diagram.</p>
<ul class="gallery">
<li>
<ul>
+ <a href="Example_2_result.vsd">
<li>
<img src="pictures/example_2_result.png" width="280" border="0"
alt="Result of the Find Flow algorithm" title="Result of the Find Flow algorithm" />
@@ -362,6 +381,7 @@
<li class="caption">
Result of the Find Flow algorithm
</li>
+ </a>
</ul>
</li>
</ul>
@@ -374,6 +394,7 @@
<ul class="gallery">
<li>
<ul>
+ <a href="Example_3_spec.vsd">
<li>
<img src="pictures/example_3_spec1.png" width="380" border="0"
alt="HMSC g specification" title="HMSC specification" />
@@ -381,10 +402,12 @@
<li class="caption">
HMSC specification
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="Example_3_spec.vsd">
<li>
<img src="pictures/example_3_spec2.png" width="280" border="0"
alt="BMSC BMSC01" title="BMSC BMSC01" />
@@ -392,10 +415,12 @@
<li class="caption">
BMSC BMSC01
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="Example_3_spec.vsd">
<li>
<img src="pictures/example_3_spec3.png" width="280" border="0"
alt="BMSC g1" title="BMSC02" />
@@ -403,10 +428,12 @@
<li class="caption">
BMSC BMSC02
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="Example_3_spec.vsd">
<li>
<img src="pictures/example_3_spec4.png" width="280" border="0"
alt="BMSC g2" title="BMSC03" />
@@ -414,25 +441,27 @@
<li class="caption">
BMSC BMSC03
</li>
+ </a>
</ul>
</li>
</ul>
<p>
- In the figures above, the specification is depicted. In the figure below a flow is depicted. The message ordering from the flow diagram coresponds with the message ordering of the scenario described by path BMSC01.BMSC03. The specification contains time constraints in the BMSC03.
+ In the figures above, the specification is depicted. In the figure below a flow is depicted. The message ordering from the flow diagram coresponds with the message ordering of the scenario described by path BMSC01.BMSC03. The specification contains time constraints in the BMSC03.
</p>
<p>
- The time interval [2,5] is compared with time interval [1,3] from the flow. Due to the time between events in the flow could be [1] or [3] the interval is <i>partialy invalid</i> (in case the it would be [1], it would be brake the time constraints of the specification; in case it would be [3], it would be satisfied the time constrains of the specification).
+ The time interval [2,5] is compared with the time interval [1,3] from the flow. Due to the time between events in the flow can be any number in [1,3] the interval is <i>partialy invalid</i> (in case the time is 1, it violates the time constraints of the specification; in case it is 3, it satisfies the time constrains of the specification).
</p>
<p>
- The time interval [8,9] is compared with time interval [10,12]. It is clear that the interval does not satisfied time constraint from the specification and so the time interval is interpreted as <i>invalid</i>.
+ The time interval [8,9] is compared with time interval [10,12]. It is clear that the interval does not satisfy time constraint from the specification thus the time interval is interpreted as <i>invalid</i>.
</p>
<ul class="gallery">
<li>
<ul>
+ <a href="Example_1_flow.vsd">
<li>
<img src="pictures/example_3_flow.png" width="280" border="0"
alt="BMSC g flow" title="BMSC flow" />
@@ -440,17 +469,19 @@
<li class="caption">
BMSC flow
</li>
+ </a>
</ul>
</li>
</ul>
<p>
- In the result, the Find Flow algorithm marks the path and the reference node which contains <i>invalid/partialy invalid</i> time intervals.
+ In the result, the Find Flow algorithm marks the path and the reference nodes which contains <i>invalid/partialy invalid</i> time intervals.
</p>
<ul class="gallery">
<li>
<ul>
+ <a href="Example_1_result.vsd">
<li>
<img src="pictures/example_3_result1.png" width="280" border="0"
alt="BMSC g3" title="Result" />
@@ -458,10 +489,12 @@
<li class="caption">
Result of the Find Flow algorithm
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="Example_1_result.vsd">
<li>
<img src="pictures/example_3_result2.png" width="280" border="0"
alt="BMSC g3" title="BMSC03" />
@@ -469,6 +502,7 @@
<li class="caption">
BMSC BMSC03 from the result
</li>
+ </a>
</ul>
</li>
</ul>
Modified: trunk/doc/help/race/race.html
===================================================================
--- trunk/doc/help/race/race.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/race/race.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -129,12 +129,13 @@
</p>
<p>
SCStudio finds all pairs of events in a given BMSC and also in BMSCs
- referenced by an HMSC. On the next picture there is an example of an BMSC
+ referenced by an HMSC. In the next picture there is an example of an BMSC
which contains race condition:
</p>
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/easyrace_1.vsd">
<li>
<img src="pictures/easyrace_1.png" width="300" border="0"
alt="Input BMSC" title="Input BMSC" />
@@ -142,10 +143,12 @@
<li class="caption">
Input BMSC
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="pictures/easyrace_2.vsd">
<li>
<img src="pictures/easyrace_2.png" width="300" border="0"
alt="Possible execution" title="Possible execution" />
@@ -153,10 +156,12 @@
<li class="caption">
Possible execution
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="pictures/easyrace_1.vsd">
<li>
<img src="pictures/easyrace_result.png" width="300" border="0"
alt="SCStudio result" title="SCStudio result" />
@@ -164,17 +169,19 @@
<li class="caption">
SCStudio result
</li>
+ </a>
</ul>
</li>
</ul>
<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:
+ race. SCStudio is capable of finding all such occurrences.
</p>
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/trickyrace_1.vsd">
<li>
<img src="pictures/trickyrace_1.png" width="100" border="0"
alt="Input HMSC" title="Input HMSC" />
@@ -182,10 +189,12 @@
<li class="caption">
Input HMSC with a race
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="pictures/trickyrace_1.vsd">
<li>
<img src="pictures/trickyrace_2.png" width="300" border="0"
alt="MSC A" title="MSC A" />
@@ -193,10 +202,12 @@
<li class="caption">
MSC A
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="pictures/trickyrace_1.vsd">
<li>
<img src="pictures/trickyrace_3.png" width="300" border="0"
alt="MSC B" title="MSC B" />
@@ -204,6 +215,7 @@
<li class="caption">
MSC B
</li>
+ </a>
</ul>
</li>
</ul>
Modified: trunk/doc/help/realizability/realizability.html
===================================================================
--- trunk/doc/help/realizability/realizability.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/realizability/realizability.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -115,10 +115,10 @@
</div>
<div class="content">
<h1>
- Strong realizability
+ Strong Realizability
</h1>
<p>
- is a property of an HMSC. A MSC is realizable if it is possible to write computer programs for all instances from the MSC in such a way that the behavior of the resulting distributed system is the same as the one described by the MSC. It is assumed that asynchronous transfer of messages is used in the realization. An HMSC is <i>strongly realizable</i> iff it is <a
+ is a property of an HMSC. An MSC is realizable if it is possible to write computer programs for all instances from the MSC in such a way that the behavior of the resulting distributed system is the same as the one described by the MSC. It is assumed that asynchronous transfer of messages is used in the realization. An HMSC is <i>strongly realizable</i> iff it is <a
href="../boundedness/boundedness.html">universally bounded</a> and
<a href="../locaLchoice/localchoice.html">local-choice</a>.
Universal boundedness assures that using finite message buffers is sufficient. If an MSC is not bounded, no realization with finite buffers is capable of performing the entire behavior described by the MSC.
Modified: trunk/doc/help/recursivity/recursivity.html
===================================================================
--- trunk/doc/help/recursivity/recursivity.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/recursivity/recursivity.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -125,6 +125,7 @@
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/recursivity.vsd">
<li>
<img src="pictures/recursivity1.png" width="150" border="0"
alt="Input HMSC" title="Input HMSC" />
@@ -132,10 +133,12 @@
<li class="caption">
Input HMSC
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="pictures/recursivity.vsd">
<li>
<img src="pictures/recursivity2.png" width="150" border="0"
alt="HMSC A violating non recursivity"
@@ -144,10 +147,12 @@
<li class="caption">
HMSC A violating non recursivity
</li>
+ </a>
</ul>
</li>
<li>
<ul>
+ <a href="pictures/recursivity3.vsd">
<li>
<img src="pictures/recursivity3.png" width="150" border="0"
alt="Non recursive HMSC" title="Non recursive HMSC" />
@@ -155,6 +160,7 @@
<li class="caption">
Non recursive HMSC
</li>
+ </a>
</ul>
</li>
</ul>
Modified: trunk/doc/help/time_consistency/time_consistency.html
===================================================================
--- trunk/doc/help/time_consistency/time_consistency.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/time_consistency/time_consistency.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -115,7 +115,7 @@
</div>
<div class="content">
<h1>
- Time Consistency
+ Time Consistent
</h1>
<p>
Time consistency is a problem of deciding whether introduced time
@@ -143,11 +143,12 @@
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.
+ An example of a time consistent BMSC is depicted in the next picture.
</p>
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/cons1.vsd">
<li>
<img src="pictures/cons1.png" width="350" border="0"
alt="Time inconsistent BMSC" title="Time inconsistent BMSC" />
@@ -155,9 +156,12 @@
<li class="caption">
Time inconsistent BMSC
</li>
+ </a>
</ul>
</li>
</ul>
+ <p>
+ </p>
<h2>
High-level MSC
</h2>
@@ -166,14 +170,16 @@
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.
+ An example of time inconsistent HMSC is depicted in the next picture (assume
+ that both reference nodes containt events). 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>
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/cons1.vsd">
<li>
<img src="pictures/cons2.png" width="250" border="0"
alt="Time inconsistent HMSC" title="Time inconsistent HMSC" />
@@ -181,9 +187,17 @@
<li class="caption">
Time inconsistent HMSC
</li>
+ </a>
</ul>
</li>
</ul>
+ <p>
+ The assumption that both reference nodes in picture above is crutial for
+ time inconsistency of the above HMSC. Imagine that one of the reference nodes
+ does not contain events. Since HMSC time constraints restricts events in
+ reference node to which it is attached the constraints attached to reference
+ node with no events are trivially consistent (they are valid in any time assignment).
+ </p>
<h3>
Current implementation:
</h3>
Modified: trunk/doc/help/time_syntax/time_syntax.html
===================================================================
--- trunk/doc/help/time_syntax/time_syntax.html 2012-01-13 11:32:12 UTC (rev 1281)
+++ trunk/doc/help/time_syntax/time_syntax.html 2012-01-13 12:10:41 UTC (rev 1282)
@@ -121,16 +121,16 @@
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.
+ not allowed by the standard or are ambiguous.
</p>
<p>
The following conditions must hold for every time constraint to suffice
- correct time constraint syntax algorithm:
+ the correct time constraint syntax algorithm:
</p>
<ul>
<li>
if the constraint is in BMSC it has to restrict events which are
- visually ordered
+ visually ordered,
</li>
<li>
if the constraint is in HMSC and it restricts nodes A and B, every path
@@ -140,7 +140,7 @@
</li>
</ul>
<p>
- An example of a time constraint can be seen on the next picture. Receive
+ An example of a time constraint can be seen in 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.
@@ -148,6 +148,7 @@
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/syntax1.vsd">
<li>
<img src="pictures/syntax3.png" width="350" border="0"
alt="Example of a wrong time constraint"
@@ -156,11 +157,12 @@
<li class="caption">
Example of a wrong time constraint
</li>
+ </a>
</ul>
</li>
</ul>
<p>
- On the next picture we see that there exists path which goes twice in a
+ In 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.
@@ -168,6 +170,7 @@
<ul class="gallery">
<li>
<ul>
+ <a href="pictures/syntax1.vsd">
<li>
<img src="pictures/syntax1.png" width="200" border="0"
alt="Violation of constraint syntax"
@@ -176,11 +179,12 @@
<li class="caption">
Violation of constraint syntax
</li>
+ </a>
</ul>
</li>
</ul>
<p>
- The last example depicts a HMSC where exists path which goes through the
+ The last example depicts an 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.
@@ -188,6 +192,7 @@
...
[truncated message content] |
