$2$ Charging Station, Single Control

Oh no$!$ Your robot's battery is almost dead! Luckily the robot is already on a straight trajectory to a wall

charging station and has positive velocity. With its remaining power, your robot has just one chance to

engage the brakes properly to bring the robot to a stop at the right place.

If the robot brakes too hard, it will not make it to the charging station and will have to wait for a

human to plug it in$.$ Running out of power is inefficient.

If the robot doesn't brake hard enough to stop at the charging station, it will dent the wall behind the

station. When building manager Jim Skees finds out, he'll have your robot banned from the building!

Running into walls is unsafe.

Hints: think carefully about all the variables that the acceleration$/$braking should depend on$.$ If you find

you can't prove the property, it could be that you missed something and your property is falsifiable. Don't

forget you learned how to find counter$-$examples in lab$0!$

$1($BetaBot$).$ Specify the missing safety and efficiency requirements that the hybrid program below should

ensure. Then fill in the missing control and continuous dynamics. Save the resulting file as L$1$Q$2\_$name.kyx$.$

$2($VeriBot$).$ Use KeYmaeraX to prove that the hybrid program is safe and efficient and translate the proof

to a tactic. Save the resulting tactic as L$1$Q$2\_$name.kyt$.$