val stopping_if_exists : state -> bool = <fun>
Goal:
begin match (state.incoming : incoming_msg option) with
| None -> true
| Some (_pat_116 : incoming_msg) ->
begin match (_pat_116 : incoming_msg) with
| Clock (_pat_117 : Rosgraph_msgs.clock) -> true
| Sensor (data : Sensor_msgs.laserScan) ->
(data.Sensor_msgs.laserScan_ranges <> [])
&& List.exists under_threshold data.Sensor_msgs.laserScan_ranges
==> (one_step state).mode = Turning
end
end.
A hint has been given, resulting in the following augmented conjecture:
Goal':
(if Is_a(None, state.incoming) then true
else
if Is_a(Clock, Option.get state.incoming) then true
else
not
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
= [])
&& (List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
< 20000)
==> (if Is_a(None, state.incoming) then state
else
if Is_a(Clock, Option.get state.incoming)
then
if state.mode = Driving
then
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None;
outgoing =
Some
(Twist
{Geometry_msgs.twist_linear =
{Geometry_msgs.vector3_x = 10000; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0};
Geometry_msgs.twist_angular =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0}})}
else
if Is_a(None, state.direction)
then
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None;
outgoing =
Some
(Twist
{Geometry_msgs.twist_linear =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0};
Geometry_msgs.twist_angular =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 10000}})}
else
if Option.get state.direction = CW
then
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None;
outgoing =
Some
(Twist
{Geometry_msgs.twist_linear =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0};
Geometry_msgs.twist_angular =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 10000}})}
else
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None;
outgoing =
Some
(Twist
{Geometry_msgs.twist_linear =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0};
Geometry_msgs.twist_angular =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = (-10000)}})}
else
if Is_a(Driving, state.mode)
then
if (if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).0
< 20000
then
{mode = Turning;
min_range =
Some
(if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).0;
direction =
Some
(if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).1;
incoming = None; outgoing = None}
else
{mode = Driving; min_range = None; direction = None;
incoming = None; outgoing = None}
else
if Is_a(None, state.min_range)
then
if (if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).0
> 25000
then
{mode = Driving; min_range = None; direction = None;
incoming = None; outgoing = None}
else
{mode = Turning;
min_range =
Some
(if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).0;
direction =
Some
(if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).1;
incoming = None; outgoing = None}
else
if (if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).0
> 25000
then
{mode = Driving; min_range = None; direction = None;
incoming = None; outgoing = None}
else
if (if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).0
> Option.get state.min_range
then
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None; outgoing = None}
else
{mode = Turning;
min_range =
Some
(if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).0;
direction =
Some
(if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).1;
incoming = None; outgoing = None}).mode
= Turning)
&& (List.exists under_threshold
(if Is_a(Some, state.incoming)
then
if Is_a(Sensor, Option.get state.incoming)
then
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
else []
else [])
==> List.fold_right anon_fun.get_min_range.1
(if Is_a(Some, state.incoming)
then
if Is_a(Sensor, Option.get state.incoming)
then
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
else 0
else 0)
(if Is_a(Some, state.incoming)
then
if Is_a(Sensor, Option.get state.incoming)
then
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
else []
else [])
< 20000)
==> (if Is_a(None, state.incoming) then true
else
if Is_a(Clock, Option.get state.incoming) then true
else
not
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
= [])
&& List.exists under_threshold
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
==> (if Is_a(None, state.incoming) then state
else
if Is_a(Clock, Option.get state.incoming)
then
if state.mode = Driving
then
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None;
outgoing =
Some
(Twist
{Geometry_msgs.twist_linear =
{Geometry_msgs.vector3_x = 10000;
Geometry_msgs.vector3_y = 0; Geometry_msgs.vector3_z = 0};
Geometry_msgs.twist_angular =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0}})}
else
if Is_a(None, state.direction)
then
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None;
outgoing =
Some
(Twist
{Geometry_msgs.twist_linear =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0};
Geometry_msgs.twist_angular =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 10000}})}
else
if Option.get state.direction = CW
then
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None;
outgoing =
Some
(Twist
{Geometry_msgs.twist_linear =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0};
Geometry_msgs.twist_angular =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 10000}})}
else
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None;
outgoing =
Some
(Twist
{Geometry_msgs.twist_linear =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0};
Geometry_msgs.twist_angular =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = (-10000)}})}
else
if Is_a(Driving, state.mode)
then
if (if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).0
< 20000
then
{mode = Turning;
min_range =
Some
(if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).0;
direction =
Some
(if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).1;
incoming = None; outgoing = None}
else
{mode = Driving; min_range = None; direction = None;
incoming = None; outgoing = None}
else
if Is_a(None, state.min_range)
then
if (if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).0
> 25000
then
{mode = Driving; min_range = None; direction = None;
incoming = None; outgoing = None}
else
{mode = Turning;
min_range =
Some
(if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).0;
direction =
Some
(if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).1;
incoming = None; outgoing = None}
else
if (if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).0
> 25000
then
{mode = Driving; min_range = None; direction = None;
incoming = None; outgoing = None}
else
if (if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).0
> Option.get state.min_range
then
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None; outgoing = None}
else
{mode = Turning;
min_range =
Some
(if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).0;
direction =
Some
(if (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
< List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)).1;
incoming = None; outgoing = None}).mode
= Turning).
1 nontautological subgoal.
Subgoal 1:
H0. Is_a(None, state.incoming) || Is_a(Clock, Option.get state.incoming)
|| not
(not
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
= [])
&& not
(20000
<= List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges))
|| ((if Is_a(None, state.incoming) then state
else
if Is_a(Clock, Option.get state.incoming)
then
if state.mode = Driving
then
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None;
outgoing =
Some
(Twist
{Geometry_msgs.twist_linear =
{Geometry_msgs.vector3_x = 10000;
Geometry_msgs.vector3_y = 0; Geometry_msgs.vector3_z = 0};
Geometry_msgs.twist_angular =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0}})}
else
if Is_a(None, state.direction)
|| (Option.get state.direction = CW)
then
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None;
outgoing =
Some
(Twist
{Geometry_msgs.twist_linear =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0};
Geometry_msgs.twist_angular =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 10000}})}
else
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None;
outgoing =
Some
(Twist
{Geometry_msgs.twist_linear =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0};
Geometry_msgs.twist_angular =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = (-10000)}})}
else
if Is_a(Driving, state.mode)
then
if 20000
<= (if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).0
then
{mode = Driving; min_range = None; direction = None;
incoming = None; outgoing = None}
else
{mode = Turning;
min_range =
Some
(if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).0;
direction =
Some
(if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).1;
incoming = None; outgoing = None}
else
if Is_a(None, state.min_range)
then
if (if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).0
<= 25000
then
{mode = Turning;
min_range =
Some
(if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).0;
direction =
Some
(if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).1;
incoming = None; outgoing = None}
else
{mode = Driving; min_range = None; direction = None;
incoming = None; outgoing = None}
else
if (if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).0
<= 25000
then
if (if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).0
<= Option.get state.min_range
then
{mode = Turning;
min_range =
Some
(if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).0;
direction =
Some
(if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).1;
incoming = None; outgoing = None}
else
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None; outgoing = None}
else
{mode = Driving; min_range = None; direction = None;
incoming = None; outgoing = None}).mode
= Turning)
H1. not
(List.exists under_threshold
(if Is_a(Some, state.incoming)
then
if Is_a(Sensor, Option.get state.incoming)
then
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
else []
else []))
|| not
(20000
<= List.fold_right anon_fun.get_min_range.1
(if Is_a(Some, state.incoming)
then
if Is_a(Sensor, Option.get state.incoming)
then
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
else 0
else 0)
(if Is_a(Some, state.incoming)
then
if Is_a(Sensor, Option.get state.incoming)
then
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
else []
else []))
H2. not
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
= [])
H3. List.exists under_threshold
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
|---------------------------------------------------------------------------
C0. Is_a(None, state.incoming)
C1. Is_a(Clock, Option.get state.incoming)
C2. (if Is_a(None, state.incoming) then state
else
if Is_a(Clock, Option.get state.incoming)
then
if state.mode = Driving
then
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None;
outgoing =
Some
(Twist
{Geometry_msgs.twist_linear =
{Geometry_msgs.vector3_x = 10000; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0};
Geometry_msgs.twist_angular =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0}})}
else
if Is_a(None, state.direction) || (Option.get state.direction = CW)
then
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None;
outgoing =
Some
(Twist
{Geometry_msgs.twist_linear =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0};
Geometry_msgs.twist_angular =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 10000}})}
else
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None;
outgoing =
Some
(Twist
{Geometry_msgs.twist_linear =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = 0};
Geometry_msgs.twist_angular =
{Geometry_msgs.vector3_x = 0; Geometry_msgs.vector3_y = 0;
Geometry_msgs.vector3_z = (-10000)}})}
else
if Is_a(Driving, state.mode)
then
if 20000
<= (if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).0
then
{mode = Driving; min_range = None; direction = None;
incoming = None; outgoing = None}
else
{mode = Turning;
min_range =
Some
(if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).0;
direction =
Some
(if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).1;
incoming = None; outgoing = None}
else
if Is_a(None, state.min_range)
then
if (if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).0
<= 25000
then
{mode = Turning;
min_range =
Some
(if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).0;
direction =
Some
(if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).1;
incoming = None; outgoing = None}
else
{mode = Driving; min_range = None; direction = None;
incoming = None; outgoing = None}
else
if (if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).0
<= 25000
then
if (if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).0
<= Option.get state.min_range
then
{mode = Turning;
min_range =
Some
(if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).0;
direction =
Some
(if List.length
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges
/ 2
<= (foldi
((Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max,
0)
None anon_fun.get_min_and_direction.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges).1
then
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CCW)
else
(List.fold_right anon_fun.get_min_range.1
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_range_max
(Destruct(Sensor, 0, Option.get state.incoming)).Sensor_msgs.laserScan_ranges,
CW)).1;
incoming = None; outgoing = None}
else
{mode = state.mode; min_range = state.min_range;
direction = state.direction; incoming = None; outgoing = None}
else
{mode = Driving; min_range = None; direction = None; incoming = None;
outgoing = None}).mode
= Turning
But simplification reduces this to true, using the forward-chaining rule
List.len_nonnegative.
ⓘ Rules:
(:fc List.len_nonnegative)
(:app apply_hint.stopping_if_exists.0)
(:app apply_hint.stopping_if_exists.1)