Make (imandra-tools.Imandra

Parameters

module DSM : Idf_intf.DSM_SIG

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

val model : node -> Imandra_interactive.Extract.model option

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.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:Imandra_util.Logic_config.op list ->
  target ->
  G.t

Decompose a state machine using a symbolic template