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

time_bound := 1;

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

// ----------------------------------------------------------
// System Description
// ----------------------------------------------------------
automaton bouncing_ball
contr_var: x, v, t;
synclabs: jump;
loc init: while x==2 & v==0 wait {x'==0 & v'==0 & t'==0}
	when x==2 & v==0 sync jump goto state;

loc state: while x>=0 & t<=time_bound wait {x'==v & v'==-g & t'==1}
	when x==0 & v<0 sync jump palt {
          50 : do {v'==-v*0.50 & x'==x & t'==t} goto change1,
          25 : do {v'==-v*0.25 & x'==x & t'==t} goto change2,
	  25 : goto error
        };

loc change1: while True wait {x'==0 & v'==0 & t'==0}
	when True sync jump goto state;

loc change2: while True wait {x'==0 & v'==0 & t'==0}
	when True sync jump goto state;

loc error: while True wait {x'==0 & v'==0 & t'==0}
initially: init & x==2 & v==0 & t==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
//bouncing_ball.set_refine_constraints((x, 0.14),(v,0.14),tau);
// bouncing_ball.set_refine_constraints((x,0.15),(v,0.15),tau);
bouncing_ball.set_refine_constraints((x, 0.05),(v,0.05),tau);
//bouncing_ball.set_refine_constraints((x, 0.07),(v,0.07),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.1),tau);
//REACH_USE_CONVEX_HULL=false;

// --------------------------------------------------------
// Definition of forbidden states
// --------------------------------------------------------

forbidden=bouncing_ball.{error & True};
bouncing_ball.reach_graph("bouncing.graph", forbidden);