The stoplight model

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

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

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

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

Next we define a transition function for the stoplight:

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

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

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

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

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

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

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

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

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

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

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

In [5]:
verify
  (fun i ->
     let i = one_step i in
     valid_car_state i &&
     i.l.light_state = Red
     ==> i.c.car_drive_state = Braking)
;;
Out[5]:
- : intersection -> bool = <fun>
Proved
proof
{ground_instances: 0 ---------------------------------------------------------------------------- definitions: 0 ---------------------------------------------------------------------------- inductions: 0 ---------------------------------------------------------------------------- search_time: `0.027s` ---------------------------------------------------------------------------- details: {smt_stats: {rlimit count: 1368 ---------------------------------------------------------------------------- num allocs: 671739 ---------------------------------------------------------------------------- time: 0.011000 ---------------------------------------------------------------------------- memory: 5.180000 ---------------------------------------------------------------------------- max memory: 5.180000 } } }
Expand
  • start[0.027s]
      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"; view = <abstr>;
     special_tag = <abstr>;
     chash = Some RG8KLMSWqFoP5WUxVonYBJLaUfqkcBd+cJdnuvCBAHY;
     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 Is_a(Green, i.l.light_state)
  • not Is_a(Yellow, i.l.light_state)
  • i.c.car_speed = 20
  • i.c.car_accel_speed = 10
  • i.c.car_max_speed = 100
  • i.c.car_min_speed = 0
let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
 {_x_0 with
 car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
 car_distance = _x_0.car_distance + _x_1};
 l = {_x_2 with current_time = _x_2.current_time + 1}}
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 Is_a(Green, i.l.light_state)
  • not Is_a(Yellow, i.l.light_state)
  • i.c.car_speed = 20
  • i.c.car_accel_speed = 10
  • i.c.car_max_speed = 100
  • i.c.car_min_speed = 0
let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
 {_x_0 with
 car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
 l = {_x_1 with current_time = _x_1.current_time + 1}}
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 Is_a(Green, i.l.light_state)
  • not Is_a(Yellow, i.l.light_state)
  • i.c.car_speed = 20
  • i.c.car_accel_speed = 10
  • i.c.car_max_speed = 100
  • i.c.car_min_speed = 0
let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
 {_x_0 with
 car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
 car_distance = _x_0.car_distance + _x_1};
 l = {_x_2 with current_time = _x_2.current_time + 1}}
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
  • not Is_a(Green, i.l.light_state)
  • Is_a(Yellow, i.l.light_state)
  • i.c.car_speed = 20
  • i.c.car_accel_speed = 10
  • i.c.car_max_speed = 100
  • i.c.car_min_speed = 0
let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
 {_x_0 with
 car_drive_state = Braking; car_speed = _x_1 + _x_0.car_accel_speed;
 car_distance = _x_0.car_distance + _x_1};
 l = {_x_2 with blinking = true; current_time = _x_2.current_time + 1}}
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
  • not Is_a(Green, i.l.light_state)
  • Is_a(Yellow, i.l.light_state)
  • i.c.car_speed = 20
  • i.c.car_accel_speed = 10
  • i.c.car_max_speed = 100
  • i.c.car_min_speed = 0
let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
 {_x_0 with
 car_drive_state = Braking; car_distance = _x_0.car_distance + _x_0.car_speed};
 l = {_x_1 with blinking = true; current_time = _x_1.current_time + 1}}
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
  • not Is_a(Green, i.l.light_state)
  • Is_a(Yellow, i.l.light_state)
  • i.c.car_speed = 20
  • i.c.car_accel_speed = 10
  • i.c.car_max_speed = 100
  • i.c.car_min_speed = 0
let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
 {_x_0 with
 car_drive_state = Braking; car_speed = _x_1 - _x_0.car_accel_speed;
 car_distance = _x_0.car_distance + _x_1};
 l = {_x_2 with blinking = true; current_time = _x_2.current_time + 1}}
23
  • i.l.light_state = Green
  • i.c.car_drive_state = Accelerating
  • let (_x_0 : car_state) = i.c in
    not ((_x_0.car_speed + _x_0.car_accel_speed) > _x_0.car_max_speed)
  • let (_x_0 : light_state) = i.l in
    not ((_x_0.current_time + 1) > _x_0.light_change_time)
  • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
  • Is_a(Green, i.l.light_state)
  • i.c.car_speed = 20
  • i.c.car_accel_speed = 10
  • i.c.car_max_speed = 100
  • i.c.car_min_speed = 0
let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
 {_x_0 with
 car_drive_state = Steady; car_speed = _x_1 + _x_0.car_accel_speed;
 car_distance = _x_0.car_distance + _x_1};
 l = {_x_2 with blinking = true; current_time = _x_2.current_time + 1}}
22
  • i.l.light_state = Green
  • not (i.c.car_drive_state = Accelerating)
  • i.c.car_drive_state = Steady
  • let (_x_0 : light_state) = i.l in
    not ((_x_0.current_time + 1) > _x_0.light_change_time)
  • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
  • Is_a(Green, i.l.light_state)
  • i.c.car_speed = 20
  • i.c.car_accel_speed = 10
  • i.c.car_max_speed = 100
  • i.c.car_min_speed = 0
let (_x_0 : car_state) = i.c in
let (_x_1 : light_state) = i.l in
{c =
 {_x_0 with
 car_drive_state = Steady; car_distance = _x_0.car_distance + _x_0.car_speed};
 l = {_x_1 with blinking = true; current_time = _x_1.current_time + 1}}
20
  • i.l.light_state = Green
  • not (i.c.car_drive_state = Accelerating)
  • not (i.c.car_drive_state = Steady)
  • let (_x_0 : car_state) = i.c in
    not ((_x_0.car_speed - _x_0.car_accel_speed) < 0)
  • let (_x_0 : light_state) = i.l in
    not ((_x_0.current_time + 1) > _x_0.light_change_time)
  • let (_x_0 : light_state) = i.l in (_x_0.current_time + 1) > _x_0.blink_time
  • Is_a(Green, i.l.light_state)
  • i.c.car_speed = 20
  • i.c.car_accel_speed = 10
  • i.c.car_max_speed = 100
  • i.c.car_min_speed = 0
let (_x_0 : car_state) = i.c in
let (_x_1 : int) = _x_0.car_speed in
let (_x_2 : light_state) = i.l in
{c =
 {_x_0 with
 car_drive_state = Steady; car_speed = _x_1 - _x_0.car_accel_speed;
 car_distance = _x_0.car_distance + _x_1};
 l = {_x_2 with blinking = true; current_time = _x_2.current_time + 1}}
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 (Record, "current_time", FieldOf (Record, "l", Var "i")) -> Var "Current time"
    | FieldOf (Record, l, FieldOf (Record, "l", Var "i")) -> Var l
    | FieldOf (Record, c, FieldOf (Record, "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 -> ('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 -> 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