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 : int;
  blink_time : int;
  light_change_time : int;
  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 : int;
  car_distance : int;
  car_accel_speed : int;
  car_max_speed : int;
  car_min_speed : int;
}
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_instances0
definitions0
inductions0
search_time
0.052s
details
Expand
smt_stats
rlimit count1317
mk bool var1
num allocs861978215
memory21.040000
max memory21.040000
Expand
  • start[0.052s]
      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:

      In [6]:
      #program;;
      let d = Modular_decomp.top ~prune:true ~assuming:"valid_car_state" "one_step";;
      
      Out[6]:
      val d : Modular_decomposition.t =
        {Imandra_interactive.Modular_decomp.MD.md_session = 1i;
         md_f =
          {Imandra_surface.Uid.name = "one_step"; id = <abstr>;
           special_tag = <abstr>; namespace = <abstr>;
           chash = Some LPN7vylOZ5CZwUBtlNQtB0fMjzjrUxJLninf2E3226I;
           depth = (5i, 4i)};
         md_args = [(i : intersection)]; md_regions = <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
      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}}
      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}}
      33
      • 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 (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 current_time = _x_2.current_time + 1}}
      32
      • 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 (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 current_time = _x_1.current_time + 1}}
      30
      • 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 (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 current_time = _x_2.current_time + 1}}
      28
      • 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
      • 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 = true; current_time = _x_2.current_time + 1}}
      27
      • 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
      • 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 = true; current_time = _x_1.current_time + 1}}
      25
      • 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
      • 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 = true; current_time = _x_2.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
      • 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
      • 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}}
      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
      • 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}}
      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}}
      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}}
      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}}
      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}}
      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}}
      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;;
      
      module Custom = struct
        open Region_pp_intf
        type t =
          (* 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 PPrinter = Region_pp.Make(Custom);;
      
      module Refiner = struct
      
        open PPrinter
        exception Ignore
      
        let refine_invariant (intersection_s : (string * node) list) : node list=
          match List.assoc "c" intersection_s, 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 (Obj (state, [])), Some speed, Some blinking, Some light_state ->
                  let speed : node = Eq (Var "car_speed", speed) in
                  let blinking : node = Eq (Var "blinking", blinking) in
                  let light_state : node = Eq (Var "light_state", light_state) in
                  begin match state with
                  | "Accelerating" -> [Custom (DriveState Accelerating); speed; blinking; light_state]
                  | "Steady" -> [Custom (DriveState Steady); speed; blinking; light_state]
                  | "Braking" -> [Custom (DriveState Braking); speed; blinking; light_state]
                  | _ -> raise Ignore
                  end
               | _ -> raise Ignore
             end
          | _, _ -> raise Ignore
      
        let walk (x : node) : node = match x with
      
          | FieldOf (Assoc, "current_time", FieldOf (Assoc, "l", Var "i")) -> Var "Current time"
          | FieldOf (Assoc, l, FieldOf (Assoc, "l", Var "i")) -> Var l
          | FieldOf (Assoc, c, FieldOf (Assoc, "c", Var "i")) -> Var c
      
          | Is (x, _, Var "car_drive_state") ->
             begin match x with
             | "Accelerating" -> Custom (DriveState Accelerating)
             | "Steady" -> Custom (DriveState Steady)
             | "Braking" -> Custom (DriveState Braking)
             | _ -> raise Ignore
             end
      
          | Eq (Var "light_state", Obj (x, [])) ->
             Is (x, [], Var "light_state")
      
          | Is (x, _, Var "light_state") ->
             begin match x with
             | "Green" -> Custom (LightState Green)
             | "Yellow" -> Custom (LightState Yellow)
             | "Red" -> Custom (LightState Red)
             | _ -> raise Ignore
             end
      
          | Minus (Var "light_change_time", Int 1) ->
             Custom TimeToChangeLight
      
          | Minus (Var "blink_time", Int 1) ->
             Custom TimeToBlink
      
          | Var "blinking" ->
             Custom (LightBlinking true)
      
          | Not (Custom (LightBlinking true)) ->
             Custom (LightBlinking false)
      
          | Geq (Var "car_max_speed", Plus (Var "car_speed", Var "car_accel_speed"))
            -> Custom (WithinMaxSpeed true)
      
          | Gt (Plus (Var "car_speed", Var "car_accel_speed"), Var "car_max_speed")
            -> Custom (WithinMaxSpeed false)
      
          | Geq (Minus (Var "car_speed", Var "car_accel_speed"), Int 0)
            -> Custom GoingForwards
      
          | Gt (Int 0, Minus (Var "car_speed", Var "car_accel_speed"))
            -> Custom GoingBackwards
      
          (* 10 is currently hard coded in the model *)
          | Geq (Int 10, Plus (Var "car_distance", Var "car_speed"))
            -> Custom (CurrentSpeedEnough false)
      
          | Gt (Plus (Var "car_distance", Var "car_speed"), Int 10)
            -> Custom (CurrentSpeedEnough true)
      
          | x -> x
      
        let rec refine (node : node) =
          try
            match node with
            | Eq (Var "F", Struct ("intersection", intersection))
              -> refine_invariant intersection |> List.flat_map refine
            | node ->
               [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 : Modular_decomposition.t) =
       Jupyter_imandra.Decompose_render.regions_doc ~pp_cs d;;
      
      #install_doc regions_doc;;
      
      Out[7]:
                                                                                                                                                                                        module Custom :
        sig
          type t =
              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 -> Region_pp_intf.comparison
          val map : 'a -> 'b -> 'b
          val driving_state_string : driving_state -> string
          val light_state_string : color -> string
          val print : 'a -> focus:'b -> Format.formatter -> t -> unit
        end
      module PPrinter :
        sig
          type custom = PPrinter.custom
          type node = custom Region_pp_intf.node_
          module XF :
            sig
              val map : (node -> node) -> node -> node
              val walk : pre:(node -> node) -> ?post:(node -> node) -> node -> node
              val fix_ : ?bound:int/2 -> ('a -> 'a) -> 'a -> 'a -> 'a
              val fix : ?bound:int/2 -> ('a -> 'a) -> 'a -> 'a
              val walk_fix : ?bound:int/2 -> (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 -> string list
          val has_symbolic_term : node -> bool
          module Printer :
            sig
              val print :
                ?p:(node CCFormat.printer ->
                    Format.formatter -> node -> unit option) ->
                ?focus:string -> unit -> node CCFormat.printer
              val to_string :
                ?p:(node CCFormat.printer ->
                    Format.formatter -> node -> unit option) ->
                ?focus:string -> node -> string
            end
          module Comparator :
            sig
              val is_eq : Region_pp_intf.comparison -> bool
              val compare : node -> node -> Region_pp_intf.comparison
              val compare_all : node list -> node list -> Region_pp_intf.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:string -> unit -> Format.formatter -> Modular_region.t -> unit
          val to_string :
            ?unify:Unifier.unifier -> ?refine:refiner -> Modular_region.t -> string
        end
      module Refiner :
        sig
          exception Ignore
          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.t -> Document.t = <fun>
      
      In [8]:
      d;;
      
      Out[8]:
      - : Top_result.modular_decomposition =
                                                                                                                                                                                                          <document>
      
      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