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 Region_pp = Imandra_tools__Region_pp
    module Term_synth = Imandra_tools__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:

  • A variant type describing all the possible messages a model can react to (message)
  • A record 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.

The first thing we need to do is define a module implementing the Idf.SIG_TPL 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 pp_state function of state to string to serialize a state value (usually, for complex types, the Genpp module provided with imandra is used to automatically generate this function)
  • a module_name value mapping to the name of the module being defined (this is necessary for reflection purposes)
  • an enough_samples function (we'll gloss over describing what this does for now and defer to a more in-depth tutorial specific to Idf, a default implementation just returns true)
In [3]:
open Imandra_tools

module DecompositionConfig = 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

  let pp_state (state : state) : string =
    Printf.sprintf "{ counter = %s; default = %s }"
                   (Int.to_string state.counter)
                   (Int.to_string state.default)
    [@@program]

  let module_name = "DecompositionConfig"
  let enough_samples ~strategy ~arg ~region evs = true [@@program]
end
Out[3]:
module DecompositionConfig :
  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
    val pp_state : state -> string
    val module_name : string
    val enough_samples : strategy:'a -> arg:'b -> region:'c -> 'd -> bool
  end

The second thing we need to do is to define a Template module implementing the Idf.Template.SIG module signature:

  • a t variant type symbolically describing events from our model
  • a concrete function from t to a list of strings mapping the symbolic event to concrete event type names
In [4]:
module Template = struct
  type t = Add | Sub | Reset | Any

  let concrete = function
    | Add -> ["Model.Add"]
    | Sub -> ["Model.Sub"]
    | Reset -> ["Model.Reset"]
    | Any -> []
end
Out[4]:
module Template :
  sig type t = Add | Sub | Reset | Any val concrete : t -> string list end

We're now ready to create a decomposition recipe and apply it to an event template:

First we use Idf.mex_for to create an imandra Mex module (this is just a convenience function wrapping imandra's Extract module)

Second we can finally hook it all together by passing DecompositionConfig, Mex, and Template as parameters to the Idf.Make functor, and obtain a D module of signature Idf.SIG.

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

  • concrete: 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 [5]:
#program;;
                                   
Idf.mex_for DecompositionConfig.module_name () 
module D = Idf.Make(DecompositionConfig)(Mex)(Template)

let paths, _ = D.Symbolic.decompose (D.Template Template.[Any;Add;Any])
Out[5]:
val imandra_gensym__1 :
  DecompositionConfig.event list -> DecompositionConfig.state = <fun>
module Mex :
  sig
    module E = Imandra_interactive.Extract_frontend
    val get_option : (E.expr -> 'a_0) -> E.expr -> 'a_0 option
    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_DecompositionConfig_event : E.expr -> DecompositionConfig.event
    val get_DecompositionConfig_state : E.expr -> DecompositionConfig.state
    val get_Template_t : E.expr -> Template.t
    type e_t = DecompositionConfig.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
    type template = Template.t list
    type funs = Imandra_prelude.string list * Imandra_prelude.string list
    type target =
      Imandra_tools__Idf.Make(DecompositionConfig)(Mex)(Template).target =
        Template of template
      | Funs of funs
    module L :
      sig
        type 'a t =
            'a
            Imandra_tools__Idf.Make(DecompositionConfig)(Mex)(Template).L.t
        val lazily : (Imandra_prelude.unit -> 'a t) -> 'a t
        val reify : Imandra_prelude.Caml.Int.t -> 'a t -> 'a list
        val reify_all : 'a t -> 'a list
        val of_list : 'a list -> 'a t
        val of_gen : 'a Imandra_tools__Idf.gen -> 'a t
        val empty : 'a t
        val is_empty : 'a t -> bool
        val map : f:('a -> 'b) -> 'a t -> 'b t
        val flat_map : f:('a -> 'b t) -> 'a t -> 'b t
        val return : 'a -> 'a t
        val default : default:'a t -> 'a t -> 'a t
        val cons : 'a -> 'a t -> 'a t
      end
    module Gen :
      sig
        val funs_of_template : template -> funs
        val funs_of_steps : Imandra_prelude.string list list -> funs
        val target_of_funs : funs -> target
      end
    module Mex :
      sig
        type event = DecompositionConfig.event
        val events_of_region :
          arg:Imandra_prelude.Caml.Int.t ->
          signature:Imandra_prelude.string ->
          Imandra_tools__Idf.Decompose.t -> event Imandra_tools__Idf.gen
      end
    module Strategy :
      sig
        module Concrete :
          sig
            type state = DecompositionConfig.state
            type event = DecompositionConfig.event
            type node_t = DecompositionConfig.state
            type edge_t = DecompositionConfig.event
            val module_name : Imandra_prelude.string
            val root_node : node_t
            val node_tpl_for_target : node_t -> Imandra_prelude.string
            val node_tpl_for_side_cond : node_t -> Imandra_prelude.string
            val step_into_region :
              node:node_t ->
              signature:Imandra_prelude.string ->
              Imandra_prelude.Caml.Int.t ->
              Imandra_tools__Idf.Decompose.t ->
              (event * node_t) Imandra_tools__Idf.gen
            val strategy : Imandra_tools__Idf.strategy
          end
        type node_t =
          Imandra_tools__Idf.Make(DecompositionConfig)(Mex)(Template).Strategy.node_t =
            Expr of (Imandra_surface.Term.t * Imandra_surface.Term.t list)
          | Str of Imandra_prelude.string * Imandra_prelude.string
        module Symbolic :
          sig
            type state = DecompositionConfig.state
            type event = DecompositionConfig.event
            type node_t = node_t
            type edge_t = Imandra_surface.Term.t list
            val module_name : Imandra_prelude.string
            val root_node : node_t
            val node_tpl_for_target : node_t -> Imandra_prelude.string
            val node_tpl_for_side_cond : node_t -> Imandra_prelude.string
            val step_into_region :
              node:node_t ->
              signature:Imandra_prelude.string ->
              Imandra_prelude.Caml.Int.t ->
              Imandra_tools__Idf.Decompose.t ->
              (event * node_t) Imandra_tools__Idf.gen
            val strategy : Imandra_tools__Idf.strategy
          end
      end
    module type SIG =
      functor
        (S : sig
               type state = DecompositionConfig.state
               type event = DecompositionConfig.event
               type node_t
               type edge_t
               val module_name : Imandra_prelude.string
               val root_node : node_t
               val node_tpl_for_target : node_t -> Imandra_prelude.string
               val node_tpl_for_side_cond : node_t -> Imandra_prelude.string
               val step_into_region :
                 node:node_t ->
                 signature:Imandra_prelude.string ->
                 Imandra_prelude.Caml.Int.t ->
                 Imandra_tools__Idf.Decompose.t ->
                 (event * node_t) Imandra_tools__Idf.gen
               val strategy : Imandra_tools__Idf.strategy
             end) ->
        sig
          type decomp_step = {
            sample : S.event;
            region : Imandra_tools__Idf.Decompose.t;
            signature : Imandra_prelude.string;
          }
          type indexed_state = {
            state : S.node_t;
            idx : Imandra_prelude.Caml.Int.t;
          }
          module G :
            sig
              type t
              module V : Graph.Sig.VERTEX
              type vertex = V.t
              module E :
                sig
                  type t
                  val compare : t -> t -> int
                  type vertex = vertex
                  val src : t -> vertex
                  val dst : t -> vertex
                  type 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:Imandra_prelude.Caml.Int.t -> Imandra_prelude.unit -> t
              module type LH =
                sig
                  val decomp_step_hash :
                    decomp_step -> Imandra_prelude.Caml.Int.t
                  val indexed_state_hash :
                    indexed_state -> Imandra_prelude.Caml.Int.t
                  val decomp_step_label :
                    decomp_step -> Imandra_prelude.string
                  val indexed_state_label :
                    indexed_state -> Imandra_prelude.string
                end
              module type SIG =
                sig
                  val output_graph :
                    t -> Imandra_prelude.string -> Imandra_prelude.unit
                  val find_edges :
                    t -> Imandra_prelude.Caml.Int.t -> decomp_step list
                  val find_vertices :
                    t -> Imandra_prelude.Caml.Int.t -> indexed_state list
                end
              val root : t -> vertex
              module Make : functor (L : LH) -> SIG
            end
          type step = indexed_state * decomp_step * indexed_state
          type path = step list
          type t = path L.t * G.t option
          val paths : ?v:G.vertex -> G.t -> path L.t
          val region_of_path : path -> Imandra_tools__Idf.Decompose.t list
          val regions : path L.t -> Imandra_tools__Idf.Decompose.t list L.t
          val replay_path : path -> (S.state * S.event * S.state) list
          type decomp_data =
              S.event * S.node_t * Imandra_tools__Idf.Decompose.t
          type 'a prod = [ `Prod of 'a ]
          type consumable_step =
              (decomp_data * step * bool) *
              (Imandra_prelude.unit -> consumable_step L.t prod)
          val decompose_one :
            ?g:G.t ->
            ?root:S.node_t ->
            ?idx:Imandra_prelude.Caml.Int.t ->
            ?basis:Imandra_prelude.string list ->
            ?max_asm_lookahead:Imandra_prelude.Caml.Int.t ->
            ?max_ctx_simp:Imandra_prelude.Caml.Int.t ->
            ?reduce_symmetry:bool ->
            ?ctx_asm_simp:bool ->
            ?aggressive_rec:bool ->
            ?compound:bool -> target -> consumable_step L.t
          val node_of_consumable_step : consumable_step -> S.node_t
          val decompose :
            ?g:G.t ->
            ?root:S.node_t ->
            ?idx:Imandra_prelude.Caml.Int.t ->
            ?cache_convergent_paths:bool ->
            ?include_partials:bool ->
            ?basis:Imandra_prelude.string list ->
            ?max_asm_lookahead:Imandra_prelude.Caml.Int.t ->
            ?max_ctx_simp:Imandra_prelude.Caml.Int.t ->
            ?reduce_symmetry:bool ->
            ?ctx_asm_simp:bool ->
            ?aggressive_rec:bool -> ?compound:bool -> target -> t
        end
    module WithStrategy :
      functor
        (S : sig
               type state = DecompositionConfig.state
               type event = DecompositionConfig.event
               type node_t
               type edge_t
               val module_name : Imandra_prelude.string
               val root_node : node_t
               val node_tpl_for_target : node_t -> Imandra_prelude.string
               val node_tpl_for_side_cond : node_t -> Imandra_prelude.string
               val step_into_region :
                 node:node_t ->
                 signature:Imandra_prelude.string ->
                 Imandra_prelude.Caml.Int.t ->
                 Imandra_tools__Idf.Decompose.t ->
                 (event * node_t) Imandra_tools__Idf.gen
               val strategy : Imandra_tools__Idf.strategy
             end) ->
        sig
          type decomp_step =
            Imandra_tools__Idf.Make(DecompositionConfig)(Mex)(Template).WithStrategy(S).decomp_step = {
            sample : S.event;
            region : Imandra_tools__Idf.Decompose.t;
            signature : Imandra_prelude.string;
          }
          type indexed_state =
            Imandra_tools__Idf.Make(DecompositionConfig)(Mex)(Template).WithStrategy(S).indexed_state = {
            state : S.node_t;
            idx : Imandra_prelude.Caml.Int.t;
          }
          module G :
            sig
              type t =
                  Imandra_tools__Idf.Make(DecompositionConfig)(Mex)(Template).WithStrategy(S).G.t
              module V :
                sig
                  type t =
                      Imandra_tools__Idf.Make(DecompositionConfig)(Mex)(Template).WithStrategy(S).G.V.t
                  val compare : t -> t -> int
                  val hash : t -> int
                  val equal : t -> t -> bool
                  type label =
                      Imandra_tools__Idf.Make(DecompositionConfig)(Mex)(Template).WithStrategy(S).G.V.label
                  val create : label -> t
                  val label : t -> label
                end
              type vertex = V.t
              module E :
                sig
                  type t =
                      Imandra_tools__Idf.Make(DecompositionConfig)(Mex)(Template).WithStrategy(S).G.E.t
                  val compare : t -> t -> int
                  type vertex = vertex
                  val src : t -> vertex
                  val dst : t -> vertex
                  type label =
                      Imandra_tools__Idf.Make(DecompositionConfig)(Mex)(Template).WithStrategy(S).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:Imandra_prelude.Caml.Int.t -> Imandra_prelude.unit -> t
              module type LH =
                sig
                  val decomp_step_hash :
                    decomp_step -> Imandra_prelude.Caml.Int.t
                  val indexed_state_hash :
                    indexed_state -> Imandra_prelude.Caml.Int.t
                  val decomp_step_label :
                    decomp_step -> Imandra_prelude.string
                  val indexed_state_label :
                    indexed_state -> Imandra_prelude.string
                end
              module type SIG =
                sig
                  val output_graph :
                    t -> Imandra_prelude.string -> Imandra_prelude.unit
                  val find_edges :
                    t -> Imandra_prelude.Caml.Int.t -> decomp_step list
                  val find_vertices :
                    t -> Imandra_prelude.Caml.Int.t -> indexed_state list
                end
              val root : t -> vertex
              module Make :
                functor (L : LH) ->
                  sig
                    val output_graph :
                      t -> Imandra_prelude.string -> Imandra_prelude.unit
                    val find_edges :
                      t -> Imandra_prelude.Caml.Int.t -> decomp_step list
                    val find_vertices :
                      t -> Imandra_prelude.Caml.Int.t -> indexed_state list
                  end
            end
          type step = indexed_state * decomp_step * indexed_state
          type path = step list
          type t = path L.t * G.t option
          val paths : ?v:G.vertex -> G.t -> path L.t
          val region_of_path : path -> Imandra_tools__Idf.Decompose.t list
          val regions : path L.t -> Imandra_tools__Idf.Decompose.t list L.t
          val replay_path : path -> (S.state * S.event * S.state) list
          type decomp_data =
              S.event * S.node_t * Imandra_tools__Idf.Decompose.t
          type 'a prod = [ `Prod of 'a ]
          type consumable_step =
              (decomp_data * step * bool) *
              (Imandra_prelude.unit -> consumable_step L.t prod)
          val decompose_one :
            ?g:G.t ->
            ?root:S.node_t ->
            ?idx:Imandra_prelude.Caml.Int.t ->
            ?basis:Imandra_prelude.string list ->
            ?max_asm_lookahead:Imandra_prelude.Caml.Int.t ->
            ?max_ctx_simp:Imandra_prelude.Caml.Int.t ->
            ?reduce_symmetry:bool ->
            ?ctx_asm_simp:bool ->
            ?aggressive_rec:bool ->
            ?compound:bool -> target -> consumable_step L.t
          val node_of_consumable_step : consumable_step -> S.node_t
          val decompose :
            ?g:G.t ->
            ?root:S.node_t ->
            ?idx:Imandra_prelude.Caml.Int.t ->
            ?cache_convergent_paths:bool ->
            ?include_partials:bool ->
            ?basis:Imandra_prelude.string list ->
            ?max_asm_lookahead:Imandra_prelude.Caml.Int.t ->
            ?max_ctx_simp:Imandra_prelude.Caml.Int.t ->
            ?reduce_symmetry:bool ->
            ?ctx_asm_simp:bool ->
            ?aggressive_rec:bool -> ?compound:bool -> target -> t
        end
    module Concrete :
      sig
        type decomp_step =
          WithStrategy(Strategy.Concrete).decomp_step = {
          sample : Strategy.Concrete.event;
          region : Imandra_tools__Idf.Decompose.t;
          signature : Imandra_prelude.string;
        }
        type indexed_state =
          WithStrategy(Strategy.Concrete).indexed_state = {
          state : Strategy.Concrete.node_t;
          idx : Imandra_prelude.Caml.Int.t;
        }
        module G :
          sig
            type t = WithStrategy(Strategy.Concrete).G.t
            module V :
              sig
                type t = WithStrategy(Strategy.Concrete).G.V.t
                val compare : t -> t -> int
                val hash : t -> int
                val equal : t -> t -> bool
                type label = WithStrategy(Strategy.Concrete).G.V.label
                val create : label -> t
                val label : t -> label
              end
            type vertex = V.t
            module E :
              sig
                type t = WithStrategy(Strategy.Concrete).G.E.t
                val compare : t -> t -> int
                type vertex = vertex
                val src : t -> vertex
                val dst : t -> vertex
                type label = WithStrategy(Strategy.Concrete).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:Imandra_prelude.Caml.Int.t -> Imandra_prelude.unit -> t
            module type LH =
              sig
                val decomp_step_hash :
                  decomp_step -> Imandra_prelude.Caml.Int.t
                val indexed_state_hash :
                  indexed_state -> Imandra_prelude.Caml.Int.t
                val decomp_step_label : decomp_step -> Imandra_prelude.string
                val indexed_state_label :
                  indexed_state -> Imandra_prelude.string
              end
            module type SIG =
              sig
                val output_graph :
                  t -> Imandra_prelude.string -> Imandra_prelude.unit
                val find_edges :
                  t -> Imandra_prelude.Caml.Int.t -> decomp_step list
                val find_vertices :
                  t -> Imandra_prelude.Caml.Int.t -> indexed_state list
              end
            val root : t -> vertex
            module Make :
              functor (L : LH) ->
                sig
                  val output_graph :
                    t -> Imandra_prelude.string -> Imandra_prelude.unit
                  val find_edges :
                    t -> Imandra_prelude.Caml.Int.t -> decomp_step list
                  val find_vertices :
                    t -> Imandra_prelude.Caml.Int.t -> indexed_state list
                end
          end
        type step = indexed_state * decomp_step * indexed_state
        type path = step list
        type t = path L.t * G.t option
        val paths : ?v:G.vertex -> G.t -> path L.t
        val region_of_path : path -> Imandra_tools__Idf.Decompose.t list
        val regions : path L.t -> Imandra_tools__Idf.Decompose.t list L.t
        val replay_path :
          path ->
          (Strategy.Concrete.state * Strategy.Concrete.event *
           Strategy.Concrete.state)
          list
        type decomp_data =
            Strategy.Concrete.event * Strategy.Concrete.node_t *
            Imandra_tools__Idf.Decompose.t
        type 'a prod = [ `Prod of 'a ]
        type consumable_step =
            (decomp_data * step * bool) *
            (Imandra_prelude.unit -> consumable_step L.t prod)
        val decompose_one :
          ?g:G.t ->
          ?root:Strategy.Concrete.node_t ->
          ?idx:Imandra_prelude.Caml.Int.t ->
          ?basis:Imandra_prelude.string list ->
          ?max_asm_lookahead:Imandra_prelude.Caml.Int.t ->
          ?max_ctx_simp:Imandra_prelude.Caml.Int.t ->
          ?reduce_symmetry:bool ->
          ?ctx_asm_simp:bool ->
          ?aggressive_rec:bool ->
          ?compound:bool -> target -> consumable_step L.t
        val node_of_consumable_step :
          consumable_step -> Strategy.Concrete.node_t
        val decompose :
          ?g:G.t ->
          ?root:Strategy.Concrete.node_t ->
          ?idx:Imandra_prelude.Caml.Int.t ->
          ?cache_convergent_paths:bool ->
          ?include_partials:bool ->
          ?basis:Imandra_prelude.string list ->
          ?max_asm_lookahead:Imandra_prelude.Caml.Int.t ->
          ?max_ctx_simp:Imandra_prelude.Caml.Int.t ->
          ?reduce_symmetry:bool ->
          ?ctx_asm_simp:bool ->
          ?aggressive_rec:bool -> ?compound:bool -> target -> t
      end
    module Symbolic :
      sig
        type decomp_step =
          WithStrategy(Strategy.Symbolic).decomp_step = {
          sample : Strategy.Symbolic.event;
          region : Imandra_tools__Idf.Decompose.t;
          signature : Imandra_prelude.string;
        }
        type indexed_state =
          WithStrategy(Strategy.Symbolic).indexed_state = {
          state : Strategy.Symbolic.node_t;
          idx : Imandra_prelude.Caml.Int.t;
        }
        module G :
          sig
            type t = WithStrategy(Strategy.Symbolic).G.t
            module V :
              sig
                type t = WithStrategy(Strategy.Symbolic).G.V.t
                val compare : t -> t -> int
                val hash : t -> int
                val equal : t -> t -> bool
                type label = WithStrategy(Strategy.Symbolic).G.V.label
                val create : label -> t
                val label : t -> label
              end
            type vertex = V.t
            module E :
              sig
                type t = WithStrategy(Strategy.Symbolic).G.E.t
                val compare : t -> t -> int
                type vertex = vertex
                val src : t -> vertex
                val dst : t -> vertex
                type label = WithStrategy(Strategy.Symbolic).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:Imandra_prelude.Caml.Int.t -> Imandra_prelude.unit -> t
            module type LH =
              sig
                val decomp_step_hash :
                  decomp_step -> Imandra_prelude.Caml.Int.t
                val indexed_state_hash :
                  indexed_state -> Imandra_prelude.Caml.Int.t
                val decomp_step_label : decomp_step -> Imandra_prelude.string
                val indexed_state_label :
                  indexed_state -> Imandra_prelude.string
              end
            module type SIG =
              sig
                val output_graph :
                  t -> Imandra_prelude.string -> Imandra_prelude.unit
                val find_edges :
                  t -> Imandra_prelude.Caml.Int.t -> decomp_step list
                val find_vertices :
                  t -> Imandra_prelude.Caml.Int.t -> indexed_state list
              end
            val root : t -> vertex
            module Make :
              functor (L : LH) ->
                sig
                  val output_graph :
                    t -> Imandra_prelude.string -> Imandra_prelude.unit
                  val find_edges :
                    t -> Imandra_prelude.Caml.Int.t -> decomp_step list
                  val find_vertices :
                    t -> Imandra_prelude.Caml.Int.t -> indexed_state list
                end
          end
        type step = indexed_state * decomp_step * indexed_state
        type path = step list
        type t = path L.t * G.t option
        val paths : ?v:G.vertex -> G.t -> path L.t
        val region_of_path : path -> Imandra_tools__Idf.Decompose.t list
        val regions : path L.t -> Imandra_tools__Idf.Decompose.t list L.t
        val replay_path :
          path ->
          (Strategy.Symbolic.state * Strategy.Symbolic.event *
           Strategy.Symbolic.state)
          list
        type decomp_data =
            Strategy.Symbolic.event * Strategy.Symbolic.node_t *
            Imandra_tools__Idf.Decompose.t
        type 'a prod = [ `Prod of 'a ]
        type consumable_step =
            (decomp_data * step * bool) *
            (Imandra_prelude.unit -> consumable_step L.t prod)
        val decompose_one :
          ?g:G.t ->
          ?root:Strategy.Symbolic.node_t ->
          ?idx:Imandra_prelude.Caml.Int.t ->
          ?basis:Imandra_prelude.string list ->
          ?max_asm_lookahead:Imandra_prelude.Caml.Int.t ->
          ?max_ctx_simp:Imandra_prelude.Caml.Int.t ->
          ?reduce_symmetry:bool ->
          ?ctx_asm_simp:bool ->
          ?aggressive_rec:bool ->
          ?compound:bool -> target -> consumable_step L.t
        val node_of_consumable_step :
          consumable_step -> Strategy.Symbolic.node_t
        val decompose :
          ?g:G.t ->
          ?root:Strategy.Symbolic.node_t ->
          ?idx:Imandra_prelude.Caml.Int.t ->
          ?cache_convergent_paths:bool ->
          ?include_partials:bool ->
          ?basis:Imandra_prelude.string list ->
          ?max_asm_lookahead:Imandra_prelude.Caml.Int.t ->
          ?max_ctx_simp:Imandra_prelude.Caml.Int.t ->
          ?reduce_symmetry:bool ->
          ?ctx_asm_simp:bool ->
          ?aggressive_rec:bool -> ?compound:bool -> target -> t
      end
  end
val side_cond_imandra_gensym__2_2 :
  DecompositionConfig.event list -> DecompositionConfig.state -> int -> bool =
  <fun>
val side_cond_imandra_gensym__2_1 :
  DecompositionConfig.event list -> DecompositionConfig.state -> int -> bool =
  <fun>
val side_cond_imandra_gensym__2_0 :
  DecompositionConfig.event list -> DecompositionConfig.state -> int -> bool =
  <fun>
val target_imandra_gensym__2_2 :
  DecompositionConfig.event list ->
  DecompositionConfig.state -> DecompositionConfig.state = <fun>
val target_imandra_gensym__2_1 :
  Model.message list ->
  DecompositionConfig.state -> DecompositionConfig.state = <fun>
val target_imandra_gensym__2_0 :
  DecompositionConfig.event list ->
  DecompositionConfig.state -> DecompositionConfig.state = <fun>
val paths : D.Symbolic.path D.L.t = <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 [6]:
let first_path = D.L.reify 1i paths |> List.hd
Out[6]:
val imandra_gensym__3 : DecompositionConfig.event list -> bool = <fun>
val imandra_gensym__4 :
  DecompositionConfig.event list -> DecompositionConfig.state = <fun>
val imandra_gensym__33 : DecompositionConfig.event list -> bool = <fun>
val imandra_gensym__34 : Model.message list -> DecompositionConfig.state =
  <fun>
val imandra_gensym__59 : DecompositionConfig.event list -> bool = <fun>
val imandra_gensym__60 :
  DecompositionConfig.event list -> DecompositionConfig.state = <fun>
val first_path : D.Symbolic.path =
  [({D.Symbolic.state =
      D.Strategy.Expr ({Model.counter = 0; Model.default = 23}, []);
     idx = 0i},
    {D.Symbolic.sample = Model.Add 1337; region = <abstr>;
     signature = "imandra_gensym__4"},
    {D.Symbolic.state =
      D.Strategy.Expr
       ({Model.counter = Destruct(Model.Add, 0, List.hd e);
         Model.default = 23},
        [List.tl (List.tl (List.tl e)) = []; (List.tl (List.tl e)) <> [];
         Is_a(Model.Add, List.hd (List.tl e)); (List.tl e) <> []; e <> [];
         not (List.hd e = Model.Reset); Is_a(Model.Add, List.hd e);
         Destruct(Model.Add, 0, List.hd e) <= 9000]);
     idx = 1i});
   ({D.Symbolic.state =
      D.Strategy.Expr
       ({Model.counter = Destruct(Model.Add, 0, List.hd e);
         Model.default = 23},
        [List.tl (List.tl (List.tl e)) = []; (List.tl (List.tl e)) <> [];
         Is_a(Model.Add, List.hd (List.tl e)); (List.tl e) <> []; e <> [];
         not (List.hd e = Model.Reset); Is_a(Model.Add, List.hd e);
         Destruct(Model.Add, 0, List.hd e) <= 9000]);
     idx = 1i},
    {D.Symbolic.sample = Model.Add 1; region = <abstr>;
     signature = "imandra_gensym__34"},
    {D.Symbolic.state =
      D.Strategy.Expr
       ({Model.counter = 23; Model.default = 23},
        [e <> []; Is_a(Model.Add, List.hd e); (List.tl e) <> [];
         List.tl (List.tl (List.tl e)) = []; (List.tl (List.tl e)) <> [];
         Is_a(Model.Add, List.hd (List.tl e));
         Destruct(Model.Add, 0, List.hd e) <= 9000;
         Destruct(Model.Add, 0, List.hd e) = 1337;
         not (List.hd e = Model.Reset)]);
     idx = 2i});
   ({D.Symbolic.state =
      D.Strategy.Expr
       ({Model.counter = 23; Model.default = 23},
        [e <> []; Is_a(Model.Add, List.hd e); (List.tl e) <> [];
         List.tl (List.tl (List.tl e)) = []; (List.tl (List.tl e)) <> [];
         Is_a(Model.Add, List.hd (List.tl e));
         Destruct(Model.Add, 0, List.hd e) <= 9000;
         Destruct(Model.Add, 0, List.hd e) = 1337;
         not (List.hd e = Model.Reset)]);
     idx = 2i},
    {D.Symbolic.sample = Model.Reset; region = <abstr>;
     signature = "imandra_gensym__60"},
    {D.Symbolic.state =
      D.Strategy.Expr
       ({Model.counter = 0; Model.default = 23},
        [e <> []; Is_a(Model.Add, List.hd e); (List.tl e) <> [];
         List.tl (List.tl (List.tl e)) = []; (List.tl (List.tl e)) <> [];
         Is_a(Model.Add, List.hd (List.tl e));
         Destruct(Model.Add, 0, List.hd e) = 1337;
         List.hd (List.tl (List.tl e)) = Model.Reset;
         Destruct(Model.Add, 0, List.hd e) <= 9000;
         not (List.hd e = Model.Reset)]);
     idx = 3i})]
Regions details
No group selected.
ConstraintsInvariant
  • List.tl (List.tl (List.tl e)) = []
  • (List.tl (List.tl e)) <> []
  • Is_a(Model.Add, List.hd (List.tl e))
  • (List.tl e) <> []
  • e <> []
  • List.hd e = Model.Reset
F = {Model.counter = 0; Model.default = 23}
  • List.tl (List.tl (List.tl e)) = []
  • (List.tl (List.tl e)) <> []
  • Is_a(Model.Add, List.hd (List.tl e))
  • (List.tl e) <> []
  • e <> []
  • not (List.hd e = Model.Reset)
  • Is_a(Model.Add, List.hd e)
  • not (Destruct(Model.Add, 0, List.hd e) <= 9000)
F = {Model.counter = 0; Model.default = 23}
  • List.tl (List.tl (List.tl e)) = []
  • (List.tl (List.tl e)) <> []
  • Is_a(Model.Add, List.hd (List.tl e))
  • (List.tl e) <> []
  • e <> []
  • not (List.hd e = Model.Reset)
  • Is_a(Model.Add, List.hd e)
  • Destruct(Model.Add, 0, List.hd e) <= 9000
F = {Model.counter = Destruct(Model.Add, 0, List.hd e); Model.default = 23}
Regions details
No group selected.
ConstraintsInvariant
  • e <> []
  • Is_a(Model.Add, List.hd e)
  • (List.tl e) <> []
  • List.tl (List.tl (List.tl e)) = []
  • (List.tl (List.tl e)) <> []
  • Is_a(Model.Add, List.hd (List.tl e))
  • Destruct(Model.Add, 0, List.hd e) <= 9000
  • not (Destruct(Model.Add, 0, List.hd e) = 1337)
  • not
    ((Destruct(Model.Add, 0, List.hd e)
      + Destruct(Model.Add, 0, List.hd (List.tl e)))
     <= 9000)
F = {Model.counter = 0; Model.default = 23}
  • e <> []
  • Is_a(Model.Add, List.hd e)
  • (List.tl e) <> []
  • List.tl (List.tl (List.tl e)) = []
  • (List.tl (List.tl e)) <> []
  • Is_a(Model.Add, List.hd (List.tl e))
  • Destruct(Model.Add, 0, List.hd e) <= 9000
  • not (Destruct(Model.Add, 0, List.hd e) = 1337)
  • (Destruct(Model.Add, 0, List.hd e)
     + Destruct(Model.Add, 0, List.hd (List.tl e)))
    <= 9000
F =
{Model.counter =
 Destruct(Model.Add, 0, List.hd e)
 + Destruct(Model.Add, 0, List.hd (List.tl e)); Model.default = 23}
  • e <> []
  • Is_a(Model.Add, List.hd e)
  • (List.tl e) <> []
  • List.tl (List.tl (List.tl e)) = []
  • (List.tl (List.tl e)) <> []
  • Is_a(Model.Add, List.hd (List.tl e))
  • Destruct(Model.Add, 0, List.hd e) <= 9000
  • Destruct(Model.Add, 0, List.hd e) = 1337
F = {Model.counter = 23; Model.default = 23}
Regions details
No group selected.
ConstraintsInvariant
  • e <> []
  • Is_a(Model.Add, List.hd e)
  • (List.tl e) <> []
  • List.tl (List.tl (List.tl e)) = []
  • (List.tl (List.tl e)) <> []
  • Is_a(Model.Add, List.hd (List.tl e))
  • Destruct(Model.Add, 0, List.hd e) = 1337
  • not (List.hd (List.tl (List.tl e)) = Model.Reset)
  • not Is_a(Model.Add, List.hd (List.tl (List.tl e)))
  • Destruct(Model.Sub, 0, List.hd (List.tl (List.tl e))) <= 23
F =
{Model.counter =
 23 + -1 * Destruct(Model.Sub, 0, List.hd (List.tl (List.tl e)));
 Model.default = 23}
  • e <> []
  • Is_a(Model.Add, List.hd e)
  • (List.tl e) <> []
  • List.tl (List.tl (List.tl e)) = []
  • (List.tl (List.tl e)) <> []
  • Is_a(Model.Add, List.hd (List.tl e))
  • Destruct(Model.Add, 0, List.hd e) = 1337
  • not (List.hd (List.tl (List.tl e)) = Model.Reset)
  • Is_a(Model.Add, List.hd (List.tl (List.tl e)))
  • not (Destruct(Model.Add, 0, List.hd (List.tl (List.tl e))) <= 8977)
F = {Model.counter = 0; Model.default = 23}
  • e <> []
  • Is_a(Model.Add, List.hd e)
  • (List.tl e) <> []
  • List.tl (List.tl (List.tl e)) = []
  • (List.tl (List.tl e)) <> []
  • Is_a(Model.Add, List.hd (List.tl e))
  • Destruct(Model.Add, 0, List.hd e) = 1337
  • not (List.hd (List.tl (List.tl e)) = Model.Reset)
  • Is_a(Model.Add, List.hd (List.tl (List.tl e)))
  • Destruct(Model.Add, 0, List.hd (List.tl (List.tl e))) <= 8977
F =
{Model.counter = 23 + Destruct(Model.Add, 0, List.hd (List.tl (List.tl e)));
 Model.default = 23}
  • e <> []
  • Is_a(Model.Add, List.hd e)
  • (List.tl e) <> []
  • List.tl (List.tl (List.tl e)) = []
  • (List.tl (List.tl e)) <> []
  • Is_a(Model.Add, List.hd (List.tl e))
  • Destruct(Model.Add, 0, List.hd e) = 1337
  • List.hd (List.tl (List.tl e)) = Model.Reset
F = {Model.counter = 0; Model.default = 23}

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

In [7]:
D.Symbolic.replay_path first_path
Out[7]:
- : (D.Strategy.Symbolic.state * D.Strategy.Symbolic.event *
     D.Strategy.Symbolic.state)
    list
=
[({Model.counter = 0; default = 23}, Model.Add 1337,
  {Model.counter = 1337; default = 23});
 ({Model.counter = 1337; default = 23}, Model.Add 0,
  {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 [8]:
#install_printer Decompose.print;;

let first_path_regions = D.Symbolic.region_of_path first_path
Out[8]:
val first_path_regions : Imandra_tools__Idf.Decompose.t list =
  [{Imandra_tools__Idf.Decompose.reg_session = 1i; reg_id = 3i;
    reg_constraints =
     [List.tl (List.tl (List.tl e)) = []; (List.tl (List.tl e)) <> [];
      Is_a(Model.Add, List.hd (List.tl e)); (List.tl e) <> []; e <> [];
      not (List.hd e = Model.Reset); Is_a(Model.Add, List.hd e);
      Destruct(Model.Add, 0, List.hd e) <= 9000];
    reg_invariant =
     F =
     {Model.counter = Destruct(Model.Add, 0, List.hd e); Model.default = 23}};
   {Imandra_tools__Idf.Decompose.reg_session = 2i; reg_id = 9i;
    reg_constraints =
     [e <> []; Is_a(Model.Add, List.hd e); (List.tl e) <> [];
      List.tl (List.tl (List.tl e)) = []; (List.tl (List.tl e)) <> [];
      Is_a(Model.Add, List.hd (List.tl e));
      Destruct(Model.Add, 0, List.hd e) <= 9000;
      Destruct(Model.Add, 0, List.hd e) = 1337];
    reg_invariant = F = {Model.counter = 23; Model.default = 23}};
   {Imandra_tools__Idf.Decompose.reg_session = 3i; reg_id = 16i;
    reg_constraints =
     [e <> []; Is_a(Model.Add, List.hd e); (List.tl e) <> [];
      List.tl (List.tl (List.tl e)) = []; (List.tl (List.tl e)) <> [];
      Is_a(Model.Add, List.hd (List.tl e));
      Destruct(Model.Add, 0, List.hd e) = 1337;
      List.hd (List.tl (List.tl e)) = Model.Reset];
    reg_invariant = F = {Model.counter = 0; Model.default = 23}}]

Idf has many more capabilities and entry points than we've just described and we haven't even touched on its scalability properties but 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 [9]:
#install_printer Region_pp.print;;

first_path_regions
Out[9]:
- : Imandra_tools__Idf.Decompose.t list =
[---[region]---
 Constraints:
   [ (List.tl (List.tl (List.tl e))) = []
   ; (List.hd (List.tl e)) is Model.Add
   ; (List.hd e) is Model.Add
   ; (List.hd e).Model.Add_0 <= 9000 ]
 Invariant:
   F = Model.{ counter = (List.hd e).Model.Add_0 ; default = 23 }
 -------------;
 ---[region]---
 Constraints:
   [ (List.hd e) is Model.Add
   ; (List.tl (List.tl (List.tl e))) = []
   ; (List.hd (List.tl e)) is Model.Add
   ; (List.hd e).Model.Add_0 = 1337 ]
 Invariant:
   F = Model.{ counter = 23 ; default = 23 }
 -------------;
 ---[region]---
 Constraints:
   [ (List.hd e) is Model.Add
   ; (List.tl (List.tl (List.tl e))) = []
   ; (List.hd (List.tl e)) is Model.Add
   ; (List.hd e).Model.Add_0 = 1337
   ; (List.hd (List.tl (List.tl e))) is Model.Reset ]
 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 [10]:
#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[10]:
val f : int Set.t -> int Set.t -> int -> int Set.t = <fun>
val rs : Imandra_reasoning.Decompose.t list =
  [---[region]---
   Constraints:
    [y = Set.union x y]
   Invariant:
    F = Map.add' x z true
   -------------;
   ---[region]---
   Constraints:
    [not (y = Set.union x y)]
   Invariant:
    F = Map.add' (Map.const false) z true
   -------------]
Regions details
No group selected.
ConstraintsInvariant
  • not (y = Set.union x y)
F = Map.add' (Map.const false) z true
  • y = Set.union x y
F = 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 [11]:
open Region_pp
open PPrinter

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.PP(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 = XF.walk_fix refine_

let print = PPrinter.print ~refine ()
Out[11]:
module Custom :
  sig
    type t = Set of t Imandra_tools.Region_pp.node_ list
    val map :
      (t Imandra_tools.Region_pp.node_ -> t Imandra_tools.Region_pp.node_) ->
      t -> t
    val compare : t -> t -> Imandra_tools.Region_pp.comparison
    val print :
      t Imandra_tools.Region_pp.node_ CCFormat.printer ->
      focus:'a -> CCFormat.t -> t -> unit
  end
module PPrinter :
  sig
    type node = Custom.t Imandra_tools__Region_pp.node_
    module XF :
      sig
        val map :
          (Custom.t Imandra_tools__Region_pp.node_ ->
           Custom.t Imandra_tools__Region_pp.node_) ->
          Custom.t Imandra_tools__Region_pp.node_ ->
          Custom.t Imandra_tools__Region_pp.node_
        val walk :
          pre:(node -> Custom.t Imandra_tools__Region_pp.node_) ->
          ?post:(Custom.t Imandra_tools__Region_pp.node_ ->
                 Custom.t Imandra_tools__Region_pp.node_) ->
          node -> Custom.t Imandra_tools__Region_pp.node_
        val fix_ : ?bound:Z.t -> ('a -> 'a) -> 'a -> 'a -> 'a
        val fix : ?bound:Z.t -> ('a -> 'a) -> 'a -> 'a
        val walk_fix : (node -> node) -> node -> node
        exception Iterated
        val iterated : Imandra_prelude.unit -> 'a
        val iter : f:(node -> 'a) -> node -> Imandra_prelude.unit
        val find : f:(node -> bool) -> node -> bool
      end
    module VarClassifier :
      sig val classify : node -> Imandra_tools__Region_pp.var_name list end
    module Printer :
      sig
        val print :
          ?focus:Imandra_tools__Region_pp.var_name ->
          Imandra_prelude.unit -> node CCFormat.printer
        val print_parens :
          focus:Imandra_tools__Region_pp.var_name -> node CCFormat.printer
        val to_string :
          ?focus:Imandra_tools__Region_pp.var_name -> node -> string
      end
    module Comparator :
      sig
        val is_eq : Imandra_tools__Region_pp.comparison -> bool
        val compare_all :
          Custom.t Imandra_tools__Region_pp.node_ list ->
          Custom.t Imandra_tools__Region_pp.node_ list ->
          Imandra_tools__Region_pp.comparison
        val compare :
          Custom.t Imandra_tools__Region_pp.node_ ->
          Custom.t Imandra_tools__Region_pp.node_ ->
          Imandra_tools__Region_pp.comparison
      end
    module Simplifier :
      sig
        val simp :
          'a Imandra_tools__Region_pp.node_ ->
          'a Imandra_tools__Region_pp.node_
        val simplify : node -> node
      end
    val has_symbolic_term : node -> bool
    module Unifier :
      sig
        val unify_ :
          unify:(node -> node -> node option) -> node -> node -> node option
        val unify_two :
          unify:(node -> node -> node option) -> node -> node -> node option
        val unify :
          ?unify:(node -> node -> node option) -> node list -> node list
      end
    module Parser :
      sig
        module T = Imandra_surface.Term
        module Ty = Imandra_surface.Type
        module V = Imandra_surface.Var
        module U = Imandra_surface.Uid
        exception Discarded of T.t
        val discard : T.t -> 'a
        val parse_binary_function :
          Imandra_prelude.string ->
          T.t -> T.t -> 'a Imandra_tools__Region_pp.node_
        val parse : T.t -> 'a Imandra_tools__Region_pp.node_
        val parse_list : T.t -> T.t list
        val is_proper_list : T.t -> bool
        val parse_expr : T.t -> 'a Imandra_tools__Region_pp.node_ option
      end
    val pp :
      ?unify:(node -> node -> node option) ->
      ?refine:(node -> node) -> ?focus:'a -> Parser.T.t CCList.t -> node list
    val print :
      ?unify:(node -> node -> node option) ->
      ?refine:(node -> node) ->
      Imandra_prelude.unit ->
      Format.formatter -> Imandra_surface.Top_result.decompose_region -> unit
    val to_string :
      ?unify:(node -> node -> node option) ->
      ?refine:(node -> node) ->
      Imandra_surface.Top_result.decompose_region -> string
  end
val refine_ :
  Custom.t Imandra_tools.Region_pp.node_ ->
  Custom.t Imandra_tools.Region_pp.node_ = <fun>
val gather_keys :
  Custom.t Imandra_tools.Region_pp.node_ ->
  Custom.t Imandra_tools.Region_pp.node_ list = <fun>
val is_proper_set : Custom.t Imandra_tools.Region_pp.node_ -> bool = <fun>
val refine : PPrinter.node -> PPrinter.node = <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.SIG, defining mapping, printing and compareing functions for an abstract Set value
  • next we instantiate Region_pp.PP 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 [12]:
#install_printer print;;
rs
Out[12]:
- : Imandra_reasoning.Decompose.t list =
[---[region]---
 Constraints:
  [y = Set.union x y]
 Invariant:
  F = Map.add' x z true
 -------------;
 ---[region]---
 Constraints:
  [not (y = Set.union x y)]
 Invariant:
  F = Map.add' (Map.const false) z true
 -------------]

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 last imandra-tools module

Term Synthesizer (Term_synth)

Imandra's ability to both reify failed proofs into counter-examples and sample values from regions provides a lot of power. Term_synth extends this power, allowing Imandra to synthesize any Term (such as a regions' constraints or invariant) 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 [13]:
Caml.List.mapi (fun i {Decompose.constraints; _} -> 
  let gs = "region_" ^ (string_of_int i) in (* Imandra_util.Util.gensym () *)
  let term = List.map Expr_trans.to_term constraints |> Term.and_l in
  let body = Term_synth.synthesize_term ~default:"false" term in
  let func = Printf.sprintf "let %s x y = %s" gs body in
  Reflect.eval func;
  gs)
  rs
Out[13]:
val region_0 : 'a Set.t -> 'a Set.t -> bool = <fun>
val region_1 : 'a Set.t -> 'a Set.t -> bool = <fun>
- : String.t list = ["region_0"; "region_1"]

The above should be quite straightforward:

  • We extract the constraints from the region
  • We convert each constraint to a Term, using Imandra's Expr_trans facility and we conjoin them into a single Term
  • We ask 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 [14]:
region_0 (Set.of_list [1]) Set.empty;;
region_0 Set.empty (Set.of_list [1]);;

region_1 Set.empty (Set.of_list [1]);;
region_1 (Set.of_list [1]) Set.empty;;
Out[14]:
- : 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 immensely powerful and at the core of Idf and other powerful analysis tools we build.