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 -> Model.message -> 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 D.

We can use the D module to start decomposing any sequences of events, by using either D.Symbolic or D.Sampling, depending on which decomposition strategy we want:

  • sampling: this strategy will decompose the first event in the sequence, sample a value off each region and continue decomposition using the sampled value as next initial state when decomposing the next event. Because of its reliance on random sampling, this strategy is not complete, but is quite fast.
  • symbolic: this strategy will synthesize the constraints and invariants of each region as ocaml code and inject them into the decomposition of the next event, no sampling is done and thus this strategy is complete, but can also be much slower than concrete.

Let's use D.Symbolic.decompose for this notebook, over a template of [any; add; any] events:

In [4]:
#program;;

module D = Idf.Make(Decomp);;
module IDF = D.Symbolic;;

let paths, _ = IDF.decompose (Decomp.Template.[Any;Add;Any]);;
Out[4]:
val g___1 : Decomp.State_machine.event list -> Decomp.State_machine.state =
  <fun>
module Mex :
  sig
    module E = Imandra_interactive.Extract
    val get_option : (E.expr -> 'a_0) -> E.expr -> 'a_0 option
    val get_nativeint : E.expr -> nativeint
    val get_Peano_nat_t : E.expr -> Peano_nat.t
    val get_unit : E.expr -> unit
    val get_result :
      (E.expr -> 'a_0) -> (E.expr -> 'a_1) -> E.expr -> ('a_0, 'a_1) result
    val get_Result_t :
      (E.expr -> 'a_0) -> (E.expr -> 'a_1) -> E.expr -> ('a_0, 'a_1) Result.t
    val get_either :
      (E.expr -> 'a_0) -> (E.expr -> 'a_1) -> E.expr -> ('a_0, 'a_1) either
    val get_List_t : (E.expr -> 'a_0) -> E.expr -> 'a_0 List.t
    val get_Int_t : E.expr -> Int.t
    val get_Option_t : (E.expr -> 'a_0) -> E.expr -> 'a_0 Option.t
    val get_Real_t : E.expr -> Real.t
    val get_Map_t :
      (E.expr -> 'a_0) -> (E.expr -> 'a_1) -> E.expr -> ('a_0, 'a_1) Map.t
    val get_Multiset_t : (E.expr -> 'a_0) -> E.expr -> 'a_0 Multiset.t
    val get_Set_t : (E.expr -> 'a_0) -> E.expr -> 'a_0 Set.t
    val get_String_t : E.expr -> String.t
    val get_Float_t : E.expr -> Float.t
    val get_Model_message : E.expr -> Model.message
    val get_Model_counter_state : E.expr -> Model.counter_state
    val get_Decomp_State_machine_event : E.expr -> Decomp.State_machine.event
    val get_Decomp_State_machine_state : E.expr -> Decomp.State_machine.state
    val get_Decomp_Template_t : E.expr -> Decomp.Template.t
    val get_Decomp_Template_c : E.expr -> Decomp.Template.c
    type e_t = Decomp.State_machine.event list
    type extract_type = { e : e_t; }
    val ret_e : extract_type -> e_t
    val of_model :
      ?signature:string ->
      Imandra_surface.Top_result.term_model -> extract_type
  end
- : unit = ()
module D :
  sig
    module Symbolic :
      sig
        module DSM :
          sig
            module State_machine :
              sig
                type state = Decomp.State_machine.state
                type event = Decomp.State_machine.event
                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 : DSM.State_machine.state -> string
        type target = DSM.Template.t list
        type step = Imandra_tools__Idf.Make(Decomp).Symbolic.step
        type node = Imandra_tools__Idf.Make(Decomp).Symbolic.node
        type edge = node * step * node
        type path = edge list
        type paths = Imandra_tools__Idf.Make(Decomp).Symbolic.paths
        type scheduler = Imandra_tools__Idf.Make(Decomp).Symbolic.scheduler
        type traversal =
          Imandra_tools__Idf.Make(Decomp).Symbolic.traversal =
            DF
          | BF
        module G :
          sig
            type t = Imandra_tools__Idf.Make(Decomp).Symbolic.G.t
            module V :
              sig
                type t = node
                val compare : t -> t -> int
                val hash : t -> int
                val equal : t -> t -> bool
                type label = node
                val create : label -> t
                val label : t -> label
              end
            type vertex = V.t
            module E :
              sig
                type t = node * step option * node
                val compare : t -> t -> int
                type vertex = vertex
                val src : t -> vertex
                val dst : t -> vertex
                type label = step option
                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
            val nb_edges : t -> int
            val out_degree : t -> vertex -> int
            val in_degree : t -> vertex -> int
            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 -> 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 output_graph : t -> file:string -> unit
          end
        type decompose =
            ?traversal:traversal ->
            ?g:G.t ->
            ?from:node ->
            ?basis:string list ->
            ?max_asm_lookahead:int ->
            ?max_ctx_simp:int ->
            ?reduce_symmetry:bool ->
            ?ctx_asm_simp:bool ->
            ?aggressive_rec:bool ->
            ?compound:bool -> target -> paths * (unit -> unit)
        val paths : ?from:node -> G.t -> path list
        val reify : int -> paths -> path list
        val reify_all : paths -> path list
        val regions : path -> Imandra_interactive.Decompose.t list
        val samples : path -> DSM.State_machine.event list
        val ids : path -> (Uuidm.t * Uuidm.t * Uuidm.t) list
        val replay :
          path ->
          (DSM.State_machine.state * DSM.State_machine.event *
           DSM.State_machine.state)
          list
        val decompose : ?lazily:bool -> decompose
        val decompose_par :
          ?active_regions:bool -> schedule:scheduler -> decompose
        val scheduler :
          ?imandra:string ->
          ?oneshot:bool ->
          par:int ->
          ?max_fail:int -> load:string -> idf:string -> unit -> scheduler
        module Worker : sig val start : sock_file:string -> unit -> unit end
      end
    module Sampling :
      sig
        module DSM :
          sig
            module State_machine :
              sig
                type state = Decomp.State_machine.state
                type event = Decomp.State_machine.event
                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 : DSM.State_machine.state -> string
        type target = DSM.Template.t list
        type step = Imandra_tools__Idf.Make(Decomp).Sampling.step
        type node = Imandra_tools__Idf.Make(Decomp).Sampling.node
        type edge = node * step * node
        type path = edge list
        type paths = Imandra_tools__Idf.Make(Decomp).Sampling.paths
        type scheduler = Imandra_tools__Idf.Make(Decomp).Sampling.scheduler
        type traversal =
          Imandra_tools__Idf.Make(Decomp).Sampling.traversal =
            DF
          | BF
        module G :
          sig
            type t = Imandra_tools__Idf.Make(Decomp).Sampling.G.t
            module V :
              sig
                type t = node
                val compare : t -> t -> int
                val hash : t -> int
                val equal : t -> t -> bool
                type label = node
                val create : label -> t
                val label : t -> label
              end
            type vertex = V.t
            module E :
              sig
                type t = node * step option * node
                val compare : t -> t -> int
                type vertex = vertex
                val src : t -> vertex
                val dst : t -> vertex
                type label = step option
                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
            val nb_edges : t -> int
            val out_degree : t -> vertex -> int
            val in_degree : t -> vertex -> int
            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 -> 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 output_graph : t -> file:string -> unit
          end
        type decompose =
            ?traversal:traversal ->
            ?g:G.t ->
            ?from:node ->
            ?basis:string list ->
            ?max_asm_lookahead:int ->
            ?max_ctx_simp:int ->
            ?reduce_symmetry:bool ->
            ?ctx_asm_simp:bool ->
            ?aggressive_rec:bool ->
            ?compound:bool -> target -> paths * (unit -> unit)
        val paths : ?from:node -> G.t -> path list
        val reify : int -> paths -> path list
        val reify_all : paths -> path list
        val regions : path -> Imandra_interactive.Decompose.t list
        val samples : path -> DSM.State_machine.event list
        val ids : path -> (Uuidm.t * Uuidm.t * Uuidm.t) list
        val replay :
          path ->
          (DSM.State_machine.state * DSM.State_machine.event *
           DSM.State_machine.state)
          list
        val decompose : ?lazily:bool -> decompose
        val decompose_par :
          ?active_regions:bool -> schedule:scheduler -> decompose
        val scheduler :
          ?imandra:string ->
          ?oneshot:bool ->
          par:int ->
          ?max_fail:int -> load:string -> idf:string -> unit -> scheduler
        module Worker : sig val start : sock_file:string -> unit -> unit end
      end
  end
module IDF = D.Symbolic
- : unit = ()
val g___2 : Decomp.State_machine.event -> Decomp.State_machine.state -> bool =
  <fun>
val side_cond_g___3_2 :
  Decomp.State_machine.event list ->
  Decomp.State_machine.state -> int -> bool = <fun>
val side_cond_g___3_1 :
  Decomp.State_machine.event list ->
  Decomp.State_machine.state -> int -> bool = <fun>
val side_cond_g___3_0 :
  Decomp.State_machine.event list ->
  Decomp.State_machine.state -> int -> bool = <fun>
val target_g___3_2 :
  Decomp.State_machine.event list ->
  Decomp.State_machine.state -> Decomp.State_machine.state = <fun>
val target_g___3_1 :
  Decomp.State_machine.event list ->
  Decomp.State_machine.state -> Decomp.State_machine.state = <fun>
val target_g___3_0 :
  Decomp.State_machine.event list ->
  Decomp.State_machine.state -> Decomp.State_machine.state = <fun>
val paths : IDF.paths = <abstr>

Something odd has happened: we've asked Idf to decompose our template, but nothing happened!

This is because Idf is a lazy framework, we need to tell it how many paths we want to produce:

In [5]:
let first_path = IDF.reify 1i paths |> List.hd
Out[5]:
val g___4 : Decomp.State_machine.event list -> bool = <fun>
val g___5 : Decomp.State_machine.event list -> Decomp.State_machine.state =
  <fun>
val sc_g___6 : Decomp.State_machine.event list -> bool = <fun>
val sc_g___24 : Decomp.State_machine.event list -> bool = <fun>
val g___69 : Decomp.State_machine.event list -> bool = <fun>
val g___70 : Decomp.State_machine.event list -> Decomp.State_machine.state =
  <fun>
val sc_g___93 : Decomp.State_machine.event list -> bool = <fun>
val sc_g___129 : Decomp.State_machine.event list -> bool = <fun>
val g___200 : Decomp.State_machine.event list -> bool = <fun>
val g___201 : Decomp.State_machine.event list -> Decomp.State_machine.state =
  <fun>
val sc_g___237 : Decomp.State_machine.event list -> bool = <fun>
val sc_g___276 : Decomp.State_machine.event list -> bool = <fun>
val first_path : IDF.path =
  [(<abstr>, <abstr>, <abstr>); (<abstr>, <abstr>, <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
Out[6]:
- : (IDF.DSM.State_machine.state * IDF.DSM.State_machine.event *
     IDF.DSM.State_machine.state)
    list
=
[({Model.counter = 0; default = 23}, Model.Add 1337,
  {Model.counter = 1337; default = 23});
 ({Model.counter = 1337; default = 23}, Model.Add 1,
  {Model.counter = 23; default = 23});
 ({Model.counter = 23; default = 23}, Model.Reset,
  {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 at each event in the template):

In [7]:
#install_printer Decompose.print;;

let first_path_regions = IDF.regions first_path
Out[7]:
val first_path_regions : Imandra_interactive.Decompose.t list =
  [---[region]---
   Constraints:
    [e <> [];
     (List.tl e) <> [];
     (List.tl (List.tl e)) <> [];
     List.tl (List.tl (List.tl e)) = [];
     Is_a(Model.Add, List.hd (List.tl e));
     Is_a(Model.Add, List.hd e);
     not (Destruct(Model.Add, 0, List.hd e) <= 0);
     not (List.hd e = Model.Reset);
     Destruct(Model.Add, 0, List.hd e) <= 9000]
   Invariant:
    F =
    {Model.counter = Destruct(Model.Add, 0, List.hd e); Model.default = 23}
   -------------;
   ---[region]---
   Constraints:
    [not (Destruct(Model.Add, 0, List.hd (List.tl e)) <= 0);
     Destruct(Model.Add, 0, List.hd e) = 1337;
     e <> [];
     (List.tl e) <> [];
     (List.tl (List.tl e)) <> [];
     List.tl (List.tl (List.tl e)) = [];
     Is_a(Model.Add, List.hd (List.tl e));
     Is_a(Model.Add, List.hd e);
     not (Destruct(Model.Add, 0, List.hd e) <= 0);
     not (List.hd e = Model.Reset);
     Destruct(Model.Add, 0, List.hd e) <= 9000]
   Invariant:
    F = {Model.counter = 23; Model.default = 23}
   -------------;
   ---[region]---
   Constraints:
    [List.hd (List.tl (List.tl e)) = Model.Reset;
     not (Destruct(Model.Add, 0, List.hd (List.tl e)) <= 0);
     Destruct(Model.Add, 0, List.hd e) = 1337;
     e <> [];
     (List.tl e) <> [];
     (List.tl (List.tl e)) <> [];
     List.tl (List.tl (List.tl e)) = [];
     Is_a(Model.Add, List.hd (List.tl e));
     Is_a(Model.Add, List.hd e);
     not (Destruct(Model.Add, 0, List.hd e) <= 0);
     not (List.hd e = Model.Reset);
     Destruct(Model.Add, 0, List.hd e) <= 9000]
   Invariant:
    F = {Model.counter = 0; Model.default = 23}
   -------------]

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 Decompose.print 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]:
- : Imandra_interactive.Decompose.t list =
[---[region]---
 Constraints:
   [ (List.hd (List.tl e)) is Model.Add
   ; (List.hd e) is Model.Add
   ; (List.tl (List.tl (List.tl e))) = []
   ; 0 < Destruct(Model.Add, 0, (List.hd e)) <= 9000 ]
 Invariant:
   F =
   Model.{ counter = Destruct(Model.Add, 0, (List.hd e)) ; default = 23 }
  -------------;
 ---[region]---
 Constraints:
   [ (List.hd (List.tl e)) is Model.Add
   ; (List.hd e) is Model.Add
   ; Destruct(Model.Add, 0, (List.hd (List.tl e))) > 0
   ; Destruct(Model.Add, 0, (List.hd e)) = 1337
   ; (List.tl (List.tl (List.tl e))) = [] ]
 Invariant:
   F = Model.{ counter = 23 ; default = 23 }
  -------------;
 ---[region]---
 Constraints:
   [ (List.hd (List.tl (List.tl e))) is Model.Reset
   ; (List.hd (List.tl e)) is Model.Add
   ; (List.hd e) is Model.Add
   ; Destruct(Model.Add, 0, (List.hd (List.tl e))) > 0
   ; Destruct(Model.Add, 0, (List.hd e)) = 1337
   ; (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 rs = Decompose.top "f";;
Out[9]:
val f : int Set.t -> int Set.t -> int -> int Set.t = <fun>
val rs : Imandra_interactive.Decompose.t list =
  [---[region]---
   Constraints:
     [ y = (Set.union x y) ]
   Invariant:
     F = Map.add' x z true
    -------------;
   ---[region]---
   Constraints:
     [ y <> (Set.union x y) ]
   Invariant:
     F = Map.add' (Map.const false) z true
    -------------]
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 (y = Set.union x y)
Map.add' (Map.const false) z true
  • y = Set.union x y
Map.add' x z true

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 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.mem el 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 ("Map.add'", _) as ks when is_proper_set ks ->
     Custom (Set (gather_keys ks))

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

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

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

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

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

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

  | x -> x

and gather_keys = function
  | Funcall ("Map.add'", [m; k; Boolean true]) -> k::gather_keys m
  | Funcall ("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 Imandra_tools.Region_pp_intf.node_ list
    val map :
      (t Imandra_tools.Region_pp_intf.node_ ->
       t Imandra_tools.Region_pp_intf.node_) ->
      t -> t
    val compare : t -> t -> Imandra_tools.Region_pp_intf.comparison
    val print :
      t Imandra_tools.Region_pp_intf.node_ CCFormat.printer ->
      focus:'a -> CCFormat.t -> 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
val refine_ :
  PPrinter.custom Imandra_tools.Region_pp_intf.node_ ->
  PPrinter.custom Imandra_tools.Region_pp_intf.node_ = <fun>
val gather_keys :
  PPrinter.custom Imandra_tools.Region_pp_intf.node_ ->
  PPrinter.custom Imandra_tools.Region_pp_intf.node_ list = <fun>
val is_proper_set :
  PPrinter.custom Imandra_tools.Region_pp_intf.node_ -> bool = <fun>
val refine : PPrinter.node -> PPrinter.node CCList.t = <fun>
val print :
  Format.formatter -> Imandra_surface.Top_result.decompose_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]:
- : Imandra_interactive.Decompose.t list =
[---[region]---
 Constraints:
   [ (Set.subset x y) = true ]
 Invariant:
   F = Set.add x z
  -------------;
 ---[region]---
 Constraints:
   [ (Set.subset x y) = false ]
 Invariant:
   F = { z }
  -------------]

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 @@ Decompose_region.constraints region in
  let body = Region_term_synth.synthesize ~default:Term.Syn.False term in
  let args = Decompose_region.args region |> List.map Var.name |> String.concat " " in
  let func = Printf.sprintf "let %s %s = %s" gs args body in
  Reflect.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.t 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 = false
- : bool = true
- : bool = false
- : bool = true

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___277 : 'a Set.t -> 'a Set.t -> 'b -> int = <fun>
- : unit = ()
val idx : (int * Imandra_surface.Decompose_region.t) list =
  [(0i,
    ---[region]---
    Constraints:
      [ (Set.subset x y) = true ]
    Invariant:
      F = Set.add x z
     -------------);
   (1i,
    ---[region]---
    Constraints:
      [ (Set.subset x y) = false ]
    Invariant:
      F = { z }
     -------------)]
val indexer : int Set.t * int Set.t * int -> int = <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]:
- : Imandra_surface.Decompose_region.t =
---[region]---
Constraints:
  [ (Set.subset x y) = true ]
Invariant:
  F = Set.add x z
 -------------

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 * Q.t * Z.t
val f' : obj * real * Z.t -> Z.t * 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 * Q.t * Z.t = <fun>
- : obj * Q.t * Z.t =
({colour = Green; broken = false}, 4247389058177329/562949953421312, 9)

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 regions = Decompose.top "f'" [@@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 regions : Imandra_interactive.Decompose.t list =
  [---[region]---
   Constraints:
     [ _x[0].colour is Red
     ; _x[0].broken
     ; _x[1] > 37/2 ]
   Invariant:
     F = (_x[2], 141/10)
    -------------;
   ---[region]---
   Constraints:
     [ _x[0].colour is Red
     ; _x[0].broken
     ; _x[1] <= 37/2 ]
   Invariant:
     F = (_x[2], 141/10)
    -------------;
   ---[region]---
   Constraints:
     [ _x[0].colour is Red
     ; not _x[0].broken
     ; _x[1] > 37/2 ]
   Invariant:
     F = (7, 141/10)
    -------------;
   ---[region]---
   Constraints:
     [ _x[0].colour is Red
     ; not _x[0].broken
     ; _x[1] <= 37/2 ]
   Invariant:
     F = (7, 141/10)
    -------------;
   ---[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 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), 141/10)
    -------------]
module Example :
  sig
    type domain = dom
    val get_probs :
      Imandra_surface.Decompose_region.t list ->
      ?assuming:string ->
      ?n:Z.t ->
      ?d:string ->
      ?step_function:(domain -> domain) ->
      ?num_steps:Z.t ->
      unit -> (int, float * Imandra_surface.Decompose_region.t) Hashtbl.t
    val query :
      (domain -> bool) ->
      ?n:Z.t ->
      ?d:string -> ?max_std_err:Q.t -> ?precision:Z.t -> unit -> unit
    val save : string -> ?n:Z.t -> ?d:domain list -> unit -> unit
    val load : string -> domain list
  end
val g___292 : obj * real * 'a -> int = <fun>
- : unit = ()
val probs : (int, float * Imandra_surface.Decompose_region.t) Hashtbl.t =
  <abstr>
Region   Probability
6        0.1407
2        0.0132
7        0.2155
3        0.2798
5        0.0578
4        0.0876
0        0.1253
1        0.0801

- : 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
ConstraintsInvariant
  • not (_x.0.colour = Red)
  • _x.1 <=. 37/2
  • not (_x.0.colour = Green)
(2 * _x.2, 141/10)
  • not (_x.0.colour = Red)
  • _x.1 <=. 37/2
  • _x.0.colour = Green
(2 * _x.2, -39/5 +. _x.1)
  • not (_x.0.colour = Red)
  • not (_x.1 <=. 37/2)
  • not (_x.0.colour = Blue)
  • _x.0.colour = Green
(2 * _x.2, -39/5 +. _x.1)
  • not (_x.0.colour = Red)
  • not (_x.1 <=. 37/2)
  • _x.0.colour = Blue
(2 * _x.2, 43/10 +. _x.1)
  • _x.0.colour = Red
  • not _x.0.broken
  • _x.1 <=. 37/2
  • not (_x.0.colour = Green)
(7, 141/10)
  • _x.0.colour = Red
  • not _x.0.broken
  • not (_x.1 <=. 37/2)
  • not (_x.0.colour = Blue)
  • not (_x.0.colour = Green)
(7, 141/10)
  • _x.0.colour = Red
  • _x.0.broken
  • _x.1 <=. 37/2
  • not (_x.0.colour = Green)
(_x.2, 141/10)
  • _x.0.colour = Red
  • _x.0.broken
  • not (_x.1 <=. 37/2)
  • not (_x.0.colour = Blue)
  • not (_x.0.colour = Green)
(_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.