<?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>// ---------------------------------------------
// Global constant or types
// ---------------------------------------------
const   int nbFederate = 2;
typedef int[1,nbFederate] FederateRange;

typedef int[0,1] BoolRange;
typedef int[0,10] MinTimeRange;
typedef int[0,10] MaxTimeRange;

// ---------------------------------------------
// Global communication channels (synchro)
// ---------------------------------------------
// Channel for sending/receicving M_Tick_Request
chan Tick_rq[FederateRange];

// Channel for sending/receicving M_Tick_Request_Next
chan Tick_rqNext[FederateRange];

// Channel for sending/receicving M_Tick_Request_Stop
chan Tick_rqStop[FederateRange];

// Does the tick request multiple callbacks?
bool multiple[FederateRange] = {false, false};

// Is there more callbacks to handle?
bool moreMsg[FederateRange]   = {false, false};

// Does current tick has minTime
int minTime[FederateRange] = {0,0}; 

// Does current tick has maxTime
int maxTime[FederateRange]= {0,0};
</declaration><template><name x="5" y="5">RTIA</name><parameter>FederateRange FedRank</parameter><declaration>// RTIA is the CERTI LRC process linked with the Federate
// a Federate and its associated RTIA communicates through messages
// which are implemented as Uppaal chan (globals)
//
// The RTIA may not be handling more than one tick request
// (originating from Federate/libRTI) at a time.
// However tick request may be split up into different
// requests:
//   - TICK_REQUEST,
//   - TICK_REQUEST_NEXT,
//   - TICK_REQUEST_STOP,

clock h;

// The number of callback to be processed
int nbCallbacks=0;</declaration><location id="id0" x="272" y="-440"><name x="230" y="-470">TICK_NEXT</name></location><location id="id1" x="-288" y="-120"><name x="-344" y="-96">TICK_CALLBACK</name></location><location id="id2" x="-280" y="-440"><name x="-304" y="-424">TICK_BLOCKING</name></location><location id="id3" x="272" y="-120"><name x="224" y="-104">TICK_RETURN</name></location><location id="id4" x="-536" y="-272"><name x="-568" y="-304">NO_TICK</name></location><init ref="id4"/><transition><source ref="id3"/><target ref="id4"/><label kind="synchronisation" x="-192" y="16">Tick_rq[FedRank]!</label><nail x="272" y="8"/><nail x="-584" y="16"/><nail x="-600" y="-248"/></transition><transition><source ref="id1"/><target ref="id1"/><label kind="select" x="-360" y="-56">fedCallback: BoolRange</label><label kind="guard" x="-336" y="-40">fedCallback &gt; 0</label><label kind="assignment" x="-368" y="-24">moreMsg[FedRank]=true</label><nail x="-224" y="-96"/><nail x="-232" y="-72"/><nail x="-288" y="-56"/><nail x="-352" y="-72"/><nail x="-352" y="-96"/></transition><transition><source ref="id0"/><target ref="id3"/><label kind="guard" x="288" y="-336">(h &gt;= maxTime[FedRank]) or 
(multiple[FedRank]) or 
(not moreMsg[FedRank])</label></transition><transition><source ref="id0"/><target ref="id1"/><label kind="guard" x="-280" y="-344">multiple[FedRank] and 
h &lt; maxTime[FedRank]</label><nail x="16" y="-376"/><nail x="-176" y="-264"/></transition><transition><source ref="id1"/><target ref="id0"/><label kind="guard" x="-32" y="-248">moreMsg[FedRank]==true</label><nail x="-96" y="-216"/><nail x="96" y="-320"/></transition><transition><source ref="id2"/><target ref="id2"/><label kind="guard" x="-360" y="-552">h &lt;= minTime[FedRank]</label><nail x="-328" y="-504"/><nail x="-272" y="-528"/><nail x="-224" y="-496"/></transition><transition><source ref="id2"/><target ref="id0"/><label kind="select" x="-200" y="-504">timeAdvance : BoolRange, fedCallback: BoolRange</label><label kind="guard" x="-152" y="-488">timeAdvance &gt; 0 or fedCallback &gt; 0</label><label kind="assignment" x="-176" y="-472">nbCallbacks++, moreMsg[FedRank]=true</label></transition><transition><source ref="id1"/><target ref="id3"/><label kind="guard" x="-88" y="-112">moreMsg[FedRank]==false</label></transition><transition><source ref="id4"/><target ref="id1"/><label kind="synchronisation" x="-544" y="-184">Tick_rq[FedRank]?</label><label kind="assignment" x="-584" y="-168">moreMsg[FedRank]=false, h=0</label></transition><transition><source ref="id4"/><target ref="id2"/><label kind="guard" x="-576" y="-432">minTime[FedRank] &gt;= 0</label><label kind="synchronisation" x="-560" y="-416">Tick_rq[FedRank]?</label><label kind="assignment" x="-592" y="-400">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) 
{
   multiple[FedRank] = mult ? true : false;
   minTime[FedRank]  = min;
   maxTime[FedRank]  = min + max;
}</declaration><location id="id5" x="-72" y="-320"><name x="-48" y="-328">TICKING</name></location><location id="id6" x="-480" y="-80"><name x="-560" y="-120">NOT_TICKING</name></location><init ref="id6"/><transition><source ref="id5"/><target ref="id6"/><label kind="synchronisation" x="-224" y="-104">Tick_rqStop[FedRank]!</label><nail x="-72" y="-184"/><nail x="-264" y="-88"/></transition><transition><source ref="id5"/><target ref="id5"/><label kind="synchronisation" x="-128" y="-440">Tick_rqNext[FedRank]!</label><nail x="-128" y="-400"/><nail x="-64" y="-416"/><nail x="40" y="-376"/></transition><transition><source ref="id5"/><target ref="id6"/><label kind="synchronisation" x="-304" y="-184">Tick_rq[FedRank]?</label><nail x="-176" y="-240"/><nail x="-344" y="-168"/></transition><transition><source ref="id6"/><target ref="id5"/><label kind="select" x="-696" y="-312">selmult : BoolRange, min : MinTimeRange, max : MaxTimeRange</label><label kind="synchronisation" x="-544" y="-296">Tick_rq[FedRank]!</label><label kind="assignment" x="-616" y="-280">buildTickMessageContent(selmult,min,max)</label><nail x="-384" y="-224"/><nail x="-280" y="-264"/></transition></template><system>// Place template instantiations here.
// We instantiate 2 federates (libRTIs) with their corresponding RTIAs
libRTI_1 = libRTI(1);
libRTI_2 = libRTI(2);
RTIA_1 = RTIA(1);
RTIA_2 = RTIA(2);


// List of processes which composed the system.
system libRTI_1, RTIA_1, libRTI_2, RTIA_2;</system></nta>