// ----------------------------------------------------------
// Hybrid System Example: Bouncing Ball
// ----------------------------------------------------------

// ----------------------------------------------------------
// Constants 
// ----------------------------------------------------------
g:=1; // constant for gravity

// ----------------------------------------------------------
// System Description
// ----------------------------------------------------------
automaton bouncing_ball
contr_var: v, x;
synclabs: jump;
loc state: while x>=0 & x<=10 & v<=10 & v>=-10 wait {x'==v & v'==-g}
	when x==0 & v<0 sync jump do {v'==-v*0.5 & x'==x} goto state;
initially: state & x==2 & v==0;
end

// ----------------------------------------------------------
// Define Partitioning
// ----------------------------------------------------------
// Add a new label for the transitions that are introduced
// between partitions
bouncing_ball.add_label(tau);

// Define the directions of the partitions
// here: in both axes with a min. threshold of partition size 0.2
bouncing_ball.set_refine_constraints((x, 0.2),(v,0.2),tau);

// With this partitioning we can use convex hull overapproximations,
// resulting in fewer polyhedra (one per partition)
//REACH_USE_CONVEX_HULL=true;

// ----------------------------------------------------------
// Define Partitioning (alternative)
// ----------------------------------------------------------
// We can also just partition in the v-direction, but then we must turn off
// the convex hull (try it...)
// bouncing_ball.set_refine_constraints((v,0.2),tau);
// REACH_USE_CONVEX_HULL=false;

// ----------------------------------------------------------
// Analysis Commands
// ----------------------------------------------------------
reg=bouncing_ball.reachable;

// ----------------------------------------------------------
// Saving Data for Graphical Output
// ----------------------------------------------------------
reg.print("out_reach",2); // output as a list of vertices

// for display with graph use, e.g.: 
//    graph -T X -C -B -q0.5 out_reach
// for display with matlab use, e.g.: 
//    plot_2d_vertices('out_m_reach')