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

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

Revision: 810
          http://scstudio.svn.sourceforge.net/scstudio/?rev=810&view=rev
Author:   lkorenciak
Date:     2010-05-23 20:46:08 +0000 (Sun, 23 May 2010)

Log Message:
-----------
added help sections for: Correct time constraint syntax, Time Consistency, Time Race and Tighten Time

Modified Paths:
--------------
    trunk/doc/help/algorithms.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

Modified: trunk/doc/help/algorithms.html
===================================================================

--- trunk/doc/help/algorithms.html	2010-05-23 19:43:14 UTC (rev 809)
+++ trunk/doc/help/algorithms.html	2010-05-23 20:46:08 UTC (rev 810)
@@ -7,14 +7,18 @@
 The following verification algorithms are supported:
 <ul>
 <li><a href="acyclic/acyclic.html">Acyclic property</a></li>
+<li><a href="time_syntax/time_syntax.html">Correct Time Constraint Syntax</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="membership/membership.html">Membership</a></li>
 <li><a href="race/race.html">Race Condition</a></li>
-<li><a href="livelock/livelock.html">Livelock</a></li>
-<li><a href="deadlock/deadlock.html">Deadlock</a></li>
+<li><a href="realizability/realizability.html">Strong Realizablilty</a></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="realizability/realizability.html">Strong Realizablilty</a></li>
 </ul>
 </body>
 </html>

Modified: trunk/doc/help/time_consistency/time_consistency.html
===================================================================
--- trunk/doc/help/time_consistency/time_consistency.html	2010-05-23 19:43:14 UTC (rev 809)
+++ trunk/doc/help/time_consistency/time_consistency.html	2010-05-23 20:46:08 UTC (rev 810)
@@ -14,14 +14,13 @@
 <P>Time consistent property is violated for BMSC B when there is no time assignment for B.</P>
 <P>The time assignment for BMSC (resp. HMSC path) is an assignment of time value to every event such that it satisfies all constraints in given BMSC (resp. HMSC path). I.e. for every constraint which restricts two events, the difference of values assigned by assignment to these events must be included in the interval set of this constraint.</P>
 <P>An example of time inconsistent BMSC is depicted on the next picture.</P>
-<img src="pictures/simple_non_fifo.png"  border="0" alt="Example of a non-fifo design" title="Example of a non-fifo design">
+<img src="pictures/cons1.png"  border="0" alt="Time inconsistent BMSC" title="Time inconsistent BMSC">
 
 <H2>High-level MSC</H2>
 
 <P>HMSC violates time consistent property if exists path from start node to end node for which there is no time assignment.</P>
 <P>An example of time inconsistent HMSC is depicted on the next picture.</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">
+<img src="pictures/cons2.png"  border="0" alt="Time inconsistent HMSC" title="Time inconsistent HMSC">
 
 
 </BODY>

Modified: trunk/doc/help/time_syntax/time_syntax.html
===================================================================
--- trunk/doc/help/time_syntax/time_syntax.html	2010-05-23 19:43:14 UTC (rev 809)
+++ trunk/doc/help/time_syntax/time_syntax.html	2010-05-23 20:46:08 UTC (rev 810)
@@ -17,14 +17,13 @@
 </ul> </p>
 
 <P>An example of a time constraint can be seen on the next picture. Receive events of HTTP Response and HTTP request messages are not visually ordered. Thus the time constraint does not satisfy the Correct Time Constraint Syntax property. </P>
-<img src="pictures/simple_non_fifo.png"  border="0" alt="Example of a wrong time constraint" title="Example of a non-fifo design">
+<img src="pictures/syntax3.png"  border="0" alt="Example of a wrong time constraint" title="Example of a wrong BMSC time constraint">
 
-<P>On the next picture we see that there exists path which goes twice through node Connection denied and thus the introduced time constraint also does not satisfy Correct Time Constraint Syntax property.</P>
+<P>On the next picture we see that there exist path which goes twice in a row through the node Connection denied and thus the introduced time constraint also does not satisfy correct time constraint syntax property.</P>
 
-<img src="pictures/fifo1.png"  border="0" alt="FIFO MSC design" title="FIFO MSC design">
+<img src="pictures/syntax1.png"  border="0" alt="Violation of constraint syntax" title="Violation of constraint syntax property">
 
 <P>The last example depicts HMSC where exist path which goes through node A of but does not go through node B. Since there is introduced time constraint restricting these nodes it violates Correct Time Constraint Syntax property.</P>
-<img src="pictures/fifo2.png"  border="0" alt="FIFO MSC design" title="FIFO MSC design">
-
+<img src="pictures/syntax2.png"  border="0" alt="Example of a wrong time constraint" title="Example of a wrong HMSC time constraint">
 </BODY>
 </HTML>

Modified: trunk/doc/help/time_tighten/time_tighten.html
===================================================================
--- trunk/doc/help/time_tighten/time_tighten.html	2010-05-23 19:43:14 UTC (rev 809)
+++ trunk/doc/help/time_tighten/time_tighten.html	2010-05-23 20:46:08 UTC (rev 810)
@@ -14,15 +14,44 @@
 <P>After tighten time algorithm, every constraint contains only values in interval sets for which exists valid time assignment.</p>
 <P>The time assignment for BMSC (resp. HMSC path) is an assignment of time value to every event such that it satisfies all constraints in given BMSC (resp. HMSC path). I.e. for every constraint which restricts two events, the difference of values assigned by assignment to these events must be included in the interval set of this constraint.</P>
 
-<P>An example of a tighten time algorithm on BMSC:</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>An example of the tighten time algorithm on a BMSC:</P>
 
 
+<table><caption align="bottom"><i>Original BMSC</i></caption><tr><td>
+<img src="pictures/tighten2_1.png"  border="0" alt="Original BMSC" title="Original BMSC">
+</tr></td></table>
+
+<table><caption align="bottom"><i>Tightened BMSC</i></caption><tr><td>
+<img src="pictures/tighten2_2.png"  border="0" alt="Tightened BMSC" title="Tightened BMSC">
+</tr></td></table>
+
 <H3> High-level MSC</H3>
 <P>After tighten time algorithm, every constraint contains only values in interval sets for which exists valid time assignment for some path from the start node to the end node.</p>
-<P>An example of tighten time algorithm on HMSC:</P>
+<P>An example of the tighten time algorithm on a HMSC:</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">
+<table><caption align="bottom"><i>Original HMSC</i></caption><tr><td>
+<img src="pictures/tighten1_1.png"  border="0" alt="Original HMSC" title="Original HMSC">
+</tr></td></table>
+
+<table><caption align="bottom"><i>Original BMSC A</i></caption><tr><td>
+<img src="pictures/tighten1_2.png"  border="0" alt="Original BMSC A" title="Original BMSC A">
+</tr></td></table>
+
+<table><caption align="bottom"><i>Original HMSC B</i></caption><tr><td>
+<img src="pictures/tighten1_3.png"  border="0" alt="Original HMSC B" title="Original BMSC B">
+</tr></td></table>
+
+<table><caption align="bottom"><i>Tightened HMSC</i></caption><tr><td>
+<img src="pictures/tighten1_4.png"  border="0" alt="Tightened HMSC" title="Tightened HMSC">
+</tr></td></table>
+
+<table><caption align="bottom"><i>Tightened BMSC A</i></caption><tr><td>
+<img src="pictures/tighten1_5.png"  border="0" alt="Tightened BMSC A" title="Tightened BMSC A">
+</tr></td></table>
+
+<table><caption align="bottom"><i>Tightened BMSC B</i></caption><tr><td>
+<img src="pictures/tighten1_6.png"  border="0" alt="Tightened BMSC B" title="Tightened BMSC B">
+</tr></td></table>
+
 </BODY>
 </HTML>

Modified: trunk/doc/help/time_trace_race/time_race.html
===================================================================
--- trunk/doc/help/time_trace_race/time_race.html	2010-05-23 19:43:14 UTC (rev 809)
+++ trunk/doc/help/time_trace_race/time_race.html	2010-05-23 20:46:08 UTC (rev 810)
@@ -10,15 +10,32 @@
 <H1>Time Race</H1>
 
 <P> Informally, two events are in race if they are specified by user to perform in some order, but there is a possibility that they can perform in inverse order.</P>
-<P> The introduction of time constraints can eliminate some race conditions. For example consider next two pictures. In the first one there is a race between HTTP Request and HTTP Response receive events. However on the second one the added time constraint caused that the BMSC is time race free. </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> The introduction of time constraints can eliminate some race conditions. For example consider next two pictures. In the first one there is a time race between HTTP Request and HTTP Response receive events. However on the second one the added time constraint caused that the BMSC is time race free. </P>
+<table><caption align="bottom"><i>BMSC with the time race</i></caption><tr><td>
+<img src="pictures/race1_1.png"  border="0" alt="BMSC with the time race" title="BMSC with the time race">
+</tr></td></table>
 
+<table><caption align="bottom"><i>Time race free BMSC</i></caption><tr><td>
+<img src="pictures/race1_2.png"  border="0" alt="Time race free BMSC" title="Time race free BMSC">
+</tr></td></table>
+
 <P>BMSC B (or HMSC path p) contains time race if there are two visually ordered events in B (or p), but there exists time assignment which assigns visually preceding event larger time value than the value assigned to subsequent event.</P>
 <P>HMSC contains time race if there exists path which contains time race. </P>
 <P>The time assignment for BMSC (resp. HMSC path) is an assignment of time value to every event such that it satisfies all constraints in given BMSC (resp. HMSC path). I.e. for every constraint which restricts two events, the difference of values assigned by assignment to these events must be included in the interval set of this constraint.</P>
 <P>Time Race algortihm checks the same as the <a href="../race/race.html">race checker</a>, but takes into account also time constraints.</P>
 <P>The next example shows HMSC which contains race condition, but which is time race free.</P>
-<img src="pictures/simple_non_fifo.png"  border="0" alt="Example of a non-fifo design" title="Example of a non-fifo design">
 
+<table><caption align="bottom"><i>BMSC B</i></caption><tr><td>
+<img src="pictures/race2_1.png"  border="0" alt="Example of time race free HMSC" title="Example of time race free HMSC">
+</tr></td></table>
+
+<table><caption align="bottom"><i>BMSC A</i></caption><tr><td>
+<img src="pictures/race2_2.png"  border="0" alt="BMSC A" title="BMSC A">
+</tr></td></table>
+
+<table><caption align="bottom"><i>BMSC B</i></caption><tr><td>
+<img src="pictures/race2_3.png"  border="0" alt="BMSC B" title="BMSC B">
+</tr></td></table>
+
 </BODY>
 </HTML>


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


