package pds-reachability

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

The type of a module which resolves dynamic pops.

The decorated type of stack elements in the PDS.

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

The decorated type of stack actions in the PDS.

The decorated type of termini in the PDS.

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.

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.