package pds-reachability

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

pds-reachability

Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module Basis : Pds_reachability_basis.Basis

module Dph : 
  Pds_reachability_types_stack.Dynamic_pop_handler
    with module Stack_element = Basis.Stack_element
     and module State = Basis.State

Signature

module State = Basis.State

The decorated type of states in the PDS.

module Stack_element = Basis.Stack_element

The decorated type of stack elements in the PDS.

module Targeted_dynamic_pop_action = Dph.Targeted_dynamic_pop_action

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

module Untargeted_dynamic_pop_action = Dph.Untargeted_dynamic_pop_action

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

Stack actions which may be performed in the PDS.

val pp_stack_action : stack_action Jhupllib.Pp_utils.pretty_printer

val show_stack_action : stack_action -> string

val stack_action_to_yojson : stack_action -> Yojson.Safe.json

type node =

| State_node of State.t
| Intermediate_node of node * stack_action list

module Node : Pds_reachability_utils.Decorated_type with type t = node

The decorated type of node used for reachability.

type edge = {

source : Node.t;
target : Node.t;
edge_action : stack_action;

}

module Edge : Pds_reachability_utils.Decorated_type with type t = edge

The decorated type of edge used in reachability.