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 (Ordinal.count dws)
sub ordinalOrdinal.Int (Ordinal.count (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 count2226
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 allocs854483833
final checks6
added eqs43
del clause5
arith eq adapter10
arith-upper13
memory20.300000
max memory20.300000
Expand
  • start[0.017s]
      let (_x_0 : int) = Ordinal.count dws in
      let (_x_1 : int list) = List.tl dws in
      let (_x_2 : int) = Ordinal.count _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) = Ordinal.count _x_0 in
    let (_x_2 : int) = Ordinal.count 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_`int list`_2465| dws_2455)
        expansions
        • unroll
          expr
          (|count_`int list`_2465| (|get.::.1_2453| dws_2455))
          expansions
          • unroll
            expr
            (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`int list`_2465|
                                                  (…
            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.034s
            details
            Expand
            smt_stats
            num checks1
            arith-make-feasible226
            arith-max-columns17
            arith-conflicts13
            rlimit count19266
            arith-cheap-eqs32
            mk clause1982
            mk bool var205
            arith-lower856
            arith-diseq1376
            decisions172
            arith-propagations1240
            propagations3776
            arith-bound-propagations-cheap1240
            arith-max-rows8
            conflicts92
            datatype accessor ax1
            minimized lits104
            arith-bound-propagations-lp360
            datatype constructor ax1
            num allocs922145022
            added eqs835
            del clause147
            arith eq adapter92
            arith-upper778
            memory21.230000
            max memory22.140000
            Expand
            • start[0.034s]
                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. 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)
                 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.493s
                Expand
                • start[0.493s, "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.493s, "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.493s, "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 : state) = next_state _x_0 s in
                        let (_x_2 : int list) = List.tl dws in
                        let (_x_3 : bool)
                            = ((dws = [] || good_state (final_state _x_1 _x_2)) || good_state _x_1)
                              || not (good_state s)
                        in
                        let (_x_4 : bool) = _x_0 = -1 in
                        let (_x_5 : bool) = _x_3 || _x_4 in
                        let (_x_6 : bool) = _x_0 = 0 in
                        let (_x_7 : bool)
                            = not (List.for_all (fun x -> x = -1 || x = 0 || x = 1) _x_2)
                        in
                        ((((_x_5 || _x_6) || not (_x_0 = 1)) || _x_7) && ((_x_5 || not _x_6) || _x_7))
                        && ((_x_3 || not _x_4) || _x_7)
                        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.493s, "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.041s
                        details
                        Expand
                        smt_stats
                        rlimit count8857
                        mk bool var1
                        num allocs3305919511
                        memory21.110000
                        max memory49.410000
                        Expand
                        • start[0.041s]
                            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. List.for_all (fun x -> x = 0) (List.tl (List.tl (List.tl dws)))
                               H1. good_state s
                               H2. (List.tl (List.tl (List.tl dws))) <> []
                               H3. dws <> []
                               H4. (List.tl dws) <> []
                               H5. (List.tl (List.tl dws)) <> []
                               H6. List.hd (List.tl dws) = 0
                               H7. List.hd dws = 0
                               H8. List.hd (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 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.for_all (fun x -> x = 0)
                                   (List.tl (List.tl (List.tl (List.tl dws))))
                               H9. 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 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.901s
                              details
                              Expand
                              smt_stats
                              num checks9
                              arith-assume-eqs7
                              arith-make-feasible342
                              arith-max-columns73
                              arith-conflicts23
                              rlimit count217680
                              arith-cheap-eqs337
                              mk clause2735
                              datatype occurs check61
                              mk bool var1142
                              arith-lower812
                              arith-diseq1362
                              decisions210
                              arith-propagations1012
                              propagations4146
                              interface eqs7
                              arith-bound-propagations-cheap1012
                              arith-max-rows42
                              conflicts78
                              datatype accessor ax16
                              minimized lits193
                              arith-bound-propagations-lp346
                              datatype constructor ax10
                              final checks11
                              added eqs3511
                              del clause1097
                              arith eq adapter347
                              arith-upper1074
                              memory60.600000
                              max memory68.100000
                              num allocs18996288449.000000
                              Expand
                              • start[1.901s, "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.901s, "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.899s, "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.899s, "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.048s
                                    details
                                    Expand
                                    smt_stats
                                    rlimit count16175
                                    mk bool var1
                                    memory42.440000
                                    max memory68.100000
                                    num allocs20140551837.000000
                                    Expand
                                    • start[0.048s]
                                        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 (Ordinal.count dws)
                                          sub ordinalOrdinal.Int (Ordinal.count (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 count2226
                                          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
                                          memory39.920000
                                          max memory68.100000
                                          num allocs20478113172.000000
                                          Expand
                                          • start[0.013s]
                                              let (_x_0 : int) = Ordinal.count dws in
                                              let (_x_1 : int list) = List.tl dws in
                                              let (_x_2 : int) = Ordinal.count _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) = Ordinal.count _x_0 in
                                            let (_x_2 : int) = Ordinal.count 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_`int list`_4715| dws_4705)
                                                expansions
                                                • unroll
                                                  expr
                                                  (|count_`int list`_4715| (|get.::.1_4703| dws_4705))
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`int list`_4715|
                                                                                          (…
                                                    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.032s):
                                                     let (dws : int list) = [1; 1; 1]
                                                    
                                                    Refuted
                                                    proof attempt
                                                    ground_instances8
                                                    definitions0
                                                    inductions0
                                                    search_time
                                                    0.032s
                                                    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
                                                    memory41.300000
                                                    max memory68.100000
                                                    num allocs20717699168.000000
                                                    Expand
                                                    • start[0.032s]
                                                        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_94 (|rec_mk.state_4754| 0 0 0) dws_4748)
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (|`List.for_all anon_fun.arbitrary_delta_ws.1[0]`_4750| dws_4748)
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (bad_final_state_94
                                                                (bad_next_state_91 (|get.::.0_4746| dws_4748) (|rec_mk.state_4754| 0 0 0))
                                                                (…
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (|`List.for_all anon_fun.arbitrary_delta_ws.1[0]`_4750|
                                                                  (|get.::.1_4747| dws_4748))
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (bad_final_state_94
                                                                    (bad_next_state_91
                                                                      (|get.::.0_4746| (|get.::.1_4747| dws_4748))
                                                                      (bad_n…
                                                                  expansions
                                                                  • unroll
                                                                    expr
                                                                    (|`List.for_all anon_fun.arbitrary_delta_ws.1[0]`_4750|
                                                                      (|get.::.1_4747| (|get.::.1_4747| dws_4748…
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (let ((a!1 (bad_next_state_91
                                                                                   (|get.::.0_4746| (|get.::.1_4747| (|get.::.1_4747| dws_47…
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (|`List.for_all anon_fun.arbitrary_delta_ws.1[0]`_4750|
                                                                          (|get.::.1_4747| (|get.::.1_4747| (|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!