package pds-reachability

You can search for identifiers within the package.

in-package search v0.2.0

pds-reachability

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Stack_element = Basis.Stack_element

The decorated type of stack elements in the PDS.

module State = Basis.State

The decorated type of states in the PDS.

module Targeted_dynamic_pop_action : Pds_reachability_utils.Decorated_type

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

module Untargeted_dynamic_pop_action : Pds_reachability_utils.Decorated_type

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

type stack_action =
  (Stack_element.t, Targeted_dynamic_pop_action.t)
    Pds_reachability_types_stack.pds_stack_action

A type alias for stack actions in this handler.

val perform_targeted_dynamic_pop : 
  Stack_element.t ->
  Targeted_dynamic_pop_action.t ->
  stack_action list Batteries.Enum.t

The 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 list * State.t) Batteries.Enum.t

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