<?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// Place global declarations here.
const int nbFederates    = 3;
typedef int[0,nbFederates-1] RangeFederateId;
const int MaxMsgFIFOSize = 2;
const int MaxMsgSendForEachSimStep = 2;

const int NumberOffStepForLiveLock = 20 ;

const int MaxSimulationTime = 10;
typedef int[0,MaxSimulationTime] RangeSimulationTime;

// Synchronization channel used to send/receive messages
chan msg[nbFederates][nbFederates];

// Timestamps of the corresponding send/receive messages
int  msgTimestamp[nbFederates][nbFederates];

// Null message channel
broadcast chan nullMsg[nbFederates];
int            nullMsgTimestamp[nbFederates];

// Channel to detect LiveLock of Federation
chan LiveLockDetected[nbFederates] ;
</declaration><template><name x="5" y="5">Federate</name><parameter>const RangeFederateId id, const int nbFederates, const int initialLk</parameter><declaration>// Place local declarations here for the Federate template.

// Array of clocks representing the local time of me and the evaluation of local time for other federates
int Clocks[nbFederates];

// lookahead parameter usefull for Null Message Algorithm [Chandy&amp;Misra]
int lookahead = initialLk;

// Lower Bound on Time Stamp now called GALT 
int   LBTS=0; 

// 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;
int   FIFOMsgTimestamp[MaxMsgFIFOSize];

// number of messages sending by the federate on each simulation step
// int   nbMsgOut = 0;

// Variable for know if all msg with timestamp less than localtime + lookahead are cossuming during the simulation process
int AllMsgConsuming = 1;

// Initialize each FIFO with 0 timestamp for each federate
void clearFIFO() {
   int i;
   nbMsgIn = 0;
   for (i=0;i&lt;MaxMsgFIFOSize;++i) {
       FIFOMsgTimestamp[i] = 0 ;
       }
} // End of clearFIFO()

// Set all clocks to zero (me and others)
void resetClocks() {
  int i;
  for (i=0;i&lt;nbFederates;++i) {
      Clocks[i] = 0;
      }
} // End of resetClocks()

// Adding one element to the receip FIFO file and sorting it by greater timestamp first
void addToFIFO(int ts) {
   int i,j;
   ++nbMsgIn;
   // insert in order
   i = 0;
   while (FIFOMsgTimestamp[i]&gt;ts) ++i;
   for (j=nbMsgIn-1;j&gt;i;--j) {
       FIFOMsgTimestamp[j] = FIFOMsgTimestamp[j-1];
       }
   FIFOMsgTimestamp[i]=ts;
} // End of addToFIFO(int ts)

// Consuming the first element from FIFO file
void popFromFIFO() {
         FIFOMsgTimestamp[nbMsgIn-1] = 0;
         nbMsgIn--;
         if (nbMsgIn == 0) AllMsgConsuming = 1;
} // End of popFromFIFO()

// Checking if FIFO contains another element to be treated on each simulation step
void checkFIFO() { 
         if (FIFOMsgTimestamp[nbMsgIn-1] &lt;= (Clocks[id] + lookahead)) AllMsgConsuming = 0;
         else AllMsgConsuming = 1;           
} // End of checkFIFO()
        
// Updating the Lower Bound Time Step for each Null Message receving by the federate
void updateLBTS(int federate, int ts) {
     int i;
     int t;
     int LBTS_tmp;
     
     Clocks[federate] = ts;
     LBTS_tmp = LBTS ;

     LBTS = Clocks[0];
     if (id==0) LBTS = Clocks[1];

     for (i=0;i&lt;nbFederates; ++i) {
        if(i!=id) {
          t = Clocks[i];
          if (t &lt; LBTS) {
             LBTS = t;
          }
        }
     }
    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"/><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 &gt;= 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 &gt;= 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] &gt;= 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 &lt; 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] &lt;= (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 &gt; (Clocks[id]+lookahead)) and (timestamp &lt;= 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] &lt; 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 ;

// Place for functions usefull in updates
void initialiseNullMessageWatchDog() {
  int i;
  for (i=0;i&lt;nbFederates;++i) {
      nullMsgFromEachFed[i] = 0;
      }
} // End of initialiseNullMessage()

void updateNullMessageWatchDog(int federate) {
++nullMsgFromEachFed[federate];
} // End of updateNullMessage(int federate)

void initialiseLiveLockWatchDog() {
  int i;
  for (i=0;i&lt;nbFederates;++i) {
      LiveLockFromEachFed[i] = 0;
      }
} // End of initialiseLiveLockWatchDog()

void updateLiveLockWatchDog(int federate) {
int i;
++LiveLockFromEachFed[federate];
for (i=0; i&lt;nbFederates;++i) {
     if (i==0) FlagForFederationLiveLock = 1;
     if (LiveLockFromEachFed[i] != 0 &amp;&amp; FlagForFederationLiveLock ==1) FlagForFederationLiveLock = 1;
     else FlagForFederationLiveLock = 0;
    }
} // 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);
Federate1 = Federate(1,nbFederates,0);
Federate2 = Federate(2,nbFederates,1);


// List one or more processes to be composed into a system.
system Federate0, Federate1, Federate2, Observant;
</system></nta>