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 [1]:
type state = {
  w : int; (* current wind speed *)
  y : int; (* y-position of the vehicle *)
  v : int; (* accumulated velocity *)
}
Out[1]:
type state = { w : int; y : int; v : int; }

Our controller and state transitions

In [2]:
let controller sgn_y sgn_old_y =
  (-3 * sgn_y) + (2 * sgn_old_y)
Out[2]:
val controller : int -> int -> int = <fun>
In [3]:
let sgn x =
  if x < 0 then -1
  else if x = 0 then 0
  else 1
Out[3]:
val sgn : int -> int = <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 [4]:
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[4]:
val next_state : int -> 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 [5]:
let arbitrary_delta_ws = List.for_all (fun x -> x = -1 || x = 0 || x = 1)
Out[5]:
val arbitrary_delta_ws : int 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 [6]:
let rec final_state s dws =
  match dws with
  | [] -> s
  | dw :: dws' ->
    let s' = next_state dw s in
    final_state s' dws'
[@@adm dws]
Out[6]:
val final_state : state -> int 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 (_cnt dws)
sub ordinalOrdinal.Int (_cnt (List.tl dws))
path[not (dws = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.017s
details
Expand
smt_stats
num checks8
arith-make-feasible20
arith-max-columns18
arith-conflicts2
rlimit count2230
mk clause12
datatype occurs check22
mk bool var65
arith-lower14
arith-diseq1
datatype splits3
decisions18
propagations13
arith-max-rows6
conflicts10
datatype accessor ax5
datatype constructor ax8
num allocs945053096
final checks6
added eqs43
del clause5
arith eq adapter10
arith-upper13
memory12.250000
max memory24.340000
Expand
  • start[0.017s]
      let (_x_0 : int) = count.list mk_nat dws in
      let (_x_1 : int list) = List.tl dws in
      let (_x_2 : int) = count.list mk_nat _x_1 in
      not (dws = []) && _x_0 >= 0 && _x_2 >= 0
      ==> _x_1 = [] || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
  • simplify
    into
    let (_x_0 : int list) = List.tl dws in
    let (_x_1 : int) = count.list mk_nat _x_0 in
    let (_x_2 : int) = count.list mk_nat dws in
    (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
    || not ((not (dws = []) && _x_2 >= 0) && _x_1 >= 0)
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|`count.list mk_nat[0]`_2702| dws_2690)
        expansions
        • unroll
          expr
          (|`count.list mk_nat[0]`_2702| (|get.::.1_2688| dws_2690))
          expansions
          • unroll
            expr
            (|Ordinal.<<_119| (|Ordinal.Int_108|
                                (|`count.list mk_nat[0]`_2702| (|get.::.1_2…
            expansions
            • Unsat

            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 [7]:
            (* 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[7]:
            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 [8]:
            theorem safety_1 s dw =
              good_state s
              && (dw = -1 || dw = 0 || dw = 1)
             ==>
              good_state (next_state dw s)
              [@@rewrite]
            
            Out[8]:
            val safety_1 : state -> int -> bool = <fun>
            
            Proved
            proof
            ground_instances0
            definitions0
            inductions0
            search_time
            0.030s
            details
            Expand
            smt_stats
            num checks1
            arith-make-feasible186
            arith-max-columns17
            arith-conflicts12
            rlimit count15543
            arith-cheap-eqs34
            mk clause1608
            mk bool var229
            arith-lower721
            arith-diseq1095
            decisions107
            arith-propagations878
            propagations2421
            arith-bound-propagations-cheap878
            arith-max-rows8
            conflicts65
            datatype accessor ax1
            minimized lits46
            arith-bound-propagations-lp341
            datatype constructor ax1
            num allocs1009806293
            added eqs715
            del clause144
            arith eq adapter89
            arith-upper578
            memory13.110000
            max memory24.340000
            Expand
            • start[0.030s]
                let (_x_0 : int) = :var_0:.w in
                let (_x_1 : int) = :var_0:.v in
                let (_x_2 : int) = _x_0 + _x_1 in
                let (_x_3 : bool) = 2 = _x_2 in
                let (_x_4 : int) = :var_0:.y in
                let (_x_5 : bool) = -2 = _x_4 in
                let (_x_6 : bool) = 1 = _x_2 in
                let (_x_7 : int) = _x_4 + _x_1 + _x_0 + :var_1: in
                let (_x_8 : int)
                    = _x_0 + :var_1:
                      + (_x_1
                         + (-3 * (if _x_7 < 0 then -1 else if _x_7 = 0 then 0 else 1)
                            + 2 * (if _x_4 < 0 then -1 else if _x_4 = 0 then 0 else 1)))
                in
                let (_x_9 : bool) = 2 = _x_8 in
                let (_x_10 : bool) = -2 = _x_7 in
                let (_x_11 : bool) = 1 = _x_8 in
                (if _x_6 && -3 = _x_4 then true
                 else
                 if _x_6 && _x_5 then true
                 else
                 if _x_3 && _x_5 then true else if _x_3 && -1 = _x_4 then true else …)
                && (:var_1: = -1 || :var_1: = 0 || :var_1: = 1)
                ==> (if _x_11 && -3 = _x_7 then true
                     else
                     if _x_11 && _x_10 then true
                     else
                     if _x_9 && _x_10 then true
                     else if _x_9 && -1 = _x_7 then true else …)
            • simplify

              into
              let (_x_0 : int) = :var_0:.w in
              let (_x_1 : int) = :var_0:.v in
              let (_x_2 : int) = :var_0:.y in
              let (_x_3 : int) = _x_2 + _x_1 + _x_0 + :var_1: in
              let (_x_4 : int)
                  = _x_0 + :var_1: + _x_1
                    + -3 * (if 0 <= _x_3 then if _x_3 = 0 then 0 else 1 else -1)
                    + 2 * (if 0 <= _x_2 then if _x_2 = 0 then 0 else 1 else -1)
              in
              let (_x_5 : bool) = 1 = _x_4 in
              let (_x_6 : bool) = -2 = _x_3 in
              let (_x_7 : bool) = 2 = _x_4 in
              let (_x_8 : bool) = -1 = _x_3 in
              let (_x_9 : bool) = -1 = _x_4 in
              let (_x_10 : bool) = 0 = _x_3 in
              let (_x_11 : bool) = -2 = _x_4 in
              let (_x_12 : bool) = 1 = _x_3 in
              let (_x_13 : bool) = 2 = _x_3 in
              let (_x_14 : int) = _x_0 + _x_1 in
              let (_x_15 : bool) = -1 = _x_14 in
              let (_x_16 : bool) = -2 = _x_14 in
              let (_x_17 : bool) = 2 = _x_2 in
              let (_x_18 : bool) = 1 = _x_2 in
              let (_x_19 : bool) = 1 = _x_14 in
              let (_x_20 : bool) = 0 = _x_2 in
              let (_x_21 : bool) = -1 = _x_2 in
              let (_x_22 : bool) = 2 = _x_14 in
              let (_x_23 : bool) = -2 = _x_2 in
              ((((((((((((_x_5 && -3 = _x_3 || _x_5 && _x_6) || _x_7 && _x_6)
                        || _x_7 && _x_8)
                       || 3 = _x_4 && _x_8)
                      || _x_9 && _x_10)
                     || _x_5 && _x_10)
                    || 0 = _x_4 && _x_10)
                   || _x_11 && _x_12)
                  || -3 = _x_4 && _x_12)
                 || _x_9 && _x_13)
                || _x_11 && _x_13)
               || _x_9 && 3 = _x_3)
              || not
                 (((((((((((((_x_15 && 3 = _x_2 || _x_16 && _x_17) || _x_15 && _x_17)
                            || -3 = _x_14 && _x_18)
                           || _x_16 && _x_18)
                          || _x_19 && _x_20)
                         || 0 = _x_14 && _x_20)
                        || _x_15 && _x_20)
                       || 3 = _x_14 && _x_21)
                      || _x_22 && _x_21)
                     || _x_22 && _x_23)
                    || _x_19 && _x_23)
                   || _x_19 && -3 = _x_2)
                  && ((:var_1: = -1 || :var_1: = 0) || :var_1: = 1))
              expansions
              []
              rewrite_steps
                forward_chaining
                • Unsat

                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 [9]:
                #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[9]:
                val all_good : state -> int 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 = [] ==> φ dws s)
                 && (not (dws = []) && φ (List.tl dws) (next_state (List.hd dws) s)
                     ==> φ dws s).
                
                2 nontautological subgoals.
                
                Subgoal 2:
                
                 H0. good_state s
                 H1. List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws
                 H2. dws = []
                |---------------------------------------------------------------------------
                 good_state (final_state s dws)
                
                But simplification reduces this to true, using the definitions of
                List.for_all and final_state.
                
                Subgoal 1:
                
                 H0. good_state s
                 H1. List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws
                 H2. not (dws = [])
                 H3. 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))
                |---------------------------------------------------------------------------
                 good_state (final_state s dws)
                
                This simplifies, using the definitions of List.for_all and final_state to the
                following 3 subgoals:
                
                Subgoal 1.3:
                
                 H0. List.hd dws = 1
                 H1. dws <> []
                 H2. good_state s
                 H3. List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
                |---------------------------------------------------------------------------
                 C0. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
                 C1. good_state (next_state (List.hd dws) s)
                 C2. List.hd dws = -1
                 C3. List.hd dws = 0
                
                But simplification reduces this to true, using the rewrite rule safety_1.
                
                Subgoal 1.2:
                
                 H0. dws <> []
                 H1. good_state s
                 H2. List.hd dws = 0
                 H3. List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
                |---------------------------------------------------------------------------
                 C0. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
                 C1. good_state (next_state (List.hd dws) s)
                 C2. List.hd dws = -1
                
                But simplification reduces this to true, using the rewrite rule safety_1.
                
                Subgoal 1.1:
                
                 H0. dws <> []
                 H1. good_state s
                 H2. List.hd dws = -1
                 H3. List.for_all (fun x -> x = -1 || x = 0 || x = 1) (List.tl dws)
                |---------------------------------------------------------------------------
                 C0. good_state (final_state (next_state (List.hd dws) s) (List.tl dws))
                 C1. good_state (next_state (List.hd dws) s)
                
                But simplification reduces this to true, using the rewrite rule safety_1.
                
                 Rules:
                    (:def List.for_all)
                    (:def final_state)
                    (:rw safety_1)
                    (:induct final_state)
                
                
                Proved
                proof
                ground_instances0
                definitions11
                inductions1
                search_time
                0.518s
                Expand
                • start[0.518s, "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.518s, "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 = [] ==> φ dws s)
                            && (not (dws = []) && φ (List.tl dws) (next_state (List.hd dws) s)
                                ==> φ dws s)
                  • Split (let (_x_0 : bool)
                               = good_state (final_state s dws)
                                 || not
                                    (good_state s
                                     && List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws)
                           in
                           let (_x_1 : bool) = not (dws = []) in
                           let (_x_2 : state) = next_state (List.hd dws) s in
                           let (_x_3 : int list) = List.tl dws in
                           (_x_0 || _x_1)
                           && (_x_0
                               || not
                                  (_x_1
                                   && (good_state (final_state _x_2 _x_3)
                                       || not
                                          (good_state _x_2
                                           && List.for_all (fun x -> x = -1 || x = 0 || x = 1)
                                              _x_3))))
                           :cases [((not (good_state s)
                                     || not
                                        (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
                                    || not (dws = []))
                                   || good_state (final_state s dws);
                                   let (_x_0 : state) = next_state (List.hd dws) s in
                                   let (_x_1 : int list) = List.tl dws in
                                   (((not (good_state s)
                                      || not
                                         (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
                                     || dws = [])
                                    || not
                                       (good_state _x_0
                                        && List.for_all (fun x -> x = -1 || x = 0 || x = 1) _x_1
                                        ==> good_state (final_state _x_0 _x_1)))
                                   || good_state (final_state s dws)])
                    • subproof
                      let (_x_0 : state) = next_state (List.hd dws) s in let (_x_1 : int list) = List.tl dws in (((not (good_state s) || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws)) || dws = []) || not (good_state _x_0 && List.for_all (fun x -> x = -1 || x = 0 || x = 1) _x_1 ==> good_state (final_state _x_0 _x_1))) || good_state (final_state s dws)
                      • start[0.518s, "1"]
                          let (_x_0 : state) = next_state (List.hd dws) s in
                          let (_x_1 : int list) = List.tl dws in
                          (((not (good_state s)
                             || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
                            || dws = [])
                           || not
                              (good_state _x_0
                               && List.for_all (fun x -> x = -1 || x = 0 || x = 1) _x_1
                               ==> good_state (final_state _x_0 _x_1)))
                          || good_state (final_state s dws)
                      • simplify
                        into
                        let (_x_0 : int) = List.hd dws in
                        let (_x_1 : bool) = dws = [] in
                        let (_x_2 : state) = next_state _x_0 s in
                        let (_x_3 : int list) = List.tl dws in
                        let (_x_4 : bool) = good_state (final_state _x_2 _x_3) in
                        let (_x_5 : bool) = good_state _x_2 in
                        let (_x_6 : bool) = not (good_state s) in
                        let (_x_7 : bool) = _x_0 = -1 in
                        let (_x_8 : bool) = _x_0 = 0 in
                        let (_x_9 : bool)
                            = not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) _x_3)
                        in
                        let (_x_10 : bool) = ((_x_1 || _x_4) || _x_5) || _x_6 in
                        ((((((((not (_x_0 = 1) || _x_1) || _x_4) || _x_5) || _x_6) || _x_7) || _x_8)
                          || _x_9)
                         && (((_x_10 || _x_7) || not _x_8) || _x_9))
                        && ((_x_10 || not _x_7) || _x_9)
                        expansions
                        [final_state, final_state, final_state, List.for_all, List.for_all,
                         final_state, final_state, final_state, List.for_all]
                        rewrite_steps
                          forward_chaining
                            • Subproof
                            • Subproof
                            • Subproof
                        • subproof
                          ((not (good_state s) || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws)) || not (dws = [])) || good_state (final_state s dws)
                          • start[0.518s, "2"]
                              ((not (good_state s)
                                || not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) dws))
                               || not (dws = []))
                              || good_state (final_state s dws)
                          • simplify
                            into
                            true
                            expansions
                            [final_state, List.for_all]
                            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 [10]:
                        #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[10]:
                        val vehicle_stays_within_3_units_of_course : int list -> bool = <fun>
                        
                        Proved
                        proof
                        ground_instances0
                        definitions0
                        inductions0
                        search_time
                        0.043s
                        details
                        Expand
                        smt_stats
                        rlimit count8854
                        mk bool var1
                        num allocs3163417828
                        memory23.830000
                        max memory46.900000
                        Expand
                        • start[0.043s]
                            let (_x_0 : int) = (final_state {w = 0; y = 0; v = 0} :var_0:).y in
                            List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_0:
                            ==> -3 <= _x_0 && _x_0 <= 3
                        • simplify

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

                              into
                              true
                              expansions
                              []
                              rewrite_steps
                                forward_chaining
                                all_good
                              • Unsat

                              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 [11]:
                              let steady_wind = List.for_all (fun x -> x = 0)
                              
                              let at_least_4 xs = match xs with
                                  _ :: _ :: _ :: _ :: _ -> true
                                | _ -> false
                              
                              Out[11]:
                              val steady_wind : int list -> bool = <fun>
                              val at_least_4 : 'a list -> bool = <fun>
                              
                              In [12]:
                              #disable next_state;;
                              #disable good_state;;
                              #max_induct 4;;
                              
                              theorem good_state_find_and_stay_zt_zero s dws =
                               good_state s
                               && steady_wind dws
                               && at_least_4 dws
                               ==>
                               let s' = (final_state s dws) [@trigger] in
                               s'.y = 0
                              [@@induct functional final_state]
                              [@@forward_chaining]
                              ;;
                              
                              Out[12]:
                              val good_state_find_and_stay_zt_zero : state -> int 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 to the
                              following 4 subgoals:
                              
                              Subgoal 1.4:
                              
                               H0. dws <> []
                               H1. good_state s
                               H2. (List.tl (List.tl (List.tl dws))) <> []
                               H3. (List.tl dws) <> []
                               H4. (List.tl (List.tl dws)) <> []
                               H5. List.hd dws = 0
                               H6. List.for_all (fun x -> x = 0) (List.tl dws)
                              |---------------------------------------------------------------------------
                               C0. good_state (next_state (List.hd dws) s)
                               C1. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                              
                              But simplification reduces this to true, using the definition of
                              List.for_all, and the rewrite rule safety_1.
                              
                              Subgoal 1.3:
                              
                               H0. dws <> []
                               H1. good_state s
                               H2. (List.tl (List.tl (List.tl dws))) <> []
                               H3. (List.tl dws) <> []
                               H4. (List.tl (List.tl dws)) <> []
                               H5. good_state (next_state (List.hd dws) s)
                               H6. List.hd dws = 0
                               H7. List.for_all (fun x -> x = 0) (List.tl dws)
                              |---------------------------------------------------------------------------
                               C0. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                               C1. List.hd (List.tl dws) = 0
                              
                              But simplification reduces this to true, using the definition of
                              List.for_all.
                              
                              Subgoal 1.2:
                              
                               H0. dws <> []
                               H1. good_state s
                               H2. (List.tl (List.tl (List.tl dws))) <> []
                               H3. (List.tl dws) <> []
                               H4. (List.tl (List.tl dws)) <> []
                               H5. good_state (next_state (List.hd dws) s)
                               H6. List.hd (List.tl dws) = 0
                               H7. List.hd dws = 0
                               H8. List.for_all (fun x -> x = 0) (List.tl dws)
                              |---------------------------------------------------------------------------
                               C0. (final_state (next_state (List.hd dws) s) (List.tl dws)).y = 0
                               C1. List.for_all (fun x -> x = 0) (List.tl (List.tl dws))
                              
                              But simplification reduces this to true, using the definition of
                              List.for_all.
                              
                              Subgoal 1.1:
                              
                               H0. dws <> []
                               H1. good_state s
                               H2. (List.tl (List.tl (List.tl dws))) <> []
                               H3. (List.tl dws) <> []
                               H4. (List.tl (List.tl dws)) <> []
                               H5. good_state (next_state (List.hd dws) s)
                               H6. List.hd (List.tl dws) = 0
                               H7. List.hd dws = 0
                               H8. List.for_all (fun x -> x = 0) (List.tl (List.tl dws))
                               H9. List.for_all (fun x -> x = 0) (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, and the rewrite rule
                              safety_1 to:
                              
                              Subgoal 1.1':
                              
                               H0. good_state s
                               H1. (List.tl (List.tl (List.tl dws))) <> []
                               H2. dws <> []
                               H3. (List.tl dws) <> []
                               H4. (List.tl (List.tl dws)) <> []
                               H5. List.hd (List.tl dws) = 0
                               H6. List.hd dws = 0
                               H7. List.hd (List.tl (List.tl dws)) = 0
                               H8. List.for_all (fun x -> x = 0) (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.1'':
                              
                               H0. good_state s
                               H1. (List.tl (List.tl (List.tl dws))) <> []
                               H2. dws <> []
                               H3. (List.tl dws) <> []
                               H4. (List.tl (List.tl dws)) <> []
                               H5. List.hd (List.tl dws) = 0
                               H6. List.hd dws = 0
                               H7. List.hd (List.tl (List.tl dws)) = 0
                               H8. List.hd (List.tl (List.tl (List.tl dws))) = 0
                               H9. List.for_all (fun x -> x = 0)
                                   (List.tl (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.1''':
                              
                               H0. good_state s
                               H1. (List.tl (List.tl (List.tl dws))) <> []
                               H2. dws <> []
                               H3. (List.tl dws) <> []
                               H4. (List.tl (List.tl dws)) <> []
                               H5. List.hd (List.tl dws) = 0
                               H6. List.hd dws = 0
                               H7. List.hd (List.tl (List.tl dws)) = 0
                               H8. List.hd (List.tl (List.tl (List.tl dws))) = 0
                              |---------------------------------------------------------------------------
                               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.1'''':
                              
                               H0. good_state s
                               H1. (List.tl (List.tl (List.tl dws))) <> []
                               H2. dws <> []
                               H3. (List.tl dws) <> []
                               H4. (List.tl (List.tl dws)) <> []
                               H5. List.hd (List.tl dws) = 0
                               H6. List.hd dws = 0
                               H7. List.hd (List.tl (List.tl dws)) = 0
                               H8. List.hd (List.tl (List.tl (List.tl dws))) = 0
                              |---------------------------------------------------------------------------
                               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.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
                              definitions18
                              inductions1
                              search_time
                              1.959s
                              details
                              Expand
                              smt_stats
                              num checks9
                              arith-assume-eqs1
                              arith-make-feasible260
                              arith-max-columns73
                              arith-conflicts10
                              rlimit count211904
                              arith-cheap-eqs266
                              mk clause2512
                              datatype occurs check21
                              mk bool var1062
                              arith-lower712
                              arith-diseq991
                              decisions126
                              arith-propagations769
                              propagations3116
                              interface eqs1
                              arith-bound-propagations-cheap769
                              arith-max-rows42
                              conflicts60
                              datatype accessor ax16
                              minimized lits88
                              arith-bound-propagations-lp248
                              datatype constructor ax10
                              final checks5
                              added eqs2824
                              del clause1166
                              arith eq adapter315
                              arith-upper685
                              memory57.090000
                              max memory74.220000
                              num allocs19096889088.000000
                              Expand
                              • start[1.959s, "Goal"]
                                  let (_x_0 : int list) = List.tl :var_1: in
                                  let (_x_1 : int list) = List.tl _x_0 in
                                  good_state :var_0:
                                  && List.for_all (fun x -> x = 0) :var_1:
                                     && :var_1: <> [] && _x_0 <> [] && _x_1 <> [] && (List.tl _x_1) <> []
                                  ==> (final_state :var_0: :var_1:).y = 0
                              • subproof

                                let (_x_0 : int list) = List.tl dws in let (_x_1 : int list) = List.tl _x_0 in (((((not (good_state s) || not (List.for_all (fun x -> x = 0) dws)) || not (dws <> [])) || not (_x_0 <> [])) || not (_x_1 <> [])) || not ((List.tl _x_1) <> [])) || (final_state s dws).y = 0
                                • start[1.959s, "1"]
                                    let (_x_0 : int list) = List.tl dws in
                                    let (_x_1 : int list) = List.tl _x_0 in
                                    (((((not (good_state s) || not (List.for_all (fun x -> x = 0) dws))
                                        || not (dws <> []))
                                       || not (_x_0 <> []))
                                      || not (_x_1 <> []))
                                     || not ((List.tl _x_1) <> []))
                                    || (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 (let (_x_0 : bool) = (final_state s dws).y = 0 in
                                         let (_x_1 : bool) = not (dws = []) in
                                         let (_x_2 : int list) = List.tl dws in
                                         let (_x_3 : bool) = _x_2 <> [] in
                                         let (_x_4 : int list) = List.tl _x_2 in
                                         let (_x_5 : bool) = _x_4 <> [] in
                                         let (_x_6 : int list) = List.tl _x_4 in
                                         let (_x_7 : bool) = _x_6 <> [] in
                                         let (_x_8 : bool)
                                             = not
                                               (((((good_state s && List.for_all (fun x -> x = 0) dws)
                                                   && dws <> [])
                                                  && _x_3)
                                                 && _x_5)
                                                && _x_7)
                                         in
                                         let (_x_9 : state) = next_state (List.hd dws) s in
                                         ((_x_0 || _x_1) || _x_8)
                                         && ((_x_0
                                              || not
                                                 (_x_1
                                                  && (not
                                                      (((((good_state _x_9
                                                           && List.for_all (fun x -> x = 0) _x_2)
                                                          && _x_3)
                                                         && _x_5)
                                                        && _x_7)
                                                       && (List.tl _x_6) <> [])
                                                      || (final_state _x_9 _x_2).y = 0)))
                                             || _x_8)
                                         :cases [let (_x_0 : int list) = List.tl dws in
                                                 let (_x_1 : int list) = List.tl _x_0 in
                                                 ((((((not (dws = []) || not (good_state s))
                                                      || not (List.for_all (fun x -> x = 0) dws))
                                                     || not (dws <> []))
                                                    || not (_x_0 <> []))
                                                   || not (_x_1 <> []))
                                                  || not ((List.tl _x_1) <> []))
                                                 || (final_state s dws).y = 0;
                                                 let (_x_0 : state) = next_state (List.hd dws) s in
                                                 let (_x_1 : int list) = List.tl dws in
                                                 let (_x_2 : bool) = _x_1 <> [] in
                                                 let (_x_3 : int list) = List.tl _x_1 in
                                                 let (_x_4 : bool) = _x_3 <> [] in
                                                 let (_x_5 : int list) = List.tl _x_3 in
                                                 let (_x_6 : bool) = _x_5 <> [] in
                                                 (((((((dws = []
                                                        || not
                                                           (((((good_state _x_0
                                                                && List.for_all (fun x -> x = 0) _x_1)
                                                               && _x_2)
                                                              && _x_4)
                                                             && _x_6)
                                                            && (List.tl _x_5) <> []
                                                            ==> (final_state _x_0 _x_1).y = 0))
                                                       || not (good_state s))
                                                      || not (List.for_all (fun x -> x = 0) dws))
                                                     || not (dws <> []))
                                                    || not _x_2)
                                                   || not _x_4)
                                                  || not _x_6)
                                                 || (final_state s dws).y = 0])
                                  • subproof
                                    let (_x_0 : state) = next_state (List.hd dws) s in let (_x_1 : int list) = List.tl dws in let (_x_2 : bool) = _x_1 <> [] in let (_x_3 : int list) = List.tl _x_1 in let (_x_4 : bool) = _x_3 <> [] in let (_x_5 : int list) = List.tl _x_3 in let (_x_6 : bool) = _x_5 <> [] in (((((((dws = [] || not (((((good_state _x_0 && List.for_all (fun x -> x = 0) _x_1) && _x_2) && _x_4) && _x_6) && (List.tl _x_5) <> [] ==> (final_state _x_0 _x_1).y = 0)) || not (good_state s)) || not (List.for_all (fun x -> x = 0) dws)) || not (dws <> [])) || not _x_2) || not _x_4) || not _x_6) || (final_state s dws).y = 0
                                    • start[1.958s, "1"]
                                        let (_x_0 : state) = next_state (List.hd dws) s in
                                        let (_x_1 : int list) = List.tl dws in
                                        let (_x_2 : bool) = _x_1 <> [] in
                                        let (_x_3 : int list) = List.tl _x_1 in
                                        let (_x_4 : bool) = _x_3 <> [] in
                                        let (_x_5 : int list) = List.tl _x_3 in
                                        let (_x_6 : bool) = _x_5 <> [] in
                                        (((((((dws = []
                                               || not
                                                  (((((good_state _x_0 && List.for_all (fun x -> x = 0) _x_1)
                                                      && _x_2)
                                                     && _x_4)
                                                    && _x_6)
                                                   && (List.tl _x_5) <> [] ==> (final_state _x_0 _x_1).y = 0))
                                              || not (good_state s))
                                             || not (List.for_all (fun x -> x = 0) dws))
                                            || not (dws <> []))
                                           || not _x_2)
                                          || not _x_4)
                                         || not _x_6)
                                        || (final_state s dws).y = 0
                                    • simplify
                                      into
                                      let (_x_0 : bool) = dws = [] in
                                      let (_x_1 : int) = List.hd dws in
                                      let (_x_2 : state) = next_state _x_1 s in
                                      let (_x_3 : bool) = good_state _x_2 in
                                      let (_x_4 : int list) = List.tl dws in
                                      let (_x_5 : bool) = (final_state _x_2 _x_4).y = 0 in
                                      let (_x_6 : bool) = not (good_state s) in
                                      let (_x_7 : int list) = List.tl _x_4 in
                                      let (_x_8 : int list) = List.tl _x_7 in
                                      let (_x_9 : bool) = not (_x_8 <> []) in
                                      let (_x_10 : bool) = not (_x_4 <> []) in
                                      let (_x_11 : bool) = not (_x_7 <> []) in
                                      let (_x_12 : bool) = not (_x_1 = 0) in
                                      let (_x_13 : bool) = not (List.for_all (fun x -> x = 0) _x_4) in
                                      let (_x_14 : bool) = not _x_3 in
                                      let (_x_15 : bool)
                                          = (((((_x_0 || _x_5) || _x_6) || _x_9) || _x_10) || _x_11) || _x_14
                                      in
                                      let (_x_16 : bool) = List.hd _x_4 = 0 in
                                      let (_x_17 : bool) = not _x_16 in
                                      let (_x_18 : bool) = List.for_all (fun x -> x = 0) _x_7 in
                                      ((((((((((_x_0 || _x_3) || _x_5) || _x_6) || _x_9) || _x_10) || _x_11)
                                          || _x_12)
                                         || _x_13)
                                        && (((_x_15 || _x_12) || _x_16) || _x_13))
                                       && ((((_x_15 || _x_17) || _x_12) || _x_18) || _x_13))
                                      && (((((((((((_x_0 || (List.tl _x_8) <> []) || _x_5) || _x_6) || _x_9)
                                                || _x_10)
                                               || _x_11)
                                              || _x_14)
                                             || _x_17)
                                            || _x_12)
                                           || not _x_18)
                                          || _x_13)
                                      expansions
                                      [final_state, List.for_all, final_state, List.for_all, final_state,
                                       List.for_all, final_state, List.for_all, final_state, List.for_all,
                                       List.for_all]
                                      rewrite_steps
                                        forward_chaining
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • all_good
                                        • Subproof
                                        • Subproof
                                        • Subproof
                                        • Subproof
                                    • subproof
                                      let (_x_0 : int list) = List.tl dws in let (_x_1 : int list) = List.tl _x_0 in ((((((not (dws = []) || not (good_state s)) || not (List.for_all (fun x -> x = 0) dws)) || not (dws <> [])) || not (_x_0 <> [])) || not (_x_1 <> [])) || not ((List.tl _x_1) <> [])) || (final_state s dws).y = 0
                                      • start[1.958s, "2"]
                                          let (_x_0 : int list) = List.tl dws in
                                          let (_x_1 : int list) = List.tl _x_0 in
                                          ((((((not (dws = []) || not (good_state s))
                                               || not (List.for_all (fun x -> x = 0) dws))
                                              || not (dws <> []))
                                             || not (_x_0 <> []))
                                            || not (_x_1 <> []))
                                           || not ((List.tl _x_1) <> []))
                                          || (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 [13]:
                                    #enable good_state;;
                                    
                                    theorem good_state_find_and_stay_0_from_origin dws =
                                     steady_wind dws
                                     && at_least_4 dws
                                     ==>
                                     let s' = final_state {y=0;w=0;v=0} dws in
                                     s'.y = 0
                                    [@@simp]
                                    
                                    Out[13]:
                                    val good_state_find_and_stay_0_from_origin : int list -> bool = <fun>
                                    
                                    Proved
                                    proof
                                    ground_instances0
                                    definitions0
                                    inductions0
                                    search_time
                                    0.053s
                                    details
                                    Expand
                                    smt_stats
                                    rlimit count16175
                                    mk bool var1
                                    memory56.490000
                                    max memory74.220000
                                    num allocs19572367017.000000
                                    Expand
                                    • start[0.053s]
                                        let (_x_0 : int list) = List.tl :var_0: in
                                        let (_x_1 : int list) = List.tl _x_0 in
                                        List.for_all (fun x -> x = 0) :var_0:
                                        && :var_0: <> [] && _x_0 <> [] && _x_1 <> [] && (List.tl _x_1) <> []
                                        ==> (final_state {w = 0; y = 0; v = 0} :var_0:).y = 0
                                    • simplify

                                      into
                                      let (_x_0 : int list) = List.tl :var_0: in
                                      let (_x_1 : int list) = List.tl _x_0 in
                                      not
                                      ((((List.for_all (fun x -> x = 0) :var_0: && :var_0: <> []) && _x_0 <> [])
                                        && _x_1 <> [])
                                       && (List.tl _x_1) <> [])
                                      || (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_good
                                            • good_state_find_and_stay_zt_zero
                                          • Unsat

                                          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 [14]:
                                          let bad_controller sgn_y sgn_old_y =
                                            (-4 * sgn_y) + (2 * sgn_old_y)
                                          
                                          Out[14]:
                                          val bad_controller : int -> int -> int = <fun>
                                          
                                          In [15]:
                                          let bad_next_state dw s =
                                            { w = s.w + dw;
                                              y = s.y + s.v + s.w + dw;
                                              v = s.v +
                                                  bad_controller
                                                    (sgn (s.y + s.v + s.w + dw))
                                                    (sgn s.y)
                                            }
                                          
                                          Out[15]:
                                          val bad_next_state : int -> state -> state = <fun>
                                          
                                          In [16]:
                                          let rec bad_final_state s dws =
                                            match dws with
                                            | [] -> s
                                            | dw :: dws' ->
                                              let s' = bad_next_state dw s in
                                              bad_final_state s' dws'
                                          [@@adm dws]
                                          
                                          Out[16]:
                                          val bad_final_state : state -> int 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`
                                          originalbad_final_state s dws
                                          subbad_final_state (bad_next_state (List.hd dws) s) (List.tl dws)
                                          original ordinalOrdinal.Int (_cnt dws)
                                          sub ordinalOrdinal.Int (_cnt (List.tl dws))
                                          path[not (dws = [])]
                                          proof
                                          detailed proof
                                          ground_instances3
                                          definitions0
                                          inductions0
                                          search_time
                                          0.013s
                                          details
                                          Expand
                                          smt_stats
                                          num checks8
                                          arith-make-feasible20
                                          arith-max-columns18
                                          arith-conflicts2
                                          rlimit count2230
                                          mk clause12
                                          datatype occurs check22
                                          mk bool var65
                                          arith-lower14
                                          arith-diseq1
                                          datatype splits3
                                          decisions18
                                          propagations13
                                          arith-max-rows6
                                          conflicts10
                                          datatype accessor ax5
                                          datatype constructor ax8
                                          final checks6
                                          added eqs43
                                          del clause5
                                          arith eq adapter10
                                          arith-upper13
                                          memory54.040000
                                          max memory74.220000
                                          num allocs19896080018.000000
                                          Expand
                                          • start[0.013s]
                                              let (_x_0 : int) = count.list mk_nat dws in
                                              let (_x_1 : int list) = List.tl dws in
                                              let (_x_2 : int) = count.list mk_nat _x_1 in
                                              not (dws = []) && _x_0 >= 0 && _x_2 >= 0
                                              ==> _x_1 = [] || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                          • simplify
                                            into
                                            let (_x_0 : int list) = List.tl dws in
                                            let (_x_1 : int) = count.list mk_nat _x_0 in
                                            let (_x_2 : int) = count.list mk_nat dws in
                                            (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                            || not ((not (dws = []) && _x_2 >= 0) && _x_1 >= 0)
                                            expansions
                                            []
                                            rewrite_steps
                                              forward_chaining
                                              • unroll
                                                expr
                                                (|`count.list mk_nat[0]`_4956| dws_4944)
                                                expansions
                                                • unroll
                                                  expr
                                                  (|`count.list mk_nat[0]`_4956| (|get.::.1_4942| dws_4944))
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (|Ordinal.<<_119| (|Ordinal.Int_108|
                                                                        (|`count.list mk_nat[0]`_4956| (|get.::.1_4…
                                                    expansions
                                                    • Unsat

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

                                                    In [17]:
                                                    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[17]:
                                                    val vehicle_stays_within_3_units_of_course : int 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.035s):
                                                     let (dws : int list) = [1; 1; 1]
                                                    
                                                    Refuted
                                                    proof attempt
                                                    ground_instances8
                                                    definitions0
                                                    inductions0
                                                    search_time
                                                    0.035s
                                                    details
                                                    Expand
                                                    smt_stats
                                                    num checks17
                                                    arith-assume-eqs12
                                                    arith-make-feasible227
                                                    arith-max-columns61
                                                    arith-conflicts3
                                                    rlimit count17439
                                                    arith-cheap-eqs200
                                                    mk clause1041
                                                    datatype occurs check183
                                                    mk bool var730
                                                    arith-lower307
                                                    arith-diseq521
                                                    datatype splits41
                                                    decisions176
                                                    arith-propagations421
                                                    propagations1707
                                                    interface eqs12
                                                    arith-bound-propagations-cheap421
                                                    arith-max-rows32
                                                    conflicts53
                                                    datatype accessor ax41
                                                    minimized lits23
                                                    arith-bound-propagations-lp139
                                                    datatype constructor ax49
                                                    final checks39
                                                    added eqs1244
                                                    del clause178
                                                    arith eq adapter198
                                                    arith-upper535
                                                    memory55.390000
                                                    max memory74.220000
                                                    num allocs20137764036.000000
                                                    Expand
                                                    • start[0.035s]
                                                        let (_x_0 : int) = (bad_final_state {w = 0; y = 0; v = 0} :var_0:).y in
                                                        List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_0:
                                                        ==> -3 <= _x_0 && _x_0 <= 3
                                                    • simplify

                                                      into
                                                      let (_x_0 : int) = (bad_final_state {w = 0; y = 0; v = 0} :var_0:).y in
                                                      not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) :var_0:)
                                                      || -3 <= _x_0 && _x_0 <= 3
                                                      expansions
                                                      []
                                                      rewrite_steps
                                                        forward_chaining
                                                        • unroll
                                                          expr
                                                          (bad_final_state_96 (|rec_mk.state_5000| 0 0 0) dws_4994)
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (|`List.for_all anon_fun.arbitrary_delta_ws.1[0]`_4996| dws_4994)
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (bad_final_state_96
                                                                (bad_next_state_93 (|get.::.0_4992| dws_4994) (|rec_mk.state_5000| 0 0 0))
                                                                (…
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (|`List.for_all anon_fun.arbitrary_delta_ws.1[0]`_4996|
                                                                  (|get.::.1_4993| dws_4994))
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (bad_final_state_96
                                                                    (bad_next_state_93
                                                                      (|get.::.0_4992| (|get.::.1_4993| dws_4994))
                                                                      (bad_n…
                                                                  expansions
                                                                  • unroll
                                                                    expr
                                                                    (|`List.for_all anon_fun.arbitrary_delta_ws.1[0]`_4996|
                                                                      (|get.::.1_4993| (|get.::.1_4993| dws_4994…
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (let ((a!1 (bad_next_state_93
                                                                                   (|get.::.0_4992| (|get.::.1_4993| (|get.::.1_4993| dws_49…
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (|`List.for_all anon_fun.arbitrary_delta_ws.1[0]`_4996|
                                                                          (|get.::.1_4993| (|get.::.1_4993| (|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 [18]:
                                                                        bad_final_state {y=0; w=0; v=0} [1;1;1]
                                                                        
                                                                        Out[18]:
                                                                        - : state = {w = 3; y = 4; v = -4}
                                                                        

                                                                        Happy verifying!