# 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
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:

In [2]:
SM.
(init_state
|> 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.

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
| 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:

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]:
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
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

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 _


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 option =
Some

• 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 option =
Some
[{IDF.state_before = 0;
state_after = 51};
{IDF.state_before = 51;
state_after = 52}]

• 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 (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
; 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
; 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)))) > 0
; 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
; (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
; 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) = [].