Created attachment 233 [details]
A dummy model with this problem.

property to check: A[] not deadlock && tail <= MAX

Comment on attachment 233 [details]
A dummy model with this problem.

<?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 SPEED = 12;
const int delta = 2;

const int EMPTY = 0;
//const int initTask = 1;

const int Task1 = 2;
const int Task1_1 = 3;
const int Task1_2 = 4;
const int Task1_3 = 5;
const int Task2 = 6;
const int Task2_1 = 7;

const int MSG = 7;	// MAX message number
meta  int[0,MSG] msg;
/************  ************/
int val;
clock c;
clock xdone;

chan delegate; 	// let's not allow explicit delegation and thus no labels here
chan invoke;
urgent chan start[MSG+1];
urgent chan finish;
chan stop;

/************* LOCAL VARIABLES ****************/
/**********************************************/
// The Min &amp; Max definitions help to simplify verification
const int MD = 10;	// Minimum deadline value
const int XD = 12;	// Maximum deadline value
const int INIT_DEADLINE = XD;
meta  int[MD,XD] deadline;
/***********************************************/
// Queue declarations here.
const int MAX = 4;	// queue length is MAX

int[0,MSG]   q [MAX];	// one extra, because we set run to MAX when queue is disabled (in shift)
int[0,MAX-1] ca[MAX];	// clock assigned
int          v[MAX];

int[MD,XD] d[MAX];
clock x[MAX];
int[0,MAX] counter[MAX];

int[0,MAX+1] tail;	// when tail == MAX+1 means queue overflow

</declaration><template><name>m_task2</name><location id="id0" x="-64" y="-16"></location><location id="id1" x="-192" y="-16"></location><init ref="id1"/><transition><source ref="id1"/><target ref="id0"/><label kind="assignment" x="-159" y="-62">c:=val</label><nail x="-168" y="-60"/><nail x="-98" y="-60"/></transition></template><template><name>Queue</name><declaration>int dca;

void insert(int msg,int pos,int dclock){
	int a=tail;
	if (tail &lt; MAX){
		while (a &gt; pos) {
			q[a] = q[a-1];
			v[a] = v[a-1];
			ca[a] = ca[a-1];
			a--;
		}
		q[pos] = msg;
		v[pos] = val;
		val = 0;
		ca[pos] = dclock;
		counter[dclock]++;
	}
	tail ++;
}

int firstFree(){
	int i;
	for (i = 0; i &lt; MAX; i++) {
		if (counter[i] == 0) {
			return i;
		}
	}
	return 0;
}

</declaration><location id="id2" x="-512" y="-32"><committed/></location><location id="id3" x="-296" y="-32"></location><init ref="id3"/><transition><source ref="id2"/><target ref="id3"/><label kind="guard" x="-520" y="-104">x[ca[0]] - x[dca] &gt;= d[ca[0]] - d[dca]</label><nail x="-512" y="-79"/><nail x="-296" y="-79"/></transition><transition><source ref="id3"/><target ref="id2"/><label kind="synchronisation" x="-386" y="-47">delegate?</label></transition></template><system>// Place template instantiations here.

// List one or more processes to be composed into a system.
system m_task2,Queue;
</system></nta>

Created attachment 236 [details]
A dummy model with this problem