Abstraction¶

An abstraction maps the (often continuous) state and action spaces of an environment onto abstract spaces. A discrete abstraction is what allows verigym to learn an explicit MDP from a simulator. An AbstractionMapper combines one AbstractionMap for the states and one for the actions. The functions under Building maps create mappers from common discretizations, e.g., linspace_mapper for evenly spaced bins. Discretization contains the underlying binning, and Gymnasium wrappers and spaces contains helpers to prepare environments, e.g., ReplaceInfObservation for observation spaces with infinite bounds. For an a detailed guide, see the abstraction mapping guide.

Abstraction maps¶

class verigym.AbstractionMapper(state_abstraction_map: AbstractionMap, action_abstraction_map: AbstractionMap, cache: bool = False)[source]¶

The full abstraction mapping between two environments: states and actions.

Holds one AbstractionMap for the state space and one for the action space. Do not confuse with AbstractionMap, which only covers a single space.

Variables:

_state_abstraction_map (AbstractionMap) – The state abstraction map between original and abstract environment.
_action_abstraction_map (AbstractionMap) – The action abstraction map between original and abstract environment.
from_continuous_states (bool | None) – Whether the original state space is continuous (gym.spaces.Box).
from_continuous_actions (bool | None) – Whether the original action space is continuous (gym.spaces.Box).
original_n_actions (original_n_states,) – Element counts of the original spaces; float('inf') if continuous.
abstract_n_actions (abstract_n_states,) – Element counts of the abstract spaces; float('inf') if continuous.

Provides a mapping between abstract and original spaces for an environment (state and action space).

Parameters:

state_abstraction_map (AbstractionMap) – Mapping between original and abstract states.
action_abstraction_map (AbstractionMap) – Mapping between original and abstract actions.
cache (bool, default False) –
Convenience forwarder: enables memoisation of the original -> abstract direction on both maps. The cache itself lives on AbstractionMap – see AbstractionMap.original_to_abstract.

Note that this mutates the two maps, so a map shared with another mapper becomes cached as well. That is sound, since the maps are required to be pure.

property state_backward_kind: BackwardKind¶

The declared payload shape of the state backward map.

Return type:: BackwardKind

property action_backward_kind: BackwardKind¶

The declared payload shape of the action backward map.

Return type:: BackwardKind

original_to_abstract_state(orig_state: NDArray) → NDArray[source]¶

Maps an original state to its abstract state.

Parameters:: orig_state (NDArray) – A state in the original environment.
Returns:: A sample of the abstract state space. Use original_to_abstract_state_enum when a single int is required. Memoised when the state map was built with cache=True, in which case the result must be treated as read-only.
Return type:: NDArray

original_to_abstract_state_enum(orig_state: NDArray) → int[source]¶

Map an original state to a single flat abstract state index.

Parameters:: orig_state (NDArray) – A state in the original environment.
Returns:: A flat index in [0, abstract_n_states), usable as a dict key and an array index. Memoised when the state map was built with cache=True.
Return type:: int

abstract_to_original_state(abs_state: int | NDArray) → Point | Interval | StateSet[source]¶

Maps an abstract state to the original state(s) it stands for.

Parameters:: abs_state (int | NDArray) – A state in the abstracted environment.
Returns:: Shape determined by state_backward_kind.
Return type:: Point | Interval | StateSet
Raises:: ValueError – If the state map has no backward map.

abstract_to_original_state_enum(abs_state: int) → Point | Interval | StateSet[source]¶

Map a flat abstract state index to the original state(s) it stands for.

Parameters:: abs_state (int) – A flat index in [0, abstract_n_states).
Returns:: Shape determined by state_backward_kind.
Return type:: Point | Interval | StateSet

original_to_abstract_action(orig_action: NDArray) → NDArray[source]¶

Maps an original action to its factored abstract action.

Parameters:: orig_action (NDArray) – An action in the original environment.
Returns:: A sample of the abstract action space. Memoised when the action map was built with cache=True, in which case the result must be treated as read-only.
Return type:: NDArray

original_to_abstract_action_enum(orig_action: NDArray) → int[source]¶

Map an original action to a single flat abstract action index.

Parameters:: orig_action (NDArray) – An action in the original environment.
Returns:: A flat index in [0, abstract_n_actions). Memoised when the action map was built with cache=True.
Return type:: int

abstract_to_original_action(abs_action: int | NDArray) → Point | Interval | StateSet[source]¶

Maps an abstract action to a(n) (set/range of) original action(s).

Parameters:: abs_action (int | NDArray) – An action in the abstract environment.
Returns:: Shape determined by action_backward_kind.
Return type:: Point | Interval | StateSet
Raises:: ValueError – If the action map has no backward map.

abstract_to_original_action_enum(abs_action: int) → Point | Interval | StateSet[source]¶

Map a flat abstract action index to the original action(s) it stands for.

Parameters:: abs_action (int) – A flat index in [0, abstract_n_actions).
Returns:: Shape determined by action_backward_kind.
Return type:: Point | Interval | StateSet

classmethod initialize_identity_mapper(state_space: Space, action_space: Space, cache: bool = False) → AbstractionMapper[source]¶

Initialize an AbstractionMapper instance that has an “identity map”, meaning that both the original space and abstract space are the same.

Parameters:

state_space (gym.Space) – The gym space the state space corresponds to.
action_space (gym.Space) – The gym space the action space corresponds to.
cache (bool, default False) – Memoise the original -> abstract direction on both maps.

Returns:

The initialized identity AbstractionMapper.

Return type:

AbstractionMapper

class verigym.abstraction.abstractionmapper.AbstractionMap(forward_map: Callable[[NDArray], NDArray], backward_map: Callable[[NDArray], Point | Interval | StateSet] | None = None, original_space: Space = None, abstract_space: Space = None, backward_kind: BackwardKind | str = BackwardKind.POINT, abstract_to_enum: Callable[[NDArray], int] | None = None, enum_to_abstract: Callable[[int], NDArray] | None = None, cache: bool = False, is_identity_map: bool = False)[source]¶

Functions mapping between one original space and one abstract space.

Usable for either a state space or an action space. Do not confuse with AbstractionMapper, which holds two maps: one for states and one for actions.

Variables:

original_space (gym.spaces.Space) – The original environment’s space.
abstract_space (gym.spaces.Space) – The abstract environment’s space. For a binned map this is MultiDiscrete(bin_edges.n_bins).
forward_map (Callable) – original_space sample -> abstract_space sample.
backward_map (Callable | None) – abstract_space sample -> original_space sample. Type is described by backward_kind paremeter.
backward_kind (BackwardKind) – The type of what backward_map returns. See BackwardKind class for details (POINT, INTERVAL, SET).
original_n_elements (int | float | None) – Element count of original_space; float('inf') for a Box.
abstract_n_elements (int | float | None) – Element count of abstract_space; float('inf') for a Box.
from_continuous_space (bool | None) – Whether original_space is a gym.spaces.Box.
abstract_to_enum (Callable | None) – abstract_space sample -> single flat index. None if the map was built without one, which makes it not is_enumerable.
enum_to_abstract (Callable | None) – Single flat index -> abstract_space sample. Inverse of abstract_to_enum.

Notes

With cache=True the forward direction is memoised in two dicts: _abstract_cache for original_to_abstract and _enum_cache for original_to_enum.

Build a map between an original and an abstract space.

Parameters:

forward_map (Callable[[NDArray], NDArray]) – Maps a sample of original_space to a sample of abstract_space.
backward_map (Callable, optional) – Maps a sample of abstract_space to original_space in the type determined by backward_kind. Default None, which forces backward_kind = BackwardKind.UNKNOWN.
original_space (gym.spaces.Space) – The original gym space.
abstract_space (gym.spaces.Space) – The abstract gym space.
backward_kind (BackwardKind | str, default BackwardKind.POINT) – “point”, “interval”, “set” among possible options. Declared type of the backward_map function output. See BackwardKind for details.
abstract_to_enum (Callable[[NDArray], int], optional) – Maps a sample from abstract to space to enumerated index. Default None.
enum_to_abstract (Callable[[int], NDArray], optional) – Maps an enumerated index to a sample in the abstract space. Default None.
cache (bool, default False) – Memoise the original -> abstract direction: both original_to_abstract and original_to_enum, each in its own dict. See original_to_abstract for the contract this places on callers.

Notes

Not supported: a stochastic forward map (returning a distribution over abstract states), or a history-dependent abstraction (over the last k observations).

property is_enumerable: bool¶

Whether this map can produce a single int abstract index.

Returns:: True if an abstract_to_enum function was given and abstract_space is finite, i.e. abstract_n_elements is not inf. False otherwise (for example for a Box abstract space).
Return type:: bool

original_to_abstract(x: NDArray) → NDArray[source]¶

Original sample -> abstract sample. Memoised when cache=True.

The single entry point to self.forward_map: every forward mapping goes through here, so the cache is defined in exactly one place.

Parameters:: x (NDArray) – A sample of original_space.
Returns:: A sample of abstract_space.
Return type:: NDArray

Notes

The key of the cache is the raw to_byte x, which ignores shape and dtype.

Examples

>>> space = Box(low=np.array([-1.0, 0.0]), high=np.array([1.0, 1.0]))
>>> amap = linspace_map(space, [4, 2], cache=True)
>>> amap.original_to_abstract(np.array([0.5, 0.25], dtype=np.float32))
array([2, 0])

abstract_to_original(a: int | NDArray) → Point | Interval | StateSet[source]¶

Abstract sample -> the original sample(s) it stands for.

The mirror of original_to_abstract and the single entry point to self.backward_map. Not cached: only the forward direction is, since the backward direction is not on any hot path.

Parameters:: a (int | NDArray) – A sample of abstract_space.
Returns:: Shape determined by backward_kind; see BackwardKind.
Return type:: Point | Interval | StateSet
Raises:: ValueError – If the map was initialized without a backward_map.

Examples

>>> abstraction_map = linspace_map(
...     Box(low=np.array([-1.0, 0.0]), high=np.array([1.0, 1.0])), [4, 2]
... )
>>> abstraction_map.abstract_to_original(np.array([2, 0]))
array([0.33333337, 0.        ], dtype=float32)

original_to_enum(x: NDArray) → int[source]¶

Original sample -> enumeration (single flat abstract index).

This uses a composition of the functions self.original_to_abstract() and self.abstract_to_enum(), and is memoised when cache=True.

The cache here is separate from the one in original_to_abstract. :param x: A sample of original_space. :type x: NDArray

Returns:: A flat index in [0, abstract_n_elements).
Return type:: int
Raises:: ValueError – If the map was initialized without an abstract_to_enum function.

Notes

Keyed exactly like original_to_abstract (see its Notes). Unlike there, the cached value is an immutable int.

Examples

>>> space = Box(low=np.array([-1.0, 0.0]), high=np.array([1.0, 1.0]))
>>> abstraction_map = linspace_map(space, [4, 2], cache=True)
>>> abstraction_map.original_to_enum(np.array([0.5, 0.25], dtype=np.float32))
4

enum_to_original(e: int) → Point | Interval | StateSet[source]¶

Enumeration index (single flat abstract index) -> original space (according to self.backward_kind).

Parameters:: e (int) – A flat index in [0, abstract_n_elements).
Returns:: Shape determined by backward_kind; see BackwardKind.
Return type:: Point | Interval | StateSet
Raises:: ValueError – If no backward map is available, or if the map was built without an enum_to_abstract function.

enum_to_abstract(e: int) → NDArray[source]¶

Enumeration index (single flat abstract index) -> abstract sample. Wraps around self._enum_to_abstract and performs type casting when necessary.

For a Discrete / MultiDiscrete abstract_space the result is cast to the shape and dtype that abstract_space.sample() returns, e.g. an np.int64 scalar for a default Discrete.

Parameters:: e (int) – A flat index in [0, abstract_n_elements).
Returns:: A sample of abstract_space.
Return type:: NDArray
Raises:: ValueError – If the map was built without an enum_to_abstract function.

classmethod initialize_identity_map(space: Space, cache: bool = False) → AbstractionMap[source]¶

Creates an identity map. Any input will be returned unchanged.

Parameters:

space (gym.Space) – The space according to which samples will be input and output.
cache (bool, default False) – Memoise the forward direction; see AbstractionMap.__init__.

Return type:

AbstractionMap

Examples

>>> env = gym.make("Taxi-v3")
>>> state_map = AbstractionMap.initialize_identity_map(env.observation_space)
>>> state_map.forward_map(3)
3

class verigym.abstraction.abstractionmapper.BackwardKind(*values)[source]¶

Defining the types of objects a backward function can return.

The shape may differ fundamentally by abstraction and cannot be inferred at runtime: a point, an interval and a two-element set can all be (2, 2) float arrays.

Overview:

=============== ================================================ ==========================
kind            payload                                          example (2-D Box)
=============== ================================================ ==========================
`"point"`       one sample of `original_space`                   `array([0.5, 2.5])`
`"interval"`    `ndarray` shape `(2, *space.shape)`;              `array([[0.5, 2.5],
                `[0]` = lower, `[1]` = upper                       [1.0, 3.0]])`
`"set"`         iterable of samples of `original_space`           `[array([0, 1]),
                                                                    array([0, 2])]`
`"unknown"`     -- no backward map, or undeclared semantics       consumers raise
                                                                   rather than guess
=============== ================================================ ==========================

Using a StrEnum rather than a string so BackwardKind.INTERVAL == "interval" stays True, while a typo raises an error at import time instead of leading to downstream error at runtime.

The corresponding data types corresponding to BackwardKind.POINT, BackwardKind.INTERVAL and BackwardKind.SET are defined in discretization:

type Point    = NDArray                # shape (*space.shape,)
type Interval = NDArray                # shape (2, *space.shape); [0]=lower, [1]=upper
type StateSet = Sequence[NDArray]      # iterable of samples of original_space

Building maps¶

verigym.abstraction.abstractionmapper.linspace_mapper(env: Env, n_bins_states: int | NDArray, n_bins_actions: int | NDArray, *, cache: bool = False) → AbstractionMapper[source]¶

Conveniently create an AbstractionMapper for a gym.Env, providing mappings from state and action space to their respective abstract spaces. Both spaces are discretized via equidistant binning.

Note: see linspace_map for a mapping of a single space. The backward kind is point (see BackwardKind.POINT).

Parameters:

env (gym.Env) – The environment with original state and action spaces for which to create the abstract space and the mappings.
n_bins_states (int | array_like) – Bins per dimension for the state space.
n_bins_actions (int | array_like) – Bins per dimension for the action space.
cache (bool, keyword-only, default False)

Returns:

The map from the original environment spaces to the abstract spaces.

Return type:

AbstractionMapper

verigym.abstraction.abstractionmapper.linspace_map(space: Space, n_bins: int | NDArray, *, backward_kind: BackwardKind | str = BackwardKind.POINT, cache: bool = False) → AbstractionMap[source]¶

Conveniently create an AbstractionMap with equidistant bins per dimension.

The backward kind is point (see BackwardKind.POINT).

Parameters:

space (gym.spaces.Space) – The space to be discretized.
n_bins (int | array_like) – Bins per dimension. If int, each dimension has the same amount of bins.
cache (bool, keyword-only, default False) – Memoise the original -> abstract direction; see AbstractionMap.

Returns:

The map from the original space to the abstract space.

Return type:

AbstractionMap

verigym.abstraction.abstractionmapper.pow_map(space: Space, n_bins: int | NDArray, *, power: int = 2, cache: bool = False) → AbstractionMap[source]¶

Build an AbstractionMap with polynomially spaced bins.

Bins are denser near the centre of each dimension’s range; see centered_pow_bin. The backward kind is point (see BackwardKind.POINT).

Parameters:

space (gym.spaces.Space) – The space to discretize.
n_bins (int | array_like) – Bins per dimension.
power (int, keyword-only, default 2) – Forwarded to centered_pow_bin.
cache (bool, keyword-only, default False) – Memoise the original -> abstract direction; see AbstractionMap.

Return type:

AbstractionMap

verigym.abstraction.abstractionmapper.binned_mapper(env: Env, bin_func: BinEdgeGenFunc, n_bins_states: int | NDArray, n_bins_actions: int | NDArray, *, backward_kind: BackwardKind | str = BackwardKind.POINT, cache: bool = False, **bin_kwargs) → AbstractionMapper[source]¶

Build an AbstractionMapper by binning both spaces of env.

Parameters:

env (gym.Env) – The environment whose observation_space and action_space are binned.
bin_func (BinEdgeGenFunc) – (start, end, n) -> NDArray of ascending bin boundaries.
n_bins_states (int | array_like) – Bins per dimension for the state space.
n_bins_actions (int | array_like) – Bins per dimension for the action space.
backward_kind (BackwardKind | str, keyword-only, default BackwardKind.POINT) – Applied to both maps.
cache (bool, keyword-only, default False) – Memoise the hot original -> abstract path on both maps.
**bin_kwargs – Extra keyword arguments forwarded to bin_func.

Return type:

AbstractionMapper

verigym.abstraction.abstractionmapper.binned_map(space: Space, bin_func: BinEdgeGenFunc, n_bins: int | NDArray, *, backward_kind: BackwardKind | str = BackwardKind.POINT, cache: bool = False, **bin_kwargs) → AbstractionMap[source]¶

Build an AbstractionMap by binning space with bin_func.

Parameters:

space (gym.spaces.Space) – The space to discretize.
bin_func (BinEdgeGenFunc) – (start, end, n) -> NDArray of ascending bin boundaries, e.g. np.linspace or centered_pow_bin.
n_bins (int | array_like) – Bins per dimension; an array must match space.shape.
backward_kind (BackwardKind | str, keyword-only, default BackwardKind.POINT) – Passed through to bin_edges_map.
cache (bool, keyword-only, default False) – Passed through to bin_edges_map.
**bin_kwargs – Extra keyword arguments forwarded to bin_func (e.g. power=3 for centered_pow_bin).

Return type:

AbstractionMap

Notes

bin_kwargs is bound to bin_func with functools.partial, not a lambda – the resulting partial is only used during bin generation and never stored on the map, so picklability of the map is unaffected.

verigym.abstraction.abstractionmapper.bin_edges_map(space: Space, bin_edges: BinEdges, *, backward_kind: BackwardKind | str = BackwardKind.POINT, cache: bool = False) → AbstractionMap[source]¶

Build an AbstractionMap from an existing BinEdges.

Parameters:

space (gym.spaces.Space) – The original space. Validated against bin_edges.
bin_edges (BinEdges) – The discretization structure supplying the codecs.
backward_kind (BackwardKind | str, keyword-only, default BackwardKind.POINT)
cache (bool, keyword-only, default False) – Memoise the original -> abstract direction; see AbstractionMap.

Returns:

forward_map = bin_edges.orig_to_idx (factored), abstract_space = MultiDiscrete(bin_edges.n_bins).

Return type:

AbstractionMap

Notes

abstract_space is built from bin_edges.n_bins

verigym.abstraction.abstractionmapper.validate_for_abstraction(mapper: AbstractionMapper, *, multithreading: bool = False) → None[source]¶

Checking AbstractionMapper: fail fast, before simulation, naming which map is at fault.

Meant to run once up front, not per sample.

Parameters:

mapper (AbstractionMapper) – The mapper about to be handed to create_abstraction.
multithreading (bool, keyword-only, default False) – Whether the caller will run create_abstraction with a multiprocessing.Pool. Enables the pickling probe.

Raises:

ValueError – With a message naming the offending map ("state" / "action") and what is wrong with it.

Notes

Three checks: (1) both maps are enumerable and their abstract element counts are finite – catches a continuous abstract space before it dies far downstream; (2) a best-effort smoke test of ~10 samples through original_to_enum, skipped if the space cannot be sampled; (3) a pickling probe, only when multithreading=True.

A backward_map is deliberately not required – only labeling and policy deployment need one.

verigym.abstraction.abstractionmapper.enumeration_of_space(space: Discrete | MultiDiscrete) → tuple[Callable[[NDArray], int], Callable[[int], NDArray]][source]¶

Builds enumeration functions (C-order ravel/unravel) for a (Multi-)Discrete space; discrete space -> enumeration and back.

This function is used for creating identity maps. When the constructor notices that the space is discrete, it will automatically create the abstract_to_enum and enum_to_abstract functions.

Parameters:: space (gym.spaces.MultiDiscrete) – A finite space, as accepted by nvec_of_space.
Returns:: (abstract_to_enum, enum_to_abstract), ready to pass to AbstractionMap. Both are picklable, as required for multithreading=True.
Return type:: tuple[Callable, Callable]

Examples

>>> to_enum, from_enum = enumeration_of_space(gym.spaces.MultiDiscrete([3, 4]))
>>> to_enum(np.array([2, 1]))
9

verigym.abstraction.abstractionmapper.nvec_of_space(space: Space) → NDArray[source]¶

Return the per-dimension cardinality vector of a finite, rectangular space.

Parameters:

space (gym.spaces.Space) – A finite space. Discrete and MultiDiscrete are supported.

Returns:

A flat, 1-D integer array of per-dimension sizes:

Discrete(n)          -> array([n])
MultiDiscrete(nvec)  -> np.asarray(nvec).ravel()

Its product is the number of abstract elements, and it is the array that np.ravel_multi_index / np.unravel_index are taken over. Always 1-D, including for Discrete – unlike BinEdges.nvec, which is 0-d for a Discrete original space. Use BinEdges.n_bins there instead.

Return type:

npt.NDArray

Raises:

ValueError – If space has no finite rectangular cardinality (e.g. Box).

Example

TODO

Discretization¶

class verigym.abstraction.discretization.BinEdges(space: Box, edges: NDArray, ranges: NDArray)[source]¶

A per-dimension binning of space, plus the conversions between representations.

The four representations of a sample:

O (orig) an arbitrary sample of the original space
V (value) a sample snapped onto bin edges; a finite subset of O
I (idx) per-dimension bin indices; a sample of MultiDiscrete(nvec)
E (enum) a single flat index; a sample of Discrete(prod(nvec))

Because V lives inside the original space, value_to_orig is a dtype/shape cast rather than a real conversion, and value_to_idx is the same operation as orig_to_idx. Six fundamental conversions: orig_to_idx, orig_to_value, idx_to_value, idx_to_enum, enum_to_idx, value_to_orig. The remaining conversions are compositions of these.

Variables:

space (Box) – The space this binning was built for. Populated for Discrete and MultiDiscrete inputs too, since value_to_orig needs a space.
edges (npt.NDArray) – Flat concatenation of the bin edges of every dimension.
ranges (npt.NDArray) – (start, end) index pairs into edges, one per flattened dimension.

Notes

The conversions are methods so that forward/backward maps handed to an AbstractionMap are bound methods (=picklable, as lambda funcs are not).

property lengths: NDArray¶

Per-dimension number of bin edges as a flat 1-D array.

n edges delimit n - 1 bins; use n_bins for bin counts.

property n_bins: NDArray¶: Per-dimension bin counts as a flat 1-D array (lengths - 1).

property nvec: NDArray¶

Per-dimension bin counts, reshaped to space.shape.

For a Discrete space this is 0-d (array(3), shape ()), because it reshapes to space.shape == (). Use n_bins instead when a flat array is needed, e.g. to build an abstract space.

orig_to_idx(x: NDArray) → NDArray[source]¶

Map an original sample to per-dimension bin indices (O -> I).

Parameters:: x (npt.NDArray) – A sample of space.
Returns:: Bin indices, shape space.shape, integer dtype. A valid sample of MultiDiscrete(self.n_bins).
Return type:: npt.NDArray

orig_to_value(x: NDArray) → NDArray[source]¶

Discretize an original sample onto its bin edges (O -> V).

Parameters:: x (npt.NDArray) – A sample of space.
Returns:: The snapped sample, shape space.shape, float dtype. Still a member of the original space.
Return type:: npt.NDArray

orig_to_enum(x: NDArray) → int[source]¶

Map an original sample to a single flat abstract index (O -> E).

Composition of idx_to_enum and orig_to_idx.

Parameters:: x (npt.NDArray) – A sample of space.
Returns:: A flat index in [0, prod(self.n_bins)).
Return type:: int

value_to_idx(x: NDArray) → NDArray[source]¶

Map an already discretized sample to per-dimension bin indices (V -> I).

Essentially the same operation as orig_to_idx: We are using a sample from the original space’s dtype, so we can use the same orig_to_idx function.

Note: Exists for clarity: so call sites can name the representation they hold. If you, as a user find it unnecessary, please provide the feedback.

Parameters:: x (npt.NDArray) – A sample of space already sitting on bin edges.
Returns:: Bin indices, shape space.shape.
Return type:: npt.NDArray

value_to_enum(x: NDArray) → int[source]¶

Map a discretized sample to a single flat abstract index (V -> E).

Parameters:: x (npt.NDArray) – A sample of space already sitting on bin edges.
Returns:: A flat index in [0, prod(self.n_bins)).
Return type:: int

idx_to_enum(x: NDArray) → int[source]¶

Flatten per-dimension bin indices into a single enumerated index (I -> E).

Parameters:: x (npt.NDArray) – Bin indices, shape space.shape.
Returns:: np.ravel_multi_index of the raveled indices over self.n_bins.
Return type:: int

enum_to_idx(x: int) → NDArray[source]¶

Expand an enumerated index back into per-dimension bin indices (factored) (E -> I).

Parameters:: x (int) – A flat index in [0, prod(self.n_bins)).
Returns:: Bin indices reshaped to space.shape. Exact inverse of idx_to_enum.
Return type:: npt.NDArray

enum_to_value(x: int) → NDArray[source]¶

Map a enumeration index to its representative discretized (factored) sample (E -> V).

Parameters:: x (int) – A flat index in [0, prod(self.n_bins)).
Returns:: The representative bin-edge value, shape space.shape, float dtype.
Return type:: npt.NDArray

enum_to_orig(x: int) → Point[source]¶

Map an enumerated index to a valid sample of space (E -> O).

Parameters:: x (int) – A flat index in [0, prod(self.n_bins)).
Returns:: A representative sample satisfying self.space.contains(...).
Return type:: Point

idx_to_value(x: NDArray) → NDArray[source]¶

Map per-dimension bin indices to their bin-edge values (I -> V).

Parameters:: x (npt.NDArray) – Bin indices, shape space.shape.
Returns:: The lower edge of each indexed bin, shape space.shape, float dtype.
Return type:: npt.NDArray

idx_to_orig(x: NDArray) → Point[source]¶

Map per-dimension bin indices to a valid sample of space (I -> O).

Parameters:: x (npt.NDArray) – Bin indices, shape space.shape.
Returns:: A representative sample satisfying self.space.contains(...).
Return type:: Point

value_to_orig(x: NDArray) → Point[source]¶

Cast a discretized value (factored) to the dtype and shape of space (V -> O).

Parameters:: x (npt.NDArray) – A snapped bin-edge value.
Returns:: The same value as a valid sample of space.
Return type:: Point

idx_to_interval(x: NDArray) → Interval[source]¶

Map bin indices to the interval they could come from in the original space (I -> Interval).

Parameters:: x (npt.NDArray) – Bin indices, shape space.shape.
Returns:: Array of shape (2, *space.shape); [0] holds the lower bound per dimension, [1] the upper. This is the canonical BackwardKind.INTERVAL payload.
Return type:: Interval

enum_to_interval(x: int) → Interval[source]¶

Map abstract state (enum representation) to the interval they could come from in the original space (E -> Interval).

Parameters:: x (int) – The enumerated abstract state value, an integer number.
Returns:: Array of shape (2, *space.shape); [0] holds the lower bound per dimension, [1] the upper. This is the canonical BackwardKind.INTERVAL payload.
Return type:: Interval

value_to_interval(x: NDArray) → Interval[source]¶

Map the value representation of an abstract state to the interval they could come from in the original space (V -> Interval).

Parameters:: x (npt.NDArray) – Value representation of abstract state, shape space.shape.
Returns:: Array of shape (2, *space.shape); [0] holds the lower bound per dimension, [1] the upper. This is the canonical BackwardKind.INTERVAL payload.
Return type:: Interval

verigym.abstraction.discretization.generate_box_bins(space: Box, bin_func: BinEdgeGenFunc, n_bins: int | NDArray[integer[Any]]) → BinEdges[source]¶

Build a BinEdges for space, using bin_func per dimension. Use this function with custom bin_func parameter for custom binning.

Parameters:

space (Box) – The space to create the BinEdges for. Discrete and MultiDiscrete are also accepted and are treated as integer-valued ranges.
bin_func (BinEdgeGenFunc) – A function (start, end, n) -> NDArray returning n bin boundaries sorted ascending, e.g. np.linspace or centered_pow_bin. It is called with n_bins + 1 edges, since that many edges delimit n_bins bins.
n_bins (int | array_like) – Bins per dimension. If an array, it must have the same shape as space.

Returns:

One BinEdge per flattened dimension of space, with space retained on the result. A scalar Discrete space is treated as a single-dimension space, so the result is always nested, consistent with vector Box spaces.

Return type:

BinEdges

Raises:

TypeError – If space is not a Box, Discrete or MultiDiscrete.

Notes

The last bin per dimension is closed, [e_{n-1}, high]: high itself (and any value above it) is clamped into it, see _orig_to_idx_njit.

verigym.abstraction.discretization.centered_pow_bin(start: float | int, end: float | int, n_samples: int, power: int = 2) → BinEdge[source]¶

Generate bin boundaries following a one-coefficient polynomial spacing.

An input x is transformed as x**power. Samples are taken from the interval [-1, 1], raised to power (sign-preserved for even powers), normalised, and then affinely mapped onto [start, end]. The result is denser near the centre of the interval than np.linspace.

Parameters:

start (float | int) – The lowest value of the bin array.
end (float | int) – The highest value of the bin array.
n_samples (int) – How many boundaries to include in the final array.
power (int, default 2) – The power to raise each element by.

Returns:

A bin boundary array of n_samples values, sorted ascending.

Return type:

BinEdge

verigym.abstraction.discretization.nvec_from_samples(a: NDArray)[source]¶

Extract the nvec parameter for a gymnasium.spaces.MultiDiscrete space from a samples array.

The function extracts all the unique observations for each dimension and creates an nvec from them.

Parameters:: a (npt.NDArray) – A numpy array containing observations from an environment or an MDP
Returns:: A vector that can be used to initialize
Return type:: npt.NDArray

Note

The nvec only describes the amount of unique values in each dimension. It does not describe the bounds for these dimensions. Use lookup_table_from_mdiscrete_samples with the same input to retrieve a lookup table mapping the index in the gym.spaces.MultiDiscrete space to the actual values.

Gymnasium wrappers and spaces¶

class verigym.abstraction.gym_utils.transform_observation.ReplaceInfObservation(env: Env[ObsType, ActType], neg_inf: int | float | NDArray[Any], pos_inf: int | float | NDArray[Any])[source]¶

Replace the infinite boundaries of a Box observation_space

Parameters:

env (gym.Env) – A gymnasium environment with a Box observation space
neg_inf (int | float | npt.NDArray) – The value to replace all negative infinity boundaries with If neg_inf is an array it must have the same shape as the space
pos_inf (int | float | npt.NDArray) – The value to replace all positive infinity boundaries with If pos_inf is an array it must have the same shape as the space

Raises:

AssertionError – Whenever the observation space is not of type Box or whenever the shape of neg_inf or pos_inf is invalid

Constructor for the transform observation wrapper.

Args:: env: The environment to wrap func: A function that will transform an observation. If this transformed observation is outside the observation space of env.observation_space then provide an observation_space. observation_space: The observation spaces of the wrapper, if None, then it is assumed the same as env.observation_space.

class verigym.abstraction.gym_utils.transform_observation.DiscretizeBoxObservation(env: ~gymnasium.core.Env[~gymnasium.core.ObsType, ~gymnasium.core.ActType], n_samples: int | ~numpy._typing._array_like.NDArray[~numpy.integer[~typing.Any]] | None = None, bin_edges: ~verigym.abstraction.discretization.BinEdges | ~verigym.abstraction.types.BinEdgeGenFunc = <function linspace>, use_box_space: bool = True, **kwargs)[source]¶

Discretization Wrapper for Box observation spaces

Parameters:

env (gym.Env) – The environment containing a continuous observation space
n_samples (optional, int | npt.NDarray[np.integer], default=None) – The number of bins to use for each dimension. If n_samples is an array it must have the same shape as the observation space. If n_samples is not provided, then a valid Bins array must be provided
bin_edges (BinEdges) – A valid BinEdges array describing how to discretize each dimension
use_box_space (bool,default=True) – Whether to keep using the Box space or construct a discrete space (setting this to False will change the observation space)
**kwargs – Additional keyword arguments that ar e forwarded to generate_box_bins

Raises:

AssertionError – Raises an AssertionError if the observation space is not a continuous Box space or if one of the boundaries is infinite

Constructor for the transform observation wrapper.

Args:: env: The environment to wrap func: A function that will transform an observation. If this transformed observation is outside the observation space of env.observation_space then provide an observation_space. observation_space: The observation spaces of the wrapper, if None, then it is assumed the same as env.observation_space.

class verigym.abstraction.gym_utils.transform_action.DiscretizeBoxAction(env: ~gymnasium.core.Env[~gymnasium.core.ObsType, ~gymnasium.core.ActType], n_samples: int | ~numpy._typing._array_like.NDArray[~numpy.integer[~typing.Any]] | None = None, bin_edges: ~verigym.abstraction.discretization.BinEdges | ~verigym.abstraction.types.BinEdgeGenFunc = <function linspace>, use_box_space: bool = True, **kwargs)[source]¶

Discretization Wrapper for Box action spaces

Parameters:

env (gym.Env) – The environment containing a continuous action space
n_samples (optional, int | npt.NDarray[np.integer], default=None) – The number of bins to use for each dimension. If n_samples is an array it must have the same shape as the action space. If n_samples is not provided, then a valid Bins array must be provided
bin_edges (BinEdges) – A valid BinEdges array describing how to discretize each dimension
use_box_space (bool,default=True) – Whether to keep using the Box space or construct a discrete space (setting this to False will change the action space)
**kwargs – Additional keyword arguments that are forwarded to generate_box_bins

Raises:

AssertionError – Raises an AssertionError if the action space is not a continuous Box space or if one of the boundaries is infinite

Initialize TransformAction.

Args:: env: The environment to wrap func: Function to apply to the step()’s action action_space: The updated action space of the wrapper given the function.

verigym.abstraction.gym_utils.spaces.is_bounded_space(space: Space) → bool[source]¶

Return True if the space has finite (non-infinite) bounds, False otherwise.

Parameters:: space – The gymnasium space to check.

verigym.abstraction.gym_utils.spaces.get_n_elements_of_space(space: Space) → int | float[source]¶

Returns the number of elements of a given gym.Space.

Parameters:: space (gymnasium.spaces.Space) – The gym space.
Returns:: Returns int if finite elements and float('inf') if infinite.
Return type:: int | float