KKostya · July 26, 2018 14:34
diff --git a/stopping_for_all_wrong.ml b/stopping_for_all_wrong.ml
 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
 )
	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
	)