[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: |
Mon, 16 Aug 2010 08:48:40 +0000 |
CVSROOT: /sources/certi
Module name: certi
Changes by: jbchaudron <jbchaudron> 10/08/16 08:48:40
Modified files:
doc : NullMessageProtocol.xml
Log message:
First UPPAAL model working for Null Messages Algorithm
CVSWeb URLs:
http://cvs.savannah.gnu.org/viewcvs/certi/doc/NullMessageProtocol.xml?cvsroot=certi&r1=1.2&r2=1.3
Patches:
Index: NullMessageProtocol.xml
===================================================================
RCS file: /sources/certi/certi/doc/NullMessageProtocol.xml,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -b -r1.2 -r1.3
--- NullMessageProtocol.xml 14 Aug 2010 12:59:22 -0000 1.2
+++ NullMessageProtocol.xml 16 Aug 2010 08:48:40 -0000 1.3
@@ -4,7 +4,7 @@
const int MaxMsgFIFOSize = 5;
const int MaxMsgSendForEachSimStep = 2;
-const int MaxSimulationTime = 10;
+const int MaxSimulationTime = 15;
typedef int[0,MaxSimulationTime] RangeSimulationTime;
// Synchronization channel used to send/receive messages
@@ -35,7 +35,7 @@
// int nbMsgOut = 0;
// Variable for know if all msg with timestamp less than localtime + lookahead
are cossuming during the simulation process
-int AllMsgConsuming = 0;
+int AllMsgConsuming = 1;
void clearFIFO() {
int i;
@@ -86,8 +86,6 @@
LBTS = Clocks[0];
if (id==0) LBTS = Clocks[1];
- if (id==1) LBTS = Clocks[2];
- // LBTS = 100000 ;
for (i=0;i<nbFederates; ++i) {
if(i!=id) {
@@ -98,11 +96,11 @@
}
}
}
-</declaration><location id="id0" x="640" y="-48"><name x="608"
y="-88">Terminate</name></location><location id="id1" x="208" y="-48"><name
x="136" y="-56">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="id1"/><target ref="id1"/><label
kind="guard" x="544" y="-224">(AllMsgConsuming == 0) and (nbMsgIn !=
0)</label><label kind="assignment" x="580" y="-234">checkFIFO()</label><nail
x="436" y="-210"/><nail x="540" y="-234"/><nail x="580" y="-210"/><nail x="524"
y="-178"/></transition><transition><source ref="id1"/><target ref="id1"/><label
kind="select" x="320" y="64">senderId: RangeFederateId</label><label
kind="synchronisation" x="352" y="80">nullMsg[senderId]?</label><label
kind="assignment" x="304"
y="96">updateLBTS(senderId,nullMsgTimestamp[senderId])</label><nail x="320"
y="0"/><nail x="400" y="56"/><nail x="320"
y="80"/></transition><transition><source ref="id1"/><target ref="id0"/><label
kind="guard" x="328" y="-72">(Clocks[id] >= MaxSimulationTime) and
(AllMsgConsuming == 1) and (nbMsgIn ==0)</label><label kind="synchronisation"
x="364" y="-63">nullMsg[id]!</label><label kind="assignment" x="296"
y="-40">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="-216" y="152">srcId: RangeFederateId</label><label
kind="guard" x="-264" y="136">(srcId != id) and (nbMsgIn <
MaxMsgFIFOSize)</label><label kind="synchronisation" x="-192"
y="120">msg[srcId][id]?</label><label kind="assignment" x="-256"
y="168">addToFIFO(msgTimestamp[srcId][id])</label><nail x="-104" y="56"/><nail
x="-112" y="120"/><nail x="-176" y="120"/><nail x="-184"
y="64"/></transition><transition><source ref="id1"/><target ref="id1"/><label
kind="guard" x="80" y="-328">(nbMsgIn !=0) and (AllMsgConsuming ==
0)</label><label kind="assignment" x="328" y="-344">popFromFIFO()</label><label
kind="comments">FIFOMsgTimestamp[nbMsgIn-1] <= (Clocks[id]+lookahead)
+</declaration><location id="id0" x="784" y="-48"><name x="752"
y="-88">Terminate</name></location><location id="id1" x="208" y="-48"><name
x="136" y="-56">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="912"
y="-16"/><nail x="936" y="32"/><nail x="896"
y="40"/></transition><transition><source ref="id1"/><target ref="id1"/><label
kind="guard" x="576" y="-216">nbMsgIn != 0</label><label kind="assignment"
x="580" y="-234">checkFIFO()</label><nail x="436" y="-210"/><nail x="540"
y="-234"/><nail x="580" y="-210"/><nail x="524"
y="-178"/></transition><transition><source ref="id1"/><target ref="id1"/><label
kind="select" x="320" y="64">senderId: RangeFederateId</label><label
kind="synchronisation" x="352" y="80">nullMsg[senderId]?</label><label
kind="assignment" x="304"
y="96">updateLBTS(senderId,nullMsgTimestamp[senderId])</label><nail x="320"
y="0"/><nail x="400" y="56"/><nail x="320"
y="80"/></transition><transition><source ref="id1"/><target ref="id0"/><label
kind="guard" x="304" y="-48">(Clocks[id] >= MaxSimulationTime ) and
(nbMsgIn ==0)</label><label kind="synchronisation" x="448"
y="-32">nullMsg[id]!</label><label kind="assignment" x="352"
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="-344" y="168">srcId: RangeFederateId</label><label
kind="guard" x="-392" y="152">(srcId != id) and (nbMsgIn <
MaxMsgFIFOSize)</label><label kind="synchronisation" x="-320"
y="136">msg[srcId][id]?</label><label kind="assignment" x="-384"
y="184">addToFIFO(msgTimestamp[srcId][id])</label><nail x="-232" y="64"/><nail
x="-248" y="136"/><nail x="-288" y="136"/><nail x="-304"
y="64"/></transition><transition><source ref="id1"/><target ref="id1"/><label
kind="guard" x="192" y="-328">(nbMsgIn !=0) and (AllMsgConsuming ==
0)</label><label kind="assignment" x="328" y="-344">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="264"
y="-240"/><nail x="280" y="-280"/><nail x="336" y="-272"/><nail x="320"
y="-240"/></transition><transition><source ref="id2"/><target ref="id2"/><label
kind="select" x="-472" y="-360">destId: RangeFederateId, timestamp:
RangeSimulationTime</label><label kind="guard" x="-592" y="-344">destId != id
and (timestamp > (Clocks[id]+lookahead)) and (timestamp <
MaxSimulationTime)</label><label kind="synchronisation" x="-352"
y="-328">msg[id][destId]!</label><label kind="assignment" x="-456"
y="-376">msgTimestamp[id][destId]=timestamp</label><nail x="-288"
y="-232"/><nail x="-272" y="-288"/><nail x="-224" y="-288"/><nail x="-216"
y="-232"/></transition><transition><source ref="id1"/><target ref="id2"/><label
kind="guard" x="-24" y="56">AllMsgConsuming == 1</label><label
kind="synchronisation" x="0" y="24">nullMsg[id]!</label><label
kind="assignment" x="-112" y="40">nullMsgTimestamp[id]=Clocks[id]+lookahead,
AllMsgConsuming = 0</label><nail x="104" y="8"/><nail x="-32"
y="8"/></transition><transition><source ref="id2"/><target ref="id1"/><label
kind="guard" x="-8" y="-136">nbMsgIn > 0</label><label kind="assignment"
x="-24" y="-152">Clocks[id]=LBTS</label><nail x="-48" y="-112"/><nail x="72"
y="-112"/></transition><transition><source ref="id3"/><target ref="id2"/><label
kind="assignment" x="-568" y="-40">resetClocks(),
clearFIFO()</label></transition></template><system>// Place template
instantiations here.
+Normalement le checkFIFO() resous le probleme</label><nail x="264"
y="-240"/><nail x="280" y="-280"/><nail x="336" y="-272"/><nail x="320"
y="-240"/></transition><transition><source ref="id2"/><target ref="id2"/><label
kind="select" x="-472" y="-360">destId: RangeFederateId, timestamp:
RangeSimulationTime</label><label kind="guard" x="-592" y="-344">destId != id
and (timestamp > (Clocks[id]+lookahead)) and (timestamp <=
MaxSimulationTime)</label><label kind="synchronisation" x="-352"
y="-328">msg[id][destId]!</label><label kind="assignment" x="-456"
y="-376">msgTimestamp[id][destId]=timestamp</label><nail x="-288"
y="-232"/><nail x="-272" y="-288"/><nail x="-224" y="-288"/><nail x="-216"
y="-232"/></transition><transition><source ref="id1"/><target ref="id2"/><label
kind="guard" x="-40" y="48">(AllMsgConsuming == 1) and (Clocks[id] <
MaxSimulationTime )</label><label kind="synchronisation" x="-8"
y="16">nullMsg[id]!</label><label kind="assignment" x="-120"
y="32">nullMsgTimestamp[id]=Clocks[id]+lookahead</label><nail x="104"
y="8"/><nail x="-32" y="8"/></transition><transition><source ref="id2"/><target
ref="id1"/><label kind="assignment" x="-24"
y="-152">Clocks[id]=LBTS</label><nail x="-48" y="-112"/><nail x="72"
y="-112"/></transition><transition><source ref="id3"/><target ref="id2"/><label
kind="assignment" x="-568" y="-40">resetClocks(),
clearFIFO()</label></transition></template><system>// Place template
instantiations here.
Federate0 = Federate(0,nbFederates,3);
Federate1 = Federate(1,nbFederates,3);