Module `Pds_reachability_structure.Make`Source

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 Types : 
  Pds_reachability_types.Types
    with module State = Basis.State
     and module Stack_element = Basis.Stack_element
     and module Targeted_dynamic_pop_action = Dph.Targeted_dynamic_pop_action
     and module Untargeted_dynamic_pop_action =
           Dph.Untargeted_dynamic_pop_action

Signature

Sourcemodule Stack_element = Basis.Stack_element

The decorated stack element type used by the PDS.

Sourcemodule Node = Types.Node

The decorated node type in the reachability structure.

Sourcemodule Edge = Types.Edge

The decorated edge type in the reachability structure.

Sourcemodule Targeted_dynamic_pop_action = Types.Targeted_dynamic_pop_action

The decorated type of targeted dynamic pop actions in this structure.

Sourcemodule Untargeted_dynamic_pop_action = Types.Untargeted_dynamic_pop_action

The decorated type of untargeted dynamic pop actions in this structure.

The type of the PDS reachability data structure.

include Pds_reachability_utils.Decorated_type

Sourcetype t

Sourceval equal : t -> t -> bool

Sourceval compare : t -> t -> int

Sourceval pp : t Jhupllib.Pp_utils.pretty_printer

Sourceval show : t -> string

Sourceval to_yojson : t -> Yojson.Safe.json

Sourceval to_yojson_delta : t -> t -> Yojson.Safe.json

Produces a Yojson structure representing the contents of a latter analysis which do not appear in the former.

Sourceval empty : t

The empty PDS reachability structure.

Sourceval add_edge : Edge.t -> t -> t

Adds an edge to a reachability structure.

Sourceval has_edge : Edge.t -> t -> bool

Determines if a structure has a particular edge.

Source

val add_untargeted_dynamic_pop_action : 
  Node.t ->
  Untargeted_dynamic_pop_action.t ->
  t ->
  t

Adds an untargeted dynamic pop action to a reachability structure.

Source

val has_untargeted_dynamic_pop_action : 
  Node.t ->
  Untargeted_dynamic_pop_action.t ->
  t ->
  bool

Determines if a given untargeted dynamic pop action is present in a reachability structure.

Query functions.

Source

val find_push_edges_by_source : 
  Node.t ->
  t ->
  (Node.t * Stack_element.t) Batteries.Enum.t

Source

val find_pop_edges_by_source : 
  Node.t ->
  t ->
  (Node.t * Stack_element.t) Batteries.Enum.t

Sourceval find_nop_edges_by_source : Node.t -> t -> Node.t Batteries.Enum.t

Source

val find_targeted_dynamic_pop_edges_by_source : 
  Node.t ->
  t ->
  (Node.t * Targeted_dynamic_pop_action.t) Batteries.Enum.t

Source

val find_untargeted_dynamic_pop_actions_by_source : 
  Node.t ->
  t ->
  Untargeted_dynamic_pop_action.t Batteries.Enum.t

Source

val find_push_edges_by_target : 
  Node.t ->
  t ->
  (Node.t * Stack_element.t) Batteries.Enum.t

Source

val find_pop_edges_by_target : 
  Node.t ->
  t ->
  (Node.t * Stack_element.t) Batteries.Enum.t

Sourceval find_nop_edges_by_target : Node.t -> t -> Node.t Batteries.Enum.t

Sourceval enumerate_nodes : t -> Node.t Batteries.Enum.t

Sourceval enumerate_edges : t -> Edge.t Batteries.Enum.t

Submodules.

Sourcemodule Node_set : Batteries.Set.S with type elt = Node.t

package pds-reachability

Module Pds_reachability_structure.MakeSource

Parameters

Signature

Query functions.

Submodules.

Module `Pds_reachability_structure.Make`Source