Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[877] trunk/doc/help
|
From: <ag...@us...> - 2010-09-07 09:03:48
|
Revision: 877
http://scstudio.svn.sourceforge.net/scstudio/?rev=877&view=rev
Author: agmy
Date: 2010-09-07 09:03:38 +0000 (Tue, 07 Sep 2010)
Log Message:
-----------
wide help
Modified Paths:
--------------
trunk/doc/help/acyclic/acyclic.html
trunk/doc/help/acyclic/pictures/acyclic.png
trunk/doc/help/acyclic/pictures/cyclic_result.png
trunk/doc/help/acyclic/pictures/cyclic_simple.png
trunk/doc/help/algorithms.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/fifo/pictures/fifo1.png
trunk/doc/help/fifo/pictures/fifo1.vsd
trunk/doc/help/fifo/pictures/fifo2.png
trunk/doc/help/fifo/pictures/label_channel_fifo.png
trunk/doc/help/fifo/pictures/nonfifo1.png
trunk/doc/help/fifo/pictures/simple_non_fifo.png
trunk/doc/help/frontend/shortcuts.html
trunk/doc/help/help.css
trunk/doc/help/livelock/livelock.html
trunk/doc/help/localchoice/localchoice.html
trunk/doc/help/localchoice/pictures/simple_nonlocal.png
trunk/doc/help/localchoice/pictures/simple_nonlocal_MSCA.png
trunk/doc/help/localchoice/pictures/simple_nonlocal_implied.png
trunk/doc/help/localchoice/pictures/simple_nonlocal_result.png
trunk/doc/help/membership/membership.html
trunk/doc/help/race/race.html
trunk/doc/help/time_consistency/pictures/cons1.png
trunk/doc/help/time_consistency/pictures/cons2.png
trunk/doc/help/time_consistency/time_consistency.html
trunk/doc/help/time_syntax/pictures/syntax1.png
trunk/doc/help/time_syntax/pictures/syntax2.png
trunk/doc/help/time_syntax/pictures/syntax3.png
trunk/doc/help/time_syntax/time_syntax.html
trunk/doc/help/time_tighten/pictures/tighten1_1.png
trunk/doc/help/time_tighten/pictures/tighten1_2.png
trunk/doc/help/time_tighten/pictures/tighten1_3.png
trunk/doc/help/time_tighten/pictures/tighten1_4.png
trunk/doc/help/time_tighten/pictures/tighten1_5.png
trunk/doc/help/time_tighten/pictures/tighten1_6.png
trunk/doc/help/time_tighten/pictures/tighten2.vsd
trunk/doc/help/time_tighten/pictures/tighten2_1.png
trunk/doc/help/time_tighten/pictures/tighten2_2.png
trunk/doc/help/time_tighten/time_tighten.html
trunk/doc/help/time_trace_race/pictures/race1_1.png
trunk/doc/help/time_trace_race/pictures/race1_2.png
trunk/doc/help/time_trace_race/pictures/race2_1.png
trunk/doc/help/time_trace_race/pictures/race2_2.png
trunk/doc/help/time_trace_race/pictures/race2_3.png
trunk/doc/help/time_trace_race/time_race.html
Added Paths:
-----------
trunk/doc/help/acyclic/acyclic.html~
trunk/doc/help/acyclic/pictures/acyclic_small.png
trunk/doc/help/acyclic/pictures/cyclic_result_small.png
trunk/doc/help/acyclic/pictures/cyclic_simple_small.png
trunk/doc/help/beautify/beautify.html~
trunk/doc/help/beautify/pictures/
trunk/doc/help/beautify/pictures/coregion1.png
trunk/doc/help/beautify/pictures/coregion1.vsd
trunk/doc/help/beautify/pictures/coregion1_small.png
trunk/doc/help/beautify/pictures/coregion2.png
trunk/doc/help/beautify/pictures/coregion2.vsd
trunk/doc/help/beautify/pictures/coregion2_small.png
trunk/doc/help/beautify/pictures/ordered.png
trunk/doc/help/beautify/pictures/ordered.vsd
trunk/doc/help/beautify/pictures/ordered_small.png
trunk/doc/help/beautify/pictures/unfifo2.png
trunk/doc/help/beautify/pictures/unfifo2.vsd
trunk/doc/help/beautify/pictures/unfifo2_small.png
trunk/doc/help/beautify/pictures/unordered.png
trunk/doc/help/beautify/pictures/unordered.vsd
trunk/doc/help/beautify/pictures/unordered_small.png
trunk/doc/help/boundedness/boundedness.html~
trunk/doc/help/boundedness/pictures/
trunk/doc/help/boundedness/pictures/unbounded.vsd
trunk/doc/help/boundedness/pictures/unbounded_hmsc.png
trunk/doc/help/boundedness/pictures/unbounded_msc.png
trunk/doc/help/boundedness/pictures/unbounded_small.png
trunk/doc/help/deadlock/deadlock.html~
trunk/doc/help/deadlock/pictures/
trunk/doc/help/deadlock/pictures/deadlock.png
trunk/doc/help/deadlock/pictures/deadlock.vsd
trunk/doc/help/deadlock/pictures/deadlock_small.png
trunk/doc/help/fifo/fifo.html~
trunk/doc/help/fifo/pictures/label_channel_fifo_small.png
trunk/doc/help/fifo/pictures/simple_chan_fifo.png
trunk/doc/help/fifo/pictures/small/
trunk/doc/help/fifo/pictures/small/fifo1_small.png
trunk/doc/help/fifo/pictures/small/fifo2_small.png
trunk/doc/help/fifo/pictures/small/nonfifo1_small.png
trunk/doc/help/fifo/pictures/small/simple_chan_fifo_small.png
trunk/doc/help/fifo/pictures/small/simple_non_fifo_small.png
trunk/doc/help/frontend/shortcuts.html~
trunk/doc/help/livelock/livelock.html~
trunk/doc/help/livelock/pictures/
trunk/doc/help/livelock/pictures/livelock.png
trunk/doc/help/livelock/pictures/livelock.vsd
trunk/doc/help/livelock/pictures/small/
trunk/doc/help/livelock/pictures/small/livelock_small.png
trunk/doc/help/localchoice/localchoice.html~
trunk/doc/help/localchoice/pictures/small/
trunk/doc/help/localchoice/pictures/small/simple_nonlocal_MSCA_small.png
trunk/doc/help/localchoice/pictures/small/simple_nonlocal_MSCB_small.png
trunk/doc/help/localchoice/pictures/small/simple_nonlocal_implied_small.png
trunk/doc/help/localchoice/pictures/small/simple_nonlocal_result_small.png
trunk/doc/help/localchoice/pictures/small/simple_nonlocal_small.png
trunk/doc/help/membership/membership.html~
trunk/doc/help/membership/pictures/
trunk/doc/help/membership/pictures/memebership_1.png
trunk/doc/help/membership/pictures/memebership_10.png
trunk/doc/help/membership/pictures/memebership_11.png
trunk/doc/help/membership/pictures/memebership_12.png
trunk/doc/help/membership/pictures/memebership_2.png
trunk/doc/help/membership/pictures/memebership_3.png
trunk/doc/help/membership/pictures/memebership_4.png
trunk/doc/help/membership/pictures/memebership_5.png
trunk/doc/help/membership/pictures/memebership_6.png
trunk/doc/help/membership/pictures/memebership_7.png
trunk/doc/help/membership/pictures/memebership_8.png
trunk/doc/help/membership/pictures/memebership_9.png
trunk/doc/help/membership/pictures/small/
trunk/doc/help/membership/pictures/small/memebership_10_small.png
trunk/doc/help/membership/pictures/small/memebership_11_small.png
trunk/doc/help/membership/pictures/small/memebership_12_small.png
trunk/doc/help/membership/pictures/small/memebership_1_small.png
trunk/doc/help/membership/pictures/small/memebership_2_small.png
trunk/doc/help/membership/pictures/small/memebership_3_small.png
trunk/doc/help/membership/pictures/small/memebership_4_small.png
trunk/doc/help/membership/pictures/small/memebership_5_small.png
trunk/doc/help/membership/pictures/small/memebership_6_small.png
trunk/doc/help/membership/pictures/small/memebership_7_small.png
trunk/doc/help/membership/pictures/small/memebership_8_small.png
trunk/doc/help/membership/pictures/small/memebership_9_small.png
trunk/doc/help/time_consistency/pictures/small/
trunk/doc/help/time_consistency/pictures/small/cons1_small.png
trunk/doc/help/time_consistency/pictures/small/cons2_small.png
trunk/doc/help/time_consistency/time_consistency.html~
trunk/doc/help/time_syntax/pictures/small/
trunk/doc/help/time_syntax/pictures/small/syntax1_small.png
trunk/doc/help/time_syntax/pictures/small/syntax2_small.png
trunk/doc/help/time_syntax/pictures/small/syntax3_small.png
trunk/doc/help/time_syntax/time_syntax.html~
trunk/doc/help/time_tighten/pictures/small/
trunk/doc/help/time_tighten/pictures/small/tighten1_1_small.png
trunk/doc/help/time_tighten/pictures/small/tighten1_2_small.png
trunk/doc/help/time_tighten/pictures/small/tighten1_3_small.png
trunk/doc/help/time_tighten/pictures/small/tighten1_4_small.png
trunk/doc/help/time_tighten/pictures/small/tighten1_5_small.png
trunk/doc/help/time_tighten/pictures/small/tighten1_6_small.png
trunk/doc/help/time_tighten/pictures/small/tighten2_1_small.png
trunk/doc/help/time_tighten/pictures/small/tighten2_2_small.png
trunk/doc/help/time_tighten/time_tighten.html~
trunk/doc/help/time_trace_race/pictures/small/
trunk/doc/help/time_trace_race/pictures/small/race1_1_small.png
trunk/doc/help/time_trace_race/pictures/small/race1_2_small.png
trunk/doc/help/time_trace_race/pictures/small/race2_1_small.png
trunk/doc/help/time_trace_race/pictures/small/race2_2_small.png
trunk/doc/help/time_trace_race/pictures/small/race2_3_small.png
trunk/doc/help/time_trace_race/time_race.html~
Modified: trunk/doc/help/acyclic/acyclic.html
===================================================================
--- trunk/doc/help/acyclic/acyclic.html 2010-09-06 20:10:23 UTC (rev 876)
+++ trunk/doc/help/acyclic/acyclic.html 2010-09-07 09:03:38 UTC (rev 877)
@@ -8,12 +8,39 @@
</HEAD>
<BODY>
<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 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 <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">
+<P> ensures that there is no cyclic dependency among events in an 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: </P>
+
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/cyclic_simple.png" width="250" BORDER="0" ALT="Cyclic BMSC" TITLE="Cyclic BMSC"></li>
+ <li>Cyclic design</li>
+ </ul></li>
+<li>
+ <ul>
+
+ <li><IMG SRC="pictures/cyclic_result.png" width="250" BORDER="0" ALT="Cyclic BMSC" TITLE="Cyclic BMSC"></li>
+ <li>Highlighted cyclic dependency</li>
+ </ul>
+</li>
+</ul>
+</div>
+
+<p style="clear: both;">
+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>
+SCStudio highlights the cyclic dependency:
+
+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>
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/acyclic.png" width="250" BORDER="0" ALT="Acyclic BMSC" TITLE="Acyclic BMSC"></li>
+ <li>Acyclic design</li>
+ </ul>
+</li>
+</ul>
+</div>
+
</BODY>
Added: trunk/doc/help/acyclic/acyclic.html~
===================================================================
--- trunk/doc/help/acyclic/acyclic.html~ (rev 0)
+++ trunk/doc/help/acyclic/acyclic.html~ 2010-09-07 09:03:38 UTC (rev 877)
@@ -0,0 +1,46 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
+<HTML>
+<HEAD>
+ <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
+ <TITLE>Acyclic property</TITLE>
+ <meta name="author" content="Martin Chmelik">
+ <LINK href="../help.css" rel="stylesheet" type="text/css"/>
+</HEAD>
+<BODY>
+<H1>Acyclic property</H1>
+<P> ensures that there is no cyclic dependency among events in an 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: </P>
+
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/cyclic_simple.png" width="250" BORDER="0" ALT="Cyclic BMSC" TITLE="Cyclic BMSC"></li>
+ <li>Cyclic design</li>
+ </ul></li>
+<li>
+ <ul>
+
+ <li><IMG SRC="pictures/cyclic_result.png" width="250" BORDER="0" ALT="Cyclic BMSC" TITLE="Cyclic BMSC"></li>
+ <li>Highlighted cyclic dependency</li>
+ </ul>
+</li>
+</ul>
+</div>
+
+<p style="clear: both;">
+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>
+SCStudio highlights the cyclic dependency:
+
+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>
+
+<div style="margin: 0 auto;">
+<ul><li>
+ <ul>
+ <li><IMG SRC="pictures/acyclic.png" width="250" BORDER="0" ALT="Acyclic BMSC" TITLE="Acyclic BMSC"></li>
+ <li>Acyclic design</li>
+ </ul>
+</li>
+</ul>
+</div>
+
+</BODY>
Modified: trunk/doc/help/acyclic/pictures/acyclic.png
===================================================================
(Binary files differ)
Added: trunk/doc/help/acyclic/pictures/acyclic_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/acyclic/pictures/acyclic_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Modified: trunk/doc/help/acyclic/pictures/cyclic_result.png
===================================================================
(Binary files differ)
Added: trunk/doc/help/acyclic/pictures/cyclic_result_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/acyclic/pictures/cyclic_result_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Modified: trunk/doc/help/acyclic/pictures/cyclic_simple.png
===================================================================
(Binary files differ)
Added: trunk/doc/help/acyclic/pictures/cyclic_simple_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/acyclic/pictures/cyclic_simple_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Modified: trunk/doc/help/algorithms.html
===================================================================
--- trunk/doc/help/algorithms.html 2010-09-06 20:10:23 UTC (rev 876)
+++ trunk/doc/help/algorithms.html 2010-09-07 09:03:38 UTC (rev 877)
@@ -2,23 +2,44 @@
<head>
<link href="help.css" rel="stylesheet" type="text/css"/>
</head>
-<body>
+
<h1>Algorithms</h1>
-The following verification algorithms are supported:
+
+
+<h2>BMSC</h2>
+The following verification algorithms for BMSC 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>Unique instance names</li>
+</ul>
+
+<h2>HMSC</h2>
+The following verification algorithms for HMSC are supported:
+<ul>
+<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 property</a></li>
<li><a href="livelock/livelock.html">Livelock</a></li>
<li><a href="membership/membership.html">Membership</a></li>
<li><a href="localchoice/localchoice.html">Nonlocal Choice</a></li>
-<li><a href="race/race.html">Race Condition</a></li>
<li><a href="realizability/realizability.html">Strong Realizablilty</a></li>
+<li>Non-recursivity</li>
<li><a href="time_consistency/time_consistency.html">Time Consistency</a></li>
<li><a href="time_trace_race/time_race.html">Time Race</a></li>
<li><a href="time_tighten/time_tighten.html">Tighten Time</a></li>
-<li><a href="boundedness/boundedness.html">Universal Boundedness</a></li>
+<li><a href="time_syntax/time_syntax.html">Correct Time Constraint Syntax</a></li>
</ul>
+
+<h2>Frontend</h2>
+<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>
</html>
Modified: trunk/doc/help/beautify/beautify.html
===================================================================
--- trunk/doc/help/beautify/beautify.html 2010-09-06 20:10:23 UTC (rev 876)
+++ trunk/doc/help/beautify/beautify.html 2010-09-07 09:03:38 UTC (rev 877)
@@ -4,11 +4,12 @@
<TITLE>Beautify documentation</TITLE>
<LINK href="../help.css" rel="stylesheet" type="text/css"/>
</HEAD>
-<BODY>
+<div>
<h2>Beautify</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>.
</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.
@@ -16,24 +17,62 @@
<a href="../acyclic/acyclic.html">acyclic</a> BMSC it makes all messages
horizontal and arranged over instances uniformly from top to down.
</P>
-<P>Before:</P>
-<img src="unordered.png" alt="Unordered BMSC">
-<P>After:</P>
-<img src="ordered.png" alt="Ordered BMSC">
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/unordered.png" width="500" BORDER="0" ALT="Unordered BMSC"></li>
+ <li>Before beautify</li>
+ </ul></li>
+<li>
+ <ul>
+
+ <li><IMG SRC="pictures/ordered.png" align="middle" width="350" BORDER="0" ALT="Ordered BMSC"></li>
+ <li>After beautify</li>
+ </ul>
+</li>
+</ul>
+</div>
+<p style="clear: both;">
+
+<h3> Example 2:</h3>
<P>A <a href="../fifo/fifo.html">non-FIFO</a> BMSC is redrawn to
a form that no messages are going up.</P>
-<img src="unfifo2.png" alt="Ordered non-FIFO BMSC">
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/unfifo2.png" width="250" BORDER="0" ALT="Ordered non-FIFO BMSC"></li>
+ <li>Acyclic design</li>
+ </ul>
+</li>
+</ul>
+</div>
+
+<p style="clear: both;">
+<h3> Example 3:</h3>
<P>For coregions it changes the order of events to minimize number
of crossing two messages. After redrawing, messages are jointed with
coregion in such way that they do not go across coregion body.
<BR></P>
-<P>Before:</P>
-<img src="coregion1.png" alt="Crossing messages jointed with coregion">
-<P>After:</P>
-<img src="coregion2.png" alt="">
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li>
+ <img src="pictures/coregion1.png" width="250" alt="Crossing messages jointed with coregion"></li>
+ <li>Before beautify</li>
+ </ul></li>
+<li>
+ <ul>
+
+ <li>
+ <img src="pictures/coregion2.png" width="250 "alt=""></li>
+ <li>After beautify</li>
+ </ul>
+</li>
+</ul>
+</div>
</BODY>
</HTML>
Added: trunk/doc/help/beautify/beautify.html~
===================================================================
--- trunk/doc/help/beautify/beautify.html~ (rev 0)
+++ trunk/doc/help/beautify/beautify.html~ 2010-09-07 09:03:38 UTC (rev 877)
@@ -0,0 +1,78 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
+<HTML>
+<HEAD>
+ <TITLE>Beautify documentation</TITLE>
+ <LINK href="../help.css" rel="stylesheet" type="text/css"/>
+</HEAD>
+<div>
+<h2>Beautify</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>.
+</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 href="../acyclic/acyclic.html">acyclic</a> BMSC it makes all messages
+horizontal and arranged over instances uniformly from top to down.
+</P>
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/unordered.png" width="500" BORDER="0" ALT="Unordered BMSC"></li>
+ <li>Before beautify</li>
+ </ul></li>
+<li>
+ <ul>
+
+ <li><IMG SRC="pictures/ordered.png" align="middle" " width="350" BORDER="0" ALT="Ordered BMSC"></li>
+ <li>After beautify</li>
+ </ul>
+</li>
+</ul>
+</div>
+<p style="clear: both;">
+
+<h3> Example 2:</h3>
+<P>A <a href="../fifo/fifo.html">non-FIFO</a> BMSC is redrawn to
+a form that no messages are going up.</P>
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/unfifo2.png" width="250" BORDER="0" ALT="Ordered non-FIFO BMSC"></li>
+ <li>Acyclic design</li>
+ </ul>
+</li>
+</ul>
+</div>
+
+<p style="clear: both;">
+<h3> Example 3:</h3>
+<P>For coregions it changes the order of events to minimize number
+of crossing two messages. After redrawing, messages are jointed with
+coregion in such way that they do not go across coregion body.
+<BR></P>
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li>
+ <img src="pictures/coregion1.png" width="250" alt="Crossing messages jointed with coregion"></li>
+ <li>Before beautify</li>
+ </ul></li>
+<li>
+ <ul>
+
+ <li>
+ <img src="pictures/coregion2.png" width="250 "alt=""></li>
+ <li>After beautify</li>
+ </ul>
+</li>
+</ul>
+</div>
+
+</BODY>
+</HTML>
Property changes on: trunk/doc/help/beautify/beautify.html~
___________________________________________________________________
Added: svn:executable
+ *
Added: trunk/doc/help/beautify/pictures/coregion1.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/beautify/pictures/coregion1.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/beautify/pictures/coregion1.vsd
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/beautify/pictures/coregion1.vsd
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/beautify/pictures/coregion1_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/beautify/pictures/coregion1_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/beautify/pictures/coregion2.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/beautify/pictures/coregion2.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/beautify/pictures/coregion2.vsd
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/beautify/pictures/coregion2.vsd
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/beautify/pictures/coregion2_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/beautify/pictures/coregion2_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/beautify/pictures/ordered.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/beautify/pictures/ordered.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/beautify/pictures/ordered.vsd
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/beautify/pictures/ordered.vsd
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/beautify/pictures/ordered_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/beautify/pictures/ordered_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/beautify/pictures/unfifo2.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/beautify/pictures/unfifo2.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/beautify/pictures/unfifo2.vsd
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/beautify/pictures/unfifo2.vsd
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/beautify/pictures/unfifo2_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/beautify/pictures/unfifo2_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/beautify/pictures/unordered.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/beautify/pictures/unordered.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/beautify/pictures/unordered.vsd
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/beautify/pictures/unordered.vsd
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/beautify/pictures/unordered_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/beautify/pictures/unordered_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Modified: trunk/doc/help/boundedness/boundedness.html
===================================================================
--- trunk/doc/help/boundedness/boundedness.html 2010-09-06 20:10:23 UTC (rev 876)
+++ trunk/doc/help/boundedness/boundedness.html 2010-09-07 09:03:38 UTC (rev 877)
@@ -8,10 +8,30 @@
</HEAD>
<BODY>
<H1>Universal Boundedness</H1>
-<P>is a property of an HMSC. An HMSC is universally bounded if there exists an upper limit on size of communication buffers of all involved processes. Informally, each instance waits for a response before sending the same message again. A dialogue is an example of bounded communication. E-mail spam is an example of unbounded communication - actually, it is not rare that an input buffer (mailbox) gets full in this case. </P>
+<P>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>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>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>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>
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/unbounded_hmsc.png" width="200" BORDER="0" ALT="Unbounded HMSC" TITLE="Unbounded HMSC"></li>
+ <li>Unbounded HMSC</li>
+ </ul></li>
+<li>
+ <ul>
+
+ <li><IMG SRC="pictures/unbounded_msc.png" width="250" BORDER="0" ALT="MSC A" TITLE="MSC A"></li>
+ <li>MSC A</li>
+ </ul>
+</li>
+</ul>
+</div>
+
+<p style="clear: both;">
+
+
+<P>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>
Added: trunk/doc/help/boundedness/boundedness.html~
===================================================================
--- trunk/doc/help/boundedness/boundedness.html~ (rev 0)
+++ trunk/doc/help/boundedness/boundedness.html~ 2010-09-07 09:03:38 UTC (rev 877)
@@ -0,0 +1,37 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
+<HTML>
+<HEAD>
+ <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
+ <TITLE>Universal Boundedness</TITLE>
+ <meta name="author" content="Martin Chmelik">
+ <LINK href="../help.css" rel="stylesheet" type="text/css"/>
+</HEAD>
+<BODY>
+<H1>Universal Boundedness</H1>
+<P>is a property of an HMSC. An HMSC is universally bounded if there exists an upper 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>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>
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/unbounded_hmsc.png" width="250" BORDER="0" ALT="Unbounded HMSC" TITLE="Unbounded HMSC"></li>
+ <li>Unbounded HMSC</li>
+ </ul></li>
+<li>
+ <ul>
+
+ <li><IMG SRC="pictures/unbounded_msc.png" width="250" BORDER="0" ALT="MSC A" TITLE="MSC A"></li>
+ <li>MSC A</li>
+ </ul>
+</li>
+</ul>
+</div>
+
+<p style="clear: both;">
+
+
+<P>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>
+</BODY>
Property changes on: trunk/doc/help/boundedness/boundedness.html~
___________________________________________________________________
Added: svn:executable
+ *
Added: trunk/doc/help/boundedness/pictures/unbounded.vsd
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/boundedness/pictures/unbounded.vsd
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/boundedness/pictures/unbounded_hmsc.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/boundedness/pictures/unbounded_hmsc.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/boundedness/pictures/unbounded_msc.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/boundedness/pictures/unbounded_msc.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/boundedness/pictures/unbounded_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/boundedness/pictures/unbounded_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Modified: trunk/doc/help/deadlock/deadlock.html
===================================================================
--- trunk/doc/help/deadlock/deadlock.html 2010-09-06 20:10:23 UTC (rev 876)
+++ trunk/doc/help/deadlock/deadlock.html 2010-09-07 09:03:38 UTC (rev 877)
@@ -8,7 +8,7 @@
</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>is a property of a 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>
<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 an example of the deadlock.
@@ -18,7 +18,14 @@
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>
-<img src="deadlock.png" alt="Typical deadlock">
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/deadlock.png" width="350" BORDER="0" ALT="Typical deadlock" TITLE="Typical deadlock"></li>
+ <li>Typical deadlock</li>
+ </ul>
+</li>
+</ul>
+</div>
</BODY>
Added: trunk/doc/help/deadlock/deadlock.html~
===================================================================
--- trunk/doc/help/deadlock/deadlock.html~ (rev 0)
+++ trunk/doc/help/deadlock/deadlock.html~ 2010-09-07 09:03:38 UTC (rev 877)
@@ -0,0 +1,31 @@
+<!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 a 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>
+
+<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 an example of the deadlock.
+</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.
+</P>
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/deadlock.png" width="250" BORDER="0" ALT="Typical deadlock" TITLE="Typical deadlock"></li>
+ <li>Typical deadlock</li>
+ </ul>
+</li>
+</ul>
+</div>
+
+</BODY>
Property changes on: trunk/doc/help/deadlock/deadlock.html~
___________________________________________________________________
Added: svn:executable
+ *
Added: trunk/doc/help/deadlock/pictures/deadlock.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/deadlock/pictures/deadlock.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/deadlock/pictures/deadlock.vsd
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/deadlock/pictures/deadlock.vsd
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/deadlock/pictures/deadlock_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/deadlock/pictures/deadlock_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Modified: trunk/doc/help/fifo/fifo.html
===================================================================
--- trunk/doc/help/fifo/fifo.html 2010-09-06 20:10:23 UTC (rev 876)
+++ trunk/doc/help/fifo/fifo.html 2010-09-07 09:03:38 UTC (rev 877)
@@ -7,13 +7,13 @@
<LINK href="../help.css" rel="stylesheet" type="text/css"/>
</HEAD>
<BODY>
-<H1>FIFO property</H1>
-<P>FIFO (First In, First Out) is a property of an MSC. The property ensures that it is possible
+<H1>FIFO (First In, First Out) property</H1>
+<P>is a BMSC property. The property ensures that it is possible
to implement the desired behavior without deadlocks, that would be
-caused by behavior of channels.</P>
+caused by channel behavior.</P>
<P>
-There are several types of channels and several ways how they can be used in MSC. Some of the most useful are the following:
+There are several types of channels and several ways how they can be used in BMSC. 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>
@@ -29,32 +29,76 @@
<P>FIFO property is violated when there are two
messages, such that they share a common source and destination
instance and the latter message may arrive before the first one.</p>
-<p> The motivation for such definition of FIFO is following. Imagine we have a system which behaves according to a specification in MSC. This system is located in environment, where all channels are FIFO. Moreover imagine that one process expects the messages to come in some order, according to specification, but the messages may be sent in different order. So that the process expects one message, but there can be different message in the head of the channel queue. In such case the system reached deadlock.
+<p> Imagine we have a system in an all-channel FIFO environment which behaves according to a BMSC specification. A process expects the messages to arrive in some order, according to specification, but the messages might have been sent in a different order. A deadlock is reached as there might 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 <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>,
this is not possible and leads to a deadlock.</P>
-<img src="pictures/simple_non_fifo.png" border="0" alt="Example of a non-fifo design" title="Example of a non-fifo design">
-<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 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
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/simple_non_fifo.png" width="250" BORDER="0" ALT="Example of a non-fifo design" TITLE="Example of a non-fifo design"></li>
+ <li>Example of a non-FIFO design</li>
+ </ul>
+</li>
+</ul>
+</div>
+<p style="clear: both;">
+
+<h4>Formal definition:</h4>
+<P>BMSC is FIFO if for all receive events <I>c</I>, <I>d</I> and their matching send events
+<I>a, b</I> (<<I>a,c</I>> forms the first message and <<I>b,d</I>> forms the second message) it holds that
+<I>c < d => a < b</I>, where < is 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 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">
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/fifo1.png" width="250" BORDER="0" ALT="FIFO MSC design" TITLE="FIFO MSC design"></li>
+ <li>Example of a FIFO design</li>
+ </ul></li>
+<li>
+ <ul>
+
+ <li><IMG SRC="pictures/fifo2.png" width="250" BORDER="0" ALT="FIFO MSC design" TITLE="FIFO MSC design"></li>
+ <li>Example of a different FIFO design</li>
+ </ul>
+</li>
+</ul>
+</div>
+<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>
-<img src="pictures/nonfifo1.png" border="0" alt="non-FIFO MSC design" title="non-FIFO MSC design">
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/nonfifo1.png" width="250" BORDER="0" ALT="non-fifo design" TITLE="non-fifo design"></li>
+ <li>Example of a non-FIFO design</li>
+ </ul>
+</li>
+</ul>
+</div>
+<p style="clear: both;">
+
<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 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">
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/label_channel_fifo.png" width="250" BORDER="0" ALT="FIFO MSC design" TITLE="FIFO MSC design"></li>
+
+ </ul>
+</li>
+</ul>
+</div>
+<p style="clear: both;">
<P>Messages <I>m2</I> and <I>m1</I> are not in the same channel, therefore they may arrive in
any order.</P>
Added: trunk/doc/help/fifo/fifo.html~
===================================================================
--- trunk/doc/help/fifo/fifo.html~ (rev 0)
+++ trunk/doc/help/fifo/fifo.html~ 2010-09-07 09:03:38 UTC (rev 877)
@@ -0,0 +1,107 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
+<HTML>
+<HEAD>
+ <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
+ <TITLE>FIFO</TITLE>
+ <meta name="author" content="Martin Chmelik">
+ <LINK href="../help.css" rel="stylesheet" type="text/css"/>
+</HEAD>
+<BODY>
+<H1>FIFO (First In, First Out) property</H1>
+<P>is a BMSC property. The property ensures that it is possible
+to implement the desired behavior without deadlocks, that would be
+caused by channel behavior.</P>
+
+<P>
+There are several types of channels and several ways how they can be used in BMSC. Some of the most useful are the following:
+<ul>
+<li> FIFO channel for every pair of instances </li>
+<li> FIFO channel for every pair of instances and labels </li>
+<li> One FIFO channel for every process </li>
+<li> One FIFO channel for all processes </li>
+</ul>
+
+The SCStudio currently supports the first two options. The extension for other options is planned.
+</P>
+
+<H2>Basic Message Sequence Chart</H2>
+<H3>FIFO channel for every pair of instances </H3>
+<P>FIFO property is violated when there are two
+messages, such that they share a common source and destination
+instance and the latter message may arrive before the first one.</p>
+<p> Imagine we have a system in an all-channel FIFO environment which behaves according to a BMSC specification. A process expects the messages to arrive in some order, according to specification, but the messages might have been sent in a different order. A deadlock is reached as there might 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 <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>,
+this is not possible and leads to a deadlock.</P>
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/simple_non_fifo.png" width="250" BORDER="0" ALT="Example of a non-fifo design" TITLE="Example of a non-fifo design"></li>
+ <li>Example of a non-FIFO design</li>
+ </ul>
+</li>
+</ul>
+</div>
+<p style="clear: both;">
+
+<h4>Formal definition:</h4>
+<P>BMSC is FIFO if for all receive events <I>c</I>, <I>d</I> and their matching send events
+<I>a, b</I> (<<I>a,c</I>> forms the first message and <<I>b,d</I>> forms the second message) it holds that
+<I>c < d => a < b</I>, where < is 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 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>
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/fifo1.png" width="250" BORDER="0" ALT="FIFO MSC design" TITLE="FIFO MSC design"></li>
+ <li>Example of a FIFO design</li>
+ </ul></li>
+<li>
+ <ul>
+
+ <li><IMG SRC="pictures/fifo2.png" width="250" BORDER="0" ALT="FIFO MSC design" TITLE="FIFO MSC design"></li>
+ <li>Example of a different FIFO design</li>
+ </ul>
+</li>
+</ul>
+</div>
+
+<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>
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/nonfifo1.png" width="250" BORDER="0" ALT="non-fifo design" TITLE="non-fifo design"></li>
+ <li>Example of a non-FIFO design</li>
+ </ul>
+</li>
+</ul>
+</div>
+<p style="clear: both;">
+
+<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 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">
+
+<P>Messages <I>m2</I> and <I>m1</I> are not in the same channel, therefore they may arrive in
+any order.</P>
+<!-- comment
+<H3>One FIFO buffer for every process</H3>
+<P>TODO, wait until implementation is done</P>
+<H3>One FIFO buffer for all processes</H3>
+<P>TODO, wait until implementation is done</P>
+-->
+<H2>High-level Message Sequence Chart</H2>
+<P>HMSC satisfies FIFO property for a certain channel
+type, if every BMSC represented by the HMSC satisfies the FIFO property
+for that channel type.</P>
+</BODY>
+</HTML>
Modified: trunk/doc/help/fifo/pictures/fifo1.png
===================================================================
(Binary files differ)
Modified: trunk/doc/help/fifo/pictures/fifo1.vsd
===================================================================
(Binary files differ)
Modified: trunk/doc/help/fifo/pictures/fifo2.png
===================================================================
(Binary files differ)
Modified: trunk/doc/help/fifo/pictures/label_channel_fifo.png
===================================================================
(Binary files differ)
Added: trunk/doc/help/fifo/pictures/label_channel_fifo_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/fifo/pictures/label_channel_fifo_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Modified: trunk/doc/help/fifo/pictures/nonfifo1.png
===================================================================
(Binary files differ)
Added: trunk/doc/help/fifo/pictures/simple_chan_fifo.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/fifo/pictures/simple_chan_fifo.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Modified: trunk/doc/help/fifo/pictures/simple_non_fifo.png
===================================================================
(Binary files differ)
Added: trunk/doc/help/fifo/pictures/small/fifo1_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/fifo/pictures/small/fifo1_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/fifo/pictures/small/fifo2_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/fifo/pictures/small/fifo2_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/fifo/pictures/small/nonfifo1_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/fifo/pictures/small/nonfifo1_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/fifo/pictures/small/simple_chan_fifo_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/fifo/pictures/small/simple_chan_fifo_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/fifo/pictures/small/simple_non_fifo_small.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/fifo/pictures/small/simple_non_fifo_small.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Modified: trunk/doc/help/frontend/shortcuts.html
===================================================================
--- trunk/doc/help/frontend/shortcuts.html 2010-09-06 20:10:23 UTC (rev 876)
+++ trunk/doc/help/frontend/shortcuts.html 2010-09-07 09:03:38 UTC (rev 877)
@@ -8,7 +8,7 @@
<h1>Visio addon keyboard accelerators</h1>
<p>The following keyboard accelerators are defined by SCStudio Visio addon:</p>
<table>
-<col width="100"> <col>
+<col width="150"> <col>
<tr><td><code>Ctrl+Alt+I</code></td><td><a href="shape-selection.html">Select all instances</a></td></tr>
<tr><td><code>Ctrl+Alt+M</code></td><td><a href="shape-selection.html">Select all message</a></td></tr>
<tr><td><code>Ctrl+Alt+F</code></td><td><a href="automatic-drawing.html#add_instances">Add instances</a></td></tr>
Added: trunk/doc/help/frontend/shortcuts.html~
===================================================================
--- trunk/doc/help/frontend/shortcuts.html~ (rev 0)
+++ trunk/doc/help/frontend/shortcuts.html~ 2010-09-07 09:03:38 UTC (rev 877)
@@ -0,0 +1,21 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
+<html>
+<head>
+<title>SCStudio Visio addon keyboard accelerators</title>
+<link href="../help.css" rel="stylesheet" type="text/css">
+</head>
+<body>
+<h1>Visio addon keyboard accelerators</h1>
+<p>The following keyboard accelerators are defined by SCStudio Visio addon:</p>
+<table>
+<col width="100"> <col>
+<tr><td><code>Ctrl+Alt+I</code></td><td><a href="shape-selection.html">Select all instances</a></td></tr>
+<tr><td><code>Ctrl+Alt+M</code></td><td><a href="shape-selection.html">Select all message</a></td></tr>
+<tr><td><code>Ctrl+Alt+F</code></td><td><a href="automatic-drawing.html#add_instances">Add instances</a></td></tr>
+<tr><td><code>Ctrl+Alt+S</code></td><td><a href="automatic-drawing.html#message_sequence">Message sequence</a></td></tr>
+<tr><td><code>Ctrl+Alt+E</code></td><td><a href="message-numbering.html">Message Numbering</a></td></tr>
+<tr><td><code>Ctrl+Alt+D</code></td><td><a href="message-numbering.html">Delete message numbering</a></td></tr>
+</table>
+
+</body>
+</html>
Modified: trunk/doc/help/help.css
===================================================================
--- trunk/doc/help/help.css 2010-09-06 20:10:23 UTC (rev 876)
+++ trunk/doc/help/help.css 2010-09-07 09:03:38 UTC (rev 877)
@@ -1,6 +1,6 @@
body {
font-family: Verdana, Arial, Helvetica, sans-serif;
- font-size: 0.7em;
+ font-size: 1.0em;
color: #000000;
}
p {
@@ -29,3 +29,6 @@
font-size: 1em;
}
+ul.gallery { clear: both; }
+ul.gallery li { list-style-type: none; float: left; }
+ul.gallery li ul li { float: none; text-align: center; font-size: 15px; }
Modified: trunk/doc/help/livelock/livelock.html
===================================================================
--- trunk/doc/help/livelock/livelock.html 2010-09-06 20:10:23 UTC (rev 876)
+++ trunk/doc/help/livelock/livelock.html 2010-09-07 09:03:38 UTC (rev 877)
@@ -12,5 +12,14 @@
<P>SCStudio finds and displays all such cycles in a given HMSC.</P>
<P> An example of livelock is depicted on the next picture. It clearly satisfies all conditions for livelock.</P>
-<P><img src="livelock.png" alt="Typical livelock"></P>
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/livelock.png" width="450" BORDER="0" ALT="Typical livelock" TITLE="Typical livelock"></li>
+ <li>Typical livelock</li>
+ </ul>
+</li>
+</ul>
+</div>
</BODY>
Added: trunk/doc/help/livelock/livelock.html~
===================================================================
--- trunk/doc/help/livelock/livelock.html~ (rev 0)
+++ trunk/doc/help/livelock/livelock.html~ 2010-09-07 09:03:38 UTC (rev 877)
@@ -0,0 +1,25 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
+<HTML>
+<HEAD>
+ <META HTTP-EQUIV="CONTENT-TYPE" CONTENT="text/html; charset=utf-8">
+ <TITLE>Livelock</TITLE>
+ <meta name="author" content="Martin Chmelik">
+ <LINK href="../help.css" rel="stylesheet" type="text/css"/>
+</HEAD>
+<BODY>
+<H1>Livelock</H1>
+<P>is a property of an HMSC. An HMSC contains a livelock if there exists a cycle of nodes from which no endnode is reachable. It is required that the cycle contains at least one reference node.</P>
+
+<P>SCStudio finds and displays all such cycles in a given HMSC.</P>
+<P> An example of livelock is depicted on the next picture. It clearly satisfies all conditions for livelock.</P>
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/livelock.png" width="450" BORDER="0" ALT="Typical livelock" TITLE="Typical livelock"></li>
+ <li>Typical livelock</li>
+ </ul>
+</li>
+</ul>
+</div>
+</BODY>
Added: trunk/doc/help/livelock/pictures/livelock.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/livelock/pictures/livelock.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/livelock/pictures/livelock.vsd
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/livelock/pictures/livelock.vsd
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added...
[truncated message content] |
