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.

Try this!

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
    module Term_utils = Imandra_tools.Term_utils
  end

Great! Let's start exploring imandra-tools.

Idf
Region_pp
Region_term_synth
Region_idx
Region_probs

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.

Try this!

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 Z.t | Sub of Z.t | Reset
    type counter_state = { counter : Z.t; default : Z.t; }
    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

Try this!

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
    type state = State_machine.state
    let concrete c t _state = 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
        type state = State_machine.state
        val concrete : t -> c -> 'a -> 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:

Try this!

In [4]:

#program;;

module IDF = Idf.Make(Decomp);;

let g = IDF.decompose (Decomp.Template.[Any;Add;Any]);;

Out[4]:

val root_ZlVYS2hhbVhQYlQzOXpQbVIwN3dhMWQ3aVdoZ2h2OVN5REVLdFNWeGVVWQ :
  Model.message list -> Model.counter_state = <fun>
module IDF :
  sig
    type shape = Imandra_tools.Idf.Make(Decomp).shape = Tree
    type pol =
      Imandra_tools.Idf.Make(Decomp).pol =
        Valid
      | Invalid
      | No
      | Custom of string
    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 state = State_machine.state
            type t = Decomp.Template.t
            type c = State_machine.event
            val concrete : t -> c -> state -> bool
          end
        val module_name : string
      end
    val pp_state : Model.counter_state -> string
    type target = DSM.Template.t list
    type node = Imandra_tools.Idf.Make(Decomp).node
    type path = node list
    module G :
      sig
        type t = Imandra_tools.Idf.Make(Decomp).G.t
        module V :
          sig
            type t = node
            val compare : t -> t -> int
            val hash : t -> int
            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 = Imandra_tools.Idf.Make(Decomp).G.E.t
            val compare : t -> t -> int
            type vertex = node
            val src : t -> vertex
            val dst : t -> vertex
            type label = Imandra_tools.Idf.Make(Decomp).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
        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 leaves : t -> vertex list
        val output_graph : t -> file:string -> unit
      end
    module Mex :
      sig val of_model : Top_result.model -> Model.message list end
    type region_id = int
    val id : node -> region_id
    val paths : ?from:node -> G.t -> path list
    val region : node -> Modular_region.RRef.t
    val concrete_region : node -> Top_result.modular_region
    val expanded_region_ids : node -> Util.Int_set.t
    val applied_expander_fns : node -> Util.Str_set.t list
    val sample : node -> Model.message list option
    val model : node -> Top_result.model option
    type region_expander =
      Imandra_tools.Idf.Make(Decomp).region_expander = {
      valid_fn : string option;
      field_projections : string list list;
      expand_when : string option;
    }
    type target_step =
      Imandra_tools.Idf.Make(Decomp).target_step = {
      event : DSM.Template.t;
      valid_pol : pol;
      region_expander : region_expander option;
    }
    val target_steps : node -> target_step list list
    type replay_sample =
      Imandra_tools.Idf.Make(Decomp).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 option
    type runner = Imandra_tools.Idf.Make(Decomp).runner
    val create :
      ?basis:string list ->
      ?expanding:string list ->
      ?assuming:string ->
      ?rule_specs:string list ->
      ?get_model_config:Logic_config.op list -> unit -> runner
    val add :
      runner:runner ->
      ?as_:shape ->
      ?prune_asm:bool ->
      ?valid_pol:pol list ->
      ?region_expander:region_expander list ->
      ?minimize:string list list -> ?shrink_heavy:bool -> target -> unit
    val run : runner -> G.t
    val decompose :
      ?as_:shape ->
      ?prune_asm:bool ->
      ?basis:string list ->
      ?expanding:string list ->
      ?assuming:string ->
      ?rule_specs:string list ->
      ?valid_pol:pol list ->
      ?region_expander:region_expander list ->
      ?minimize:string list list ->
      ?shrink_heavy:bool ->
      ?get_model_config:Logic_config.op list -> target -> G.t
  end
val guard__ZlVYS2hhbVhQYlQzOXpQbVIwN3dhMWQ3aVdoZ2h2OVN5REVLdFNWeGVVWQ_RGVjb21wLlRlbXBsYXRlLkFueTpWYWxpZA_true :
  Model.message list -> bool = <fun>
val target__ZlVYS2hhbVhQYlQzOXpQbVIwN3dhMWQ3aVdoZ2h2OVN5REVLdFNWeGVVWQ_RGVjb21wLlRlbXBsYXRlLkFueTpWYWxpZA_true :
  Model.message list -> Model.counter_state = <fun>
val guard__ZlVYS2hhbVhQYlQzOXpQbVIwN3dhMWQ3aVdoZ2h2OVN5REVLdFNWeGVVWQ_RGVjb21wLlRlbXBsYXRlLkFueTpWYWxpZCxEZWNvbXAuVGVtcGxhdGUuQW55OlZhbGlkRGVjb21wLlRlbXBsYXRlLkFkZDpWYWxpZA_true :
  Model.message list -> bool = <fun>
val target__ZlVYS2hhbVhQYlQzOXpQbVIwN3dhMWQ3aVdoZ2h2OVN5REVLdFNWeGVVWQ_RGVjb21wLlRlbXBsYXRlLkFueTpWYWxpZCxEZWNvbXAuVGVtcGxhdGUuQW55OlZhbGlkRGVjb21wLlRlbXBsYXRlLkFkZDpWYWxpZA_true :
  Model.message list -> Model.counter_state = <fun>
val guard__ZlVYS2hhbVhQYlQzOXpQbVIwN3dhMWQ3aVdoZ2h2OVN5REVLdFNWeGVVWQ_RGVjb21wLlRlbXBsYXRlLkFueTpWYWxpZCxEZWNvbXAuVGVtcGxhdGUuQW55OlZhbGlkRGVjb21wLlRlbXBsYXRlLkFkZDpWYWxpZCxEZWNvbXAuVGVtcGxhdGUuQW55OlZhbGlkRGVjb21wLlRlbXBsYXRlLkFkZDpWYWxpZERlY29tcC5UZW1wbGF0ZS5Bbnk6VmFsaWQ_true :
  Model.message list -> bool = <fun>
val target__ZlVYS2hhbVhQYlQzOXpQbVIwN3dhMWQ3aVdoZ2h2OVN5REVLdFNWeGVVWQ_RGVjb21wLlRlbXBsYXRlLkFueTpWYWxpZCxEZWNvbXAuVGVtcGxhdGUuQW55OlZhbGlkRGVjb21wLlRlbXBsYXRlLkFkZDpWYWxpZCxEZWNvbXAuVGVtcGxhdGUuQW55OlZhbGlkRGVjb21wLlRlbXBsYXRlLkFkZDpWYWxpZERlY29tcC5UZW1wbGF0ZS5Bbnk6VmFsaWQ_true :
  Model.message list -> Model.counter_state = <fun>
val g : IDF.G.t = <abstr>

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:

Try this!

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>];[...;...;...;...]]
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:

Try this!

In [6]:

IDF.replay (first_path |> CCList.last_opt |> CCOption.get_exn_or "no paths")

Out[6]:

- : IDF.replay_sample list option =
Some
 [{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 1;
   state_after = {Model.counter = 1; default = 23}};
  {IDF.state_before = {Model.counter = 1; default = 23}; event = Model.Sub 1;
   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):

Try this!

In [7]:

let first_path_regions = List.map (fun n -> Remote_ref.get_shared_block (IDF.region n)) first_path

Out[7]:

val first_path_regions : Top_result.modular_region list =
  [{Constraints:
      []
    Invariant:
      {Model.counter = 0; Model.default = 23}};
   {Constraints:
      [e <> [] &&
       Is_a(Model.Reset, List.hd e) &&
       not Is_a(Model.Add, List.hd e)]
    Invariant:
      {Model.counter = 0; Model.default = 23}};
   {Constraints:
      [Destruct(Model.Add, 0, List.hd (List.tl e)) > 0 &&
       (List.tl e) <> [] &&
       e <> [] &&
       Is_a(Model.Reset, List.hd e) &&
       not Is_a(Model.Add, List.hd e) &&
       not (0 + Destruct(Model.Add, 0, List.hd (List.tl e)) > 9000) &&
       Is_a(Model.Add, List.hd (List.tl e))]
    Invariant:
      {Model.counter = 0 + Destruct(Model.Add, 0, List.hd (List.tl e));
       Model.default = 23}};
   {Constraints:
      [let (_x_0 : Decomp.State_machine.event list) = List.tl e in
       Destruct(Model.Sub, 0, List.hd (List.tl _x_0))
       <= 0 + Destruct(Model.Add, 0, List.hd _x_0) &&
       (List.tl (List.tl e)) <> [] &&
       Destruct(Model.Add, 0, List.hd (List.tl e)) > 0 &&
       (List.tl e) <> [] &&
       e <> [] &&
       Is_a(Model.Reset, List.hd e) &&
       not Is_a(Model.Add, List.hd e) &&
       not (0 + Destruct(Model.Add, 0, List.hd (List.tl e)) > 9000) &&
       Is_a(Model.Add, List.hd (List.tl e)) &&
       Destruct(Model.Sub, 0, List.hd (List.tl (List.tl e))) > 0 &&
       let (_x_0 : Decomp.State_machine.event list) = List.tl e in
       not
       (Destruct(Model.Sub, 0, List.hd (List.tl _x_0))
        > 0 + Destruct(Model.Add, 0, List.hd _x_0)) &&
       not Is_a(Model.Reset, List.hd (List.tl (List.tl e))) &&
       not Is_a(Model.Add, List.hd (List.tl (List.tl e))) &&
       not (0 + Destruct(Model.Add, 0, List.hd (List.tl e)) = 1337)]
    Invariant:
      let (_x_0 : Decomp.State_machine.event list) = List.tl e in
      {Model.counter =
       (0 + Destruct(Model.Add, 0, List.hd _x_0))
       - Destruct(Model.Sub, 0, List.hd (List.tl _x_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 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:

Try this!

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) = Model.Reset ]
 Invariant:
   F = Model.{ counter = 0 ; default = 23 }
  -------------;
 ---[region]---
 Constraints:
   [ (List.hd (List.tl e)) is Model.Add
   ; 0 < Destruct(Model.Add, 0, (List.hd (List.tl e))) <= 9000
   ; (List.hd e) = Model.Reset ]
 Invariant:
   F =
   Model.{
     counter = Destruct(Model.Add, 0, (List.hd (List.tl e)))
   ; default = 23
   }
  -------------;
 ---[region]---
 Constraints:
   [ (List.hd (List.tl e)) is Model.Add
   ; (List.hd (List.tl (List.tl e))) is Model.Sub
   ; Destruct(Model.Add, 0, (List.hd (List.tl e))) >=
       Destruct(Model.Sub, 0, (List.hd (List.tl (List.tl e))))
   ; 0 < Destruct(Model.Add, 0, (List.hd (List.tl e))) <= 9000
   ; (List.hd e) = Model.Reset
   ; Destruct(Model.Sub, 0, (List.hd (List.tl (List.tl e)))) > 0
   ; Destruct(Model.Add, 0, (List.hd (List.tl e))) <> 1337 ]
 Invariant:
   F =
   Model.{
     counter =
       Destruct(Model.Add, 0, (List.hd (List.tl e))) -
         Destruct(Model.Sub, 0, (List.hd (List.tl (List.tl e))))
   ; 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:

Try this!

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";;

Modular_decomp.get_concrete d;;

let rs = Modular_decomp.get_concrete_regions d;;

Out[9]:

val f : Z.t Set.t -> Z.t Set.t -> Z.t -> Z.t Set.t = <fun>
val d : Modular_decomp_intf.decomp_ref = <abstr>
- : Modular_decomp_intf.decomp =
(decomp (f x, y, z
 :regions ((<reg 0>
            ---[region]---
            Constraints:
              [ Set.subset x y ]
            Invariant:
              F = Set.add z x
             -------------),
           (<reg 1>
            ---[region]---
            Constraints:
              [ not (Set.subset x y) ]
            Invariant:
              F = { z }
             -------------)))
val rs : Top_result.modular_region list =
  [---[region]---
   Constraints:
     [ Set.subset x y ]
   Invariant:
     F = Set.add z x
    -------------;
   ---[region]---
   Constraints:
     [ not (Set.subset x y) ]
   Invariant:
     F = { z }
    -------------]

Voronoi (2 of 2)
Table

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_id	Constraints	Invariant
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:

Try this!

In [10]:

open Region_pp_intf

module Custom = struct

  type ty = string

  type c = Set of (ty, c) 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 TY = Region_pp.String_conv

module PPrinter = Region_pp.Make (TY) (Custom)
open Custom
open PPrinter

let to_curried_types : PPrinter.ty -> PPrinter.ty list =
 fun t -> CCString.split ~by:"->" t |> CCList.map CCString.trim

let from_curried_types : PPrinter.ty list -> PPrinter.ty =
  CCString.concat " -> "

let get_input_types : PPrinter.ty list -> ty list =
  let open Caml in
  fun t -> CCList.take (CCList.length t - 1i) t

let rec refine_ n =
  let union_to_subset ty =
    let bool_type = TY.translate_imandra_type Type.bool in
    let types_of_union_input = to_curried_types ty |> get_input_types in
    let subset_type = types_of_union_input @ [ bool_type ] in
    from_curried_types subset_type
  in
  match view n with
  | Funcall ({ view = Var "Map.add'"; _ }, _) when is_proper_set n ->
    mk ~ty:n.ty (Custom (Set (gather_keys n)))
  | Funcall ({ view = Var "Map.add'"; ty }, [ m; k; { view = Boolean true; _ } ])
    ->
    mk ~ty:n.ty (Funcall (mk ~ty (Var "Set.add"), [ m; k ]))
    (* verify (fun x y -> Set.union x y = y ==> Set.subset x y)  *)
  | Eq ({ view = Funcall ({ view = Var "Set.union"; ty }, [ x; y ]); _ }, z)
    when Comparator.(is_eq (compare y z)) ->
    let ty = union_to_subset ty in
    mk ~ty:n.ty
      (Eq
         ( mk ~ty:n.ty (Funcall (mk ~ty (Var "Set.subset"), [ x; y ])),
           mk ~ty:n.ty (Boolean true) ))
  | Neq ({ view = Funcall ({ view = Var "Set.union"; ty }, [ x; y ]); _ }, z)
    when Comparator.(is_eq (compare y z)) ->
    let ty = union_to_subset ty in
    mk ~ty:n.ty
      (Eq
         ( mk ~ty:n.ty (Funcall (mk ~ty (Var "Set.subset"), [ x; y ])),
           mk ~ty:n.ty (Boolean false) ))
  | Eq (z, { view = Funcall ({ view = Var "Set.union"; ty }, [ x; y ]); _ })
    when Comparator.(is_eq (compare y z)) ->
    let ty = union_to_subset ty in
    mk ~ty:n.ty
      (Eq
         ( mk ~ty:n.ty (Funcall (mk ~ty (Var "Set.subset"), [ x; y ])),
           mk ~ty:n.ty (Boolean true) ))
  | Neq (z, { view = Funcall ({ view = Var "Set.union"; ty }, [ x; y ]); _ })
    when Comparator.(is_eq (compare y z)) ->
    mk ~ty:n.ty
      (Eq
         ( mk ~ty:n.ty (Funcall (mk ~ty (Var "Set.subset"), [ x; y ])),
           mk ~ty:n.ty (Boolean false) ))
  | _ -> n

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

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 ty = string
    type c = Set of (ty, c) node list
    val map : ((ty, c) node -> (ty, c) node) -> c -> c
    val compare :
      ((ty, c) node -> (ty, c) node -> comparison) -> c -> c -> comparison
    val print : (ty, c) node Fmt.printer -> focus:'a -> Fmt.t -> c -> unit
  end
module TY = Imandra_tools.Region_pp.String_conv
module PPrinter :
  sig
    type custom = Custom.c
    type ty = string
    module TY :
      sig
        type ty = string
        val show : ty -> ty
        val equal : ty -> ty -> bool
        val translate_imandra_type : Type.t -> ty
        val mk_tuple : ty list -> ty
        val mk_list : ty -> ty
        val mk_func : ty list -> ty
        val type_var : ty -> ty
        val mk_set : ty -> ty
      end
    type nonrec node = (ty, custom) node
    type nonrec view = (ty, custom) view
    val view : node -> view
    val ty : node -> ty
    val mk : ty:ty -> view -> 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 -> ty list
    val has_symbolic_term : node -> bool
    module Printer :
      sig
        val print :
          ?p:(node Fmt.printer -> Fmt.t -> node -> unit option) ->
          ?focus:ty -> unit -> node Fmt.printer
        val to_string :
          ?p:(node Fmt.printer -> Fmt.t -> node -> unit option) ->
          ?focus:ty -> node -> ty
      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
        val propagate : node list -> node list
      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 Fmt.printer -> Fmt.t -> node -> unit option) ->
      ?skip_invariant:bool ->
      ?focus:ty -> unit -> Fmt.t -> Top_result.modular_region -> unit
    val to_string :
      ?unify:Unifier.unifier ->
      ?refine:refiner -> Top_result.modular_region -> ty
  end
val to_curried_types : ty -> ty list = <fun>
val from_curried_types : ty list -> ty = <fun>
val get_input_types : ty list -> ty list = <fun>
val refine_ : PPrinter.node -> PPrinter.node = <fun>
val gather_keys : PPrinter.node -> (ty, custom) Region_pp_intf.node list =
  <fun>
val is_proper_set : PPrinter.node -> bool = <fun>
val refine : PPrinter.node -> PPrinter.node list = <fun>
val print : Fmt.t -> 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:

Try this!

In [11]:

#install_printer print;;
rs

Out[11]:

- : Top_result.modular_region list =
[---[region]---
 Constraints:
   [ Set.subset x y ]
 Invariant:
   F = Set.add z x
  -------------;
 ---[region]---
 Constraints:
   [ not (Set.subset x y) ]
 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:

Try this!

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.(mk ~loc:Iloc.none 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>
- : ty 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:

Try this!

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.

Try this!

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

Try this!

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:

Try this!

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
val pp_colour : colour Fmt.printer = <fun>
val string_of_colour : colour -> ty = <fun>
type obj = { colour : colour; broken : bool; }
val pp_obj : obj Fmt.printer = <fun>
val string_of_obj : obj -> ty = <fun>
type dom = obj * real * Z.t
val pp_dom : dom Fmt.printer = <fun>
val string_of_dom : dom -> ty = <fun>
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:

Try this!

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 * Z.t = <fun>
- : obj * real * Z.t =
({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:

Try this!

In [18]:

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

let regions = Modular_decomp.get_concrete_regions d [@@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 : Modular_decomp_intf.decomp_ref = <abstr>
val regions : Top_result.modular_region list =
  [---[region]---
   Constraints:
     [ _x[1] > 37/2
     ; _x[0].broken
     ; _x[0].colour = Red ]
   Invariant:
     F = (_x[2], 141/10)
    -------------;
   ---[region]---
   Constraints:
     [ _x[1] <= 37/2
     ; _x[0].broken
     ; _x[0].colour = Red ]
   Invariant:
     F = (_x[2], 141/10)
    -------------;
   ---[region]---
   Constraints:
     [ _x[1] > 37/2
     ; not _x[0].broken
     ; _x[0].colour = Red ]
   Invariant:
     F = (7, 141/10)
    -------------;
   ---[region]---
   Constraints:
     [ _x[1] <= 37/2
     ; not _x[0].broken
     ; _x[0].colour = Red ]
   Invariant:
     F = (7, 141/10)
    -------------;
   ---[region]---
   Constraints:
     [ _x[1] > 37/2
     ; _x[0].colour = Blue ]
   Invariant:
     F = ((_x[2] * 2), (_x[1] + 43/10))
    -------------;
   ---[region]---
   Constraints:
     [ _x[1] > 37/2
     ; _x[0].colour = Green ]
   Invariant:
     F = ((_x[2] * 2), (_x[1] - 39/5))
    -------------;
   ---[region]---
   Constraints:
     [ _x[1] <= 37/2
     ; _x[0].colour = Green ]
   Invariant:
     F = ((_x[2] * 2), (_x[1] - 39/5))
    -------------;
   ---[region]---
   Constraints:
     [ _x[1] <= 37/2
     ; _x[0].colour = Blue ]
   Invariant:
     F = ((_x[2] * 2), 141/10)
    -------------]
module Example :
  sig
    type domain = dom
    val get_probs :
      Top_result.modular_region list ->
      ?assuming:ty ->
      ?n:Z.t ->
      ?d:ty ->
      ?step_function:(domain -> domain) ->
      ?num_steps:Z.t ->
      unit -> (int, float * Top_result.modular_region) Hashtbl.t
    val query :
      (domain -> bool) ->
      ?n:Z.t -> ?d:ty -> ?max_std_err:real -> ?precision:Z.t -> unit -> unit
    val save : ty -> ?n:Z.t -> ?d:domain list -> unit -> unit
    val load : ty -> domain list
  end
val g___23 : obj * real * 'a -> int = <fun>
- : unit = ()
val probs : (int, float * Top_result.modular_region) Hashtbl.t = <abstr>
Region   Probability
6        0.1449
2        0.0141
7        0.2147
3        0.2905
5        0.0516
4        0.0817
0        0.1292
1        0.0733

- : unit = ()

Voronoi (8 of 8)
Table

{
  "regions": [
    {
      "constraints": [ "_x[1] > 37/2" ],
      "region": null,
      "groups": [
        {
          "constraints": [ "_x[1] > 37/2", "_x[0].colour = Green" ],
          "region": {
            "constraints": [ "_x[1] > 37/2", "_x[0].colour = Green" ],
            "invariant": "F = ((_x[2] * 2), (_x[1] - 39/5))"
          },
          "groups": [],
          "label": "2",
          "weight": 1
        },
        {
          "constraints": [ "_x[1] > 37/2", "_x[0].colour = Blue" ],
          "region": {
            "constraints": [ "_x[1] > 37/2", "_x[0].colour = Blue" ],
            "invariant": "F = ((_x[2] * 2), (_x[1] + 43/10))"
          },
          "groups": [],
          "label": "1",
          "weight": 1
        }
      ],
      "label": "",
      "weight": 2
    },
    {
      "constraints": [ "_x[1] <= 37/2" ],
      "region": null,
      "groups": [
        {
          "constraints": [ "_x[1] <= 37/2", "_x[0].colour = Green" ],
          "region": {
            "constraints": [ "_x[1] <= 37/2", "_x[0].colour = Green" ],
            "invariant": "F = ((_x[2] * 2), (_x[1] - 39/5))"
          },
          "groups": [],
          "label": "2.2",
          "weight": 1
        },
        {
          "constraints": [ "_x[1] <= 37/2", "_x[0].colour = Blue" ],
          "region": {
            "constraints": [ "_x[1] <= 37/2", "_x[0].colour = Blue" ],
            "invariant": "F = ((_x[2] * 2), 141/10)"
          },
          "groups": [],
          "label": "2.1",
          "weight": 1
        }
      ],
      "label": "",
      "weight": 2
    },
    {
      "constraints": [ "_x[0].colour = Red" ],
      "region": null,
      "groups": [
        {
          "constraints": [
            "_x[0].colour = Red", "_x[1] > 37/2", "not _x[0].broken"
          ],
          "region": {
            "constraints": [
              "_x[1] > 37/2", "not _x[0].broken", "_x[0].colour = Red"
            ],
            "invariant": "F = (7, 141/10)"
          },
          "groups": [],
          "label": "1.3.1",
          "weight": 1
        },
        {
          "constraints": [
            "_x[0].colour = Red", "_x[1] <= 37/2", "not _x[0].broken"
          ],
          "region": {
            "constraints": [
              "_x[1] <= 37/2", "not _x[0].broken", "_x[0].colour = Red"
            ],
            "invariant": "F = (7, 141/10)"
          },
          "groups": [],
          "label": "1.2.1",
          "weight": 1
        },
        {
          "constraints": [ "_x[0].colour = Red", "_x[0].broken" ],
          "region": null,
          "groups": [
            {
              "constraints": [
                "_x[0].colour = Red", "_x[0].broken", "_x[1] > 37/2"
              ],
              "region": {
                "constraints": [
                  "_x[1] > 37/2", "_x[0].broken", "_x[0].colour = Red"
                ],
                "invariant": "F = (_x[2], 141/10)"
              },
              "groups": [],
              "label": "1.1.2",
              "weight": 1
            },
            {
              "constraints": [
                "_x[0].colour = Red", "_x[0].broken", "_x[1] <= 37/2"
              ],
              "region": {
                "constraints": [
                  "_x[1] <= 37/2", "_x[0].broken", "_x[0].colour = Red"
                ],
                "invariant": "F = (_x[2], 141/10)"
              },
              "groups": [],
              "label": "1.1.1",
              "weight": 1
            }
          ],
          "label": "",
          "weight": 2
        }
      ],
      "label": "",
      "weight": 4
    }
  ]
}

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_id	Constraints	Invariant
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.

An introduction to imandra-tools¶

Iterative Decomposition Framework (Idf)¶

Region Pretty Printer (Region_pp)¶

Region Term Synthesizer (Region_term_synth)¶

Region Indexer (Region_idx)¶

Region Probabilities (Region_probs)¶

An introduction to `imandra-tools`¶