Iterative Decomposition Framework

Imandra has the ability to enumerate the state space of a function via its decomposition feature.

IDF is a framework that builds on top of that and adds the ability to enumerate the state space of a (possibly infinite) state machine after a bounded number of abstract transitions.

Let's define one such state machine and see how IDF can help us navigating its state space: we must define a module conforming to Idf_intf.SM_SIG. An additional constraint which is not enforciable by the OCaml type system but is enforced at runtime by IDF is that the type of event must be an algebraic variant type (or an alias to one).

Try this!
In [1]:
module SM = struct

  type i = Int of int | Zero

  (* type of state machine events *)
  type event = Add of i | Sub of int | Reset

  (* type of state machine state *)
  type state = int

  (* initial state of the state machine *)
  let init_state = 0

  (* transition function of the state machine *)
  let step event state =
    if state = 1337 then
      state
    else
      match event with
      | Reset -> 0
      | Add (Zero) -> state
      | Add (Int n) ->
        if n < 0 then
          state
        else if n = 0 || n + state > 9000 then
          0
        else
          state + n
      | Sub n ->
        if n > state then
          state
        else
          state - n

  (* validity function for an event transition *)
  let is_valid event state =
    match event with
    | Add (Int n) when state < 3 -> n > 50
    | Add (Int 0) -> false
    | Sub n -> (n > 0 && n <= state) || (n < 0)
    | _ -> true

end
Out[1]:
module SM :
  sig
    type i = Int of Z.t | Zero
    type event = Add of i | Sub of Z.t | Reset
    type state = Z.t
    val init_state : state
    val step : event -> state -> state
    val is_valid : event -> state -> bool
  end

We can try to compute with this state machine:

Try this!
In [2]:
SM.
(init_state
|> step (Add Zero)
|> step (Add (Int 15))
|> step Reset
|> step (Sub (-1)))
Out[2]:
- : SM.state = 1

Now that we have a model to decompose, we must create a symbolic template of SM events, by creating a module conforming to Idf_intf.TPL_SIG

Note that there's not necessarily a 1:1 correspondence between the variant constructors of SM.event and the ones of TPL.t, for example TPL.Any is an empty mapping, meaning that no constructor will be constrained for that symbolic event, TPL.AddInt on the other hand fixes the event to be a SM.Add (SM.Int _), thus excluding SM.Add SM.Zero.

Try this!
In [3]:
module TPL = struct
  (* type of a symbolic state machine event *)
  type t = Add | AddInt | Sub | Reset | Any
  type c = SM.event

  type state = SM.state

  (* mapping function from a symbolic state machine event to a concrete event *)
  let concrete t c _ = match t,c with
    | Any, _ -> true
    | Add, SM.Add _ -> true
    | AddInt, SM.Add(SM.Int _) -> true
    | Sub, SM.Sub _ -> true
    | Reset, SM.Reset -> true
    | _ -> false
end
Out[3]:
module TPL :
  sig
    type t = Add | AddInt | Sub | Reset | Any
    type c = SM.event
    type state = SM.state
    val concrete : t -> c -> 'a -> bool
  end

Next we need to hook the SM and TPL modules into a module conforming to Idf_intf.DSM_SIG:

Try this!
In [4]:
module Decomp = struct

  module State_machine = SM

  module Template = TPL

  let module_name = "Decomp"

end
Out[4]:
module Decomp :
  sig
    module State_machine = SM
    module Template = TPL
    val module_name : string
  end

And finally we can instantiate Idf using Decomp:

Try this!
In [5]:
#program;;

module IDF = Imandra_tools.Idf.Make(Decomp)
Out[5]:
val root_ZG0wYy1Ld3BtSmpfanUzazI4eFJsaTF1RHNFWi1PZTQ2YnRtbjI5UG1vNA :
  TPL.c list -> TPL.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 = TPL.state
            type event = TPL.c
            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 = TPL.t
            type c = State_machine.event
            val concrete : t -> c -> state -> bool
          end
        val module_name : string
      end
    val pp_state : TPL.state -> string
    type target = TPL.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 -> TPL.c 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 -> TPL.c 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 : TPL.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 : TPL.state;
      event : TPL.c;
      state_after : TPL.state;
    }
    val replay_events : TPL.c 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

We are now ready to decompose a SM state machine under a particular TPL.t template

Try this!
In [6]:
let g = IDF.decompose TPL.[Any;AddInt]
Out[6]:
val guard__ZG0wYy1Ld3BtSmpfanUzazI4eFJsaTF1RHNFWi1PZTQ2YnRtbjI5UG1vNA_VFBMLkFueTpWYWxpZA_true :
  TPL.c list -> bool = <fun>
val target__ZG0wYy1Ld3BtSmpfanUzazI4eFJsaTF1RHNFWi1PZTQ2YnRtbjI5UG1vNA_VFBMLkFueTpWYWxpZA_true :
  TPL.c list -> TPL.state = <fun>
val guard__ZG0wYy1Ld3BtSmpfanUzazI4eFJsaTF1RHNFWi1PZTQ2YnRtbjI5UG1vNA_VFBMLkFueTpWYWxpZCxUUEwuQW55OlZhbGlkVFBMLkFkZEludDpWYWxpZA_true :
  TPL.c list -> bool = <fun>
val target__ZG0wYy1Ld3BtSmpfanUzazI4eFJsaTF1RHNFWi1PZTQ2YnRtbjI5UG1vNA_VFBMLkFueTpWYWxpZCxUUEwuQW55OlZhbGlkVFBMLkFkZEludDpWYWxpZA_true :
  TPL.c list -> TPL.state = <fun>
val g : IDF.G.t = <abstr>

We've invoked IDF.decompose over a template of [Any;AddInt], which means we'll try to symbolically decompose the state space of a state machine after the following steps (_ is used to indicate a symbolic value):

SM.
(init_state
 |> step _
 |> step (Add (Int _)))

In order to consume concrete paths, we must extract them from the decomposition graph g:

Try this!
In [7]:
let first_path = IDF.paths g |> List.hd;;
let full_node = first_path |> CCList.rev |> CCList.hd
Out[7]:
val first_path : IDF.path = [<abstr>;<abstr>;<abstr>]
val full_node : IDF.node = <abstr>

Now that we have a path value available, we can explore what we can do with it:

  • We can ask for sample event values for the current path, which will return a sample for each event in the path:
Try this!
In [8]:
let samples = IDF.sample full_node
Out[8]:
val samples : TPL.c list option =
  Some
   [Decomp.State_machine.Add (Decomp.State_machine.Int 51);
    Decomp.State_machine.Add (Decomp.State_machine.Int 1)]
  • We can ask for a sample execution replay of the current path, which will return a list of tuples of input state * input event * output state for each sample event in the path:
Try this!
In [9]:
let replayed_node = IDF.replay full_node
Out[9]:
val replayed_node : IDF.replay_sample list option =
  Some
   [{IDF.state_before = 0;
     event = Decomp.State_machine.Add (Decomp.State_machine.Int 51);
     state_after = 51};
    {IDF.state_before = 51;
     event = Decomp.State_machine.Add (Decomp.State_machine.Int 1);
     state_after = 52}]
  • We can ask for the concrete regions representing the constraints of the state machine up to each event in the path:
Try this!
In [10]:
#install_printer Imandra_tools.Region_pp.print;;

let regions = List.map (fun n -> Remote_ref.get_shared_block (IDF.region n)) first_path
Out[10]:
val regions : Top_result.modular_region list =
  [---[region]---
   Constraints:
     [  ]
   Invariant:
     F = 0
    -------------;
   ---[region]---
   Constraints:
     [ Destruct(SM.Add, 0, (List.hd e)) is SM.Int
     ; (List.hd e) is SM.Add
     ; 50 < Destruct(SM.Int, 0, Destruct(SM.Add, 0, (List.hd e))) <= 9000
     ; Destruct(SM.Int, 0, Destruct(SM.Add, 0, (List.hd e))) <> 0 ]
   Invariant:
     F = Destruct(SM.Int, 0, Destruct(SM.Add, 0, (List.hd e)))
    -------------;
   ---[region]---
   Constraints:
     [ Destruct(SM.Add, 0, (List.hd e)) is SM.Int
     ; (List.hd e) is SM.Add
     ; Destruct(SM.Add, 0, (List.hd (List.tl e))) is SM.Int
     ; (List.hd (List.tl e)) is SM.Add
     ; (Destruct(SM.Int, 0, Destruct(SM.Add, 0, (List.hd (List.tl e)))) +
          Destruct(SM.Int, 0, Destruct(SM.Add, 0, (List.hd e))))
         <= 9000
     ; 50 < Destruct(SM.Int, 0, Destruct(SM.Add, 0, (List.hd e))) <= 9000
     ; Destruct(SM.Int, 0, Destruct(SM.Add, 0, (List.hd (List.tl e)))) > 0
     ; Destruct(SM.Int, 0, Destruct(SM.Add, 0, (List.hd e))) <> 0
     ; Destruct(SM.Int, 0, Destruct(SM.Add, 0, (List.hd e))) <> 1337 ]
   Invariant:
     F =
     Destruct(SM.Int, 0, Destruct(SM.Add, 0, (List.hd e))) +
       Destruct(SM.Int, 0, Destruct(SM.Add, 0, (List.hd (List.tl e))))
    -------------]

It is to be noted that the each symbolic event in those constraints is represented as the nth element of the list e, thus the first Any event will be List.hd e, the second AddInt will be List.hd (List.tl e), and since we've asked IDF to decompose a path of exactly two events, there will be no third or more events, and thus we can find a constraint to that effect: List.tl (List.tl e) = [].