module Basis : Pds_reachability_basis.Basismodule Dph :
Pds_reachability_types_stack.Dynamic_pop_handler
with module Stack_element = Basis.Stack_element
and module State = Basis.Stateinclude 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
with module Stack_action = Dph.Stack_action
with module Terminus = Dph.Terminusmodule State = Basis.StateThe decorated type of states in the PDS.
module Stack_element = Basis.Stack_elementThe decorated type of stack elements in the PDS.
The type of classes of states in the PDS.
module Targeted_dynamic_pop_action = Dph.Targeted_dynamic_pop_actionThe decorated type of targeted dynamic pop actions in the PDS.
module Untargeted_dynamic_pop_action = Dph.Untargeted_dynamic_pop_actionThe decorated type of untargeted dynamic pop actions in the PDS.
module Stack_action = Dph.Stack_actionStack actions which may be performed in the PDS.
module Terminus = Dph.TerminusTermini of paths which may exist in the PDS.
type intermediate_destination = | Static_destination of node| Dynamic_destination of Untargeted_dynamic_pop_action.tand node = | State_node of State.t| Intermediate_node of intermediate_destination * Stack_action.t listmodule Node : Pds_reachability_utils.Decorated_type with type t = nodeThe decorated type of node used for reachability.
module Edge : Pds_reachability_utils.Decorated_type with type t = edgeThe decorated type of edge used in reachability.
type edge_function =
State.t ->
(Stack_action.t list * Terminus.t) Batteries.Enum.tThe type of edge-generating functions used in this analysis.
type untargeted_dynamic_pop_action_function =
State.t ->
Untargeted_dynamic_pop_action.t Batteries.Enum.tThe type of functions to generate untargeted dynamic pop actions in this analysis.
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.
val empty :
?logging_function:analysis_logging_function option ->
unit ->
analysisThe empty analysis. This analysis has no states, edges, or edge functions.
val add_edge :
State.t ->
Stack_action.t list ->
State.t ->
analysis ->
analysisAdds a single edge to a reachability analysis.
val add_edge_function : edge_function -> analysis -> analysisAdds 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. This routine will be called on all nodes that are introduced to the PDS.
val add_classified_edge_function :
Class.t ->
edge_function ->
analysis ->
analysisAdds a function to generate edges for a reachability analysis on states with the specified class. This routine operates as add_edge_function except that the provided function will *not* be called on nodes which have a different class.
val add_untargeted_dynamic_pop_action :
State.t ->
Untargeted_dynamic_pop_action.t ->
analysis ->
analysisAdds 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.
val add_untargeted_dynamic_pop_action_function :
untargeted_dynamic_pop_action_function ->
analysis ->
analysisAdds 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.
val add_classified_untargeted_dynamic_pop_action_function :
Class.t ->
untargeted_dynamic_pop_action_function ->
analysis ->
analysisAdds a function to generate untargeted dynamic pop ations for a reachability analysis for nodes of a particular class. This routine works as add_untargeted_dynamic_pop_action_function but only invokes the provided function on nodes of a particular class.
val add_start_state : State.t -> Stack_action.t list -> analysis -> analysisAdds 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.
val is_closed : analysis -> boolDetermines whether the reachability analysis is closed.
Takes a step toward closing a given reachability analysis. If the analysis is already closed, it is returned unchanged.
val closure_step_reachable :
analysis ->
analysis * (State.t * Stack_action.t list * State.t) option Stdlib.Lazy.tTakes a step toward closing a given reachability analysis. If the analysis is already closed, it is returned unchanged. If a start state is found to reach another state, that pair of states will be returned in a lazy computation.
val get_reachable_states :
State.t ->
Stack_action.t list ->
analysis ->
State.t Batteries.Enum.tDetermines 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.
val pp_analysis : analysis Jhupllib.Pp_utils.pretty_printerPretty-printing function for the analysis.
val show_analysis : analysis -> stringexception Reachability_request_for_non_start_state of State.tAn exception raised when a reachable state query occurs before the state is added as a start state.
val get_size : analysis -> int * intDetermines the size of the provided analysis in terms of both node and edge count (respectively).
val get_work_count : analysis -> intDetermines the amount of work done on a particular analysis.
val dump_yojson : analysis -> Yojson.Safe.tExtracts 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.
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.