Can you please show me where in the graph for checking if condition is reachable? The system for the graph. I'm assuming the graph is on the vertices (inputs (xi) and outputs (yi) at each reaction (I))

// Hybrid System Example: Bouncing Ball

g:=1; // constant acceleration from gravity

automaton bouncing_ball contr_var: x, v; //the position and velocity synclabs: jump; loc falling: while 0

// --------------------- Analysis begin------------------------------------- bouncing_ball.add_label(tau); pc:=0.2; //define partition constraint bouncing_ball.set_partition_constraints((x,pc),(v,pc),tau);

reg=bouncing_ball.reachable; // reached part of state space reg.print("out_bball",2); // output as a list of vertices

25 Fir 0.5 1.0 1.5 2.0 2. Check whether it is possible, using the default settings in the model, to prove that the velocity of the ball is always below positive 1.05. You can do this by showing that the system cannot reach any part of the state space in which the velocity equals or exceeds 1.05. In other words, you are proving property G(v