package pds-reachability

  1. Overview
  2. Docs
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.

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

The decorated type of untargeted dynamic pop actions 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.