package pds-reachability

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
module State = Basis.State

The decorated type of states in the PDS.

module Stack_element = Basis.Stack_element

The decorated type of stack elements in the PDS.

module Targeted_dynamic_pop_action = Dph.Targeted_dynamic_pop_action

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

module Untargeted_dynamic_pop_action = Dph.Untargeted_dynamic_pop_action

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

type intermediate_destination =
  1. | Static_destination of node
  2. | Dynamic_destination of Untargeted_dynamic_pop_action.t
and node =
  1. | State_node of State.t
  2. | Intermediate_node of intermediate_destination * Stack_action.t list

The decorated type of node used for reachability.

type edge = {
  1. source : Node.t;
  2. target : Node.t;
  3. edge_action : Stack_action.t;
}

The decorated type of edge used in reachability.