Make (p.pds-reachability.0.2.doc.pds-reachability.Pds_reachability

Parameters

module Basis : Pds_reachability_basis.Basis

module Dph : 
  Pds_reachability_types_stack.Dynamic_pop_handler
    with module Stack_element = Basis.Stack_element
     and module State = Basis.State

module Work_collection_template_impl : Pds_reachability_work_collection.Work_collection_template

Signature

include Pds_reachability_types.Types
  with module State = Basis.State
  with module Stack_element = Basis.Stack_element
  with module Targeted_dynamic_pop_action = Dph.Targeted_dynamic_pop_action
  with module Untargeted_dynamic_pop_action = Dph.Untargeted_dynamic_pop_action

Sourcemodule State = Basis.State

The decorated type of states in the PDS.

Sourcemodule Stack_element = Basis.Stack_element

The decorated type of stack elements in the PDS.

Sourcemodule Targeted_dynamic_pop_action = Dph.Targeted_dynamic_pop_action

The decorated type of targeted dynamic pop actions in the PDS.

Sourcemodule Untargeted_dynamic_pop_action = Dph.Untargeted_dynamic_pop_action

The decorated type of untargeted dynamic pop actions in the PDS.

Source

type stack_action =
  (Stack_element.t, Targeted_dynamic_pop_action.t)
    Pds_reachability_types_stack.pds_stack_action

Stack actions which may be performed in the PDS.

Sourceval pp_stack_action : stack_action Jhupllib.Pp_utils.pretty_printer

Sourceval show_stack_action : stack_action -> string

Sourceval stack_action_to_yojson : stack_action -> Yojson.Safe.json

Sourcetype node =

| State_node of State.t
| Intermediate_node of node * stack_action list

Sourcemodule Node : Pds_reachability_utils.Decorated_type with type t = node

The decorated type of node used for reachability.

Sourcetype edge = {

source : Node.t;
target : Node.t;
edge_action : stack_action;

}

Sourcemodule Edge : Pds_reachability_utils.Decorated_type with type t = edge

The decorated type of edge used in reachability.

Sourcetype edge_function = State.t -> (stack_action list * State.t) Batteries.Enum.t

The type of edge-generating functions used in this analysis.

Source

type untargeted_dynamic_pop_action_function =
  State.t ->
  Untargeted_dynamic_pop_action.t Batteries.Enum.t

The type of functions to generate untargeted dynamic pop actions in this analysis.

Sourcetype analysis

The type of a reachability analysis in this module.

Sourcetype analysis_logging_function = analysis -> analysis -> unit

The type of reachability analysis logging functions. These functions are called whenever the associated analysis is stepped. The two arguments are the analysis before stepping and the analysis after.

Source

val empty : 
  ?logging_function:analysis_logging_function option ->
  unit ->
  analysis

The empty analysis. This analysis has no states, edges, or edge functions.

Sourceval add_edge : State.t -> stack_action list -> State.t -> analysis -> analysis

Adds a single edge to a reachability analysis.

Sourceval add_edge_function : edge_function -> analysis -> analysis

Adds a function to generate edges for a reachability analysis. Given a source node, the function generates edges from that source node. The function must be pure; for a given source node, it must generate all edges that it can generate on the first call.

Source

val add_untargeted_dynamic_pop_action : 
  State.t ->
  Untargeted_dynamic_pop_action.t ->
  analysis ->
  analysis

Adds an untargeted pop action to a reachability analysis. Untargeted pop action are similar to targeted pop actions except that they are not created as an edge with a target node; instead, the target is decided in some way by the pushed element that the untargeted dynamic pop is consuming.

Source

val add_untargeted_dynamic_pop_action_function : 
  untargeted_dynamic_pop_action_function ->
  analysis ->
  analysis

Adds a function to generate untargeted dynamic pop ations for a reachability analysis. Given a source node, the function generates untargeted actions from that source node. The function must be pure; for a given source, it must generate all actions that it can generate on the first call.

Sourceval add_start_state : State.t -> stack_action list -> analysis -> analysis

Adds a state and initial stack element to the analysis. This permits the state to be used as the source state of a call to get_reachable_states.

Sourceval is_closed : analysis -> bool

Determines whether the reachability analysis is closed.

Sourceval closure_step : analysis -> analysis

Takes a step toward closing a given reachability analysis. If the analysis is already closed, it is returned unchanged.

Sourceval fully_close : analysis -> analysis

Fully closes the provided analysis.

Source

val get_reachable_states : 
  State.t ->
  stack_action list ->
  analysis ->
  State.t Batteries.Enum.t

Determines the states which are reachable from a given state and initial stack element. This state must have been added to the analysis previously. If the analysis is not fully closed, then the enumeration of reachable states may be incomplete.

Sourceval pp_analysis : analysis Jhupllib.Pp_utils.pretty_printer

Pretty-printing function for the analysis.

Sourceval show_analysis : analysis -> string

Sourceexception Reachability_request_for_non_start_state of State.t

An exception raised when a reachable state query occurs before the state is added as a start state.

Sourceval get_size : analysis -> int * int

Determines the size of the provided analysis in terms of both node and edge count (respectively).

Sourceval get_work_count : analysis -> int

Determines the amount of work done on a particular analysis.

Sourceval dump_yojson : analysis -> Yojson.Safe.json

Extracts a subset of information about an analysis state as JSON data. Some parts of the analysis state (such as edge functions) will be elided as they cannot be represented.

Sourceval dump_yojson_delta : analysis -> analysis -> Yojson.Safe.json

Extracts a subset of information about an analysis state as JSON data. This extraction generates a /difference/ between two reachability analyses, giving values appearing in the latter but not the former. This function assumes the latter is a strict superset of the former; any values appearing in the former and not the latter are ignored. The format of this dump is identical to that given by dump_yojson.