extern real java.lang.Math.pow(real, real)
extern real java.lang.Math.sin(real)
extern real java.lang.Math.cos(real)
extern real java.lang.Math.sqrt(real)

agent aircrafts () {
	private signal real x1;
	private signal real y1;
	private signal real x2;
	private signal real y2;
	private signal real minDistance;
	private signal real minDistanceTime;
	private signal real r;
	private signal real t;

	agent a1 = aircraft1();
	agent a2 = aircraft2();
	agent w = watcher();
}

agent aircraft1() {
	output signal real x1;
	output signal real y1;

	mode main = main1();
}

agent aircraft2() {
	output signal real x2;
	output signal real y2;

	mode main = main2();
}

agent watcher() {
	input signal real x1;
	input signal real y1;
	input signal real x2;
	input signal real y2;
	output signal real minDistance;
	output signal real minDistanceTime;
	output signal real r;
	output signal real t;

	mode main = mainw();
}

mode main1() {
	output signal real x1;
	output signal real y1;

	mode op = operation1();

	trans from default to op when true do {}

}

mode main2() {
	output signal real x2;
	output signal real y2;

	mode op = operation2();

	trans from default to op when true do {}

}

mode mainw() {
	input signal real x1;
	input signal real y1;
	input signal real x2;
	input signal real y2;
	output signal real minDistance;
	output signal real minDistanceTime;
	output signal real r;
	output signal real t;

	mode op = operationw();

	trans from default to op when true do {}
}

mode operationw() {
	input signal real x1;
	input signal real y1;
	input signal real x2;
	input signal real y2;
	output signal real minDistance;
	output signal real minDistanceTime;
	output signal real r;
	output signal real t;

	mode modeWatching = md();

	trans from default to modeWatching when true do { minDistance=50000 }
	trans from modeWatching to modeWatching when r<minDistance && t>1 do { minDistance=r; minDistanceTime=t }

	alge { r == java.lang.Math.sqrt((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2)) }

	diff { d(t) == 1 }

}

mode operation1() {
	output signal real x1;
	output signal real y1;
	private signal real h;
	private signal real v;
	private signal real mf;
	private signal real T;
	private signal real phi;
	private signal real psi;
	private signal real m;
	private signal real CD;
	private signal real CL;
	private signal real S;
	private signal real ro;
	private signal real nu;
	private signal real g;
	private signal real apsi;

	mode md0 = md();
	mode cruise1 = md();
	mode turn1 = md();
	mode cruise2 = md();
	mode turn2 = md();
	mode cruise3 = md();

	trans from default to md0 when true do {}
	sttrans from md0 when true distr 0 to cruise1 do { mf=50000; x1=0; y1=0; psi=randUniform(-0.7854,0.7854); phi=0 } weight 1
	sttrans from cruise1 when true distr randUniform(60,300) to turn1 do { phi=-0.6109 } weight 1 to turn1 do { phi=0.6109 } weight 1
	sttrans from turn1 when true distr randUniform(10,60) to cruise2 do { phi=0 } weight 1
	sttrans from cruise2 when true distr randUniform(60,300) to turn2 do { phi=-0.6109 } weight 1 to turn2 do { phi=0.6109 } weight 1
	sttrans from turn2 when true distr randUniform(10,60) to cruise3 do { phi=0 } weight 1

	alge { v == 130 }
	alge { h == 20000 }
	alge { g == 9.83 }
	alge { S == 260 }
	alge { m == 90000 + mf}
	alge { nu == 0.0000147*(1+v/8696.74) }
	alge { ro == 1.225*java.lang.Math.pow((1-1.9812*h/288150), 4.35864) }
	alge { CL == 2*m*g/(ro*v*v*S*java.lang.Math.cos(phi)) }
	alge { CD == 0.019 + 0.053*CL*CL }
	alge { T == CD*S*ro*v*v/2 }
	alge { apsi == CL*S*ro*v*java.lang.Math.sin(phi)/(2*m) }

	SDE { d(x1) == v*java.lang.Math.cos(psi)*dt + 10*dB(t) }
	SDE { d(y1) == v*java.lang.Math.sin(psi)*dt + 10*dB(t) }
	diff { d(psi) == apsi }
	diff { d(mf) == -nu*T }
}

mode operation2() {
	output signal real x2;
	output signal real y2;
	private signal real h;
	private signal real v;
	private signal real mf;
	private signal real T;
	private signal real phi;
	private signal real psi;
	private signal real m;
	private signal real CD;
	private signal real CL;
	private signal real S;
	private signal real ro;
	private signal real nu;
	private signal real g;
	private signal real apsi;

	mode md0 = md();
	mode cruise1 = md();
	mode turn1 = md();
	mode cruise2 = md();
	mode turn2 = md();
	mode cruise3 = md();

	trans from default to md0 when true do {}
	sttrans from md0 when true distr 0 to cruise1 do { mf=50000; x2=50000; y2=0; psi=randUniform(2.3562,3.9270); phi=0 } weight 1
	sttrans from cruise1 when true distr randUniform(60,300) to turn1 do { phi=-0.6109 } weight 1 to turn1 do { phi=0.6109 } weight 1
	sttrans from turn1 when true distr randUniform(10,60) to cruise2 do { phi=0 } weight 1
	sttrans from cruise2 when true distr randUniform(60,300) to turn2 do { phi=-0.6109 } weight 1 to turn2 do { phi=0.6109 } weight 1
	sttrans from turn2 when true distr randUniform(10,60) to cruise3 do { phi=0 } weight 1


	alge { v == 130 }
	alge { h == 20000 }
	alge { g == 9.83 }
	alge { S == 260 }
	alge { m == 90000 + mf}
	alge { nu == 0.0000147*(1+v/8696.74) }
	alge { ro == 1.225*java.lang.Math.pow((1-1.9812*h/288150), 4.35864) }
	alge { CL == 2*m*g/(ro*v*v*S*java.lang.Math.cos(phi)) }
	alge { CD == 0.019 + 0.053*CL*CL }
	alge { T == CD*S*ro*v*v/2 }
	alge { apsi == CL*S*ro*v*java.lang.Math.sin(phi)/(2*m) }

	SDE { d(x2) == v*java.lang.Math.cos(psi)*dt + 10*dB(t) }
	SDE { d(y2) == v*java.lang.Math.sin(psi)*dt + 10*dB(t) }
	diff { d(psi) == apsi }
	diff { d(mf) == -nu*T }
}

mode md() {}