<?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_2.dtd'>
<nta>
	<declaration>/*
*  --------- BEGIN CONFIGURATION SECTION
*/
const bool Periodic = true;

const int MaxTime = 21;
typedef int[0,MaxTime] time_t;

const int Tasks = 5;                 // Number of tasks
typedef int[0,Tasks-1] t_id;

const int Procs = 3;                 // Number of resources
typedef int[0,Procs-1] r_id;

typedef struct { 
  time_t initial_offset;
  time_t min_period;
  time_t max_period;
  time_t offset;
  time_t deadline;
  time_t bcet;
  time_t wcet;
  r_id resource;
  int pri;  
} task_t;

//init_offset, min_period, max_period, offset, deadline, bcet, wcet, resource, priority
const task_t task[Tasks] = {
{0,20,20,0,20,6,6,0,1},
{0,20,20,0,20,6,6,0,1},
{0,20,20,0,20,10,10,1,1},
{0,20,20,0,20,4,4,1,1},
{0,20,20,0,20,5,5,2,1}
};

typedef struct {
  int[0,Tasks] length;
  t_id element[Tasks];
} buffer_t; 

buffer_t buffer[Procs];

const int Policies      = 3;
const int EDF  		= 0;
const int FIFO 		= 1;
const int FPS  		= 2;

chan inserted, insert_task[Policies];
typedef int[0,Policies-1] policy_t;

/*
* Task graph definition of dependencies
*
* Meaning of Depend[i][j]:
*    - 0/false : task i does not depend on task j
*    - 1/true  : task i depends on task j
*/
const bool Depend[Tasks][Tasks] = {  // Task graph
{0,0,0,0,0},
{1,0,0,0,0},
{0,0,0,0,0},
{0,0,1,0,1},
{1,0,0,0,0}
};

/*
*  --------- END CONFIGURATION SECTION
*/
clock time[Tasks];//, exec[Tasks];
bool complete[Tasks];


urgent chan ready[Procs];
chan finished[Tasks];//run[Procs+1], stop[Procs], done[Procs];


meta struct {
  meta t_id task;
  meta r_id resource;
  meta bool preempt;
} param;

void setParams(t_id t, r_id r, bool preempt) {
  param.task = t; param.resource = r; param.preempt = preempt;
}

meta t_id ready_task;

void insert_at(int[0,Tasks] pos, t_id tid, r_id rid) {
  int i;
  for(i = buffer[rid].length; i &gt; pos; i--) {
    buffer[rid].element[i] = buffer[rid].element[i-1];
  }
  buffer[rid].element[pos] = tid;
  buffer[rid].length++;

}

</declaration>
	<template>
		<name>Resource</name>
		<parameter>const r_id id, bool preemptive, policy_t policy</parameter>
		<declaration>
void removeTask() {
  int i = 0;
  buffer[id].length--;
  do {
    buffer[id].element[i] = buffer[id].element[i+1];
    i++;
  } while (i &lt; buffer[id].length);
  buffer[id].element[buffer[id].length] = 0;
}

t_id front() { return buffer[id].element[0]; }

bool empty() {
  return buffer[id].length == 0;
}</declaration>
		<location id="id0" x="-336" y="-240">
			<committed/>
		</location>
		<location id="id1" x="-56" y="-240">
			<committed/>
		</location>
		<location id="id2" x="-496" y="-288">
			<committed/>
		</location>
		<location id="id3" x="-448" y="-128">
			<name x="-464" y="-112">InUse</name>
		</location>
		<location id="id4" x="-336" y="-288">
			<name x="-352" y="-320">Idle</name>
		</location>
		<init ref="id4"/>
		<transition>
			<source ref="id1"/>
			<target ref="id3"/>
			<label kind="guard" x="-144" y="-216">empty()</label>
			<label kind="assignment" x="-312" y="-200">insert_at(0,ready_task,id)</label>
			<nail x="-104" y="-184"/>
			<nail x="-376" y="-184"/>
		</transition>
		<transition>
			<source ref="id0"/>
			<target ref="id3"/>
			<label kind="synchronisation" x="-400" y="-224">inserted?</label>
			<nail x="-336" y="-208"/>
			<nail x="-408" y="-208"/>
			<nail x="-448" y="-184"/>
		</transition>
		<transition>
			<source ref="id1"/>
			<target ref="id0"/>
			<label kind="guard" x="-304" y="-256">!empty()</label>
			<label kind="synchronisation" x="-232" y="-256">insert_task[policy]!</label>
			<label kind="assignment" x="-320" y="-240">setParams(ready_task,id,preemptive)</label>
		</transition>
		<transition>
			<source ref="id3"/>
			<target ref="id2"/>
			<label kind="synchronisation" x="-608" y="-184">finished[front()]?</label>
			<label kind="assignment" x="-592" y="-216">removeTask()</label>
			<nail x="-496" y="-128"/>
		</transition>
		<transition>
			<source ref="id3"/>
			<target ref="id1"/>
			<label kind="synchronisation" x="-128" y="-152">ready[id]?</label>
			<nail x="-56" y="-128"/>
		</transition>
		<transition>
			<source ref="id2"/>
			<target ref="id3"/>
			<label kind="guard" x="-472" y="-248">!empty()</label>
			<nail x="-480" y="-256"/>
			<nail x="-480" y="-160"/>
		</transition>
		<transition>
			<source ref="id2"/>
			<target ref="id4"/>
			<label kind="guard" x="-472" y="-312">empty()</label>
		</transition>
		<transition>
			<source ref="id4"/>
			<target ref="id1"/>
			<label kind="synchronisation" x="-128" y="-288">ready[id]?</label>
			<nail x="-56" y="-288"/>
		</transition>
	</template>
	<template>
		<name x="5" y="5">Task</name>
		<parameter>const t_id id</parameter>
		<declaration>clock x;

bool dependencies_met() {
  return forall (j : t_id)  Depend[id][j] imply complete[j];
}

void completed() {
  complete[id] = true;
}

void new_period() {
//  int i = 0;
//  for ( i  = 0; i &lt; Tasks; i++) {
//    complete[i] = false;
//  }
  complete[id] = false;
}

time_t initialOffset() { return task[id].initial_offset; }
time_t minPeriod() { return task[id].min_period; }
time_t maxPeriod() { return task[id].max_period; }
time_t offset() { return task[id].offset; }
time_t deadline() { return task[id].deadline; }
time_t BCET() { return task[id].bcet; }
time_t WCET() { return task[id].wcet; }
time_t resource() { return task[id].resource; }
time_t priotiry() { return task[id].pri; }

int[0,1] isRunning() {
  return (buffer[resource()].element[0] == id? 1 : 0);
}


</declaration>
		<location id="id5" x="-32" y="-320">
			<name x="-16" y="-336">WaitingDepedency</name>
			<label kind="invariant" x="-16" y="-320">x' == 0</label>
		</location>
		<location id="id6" x="-256" y="-120">
			<name x="-272" y="-152">Done</name>
			<label kind="invariant" x="-280" y="-104">x' == 0</label>
		</location>
		<location id="id7" x="-32" y="-120">
			<committed/>
		</location>
		<location id="id8" x="-248" y="-376">
			<committed/>
		</location>
		<location id="id9" x="-248" y="-480">
			<name x="-256" y="-512">Initial</name>
			<label kind="invariant" x="-224" y="-496">x' == 0 &amp;&amp;
time[id] &lt;= initialOffset()</label>
		</location>
		<location id="id10" x="-256" y="-232" color="#ff0000">
			<name x="-272" y="-264">Error</name>
		</location>
		<location id="id11" x="-32" y="-56">
			<name x="-16" y="-64">PeriodDone</name>
			<label kind="invariant" x="-88" y="-40">x' == 0 &amp;&amp;
time[id] &lt;= maxPeriod()</label>
		</location>
		<location id="id12" x="-32" y="-232">
			<name x="-16" y="-240">Ready</name>
			<label kind="invariant" x="32" y="-248">x' == isRunning() &amp;&amp;
x &lt;= WCET()</label>
		</location>
		<location id="id13" x="-32" y="-376">
			<name x="-56" y="-408">WaitingOffset</name>
			<label kind="invariant" x="-8" y="-392">x' == 0 &amp;&amp;
time[id] &lt;= offset()</label>
		</location>
		<init ref="id9"/>
		<transition>
			<source ref="id13"/>
			<target ref="id5"/>
			<label kind="guard" x="-24" y="-360">time[id] == offset()</label>
		</transition>
		<transition>
			<source ref="id7"/>
			<target ref="id6"/>
			<label kind="guard" x="-112" y="-144">!Periodic</label>
		</transition>
		<transition>
			<source ref="id7"/>
			<target ref="id11"/>
			<label kind="guard" x="-24" y="-104">Periodic</label>
		</transition>
		<transition>
			<source ref="id9"/>
			<target ref="id8"/>
			<label kind="guard" x="-240" y="-448">time[id] == initialOffset()</label>
		</transition>
		<transition>
			<source ref="id8"/>
			<target ref="id13"/>
			<label kind="assignment" x="-232" y="-392">time[id] = 0, x = 0,
new_period()</label>
		</transition>
		<transition>
			<source ref="id11"/>
			<target ref="id8"/>
			<label kind="guard" x="-288" y="-80">time[id] &gt;= minPeriod()</label>
			<nail x="-296" y="-56"/>
			<nail x="-296" y="-376"/>
		</transition>
		<transition>
			<source ref="id12"/>
			<target ref="id10"/>
			<label kind="guard" x="-232" y="-248">time[id] &gt; deadline()</label>
		</transition>
		<transition>
			<source ref="id12"/>
			<target ref="id7"/>
			<label kind="guard" x="-24" y="-200">x &gt;= BCET()</label>
			<label kind="synchronisation" x="-24" y="-176">finished[id]!</label>
			<label kind="assignment" x="-24" y="-152">completed()</label>
		</transition>
		<transition>
			<source ref="id5"/>
			<target ref="id12"/>
			<label kind="guard" x="-24" y="-304">dependencies_met()</label>
			<label kind="synchronisation" x="-24" y="-288">ready[resource()]!</label>
			<label kind="assignment" x="-24" y="-264">ready_task = id</label>
		</transition>
	</template>
	<template>
		<name>Policy_FIFO</name>
		<location id="id14" x="-176" y="-128">
			<committed/>
		</location>
		<location id="id15" x="-176" y="-248">
		</location>
		<init ref="id15"/>
		<transition>
			<source ref="id14"/>
			<target ref="id15"/>
			<label kind="synchronisation" x="-256" y="-128">inserted!</label>
			<nail x="-224" y="-128"/>
			<nail x="-224" y="-248"/>
		</transition>
		<transition>
			<source ref="id15"/>
			<target ref="id14"/>
			<label kind="synchronisation" x="-168" y="-232">insert_task[FIFO]?</label>
			<label kind="assignment" x="-168" y="-200">insert_at(buffer[param.resource].length,
	param.task,
	param.resource)</label>
		</transition>
	</template>
	<template>
		<name>Policy_FPS</name>
		<declaration>
void insert_task_in_buffer() {
  t_id t = param.task;
  r_id r = param.resource;
  int place = (param.preempt ? 0 : 1);
  int i;
  // Find out where to put the task
  while ( place &lt; buffer[r].length &amp;&amp; task[buffer[r].element[place]].pri &gt;= task[t].pri ) {
    place++;
  }
  insert_at(place,t,r);
}</declaration>
		<location id="id16" x="-176" y="-144">
			<committed/>
		</location>
		<location id="id17" x="-176" y="-248">
		</location>
		<init ref="id17"/>
		<transition>
			<source ref="id16"/>
			<target ref="id17"/>
			<label kind="synchronisation" x="-256" y="-144">inserted!</label>
			<nail x="-216" y="-144"/>
			<nail x="-216" y="-248"/>
		</transition>
		<transition>
			<source ref="id17"/>
			<target ref="id16"/>
			<label kind="synchronisation" x="-168" y="-224">insert_task[FPS]?</label>
			<label kind="assignment" x="-168" y="-192">insert_task_in_buffer()</label>
		</transition>
	</template>
	<template>
		<name>Policy_EDF</name>
		<declaration>int[0,Tasks] place;
t_id tid;
r_id rid;
bool preempt;

void readParameters() {
  tid = param.task; rid = param.resource; preempt = param.preempt;
}

void resetVars() {
  place = tid = rid = 0;
}</declaration>
		<location id="id18" x="-176" y="-128">
			<committed/>
		</location>
		<location id="id19" x="-176" y="-264">
			<committed/>
		</location>
		<location id="id20" x="-176" y="-384">
		</location>
		<init ref="id20"/>
		<transition>
			<source ref="id18"/>
			<target ref="id20"/>
			<label kind="synchronisation" x="-288" y="-176">inserted!</label>
			<label kind="assignment" x="-304" y="-232">resetVars()</label>
			<nail x="-224" y="-128"/>
			<nail x="-224" y="-384"/>
		</transition>
		<transition>
			<source ref="id19"/>
			<target ref="id19"/>
			<label kind="guard" x="-128" y="-304">place &lt; buffer[rid].length &amp;&amp;
time[tid]-task[tid].deadline &lt;=
time[buffer[rid].element[place]] - task[buffer[rid].element[place]].deadline</label>
			<label kind="assignment" x="-128" y="-256">place++</label>
			<nail x="-136" y="-280"/>
			<nail x="-136" y="-248"/>
		</transition>
		<transition>
			<source ref="id19"/>
			<target ref="id18"/>
			<label kind="guard" x="-168" y="-232">place == buffer[rid].length ||
time[tid]-task[tid].deadline &gt;
time[buffer[rid].element[place]] - task[buffer[rid].element[place]].deadline</label>
			<label kind="assignment" x="-168" y="-176">insert_at(place,tid,rid)</label>
		</transition>
		<transition>
			<source ref="id20"/>
			<target ref="id19"/>
			<label kind="synchronisation" x="-168" y="-368">insert_task[EDF]?</label>
			<label kind="assignment" x="-168" y="-344">readParameters(),
place = (preempt ? 0 : 1)</label>
		</transition>
	</template>
	<system>

//Task id, res. ass., bcet, wcet, deadline, offset, period

P0  = Resource(0,true,FPS);
P1  = Resource(1,true,FPS);
Bus = Resource(2,false,FIFO);

system Task, P0, P1, Bus, Policy_FPS, Policy_FIFO;</system>
	<queries>
		<query>
			<formula>A[] forall (i : t_id) not Task(i).Error
			</formula>
			<comment>
			</comment>
		</query>
	</queries>
</nta>
