Module Idf.Make

Create a new IDF module for the given SM state machine

Parameters

Signature

type shape =
| Tree
type pol =
| Valid
| Invalid
| No
| Custom of string
module DSM = DSM

State machine to decompose

val pp_state : DSM.State_machine.state -> string

Printer function for a value of the state machine *

type target = DSM.Template.t list

Symbolic target of a decomposition

type node

Symbolic decomposed node of a state machine

type path = node list

Symbolic decomposed list of edges of a state machine

module G : sig ... end

Decomposition graph

module Mex : sig ... end
type region_id = int
val id : node -> region_id
val paths : ?from:node -> G.t -> path list

Return a list of paths from a decomposition graph starting at optional node (defaults to the root node)

val region : node -> Imandra_surface.Modular_region.RRef.t

Returns the region of a node

val concrete_region : node -> Imandra_surface.Modular_region.t

Returns the concrete region of a node

val expanded_region_ids : node -> Imandra_util.Util.Int_set.t

Returns set of regions originating from region expansion.

val applied_expander_fns : node -> Imandra_util.Util.Str_set.t list

Returns the set of projection functions applied during region expansion, by step.

val sample : node -> DSM.State_machine.event list option

Returns the sample point of a node - a list of concrete events to get to the current node

type region_expander = {
valid_fn : string option;
field_projections : string list list;
expand_when : string option;
}
type target_step = {
event : DSM.Template.t;
valid_pol : pol;
region_expander : region_expander option;
}
val target_steps : node -> target_step list list
type replay_sample = {
state_before : DSM.State_machine.state;
event : DSM.State_machine.event;
state_after : DSM.State_machine.state;
}

sample replay output states and event

val replay_events : DSM.State_machine.event list -> replay_sample list

Replay a list of events to generate concrete state machine states from the initial state

val replay : node -> replay_sample list option

Replay a node's sample events to generate concrete state machine states from the initial state

type runner
val create : ?basis:string list -> ?expanding:string list -> ?assuming:string -> ?rule_specs:string list -> ?get_model_config:Imandra_util.Pconfig.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:Imandra_util.Pconfig.op list -> target -> G.t

Decompose a state machine using a symbolic template