verify ( fun state -> let open Sensor_msgs in match state.incoming with None | Some (Clock _ ) -> true | Some ( Sensor data ) -> ( List.for_all (fun x -> x < 20000) data.laserScan_ranges ) ==> (one_step state).mode = Turning )