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

[<va...@us...>]

Revision: 803
          http://scstudio.svn.sourceforge.net/scstudio/?rev=803&view=rev
Author:   vacek
Date:     2010-05-22 20:32:19 +0000 (Sat, 22 May 2010)

Log Message:
-----------
Help improvements

Modified Paths:
--------------
    trunk/doc/help/boundedness/boundedness.html
    trunk/doc/help/deadlock/deadlock.html
    trunk/doc/help/livelock/livelock.html
    trunk/doc/help/race/race.html
    trunk/doc/help/realizability/realizability.html

Added Paths:
-----------
    trunk/doc/help/boundedness/unbounded.png
    trunk/doc/help/deadlock/deadlock.png
    trunk/doc/help/livelock/livelock.png

Modified: trunk/doc/help/boundedness/boundedness.html
===================================================================
--- trunk/doc/help/boundedness/boundedness.html	2010-05-22 10:32:29 UTC (rev 802)
+++ trunk/doc/help/boundedness/boundedness.html	2010-05-22 20:32:19 UTC (rev 803)
@@ -11,4 +11,7 @@
 <P>is a property of an HMSC. An HMSC is universally bounded if there exists an upper limit on size of communication buffers of all involved processes. Informally, each instance waits for a response before sending the same message again. A dialogue is an example of bounded communication. E-mail spam is an example of unbounded communication - actually, it is not rare that an input buffer (mailbox) gets full in this case. </P>
 
 <P>When all the possible executions of an HMSC are finite, the HMSC is universally bounded. Therefore only HMSCs containing a cycle may be unbounded. Every cycle whose repetitive execution may lead to unbounded grow of an input buffer is found and displayed by SCStudio.</P>
+
+<p>
+<img src="unbounded.png" alt="Unbounded HMSC">
 </BODY>

Added: trunk/doc/help/boundedness/unbounded.png
===================================================================
(Binary files differ)


Property changes on: trunk/doc/help/boundedness/unbounded.png
___________________________________________________________________
Added: svn:mime-type
   + application/octet-stream

Modified: trunk/doc/help/deadlock/deadlock.html
===================================================================
--- trunk/doc/help/deadlock/deadlock.html	2010-05-22 10:32:29 UTC (rev 802)
+++ trunk/doc/help/deadlock/deadlock.html	2010-05-22 20:32:19 UTC (rev 803)
@@ -14,4 +14,7 @@
 SCStudio finds all deadlocked nodes in a given HMSC. For each deadlocked node a path from the start node to the node is available.
 </P>
 
+<p>
+<img src="deadlock.png" alt="Typical deadlock">
+
 </BODY>

Added: trunk/doc/help/deadlock/deadlock.png
===================================================================
(Binary files differ)


Property changes on: trunk/doc/help/deadlock/deadlock.png
___________________________________________________________________
Added: svn:mime-type
   + application/octet-stream

Modified: trunk/doc/help/livelock/livelock.html
===================================================================
--- trunk/doc/help/livelock/livelock.html	2010-05-22 10:32:29 UTC (rev 802)
+++ trunk/doc/help/livelock/livelock.html	2010-05-22 20:32:19 UTC (rev 803)
@@ -11,4 +11,6 @@
 <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><img src="livelock.png" alt="Typical livelock"></P>
 </BODY>

Added: trunk/doc/help/livelock/livelock.png
===================================================================
(Binary files differ)


Property changes on: trunk/doc/help/livelock/livelock.png
___________________________________________________________________
Added: svn:mime-type
   + application/octet-stream

Modified: trunk/doc/help/race/race.html
===================================================================
--- trunk/doc/help/race/race.html	2010-05-22 10:32:29 UTC (rev 802)
+++ trunk/doc/help/race/race.html	2010-05-22 20:32:19 UTC (rev 803)
@@ -8,6 +8,6 @@
 </HEAD>
 <BODY>
 <H1>Race Condition</H1>
-<P>Race Condition occurs in an MSC if a pair of events is drawn in a particular order but the events may occur in the other order during an execution of the MSC. If the real implementation is based on the drawing, it may lead to a system failure. Please don't mix up race condition with FIFO; race condition is only applicable for MSCs that satisfy FIFO.</P>
+<P>Race Condition occurs in an MSC if a pair of events is drawn in a particular order but the events may occur in the other order during an execution of the MSC. If the real implementation is based on the drawing, it may lead to a system failure. Please don't mix up race condition with <a href="../fifo/fifo.html">FIFO</a>; race condition is only applicable for MSCs that satisfy FIFO.</P>
 <P>SCStudio currently finds all such pairs of events in a given BMSC and also in BMSCs referenced by a HMSC. The race condition may also occur between events from different BMSC. SCStudio is capable of finding one such occurence.</P>
 </BODY>

Modified: trunk/doc/help/realizability/realizability.html
===================================================================
--- trunk/doc/help/realizability/realizability.html	2010-05-22 10:32:29 UTC (rev 802)
+++ trunk/doc/help/realizability/realizability.html	2010-05-22 20:32:19 UTC (rev 803)
@@ -8,6 +8,6 @@
 </HEAD>
 <BODY>
 <H1>Strong realizability</H1>
-<P>is a property of an HMSC. An HMSC is strongly realizable iff it is universally bounded and local-choice.</P>
+<P>is a property of an HMSC. An HMSC is strongly realizable iff it is <a href="../boundedness/boundedness.html">universally bounded</a> and <a href="../locaLchoice/localchoice.html">local-choice</a>.</P>
 
 </BODY>


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.