Menu
▾
▴
[Scstudio-commits] SF.net SVN: scstudio:[885] trunk/doc/help
|
From: <ag...@us...> - 2010-09-08 07:30:47
|
Revision: 885
http://scstudio.svn.sourceforge.net/scstudio/?rev=885&view=rev
Author: agmy
Date: 2010-09-08 07:30:40 +0000 (Wed, 08 Sep 2010)
Log Message:
-----------
help, added unique instacne, non-recursivity, improved race, fixed non local choice
Modified Paths:
--------------
trunk/doc/help/algorithms.html
trunk/doc/help/localchoice/pictures/simple_nonlocal_MSCB.png
trunk/doc/help/race/race.html
Added Paths:
-----------
trunk/doc/help/race/pictures/
trunk/doc/help/race/pictures/easyrace_1.png
trunk/doc/help/race/pictures/easyrace_2.png
trunk/doc/help/race/pictures/easyrace_result.png
trunk/doc/help/race/pictures/trickyrace_1.png
trunk/doc/help/race/pictures/trickyrace_2.png
trunk/doc/help/race/pictures/trickyrace_3.png
trunk/doc/help/recursivity/
trunk/doc/help/recursivity/pictures/
trunk/doc/help/recursivity/pictures/recursivity.vsd
trunk/doc/help/recursivity/pictures/recursivity1.png
trunk/doc/help/recursivity/pictures/recursivity2.png
trunk/doc/help/recursivity/pictures/recursivity3.png
trunk/doc/help/recursivity/recursivity.html
trunk/doc/help/unique_instance/
trunk/doc/help/unique_instance/pictures/
trunk/doc/help/unique_instance/pictures/uniqueinstance.png
trunk/doc/help/unique_instance/pictures/uniqueinstance.vsd
trunk/doc/help/unique_instance/pictures/uniqueinstance2.png
trunk/doc/help/unique_instance/unique_instance.html
Modified: trunk/doc/help/algorithms.html
===================================================================
--- trunk/doc/help/algorithms.html 2010-09-07 22:14:50 UTC (rev 884)
+++ trunk/doc/help/algorithms.html 2010-09-08 07:30:40 UTC (rev 885)
@@ -13,7 +13,7 @@
<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>
+<li><a href="unique_instance/unique_instance.html">Unique instance names</a></li>
</ul>
<h2>HMSC</h2>
@@ -25,7 +25,7 @@
<li><a href="membership/membership.html">Membership</a></li>
<li><a href="localchoice/localchoice.html">Nonlocal Choice</a></li>
<li><a href="realizability/realizability.html">Strong Realizablilty</a></li>
-<li>Non-recursivity</li>
+<li><a href="recursivity/recursivity.html">Non-recursivity</li>
<li><a href="time_consistency/time_consistency.html">Time Consistency</a></li>
<li><a href="time_trace_race/time_race.html">Time Race</a></li>
<li><a href="time_tighten/time_tighten.html">Tighten Time</a></li>
Modified: trunk/doc/help/localchoice/pictures/simple_nonlocal_MSCB.png
===================================================================
(Binary files differ)
Added: trunk/doc/help/race/pictures/easyrace_1.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/race/pictures/easyrace_1.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/race/pictures/easyrace_2.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/race/pictures/easyrace_2.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/race/pictures/easyrace_result.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/race/pictures/easyrace_result.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/race/pictures/trickyrace_1.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/race/pictures/trickyrace_1.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/race/pictures/trickyrace_2.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/race/pictures/trickyrace_2.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/race/pictures/trickyrace_3.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/race/pictures/trickyrace_3.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Modified: trunk/doc/help/race/race.html
===================================================================
--- trunk/doc/help/race/race.html 2010-09-07 22:14:50 UTC (rev 884)
+++ trunk/doc/help/race/race.html 2010-09-08 07:30:40 UTC (rev 885)
@@ -9,7 +9,54 @@
<BODY>
<H1>Race Condition</H1>
<P>Race Condition occurs in an BMSC 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>
+<P>SCStudio currently finds all such pairs of events in a given BMSC and also in BMSCs referenced by a HMSC. On the next picture there is an example of an BMSC which contains race condition:
-<P>On the next picture there is an example of an BMSC which contains race condition. The receive events of messages ... but it is possibele that...</P>
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/easyrace_1.png" width="300" BORDER="0" ALT="Input BMSC" TITLE="Input BMSC"></li>
+ <li>Input BMSC</li>
+ </ul></li>
+<li>
+ <ul>
+
+ <li><IMG SRC="pictures/easyrace_2.png" width="300" BORDER="0" ALT="Possible execution" TITLE="Possible execution"></li>
+ <li>Possible execution</li>
+ </ul>
+</li>
+<li>
+ <ul>
+
+ <li><IMG SRC="pictures/easyrace_result.png" width="300" BORDER="0" ALT="SCStudio result" TITLE="SCStudio result"></li>
+ <li>SCStudio result</li>
+ </ul>
+</li>
+</ul>
+</div>
+<p style="clear: both;">
+The race condition may also occur between events from different BMSC. SCStudio is capable of finding one such occurence:</P>
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/trickyrace_1.png" width="100" BORDER="0" ALT="Input HMSC" TITLE="Input HMSC"></li>
+ <li>Input HMSC with a race</li>
+ </ul></li>
+<li>
+ <ul>
+
+ <li><IMG SRC="pictures/trickyrace_2.png" width="300" BORDER="0" ALT="MSC A" TITLE="MSC A"></li>
+ <li>MSC A</li>
+ </ul>
+</li>
+<li>
+ <ul>
+
+ <li><IMG SRC="pictures/trickyrace_3.png" width="300" BORDER="0" ALT="MSC B" TITLE="MSC B"></li>
+ <li>MSC B</li>
+ </ul>
+</li>
+</ul>
+</div>
+
</BODY>
Added: trunk/doc/help/recursivity/pictures/recursivity.vsd
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/recursivity/pictures/recursivity.vsd
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/recursivity/pictures/recursivity1.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/recursivity/pictures/recursivity1.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/recursivity/pictures/recursivity2.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/recursivity/pictures/recursivity2.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/recursivity/pictures/recursivity3.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/recursivity/pictures/recursivity3.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/recursivity/recursivity.html
===================================================================
--- trunk/doc/help/recursivity/recursivity.html (rev 0)
+++ trunk/doc/help/recursivity/recursivity.html 2010-09-08 07:30:40 UTC (rev 885)
@@ -0,0 +1,39 @@
+<!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>Non recursivity</H1>
+<P> ensures that no HMSC can reference itself (even indirectly). By this condition no infinite unfolding of HMSCs is allowed. Infinite behaviors should be achieved by using cycles, not by using recursion.</P>
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/recursivity1.png" width="150" BORDER="0" ALT="Input HMSC" TITLE="Input HMSC"></li>
+ <li>Input HMSC</li>
+ </ul></li>
+<li>
+ <ul>
+
+ <li><IMG SRC="pictures/recursivity2.png" width="150" BORDER="0" ALT="HMSC A violating non recursivity" TITLE="HMSC A violating non recursivity"></li>
+ <li>HMSC A violating non recursivity</li>
+ </ul>
+</li>
+<li>
+ <ul>
+
+ <li><IMG SRC="pictures/recursivity3.png" width="150" BORDER="0" ALT="Non recursive HMSC" TITLE="Non recursive HMSC"></li>
+ <li>Non recursive HMSC</li>
+ </ul>
+</li>
+
+</ul>
+</div>
+
+
+<p style="clear: both;">
+
+</BODY>
\ No newline at end of file
Property changes on: trunk/doc/help/recursivity/recursivity.html
___________________________________________________________________
Added: svn:executable
+ *
Added: trunk/doc/help/unique_instance/pictures/uniqueinstance.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/unique_instance/pictures/uniqueinstance.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/unique_instance/pictures/uniqueinstance.vsd
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/unique_instance/pictures/uniqueinstance.vsd
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/unique_instance/pictures/uniqueinstance2.png
===================================================================
(Binary files differ)
Property changes on: trunk/doc/help/unique_instance/pictures/uniqueinstance2.png
___________________________________________________________________
Added: svn:executable
+ *
Added: svn:mime-type
+ application/octet-stream
Added: trunk/doc/help/unique_instance/unique_instance.html
===================================================================
--- trunk/doc/help/unique_instance/unique_instance.html (rev 0)
+++ trunk/doc/help/unique_instance/unique_instance.html 2010-09-08 07:30:40 UTC (rev 885)
@@ -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>Acyclic property</TITLE>
+ <meta name="author" content="Martin Chmelik">
+ <LINK href="../help.css" rel="stylesheet" type="text/css"/>
+</HEAD>
+<BODY>
+<H1>Unique instance names</H1>
+<P> ensures that there are no two instances with the same name within a BMSC.</P>
+
+<div style="margin: 0 auto;">
+<ul class="gallery"><li>
+ <ul>
+ <li><IMG SRC="pictures/uniqueinstance.png" width="350" BORDER="0" ALT="BMSC violating unique instance names" TITLE="BMSC violating unique instance names"></li>
+ <li>BMSC violating unique instance names</li>
+ </ul></li>
+<li>
+ <ul>
+
+ <li><IMG SRC="pictures/uniqueinstance2.png" width="350" BORDER="0" ALT="SCStudio result" TITLE="SCStudio result"></li>
+ <li>SCStudio result</li>
+ </ul>
+</li>
+</ul>
+</div>
+
+<p style="clear: both;">
+
+</BODY>
\ No newline at end of file
Property changes on: trunk/doc/help/unique_instance/unique_instance.html
___________________________________________________________________
Added: svn:executable
+ *
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
