hybrid reachability
{
	state var x1, y1, alpha1, x2, y2, alpha2, z
	setting
	{
		fixed steps 0.02
		time 15
		remainder estimation 1e-6
		identity precondition
		gnuplot octagon x1,y1
		adaptive orders { min 2 , max 5 }
		cutoff 1e-12
		precision 53
		output aircraft
		max jumps 2 # bound of the jump depth
		print on
 	}

 	modes
	{
		mode1
		{
			nonpoly ode
			{
				x1’ = cos(alpha1) y1’ = sin(alpha1) alpha1’ = 0
				x2’ = cos(alpha2) y2’ = sin(alpha2) alpha2’ = 0
				z’ = 0
			}
			inv { (x1 - x2)^2 + (y1 - y2)^2 >= 4 }
		}

		mode2
		{
			nonpoly ode
			{
				x1’ = cos(alpha1) y1’ = sin(alpha1) alpha1’ = 1
				x2’ = cos(alpha2) y2’ = sin(alpha2) alpha2’ = 1
				z’ = 1
			}
			inv { z <= 3.1415 }
		}

		mode3
		{
			nonpoly ode
			{
			x1’ = cos(alpha1) y1’ = sin(alpha1) alpha1’ = 0
			x2’ = cos(alpha2) y2’ = sin(alpha2) alpha2’ = 0
			z’ = 0
		}
			inv { }
		}
	}

 	jumps
 	{
		mode1 - > mode2
		guard { (x1 - x2)^2 + (y1 - y2)^2 = 4 }
		reset { alpha1’ := alpha1 - 1.57075 alpha2’ := alpha2 - 1.57075 }
		parallelotope aggregation { [x1:1,y1:1] [x2:1,y2:1] }

 		mode2 - > mode3
		guard { z = 3.1415 }
		reset { alpha1’ := alpha1 - 1.57075 alpha2’ := alpha2 - 1.57075 }
		parallelotope aggregation { }
 	}

 	init
 	{
 		mode1
		{
			x1 in [-0.1,0.1] y1 in [-0.1,0.1] alpha1 in [0.785374,0.785376]
			x2 in [9.9,10.1] y2 in [-0.1,0.1] alpha2 in [2.35612,2.35613]
			z in [0,0]
		}
	}
 }

 unsafe set
 {
 mode1 { x1 - x2 <= 0.2 x1 - x2 >= -0.2 y1 - y2 <= 0.2 y1 - y2 >= -0.2 }
 mode2 { x1 - x2 <= 0.2 x1 - x2 >= -0.2 y1 - y2 <= 0.2 y1 - y2 >= -0.2 }
 mode3 { x1 - x2 <= 0.2 x1 - x2 >= -0.2 y1 - y2 <= 0.2 y1 - y2 >= -0.2 }
 }