# Verifying a simple autonomous vehicle controller in Imandra¶ In this notebook, we'll design and verify a simple autonomous vehicle controller in Imandra. The controller we analyse is due to Boyer, Green and Moore, and is described and analysed in their article The Use of a Formal Simulator to Verify a Simple Real Time Control Program.

This controller will receive sequences of sensor readings measuring changes in wind speed, and will have to respond to keep the vehicle on course. The final theorems we prove will establish the following safety and correctness properties:

• If the vehicle starts at the initial state (0,0,0), then the controller guarantees the vehicle never strays farther than 3 units from the x-axis.
• If the wind ever becomes constant for at least 4 sampling intervals, then the vehicle returns to the x-axis and stays there as long as the wind remains constant.

These results formally prove that the simulated vehicle appropriately stays on course under each of the infinite number of possible wind histories.

## The controller and its environment¶

Quantities in the model are measured using integral units. The model is one-dimensional: it considers the y-components of both the vehicle and wind velocity.

Wind speed is measured in terms of the number of units in the y-direction the wind would blow a passive vehicle in one sampling interval. From one sampling interval to the next, the wind speed can change by at most one unit in either direction. The wind is permitted to blow up to arbitrarily high velocities.

At each sampling interval, the controller may increment or decrement the y-component of its velocity. We let v be the accumulated speed in the y-direction measured as the number of units the vehicle would move in one sampling interval if there were no wind. We make no assumption limiting how fast v may be changed by the control program. We permit v to become arbitrary large.

# The Imandra model¶

The Imandra model of our system and its environment is rooted in a state vector consisting of three values:

• w - current wind velocity
• y - current y-position of the vehicle
• v - accumulated velocity of the vehicle
In :
type state = {
w : int; (* current wind speed *)
y : int; (* y-position of the vehicle *)
v : int; (* accumulated velocity *)
}

Out:
type state = { w : int; y : int; v : int; }


# Our controller and state transitions¶

In :
let controller sgn_y sgn_old_y =
(-3 * sgn_y) + (2 * sgn_old_y)

Out:
val controller : Z.t -> Z.t -> Z.t = <fun>

In :
let sgn x =
if x < 0 then -1
else if x = 0 then 0
else 1

Out:
val sgn : int -> Z.t = <fun>


Given a wind-speed delta sensor reading and a current state, next_state computes the next state of the system as dictated by our controller.

In :
let next_state dw s =
{ w = s.w + dw;
y = s.y + s.v + s.w + dw;
v = s.v +
controller
(sgn (s.y + s.v + s.w + dw))
(sgn s.y)
}

Out:
val next_state : Z.t -> state -> state = <fun>


# Sensing the environment¶

The behaviour of the wind over n sampling intervals is represented as a sequence of length n. Each element of the sequence is either -1, 0, or 1 indicating how the wind changed between sampling intervals.

We define the predicate arbitrary_delta_ws to describe valid sequences of wind sensor readings.

In :
let arbitrary_delta_ws = List.for_all (fun x -> x = -1 || x = 0 || x = 1)

Out:
val arbitrary_delta_ws : Z.t list -> bool = <fun>


# The top-level state machine¶

We now define the final_state function which takes a description of an arbitrary wind sampling history and an initial state, and computes the result of running the controller (i.e., simulating the vehicle) as it responds to the changes in wind.

In :
let rec final_state s dws =
match dws with
| [] -> s
| dw :: dws' ->
let s' = next_state dw s in
final_state s' dws'

Out:
val final_state : state -> Z.t list -> state = <fun>

termination proof

### Termination proof

call final_state (next_state (List.hd dws) s) (List.tl dws) from final_state s dws
originalfinal_state s dws
subfinal_state (next_state (List.hd dws) s) (List.tl dws)
original ordinalOrdinal.Int (Ordinal.count dws)
sub ordinalOrdinal.Int (Ordinal.count (List.tl dws))
path[not (dws = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.027s
details
Expand
smt_stats
 num checks 8 arith assert lower 16 arith pivots 9 rlimit count 2429 mk clause 19 datatype occurs check 21 mk bool var 78 arith assert upper 14 datatype splits 3 decisions 14 arith add rows 18 propagations 14 conflicts 9 arith fixed eqs 7 datatype accessor ax 5 arith conflicts 2 datatype constructor ax 8 num allocs 1.16703e+06 final checks 6 added eqs 50 del clause 8 arith eq adapter 11 memory 6.67 max memory 6.67
Expand
• start[0.027s]
not (dws = [])
&& Ordinal.count dws >= 0 && Ordinal.count (List.tl dws) >= 0
==> List.tl dws = []
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl dws)))
(Ordinal.Int (Ordinal.count dws))
• ##### simplify
 into (not ((not (dws = []) && Ordinal.count dws >= 0) && Ordinal.count (List.tl dws) >= 0) || List.tl dws = []) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl dws))) (Ordinal.Int (Ordinal.count dws)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_int list_1239| (… expansions
• unroll
 expr (|count_int list_1239| (|get.::.1_1227| dws_1229)) expansions
• unroll
 expr (|count_int list_1239| dws_1229) expansions
• ##### unsat
(let ((a!1 (>= (ite (>= (|get.::.0_1226| dws_1229) 0)
(|get.::.0_1226| dws_1229)…

# Verifying our controller¶

We now partition our state-space into a collection of regions, some "good," most "bad," and show that if we start in a "good" state (like (0,0,0)), then we'll (inductively) always end up in a "good" state.

In :
(* What it means to be a good'' state *)

let good_state s =
match s.y, s.w + s.v with
| -3, 1 -> true
| -2, 1 -> true
| -2, 2 -> true
| -1, 2 -> true
| -1, 3 -> true
| 0, -1 -> true
| 0, 0  -> true
| 0, 1  -> true
| 1, -2 -> true
| 1, -3 -> true
| 2, -1 -> true
| 2, -2 -> true
| 3, -1 -> true
| _ -> false

Out:
val good_state : state -> bool = <fun>


## Theorem: Single step safety¶

We prove: If we start in a good state and evolve the system responding to one sensor reading, we end up in a good state.

In :
theorem safety_1 s dw =
good_state s
&& (dw = -1 || dw = 0 || dw = 1)
==>
good_state (next_state dw s)
[@@rewrite]

Out:
val safety_1 : state -> Z.t -> bool = <fun>

Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.041s
details
Expand
smt_stats
 arith offset eqs 8 num checks 1 arith assert lower 759 arith pivots 37 rlimit count 13795 mk clause 948 mk bool var 352 arith assert upper 812 decisions 222 arith add rows 20 arith bound prop 316 propagations 3464 conflicts 104 arith fixed eqs 35 datatype accessor ax 1 minimized lits 133 arith conflicts 17 arith assert diseq 675 datatype constructor ax 1 num allocs 8.43633e+06 added eqs 815 del clause 452 arith eq adapter 322 memory 7.72 max memory 8.54
Expand
• start[0.041s]
(if 1 = :var_0:.w + :var_0:.v && -3 = :var_0:.y then true
else
if 1 = :var_0:.w + :var_0:.v && -2 = :var_0:.y then true
else
if 2 = :var_0:.w + :var_0:.v && -2 = :var_0:.y then true
else if 2 = :var_0:.w + :var_0:.v && -1 = :var_0:.y then true else …)
&& (:var_1: = -1 || :var_1: = 0 || :var_1: = 1)
==> (if 1 =
(:var_0:.w + :var_1:)
+ :var_0:.v
+ -3
* (if (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) < 0
then -1
else
if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0
then 0 else 1)
+ 2
* (if :var_0:.y < 0 then -1
else if :var_0:.y = 0 then 0 else 1)
&& -3 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:
then true
else
if 1 =
(:var_0:.w + :var_1:)
+ :var_0:.v
+ -3
* (if (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) < 0
then -1
else
if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0
then 0 else 1)
+ 2
* (if :var_0:.y < 0 then -1
else if :var_0:.y = 0 then 0 else 1)
&& -2 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:
then true
else
if 2 =
(:var_0:.w + :var_1:)
+ :var_0:.v
+ -3
* (if (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) < 0
then -1
else
if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0
then 0 else 1)
+ 2
* (if :var_0:.y < 0 then -1
else if :var_0:.y = 0 then 0 else 1)
&& -2 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:
then true
else
if 2 =
(:var_0:.w + :var_1:)
+ :var_0:.v
+ -3
* (if (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) < 0
then -1
else
if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0
then 0 else 1)
+ 2
* (if :var_0:.y < 0 then -1
else if :var_0:.y = 0 then 0 else 1)
&& -1 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:
then true else …)
• #### simplify

 into ((((((((((((not (((((((((((((1 = :var_0:.w + :var_0:.v && -3 = :var_0:.y || 1 = :var_0:.w + :var_0:.v && -2 = :var_0:.y) || 2 = :var_0:.w + :var_0:.v && -2 = :var_0:.y) || 2 = :var_0:.w + :var_0:.v && -1 = :var_0:.y) || 3 = :var_0:.w + :var_0:.v && -1 = :var_0:.y) || -1 = :var_0:.w + :var_0:.v && 0 = :var_0:.y) || 0 = :var_0:.w + :var_0:.v && 0 = :var_0:.y) || 1 = :var_0:.w + :var_0:.v && 0 = :var_0:.y) || -2 = :var_0:.w + :var_0:.v && 1 = :var_0:.y) || -3 = :var_0:.w + :var_0:.v && 1 = :var_0:.y) || -1 = :var_0:.w + :var_0:.v && 2 = :var_0:.y) || -2 = :var_0:.w + :var_0:.v && 2 = :var_0:.y) || -1 = :var_0:.w + :var_0:.v && 3 = :var_0:.y) && ((:var_1: = -1 || :var_1: = 0) || :var_1: = 1)) || 1 = (((:var_0:.w + :var_1:) + :var_0:.v) + -3 * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) then if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0 else 1 else -1)) + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1) && -3 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) || 1 = (((:var_0:.w + :var_1:) + :var_0:.v) + -3 * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) then if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0 else 1 else -1)) + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1) && -2 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) || 2 = (((:var_0:.w + :var_1:) + :var_0:.v) + -3 * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) then if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0 else 1 else -1)) + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1) && -2 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) || 2 = (((:var_0:.w + :var_1:) + :var_0:.v) + -3 * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) then if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0 else 1 else -1)) + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1) && -1 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) || 3 = (((:var_0:.w + :var_1:) + :var_0:.v) + -3 * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) then if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0 else 1 else -1)) + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1) && -1 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) || -1 = (((:var_0:.w + :var_1:) + :var_0:.v) + -3 * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) then if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0 else 1 else -1)) + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1) && 0 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) || 0 = (((:var_0:.w + :var_1:) + :var_0:.v) + -3 * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) then if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0 else 1 else -1)) + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1) && 0 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) || 1 = (((:var_0:.w + :var_1:) + :var_0:.v) + -3 * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) then if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0 else 1 else -1)) + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1) && 0 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) || -2 = (((:var_0:.w + :var_1:) + :var_0:.v) + -3 * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) then if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0 else 1 else -1)) + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1) && 1 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) || -3 = (((:var_0:.w + :var_1:) + :var_0:.v) + -3 * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) then if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0 else 1 else -1)) + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1) && 1 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) || -1 = (((:var_0:.w + :var_1:) + :var_0:.v) + -3 * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) then if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0 else 1 else -1)) + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1) && 2 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) || -2 = (((:var_0:.w + :var_1:) + :var_0:.v) + -3 * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) then if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0 else 1 else -1)) + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1) && 2 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) || -1 = (((:var_0:.w + :var_1:) + :var_0:.v) + -3 * (if 0 <= (((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1:) then if ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: = 0 then 0 else 1 else -1)) + 2 * (if 0 <= :var_0:.y then if :var_0:.y = 0 then 0 else 1 else -1) && 3 = ((:var_0:.y + :var_0:.v) + :var_0:.w) + :var_1: expansions [] rewrite_steps forward_chaining
• #### unsat

(let ((a!1 (<= 0 (+ (y_16 s_1256) (v_17 s_1256) (w_15 s_1256) dw_1257)))
(a!2 (= (+ (y_16 s_12…

#### Warning

Pattern will match only if good_state is disabled
(non-recursive function)
See https://docs.imandra.ai/imandra-docs/notebooks/verification-simplification

#### Warning

Pattern will match only if next_state is disabled
(non-recursive function)
See https://docs.imandra.ai/imandra-docs/notebooks/verification-simplification

## Theorem: Multistep safety¶

We prove: If we start in a good state and simulate the controller w.r.t. an arbitrary sequence of sensor readings, then we still end up in a good state.

In :
#disable next_state;;
#disable good_state;;

theorem all_good s dws =
good_state s && arbitrary_delta_ws dws
==>
good_state ((final_state s dws) [@trigger])
[@@induct functional final_state]
[@@forward_chaining]

Out:
val all_good : state -> Z.t list -> bool = <fun>
Goal:

good_state s && arbitrary_delta_ws dws ==> good_state (final_state s dws).

1 nontautological subgoal.

We shall induct according to a scheme derived from final_state.

Induction scheme:

(dws = [] ==> φ s dws)
&& (not (dws = []) && φ (next_state (List.hd dws) s) (List.tl dws)
==> φ s dws).

2 nontautological subgoals.

Subgoal 2:

H0. dws = []
H1. good_state s
H2. List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws
|---------------------------------------------------------------------------
good_state (final_state s dws)

But simplification reduces this to true, using the definition of final_state.

Subgoal 1:

H0. not (dws = [])
H1. good_state (next_state (List.hd dws) s)
&& List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
==> good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
H2. good_state s
H3. List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws
|---------------------------------------------------------------------------
good_state (final_state s dws)

But simplification reduces this to true, using the definitions of
List.for_all and final_state, and the rewrite rule safety_1.

ⓘ  Rules:
(:def List.for_all)
(:def final_state)
(:rw safety_1)
(:induct final_state)


Proved
proof
 ground_instances 0 definitions 3 inductions 1 search_time 0.158s
Expand
• start[0.158s, "Goal"]
good_state :var_0:
&& List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_1:
==> good_state (final_state :var_0: :var_1:)
• #### subproof

(not (good_state s) || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws)) || good_state (final_state s dws)
• start[0.158s, "1"]
(not (good_state s)
|| not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
|| good_state (final_state s dws)
• induction on (functional final_state)
:scheme (dws = [] ==> φ s dws)
&& (not (dws = []) && φ (next_state (List.hd dws) s) (List.tl dws)
==> φ s dws)
• Split (((not (dws = [])
|| not
(good_state s
&& List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
|| good_state (final_state s dws))
&& ((not
(not (dws = [])
&& (not
(good_state (next_state (List.hd dws) s)
&& List.for_all (fun x -> x = -1 || x = 0 || x = 1)
(List.tl dws))
|| good_state
(final_state (next_state (List.hd dws) s) (List.tl dws))))
|| not
(good_state s
&& List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
|| good_state (final_state s dws))
:cases [((not (dws = []) || not (good_state s))
|| not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
|| good_state (final_state s dws);
(((dws = []
|| not
(not
(good_state (next_state (List.hd dws) s)
&& List.for_all (fun x -> x = -1 || x = 0 || x = 1)
(List.tl dws))
|| good_state
(final_state (next_state (List.hd dws) s)
(List.tl dws))))
|| not (good_state s))
|| not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
|| good_state (final_state s dws)])
• ##### subproof
(((dws = [] || not (not (good_state (next_state (List.hd dws) s) && List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)) || good_state (final_state (next_state (List.hd dws) s) (List.tl dws)))) || not (good_state s)) || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws)) || good_state (final_state s dws)
• start[0.158s, "1"]
(((dws = []
|| not
(not
(good_state (next_state (List.hd dws) s)
&& List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws))
|| good_state
(final_state (next_state (List.hd dws) s) (List.tl dws))))
|| not (good_state s))
|| not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
|| good_state (final_state s dws)
• ###### simplify
 into true expansions [List.for_all, final_state] rewrite_steps safety_1safety_1safety_1 forward_chaining
• ##### subproof
((not (dws = []) || not (good_state s)) || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws)) || good_state (final_state s dws)
• start[0.158s, "2"]
((not (dws = []) || not (good_state s))
|| not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
|| good_state (final_state s dws)
• ###### simplify
 into true expansions final_state rewrite_steps forward_chaining

# Theorem: Cannot get more than 3 units off course.¶

We prove: No matter how the wind behaves, if the vehicle starts at the initial state (0,0,0), then the controller guarantees the vehicle never strays farther than 3 units from the x-axis.

In :
#enable next_state;;
#enable good_state;;

theorem vehicle_stays_within_3_units_of_course dws =
arbitrary_delta_ws dws
==>
let s' = final_state {y=0;w=0;v=0} dws in
-3 <= s'.y && s'.y <= 3
[@@simp]

Out:
val vehicle_stays_within_3_units_of_course : Z.t list -> bool = <fun>

Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.040s
details
Expand
smt_stats
 rlimit count 7379 mk bool var 5 num allocs 1.20983e+09 memory 21.19 max memory 32.56
Expand
• start[0.040s]
List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_0:
==> -3 <= (final_state {w = 0; y = 0; v = 0} :var_0:).y
&& (final_state {w = 0; y = 0; v = 0} :var_0:).y <= 3
• #### simplify

 into not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_0:) || -3 <= (final_state {w = 0; y = 0; v = 0} :var_0:).y && (final_state {w = 0; y = 0; v = 0} :var_0:).y <= 3 expansions [] rewrite_steps forward_chaining
• #### simplify

 into true expansions [] rewrite_steps forward_chaining all_good
• #### unsat

(mp (asserted (not true)) (rewrite (= (not true) false)) false)

# Theorem: If wind is stable for 4 intervals, we get back on course.¶

We prove: If the wind ever becomes constant for at least 4 sampling intervals, then the vehicle returns to the x-axis and stays there as long as the wind remains constant.

In :
let steady_wind = List.for_all (fun x -> x = 0)

let at_least_4 xs = match xs with
_ :: _ :: _ :: _ :: _ -> true
| _ -> false

Out:
val steady_wind : Z.t list -> bool = <fun>
val at_least_4 : 'a list -> bool = <fun>

In :
#disable next_state;;
#disable good_state;;
#max_induct 4;;

theorem good_state_find_and_stay_zt_zero s dws =
good_state s
&& at_least_4 dws
==>
let s' = (final_state s dws) [@trigger] in
s'.y = 0
[@@induct functional final_state]
[@@forward_chaining]
;;

Out:
val good_state_find_and_stay_zt_zero : state -> Z.t list -> bool = <fun>
Goal:

good_state s && steady_wind dws && at_least_4 dws
==> let (s' : state) = final_state s dws in s'.y = 0.

1 nontautological subgoal.

We shall induct according to a scheme derived from final_state.

Induction scheme:

(dws = [] ==> φ dws s)
&& (not (dws = []) && φ (List.tl dws) (next_state (List.hd dws) s)
==> φ dws s).

2 nontautological subgoals.

Subgoal 2:

H0. dws = []
H1. good_state s
H2. List.for_all (fun x -> x = 0) dws
H3. dws <> []
H4. (List.tl dws) <> []
H5. (List.tl (List.tl dws)) <> []
H6. (List.tl (List.tl (List.tl dws))) <> []
|---------------------------------------------------------------------------
(final_state s dws).y = 0

But simplification reduces this to true.

Subgoal 1:

H0. not (dws = [])
H1. ((((good_state (next_state (List.hd dws) s)
&& List.for_all (fun x -> x = 0) (List.tl dws))
&& (List.tl dws) <> [])
&& (List.tl (List.tl dws)) <> [])
&& (List.tl (List.tl (List.tl dws))) <> [])
&& (List.tl (List.tl (List.tl (List.tl dws)))) <> []
==> (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
H2. good_state s
H3. List.for_all (fun x -> x = 0) dws
H4. dws <> []
H5. (List.tl dws) <> []
H6. (List.tl (List.tl dws)) <> []
H7. (List.tl (List.tl (List.tl dws))) <> []
|---------------------------------------------------------------------------
(final_state s dws).y = 0

This simplifies, using the definitions of List.for_all and final_state, and
the rewrite rule safety_1 to:

Subgoal 1':

H0. dws <> []
H1. good_state s
H2. List.for_all (fun x -> x = 0) (List.tl dws)
H3. List.hd dws = 0
H4. (List.tl dws) <> []
H5. (List.tl (List.tl dws)) <> []
H6. (List.tl (List.tl (List.tl dws))) <> []
|---------------------------------------------------------------------------
C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C1. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0

This simplifies, using the definition of List.for_all to:

Subgoal 1'':

H0. dws <> []
H1. good_state s
H2. List.for_all (fun x -> x = 0) (List.tl (List.tl dws))
H3. List.hd (List.tl dws) = 0
H4. List.hd dws = 0
H5. (List.tl dws) <> []
H6. (List.tl (List.tl dws)) <> []
H7. (List.tl (List.tl (List.tl dws))) <> []
|---------------------------------------------------------------------------
C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C1. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0

This simplifies, using the definition of List.for_all to:

Subgoal 1''':

H0. dws <> []
H1. good_state s
H2. List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws)))
H3. List.hd (List.tl (List.tl dws)) = 0
H4. List.hd (List.tl dws) = 0
H5. List.hd dws = 0
H6. (List.tl dws) <> []
H7. (List.tl (List.tl dws)) <> []
H8. (List.tl (List.tl (List.tl dws))) <> []
|---------------------------------------------------------------------------
C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C1. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0

This simplifies, using the definition of List.for_all to:

Subgoal 1'''':

H0. dws <> []
H1. good_state s
H2. List.for_all (fun x -> x = 0)
(List.tl (List.tl (List.tl (List.tl dws))))
H3. List.hd (List.tl (List.tl (List.tl dws))) = 0
H4. List.hd (List.tl (List.tl dws)) = 0
H5. List.hd (List.tl dws) = 0
H6. List.hd dws = 0
H7. (List.tl dws) <> []
H8. (List.tl (List.tl dws)) <> []
H9. (List.tl (List.tl (List.tl dws))) <> []
|---------------------------------------------------------------------------
C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C1. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0

This simplifies, using the definition of List.for_all to:

Subgoal 1''''':

H0. dws <> []
H1. good_state s
H2. List.hd (List.tl (List.tl (List.tl dws))) = 0
H3. List.hd (List.tl (List.tl dws)) = 0
H4. List.hd (List.tl dws) = 0
H5. List.hd dws = 0
H6. (List.tl dws) <> []
H7. (List.tl (List.tl dws)) <> []
H8. (List.tl (List.tl (List.tl dws))) <> []
|---------------------------------------------------------------------------
C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C1. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0

This further simplifies to:

Subgoal 1'''''':

H0. dws <> []
H1. good_state s
H2. List.hd (List.tl (List.tl (List.tl dws))) = 0
H3. List.hd (List.tl (List.tl dws)) = 0
H4. List.hd (List.tl dws) = 0
H5. List.hd dws = 0
H6. (List.tl dws) <> []
H7. (List.tl (List.tl dws)) <> []
H8. (List.tl (List.tl (List.tl dws))) <> []
|---------------------------------------------------------------------------
C0. (List.tl (List.tl (List.tl (List.tl dws)))) <> []
C1. (final_state (next_state 0 s) (List.tl dws)).y = 0

But we verify Subgoal 1'''''' by recursive unrolling.

ⓘ  Rules:
(:def List.for_all)
(:def final_state)
(:rw safety_1)
(:fc all_good)
(:induct final_state)


Proved
proof
ground_instances4
definitions6
inductions1
search_time
1.282s
details
Expand
smt_stats
 arith offset eqs 52 num checks 9 arith assert lower 671 arith pivots 82 rlimit count 123418 mk clause 713 datatype occurs check 16 mk bool var 726 arith assert upper 620 decisions 214 arith add rows 683 arith bound prop 119 propagations 2271 conflicts 100 arith fixed eqs 47 datatype accessor ax 12 minimized lits 206 arith conflicts 29 arith assert diseq 468 datatype constructor ax 7 final checks 4 added eqs 1057 del clause 351 arith eq adapter 347 memory 52.54 max memory 75.93 num allocs 1.37028e+10
Expand
• start[1.282s, "Goal"]
good_state :var_0:
&& List.for_all (fun x -> x = 0) :var_1:
&& :var_1: <> []
&& (List.tl :var_1:) <> []
&& (List.tl (List.tl :var_1:)) <> []
&& (List.tl (List.tl (List.tl :var_1:))) <> []
==> (final_state :var_0: :var_1:).y = 0
• #### subproof

(((((not (good_state s) || not (List.for_all (fun x -> x = 0) dws)) || not (dws <> [])) || not ((List.tl dws) <> [])) || not ((List.tl (List.tl dws)) <> [])) || not ((List.tl (List.tl (List.tl dws))) <> [])) || (final_state s dws).y = 0
• start[1.282s, "1"]
(((((not (good_state s) || not (List.for_all (fun x -> x = 0) dws))
|| not (dws <> []))
|| not ((List.tl dws) <> []))
|| not ((List.tl (List.tl dws)) <> []))
|| not ((List.tl (List.tl (List.tl dws))) <> []))
|| (final_state s dws).y = 0
• induction on (functional final_state)
:scheme (dws = [] ==> φ dws s)
&& (not (dws = []) && φ (List.tl dws) (next_state (List.hd dws) s)
==> φ dws s)
• Split (((not (dws = [])
|| not
(((((good_state s && List.for_all (fun x -> x = 0) dws)
&& dws <> [])
&& (List.tl dws) <> [])
&& (List.tl (List.tl dws)) <> [])
&& (List.tl (List.tl (List.tl dws))) <> []))
|| (final_state s dws).y = 0)
&& ((not
(not (dws = [])
&& (not
(((((good_state (next_state (List.hd dws) s)
&& List.for_all (fun x -> x = 0) (List.tl dws))
&& (List.tl dws) <> [])
&& (List.tl (List.tl dws)) <> [])
&& (List.tl (List.tl (List.tl dws))) <> [])
&& (List.tl (List.tl (List.tl (List.tl dws)))) <> [])
|| (final_state (next_state (List.hd dws) s) (List.tl dws)).y
= 0))
|| not
(((((good_state s && List.for_all (fun x -> x = 0) dws)
&& dws <> [])
&& (List.tl dws) <> [])
&& (List.tl (List.tl dws)) <> [])
&& (List.tl (List.tl (List.tl dws))) <> []))
|| (final_state s dws).y = 0)
:cases [((((((not (dws = []) || not (good_state s))
|| not (List.for_all (fun x -> x = 0) dws))
|| not (dws <> []))
|| not ((List.tl dws) <> []))
|| not ((List.tl (List.tl dws)) <> []))
|| not ((List.tl (List.tl (List.tl dws))) <> []))
|| (final_state s dws).y = 0;
(((((((dws = []
|| not
(not
(((((good_state (next_state (List.hd dws) s)
&& List.for_all (fun x -> x = 0) (List.tl dws))
&& (List.tl dws) <> [])
&& (List.tl (List.tl dws)) <> [])
&& (List.tl (List.tl (List.tl dws))) <> [])
&& (List.tl (List.tl (List.tl (List.tl dws)))) <> [])
|| (final_state (next_state (List.hd dws) s)
(List.tl dws)).y
= 0))
|| not (good_state s))
|| not (List.for_all (fun x -> x = 0) dws))
|| not (dws <> []))
|| not ((List.tl dws) <> []))
|| not ((List.tl (List.tl dws)) <> []))
|| not ((List.tl (List.tl (List.tl dws))) <> []))
|| (final_state s dws).y = 0])
• ##### subproof
(((((((dws = [] || not (not (((((good_state (next_state (List.hd dws) s) && List.for_all (fun x -> x = 0) (List.tl dws)) && (List.tl dws) <> []) && (List.tl (List.tl dws)) <> []) && (List.tl (List.tl (List.tl dws))) <> []) && (List.tl (List.tl (List.tl (List.tl dws)))) <> []) || (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0)) || not (good_state s)) || not (List.for_all (fun x -> x = 0) dws)) || not (dws <> [])) || not ((List.tl dws) <> [])) || not ((List.tl (List.tl dws)) <> [])) || not ((List.tl (List.tl (List.tl dws))) <> [])) || (final_state s dws).y = 0
• start[1.281s, "1"]
(((((((dws = []
|| not
(not
(((((good_state (next_state (List.hd dws) s)
&& List.for_all (fun x -> x = 0) (List.tl dws))
&& (List.tl dws) <> [])
&& (List.tl (List.tl dws)) <> [])
&& (List.tl (List.tl (List.tl dws))) <> [])
&& (List.tl (List.tl (List.tl (List.tl dws)))) <> [])
|| (final_state (next_state (List.hd dws) s) (List.tl dws)).y =
0))
|| not (good_state s))
|| not (List.for_all (fun x -> x = 0) dws))
|| not (dws <> []))
|| not ((List.tl dws) <> []))
|| not ((List.tl (List.tl dws)) <> []))
|| not ((List.tl (List.tl (List.tl dws))) <> []))
|| (final_state s dws).y = 0
• ###### simplify
 into (((((((dws = [] || (List.tl (List.tl (List.tl (List.tl dws)))) <> []) || not (good_state s)) || not (List.for_all (fun x -> x = 0) (List.tl dws))) || not (List.hd dws = 0)) || not ((List.tl dws) <> [])) || not ((List.tl (List.tl dws)) <> [])) || not ((List.tl (List.tl (List.tl dws))) <> [])) || (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0 expansions [List.for_all, final_state] rewrite_steps safety_1 forward_chaining all_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_good
• ###### simplify
 into ((((((((not (dws <> []) || not (good_state s)) || not (List.for_all (fun x -> x = 0) (List.tl (List.tl dws)))) || not (List.hd (List.tl dws) = 0)) || not (List.hd dws = 0)) || not ((List.tl dws) <> [])) || not ((List.tl (List.tl dws)) <> [])) || not ((List.tl (List.tl (List.tl dws))) <> [])) || (List.tl (List.tl (List.tl (List.tl dws)))) <> []) || (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0 expansions List.for_all rewrite_steps forward_chaining all_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_good
• ###### simplify
 into (((((((((not (dws <> []) || not (good_state s)) || not (List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws))))) || not (List.hd (List.tl (List.tl dws)) = 0)) || not (List.hd (List.tl dws) = 0)) || not (List.hd dws = 0)) || not ((List.tl dws) <> [])) || not ((List.tl (List.tl dws)) <> [])) || not ((List.tl (List.tl (List.tl dws))) <> [])) || (List.tl (List.tl (List.tl (List.tl dws)))) <> []) || (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0 expansions List.for_all rewrite_steps forward_chaining all_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_good
• ###### simplify
 into ((((((((((not (dws <> []) || not (good_state s)) || not (List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl (List.tl dws)))))) || not (List.hd (List.tl (List.tl (List.tl dws))) = 0)) || not (List.hd (List.tl (List.tl dws)) = 0)) || not (List.hd (List.tl dws) = 0)) || not (List.hd dws = 0)) || not ((List.tl dws) <> [])) || not ((List.tl (List.tl dws)) <> [])) || not ((List.tl (List.tl (List.tl dws))) <> [])) || (List.tl (List.tl (List.tl (List.tl dws)))) <> []) || (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0 expansions List.for_all rewrite_steps forward_chaining all_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_good
• ###### simplify
 into (((((((((not (dws <> []) || not (good_state s)) || not (List.hd (List.tl (List.tl (List.tl dws))) = 0)) || not (List.hd (List.tl (List.tl dws)) = 0)) || not (List.hd (List.tl dws) = 0)) || not (List.hd dws = 0)) || not ((List.tl dws) <> [])) || not ((List.tl (List.tl dws)) <> [])) || not ((List.tl (List.tl (List.tl dws))) <> [])) || (List.tl (List.tl (List.tl (List.tl dws)))) <> []) || (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0 expansions List.for_all rewrite_steps forward_chaining all_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_goodall_good
• ###### simplify
 into (((((((((not (dws <> []) || not (good_state s)) || not (List.hd (List.tl (List.tl (List.tl dws))) = 0)) || not (List.hd (List.tl (List.tl dws)) = 0)) || not (List.hd (List.tl dws) = 0)) || not (List.hd dws = 0)) || not ((List.tl dws) <> [])) || not ((List.tl (List.tl dws)) <> [])) || not ((List.tl (List.tl (List.tl dws))) <> [])) || (List.tl (List.tl (List.tl (List.tl dws)))) <> []) || (final_state (next_state 0 s) (List.tl dws)).y = 0 expansions [] rewrite_steps forward_chaining
• ###### subproof
(((((((((not (:var_2: <> []) || not (if 1 = :var_3:.w + :var_3:.v && -3 = :var_3:.y then true else if 1 = :var_3:.w + :var_3:.v && -2 = :var_3:.y then true else if 2 = :var_3:.w + :var_3:.v && -2 = :var_3:.y then true else if 2 = :var_3:.w + :var_3:.v && -1 = :var_3:.y then true else …)) || not (List.hd (List.tl (List.tl (List.tl :var_2:))) = 0)) || not (List.hd (List.tl (List.tl :var_2:)) = 0)) || not (List.hd (List.tl :var_2:) = 0)) || not (List.hd :var_2: = 0)) || not ((List.tl :var_2:) <> [])) || not ((List.tl (List.tl :var_2:)) <> [])) || not ((List.tl (List.tl (List.tl :var_2:))) <> [])) || (List.tl (List.tl (List.tl (List.tl :var_2:)))) <> []) || (final_state {w = :var_3:.w + 0; y = ((:var_3:.y + :var_3:.v) + :var_3:.w) + 0; v = :var_3:.v + -3 * (if (((:var_3:.y + :var_3:.v) + :var_3:.w) + 0) < 0 then -1 else …) + 2 * (if :var_3:.y < 0 then -1 else …)} (List.tl :var_2:)).y = 0
Start ((((((((((not (:var_2: <> [])
|| not
(if 1 = :var_3:.w + :var_3:.v && -3 = :var_3:.y then true
else
if 1 = :var_3:.w + :var_3:.v && -2 = :var_3:.y then true
else
if 2 = :var_3:.w + :var_3:.v && -2 = :var_3:.y then true
else
if 2 = :var_3:.w + :var_3:.v && -1 = :var_3:.y then true
else …))
|| not (List.hd (List.tl (List.tl (List.tl :var_2:))) = 0))
|| not (List.hd (List.tl (List.tl :var_2:)) = 0))
|| not (List.hd (List.tl :var_2:) = 0))
|| not (List.hd :var_2: = 0))
|| not ((List.tl :var_2:) <> []))
|| not ((List.tl (List.tl :var_2:)) <> []))
|| not ((List.tl (List.tl (List.tl :var_2:))) <> []))
|| (List.tl (List.tl (List.tl (List.tl :var_2:)))) <> [])
|| (final_state
{w = :var_3:.w + 0; y = ((:var_3:.y + :var_3:.v) + :var_3:.w) + 0;
v =
:var_3:.v
+ -3
* (if (((:var_3:.y + :var_3:.v) + :var_3:.w) + 0) < 0 then -1
else …)
+ 2 * (if :var_3:.y < 0 then -1 else …)}
(List.tl :var_2:)).y
= 0
:time 0.037s)
• ##### subproof
((((((not (dws = []) || not (good_state s)) || not (List.for_all (fun x -> x = 0) dws)) || not (dws <> [])) || not ((List.tl dws) <> [])) || not ((List.tl (List.tl dws)) <> [])) || not ((List.tl (List.tl (List.tl dws))) <> [])) || (final_state s dws).y = 0
• start[1.281s, "2"]
((((((not (dws = []) || not (good_state s))
|| not (List.for_all (fun x -> x = 0) dws))
|| not (dws <> []))
|| not ((List.tl dws) <> []))
|| not ((List.tl (List.tl dws)) <> []))
|| not ((List.tl (List.tl (List.tl dws))) <> []))
|| (final_state s dws).y = 0
• ###### simplify
 into true expansions [] rewrite_steps forward_chaining

You may enjoy reading the above proof! Now, we prove the final part of our main safety theorem.

In :
#enable good_state;;

theorem good_state_find_and_stay_0_from_origin dws =
&& at_least_4 dws
==>
let s' = final_state {y=0;w=0;v=0} dws in
s'.y = 0
[@@simp]

Out:
val good_state_find_and_stay_0_from_origin : Z.t list -> bool = <fun>

Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.044s
details
Expand
smt_stats
 rlimit count 11527 mk bool var 5 memory 46.65 max memory 75.93 num allocs 1.55412e+10
Expand
• start[0.044s]
List.for_all (fun x -> x = 0) :var_0:
&& :var_0: <> []
&& (List.tl :var_0:) <> []
&& (List.tl (List.tl :var_0:)) <> []
&& (List.tl (List.tl (List.tl :var_0:))) <> []
==> (final_state {w = 0; y = 0; v = 0} :var_0:).y = 0
• #### simplify

 into not ((((List.for_all (fun x -> x = 0) :var_0: && :var_0: <> []) && (List.tl :var_0:) <> []) && (List.tl (List.tl :var_0:)) <> []) && (List.tl (List.tl (List.tl :var_0:))) <> []) || (final_state {w = 0; y = 0; v = 0} :var_0:).y = 0 expansions [] rewrite_steps forward_chaining
• #### simplify

 into true expansions [] rewrite_steps forward_chaining all_goodgood_state_find_and_stay_zt_zero
• #### unsat

(mp (asserted (not true)) (rewrite (= (not true) false)) false)

# Experiments with a flawed version¶

Now that we've verified the controller, let us imagine instead that we'd made a mistake in its design and use Imandra to find such a mistake. For example, what if we'd defined the controller as follows?

In :
let bad_controller sgn_y sgn_old_y =
(-4 * sgn_y) + (2 * sgn_old_y)

Out:
val bad_controller : Z.t -> Z.t -> Z.t = <fun>

In :
let bad_next_state dw s =
{ w = s.w + dw;
y = s.y + s.v + s.w + dw;
v = s.v +
(sgn (s.y + s.v + s.w + dw))
(sgn s.y)
}

Out:
val bad_next_state : Z.t -> state -> state = <fun>

In :
let rec bad_final_state s dws =
match dws with
| [] -> s
| dw :: dws' ->
let s' = bad_next_state dw s in

Out:
val bad_final_state : state -> Z.t list -> state = <fun>

termination proof

### Termination proof

call bad_final_state (bad_next_state (List.hd dws) s) (List.tl dws) from bad_final_state s dws
original ordinalOrdinal.Int (Ordinal.count dws)
sub ordinalOrdinal.Int (Ordinal.count (List.tl dws))
path[not (dws = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
 num checks 8 arith assert lower 17 arith pivots 10 rlimit count 2400 mk clause 19 datatype occurs check 21 mk bool var 79 arith assert upper 12 datatype splits 3 decisions 13 arith add rows 16 arith bound prop 1 propagations 13 conflicts 9 arith fixed eqs 7 datatype accessor ax 5 arith conflicts 2 datatype constructor ax 8 final checks 6 added eqs 47 del clause 7 arith eq adapter 10 memory 34.97 max memory 75.93 num allocs 1.66005e+10
Expand
• start[0.014s]
not (dws = [])
&& Ordinal.count dws >= 0 && Ordinal.count (List.tl dws) >= 0
==> List.tl dws = []
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl dws)))
(Ordinal.Int (Ordinal.count dws))
• ##### simplify
 into (not ((not (dws = []) && Ordinal.count dws >= 0) && Ordinal.count (List.tl dws) >= 0) || List.tl dws = []) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl dws))) (Ordinal.Int (Ordinal.count dws)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_int list_2375| (… expansions
• unroll
 expr (|count_int list_2375| (|get.::.1_2363| dws_2365)) expansions
• unroll
 expr (|count_int list_2375| dws_2365) expansions
• ##### unsat
(let ((a!1 (>= (ite (>= (|get.::.0_2362| dws_2365) 0)
(|get.::.0_2362| dws_2365)…

Now, let's try one of our main safety theorems:

In :
theorem vehicle_stays_within_3_units_of_course dws =
arbitrary_delta_ws dws
==>
let s' = bad_final_state {y=0;w=0;v=0} dws in
-3 <= s'.y && s'.y <= 3

Out:
val vehicle_stays_within_3_units_of_course : Z.t list -> bool = <fun>
module CX : sig val dws : int list end
Error: vehicle_stays_within_3_units_of_course is not a theorem.

Counterexample (after 8 steps, 0.039s):
let (dws : int list) = [1; 1; 1]

Refuted
proof attempt
ground_instances8
definitions0
inductions0
search_time
0.039s
details
Expand
smt_stats
 arith offset eqs 31 num checks 17 arith assert lower 274 arith pivots 28 rlimit count 12184 mk clause 386 datatype occurs check 181 mk bool var 523 arith assert upper 181 datatype splits 41 decisions 185 arith add rows 92 arith bound prop 52 propagations 988 interface eqs 10 conflicts 40 arith fixed eqs 74 datatype accessor ax 38 minimized lits 8 arith conflicts 5 arith assert diseq 140 datatype constructor ax 46 final checks 37 added eqs 660 del clause 100 arith eq adapter 120 memory 34.47 max memory 75.93 num allocs 1.7084e+10
Expand
• start[0.039s]
List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_0:
==> -3 <= (bad_final_state {w = 0; y = 0; v = 0} :var_0:).y
&& (bad_final_state {w = 0; y = 0; v = 0} :var_0:).y <= 3
• #### simplify

 into not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_0:) || -3 <= (bad_final_state {w = 0; y = 0; v = 0} :var_0:).y && (bad_final_state {w = 0; y = 0; v = 0} :var_0:).y <= 3 expansions [] rewrite_steps forward_chaining
• unroll
 expr (bad_final_state_95 (|rec_mk.state_2396| 0 0 0) dws_2390) expansions
• unroll
 expr (|List.for_all anon_fun.arbitrary_delta_ws.0_2392| dws_2390) expansions
• unroll
 expr (let ((a!1 (+ (y_16 (|rec_mk.state_2396| 0 0 0)) (v_17 (|rec_mk.state_2396| 0 0 0)) … expansions
• unroll
 expr (|List.for_all anon_fun.arbitrary_delta_ws.0_2392| (|get.::.1_2389| dws_2390)) expansions
• unroll
 expr (let ((a!1 (+ (y_16 (|rec_mk.state_2396| 0 0 0)) (v_17 (|rec_mk.state_2396| 0 0 0)) … expansions
• unroll
 expr (|List.for_all anon_fun.arbitrary_delta_ws.0_2392| (|get.::.1_2389| (|get.::.1_2389| dws_2390… expansions
• unroll
 expr (let ((a!1 (+ (y_16 (|rec_mk.state_2396| 0 0 0)) (v_17 (|rec_mk.state_2396| 0 0 0)) … expansions
• unroll
 expr (|List.for_all anon_fun.arbitrary_delta_ws.0_2392| (|get.::.1_2389| (|get.::.1_2389| (|get.::… expansions
• Sat (Some let (dws : int list) = [1; 1; 1] )

Imandra shows us that with our flawed controller, this conjecture is not true! In fact, Imandra computes a counterexample consisting of a sequence of three 1-valued wind speed sensor readings.

If we plug these in, we can see the counterexample in action:

In :
bad_final_state {y=0; w=0; v=0} [1;1;1]

Out:
- : state = {w = 3; y = 4; v = -4}


Happy verifying!