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:

Try this!
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:

Try this!
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:

Try this!
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:

Try this!
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:

Try this!
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.022s
details:
Expand
smt_stats:
rlimit count:2392
num allocs:6614507
time:0.008000
memory:16.880000
max memory:16.880000
Expand
  • start[0.022s]
  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_speed in
let (_x_1 : int) = ….car_distance in
let (_x_2 : int) = ….car_accel_speed in
let (_x_3 : int) = ….car_max_speed in
let (_x_4 : int) = ….car_min_speed in
let (_x_5 : car_state)
    = {car_drive_state = Braking; car_speed = _x_0; car_distance = _x_1;
       car_accel_speed = _x_2; car_max_speed = _x_3; car_min_speed = _x_4}
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)
    = if _x_8 = Green
      then
        {car_drive_state = Steady; car_speed = _x_0; car_distance = _x_1;
         car_accel_speed = _x_2; car_max_speed = _x_3; car_min_speed = _x_4}
      else
      if _x_9 then _x_5
      else if not ….blinking && not (_x_1 <= 10) then … else _x_5
in
not
((_x_10.car_speed = 20) && (_x_10.car_accel_speed = 10)
 && (_x_10.car_max_speed = 100) && (_x_10.car_min_speed = 0) && _x_9)
|| (_x_10.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:

      Try this!
      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:

      Try this!
      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 show : ty -> ty
        val equal : ty -> ty -> bool
        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
        val propagate : node list -> node list
      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>
      Try this!
      In [8]:
      d;;
      Out[8]:
      - : Modular_decomp_intf.decomp_ref = <abstr>