$1$ Autobots, Roll Out

As the n$00$b in your robotics group, the senior members gave you the broken robot. Its steering is jammed,

so it can only move in a straight line and control acceleration.

$1($BetaBot$).$ Fill in the missing continuous dynamics in the hybrid program below that will model your

robot accelerating in a straight line, with position pos, velocity vel, and acceleration acc.

$2($BetaBot$).$ Fill in the safety condition that will ensure the velocity of the robot is never negative. Save

this file as L$1$Q$1\_$name.kyx $($where name is replaced with your Andrew ID$).$

$3($VeriBot$).$ Use KeYmaeraX to prove the velocity of the robot is always positive. Translate the resulting

proof into a tactic and save the tactic in L$1$Q$1\_$name.kyt$.$ All of the tasks in this lab should prove automat$-$

ically $-$ but keep in mind that proving manually will significantly help be necessary in the later labs and it

helps if you start early!