A module which serves as a dummy dynamic pop handler. This handler should be used when no dynamic pops are required of the PDS.
module Basis : Pds_reachability_basis.Basismodule Stack_element = Basis.Stack_elementThe decorated type of stack elements in the PDS.
module State = Basis.StateThe decorated type of states in the PDS.
The decorated type of targeted dynamic pop actions in the PDS.
The decorated type of untargeted dynamic pop actions in the PDS.
module Stack_action :
Decorated_stack_action_type
with type stack_element = Stack_element.t
and type targeted_dynamic_pop_action = Targeted_dynamic_pop_action.tThe decorated type of stack actions in the PDS.
module Terminus :
Decorated_terminus_type
with type state = State.t
and type untargeted_dynamic_pop_action = Untargeted_dynamic_pop_action.tThe decorated type of termini in the PDS.
val perform_targeted_dynamic_pop :
Stack_element.t ->
Targeted_dynamic_pop_action.t ->
Stack_action.t list Batteries.Enum.tThe resolution function for targeted dynamic pops. This function takes a stack element which was pushed and the associated dynamic pop action. The result is an enumeration of stack action sequences. Each sequence is added to the PDS such that it starts at the source of the push and ends at the target of the dynamic pop.
val perform_untargeted_dynamic_pop :
Stack_element.t ->
Untargeted_dynamic_pop_action.t ->
(Stack_action.t list * Terminus.t) Batteries.Enum.tThe resolution function for untargeted dynamic pops. This function takes a stack element which was pushed and the associated dynamic pop action. The result is an enumeration of pairs between stack action sequences and their eventual target.