Mode switching synthesis for reachability specifications