[certi-cvs] certi/doc CERTI-tickHandling.xml

[certi-cvs]

CVSROOT:        /sources/certi
Module name:    certi
Changes by:     Eric NOULARD <erk>      10/11/20 17:49:45

Modified files:
        doc            : CERTI-tickHandling.xml 

Log message:
        Uppaal model update

CVSWeb URLs:
http://cvs.savannah.gnu.org/viewcvs/certi/doc/CERTI-tickHandling.xml?cvsroot=certi&r1=1.4&r2=1.5

Patches:
Index: CERTI-tickHandling.xml
===================================================================
RCS file: /sources/certi/certi/doc/CERTI-tickHandling.xml,v
retrieving revision 1.4
retrieving revision 1.5
diff -u -b -r1.4 -r1.5
--- CERTI-tickHandling.xml      20 Nov 2010 16:39:28 -0000      1.4
+++ CERTI-tickHandling.xml      20 Nov 2010 17:49:45 -0000      1.5
@@ -46,7 +46,10 @@
 clock h;
 
 // The number of callback to be processed
-int nbCallbacks=0;</declaration><location id="id0" x="128" y="-480"><name 
x="86" y="-510">TICK_NEXT</name></location><location id="id1" x="-352" 
y="-160"><name x="-408" y="-136">TICK_CALLBACK</name></location><location 
id="id2" x="-344" y="-480"><name x="-368" 
y="-464">TICK_BLOCKING</name></location><location id="id3" x="128" 
y="-160"><name x="90" y="-122">TICK_RETURN</name></location><location id="id4" 
x="-600" y="-312"><name x="-632" y="-344">NO_TICK</name></location><init 
ref="id4"/><transition><source ref="id0"/><target ref="id3"/><label 
kind="guard" x="68" y="-350">h &gt;= 
maxTime[FedRank]</label></transition><transition><source ref="id0"/><target 
ref="id1"/><label kind="guard" x="-416" y="-376">multiple[FedRank] and h &lt; 
maxTime[FedRank]</label><nail x="-64" y="-408"/><nail x="-240" 
y="-288"/></transition><transition><source ref="id1"/><target ref="id0"/><label 
kind="assignment" x="-112" y="-280">moreMsg[FedRank]=true</label><nail x="-176" 
y="-248"/><nail x="0" y="-368"/></transition><transition><source 
ref="id2"/><target ref="id2"/><label kind="guard" x="-424" y="-592">h &lt;= 
minTime[FedRank]</label><nail x="-392" y="-544"/><nail x="-336" y="-568"/><nail 
x="-288" y="-536"/></transition><transition><source ref="id2"/><target 
ref="id0"/><label kind="select" x="-264" y="-544">timeAdvance : BoolRange, 
fedCallback: BoolRange</label><label kind="guard" x="-216" y="-528">timeAdvance 
&gt; 0 or fedCallback &gt; 0</label><label kind="assignment" x="-240" 
y="-512">nbCallbacks++, 
moreMsg[FedRank]=true</label></transition><transition><source 
ref="id1"/><target ref="id3"/></transition><transition><source 
ref="id4"/><target ref="id1"/><label kind="synchronisation" x="-592" 
y="-208">Tick_rq[FedRank]?</label><label kind="assignment" x="-640" 
y="-184">moreMsg[FedRank]=false, h=0</label></transition><transition><source 
ref="id4"/><target ref="id2"/><label kind="guard" x="-640" 
y="-472">minTime[FedRank] &gt;= 0</label><label kind="synchronisation" x="-632" 
y="-448">Tick_rq[FedRank]?</label><label kind="assignment" x="-664" 
y="-424">moreMsg[FedRank]=false, 
h=0</label></transition></template><template><name>libRTI</name><parameter>FederateRange
 FedRank</parameter><declaration>// libRTI is the library linked with the 
Federate
+int nbCallbacks=0;</declaration><location id="id0" x="208" y="-480"><name 
x="166" y="-510">TICK_NEXT</name></location><location id="id1" x="-352" 
y="-160"><name x="-408" y="-136">TICK_CALLBACK</name></location><location 
id="id2" x="-344" y="-480"><name x="-368" 
y="-464">TICK_BLOCKING</name></location><location id="id3" x="208" 
y="-160"><name x="160" y="-144">TICK_RETURN</name></location><location id="id4" 
x="-600" y="-312"><name x="-632" y="-344">NO_TICK</name></location><init 
ref="id4"/><transition><source ref="id3"/><target ref="id4"/><label 
kind="synchronisation" x="-256" y="-24">Tick_rq[FedRank]!</label><nail x="208" 
y="-32"/><nail x="-648" y="-24"/><nail x="-664" 
y="-288"/></transition><transition><source ref="id1"/><target ref="id1"/><label 
kind="select" x="-424" y="-96">fedCallback: BoolRange</label><label 
kind="guard" x="-400" y="-80">fedCallback &gt; 0</label><label 
kind="assignment" x="-432" y="-64">moreMsg[FedRank]=true</label><nail x="-288" 
y="-136"/><nail x="-296" y="-112"/><nail x="-352" y="-96"/><nail x="-416" 
y="-112"/><nail x="-416" y="-136"/></transition><transition><source 
ref="id0"/><target ref="id3"/><label kind="guard" x="224" y="-376">(h &gt;= 
maxTime[FedRank]) or 
+(multiple[FedRank]) or 
+(not moreMsg[FedRank])</label></transition><transition><source 
ref="id0"/><target ref="id1"/><label kind="guard" x="-344" 
y="-384">multiple[FedRank] and 
+h &lt; maxTime[FedRank]</label><nail x="-48" y="-416"/><nail x="-240" 
y="-304"/></transition><transition><source ref="id1"/><target ref="id0"/><label 
kind="guard" x="-96" y="-288">moreMsg[FedRank]==true</label><nail x="-160" 
y="-256"/><nail x="32" y="-360"/></transition><transition><source 
ref="id2"/><target ref="id2"/><label kind="guard" x="-424" y="-592">h &lt;= 
minTime[FedRank]</label><nail x="-392" y="-544"/><nail x="-336" y="-568"/><nail 
x="-288" y="-536"/></transition><transition><source ref="id2"/><target 
ref="id0"/><label kind="select" x="-264" y="-544">timeAdvance : BoolRange, 
fedCallback: BoolRange</label><label kind="guard" x="-216" y="-528">timeAdvance 
&gt; 0 or fedCallback &gt; 0</label><label kind="assignment" x="-240" 
y="-512">nbCallbacks++, 
moreMsg[FedRank]=true</label></transition><transition><source 
ref="id1"/><target ref="id3"/><label kind="guard" x="-152" 
y="-152">moreMsg[FedRank]==false</label></transition><transition><source 
ref="id4"/><target ref="id1"/><label kind="synchronisation" x="-608" 
y="-224">Tick_rq[FedRank]?</label><label kind="assignment" x="-648" 
y="-208">moreMsg[FedRank]=false, h=0</label></transition><transition><source 
ref="id4"/><target ref="id2"/><label kind="guard" x="-640" 
y="-472">minTime[FedRank] &gt;= 0</label><label kind="synchronisation" x="-624" 
y="-456">Tick_rq[FedRank]?</label><label kind="assignment" x="-656" 
y="-440">moreMsg[FedRank]=false, 
h=0</label></transition></template><template><name>libRTI</name><parameter>FederateRange
 FedRank</parameter><declaration>// libRTI is the library linked with the 
Federate
 
 void
 buildTickMessageContent(BoolRange mult, MinTimeRange min, MaxTimeRange max) 
@@ -54,7 +57,7 @@
    multiple[FedRank] = mult ? true : false;
    minTime[FedRank]  = min;
    maxTime[FedRank]  = min + max;
-}</declaration><location id="id5" x="248" y="56"><name x="238" 
y="26">HANDLE_CALLBACK</name></location><location id="id6" x="88" 
y="-192"><name x="40" y="-224">TICKING</name></location><location id="id7" 
x="-320" y="48"><name x="-400" y="8">NOT_TICKING</name></location><init 
ref="id7"/><transition><source ref="id5"/><target ref="id6"/><label 
kind="synchronisation" x="248" y="-168">Tick_rqNext[FedRank]!</label><nail 
x="272" y="-88"/><nail x="208" y="-184"/></transition><transition><source 
ref="id5"/><target ref="id7"/><label kind="synchronisation" x="-112" 
y="64">Tick_rqStop[FedRank]!</label></transition><transition><source 
ref="id6"/><target ref="id5"/></transition><transition><source 
ref="id6"/><target ref="id7"/><label kind="synchronisation" x="-144" 
y="-40">Tick_rq[FedRank]?</label><nail x="-72" y="-64"/><nail x="-176" 
y="-32"/></transition><transition><source ref="id7"/><target ref="id6"/><label 
kind="select" x="-456" y="-224">selmult : BoolRange, min : MinTimeRange, max : 
MaxTimeRange</label><label kind="synchronisation" x="-304" 
y="-208">Tick_rq[FedRank]!</label><label kind="assignment" x="-376" 
y="-192">buildTickMessageContent(selmult,min,max)</label><nail x="-224" 
y="-96"/><nail x="-120" y="-136"/></transition></template><system>// Place 
template instantiations here.
+}</declaration><location id="id5" x="88" y="-192"><name x="112" 
y="-200">TICKING</name></location><location id="id6" x="-320" y="48"><name 
x="-400" y="8">NOT_TICKING</name></location><init 
ref="id6"/><transition><source ref="id5"/><target ref="id6"/><label 
kind="synchronisation" x="-64" y="24">Tick_rqStop[FedRank]!</label><nail x="88" 
y="-56"/><nail x="-104" y="40"/></transition><transition><source 
ref="id5"/><target ref="id5"/><label kind="synchronisation" x="32" 
y="-312">Tick_rqNext[FedRank]!</label><nail x="32" y="-272"/><nail x="96" 
y="-288"/><nail x="200" y="-248"/></transition><transition><source 
ref="id5"/><target ref="id6"/><label kind="synchronisation" x="-144" 
y="-56">Tick_rq[FedRank]?</label><nail x="-16" y="-112"/><nail x="-184" 
y="-40"/></transition><transition><source ref="id6"/><target ref="id5"/><label 
kind="select" x="-536" y="-184">selmult : BoolRange, min : MinTimeRange, max : 
MaxTimeRange</label><label kind="synchronisation" x="-384" 
y="-168">Tick_rq[FedRank]!</label><label kind="assignment" x="-456" 
y="-152">buildTickMessageContent(selmult,min,max)</label><nail x="-224" 
y="-96"/><nail x="-120" y="-136"/></transition></template><system>// Place 
template instantiations here.
 // We instantiate 2 federates (libRTIs) with their corresponding RTIAs
 libRTI_1 = libRTI(1);
 libRTI_2 = libRTI(2);