An introduction to imandra-tools

In this notebook, we'll introduce the imandra-tools library and go through how to use its powerful modules to augment Imandra's decomposition facilities.

Normally, before using imandra-tools, one would have to require it in their Imandra toplevel by executing the require statement #require "imandra-tools". Since the #require directive is disabled for security reasons in this notebook, this step won't be necessary as we've pre-loaded imandra-tools.

Let's make sure this is actually the case before starting.

In [1]:
#show Imandra_tools;;
Out[1]:
module Imandra_tools :
  sig
    module Idf = Imandra_tools.Idf
    module Idf_intf = Imandra_tools.Idf_intf
    module Region_idx = Imandra_tools.Region_idx
    module Region_json = Imandra_tools.Region_json
    module Region_pp = Imandra_tools.Region_pp
    module Region_pp_intf = Imandra_tools.Region_pp_intf
    module Region_probs = Imandra_tools.Region_probs
    module Region_term_synth = Imandra_tools.Region_term_synth
  end

Great! Let's start exploring imandra-tools.

Note: this is an introductory walkthrough of the capabilities of `imandra-tools`, much more than what's described in this notebook is possible with it, but we'll defer a more in-depth explanation of each module in future notebooks.

Iterative Decomposition Framework (Idf)

The first module we're going to explore is Imandra_tools.Idf. Its broad purpose is to provide a framework allowing for iterative, lazy decomposition of state-machine models.

Before diving into its usage, let's first define a simple example of such a model.

In [2]:
module Model = struct
  type message = Add of int | Sub of int | Reset

  type counter_state = { counter : int
                       ; default : int }

  let one_step msg state =
    if state.counter = 1337 then
      { state with counter = state.default }
    else
      match msg with
      | Reset -> { state with counter = 0 }
      | Add n ->
         if state.counter + n > 9000 then
           { state with counter = 0 }
         else
           { state with counter = state.counter + n }
      | Sub n ->
         if n > state.counter then
           state
         else
           { state with counter = state.counter - n }
  end
Out[2]:
module Model :
  sig
    type message = Add of int | Sub of int | Reset
    type counter_state = { counter : int; default : int; }
    val one_step : message -> counter_state -> counter_state
  end

The above model is not very interesting but it exemplifies all that's needed for a model to be suitable for usage with Idf:

  • An algebraic type describing all the possible messages a model can react to (message)
  • A type describing the current state of the model (counter_state)
  • A transition function from message and state to new state (one_step)

Now that the module is defined, we need to set-up Idf for its decomposition.

We need to do is define a module implementing the Idf_intf.DFSM_SIG module signature:

  • a State_machine module implementing the Idf_intf.SM_SIG module signature:
    • an event type mapping to the model message type
    • a state type mapping to the model state type
    • an init_state value of type state
    • a step transition function mapping to the model transition function
    • an is_valid function that takes an event and a state and checks whether that <event,state> transition is valid or not
  • a module_name value mapping to the name of the module being defined (this is necessary for reflection purposes)
  • a Template module implementing the Idf_intf.TPL_SIG module signature:
    • a t variant type symbolically describing events from our model
    • a c variant type mapping to the concrete event type
    • a concrete function mapping t events to c events
In [3]:
open Imandra_tools

module Decomp = struct

  module State_machine = struct
    open Model

    type event = message
    type state = counter_state

    let init_state : state =
      { counter = 0 ; default = 23 }

    let step (event : event) (state : state) : state =
       one_step event state

    let is_valid (event : event) (state : state) : bool =
      match event with
      | Reset -> true
      | Add n -> n > 0
      | Sub n -> n > 0 && n <= state.counter

  end

  let module_name = "Decomp"

  module Template = struct
    type t = Add | Sub | Reset | Any
    type c = State_machine.event

    let concrete c t = match c, t with
        | Add, Model.Add _ -> true
        | Sub, Model.Sub _ -> true
        | Reset, Model.Reset -> true
        | Any, _ -> true
        | _ -> false
  end

end
Out[3]:
module Decomp :
  sig
    module State_machine :
      sig
        type event = Model.message
        type state = Model.counter_state
        val init_state : state
        val step : event -> state -> state
        val is_valid : event -> state -> bool
      end
    val module_name : string
    module Template :
      sig
        type t = Add | Sub | Reset | Any
        type c = State_machine.event
        val concrete : t -> c -> bool
      end
  end

We're now ready to create a decomposition recipe and apply it to an event template, simply instantiating Idf with Decomp in a module IDF.

We can use the IDF module to start decomposing any sequences of events, let's do that over a template of [any; add; any] events:

In [4]:
#program;;

module IDF = Idf.Make(Decomp);;

let g = IDF.G.create ();;
IDF.decompose ~g (Decomp.Template.[Any;Add;Any]) ();;
Out[4]:
val g___1 : Model.message list -> Model.counter_state = <fun>
module Mex :
  sig
    val get_option : (Term.term -> 'a_0) -> Term.term -> 'a_0 option
    val get_nativeint : Term.term -> nativeint
    val get_Peano_nat_t : Term.term -> Peano_nat.t
    val get_unit : Term.term -> unit
    val get_result :
      (Term.term -> 'a_0) ->
      (Term.term -> 'a_1) -> Term.term -> ('a_0, 'a_1) result
    val get_Result_t :
      (Term.term -> 'a_0) ->
      (Term.term -> 'a_1) -> Term.term -> ('a_0, 'a_1) result
    val get_either :
      (Term.term -> 'a_0) ->
      (Term.term -> 'a_1) -> Term.term -> ('a_0, 'a_1) either
    val get_List_t : (Term.term -> 'a_0) -> Term.term -> 'a_0 list
    val get_Int_t : Term.term -> int
    val get_Bool_t : Term.term -> bool
    val get_Option_t : (Term.term -> 'a_0) -> Term.term -> 'a_0 option
    val get_Real_t : Term.term -> real
    val get_Map_t :
      (Term.term -> 'a_0) ->
      (Term.term -> 'a_1) -> Term.term -> ('a_0, 'a_1) Map.t
    val get_Multiset_t : (Term.term -> 'a_0) -> Term.term -> 'a_0 Multiset.t
    val get_Set_t : (Term.term -> 'a_0) -> Term.term -> 'a_0 Set.t
    val get_String_t : Term.term -> string
    val get_Float_t : Term.term -> float
    val get_Reflect_Uid_t : Term.term -> Reflect.Uid.t
    val get_Reflect_Type_t : Term.term -> Reflect.Type.t
    val get_Reflect_Var_t : Term.term -> Reflect.Var.t
    val get_Reflect_Term_const : Term.term -> Reflect.Term.const
    val get_Reflect_Term_binding :
      (Term.term -> 'a_0) -> Term.term -> 'a_0 Reflect.Term.binding
    val get_Reflect_Term_t : Term.term -> Reflect.Term.t
    val get_Model_message : Term.term -> Model.message
    val get_Model_counter_state : Term.term -> Model.counter_state
    val get_Decomp_State_machine_event : Term.term -> Model.message
    val get_Decomp_State_machine_state : Term.term -> Model.counter_state
    val get_Decomp_Template_t : Term.term -> Decomp.Template.t
    val get_Decomp_Template_c : Term.term -> Model.message
    type e_t = Model.message list
    type extract_type = { e : e_t; }
    val ret_e : extract_type -> e_t
    val of_model : ?signature:string -> Top_result.term_model -> extract_type
  end
- : unit = ()
module IDF :
  sig
    module DSM :
      sig
        module State_machine :
          sig
            type state = Model.counter_state
            type event = Model.message
            val init_state : state
            val step : event -> state -> state
            val is_valid : event -> state -> bool
          end
        module Template :
          sig
            type t = Decomp.Template.t
            type c = State_machine.event
            val concrete : t -> c -> bool
          end
        val module_name : string
      end
    val pp_state : Model.counter_state -> string
    type target = DSM.Template.t list
    type node = IDF.node
    type path = node list
    module G :
      sig
        type t = IDF.G.t
        module V :
          sig
            type t = node
            val compare : t -> t -> int/2
            val hash : t -> int/2
            val equal : t -> t -> bool
            type label = t
            val create : t -> t
            val label : t -> t
          end
        type vertex = node
        module E :
          sig
            type t = IDF.G.edge
            val compare : t -> t -> int/2
            type vertex = node
            val src : t -> vertex
            val dst : t -> vertex
            type label = IDF.G.E.label
            val create : vertex -> label -> vertex -> t
            val label : t -> label
          end
        type edge = E.t
        val is_directed : bool
        val is_empty : t -> bool
        val nb_vertex : t -> int/2
        val nb_edges : t -> int/2
        val out_degree : t -> vertex -> int/2
        val in_degree : t -> vertex -> int/2
        val mem_vertex : t -> vertex -> bool
        val mem_edge : t -> vertex -> vertex -> bool
        val mem_edge_e : t -> edge -> bool
        val find_edge : t -> vertex -> vertex -> edge
        val find_all_edges : t -> vertex -> vertex -> edge list
        val succ : t -> vertex -> vertex list
        val pred : t -> vertex -> vertex list
        val succ_e : t -> vertex -> edge list
        val pred_e : t -> vertex -> edge list
        val iter_vertex : (vertex -> unit) -> t -> unit
        val fold_vertex : (vertex -> 'a -> 'a) -> t -> 'a -> 'a
        val iter_edges : (vertex -> vertex -> unit) -> t -> unit
        val fold_edges : (vertex -> vertex -> 'a -> 'a) -> t -> 'a -> 'a
        val iter_edges_e : (edge -> unit) -> t -> unit
        val fold_edges_e : (edge -> 'a -> 'a) -> t -> 'a -> 'a
        val map_vertex : (vertex -> vertex) -> t -> t
        val iter_succ : (vertex -> unit) -> t -> vertex -> unit
        val iter_pred : (vertex -> unit) -> t -> vertex -> unit
        val fold_succ : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
        val fold_pred : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
        val iter_succ_e : (edge -> unit) -> t -> vertex -> unit
        val fold_succ_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
        val iter_pred_e : (edge -> unit) -> t -> vertex -> unit
        val fold_pred_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
        val create : ?size:int/2 -> unit -> t
        val clear : t -> unit
        val copy : t -> t
        val add_vertex : t -> vertex -> unit
        val remove_vertex : t -> vertex -> unit
        val add_edge : t -> vertex -> vertex -> unit
        val add_edge_e : t -> edge -> unit
        val remove_edge : t -> vertex -> vertex -> unit
        val remove_edge_e : t -> edge -> unit
        val root : t -> vertex
        val leaves : t -> vertex list
        val output_graph : t -> file:string -> unit
      end
    val paths : ?from:node -> G.t -> path list
    val region : node -> Top_result.modular_region
    val expanded_constraints : node -> Term.term list
    val sample : node -> Model.message list
    val sample_region : Top_result.modular_region -> Model.message list
    val target_steps : node -> (DSM.Template.t * bool option) list
    type replay_sample =
      IDF.replay_sample = {
      state_before : Model.counter_state;
      event : Model.message;
      state_after : Model.counter_state;
    }
    val replay_events : Model.message list -> replay_sample list
    val replay : node -> replay_sample list
    val decompose :
      g:G.t ->
      ?basis:string list ->
      ?include_partial_paths:bool ->
      ?expanding:string list ->
      ?valid_pol:bool option list ->
      ?assuming:string ->
      ?region_expander:(string option * string list * string option) list ->
      target -> unit -> unit
  end
val g : IDF.G.t = <abstr>
- : unit = ()
val guard_g___2_0 : Model.message list -> bool = <fun>
val target_g___2_0 : Model.message list -> Model.counter_state = <fun>
val guard_g___2_1 : Model.message list -> bool = <fun>
val target_g___2_1 : Model.message list -> Model.counter_state = <fun>
val guard_g___2_2 : Model.message list -> bool = <fun>
val target_g___2_2 : Model.message list -> Model.counter_state = <fun>
- : unit = ()

Since IDF generates a decomposition graph, we need to first create an empty graph via IDF.G.create, we can then list all the paths of the decomposition graph from the initial state to the final state:

In [5]:
let paths = IDF.paths g
let first_path = List.hd paths
Out[5]:
val paths : IDF.path list =
  [[<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>];
   [<abstr>; <abstr>; <abstr>; <abstr>]]
val first_path : IDF.path = [<abstr>; <abstr>; <abstr>; <abstr>]

This output is not very useful, but we can ask Idf to play out a sample execution of that path:

In [6]:
IDF.replay (first_path |> CCList.last_opt |> CCOpt.get_exn)
Out[6]:
- : IDF.replay_sample list =
[{IDF.state_before = {Model.counter = 0; default = 23}; event = Model.Reset;
  state_after = {Model.counter = 0; default = 23}};
 {IDF.state_before = {Model.counter = 0; default = 23};
  event = Model.Add 9001; state_after = {Model.counter = 0; default = 23}};
 {IDF.state_before = {Model.counter = 0; default = 23};
  event = Model.Add 9039; state_after = {Model.counter = 0; default = 23}}]

Or we can ask Idf to let us inspect the regions for that path (each region in the list will correspond to the constraints and invariant of the model up to each event in the template):

In [7]:
let first_path_regions = List.map IDF.region first_path
Out[7]:
val first_path_regions : Top_result.modular_region list =
  [{Imandra_surface.Modular_region.mreg_session = 1i; mreg_id = 0i;
    mreg_constraints = [true];
    mreg_invariant = {Model.counter = 0; Model.default = 23};
    mreg_args = [(e : Decomp.State_machine.event list)];
    mreg_status = Imandra_surface.Modular_region.Unknown};
   {Imandra_surface.Modular_region.mreg_session = 1i; mreg_id = 3i;
    mreg_constraints = [List.hd e = Model.Reset; e <> []; List.tl e = []];
    mreg_invariant = {Model.counter = 0; Model.default = 23};
    mreg_args = [(e : Decomp.State_machine.event list)];
    mreg_status = Imandra_surface.Modular_region.Unknown};
   {Imandra_surface.Modular_region.mreg_session = 1i; mreg_id = 10i;
    mreg_constraints =
     [List.hd e = Model.Reset;
      not (Destruct(Model.Add, 0, List.hd (List.tl e)) <= 9000);
      Is_a(Model.Add, List.hd (List.tl e)); e <> []; (List.tl e) <> [];
      List.tl (List.tl e) = []];
    mreg_invariant = {Model.counter = 0; Model.default = 23};
    mreg_args = [(e : Decomp.State_machine.event list)];
    mreg_status = Imandra_surface.Modular_region.Unknown};
   {Imandra_surface.Modular_region.mreg_session = 1i; mreg_id = 44i;
    mreg_constraints =
     [Is_a(Model.Add, List.hd (List.tl e));
      not (Destruct(Model.Add, 0, List.hd (List.tl e)) <= 9000);
      List.hd e = Model.Reset;
      not (Destruct(Model.Add, 0, List.hd (List.tl (List.tl e))) <= 9000);
      Is_a(Model.Add, List.hd (List.tl (List.tl e))); e <> [];
      (List.tl e) <> []; (List.tl (List.tl e)) <> [];
      List.tl (List.tl (List.tl e)) = []];
    mreg_invariant = {Model.counter = 0; Model.default = 23};
    mreg_args = [(e : Decomp.State_machine.event list)];
    mreg_status = Imandra_surface.Modular_region.Unknown}]

For a full description of the Idf API and capabilities, check out the Iterative Decomposition Framework page.

Looking at the above regions we can spot a common problem with decompositions: the regions become very hard to read, even with quite simple models.

This is a good moment to introduce a second imandra-tools module:

Region Pretty Printer (Region_pp)

The purpose of the Region_pp module is twofold: it provides a default drop-in pretty printer for regions, much more powerful than the default region printer and it also provides an extensible framework for creating powerful printers with semantic and ontologic understanding of the model being decomposed.

Behind the scenes, the printer has phases for constraint unification, merging, normalisation and pruning, symbolic evaluation, and much more - all of it is user-extensible and customizable.

All it takes to start reaping the benefits is to install the default pretty printer:

In [8]:
#install_printer Region_pp.print;;

first_path_regions
Out[8]:
- : Top_result.modular_region list =
[---[region]---
 Constraints:
   [  ]
 Invariant:
   F = Model.{ counter = 0 ; default = 23 }
  -------------;
 ---[region]---
 Constraints:
   [ (List.hd e) is Model.Reset
   ; (List.tl e) = [] ]
 Invariant:
   F = Model.{ counter = 0 ; default = 23 }
  -------------;
 ---[region]---
 Constraints:
   [ (List.hd e) is Model.Reset
   ; (List.hd (List.tl e)) is Model.Add
   ; Destruct(Model.Add, 0, (List.hd (List.tl e))) > 9000
   ; (List.tl (List.tl e)) = [] ]
 Invariant:
   F = Model.{ counter = 0 ; default = 23 }
  -------------;
 ---[region]---
 Constraints:
   [ (List.hd (List.tl e)) is Model.Add
   ; (List.hd e) is Model.Reset
   ; (List.hd (List.tl (List.tl e))) is Model.Add
   ; Destruct(Model.Add, 0, (List.hd (List.tl e))) > 9000
   ; Destruct(Model.Add, 0, (List.hd (List.tl (List.tl e)))) >
       9000
   ; (List.tl (List.tl (List.tl e))) = [] ]
 Invariant:
   F = Model.{ counter = 0 ; default = 23 }
  -------------]

We can immediately appreciate that just under half the total constraints have been identified as redundant and eliminated.

Let's look at another example:

In [9]:
#logic;;

let f (x : int Set.t) y z =
  if Set.subset x y then
    Set.add z x
  else
    Set.add z (Set.empty);;

#program;;

let d = Modular_decomp.top "f";;

let rs = Modular_decomposition.to_region_list d |> CCList.map (fun (i, _) -> Modular_decomp.get_region d i);;
Out[9]:
val f : int Set.t -> int Set.t -> int -> int Set.t = <fun>
val d : Top_result.modular_decomposition =
  {Imandra_interactive.Modular_decomp.MD.md_session = 2i;
   md_f =
    {Imandra_surface.Uid.name = "f"; id = <abstr>; special_tag = <abstr>;
     namespace = <abstr>;
     chash = Some 5TxglC7SODQbo0rSHeXCN7M4LjjUd1E+ZgVXWZQ6FoA;
     depth = (3i, 2i)};
   md_args = [(x : (int, bool) Map.t); (y : (int, bool) Map.t); (z : int)];
   md_regions = <abstr>}
val rs : Top_result.modular_region list =
  [---[region]---
   Constraints:
     [ not (Set.subset x y) ]
   Invariant:
     F = Set.add z Set.empty
    -------------;
   ---[region]---
   Constraints:
     [ Set.subset x y ]
   Invariant:
     F = Set.add z x
    -------------]
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 (f x, y, z
Reg_idConstraintsInvariant
1
  • not (Set.subset x y)
Set.add z Set.empty
0
  • Set.subset x y
Set.add z x

It seems like Region_pp could do a better job here:

  • Set.subset x y is printed as Set.union x y = y
  • Set.add x y is printed as Map.add x y true
  • Set.add z (Set.empty) is printed as Map.add' (Map.const false) z true instead of using a more desiderable set syntax like { z }

Let's use the extension mechanisms of Region_pp to achieve just that:

In [10]:
open Region_pp_intf

module Custom = struct

  type t =
    | Set of t node_ list

  let map f = function
    | Set els -> Set (List.map f els)

  let compare compare one two =
    match one, two with
    | Set s_one, Set s_two ->
       if List.length s_one = List.length s_two &&
            CCList.for_all (fun el -> (List.exists (fun x -> compare el x = Equivalent) s_two)) s_one then
         Equivalent
       else
         UnComparable

  let print p ~focus out = function
    | Set s -> CCFormat.(fprintf out "@[<hv>{ %a@ }@]" (list ~sep:(return "@ ; ") p)) s
end

module PPrinter = Region_pp.Make(Custom)

open Custom
open PPrinter

let rec refine_ = function
  | Funcall (Var "Map.add'", _) as ks when is_proper_set ks ->
     Custom (Set (gather_keys ks))

  | Funcall (Var "Map.add'", [m; k; Boolean true]) ->
     Funcall (Var "Set.add", [m; k])

    (* verify (fun x y -> Set.union x y = y ==> Set.subset x y)  *)

  | Eq (Funcall (Var "Set.union", [x;y]), z) when Comparator.(is_eq (compare y z)) ->
     Eq (Funcall (Var "Set.subset", [x;y]), Boolean true)

  | Neq (Funcall (Var "Set.union", [x;y]), z) when Comparator.(is_eq (compare y z)) ->
     Eq (Funcall (Var "Set.subset", [x;y]), Boolean false)

  | Eq (z, Funcall (Var "Set.union", [x;y])) when Comparator.(is_eq (compare y z)) ->
     Eq (Funcall (Var "Set.subset", [x;y]), Boolean true)

  | Neq (z, Funcall (Var "Set.union", [x;y])) when Comparator.(is_eq (compare y z)) ->
     Eq (Funcall (Var "Set.subset", [x;y]), Boolean false)

  | x -> x

and gather_keys = function
  | Funcall (Var "Map.add'", [m; k; Boolean true]) -> k::gather_keys m
  | Funcall (Var "Map.const", [Boolean false]) -> []
  | x -> failwith (Printf.sprintf "Unexpected set value: %s" (PPrinter.Printer.to_string x))

and is_proper_set x =
  try ignore(gather_keys x); true with _ -> false

let refine ast = XF.walk_fix refine_ ast |> CCList.return

let print = PPrinter.print ~refine ()
Out[10]:
module Custom :
  sig
    type t = Set of t node_ list
    val map : (t node_ -> t node_) -> t -> t
    val compare : (t node_ -> t node_ -> comparison) -> t -> t -> comparison
    val print :
      t node_ CCFormat.printer -> focus:'a -> Format.formatter -> t -> unit
  end
module PPrinter :
  sig
    type custom = PPrinter.custom
    type node = custom node_
    module XF :
      sig
        val map : (node -> node) -> node -> node
        val walk : pre:(node -> node) -> ?post:(node -> node) -> node -> node
        val fix_ : ?bound:int/2 -> ('a -> 'a) -> 'a -> 'a -> 'a
        val fix : ?bound:int/2 -> ('a -> 'a) -> 'a -> 'a
        val walk_fix : ?bound:int/2 -> (node -> node) -> node -> node
        val iterated : unit -> 'a
        val iter : f:(node -> unit) -> node -> unit
        val exists : f:(node -> bool) -> node -> bool
      end
    val vars : node -> string list
    val has_symbolic_term : node -> bool
    module Printer :
      sig
        val print :
          ?p:(node CCFormat.printer ->
              Format.formatter -> node -> unit option) ->
          ?focus:string -> unit -> node CCFormat.printer
        val to_string :
          ?p:(node CCFormat.printer ->
              Format.formatter -> node -> unit option) ->
          ?focus:string -> node -> string
      end
    module Comparator :
      sig
        val is_eq : comparison -> bool
        val compare : node -> node -> comparison
        val compare_all : node list -> node list -> comparison
      end
    module Simplifier : sig val simplify : node -> node end
    module Unifier :
      sig
        type unifier = node -> node -> node option
        val unify : ?unify:unifier -> node list -> node list
      end
    module Parser : sig val parse : Term.term -> node option end
    module Compactor : sig val compact : node list -> node list end
    type refiner = node -> node list
    type pprinter =
        ?unify:Unifier.unifier ->
        ?refine:refiner -> ?inv:bool -> Term.term list -> node list
    val pp : pprinter
    val print :
      ?pp:pprinter ->
      ?unify:Unifier.unifier ->
      ?refine:refiner ->
      ?print:(node CCFormat.printer ->
              Format.formatter -> node -> unit option) ->
      ?skip_invariant:bool ->
      ?focus:string ->
      unit -> Format.formatter -> Top_result.modular_region -> unit
    val to_string :
      ?unify:Unifier.unifier ->
      ?refine:refiner -> Top_result.modular_region -> string
  end
val refine_ : custom node_ -> custom node_ = <fun>
val gather_keys : custom node_ -> custom node_ list = <fun>
val is_proper_set : custom node_ -> bool = <fun>
val refine : node -> node list = <fun>
val print : Format.formatter -> Top_result.modular_region -> unit = <fun>

Let's look at what we've done:

  • first we've defined a Custom module whose signature includes the signature of Region_pp_intf.SIG, defining mapping, printing and compareing functions for an abstract Set value
  • next we instantiate Region_pp.Make using this Custom module, creating a PPrinter module that is Set-aware
  • finally we define a refine function that transforms a PPrinter.node into custom Set values or converts Map. invocations into appropriate Set. ones.

Let's install this printer and look at the regions again:

In [11]:
#install_printer print;;
rs
Out[11]:
- : Top_result.modular_region list =
[---[region]---
 Constraints:
   [ not (Set.subset x y) ]
 Invariant:
   F = Set.add z Set.empty
  -------------;
 ---[region]---
 Constraints:
   [ Set.subset x y ]
 Invariant:
   F = Set.add z x
  -------------]

Great! Exactly what we wanted to be printed.

Region_pp provides more extension hooks and utilities than just the PP functor and ~refine, but we'll go over that in more detail in a dedicated notebook.

Let's explore the next imandra-tools module

Region Term Synthesizer (Region_term_synth)

Imandra's ability to both reify failed proofs into counter-examples and sample values from regions provides a lot of power. Region_term_synth extends this power, allowing Imandra to synthesize any region's Term expression as code.

This, combined with Imandra's decomposition facilities, allow us to generate powerful and complete regression test suites, analyse existing test suites to detect region coverage, and much more.

Let's see a quick example of how this works in practice:

In [12]:
Caml.List.mapi (fun i region ->
  let gs = "region_" ^ (string_of_int i) in (* Imandra_util.Util.gensym () *)
  let term = Term.and_l @@ Modular_region.constraints region in
  let body = Region_term_synth.synthesize ~default:Term.Syn.False term in
  let args = Modular_region.args region |> List.map Var.name |> String.concat " " in
  let func = Printf.sprintf "let %s %s = %s" gs args body in
  System.eval func;
  gs)
  rs
Out[12]:
val region_0 : 'a Set.t -> 'a Set.t -> 'b -> bool = <fun>
val region_1 : 'a Set.t -> 'a Set.t -> 'b -> bool = <fun>
- : string list = ["region_0"; "region_1"]

The above should be quite straightforward:

  • We extract the constraints from the region and we conjoin them into a single Term
  • We ask Region_term_synth to synthesize our term, using false as a default value (we're synthesizing a boolean function)
  • Finally we generate a string representation of a function using the synthesized term as its body, and evaluate it

We can start playing with those functions immediately:

In [13]:
region_0 (Set.of_list [1]) Set.empty 0;;
region_0 Set.empty (Set.of_list [1]) 0;;

region_1 Set.empty (Set.of_list [1]) 0;;
region_1 (Set.of_list [1]) Set.empty 0;;
Out[13]:
- : bool = true
- : bool = false
- : bool = true
- : bool = false

Great! region_0 is now a boolean function that checks whether or not certain values of x and y belong to the region of behaviour 0. region_1 does the same for the region of behaviour 1.

This ability to generate total functions from partial regions of behaviour is fundamental to creating modules like Idf and Region_idx.

Region Indexer (Region_idx)

It may be sometimes useful to know which region a particular input belongs to; while this can be done by using Region_term_synth and synthesizing recogniser functions for each region and testing them against the value until we find a match, this could get very computationally expensive in the presence of a large number of regions and constraints.

Region_idx provides a solution for this: it allows to create "indexing" functions that efficiently match input values against a single entry in a list of regions. After providing a first class module specificing the types of the arguments to the function the regions belong to (as a tuple), Region_idx.indexer_for returns an index alist and an indexer function.

In [14]:
let idx, indexer =
  let args = (module struct type args = int Set.t * int Set.t * int end : Region_idx.Args with type args = _) in
  Region_idx.indexer_for args rs;;
Out[14]:
val g___3 : 'a Set.t -> 'a Set.t -> 'b -> int/2 = <fun>
- : unit = ()
val idx : (int/2 * Top_result.modular_region) list =
  [(0i,
    ---[region]---
    Constraints:
      [ not (Set.subset x y) ]
    Invariant:
      F = Set.add z Set.empty
     -------------);
   (1i,
    ---[region]---
    Constraints:
      [ Set.subset x y ]
    Invariant:
      F = Set.add z x
     -------------)]
val indexer : int/1 Set.t * int/1 Set.t * int/1 -> int/2 = <fun>

The first value returned is an alist of index -> region, while the second value is the indexer function, taking as inputs the arguments of the regions (as a tuple) and returning the index of the matching region, or raising Not_found if the values don't match any regions (This can happen if the values provided don't satisfy the side condition, or if the list of regions passed to indexer_for was partial).

Let's say we want to know which region the arguments Set.empty, (Set.of_list [1]), 0 belong to, we just need to find its index and find the matching region:

In [15]:
let i = indexer (Set.empty, (Set.of_list [1]), 0) in
  CCList.assq i idx;;
Out[15]:
- : Top_result.modular_region =
---[region]---
Constraints:
  [ Set.subset x y ]
Invariant:
  F = Set.add z x
 -------------

Region Probabilities (Region_probs)

What if we want to not just identify the distinct regions of a program's behaviour, but how likely those behaviours are to occur? The Region_probs module allows us to do just that. In particular, users can easily create custom hierarchical statistical models defining joint distributions over inputs to their programs or functions, then sample from these models to get a probability distribution over regions, or query them with Boolean conditions. Alternatively, a dataset in the form of a CSV file can be imported and used as a set of samples when the underlying distribution is unknown. This introduction contains a short example, but for a more detailed tutorial of how to use the module, please see the dedicated Region Probabilities notebook.

First we'll open the Region_probs module, then define some custom types and a function that we'll be decomposing:

In [16]:
#logic;;
open Region_probs;;

type colour = Red | Green | Blue;;
type obj = {colour : colour; broken : bool};;
type dom = (obj * Q.t * Z.t);;

let f' (obj, temp, num) =
  let a =
    if obj.colour = Red then
      if obj.broken then num else 7
    else
      num * 2 in
  let b =
    if temp >. 18.5 && obj.colour = Blue then
      temp +. 4.3
    else if obj.colour = Green then
      temp -. 7.8
    else
      14.1 in
  (a, b);;
Out[16]:
type colour = Red | Green | Blue
type obj = { colour : colour; broken : bool; }
type dom = obj * real * int
val f' : obj * real * int -> int * real = <fun>

Now we can define a joint distribution over inputs to f using some built-in probability distributions and a sequential sampling procedure. We can call this function with the unit argument () to generate samples:

In [17]:
let distribution () =
  let c = categorical ~classes:[Red; Green; Blue] ~probs:[0.5; 0.2; 0.3] () in
  let b = bernoulli ~p:0.4 () in
  let mu = if b then 20. else 10. in
  let temp = gaussian ~mu ~sigma:5. () in
  let num =
    if c = Green then
      poisson ~lambda:6.5 ~constraints:[(7, 10)] ()
    else
      poisson ~lambda:6.5 () in
  ({colour = c; broken = b}, temp, num) [@@program];;

distribution ();;
Out[17]:
val distribution : unit -> obj * real * int = <fun>
- : obj * real * int =
({colour = Red; broken = false}, 3692047287333181/281474976710656, 5)

Now we have all these components we can find the regions of f, create a model from our distribution function, then estimate and display region probabilities:

In [18]:
let d = Modular_decomp.top "f'" [@@program];;
Modular_decomp.prune d [@@program];;

let regions =
  Modular_decomposition.to_region_list d
  |> CCList.map (fun (i, _) -> Modular_decomp.get_region d i) [@@program];;

module Example = Distribution.From_Sampler (struct type domain = dom let dist = distribution end) [@@program];;

let probs = Example.get_probs regions () [@@program];;

print_probs probs;;
Out[18]:
val d : Top_result.modular_decomposition =
  {Imandra_interactive.Modular_decomp.MD.md_session = 3i;
   md_f =
    {Imandra_surface.Uid.name = "f'"; id = <abstr>; special_tag = <abstr>;
     namespace = <abstr>;
     chash = Some YFaICL9zUmzK01GcQMEnt6tJme/GNl9xF9eRBwCjBBM;
     depth = (3i, 3i)};
   md_args = [(_x : (obj * real * int))]; md_regions = <abstr>}
- : unit = ()
val regions : Top_result.modular_region list =
  [---[region]---
   Constraints:
     [ _x[0].colour is Blue
     ; _x[1] <= 37/2 ]
   Invariant:
     F = ((_x[2] * 2), 141/10)
    -------------;
   ---[region]---
   Constraints:
     [ _x[0].colour is Green
     ; _x[1] <= 37/2 ]
   Invariant:
     F = ((_x[2] * 2), (_x[1] - 39/5))
    -------------;
   ---[region]---
   Constraints:
     [ _x[0].colour is Green
     ; _x[1] > 37/2 ]
   Invariant:
     F = ((_x[2] * 2), (_x[1] - 39/5))
    -------------;
   ---[region]---
   Constraints:
     [ _x[0].colour is Blue
     ; _x[1] > 37/2 ]
   Invariant:
     F = ((_x[2] * 2), (_x[1] + 43/10))
    -------------;
   ---[region]---
   Constraints:
     [ _x[0].colour is Red
     ; _x[1] <= 37/2
     ; not _x[0].broken ]
   Invariant:
     F = (7, 141/10)
    -------------;
   ---[region]---
   Constraints:
     [ _x[0].colour is Red
     ; _x[1] > 37/2
     ; not _x[0].broken ]
   Invariant:
     F = (7, 141/10)
    -------------;
   ---[region]---
   Constraints:
     [ _x[0].colour is Red
     ; _x[1] <= 37/2
     ; _x[0].broken ]
   Invariant:
     F = (_x[2], 141/10)
    -------------;
   ---[region]---
   Constraints:
     [ _x[0].colour is Red
     ; _x[1] > 37/2
     ; _x[0].broken ]
   Invariant:
     F = (_x[2], 141/10)
    -------------]
module Example :
  sig
    type domain = dom
    val get_probs :
      Top_result.modular_region list ->
      ?assuming:string ->
      ?n:int/1 ->
      ?d:string ->
      ?step_function:(dom -> dom) ->
      ?num_steps:int/1 ->
      unit -> (int/2, float * Top_result.modular_region) Hashtbl.t
    val query :
      (dom -> bool) ->
      ?n:int ->
      ?d:string -> ?max_std_err:real -> ?precision:int -> unit -> unit
    val save : string -> ?n:int -> ?d:dom list -> unit -> unit
    val load : string -> dom list
  end
val g___21 : obj * real * 'a -> int/2 = <fun>
- : unit = ()
val probs : (int/2, float * Top_result.modular_region) Hashtbl.t = <abstr>
Region   Probability
6        0.0733
2        0.0516
7        0.1292
3        0.0817
5        0.0141
4        0.2905
0        0.2147
1        0.1449

- : unit = ()
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 (f' _x
Reg_idConstraintsInvariant
7
  • not (_x.0.colour = Green)
  • not (_x.1 >. 37/2)
  • not (_x.0.colour = Red)
(_x.2 * 2, 141/10)
6
  • _x.0.colour = Green
  • not (_x.1 >. 37/2)
  • not (_x.0.colour = Red)
(_x.2 * 2, _x.1 -. 39/5)
5
  • _x.0.colour = Green
  • not (_x.0.colour = Blue)
  • _x.1 >. 37/2
  • not (_x.0.colour = Red)
(_x.2 * 2, _x.1 -. 39/5)
4
  • _x.0.colour = Blue
  • _x.1 >. 37/2
  • not (_x.0.colour = Red)
(_x.2 * 2, _x.1 +. 43/10)
3
  • not (_x.0.colour = Green)
  • not (_x.1 >. 37/2)
  • not _x.0.broken
  • _x.0.colour = Red
(7, 141/10)
2
  • not (_x.0.colour = Green)
  • not (_x.0.colour = Blue)
  • _x.1 >. 37/2
  • not _x.0.broken
  • _x.0.colour = Red
(7, 141/10)
1
  • not (_x.0.colour = Green)
  • not (_x.1 >. 37/2)
  • _x.0.broken
  • _x.0.colour = Red
(_x.2, 141/10)
0
  • not (_x.0.colour = Green)
  • not (_x.0.colour = Blue)
  • _x.1 >. 37/2
  • _x.0.broken
  • _x.0.colour = Red
(_x.2, 141/10)

To see more of what can be done with the Region_probs module, including forming models based on existing datasets and querying models using Boolean conditions, along with additional options, please see the Region Probabilities notebook.