This module defines basic data types for the stack of a PDS.
module type Decorated_stack_action_type = sig ... endThe type of a decorated stack action module.
module Stack_action_constructor
(Stack_element : Pds_reachability_utils.Decorated_type)
(Targeted_dynamic_pop_action : Pds_reachability_utils.Decorated_type) :
Decorated_stack_action_type
with type stack_element = Stack_element.t
and type targeted_dynamic_pop_action = Targeted_dynamic_pop_action.tA functor to create a decorated stack action type.
module type Decorated_terminus_type = sig ... endThe type of a module containing a decorated type for describing the end of a path in a PDS.
module Terminus_constructor
(State : Pds_reachability_utils.Decorated_type)
(Untargeted_dynamic_pop_action : Pds_reachability_utils.Decorated_type) :
Decorated_terminus_type
with type state = State.t
and type untargeted_dynamic_pop_action = Untargeted_dynamic_pop_action.tA functor to create a decorated stack action type.
module type Dynamic_pop_handler = sig ... endThe type of a module which resolves dynamic pops.
module Null_dynamic_pop_hanlder
(Basis : Pds_reachability_basis.Basis) :
Dynamic_pop_handler
with module Stack_element = Basis.Stack_element
and module State = Basis.StateA module which serves as a dummy dynamic pop handler. This handler should be used when no dynamic pops are required of the PDS.