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.025s
details
Expand
smt_stats
num checks1
rlimit count2235
mk clause50
mk bool var191
datatype splits23
decisions2
propagations8
conflicts2
datatype accessor ax25
datatype constructor ax8
num allocs3186636
added eqs137
del clause16
memory7.370000
max memory7.910000
Expand
  • start[0.025s]
      ((if ….light_state = Green then … else …).car_speed = 20
       && (if ….light_state = Green then … else …).car_accel_speed = 10
          && (if ….light_state = Green then … else …).car_max_speed = 100
             && (if ….light_state = Green then … else …).car_min_speed = 0)
      && ….l.light_state = Red
      ==> (if ….light_state = Green then … else …).car_drive_state =
          Braking
  • simplify

    into
    not
    (((((if (if :var_0:.l.current_time <= (-1 + :var_0:.l.light_change_time)
             then
               if :var_0:.l.current_time <= (-1 + :var_0:.l.blink_time) then …
               else …
             else if :var_0:.l.light_state = Green then … else …).light_state
            = Green
         then
           {car_drive_state = Steady; car_speed = ….car_speed;
            car_distance = ….car_distance;
            car_accel_speed = ….car_accel_speed;
            car_max_speed = ….car_max_speed; car_min_speed = ….car_min_speed}
         else
         if (if :var_0:.l.current_time <= (-1 + :var_0:.l.light_change_time)
             then
               if :var_0:.l.current_time <= (-1 + :var_0:.l.blink_time) then …
               else …
             else if :var_0:.l.light_state = Green then … else …).light_state
            = Red
         then
           {car_drive_state = …; car_speed = ….car_speed;
            car_distance = ….car_distance;
            car_accel_speed = ….car_accel_speed;
            car_max_speed = ….car_max_speed; car_min_speed = ….car_min_speed}
         else
         if not ….blinking && not (….car_distance <= 10) then …
         else
           {car_drive_state = …; car_speed = ….car_speed;
            car_distance = ….car_distance;
            car_accel_speed = ….car_accel_speed;
            car_max_speed = ….car_max_speed; car_min_speed = ….car_min_speed}).car_speed
        = 20
        && (if (if :var_0:.l.current_time <= (-1 + :var_0:.l.light_change_time)
                then
                  if :var_0:.l.current_time <= (-1 + :var_0:.l.blink_time)
                  then … else …
                else if :var_0:.l.light_state = Green then … else …).light_state
               = Green
            then
              {car_drive_state = Steady; car_speed = ….car_speed;
               car_distance = ….car_distance;
               car_accel_speed = ….car_accel_speed;
               car_max_speed = ….car_max_speed;
               car_min_speed = ….car_min_speed}
            else
            if (if :var_0:.l.current_time <= (-1 + :var_0:.l.light_change_time)
                then
                  if :var_0:.l.current_time <= (-1 + :var_0:.l.blink_time)
                  then … else …
                else if :var_0:.l.light_state = Green then … else …).light_state
               = Red
            then
              {car_drive_state = …; car_speed = ….car_speed;
               car_distance = ….car_distance;
               car_accel_speed = ….car_accel_speed;
               car_max_speed = ….car_max_speed;
               car_min_speed = ….car_min_speed}
            else
            if not ….blinking && not (….car_distance <= 10) then …
            else
              {car_drive_state = …; car_speed = ….car_speed;
               car_distance = ….car_distance;
               car_accel_speed = ….car_accel_speed;
               car_max_speed = ….car_max_speed;
               car_min_speed = ….car_min_speed}).car_accel_speed
           = 10)
       && (if (if :var_0:.l.current_time <= (-1 + :var_0:.l.light_change_time)
               then
                 if :var_0:.l.current_time <= (-1 + :var_0:.l.blink_time)
                 then … else …
               else if :var_0:.l.light_state = Green then … else …).light_state
              = Green
           then
             {car_drive_state = Steady; car_speed = ….car_speed;
              car_distance = ….car_distance;
              car_accel_speed = ….car_accel_speed;
              car_max_speed = ….car_max_speed;
              car_min_speed = ….car_min_speed}
           else
           if (if :var_0:.l.current_time <= (-1 + :var_0:.l.light_change_time)
               then
                 if :var_0:.l.current_time <= (-1 + :var_0:.l.blink_time)
                 then … else …
               else if :var_0:.l.light_state = Green then … else …).light_state
              = Red
           then
             {car_drive_state = …; car_speed = ….car_speed;
              car_distance = ….car_distance;
              car_accel_speed = ….car_accel_speed;
              car_max_speed = ….car_max_speed;
              car_min_speed = ….car_min_speed}
           else
           if not ….blinking && not (….car_distance <= 10) then …
           else
             {car_drive_state = …; car_speed = ….car_speed;
              car_distance = ….car_distance;
              car_accel_speed = ….car_accel_speed;
              car_max_speed = ….car_max_speed;
              car_min_speed = ….car_min_speed}).car_max_speed
          = 100)
      && (if (if :var_0:.l.current_time <= (-1 + :var_0:.l.light_change_time)
              then
                if :var_0:.l.current_time <= (-1 + :var_0:.l.blink_time) 
                then … else …
              else if :var_0:.l.light_state = Green then … else …).light_state
             = Green
          then
            {car_drive_state = Steady; car_speed = ….car_speed;
             car_distance = ….car_distance;
             car_accel_speed = ….car_accel_speed;
             car_max_speed = ….car_max_speed; car_min_speed = ….car_min_speed}
          else
          if (if :var_0:.l.current_time <= (-1 + :var_0:.l.light_change_time)
              then
                if :var_0:.l.current_time <= (-1 + :var_0:.l.blink_time) 
                then … else …
              else if :var_0:.l.light_state = Green then … else …).light_state
             = Red
          then
            {car_drive_state = …; car_speed = ….car_speed;
             car_distance = ….car_distance;
             car_accel_speed = ….car_accel_speed;
             car_max_speed = ….car_max_speed; car_min_speed = ….car_min_speed}
          else
          if not ….blinking && not (….car_distance <= 10) then …
          else
            {car_drive_state = …; car_speed = ….car_speed;
             car_distance = ….car_distance;
             car_accel_speed = ….car_accel_speed;
             car_max_speed = ….car_max_speed; car_min_speed = ….car_min_speed}).car_min_speed
         = 0)
     && (if :var_0:.l.current_time <= (-1 + :var_0:.l.light_change_time)
         then
           if :var_0:.l.current_time <= (-1 + :var_0:.l.blink_time) then …
           else …
         else if :var_0:.l.light_state = Green then … else …).light_state
        = Red)
    || (if (if :var_0:.l.current_time <= (-1 + :var_0:.l.light_change_time)
            then
              if :var_0:.l.current_time <= (-1 + :var_0:.l.blink_time) then …
              else …
            else if :var_0:.l.light_state = Green then … else …).light_state
           = Green
        then
          {car_drive_state = Steady; car_speed = ….car_speed;
           car_distance = ….car_distance;
           car_accel_speed = ….car_accel_speed;
           car_max_speed = ….car_max_speed; car_min_speed = ….car_min_speed}
        else …).car_drive_state
       = …
    expansions
    []
    rewrite_steps
      forward_chaining
      • unsat

        (let ((a!1 (<= (current_time_20 (l_48 i_62))
                       (+ (- 1) (light_change_time_22 (l_48 i_6…

      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 regions = Decompose.top ~assuming:"valid_car_state" "one_step";;
      
      Out[6]:
      val regions : Imandra_interactive.Decompose.t list =
        [<region>; <region>; <region>; <region>; <region>; <region>; <region>;
         <region>; <region>; <region>; <region>; <region>; <region>; <region>;
         <region>; <region>; <region>; <region>; <region>; <region>; <region>;
         <region>; <region>; <region>; <region>; <region>; <region>; <region>;
         <region>; <region>; <region>; <region>; <region>; <region>; <region>;
         <region>]
      
      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
      ConstraintsInvariant
      • not (i.l.current_time <= (-1 + i.l.light_change_time))
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Yellow)
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • 0 <= (i.c.car_speed + -1 * i.c.car_accel_speed)
      {c =
       {car_drive_state = Steady;
        car_speed = i.c.car_speed + -1 * i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = false; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = Green}}
      • not (i.l.current_time <= (-1 + i.l.light_change_time))
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Yellow)
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      {c =
       {car_drive_state = Steady; car_speed = i.c.car_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = false; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = Green}}
      • not (i.l.current_time <= (-1 + i.l.light_change_time))
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Yellow)
      • i.c.car_drive_state = Accelerating
      • (i.c.car_speed + i.c.car_accel_speed) <= i.c.car_max_speed
      {c =
       {car_drive_state = Steady; car_speed = i.c.car_speed + i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = false; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = Green}}
      • not (i.l.current_time <= (-1 + i.l.light_change_time))
      • not (i.l.light_state = Green)
      • i.l.light_state = Yellow
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • 0 <= (i.c.car_speed + -1 * i.c.car_accel_speed)
      {c =
       {car_drive_state = Braking;
        car_speed = i.c.car_speed + -1 * i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = false; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = Red}}
      • not (i.l.current_time <= (-1 + i.l.light_change_time))
      • not (i.l.light_state = Green)
      • i.l.light_state = Yellow
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      {c =
       {car_drive_state = Braking; car_speed = i.c.car_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = false; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = Red}}
      • not (i.l.current_time <= (-1 + i.l.light_change_time))
      • not (i.l.light_state = Green)
      • i.l.light_state = Yellow
      • i.c.car_drive_state = Accelerating
      • (i.c.car_speed + i.c.car_accel_speed) <= i.c.car_max_speed
      {c =
       {car_drive_state = Braking; car_speed = i.c.car_speed + i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = false; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = Red}}
      • not (i.l.current_time <= (-1 + i.l.light_change_time))
      • i.l.light_state = Green
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • 0 <= (i.c.car_speed + -1 * i.c.car_accel_speed)
      • (i.c.car_distance + i.c.car_speed) <= 10
      {c =
       {car_drive_state = Braking;
        car_speed = i.c.car_speed + -1 * i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = false; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = Yellow}}
      • not (i.l.current_time <= (-1 + i.l.light_change_time))
      • i.l.light_state = Green
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • 0 <= (i.c.car_speed + -1 * i.c.car_accel_speed)
      • not ((i.c.car_distance + i.c.car_speed) <= 10)
      {c =
       {car_drive_state = Accelerating;
        car_speed = i.c.car_speed + -1 * i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = false; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = Yellow}}
      • not (i.l.current_time <= (-1 + i.l.light_change_time))
      • i.l.light_state = Green
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • (i.c.car_distance + i.c.car_speed) <= 10
      {c =
       {car_drive_state = Braking; car_speed = i.c.car_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = false; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = Yellow}}
      • not (i.l.current_time <= (-1 + i.l.light_change_time))
      • i.l.light_state = Green
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • not ((i.c.car_distance + i.c.car_speed) <= 10)
      {c =
       {car_drive_state = Accelerating; car_speed = i.c.car_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = false; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = Yellow}}
      • not (i.l.current_time <= (-1 + i.l.light_change_time))
      • i.l.light_state = Green
      • i.c.car_drive_state = Accelerating
      • (i.c.car_speed + i.c.car_accel_speed) <= i.c.car_max_speed
      • (i.c.car_distance + i.c.car_speed) <= 10
      {c =
       {car_drive_state = Braking; car_speed = i.c.car_speed + i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = false; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = Yellow}}
      • not (i.l.current_time <= (-1 + i.l.light_change_time))
      • i.l.light_state = Green
      • i.c.car_drive_state = Accelerating
      • (i.c.car_speed + i.c.car_accel_speed) <= i.c.car_max_speed
      • not ((i.c.car_distance + i.c.car_speed) <= 10)
      {c =
       {car_drive_state = Accelerating;
        car_speed = i.c.car_speed + i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = false; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = Yellow}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • not (i.l.current_time <= (-1 + i.l.blink_time))
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Yellow)
      • i.l.light_state = Red
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • 0 <= (i.c.car_speed + -1 * i.c.car_accel_speed)
      {c =
       {car_drive_state = Braking;
        car_speed = i.c.car_speed + -1 * i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • not (i.l.current_time <= (-1 + i.l.blink_time))
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Yellow)
      • i.l.light_state = Red
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      {c =
       {car_drive_state = Braking; car_speed = i.c.car_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • not (i.l.current_time <= (-1 + i.l.blink_time))
      • not (i.l.light_state = Green)
      • not (i.l.light_state = Yellow)
      • i.l.light_state = Red
      • i.c.car_drive_state = Accelerating
      • (i.c.car_speed + i.c.car_accel_speed) <= i.c.car_max_speed
      {c =
       {car_drive_state = Braking; car_speed = i.c.car_speed + i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • not (i.l.current_time <= (-1 + i.l.blink_time))
      • not (i.l.light_state = Green)
      • i.l.light_state = Yellow
      • not (i.l.light_state = Red)
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • 0 <= (i.c.car_speed + -1 * i.c.car_accel_speed)
      {c =
       {car_drive_state = Braking;
        car_speed = i.c.car_speed + -1 * i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = true; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • not (i.l.current_time <= (-1 + i.l.blink_time))
      • not (i.l.light_state = Green)
      • i.l.light_state = Yellow
      • not (i.l.light_state = Red)
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      {c =
       {car_drive_state = Braking; car_speed = i.c.car_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = true; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • not (i.l.current_time <= (-1 + i.l.blink_time))
      • not (i.l.light_state = Green)
      • i.l.light_state = Yellow
      • not (i.l.light_state = Red)
      • i.c.car_drive_state = Accelerating
      • (i.c.car_speed + i.c.car_accel_speed) <= i.c.car_max_speed
      {c =
       {car_drive_state = Braking; car_speed = i.c.car_speed + i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = true; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • i.l.current_time <= (-1 + i.l.blink_time)
      • not (i.l.light_state = Red)
      • i.l.blinking
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • 0 <= (i.c.car_speed + -1 * i.c.car_accel_speed)
      {c =
       {car_drive_state = Braking;
        car_speed = i.c.car_speed + -1 * i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • i.l.current_time <= (-1 + i.l.blink_time)
      • not (i.l.light_state = Red)
      • i.l.blinking
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      {c =
       {car_drive_state = Braking; car_speed = i.c.car_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • i.l.current_time <= (-1 + i.l.blink_time)
      • not (i.l.light_state = Red)
      • i.l.blinking
      • i.c.car_drive_state = Accelerating
      • (i.c.car_speed + i.c.car_accel_speed) <= i.c.car_max_speed
      {c =
       {car_drive_state = Braking; car_speed = i.c.car_speed + i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • i.l.current_time <= (-1 + i.l.blink_time)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • 0 <= (i.c.car_speed + -1 * i.c.car_accel_speed)
      • (i.c.car_distance + i.c.car_speed) <= 10
      {c =
       {car_drive_state = Braking;
        car_speed = i.c.car_speed + -1 * i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • i.l.current_time <= (-1 + i.l.blink_time)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • 0 <= (i.c.car_speed + -1 * i.c.car_accel_speed)
      • not ((i.c.car_distance + i.c.car_speed) <= 10)
      {c =
       {car_drive_state = Accelerating;
        car_speed = i.c.car_speed + -1 * i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • i.l.current_time <= (-1 + i.l.blink_time)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • (i.c.car_distance + i.c.car_speed) <= 10
      {c =
       {car_drive_state = Braking; car_speed = i.c.car_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • i.l.current_time <= (-1 + i.l.blink_time)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • not ((i.c.car_distance + i.c.car_speed) <= 10)
      {c =
       {car_drive_state = Accelerating; car_speed = i.c.car_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • i.l.current_time <= (-1 + i.l.blink_time)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • i.c.car_drive_state = Accelerating
      • (i.c.car_speed + i.c.car_accel_speed) <= i.c.car_max_speed
      • (i.c.car_distance + i.c.car_speed) <= 10
      {c =
       {car_drive_state = Braking; car_speed = i.c.car_speed + i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • i.l.current_time <= (-1 + i.l.blink_time)
      • not (i.l.light_state = Red)
      • not i.l.blinking
      • i.c.car_drive_state = Accelerating
      • (i.c.car_speed + i.c.car_accel_speed) <= i.c.car_max_speed
      • not ((i.c.car_distance + i.c.car_speed) <= 10)
      {c =
       {car_drive_state = Accelerating;
        car_speed = i.c.car_speed + i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • i.l.current_time <= (-1 + i.l.blink_time)
      • i.l.light_state = Red
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • 0 <= (i.c.car_speed + -1 * i.c.car_accel_speed)
      {c =
       {car_drive_state = Braking;
        car_speed = i.c.car_speed + -1 * i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • i.l.current_time <= (-1 + i.l.blink_time)
      • i.l.light_state = Red
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      {c =
       {car_drive_state = Braking; car_speed = i.c.car_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • not (i.l.light_state = Green)
      • i.l.current_time <= (-1 + i.l.blink_time)
      • i.l.light_state = Red
      • i.c.car_drive_state = Accelerating
      • (i.c.car_speed + i.c.car_accel_speed) <= i.c.car_max_speed
      {c =
       {car_drive_state = Braking; car_speed = i.c.car_speed + i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • i.l.light_state = Green
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • 0 <= (i.c.car_speed + -1 * i.c.car_accel_speed)
      • not (i.l.current_time <= (-1 + i.l.blink_time))
      • i.l.light_state = Green
      {c =
       {car_drive_state = Steady;
        car_speed = i.c.car_speed + -1 * i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = true; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • i.l.light_state = Green
      • not (i.c.car_drive_state = Accelerating)
      • not (i.c.car_drive_state = Steady)
      • 0 <= (i.c.car_speed + -1 * i.c.car_accel_speed)
      • i.l.current_time <= (-1 + i.l.blink_time)
      {c =
       {car_drive_state = Steady;
        car_speed = i.c.car_speed + -1 * i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • i.l.light_state = Green
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • not (i.l.current_time <= (-1 + i.l.blink_time))
      • i.l.light_state = Green
      {c =
       {car_drive_state = Steady; car_speed = i.c.car_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = true; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • i.l.light_state = Green
      • not (i.c.car_drive_state = Accelerating)
      • i.c.car_drive_state = Steady
      • i.l.current_time <= (-1 + i.l.blink_time)
      {c =
       {car_drive_state = Steady; car_speed = i.c.car_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • i.l.light_state = Green
      • i.c.car_drive_state = Accelerating
      • (i.c.car_speed + i.c.car_accel_speed) <= i.c.car_max_speed
      • not (i.l.current_time <= (-1 + i.l.blink_time))
      • i.l.light_state = Green
      {c =
       {car_drive_state = Steady; car_speed = i.c.car_speed + i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = true; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}
      • i.l.current_time <= (-1 + i.l.light_change_time)
      • i.l.light_state = Green
      • i.c.car_drive_state = Accelerating
      • (i.c.car_speed + i.c.car_accel_speed) <= i.c.car_max_speed
      • i.l.current_time <= (-1 + i.l.blink_time)
      {c =
       {car_drive_state = Steady; car_speed = i.c.car_speed + i.c.car_accel_speed;
        car_distance = i.c.car_distance + i.c.car_speed;
        car_accel_speed = i.c.car_accel_speed; car_max_speed = i.c.car_max_speed;
        car_min_speed = i.c.car_min_speed};
       l =
       {blinking = i.l.blinking; current_time = 1 + i.l.current_time;
        blink_time = i.l.blink_time; light_change_time = i.l.light_change_time;
        light_state = i.l.light_state}}

      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 (regions : Decompose.t list) =
       Jupyter_imandra.Decompose_render.regions_doc ~pp_cs regions;;
      
      #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 ->
            Imandra_tools.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 = Custom.t
          type node = custom Imandra_tools.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 -> ('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 -> Imandra_tools.Region_pp_intf.var_name list
          val has_symbolic_term : node -> bool
          module Printer :
            sig
              val print :
                ?p:(node CCFormat.printer ->
                    CCFormat.formatter -> node -> unit option) ->
                ?focus:Imandra_tools.Region_pp_intf.var_name ->
                unit -> node CCFormat.printer
              val to_string :
                ?p:(node CCFormat.printer ->
                    CCFormat.formatter -> node -> unit option) ->
                ?focus:Imandra_tools.Region_pp_intf.var_name -> node -> string
            end
          module Comparator :
            sig
              val is_eq : Imandra_tools.Region_pp_intf.comparison -> bool
              val compare : node -> node -> Imandra_tools.Region_pp_intf.comparison
              val compare_all :
                node list -> node list -> Imandra_tools.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 : Imandra_surface.Term.t -> 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 -> Imandra_surface.Term.t list -> node list
          val pp : pprinter
          val print :
            ?pp:pprinter ->
            ?unify:Unifier.unifier ->
            ?refine:refiner ->
            ?print:(node CCFormat.printer ->
                    CCFormat.formatter -> node -> unit option) ->
            ?skip_invariant:bool ->
            ?focus:Imandra_tools.Region_pp_intf.var_name ->
            unit ->
            Format.formatter -> Imandra_surface.Top_result.decompose_region -> unit
          val to_string :
            ?unify:Unifier.unifier ->
            ?refine:refiner ->
            Imandra_surface.Top_result.decompose_region -> 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 -> Imandra_surface.Term.t list -> string list = <fun>
      val regions_doc :
        Imandra_interactive.Decompose.t list -> Imandra_surface.Document.t = <fun>
      
      In [8]:
      regions;;
      
      Out[8]:
      - : Imandra_interactive.Decompose.t list =
                                                                                                                                                                                                            <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