pds-reachability 0.2.2 · OCaml Package

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

module Stack_element = Basis.Stack_element

The decorated stack element type used by the PDS.

module Node = Types.Node

The decorated node type in the reachability structure.

module Edge = Types.Edge

The decorated edge type in the reachability structure.

module Targeted_dynamic_pop_action = Types.Targeted_dynamic_pop_action

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

module 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

type t

val equal : t -> t -> bool

val compare : t -> t -> int

val pp : t Jhupllib.Pp_utils.pretty_printer

val show : t -> string

val to_yojson : t -> Yojson.Safe.json

val 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.

val empty : t

The empty PDS reachability structure.

val add_edge : Edge.t -> t -> t

Adds an edge to a reachability structure.

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

Determines if a structure has a particular edge.

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.

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.

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

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

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

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

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

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

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

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

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

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

Submodules.

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

package pds-reachability

Parameters

Signature

Query functions.

Submodules.