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).

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 int | Zero
    type event = Add of i | Sub of int | Reset
    type state = int
    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:

In [2]:
SM.
(init_state
|> step (Add Zero)
|> step (Add (Int 15))
|> step Reset
|> step (Sub (-1)))
Out[2]:
- : int = 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.

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

  (* 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 = TPL.c
    val concrete : t -> c -> bool
  end

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

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:

In [5]:
#program;;

module IDF = Imandra_tools.Idf.Make(Decomp)
Out[5]:
- : unit = ()
val root_Q01oWlRQekF4cXdRb2N5UFlkTzhtMzBHUDFEbEExNUJtcjdLL1NWZE5NWQ_val : int =
  0
val root_Q01oWlRQekF4cXdRb2N5UFlkTzhtMzBHUDFEbEExNUJtcjdLL1NWZE5NWQ :
  TPL.c list -> int = <fun>
module IDF :
  sig
    type pol = IDF.pol = Valid | Invalid | No | Custom of string
    module DSM :
      sig
        module State_machine :
          sig
            type state = int
            type event = TPL.c
            val init_state : state
            val step : event -> state -> state
            val is_valid : event -> state -> bool
          end
        module Template :
          sig
            type t = TPL.t
            type c = State_machine.event
            val concrete : t -> c -> bool
          end
        val module_name : string
      end
    val pp_state : int -> string
    type target = TPL.t list
    type node = IDF.node
    type path = node list
    module G :
      sig
        type t = IDF.G.t
        module V :
          sig
            type t = node
            val compare : t -> t -> int/2
            val hash : t -> int/2
            val equal : t -> t -> bool
            type label = t
            val create : t -> t
            val label : t -> t
          end
        type vertex = node
        module E :
          sig
            type t = IDF.G.edge
            val compare : t -> t -> int/2
            type vertex = node
            val src : t -> vertex
            val dst : t -> vertex
            type label = IDF.G.E.label
            val create : vertex -> label -> vertex -> t
            val label : t -> label
          end
        type edge = E.t
        val is_directed : bool
        val is_empty : t -> bool
        val nb_vertex : t -> int/2
        val nb_edges : t -> int/2
        val out_degree : t -> vertex -> int/2
        val in_degree : t -> vertex -> int/2
        val mem_vertex : t -> vertex -> bool
        val mem_edge : t -> vertex -> vertex -> bool
        val mem_edge_e : t -> edge -> bool
        val find_edge : t -> vertex -> vertex -> edge
        val find_all_edges : t -> vertex -> vertex -> edge list
        val succ : t -> vertex -> vertex list
        val pred : t -> vertex -> vertex list
        val succ_e : t -> vertex -> edge list
        val pred_e : t -> vertex -> edge list
        val iter_vertex : (vertex -> unit) -> t -> unit
        val fold_vertex : (vertex -> 'a -> 'a) -> t -> 'a -> 'a
        val iter_edges : (vertex -> vertex -> unit) -> t -> unit
        val fold_edges : (vertex -> vertex -> 'a -> 'a) -> t -> 'a -> 'a
        val iter_edges_e : (edge -> unit) -> t -> unit
        val fold_edges_e : (edge -> 'a -> 'a) -> t -> 'a -> 'a
        val map_vertex : (vertex -> vertex) -> t -> t
        val iter_succ : (vertex -> unit) -> t -> vertex -> unit
        val iter_pred : (vertex -> unit) -> t -> vertex -> unit
        val fold_succ : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
        val fold_pred : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
        val iter_succ_e : (edge -> unit) -> t -> vertex -> unit
        val fold_succ_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
        val iter_pred_e : (edge -> unit) -> t -> vertex -> unit
        val fold_pred_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
        val create : ?size:int/2 -> unit -> t
        val clear : t -> unit
        val copy : t -> t
        val add_vertex : t -> vertex -> unit
        val remove_vertex : t -> vertex -> unit
        val add_edge : t -> vertex -> vertex -> unit
        val add_edge_e : t -> edge -> unit
        val remove_edge : t -> vertex -> vertex -> unit
        val remove_edge_e : t -> edge -> unit
        val root : t -> vertex
        val leaves : t -> vertex list
        val output_graph : t -> file:string -> unit
      end
    val paths : ?from:node -> G.t -> path list
    val region : node -> Top_result.modular_region
    val expanded_constraints : node -> Term.term list
    val sample : node -> TPL.c list
    val sample_region : Top_result.modular_region -> TPL.c list
    type region_expander = string option * string list * string option
    type target_step =
      IDF.target_step = {
      event : TPL.t;
      valid_pol : pol;
      region_expander : region_expander option;
    }
    val target_steps : node -> target_step list list
    type replay_sample =
      IDF.replay_sample = {
      state_before : int;
      event : TPL.c;
      state_after : int;
    }
    val replay_events : TPL.c list -> replay_sample list
    val replay : node -> replay_sample list
    type runner = IDF.runner
    val create :
      ?basis:string list ->
      ?expanding:string list -> ?assuming:string -> unit -> runner
    val add :
      runner:runner ->
      g:G.t ->
      ?valid_pol:pol list ->
      ?region_expander:region_expander list -> target -> unit
    val run : runner -> unit -> unit
    val decompose :
      g:G.t ->
      ?basis:string list ->
      ?expanding:string list ->
      ?assuming:string ->
      ?valid_pol:pol list ->
      ?region_expander:region_expander list -> target -> unit -> unit
  end

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

In [6]:
let g = IDF.G.create ();;
IDF.decompose ~g TPL.[Any;AddInt] ()
Out[6]:
val g : IDF.G.t = <abstr>
val guard_Q01oWlRQekF4cXdRb2N5UFlkTzhtMzBHUDFEbEExNUJtcjdLL1NWZE5NWQ_VFBMLkFueTpWYWxpZA_true :
  TPL.c list -> bool = <fun>
val target_Q01oWlRQekF4cXdRb2N5UFlkTzhtMzBHUDFEbEExNUJtcjdLL1NWZE5NWQ_VFBMLkFueTpWYWxpZA_true :
  TPL.c list -> int = <fun>
val guard_Q01oWlRQekF4cXdRb2N5UFlkTzhtMzBHUDFEbEExNUJtcjdLL1NWZE5NWQ_VFBMLkFueTpWYWxpZCxUUEwuQW55OlZhbGlkVFBMLkFkZEludDpWYWxpZA_true :
  TPL.c list -> bool = <fun>
val target_Q01oWlRQekF4cXdRb2N5UFlkTzhtMzBHUDFEbEExNUJtcjdLL1NWZE5NWQ_VFBMLkFueTpWYWxpZCxUUEwuQW55OlZhbGlkVFBMLkFkZEludDpWYWxpZA_true :
  TPL.c list -> int = <fun>
- : unit = ()

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:

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:
In [8]:
let samples = IDF.sample full_node
Out[8]:
val samples : TPL.c list =
  [Decomp.State_machine.Add (Decomp.State_machine.Int 9001);
   Decomp.State_machine.Add (Decomp.State_machine.Int 9039)]
  • 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:
In [9]:
let replayed_node = IDF.replay full_node
Out[9]:
val replayed_node : IDF.replay_sample list =
  [{IDF.state_before = 0;
    event = Decomp.State_machine.Add (Decomp.State_machine.Int 9001);
    state_after = 0};
   {IDF.state_before = 0;
    event = Decomp.State_machine.Add (Decomp.State_machine.Int 9039);
    state_after = 0}]
  • We can ask for the concrete regions representing the constraints of the state machine up to each event in the path:
In [10]:
#install_printer Imandra_tools.Region_pp.print;;

let regions = List.map IDF.region first_path
Out[10]:
val regions : Top_result.modular_region list =
  [---[region]---
   Constraints:
     [  ]
   Invariant:
     F = 0
    -------------;
   ---[region]---
   Constraints:
     [ (List.hd e) is SM.Add
     ; Destruct(SM.Add, 0, (List.hd e)) is SM.Int
     ; Destruct(SM.Int, 0, Destruct(SM.Add, 0, (List.hd e))) > 9000
     ; (List.tl e) = [] ]
   Invariant:
     F = 0
    -------------;
   ---[region]---
   Constraints:
     [ Destruct(SM.Add, 0, (List.hd e)) is SM.Int
     ; (List.hd e) is SM.Add
     ; (List.hd (List.tl e)) is SM.Add
     ; Destruct(SM.Add, 0, (List.hd (List.tl e))) is SM.Int
     ; 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)))) > 9000
     ; (List.tl (List.tl e)) = [] ]
   Invariant:
     F = 0
    -------------]

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) = [].