pds-reachability 0.2 · OCaml Package

This module defines basic data types for the stack of a PDS.

type ('stack_element, 'targeted_dynamic_pop_action) pds_stack_action =

| Push of 'stack_element
(*
Represents the push of a single stack element.
*)
| Pop of 'stack_element
(*
Represents the pop of a single stack element.
*)
| Nop
(*
Represents no action being taken on the stack.
*)
| Pop_dynamic_targeted of 'targeted_dynamic_pop_action
(*
Represents a pop operation which leads to the target node only after performing a series of stack actions. These stack actions are not fixed; they vary depending upon the stack element which is provided. This operation may also be non-deterministic, providing several chains of operations to the same target.
*)

The type of stack actions which may be performed in a PDS.

val equal_pds_stack_action : 
  'stack_element 'targeted_dynamic_pop_action. ('stack_element ->
                                                 'stack_element ->
                                                 Ppx_deriving_runtime.bool) ->
  ('targeted_dynamic_pop_action ->
    'targeted_dynamic_pop_action ->
    Ppx_deriving_runtime.bool) ->
  ('stack_element, 'targeted_dynamic_pop_action) pds_stack_action ->
  ('stack_element, 'targeted_dynamic_pop_action) pds_stack_action ->
  Ppx_deriving_runtime.bool

val compare_pds_stack_action : 
  'stack_element 'targeted_dynamic_pop_action. ('stack_element ->
                                                 'stack_element ->
                                                 Ppx_deriving_runtime.int) ->
  ('targeted_dynamic_pop_action ->
    'targeted_dynamic_pop_action ->
    Ppx_deriving_runtime.int) ->
  ('stack_element, 'targeted_dynamic_pop_action) pds_stack_action ->
  ('stack_element, 'targeted_dynamic_pop_action) pds_stack_action ->
  Ppx_deriving_runtime.int

val pp_pds_stack_action : 
  'stack_element 'targeted_dynamic_pop_action. (Ppx_deriving_runtime.Format.formatter ->
                                                 'stack_element ->
                                                 Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter ->
    'targeted_dynamic_pop_action ->
    Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  ('stack_element, 'targeted_dynamic_pop_action) pds_stack_action ->
  Ppx_deriving_runtime.unit

val show_pds_stack_action : 
  'stack_element 'targeted_dynamic_pop_action. (Ppx_deriving_runtime.Format.formatter ->
                                                 'stack_element ->
                                                 Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter ->
    'targeted_dynamic_pop_action ->
    Ppx_deriving_runtime.unit) ->
  ('stack_element, 'targeted_dynamic_pop_action) pds_stack_action ->
  Ppx_deriving_runtime.string

val pds_stack_action_to_yojson : 
  'stack_element 'targeted_dynamic_pop_action. ('stack_element ->
                                                 Yojson.Safe.t) ->
  ('targeted_dynamic_pop_action -> Yojson.Safe.t) ->
  ('stack_element, 'targeted_dynamic_pop_action) pds_stack_action ->
  Yojson.Safe.t

val _ : 
  ('a -> Yojson.Safe.t) ->
  ('b -> Yojson.Safe.t) ->
  ('a, 'b) pds_stack_action ->
  Yojson.Safe.t

module type Dynamic_pop_handler = sig ... end

The type of a module which resolves dynamic pops.

module Null_dynamic_pop_hanlder
  (Basis : Pds_reachability_basis.Basis) : 
  Dynamic_pop_handler
    with module Stack_element = Basis.Stack_element
     and module State = Basis.State

A module which serves as a dummy dynamic pop handler. This handler should be used when no dynamic pops are required of the PDS.

package pds-reachability