Skip to content

Instantly share code, notes, and snippets.

@KKostya

KKostya/stopping_if_for_all.ml

Created July 26, 2018 14:37
Show Gist options
  • Save KKostya/d29025a67828dbe11b5fc049f3efc4eb to your computer and use it in GitHub Desktop.
Save KKostya/d29025a67828dbe11b5fc049f3efc4eb to your computer and use it in GitHub Desktop.
Download ZIP
Raw
stopping_if_for_all.ml
theorem stopping_if_for_all state =
let open Sensor_msgs in
match state.incoming with None | Some (Clock _ ) -> true
| Some ( Sensor data ) ->
( data.laserScan_ranges <> []
&& List.for_all (fun x -> x < 20000) data.laserScan_ranges
) ==> (one_step state).mode = Turning
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment