The stoplight model

In this notebook we want to explore a simple model of a car approaching an intersection. The model is not supposed to be representative of a real world simulation, but rather a first stage high level abstraction of one such.

We start by defining datatypes representing the state of the stoplight in the intersection:

In [1]:
(* Street light color *)
type color = Green | Yellow | Red ;;

(* State representation of an intersection. *)
type light_state = {
    blinking : bool;
    current_time : int;
    (* Transition every X seconds *)
    blink_time : int;
    (* Transition period *)
    light_change_time : int;
    (* Intersection light *)
    light_state : color;
  };;
Out[1]:
type color = Green | Yellow | Red
type light_state = {
  blinking : bool;
  current_time : Z.t;
  blink_time : Z.t;
  light_change_time : Z.t;
  light_state : color;
}

Next we define a transition function for the stoplight:

In [2]:
(* Update the light *)
let light_step (l : light_state) =
  let l = { l with current_time = l.current_time + 1 } in
  if l.current_time > l.light_change_time then
    begin
      let l = { l with blinking = false } in
      match l.light_state with
      | Green -> { l with light_state = Yellow }
      | Yellow -> { l with light_state = Red }
      | Red -> { l with light_state = Green }
    end
  else if l.current_time > l.blink_time then
    begin match l.light_state with
    | Green | Yellow -> { l with blinking = true }
    | Red -> l
    end
  else
    l
;;
Out[2]:
val light_step : light_state -> light_state = <fun>

We do the same for the state of the car approaching said stoplight:

In [3]:
(* Driving state *)
type driving_state = Accelerating | Steady | Braking;;

(* Current car state *)
type car_state = {
    car_drive_state : driving_state;
    car_speed : int; (* Speed of the car meters/time *)
    car_distance : int; (* Distance to the intersection *)
    (* Define some parameters. We'll condition our model
  on these later. *)
    car_accel_speed : int;
    car_max_speed : int;
    car_min_speed : int;
  };;

(* Our simple car controller - takes the current state of the car
and the streetlight and adjusts the speed. *)
let car_controller (c, l : car_state * light_state) =
  (* Let's define possible commands here. *)
  let steady = { c with car_drive_state = Steady } in
  let brake = { c with car_drive_state = Braking } in
  let accelerate = { c with car_drive_state = Accelerating } in
  (* Now we're going to update the speed based on the current light *)
  match l.light_state with
  | Green -> steady (* If it's green, let's just do what we do. *)
  | Red -> brake
  | Yellow ->
     if not l.blinking && c.car_distance > 10 then
       accelerate
     else
       brake
;;
Out[3]:
type driving_state = Accelerating | Steady | Braking
type car_state = {
  car_drive_state : driving_state;
  car_speed : Z.t;
  car_distance : Z.t;
  car_accel_speed : Z.t;
  car_max_speed : Z.t;
  car_min_speed : Z.t;
}
val car_controller : car_state * light_state -> car_state = <fun>

We can now define our intersection as a struct containing both the car and the stoplight state, and we can then define a one_step function over the state of the intersection, by first updating the state of the stoplight and then letting the car react to this new state of the world:

In [4]:
type intersection = {
    c : car_state;
    l : light_state;
  };;

(* Our car state transition here *)
let car_step (i : intersection) =
  let c = i.c in
  (* Update distance given the current speed *)
  let c = { c with car_distance = c.car_distance + c.car_speed } in
  let c = match c.car_drive_state with
    | Accelerating ->
       let new_speed = c.car_speed + c.car_accel_speed in
       if new_speed > c.car_max_speed then { c with car_speed = c.car_max_speed }
       else { c with car_speed = new_speed }
    | Steady -> c
    | Braking ->
       let new_speed = c.car_speed - c.car_accel_speed in
       if new_speed < 0 then { c with car_speed = 0 }
       else { c with car_speed = new_speed } in
  (* We have our current distance, speed and acceleration. *)
  let c' = car_controller (c, i.l) in
  { i with c = c'}
;;

(* State transitions of our core values... *)
let one_step (i : intersection) =
  let l' = light_step (i.l) in
  car_step ({i with l = l'});;

let valid_car_state (i: intersection) =
  (* let's make sure the car is going in a good speed *)
  i.c.car_speed = 20 &&
    i.c.car_accel_speed = 10 &&
      i.c.car_max_speed = 100 &&
        i.c.car_min_speed = 0;;
Out[4]:
type intersection = { c : car_state; l : light_state; }
val car_step : intersection -> intersection = <fun>
val one_step : intersection -> intersection = <fun>
val valid_car_state : intersection -> bool = <fun>

Let's verify that our model ensures that the car will always brake when approaching a red light:

In [5]:
verify
  (fun i ->
     let i = one_step i in
     valid_car_state i &&
     i.l.light_state = Red
     ==> i.c.car_drive_state = Braking)
;;
Out[5]:
- : intersection -> bool = <fun>
Proved
proof
ground_instances:0
definitions:0
inductions:0
search_time:
0.016s
details:
Expand
smt_stats:
rlimit count:2392
num allocs:6611401
time:0.007000
memory:16.900000
max memory:16.900000
Expand
  • start[0.016s]
      let (_x_0 : car_state) = if ….light_state = Green then … else … in
      (_x_0.car_speed = 20
       && _x_0.car_accel_speed = 10
          && _x_0.car_max_speed = 100 && _x_0.car_min_speed = 0)
      && ….l.light_state = Red ==> _x_0.car_drive_state = Braking
  • simplify

    into:
    let (_x_0 : int) = ….car_distance in
    let (_x_1 : car_state)
        = if not ….blinking && not (_x_0 <= 10) then … else …
    in
    let (_x_2 : int) = ….car_speed in
    let (_x_3 : int) = ….car_accel_speed in
    let (_x_4 : int) = ….car_max_speed in
    let (_x_5 : int) = ….car_min_speed in
    let (_x_6 : light_state) = ( :var_0: ).l in
    let (_x_7 : int) = _x_6.current_time in
    let (_x_8 : color)
        = (if _x_7 <= ((-1) + _x_6.light_change_time)
           then if _x_7 <= ((-1) + _x_6.blink_time) then … else …
           else if _x_6.light_state = Green then … else …).light_state
    in
    let (_x_9 : bool) = _x_8 = Red in
    let (_x_10 : car_state)
        = {car_drive_state = Steady; car_speed = _x_2; car_distance = _x_0;
           car_accel_speed = _x_3; car_max_speed = _x_4; car_min_speed = _x_5}
    in
    let (_x_11 : bool) = _x_8 = Green in
    let (_x_12 : car_state) = if _x_11 then _x_10 else if _x_9 then … else _x_1
    in
    not
    (((((if _x_11 then _x_10
         else
         if _x_9
         then
           {car_drive_state = Braking; car_speed = _x_2; car_distance = _x_0;
            car_accel_speed = _x_3; car_max_speed = _x_4; car_min_speed = _x_5}
         else _x_1).car_speed
        = 20 && _x_12.car_accel_speed = 10)
       && _x_12.car_max_speed = 100)
      && _x_12.car_min_speed = 0)
     && _x_9)
    || _x_12.car_drive_state = Braking
    expansions:
    []
    rewrite_steps:
      forward_chaining:
      • Unsat

      Let's now use Imandra's Principal Region Decomposition to enumerate all the possible distinct regions of behavior of the intersection:

      In [6]:
      #program;;
      let d = Modular_decomp.top ~prune:true ~assuming:"valid_car_state" "one_step";;
      
      Out[6]:
      val d : Modular_decomp_intf.decomp_ref = <abstr>
      
      Regions details

      No group selected.

      • Concrete regions are numbered
      • Unnumbered regions are groups whose children share a particular constraint
      • Click on a region to view its details
      • Double click on a region to zoom in on it
      • Shift+double click to zoom out
      • Hit escape to reset back to the top
      decomp of (one_step i
      Reg_idConstraintsInvariant
      59
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • i.l.blinking
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        (_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_0.car_max_speed;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      58
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_distance + _x_0.car_speed) > 10)
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        (_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_0.car_max_speed;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      57
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • let (_x_0 : car_state) = i.c in (_x_0.car_distance + _x_0.car_speed) > 10
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        (_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Accelerating; car_speed = _x_0.car_max_speed;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      56
      • not (i.l.light_state = Green)
      • i.l.light_state = Red
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        (_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_0.car_max_speed;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      55
      • i.l.light_state = Green
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        (_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Steady; car_speed = _x_0.car_max_speed;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      54
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • i.l.blinking
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with current_time = _x_2.current_time + 1}}
      53
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_distance + _x_0.car_speed) > 10)
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with current_time = _x_2.current_time + 1}}
      52
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • let (_x_0 : car_state) = i.c in (_x_0.car_distance + _x_0.car_speed) > 10
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Accelerating; car_speed = _x_1 + _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with current_time = _x_2.current_time + 1}}
      51
      • not (i.l.light_state = Green)
      • i.l.light_state = Red
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with current_time = _x_2.current_time + 1}}
      50
      • i.l.light_state = Green
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Steady; car_speed = _x_1 + _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with current_time = _x_2.current_time + 1}}
      49
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • i.l.blinking
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      48
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_distance + _x_0.car_speed) > 10)
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      47
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • let (_x_0 : car_state) = i.c in (_x_0.car_distance + _x_0.car_speed) > 10
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Accelerating;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      46
      • not (i.l.light_state = Green)
      • i.l.light_state = Red
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      45
      • i.l.light_state = Green
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Steady; car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      44
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • i.l.blinking
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in (_x_0.car_speed - _x_0.car_accel_speed) < 0
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = 0;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      43
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_distance + _x_0.car_speed) > 10)
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in (_x_0.car_speed - _x_0.car_accel_speed) < 0
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = 0;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      42
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • let (_x_0 : car_state) = i.c in (_x_0.car_distance + _x_0.car_speed) > 10
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in (_x_0.car_speed - _x_0.car_accel_speed) < 0
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Accelerating; car_speed = 0;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      41
      • not (i.l.light_state = Green)
      • i.l.light_state = Red
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in (_x_0.car_speed - _x_0.car_accel_speed) < 0
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = 0;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      40
      • i.l.light_state = Green
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in (_x_0.car_speed - _x_0.car_accel_speed) < 0
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Steady; car_speed = 0;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      39
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • i.l.blinking
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed - _x_0.car_accel_speed) < 0)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with current_time = _x_2.current_time + 1}}
      38
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_distance + _x_0.car_speed) > 10)
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed - _x_0.car_accel_speed) < 0)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with current_time = _x_2.current_time + 1}}
      37
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • let (_x_0 : car_state) = i.c in (_x_0.car_distance + _x_0.car_speed) > 10
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed - _x_0.car_accel_speed) < 0)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Accelerating; car_speed = _x_1 - _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with current_time = _x_2.current_time + 1}}
      36
      • not (i.l.light_state = Green)
      • i.l.light_state = Red
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed - _x_0.car_accel_speed) < 0)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with current_time = _x_2.current_time + 1}}
      35
      • i.l.light_state = Green
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed - _x_0.car_accel_speed) < 0)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.blink_time)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Steady; car_speed = _x_1 - _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with current_time = _x_2.current_time + 1}}
      34
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        (_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
      • not Is_a(Green, i.l.light_state)
      • not Is_a(Red, i.l.light_state)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_0.car_max_speed;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with blinking = true; current_time = _x_1.current_time + 1}}
      33
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
      • not Is_a(Green, i.l.light_state)
      • not Is_a(Red, i.l.light_state)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with blinking = true; current_time = _x_2.current_time + 1}}
      32
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
      • not Is_a(Green, i.l.light_state)
      • not Is_a(Red, i.l.light_state)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with blinking = true; current_time = _x_1.current_time + 1}}
      31
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in (_x_0.car_speed - _x_0.car_accel_speed) < 0
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
      • not Is_a(Green, i.l.light_state)
      • not Is_a(Red, i.l.light_state)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = 0;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with blinking = true; current_time = _x_1.current_time + 1}}
      30
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Red)
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed - _x_0.car_accel_speed) < 0)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
      • not Is_a(Green, i.l.light_state)
      • not Is_a(Red, i.l.light_state)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with blinking = true; current_time = _x_2.current_time + 1}}
      29
      • not (i.l.light_state = Green)
      • i.l.light_state = Red
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        (_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
      • not Is_a(Green, i.l.light_state)
      • Is_a(Red, i.l.light_state)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_0.car_max_speed;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      28
      • not (i.l.light_state = Green)
      • i.l.light_state = Red
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
      • not Is_a(Green, i.l.light_state)
      • Is_a(Red, i.l.light_state)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with current_time = _x_2.current_time + 1}}
      27
      • not (i.l.light_state = Green)
      • i.l.light_state = Red
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
      • not Is_a(Green, i.l.light_state)
      • Is_a(Red, i.l.light_state)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      26
      • not (i.l.light_state = Green)
      • i.l.light_state = Red
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in (_x_0.car_speed - _x_0.car_accel_speed) < 0
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
      • not Is_a(Green, i.l.light_state)
      • Is_a(Red, i.l.light_state)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = 0;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with current_time = _x_1.current_time + 1}}
      25
      • not (i.l.light_state = Green)
      • i.l.light_state = Red
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed - _x_0.car_accel_speed) < 0)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
      • not Is_a(Green, i.l.light_state)
      • Is_a(Red, i.l.light_state)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with current_time = _x_2.current_time + 1}}
      24
      • i.l.light_state = Green
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        (_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
      • Is_a(Green, i.l.light_state)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Steady; car_speed = _x_0.car_max_speed;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with blinking = true; current_time = _x_1.current_time + 1}}
      23
      • i.l.light_state = Green
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
      • Is_a(Green, i.l.light_state)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Steady; car_speed = _x_1 + _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with blinking = true; current_time = _x_2.current_time + 1}}
      22
      • i.l.light_state = Green
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
      • Is_a(Green, i.l.light_state)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Steady; car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with blinking = true; current_time = _x_1.current_time + 1}}
      21
      • i.l.light_state = Green
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in (_x_0.car_speed - _x_0.car_accel_speed) < 0
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
      • Is_a(Green, i.l.light_state)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Steady; car_speed = 0;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l = {_x_1 with blinking = true; current_time = _x_1.current_time + 1}}
      20
      • i.l.light_state = Green
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed - _x_0.car_accel_speed) < 0)
      • let (_x_0 : light_state) = i.l in
        not ((_x_0.current_time + 1) > _x_0.light_change_time)
      • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
      • Is_a(Green, i.l.light_state)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Steady; car_speed = _x_1 - _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l = {_x_2 with blinking = true; current_time = _x_2.current_time + 1}}
      19
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        (_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Yellow)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Steady; car_speed = _x_0.car_max_speed;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l =
       {_x_1 with
       blinking = false; current_time = _x_1.current_time + 1; light_state = Green}}
      18
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed)
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Yellow)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Steady; car_speed = _x_1 + _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l =
       {_x_2 with
       blinking = false; current_time = _x_2.current_time + 1; light_state = Green}}
      17
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Yellow)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Steady; car_distance = _x_0.car_distance + _x_0.car_speed};
       l =
       {_x_1 with
       blinking = false; current_time = _x_1.current_time + 1; light_state = Green}}
      16
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in (_x_0.car_speed - _x_0.car_accel_speed) < 0
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Yellow)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Steady; car_speed = 0;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l =
       {_x_1 with
       blinking = false; current_time = _x_1.current_time + 1; light_state = Green}}
      15
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed - _x_0.car_accel_speed) < 0)
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Yellow)
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Steady; car_speed = _x_1 - _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l =
       {_x_2 with
       blinking = false; current_time = _x_2.current_time + 1; light_state = Green}}
      14
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        (_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • not (i.l.light_state = Green)
      • i.l.light_state = Yellow
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_0.car_max_speed;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l =
       {_x_1 with
       blinking = false; current_time = _x_1.current_time + 1; light_state = Red}}
      13
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed)
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • not (i.l.light_state = Green)
      • i.l.light_state = Yellow
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l =
       {_x_2 with
       blinking = false; current_time = _x_2.current_time + 1; light_state = Red}}
      12
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • not (i.l.light_state = Green)
      • i.l.light_state = Yellow
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
       l =
       {_x_1 with
       blinking = false; current_time = _x_1.current_time + 1; light_state = Red}}
      11
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in (_x_0.car_speed - _x_0.car_accel_speed) < 0
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • not (i.l.light_state = Green)
      • i.l.light_state = Yellow
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = 0;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l =
       {_x_1 with
       blinking = false; current_time = _x_1.current_time + 1; light_state = Red}}
      10
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed - _x_0.car_accel_speed) < 0)
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • not (i.l.light_state = Green)
      • i.l.light_state = Yellow
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l =
       {_x_2 with
       blinking = false; current_time = _x_2.current_time + 1; light_state = Red}}
      9
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_distance + _x_0.car_speed) > 10)
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        (_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • i.l.light_state = Green
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_0.car_max_speed;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l =
       {_x_1 with
       blinking = false; current_time = _x_1.current_time + 1; light_state = Yellow}}
      8
      • let (_x_0 : car_state) = i.c in (_x_0.car_distance + _x_0.car_speed) > 10
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        (_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • i.l.light_state = Green
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Accelerating; car_speed = _x_0.car_max_speed;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l =
       {_x_1 with
       blinking = false; current_time = _x_1.current_time + 1; light_state = Yellow}}
      7
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_distance + _x_0.car_speed) > 10)
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed)
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • i.l.light_state = Green
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l =
       {_x_2 with
       blinking = false; current_time = _x_2.current_time + 1; light_state = Yellow}}
      6
      • let (_x_0 : car_state) = i.c in (_x_0.car_distance + _x_0.car_speed) > 10
      • i.c.car_drive_state = Accelerating
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed)
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • i.l.light_state = Green
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Accelerating; car_speed = _x_1 + _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l =
       {_x_2 with
       blinking = false; current_time = _x_2.current_time + 1; light_state = Yellow}}
      5
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_distance + _x_0.car_speed) > 10)
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • i.l.light_state = Green
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
       l =
       {_x_1 with
       blinking = false; current_time = _x_1.current_time + 1; light_state = Yellow}}
      4
      • let (_x_0 : car_state) = i.c in (_x_0.car_distance + _x_0.car_speed) > 10
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • i.l.light_state = Green
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Accelerating;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l =
       {_x_1 with
       blinking = false; current_time = _x_1.current_time + 1; light_state = Yellow}}
      3
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_distance + _x_0.car_speed) > 10)
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in (_x_0.car_speed - _x_0.car_accel_speed) < 0
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • i.l.light_state = Green
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = 0;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l =
       {_x_1 with
       blinking = false; current_time = _x_1.current_time + 1; light_state = Yellow}}
      2
      • let (_x_0 : car_state) = i.c in (_x_0.car_distance + _x_0.car_speed) > 10
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in (_x_0.car_speed - _x_0.car_accel_speed) < 0
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • i.l.light_state = Green
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Accelerating; car_speed = 0;
       car_distance = _x_0.car_distance + _x_0.car_speed};
       l =
       {_x_1 with
       blinking = false; current_time = _x_1.current_time + 1; light_state = Yellow}}
      1
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_distance + _x_0.car_speed) > 10)
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed - _x_0.car_accel_speed) < 0)
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • i.l.light_state = Green
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l =
       {_x_2 with
       blinking = false; current_time = _x_2.current_time + 1; light_state = Yellow}}
      0
      • let (_x_0 : car_state) = i.c in (_x_0.car_distance + _x_0.car_speed) > 10
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • let (_x_0 : car_state) = i.c in
        not ((_x_0.car_speed - _x_0.car_accel_speed) < 0)
      • let (_x_0 : light_state) = i.l in
        (_x_0.current_time + 1) > _x_0.light_change_time
      • i.l.light_state = Green
      • i.c.car_speed = 20
      • i.c.car_accel_speed = 10
      • i.c.car_max_speed = 100
      • i.c.car_min_speed = 0
      let (_x_0 : car_state) = i.c in
      let (_x_1 : int) = _x_0.car_speed in
      let (_x_2 : light_state) = i.l in
      {c =
       {_x_0 with
       car_drive_state = Accelerating; car_speed = _x_1 - _x_0.car_accel_speed;
       car_distance = _x_0.car_distance + _x_1};
       l =
       {_x_2 with
       blinking = false; current_time = _x_2.current_time + 1; light_state = Yellow}}

      Imandra has computed all the regions of behavior, let's now implement a custom printer using the Imandra-tools library to explore the behavior of the car in plain english:

      In [7]:
      open Imandra_tools;;
      
      open Region_pp_intf
      
      module Custom = struct
      
        type ty = string
      
        type c =
          (* todo: collapse? *)
          | DriveState of driving_state
          | WithinMaxSpeed of bool
          | GoingForwards
          | GoingBackwards
          | CurrentSpeedEnough of bool
          (* todo: collapse? *)
          | LightState of color
          | LightBlinking of bool
          | TimeToBlink
          | TimeToChangeLight
      
        let compare _ _ _ = UnComparable
      
        let map _ = id
      
        let driving_state_string = function
          | Accelerating -> "accelerating"
          | Steady -> "steady"
          | Braking -> "braking"
      
        let light_state_string = function
          | Green -> "green"
          | Yellow -> "yellow"
          | Red -> "red"
      
        let print p ~focus out = function
          | DriveState d -> Format.fprintf out "Car is %s" (driving_state_string d)
          | WithinMaxSpeed b -> Format.fprintf out "Car is %s max speed limits" (if b then "within" else "exceeding")
          | GoingForwards -> Format.fprintf out "Car is moving forwards"
          | GoingBackwards -> Format.fprintf out "Car is moving backwards"
          | LightState l -> Format.fprintf out "Light is %s" (light_state_string l)
          | LightBlinking b -> Format.fprintf out "Light is%s blinking" (if b then "" else "n't")
          | TimeToBlink -> Format.fprintf out "Time to blink"
          | TimeToChangeLight -> Format.fprintf out "Time to change light"
          | CurrentSpeedEnough b -> Format.fprintf out "Car's current speed is%s enough to make it in time"
                                                   (if b then "" else "n't")
      end
      
      module TY = Region_pp.String_conv
      
      module PPrinter = Region_pp.Make (TY) (Custom)
      
      module Refiner = struct
      
        open PPrinter
        open Region_pp
        exception Ignore
      
        let bool_type = TY.translate_imandra_type Type.bool
      
        let refine_invariant (intersection_s : (string * node) list) : node list =
          let open Custom in
          match CCOption.map view (List.assoc "c" intersection_s), CCOption.map view (List.assoc "l" intersection_s) with
          | Some Struct ("car_state", car_state_s), Some Struct ("light_state", light_state_s) ->
             begin
               match List.assoc "car_drive_state" car_state_s,
                     List.assoc "car_speed" car_state_s,
                     List.assoc "blinking" light_state_s,
                     List.assoc "light_state" light_state_s
               with
               | Some {view = (Obj (state, []));ty=obj_ty}, Some ({ty = speed_ty;_} as speed), Some ({ty = blinking_ty;_} as blinking), Some ({ty = light_state_ty;_} as light_state) ->
                  let speed : node = mk ~ty:bool_type (Eq (mk ~ty:speed_ty (Var "car_speed"), speed)) in
                  let blinking : node = mk ~ty:bool_type (Eq (mk ~ty:blinking_ty (Var "blinking"), blinking)) in
                  let light_state : node = mk ~ty:bool_type (Eq (mk ~ty:light_state_ty (Var "light_state"), light_state)) in
                  begin match state with
                  | "Accelerating" -> [mk ~ty:obj_ty (Custom (DriveState Accelerating)); speed; blinking; light_state]
                  | "Steady" -> [mk ~ty:obj_ty (Custom (DriveState Steady)); speed; blinking; light_state]
                  | "Braking" -> [mk ~ty:obj_ty (Custom (DriveState Braking)); speed; blinking; light_state]
                  | _ -> raise Ignore
                  end
               | _ -> raise Ignore
             end
          | _, _ -> raise Ignore
      
        let walk (x : node) : node =
          let open Custom in
          let r_x = match view x with
         | FieldOf (Record, "current_time", {view = FieldOf (Record, "l", {view = Var "i";_});_}) ->
            Ok (Var "Current time")
           | FieldOf (Record, l, {view = FieldOf (Record, "l", {view = Var "i";_});_}) ->
            Ok (Var l)
          | FieldOf (Record, c, {view = FieldOf (Record, "c", {view = Var "i";_});_}) ->
            Ok (Var c)
          | Is (x, _, {view = Var "car_drive_state";_}) ->
             begin match x with
             | "Accelerating" -> Ok  (Custom (DriveState Accelerating))
             | "Steady" -> Ok (Custom (DriveState Steady))
             | "Braking" -> Ok (Custom (DriveState Braking))
             | _ -> Error Ignore
             end
      
          | Eq ({view = Var "light_state";ty}, {view = Obj (x, []);_}) ->
             Ok (Is (x, [], mk ~ty (Var "light_state")))
      
          | Is (x, _, {view = Var "light_state";_}) ->
             begin match x with
             | "Green" -> Ok (Custom (LightState Green))
             | "Yellow" -> Ok (Custom (LightState Yellow))
             | "Red" -> Ok (Custom (LightState Red))
             | _ -> Error Ignore
             end
      
          | Minus ({view = Var "light_change_time";_}, {view = Int 1;_}) ->
             Ok (Custom TimeToChangeLight)
      
          | Minus ({view = Var "blink_time";_}, {view = Int 1;_}) ->
             Ok (Custom TimeToBlink)
      
          | Var "blinking" ->
             Ok (Custom (LightBlinking true))
      
          | Not ({view = Custom (LightBlinking true);_}) ->
             Ok (Custom (LightBlinking false))
      
          | Geq ({view = Var "car_max_speed";_}, {view = Plus ({view = Var "car_speed";_}, {view = Var "car_accel_speed";_});_})
            -> Ok (Custom (WithinMaxSpeed true))
      
          | Gt ({view = Plus ({view = Var "car_speed";_}, {view = Var "car_accel_speed";_});_}, {view = Var "car_max_speed";_})
            -> Ok (Custom (WithinMaxSpeed false))
      
          | Geq ({view = Minus ({view = Var "car_speed";_}, {view = Var "car_accel_speed";_});_}, {view = Int 0;_})
            -> Ok (Custom GoingForwards)
      
          | Gt ({view = Int 0;_}, {view = Minus ({view = Var "car_speed";_}, {view = Var "car_accel_speed";_});_})
            -> Ok (Custom GoingBackwards)
      
          (* 10 is currently hard coded in the model *)
          | Geq ({view = Int 10;_}, {view = Plus ({view = Var "car_distance";_}, {view = Var "car_speed";_});_})
            -> Ok (Custom (CurrentSpeedEnough false))
      
          | Gt ({view = Plus ({view = Var "car_distance";_}, {view = Var "car_speed";_});_}, {view = Int 10;_})
            -> Ok (Custom (CurrentSpeedEnough true))
          | x -> Ok x
          in match r_x with
          | Ok node_view -> mk ~ty:x.ty node_view
          | Error e -> raise e
      
        let rec refine (node : node) =
          try
            match view node with
            | Eq ({view = Var "F";_}, {view = Struct ("intersection", intersection);_})
              -> refine_invariant intersection |> List.flat_map refine
            | _ ->
               [XF.walk_fix walk node]
          with Ignore ->
            []
      end;;
      
      let pp_cs ?inv cs =
       cs
       |> PPrinter.pp ~refine:Refiner.refine ?inv
       |> List.map (CCFormat.to_string (PPrinter.Printer.print ()))
      
      let regions_doc d =
       Jupyter_imandra.Decompose_render.regions_doc ~pp_cs d;;
      
      #install_doc regions_doc;;
      
      Out[7]:
                                                                                                                                                                                                                                                                                                                                        
      module Custom :
        sig
          type ty =
              string
          type c =
              DriveState of
                driving_state
            | WithinMaxSpeed of
                bool
            | GoingForwards
            | GoingBackwards
            | CurrentSpeedEnough of
                bool
            | LightState of
                color
            | LightBlinking of
                bool
            | TimeToBlink
            | TimeToChangeLight
          val compare :
            'a ->
            'b ->
            'c ->
            comparison
          val map :
            'a ->
            'b ->
            'b
          val driving_state_string :
            driving_state ->
            ty
          val light_state_string :
            color ->
            ty
          val print :
            'a ->
            focus:'b ->
            Format.formatter ->
            c ->
            unit
        end
      module TY = Imandra_tools.Region_pp.String_conv
      module PPrinter :
        sig
          type custom = Custom.c
          type ty = string
          module TY :
            sig
              type ty = string
              val translate_imandra_type : Type.t -> ty
              val mk_tuple : ty list -> ty
              val mk_list : ty -> ty
              val mk_func : ty list -> ty
              val type_var : ty -> ty
              val mk_set : ty -> ty
            end
          type nonrec node = (ty, custom) node
          type nonrec view = (ty, custom) view
          val view : node -> view
          val ty : node -> ty
          val mk : ty:ty -> view -> node
          module XF :
            sig
              val map : (node -> node) -> node -> node
              val walk : pre:(node -> node) -> ?post:(node -> node) -> node -> node
              val fix_ : ?bound:int -> ('a -> 'a) -> 'a -> 'a -> 'a
              val fix : ?bound:int -> ('a -> 'a) -> 'a -> 'a
              val walk_fix : ?bound:int -> (node -> node) -> node -> node
              val iterated : unit -> 'a
              val iter : f:(node -> unit) -> node -> unit
              val exists : f:(node -> bool) -> node -> bool
            end
          val vars : node -> ty list
          val has_symbolic_term : node -> bool
          module Printer :
            sig
              val print :
                ?p:(node CCFormat.printer ->
                    Format.formatter -> node -> unit option) ->
                ?focus:ty -> unit -> node CCFormat.printer
              val to_string :
                ?p:(node CCFormat.printer ->
                    Format.formatter -> node -> unit option) ->
                ?focus:ty -> node -> ty
            end
          module Comparator :
            sig
              val is_eq : comparison -> bool
              val compare : node -> node -> comparison
              val compare_all : node list -> node list -> comparison
            end
          module Simplifier : sig val simplify : node -> node end
          module Unifier :
            sig
              type unifier = node -> node -> node option
              val unify : ?unify:unifier -> node list -> node list
            end
          module Parser : sig val parse : Term.term -> node option end
          module Compactor : sig val compact : node list -> node list end
          type refiner = node -> node list
          type pprinter =
              ?unify:Unifier.unifier ->
              ?refine:refiner -> ?inv:bool -> Term.term list -> node list
          val pp : pprinter
          val print :
            ?pp:pprinter ->
            ?unify:Unifier.unifier ->
            ?refine:refiner ->
            ?print:(node CCFormat.printer ->
                    Format.formatter -> node -> unit option) ->
            ?skip_invariant:bool ->
            ?focus:ty ->
            unit -> Format.formatter -> Top_result.modular_region -> unit
          val to_string :
            ?unify:Unifier.unifier ->
            ?refine:refiner -> Top_result.modular_region -> ty
        end
      module Refiner :
        sig
          exception Ignore
          val bool_type : string
          val refine_invariant :
            (string * PPrinter.node) list -> PPrinter.node list
          val walk : PPrinter.node -> PPrinter.node
          val refine : PPrinter.node -> PPrinter.node list
        end
      val pp_cs : ?inv:bool -> Term.term list -> string list = <fun>
      val regions_doc : Modular_decomposition.concrete -> Document.t = <fun>
      
      In [8]:
      d;;
      
      Out[8]:
      - : Modular_decomp_intf.decomp_ref = <abstr>