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; moreover it can do this in a distributed fashion, bringing terrific performance improvements over single-process decompositions.

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 : Z.t
    val step : event -> int -> int
    val is_valid : event -> int -> 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

  (* mapping function from a symbolic state machine event to a concrete event name *)
  let concrete = function
    | Any -> []
    | Add -> ["SM.Add"]
    | AddInt -> ["SM.Add"; "SM.Int"]
    | Sub -> ["SM.Sub"]
    | Reset -> ["SM.Reset"]
end
Out[3]:
module TPL :
  sig
    type t = Add | AddInt | Sub | Reset | Any
    val concrete : t -> string list
  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 D = Imandra_tools.Idf.Make(Decomp)

module IDF = D.Symbolic
Out[5]:
val g___1 : Decomp.State_machine.event list -> Decomp.State_machine.state =
  <fun>
module Mex :
  sig
    module E = Imandra_interactive.Extract
    val get_option : (E.expr -> 'a_0) -> E.expr -> 'a_0 option
    val get_nativeint : E.expr -> nativeint
    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_SM_i : E.expr -> SM.i
    val get_SM_event : E.expr -> SM.event
    val get_SM_state : E.expr -> SM.state
    val get_TPL_t : E.expr -> TPL.t
    type e_t = SM.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
    module Symbolic :
      sig
        module DSM :
          sig
            module Template :
              sig
                type t = Decomp.Template.t
                val concrete : t -> string list
              end
            module State_machine :
              sig
                type state = Decomp.State_machine.state
                type event = Decomp.State_machine.event
                val init_state : state
                val step : event -> state -> state
                val is_valid : event -> state -> bool
              end
            val module_name : string
          end
        type target = DSM.Template.t list
        type step = Imandra_tools__Idf.Make(Decomp).Symbolic.step
        type node = Imandra_tools__Idf.Make(Decomp).Symbolic.node
        type edge = node * step * node
        type path = edge list
        type paths = Imandra_tools__Idf.Make(Decomp).Symbolic.paths
        type scheduler = Imandra_tools__Idf.Make(Decomp).Symbolic.scheduler
        type traversal =
          Imandra_tools__Idf.Make(Decomp).Symbolic.traversal =
            DF
          | BF
        module G :
          sig
            type t = Imandra_tools__Idf.Make(Decomp).Symbolic.G.t
            module V :
              sig
                type t = node
                val compare : t -> t -> int
                val hash : t -> int
                val equal : t -> t -> bool
                type label = node
                val create : label -> t
                val label : t -> label
              end
            type vertex = V.t
            module E :
              sig
                type t = node * step option * node
                val compare : t -> t -> int
                type vertex = vertex
                val src : t -> vertex
                val dst : t -> vertex
                type label = step option
                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 output_graph : t -> file:string -> unit
          end
        type decompose =
            ?traversal:traversal ->
            ?g:G.t ->
            ?from:node ->
            ?basis:string list ->
            ?max_asm_lookahead:int ->
            ?max_ctx_simp:int ->
            ?reduce_symmetry:bool ->
            ?ctx_asm_simp:bool ->
            ?aggressive_rec:bool ->
            ?compound:bool -> target -> paths * (unit -> unit)
        val paths : ?from:node -> G.t -> path list
        val reify : int -> paths -> path list
        val reify_all : paths -> path list
        val regions : path -> Imandra_interactive.Decompose.t list
        val samples : path -> DSM.State_machine.event list
        val ids : path -> (Uuidm.t * Uuidm.t * Uuidm.t) list
        val replay :
          path ->
          (DSM.State_machine.state * DSM.State_machine.event *
           DSM.State_machine.state)
          list
        val decompose : ?lazily:bool -> decompose
        val decompose_par :
          ?active_regions:bool -> schedule:scheduler -> decompose
        val scheduler :
          ?imandra:string ->
          ?oneshot:bool ->
          par:int ->
          ?max_fail:int -> load:string -> idf:string -> unit -> scheduler
        module Worker : sig val start : sock_file:string -> unit -> unit end
      end
    module Sampling :
      sig
        module DSM :
          sig
            module Template :
              sig
                type t = Decomp.Template.t
                val concrete : t -> string list
              end
            module State_machine :
              sig
                type state = Decomp.State_machine.state
                type event = Decomp.State_machine.event
                val init_state : state
                val step : event -> state -> state
                val is_valid : event -> state -> bool
              end
            val module_name : string
          end
        type target = DSM.Template.t list
        type step = Imandra_tools__Idf.Make(Decomp).Sampling.step
        type node = Imandra_tools__Idf.Make(Decomp).Sampling.node
        type edge = node * step * node
        type path = edge list
        type paths = Imandra_tools__Idf.Make(Decomp).Sampling.paths
        type scheduler = Imandra_tools__Idf.Make(Decomp).Sampling.scheduler
        type traversal =
          Imandra_tools__Idf.Make(Decomp).Sampling.traversal =
            DF
          | BF
        module G :
          sig
            type t = Imandra_tools__Idf.Make(Decomp).Sampling.G.t
            module V :
              sig
                type t = node
                val compare : t -> t -> int
                val hash : t -> int
                val equal : t -> t -> bool
                type label = node
                val create : label -> t
                val label : t -> label
              end
            type vertex = V.t
            module E :
              sig
                type t = node * step option * node
                val compare : t -> t -> int
                type vertex = vertex
                val src : t -> vertex
                val dst : t -> vertex
                type label = step option
                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 output_graph : t -> file:string -> unit
          end
        type decompose =
            ?traversal:traversal ->
            ?g:G.t ->
            ?from:node ->
            ?basis:string list ->
            ?max_asm_lookahead:int ->
            ?max_ctx_simp:int ->
            ?reduce_symmetry:bool ->
            ?ctx_asm_simp:bool ->
            ?aggressive_rec:bool ->
            ?compound:bool -> target -> paths * (unit -> unit)
        val paths : ?from:node -> G.t -> path list
        val reify : int -> paths -> path list
        val reify_all : paths -> path list
        val regions : path -> Imandra_interactive.Decompose.t list
        val samples : path -> DSM.State_machine.event list
        val ids : path -> (Uuidm.t * Uuidm.t * Uuidm.t) list
        val replay :
          path ->
          (DSM.State_machine.state * DSM.State_machine.event *
           DSM.State_machine.state)
          list
        val decompose : ?lazily:bool -> decompose
        val decompose_par :
          ?active_regions:bool -> schedule:scheduler -> decompose
        val scheduler :
          ?imandra:string ->
          ?oneshot:bool ->
          par:int ->
          ?max_fail:int -> load:string -> idf:string -> unit -> scheduler
        module Worker : sig val start : sock_file:string -> unit -> unit end
      end
  end
module IDF = D.Symbolic

We are now ready to decompose a SM state machine under a particular TPL.t template using either of the available strategies provided by D, both conforming to the Idf_intf.SIG signature:

  • Sampling: this decomposition strategy is a non complete search that can be used to get an approximate view of the entire state space, as it uses concrete sample values for each event instead of purely symbolic constraints.

  • Symbolic: this decomposition strategy is complete but significantly more computationally expensive than the Sampling strategy, as all the symbolic events are expressed as pure constraints instead of concrete samples.

While the two decomposition strategies work in quite fundamentally different ways, their API is identical and thus switching between one or the other is simply a matter of using D.Symbolic over D.Sampling or vice-versa.

Once we've decided which decomposition strategy to use (we're going to use D.Symbolic in this example, aliased to IDF for simplicity), we need to chose whether to use the in-process, synchronous and potentially lazy entrypoint decompose, or the eager, non blocking and distributed entrypoint decompose_par.

As per Symbolic vs Sampling, we've tried our best to keep the APIs of the two entrypoints as identical as possible, let's look at their similarities and differences:

In [6]:
#show IDF.decompose_par;;
#show IDF.decompose;;
Out[6]:
val decompose_par :
  ?active_regions:bool -> schedule:IDF.scheduler -> IDF.decompose
val decompose : ?lazily:bool -> IDF.decompose
type nonrec decompose =
    ?traversal:IDF.traversal ->
    ?g:IDF.G.t ->
    ?from:IDF.node ->
    ?basis:string list ->
    ?max_asm_lookahead:int ->
    ?max_ctx_simp:int ->
    ?reduce_symmetry:bool ->
    ?ctx_asm_simp:bool ->
    ?aggressive_rec:bool ->
    ?compound:bool -> IDF.target -> IDF.paths * (unit -> unit)

We can see that both functions return a function with type IDF.decompose after a few initial setup differences:

  • decompose takes an optional lazily named argument, which defaults to true and controls whether the decomposition will be lazy or eager
  • decompose_par takes a schedule named argument of type IDF.scheduler which is needed to control the parameters of its parallel/distributed behavior and an optional active_regions named argument, which defaults to true and controls whether the returned regions must be "active" (i.e. usable to be refined or manually extract sample points) in the current process.

Apart from those initial different parameters, the API is then completely identical so swapping between one entrypoint and the other should be just a few lines of difference in the initial setup, looking at the signature of IDF.decompose (printed above), we can see that most of the optional flags are identical to the ones of Imandra's "native" decompose facility, so we'll just defer to its docs for those.

Notable omissions are assuming, which is fundamentally incompatible with Idf, (State_machine.is_valid takes that space), and interpret_basis, which Idf needs to hardcode to true in order to work correctly.

The extra flags are:

  • g: a G.t mutable graph that is a view of the decomposition state of the state machine, defaults to a throwaway graph that will only be used internally. Paths can be extracted from such a graph using the IDF.paths function
  • traversal: the traversal strategy of the decomposition graph, either DF (depth first, default) or BF (breadth first)
  • from: the initial node to start the decomposition from, defaults to a node representing the initial state of the state machine, can be used when running multiple decompositions over a same shared graph

Let's now showcase, using the slightly simpler IDF.decompose, how to start using the IDF module:

In [7]:
let paths, close = IDF.decompose TPL.[Any;AddInt]
Out[7]:
val g___2 : Decomp.State_machine.event -> int -> bool = <fun>
val side_cond_g___3_1 : SM.event list -> int -> int -> bool = <fun>
val side_cond_g___3_0 : Decomp.State_machine.event list -> int -> int -> bool =
  <fun>
val target_g___3_1 : SM.event list -> int -> int = <fun>
val target_g___3_0 : Decomp.State_machine.event list -> int -> int = <fun>
val paths : IDF.paths = <abstr>
val close : unit -> unit = <fun>

We've invoked D.Symbolic.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 _)))

Calls to decompose (and decompose_par) return a tuple of two values: the first value is a paths generator, while the second is a unit -> unit function to be invoked once all the regions one needs have been computed, in order to release all the resources.

In order to consume concrete paths from the paths generator we must reify them (we'll just reify a single path for this example, and release the resources immediately after):

In [8]:
let first_path = IDF.reify 1i paths |> List.hd;;
close ();;
Out[8]:
val g___4 : Decomp.State_machine.event list -> bool = <fun>
val g___5 : Decomp.State_machine.event list -> int = <fun>
val sc_g___6 : Decomp.State_machine.event list -> bool = <fun>
val sc_g___34 : Decomp.State_machine.event list -> bool = <fun>
val g___89 : SM.event list -> bool = <fun>
val g___90 : SM.event list -> int = <fun>
val sc_g___118 : SM.event list -> bool = <fun>
val sc_g___154 : Decomp.State_machine.event list -> bool = <fun>
val first_path : IDF.path =
  [(<abstr>, <abstr>, <abstr>); (<abstr>, <abstr>, <abstr>)]
- : unit = ()

Since we're decomposing lazily (i.e. we haven't invoked IDF.decompose ~lazily:false), the process of reifying a path for the first time will actually be responsible for starting the decomposition process until a first path is available.

Reifying the nth path multiple times will only cause it to be computed the first time, subsequent reifications will simply return the cached path.

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 [9]:
let samples = IDF.samples first_path
Out[9]:
val samples : IDF.DSM.State_machine.event list =
  [Decomp.State_machine.Add Decomp.State_machine.Zero;
   Decomp.State_machine.Add (Decomp.State_machine.Int 51)]
  • 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 [10]:
let replayed_path = IDF.replay first_path
Out[10]:
val replayed_path :
  (IDF.DSM.State_machine.state * IDF.DSM.State_machine.event *
   IDF.DSM.State_machine.state)
  list =
  [(0, Decomp.State_machine.Add Decomp.State_machine.Zero, 0);
   (0, Decomp.State_machine.Add (Decomp.State_machine.Int 51), 51)]
  • We can ask for the concrete regions representing the constraints of the state machine up to each event in the path:
In [11]:
#install_printer Imandra_tools.Region_pp.print;;

let regions = IDF.regions first_path
Out[11]:
val regions : Imandra_interactive.Decompose.t list =
  [---[region]---
   Constraints:
     [ Destruct(SM.Add, 0, (List.hd (List.tl e))) is SM.Int
     ; (List.hd (List.tl e)) is SM.Add
     ; (List.hd e) is SM.Add
     ; Destruct(SM.Add, 0, (List.hd e)) is SM.Zero
     ; (List.tl (List.tl e)) = [] ]
   Invariant:
     F = 0
    -------------;
   ---[region]---
   Constraints:
     [ Destruct(SM.Add, 0, (List.hd e)) is SM.Zero
     ; (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
     ; (List.tl (List.tl e)) = []
     ; 50 <
       Destruct(SM.Int, 0, Destruct(SM.Add, 0, (List.hd (List.tl e)))) <=
       9000 ]
   Invariant:
     F = 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) = [].

  • We can ask for the unique ids of each state and event values in a path, the string repr of each uuid is used as labels in the G.t graph
In [12]:
#install_printer Uuidm.pp;;

let ids = IDF.ids first_path
Out[12]:
val ids : (Uuidm.t * Uuidm.t * Uuidm.t) list =
  [(46742573-0ed5-4201-ad0b-19967edcfb4c,
    9e7726e5-5498-4171-812c-a8c8a6a071e0,
    80f70a41-a220-48b1-a361-df8228449946);
   (80f70a41-a220-48b1-a361-df8228449946,
    626e5aef-7ab8-4d8d-a16c-040b82ca18eb,
    d7184fb6-f864-4fc8-ae1e-a8c1b355e5fa)]

Finally, let's showcase what it would take to set up a parallel decomposition:

let scheduler = IDF.scheduler ~par:1i ~load:"idf_setup.iml" ~idf:"D.Symbolic" ()
let paths, close = IDF.decompose_par ~schedule:scheduler TPL.[Any;AddInt]

The first thing we've created is a scheduler telling it to:

  • use a parallelism level of 1, meaning that 1 extra worker will be started (the parallel decomposer uses by default a minumum of 2 processes, a coordinator and worker)
  • setup idf from a local file called idf_setup.iml: the file should contain all the code we've shown above up to (and including) the insantiatiation of the D module
  • the name of the module implementing Idf_intf.SIG to be used to decompose the model from the worker processes

After having created a scheduler, all the remains to do is merely to invoke decompose_par with the appropriate schedule argument, and the usage is identical to what we've already described for decompose.