[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[certi-cvs] certi/doc NullMessageProtocol.xml
|
From: |
certi-cvs |
|
Subject: |
[certi-cvs] certi/doc NullMessageProtocol.xml |
|
Date: |
Fri, 20 Aug 2010 12:45:39 +0000 |
CVSROOT: /sources/certi
Module name: certi
Changes by: jbchaudron <jbchaudron> 10/08/20 12:45:39
Modified files:
doc : NullMessageProtocol.xml
Log message:
Update for FederationLiveLocked State For Observer Template
CVSWeb URLs:
http://cvs.savannah.gnu.org/viewcvs/certi/doc/NullMessageProtocol.xml?cvsroot=certi&r1=1.5&r2=1.6
Patches:
Index: NullMessageProtocol.xml
===================================================================
RCS file: /sources/certi/certi/doc/NullMessageProtocol.xml,v
retrieving revision 1.5
retrieving revision 1.6
diff -u -b -r1.5 -r1.6
--- NullMessageProtocol.xml 17 Aug 2010 14:57:05 -0000 1.5
+++ NullMessageProtocol.xml 20 Aug 2010 12:45:39 -0000 1.6
@@ -114,11 +114,11 @@
} // End of updateLBTS(int federate, int ts)
</declaration><location id="id0" x="912" y="-56"><name x="880"
y="-96">Terminate</name></location><location id="id1" x="336" y="-56"><name
x="264" y="-64">Process</name></location><location id="id2" x="-168"
y="-56"><name x="-144" y="-64">Wait</name></location><location id="id3"
x="-608" y="-56"><name x="-624" y="-96">Init</name></location><init
ref="id3"/><transition><source ref="id0"/><target ref="id0"/><label
kind="comments">This transition is because a system could never terminate
really in UPPAAL Model</label><nail x="968" y="0"/><nail x="864"
y="0"/></transition><transition><source ref="id1"/><target ref="id1"/><label
kind="guard" x="376" y="248">StepWithoutLBTSchange >=
NumberOffStepForLiveLock and
LiveLockforFederate == 0</label><label kind="synchronisation" x="488"
y="232">LiveLockDetected[id]!</label><label kind="assignment" x="488"
y="280">LiveLockforFederate = 1</label><nail x="480" y="96"/><nail x="576"
y="216"/><nail x="512" y="216"/></transition><transition><source
ref="id2"/><target ref="id2"/><label kind="guard" x="-432"
y="248">StepWithoutLBTSchange >= NumberOffStepForLiveLock and
-LiveLockforFederate == 0</label><label kind="synchronisation" x="-344"
y="232">LiveLockDetected[id]!</label><label kind="assignment" x="-344"
y="280">LiveLockforFederate = 1</label><nail x="-296" y="168"/><nail x="-288"
y="224"/><nail x="-232" y="232"/></transition><transition><source
ref="id1"/><target ref="id1"/><label kind="guard" x="624" y="-200">nbMsgIn !=
0</label><label kind="assignment" x="632" y="-216">checkFIFO()</label><nail
x="548" y="-182"/><nail x="604" y="-198"/><nail x="624" y="-176"/><nail x="584"
y="-136"/></transition><transition><source ref="id1"/><target ref="id1"/><label
kind="select" x="608" y="96">senderId: RangeFederateId</label><label
kind="synchronisation" x="632" y="112">nullMsg[senderId]?</label><label
kind="assignment" x="544"
y="128">updateLBTS(senderId,nullMsgTimestamp[senderId])</label><nail x="616"
y="48"/><nail x="688" y="88"/><nail x="608"
y="88"/></transition><transition><source ref="id1"/><target ref="id0"/><label
kind="guard" x="480" y="-48">(Clocks[id] >= MaxSimulationTime ) and
(nbMsgIn ==0)</label><label kind="synchronisation" x="624"
y="-32">nullMsg[id]!</label><label kind="assignment" x="528"
y="-16">nullMsgTimestamp[id] =
MaxSimulationTime</label></transition><transition><source ref="id2"/><target
ref="id2"/><label kind="select" x="-616" y="-216">senderId:
RangeFederateId</label><label kind="synchronisation" x="-576"
y="-184">nullMsg[senderId]?</label><label kind="assignment" x="-712"
y="-200">updateLBTS(senderId,nullMsgTimestamp[senderId])</label><nail x="-424"
y="-136"/><nail x="-440" y="-176"/><nail x="-344"
y="-176"/></transition><transition><source ref="id2"/><target ref="id2"/><label
kind="select" x="-560" y="120">srcId: RangeFederateId</label><label
kind="guard" x="-624" y="104">(srcId != id) and (nbMsgIn <
MaxMsgFIFOSize)</label><label kind="synchronisation" x="-536"
y="88">msg[srcId][id]?</label><label kind="assignment" x="-600"
y="136">addToFIFO(msgTimestamp[srcId][id])</label><nail x="-424" y="80"/><nail
x="-528" y="80"/><nail x="-472" y="24"/><nail x="-344"
y="0"/></transition><transition><source ref="id1"/><target ref="id1"/><label
kind="guard" x="304" y="-320">(nbMsgIn !=0) and (AllMsgConsuming ==
0)</label><label kind="assignment" x="392" y="-336">popFromFIFO()</label><label
kind="comments">FIFOMsgTimestamp[nbMsgIn-1] <= (Clocks[id]+lookahead)
+LiveLockforFederate == 0</label><label kind="synchronisation" x="-344"
y="232">LiveLockDetected[id]!</label><label kind="assignment" x="-344"
y="280">LiveLockforFederate = 1</label><nail x="-296" y="168"/><nail x="-288"
y="224"/><nail x="-232" y="232"/></transition><transition><source
ref="id1"/><target ref="id1"/><label kind="guard" x="624" y="-200">nbMsgIn !=
0</label><label kind="assignment" x="632" y="-216">checkFIFO()</label><nail
x="548" y="-182"/><nail x="604" y="-198"/><nail x="624" y="-176"/><nail x="584"
y="-136"/></transition><transition><source ref="id1"/><target ref="id1"/><label
kind="select" x="608" y="96">senderId: RangeFederateId</label><label
kind="synchronisation" x="632" y="112">nullMsg[senderId]?</label><label
kind="assignment" x="544"
y="128">updateLBTS(senderId,nullMsgTimestamp[senderId])</label><nail x="616"
y="48"/><nail x="688" y="88"/><nail x="608"
y="88"/></transition><transition><source ref="id1"/><target ref="id0"/><label
kind="guard" x="480" y="-48">(Clocks[id] >= MaxSimulationTime ) and
(nbMsgIn ==0)</label><label kind="synchronisation" x="624"
y="-32">nullMsg[id]!</label><label kind="assignment" x="528"
y="-16">nullMsgTimestamp[id] =
MaxSimulationTime</label></transition><transition><source ref="id2"/><target
ref="id2"/><label kind="select" x="-616" y="-216">senderId:
RangeFederateId</label><label kind="synchronisation" x="-576"
y="-184">nullMsg[senderId]?</label><label kind="assignment" x="-712"
y="-200">updateLBTS(senderId,nullMsgTimestamp[senderId])</label><nail x="-424"
y="-136"/><nail x="-440" y="-176"/><nail x="-344"
y="-176"/></transition><transition><source ref="id2"/><target ref="id2"/><label
kind="select" x="-560" y="120">srcId: RangeFederateId</label><label
kind="guard" x="-624" y="104">(srcId != id) and (nbMsgIn <
MaxMsgFIFOSize)</label><label kind="synchronisation" x="-536"
y="88">msg[srcId][id]?</label><label kind="assignment" x="-600"
y="136">addToFIFO(msgTimestamp[srcId][id])</label><nail x="-424" y="80"/><nail
x="-528" y="80"/><nail x="-472" y="24"/></transition><transition><source
ref="id1"/><target ref="id1"/><label kind="guard" x="304" y="-320">(nbMsgIn
!=0) and (AllMsgConsuming == 0)</label><label kind="assignment" x="392"
y="-336">popFromFIFO()</label><label
kind="comments">FIFOMsgTimestamp[nbMsgIn-1] <= (Clocks[id]+lookahead)
J'ai enlevé cette partie car cela faisait une erreur lorsque nbMsgIn etait
egual à 0
-Normalement le checkFIFO() resous le probleme</label><nail x="384"
y="-248"/><nail x="408" y="-288"/><nail x="464" y="-280"/><nail x="448"
y="-240"/></transition><transition><source ref="id2"/><target ref="id2"/><label
kind="select" x="-472" y="-352">destId: RangeFederateId, timestamp:
RangeSimulationTime</label><label kind="guard" x="-592" y="-336">destId != id
and (timestamp > (Clocks[id]+lookahead)) and (timestamp <=
MaxSimulationTime)</label><label kind="synchronisation" x="-352"
y="-320">msg[id][destId]!</label><label kind="assignment" x="-456"
y="-368">msgTimestamp[id][destId]=timestamp</label><nail x="-288"
y="-232"/><nail x="-288" y="-288"/><nail x="-248" y="-288"/><nail x="-216"
y="-232"/></transition><transition><source ref="id1"/><target ref="id2"/><label
kind="guard" x="-120" y="40">(AllMsgConsuming == 1) and (Clocks[id] <
MaxSimulationTime )</label><label kind="synchronisation" x="40"
y="8">nullMsg[id]!</label><label kind="assignment" x="-72"
y="24">nullMsgTimestamp[id]=Clocks[id]+lookahead</label><nail x="216"
y="8"/><nail x="-64" y="8"/></transition><transition><source ref="id2"/><target
ref="id1"/><label kind="assignment" x="24"
y="-136">Clocks[id]=LBTS</label><nail x="-64" y="-112"/><nail x="216"
y="-112"/></transition><transition><source ref="id3"/><target ref="id2"/><label
kind="assignment" x="-512" y="-48">resetClocks(),
clearFIFO()</label></transition></template><template><name>Observant</name><declaration>//
Place local declarations here for the Observateur template.
+Normalement le checkFIFO() resous le probleme</label><nail x="384"
y="-248"/><nail x="408" y="-288"/><nail x="464" y="-280"/><nail x="448"
y="-240"/></transition><transition><source ref="id2"/><target ref="id2"/><label
kind="select" x="-472" y="-352">destId: RangeFederateId, timestamp:
RangeSimulationTime</label><label kind="guard" x="-592" y="-336">destId != id
and (timestamp > (Clocks[id]+lookahead)) and (timestamp <=
MaxSimulationTime)</label><label kind="synchronisation" x="-352"
y="-320">msg[id][destId]!</label><label kind="assignment" x="-456"
y="-368">msgTimestamp[id][destId]=timestamp</label><nail x="-288"
y="-232"/><nail x="-288" y="-288"/><nail x="-248" y="-288"/><nail x="-216"
y="-232"/></transition><transition><source ref="id1"/><target ref="id2"/><label
kind="guard" x="-120" y="40">(AllMsgConsuming == 1) and (Clocks[id] <
MaxSimulationTime )</label><label kind="synchronisation" x="40"
y="8">nullMsg[id]!</label><label kind="assignment" x="-72"
y="24">nullMsgTimestamp[id]=Clocks[id]+lookahead</label><nail x="216"
y="8"/><nail x="-64" y="8"/></transition><transition><source ref="id2"/><target
ref="id1"/><label kind="assignment" x="24"
y="-136">Clocks[id]=LBTS</label><nail x="-64" y="-112"/><nail x="216"
y="-112"/></transition><transition><source ref="id3"/><target ref="id2"/><label
kind="assignment" x="-512" y="-48">resetClocks(),
clearFIFO()</label></transition></template><template><name>Observer</name><declaration>//
Place local declarations here for the Observateur template.
int nullMsgFromEachFed[nbFederates];
int LiveLockFromEachFed[nbFederates];
int FlagForFederationLiveLock = 0 ;
@@ -150,7 +150,7 @@
if (LiveLockFromEachFed[i] != 0 && FlagForFederationLiveLock ==1)
FlagForFederationLiveLock = 1;
else FlagForFederationLiveLock = 0;
}
-} // End of updateNullMessage(int federate)</declaration><location id="id4"
x="208" y="-184"><name x="96"
y="-224">FederationLiveLocked</name></location><location id="id5" x="-64"
y="0"><name x="-74" y="-30">Look</name></location><location id="id6" x="-520"
y="0"><name x="-530" y="-30">Init_Observant</name></location><init
ref="id6"/><transition><source ref="id5"/><target ref="id5"/><label
kind="select" x="344"
y="120">FederateLiveLockedId:RangeFederateId</label><label
kind="synchronisation" x="344"
y="136">LiveLockDetected[FederateLiveLockedId]?</label><label kind="assignment"
x="328" y="152">updateLiveLockWatchDog(FederateLiveLockedId)</label><nail
x="292" y="80"/><nail x="324" y="144"/><nail x="300" y="216"/><nail x="228"
y="192"/></transition><transition><source ref="id4"/><target ref="id4"/><nail
x="352" y="-248"/><nail x="360" y="-144"/></transition><transition><source
ref="id5"/><target ref="id4"/><label kind="guard" x="-140"
y="-126">FlagForFederationLiveLock == 1</label></transition><transition><source
ref="id5"/><target ref="id5"/><label kind="select" x="-176" y="248">senderId:
RangeFederateId</label><label kind="synchronisation" x="-152"
y="264">nullMsg[senderId]?</label><label kind="assignment" x="-208"
y="280">updateNullMessageWatchDog(senderId)</label><nail x="-72" y="184"/><nail
x="-72" y="240"/><nail x="-120" y="240"/><nail x="-168"
y="184"/></transition><transition><source ref="id6"/><target ref="id5"/><label
kind="assignment" x="-432" y="0">initialiseNullMessageWatchDog(),
+} // End of updateNullMessage(int federate)</declaration><location id="id4"
x="208" y="-184" color="#ff0000"><name x="96"
y="-224">FederationLiveLocked</name></location><location id="id5" x="56"
y="0"><name x="32" y="-32">Look</name></location><location id="id6" x="-520"
y="0"><name x="-530" y="-30">Init_Observant</name></location><init
ref="id6"/><transition><source ref="id5"/><target ref="id5"/><label
kind="select" x="488"
y="152">FederateLiveLockedId:RangeFederateId</label><label
kind="synchronisation" x="488"
y="168">LiveLockDetected[FederateLiveLockedId]?</label><label kind="assignment"
x="464" y="184">updateLiveLockWatchDog(FederateLiveLockedId)</label><nail
x="444" y="144"/><nail x="448" y="216"/><nail x="400"
y="216"/></transition><transition><source ref="id4"/><target ref="id4"/><nail
x="352" y="-248"/><nail x="360" y="-144"/></transition><transition><source
ref="id5"/><target ref="id4"/><label kind="guard" x="-140"
y="-126">FlagForFederationLiveLock == 1</label></transition><transition><source
ref="id5"/><target ref="id5"/><label kind="select" x="-56" y="248">senderId:
RangeFederateId</label><label kind="synchronisation" x="-32"
y="264">nullMsg[senderId]?</label><label kind="assignment" x="-88"
y="280">updateNullMessageWatchDog(senderId)</label><nail x="48" y="184"/><nail
x="48" y="240"/><nail x="0" y="240"/><nail x="-48"
y="184"/></transition><transition><source ref="id6"/><target ref="id5"/><label
kind="assignment" x="-368" y="0">initialiseNullMessageWatchDog(),
initialiseLiveLockWatchDog()</label></transition></template><system>// Place
template instantiations here.
Federate0 = Federate(0,nbFederates,0);