[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: |
Tue, 17 Aug 2010 14:57:05 +0000 |
CVSROOT: /sources/certi
Module name: certi
Changes by: jbchaudron <jbchaudron> 10/08/17 14:57:05
Modified files:
doc : NullMessageProtocol.xml
Log message:
Updating the Live Lock detection by reducing the number of
synchronization needed between each federate templates
CVSWeb URLs:
http://cvs.savannah.gnu.org/viewcvs/certi/doc/NullMessageProtocol.xml?cvsroot=certi&r1=1.4&r2=1.5
Patches:
Index: NullMessageProtocol.xml
===================================================================
RCS file: /sources/certi/certi/doc/NullMessageProtocol.xml,v
retrieving revision 1.4
retrieving revision 1.5
diff -u -b -r1.4 -r1.5
--- NullMessageProtocol.xml 17 Aug 2010 13:59:54 -0000 1.4
+++ NullMessageProtocol.xml 17 Aug 2010 14:57:05 -0000 1.5
@@ -4,9 +4,9 @@
const int MaxMsgFIFOSize = 2;
const int MaxMsgSendForEachSimStep = 2;
-const int NumberOffStepForLiveLock = 15 ;
+const int NumberOffStepForLiveLock = 20 ;
-const int MaxSimulationTime = 20;
+const int MaxSimulationTime = 10;
typedef int[0,MaxSimulationTime] RangeSimulationTime;
// Synchronization channel used to send/receive messages
@@ -34,6 +34,7 @@
// Flag to known how many step are pass without any modification of LBTS
int StepWithoutLBTSchange =0;
+int LiveLockforFederate = 0;
// number of message in Timestamped FIFO
int nbMsgIn = 0;
@@ -111,7 +112,9 @@
if (LBTS == LBTS_tmp) ++StepWithoutLBTSchange;
else StepWithoutLBTSchange = 0;
} // 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"/><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</label><label kind="synchronisation" x="488"
y="232">LiveLockDetected[id]!</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</label><label
kind="synchronisation" x="-344" y="232">LiveLockDetected[id]!</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)
+</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)
J'ai enlevé cette partie car cela faisait une erreur lorsque nbMsgIn etait
egual à 0
@@ -147,12 +150,13 @@
if (LiveLockFromEachFed[i] != 0 && FlagForFederationLiveLock ==1)
FlagForFederationLiveLock = 1;
else FlagForFederationLiveLock = 0;
}
-} // End of updateNullMessage(int federate)</declaration><location id="id4"
x="64" y="-192"><name x="-48"
y="-232">FederationLiveLocked</name></location><location id="id5" x="-64"
y="0"><name x="-74" y="-30">Look</name></location><location id="id6" x="-584"
y="0"></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="176" y="-256"/><nail x="224" y="-200"/><nail x="216"
y="-152"/></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="-512" y="0">initialiseNullMessageWatchDog(),
+} // 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(),
initialiseLiveLockWatchDog()</label></transition></template><system>// Place
template instantiations here.
-Federate0 = Federate(0,nbFederates,1);
+Federate0 = Federate(0,nbFederates,0);
Federate1 = Federate(1,nbFederates,0);
-Federate2 = Federate(2,nbFederates,2);
+Federate2 = Federate(2,nbFederates,1);
+
// List one or more processes to be composed into a system.
system Federate0, Federate1, Federate2, Observant;