Mapping

AbstractMapping{N, T}

The concrete ↔ abstract discretization: a bijection between a universe of integer state labels 1:get_n_state(m) and points/cells of an N-dimensional concrete space (element type T).

Extending

Implement get_n_state, get_state_by_coord, get_states_by_coord, get_coord_by_state, get_elem_by_state, get_elem_by_coord, has_overlapping_cells. enum_states, enum_coords, enum_elems, is_valid_state, get_dim have generic defaults.

AbstractMultiLevelMapping{N, T} <: AbstractMapping{N, T}

A mapping whose labels are distributed across several resolution levels. Unlike a GridMapping, a position is a (level, pos) pair and the pos-based methods take an explicit level argument — so a multi-level mapping is deliberately not a GridMapping{N,T} (it does not satisfy the single-grid get_pos_by_state(m, q)::NTuple{N,Int} contract).

AbstractStateSet{N}

A set of abstract states (integer labels) over an N-dimensional concrete space. The labels only have meaning relative to an AbstractMapping, which is why the membership/enumeration methods take the mapping m as an argument. For a self-contained object that bundles the set with its mapping, use MappedStateSet (the public surface); the (S, m, …) methods below are the implementation it forwards to.

Extending

Implement contains_state, enum_states, add_state!, remove_state!, empty_states!. get_n_state, add_states!, add_set!, remove_set! have generic defaults.

CellUnion(grid, positions)

The union of whole cells of grid at the given positions (an iterable of integer tuples), as a LazySets.LazySet.

Its grid discretization is exact by dispatch: under every inclusion mode, get_pos_from_set returns exactly the member positions — shared faces are owned by the member cell, so a cell-aligned hole removes exactly its cells (no face-adjacent over-removal) and a cell-aligned target is recovered exactly under INNER. Coordinate membership (x ∈ S) quantizes x to its cell; position membership (pos ∈ S) tests the tuple directly.

Use cells_where to build one from a predicate and image_blocked_cells for constraints on a nonlinear image of the state.

ExplicitGridMapping: explicit enumeration of positions -> ids (dict) and ids -> positions (vector)

ExplicitIdSet{N} <: AbstractStateSet{N}

A state set stored as an explicit BitSet of integer labels.

FullStateSet{N} <: AbstractStateSet{N}

The read-only "all states" set: it contains every valid label of whatever AbstractMapping it is queried against (1:get_n_state(m)). Used as the default state set of a symbolic model ("consider every cell of the grid").

abstract type Grid{N, T} end

Defines an abstract type for grid-based structures in N dimensions with floating-point values T.

GridEllipsoidalRectangular{N,T} <: Grid{N,T}

Uniform grid on rectangular space rect, centered at orig and with steps set by the vector h. Cells are (possibly overlapping) ellipsoids defined at each grid point c as (x-c)'P(x-c) ≤ 1.

P (the quadratic form, hot membership loop) and its inverse Q (the LazySets shape matrix, cell construction) are both stored so neither path re-inverts.

GridFree{N,T} <: Grid{N,T}

Uniform grid on unbounded space, centered at orig and with steps set by the vector h.

GridMapping{N,T} <: AbstractMapping{N,T}:

• adds grid, and pos <-> state conversions

HierarchicalGridMapping{N, T, ML} <: AbstractMultiLevelMapping{N, T}

Multiscale grid mapping with several levels of resolution; each level is itself a GridMapping (e.g. an ImplicitGridMapping). Global labels are assigned by concatenating the levels (offsets[l] is the number of labels before level l).

ImplicitGridMapping:

• universe is a rectangular index box (minpos..maxpos) possibly periodic
• id computed by row-major linearization (no dict)
• pos recovered by inverse mapping

ImplicitStateSet{N} <: AbstractStateSet{N}

A geometry-backed state set: membership is decided lazily from a stored LazySet and an inclusion mode, rather than from an explicit list of labels.

The set field is deliberately abstractly typed (LazySets.LazySet): the set is mutated in place through add_set!/remove_set!, and each operation may return a different concrete LazySet subtype (EmptySet → UnionSetArray → Intersection, …), so the field cannot be a fixed concrete parameter.

ListMapping{N,T} <: AbstractMapping{N,T}

Finite list of concrete points (SVector{N,T}) with id=1..K.

MappedStateSet{N, S, M}

A state set bundled with the mapping that gives its integer labels meaning. Consumers hold one self-contained object instead of threading the (set, mapping) pair through every call — which also removes the "wrong mapping" bug class. This is the public surface for state sets; the (set, mapping, …) methods on AbstractStateSet are what it forwards to.

PeriodicGridMapping{N, T, M, P} <: GridMapping{N, T}

A periodic wrapper over an underlying GridMapping.

Fields (mirrors PeriodicDomainList):

• periodic_dims::SVector{P, Int}
• periods::SVector{P, T}
• start::SVector{P, T}
• underlying_mapping::M
• periodic_index_map::NTuple{N, Union{Nothing, Int}}

SetMinusStateSet{N, S1, S2} <: AbstractStateSet{N}

Lazy difference A ∖ B of two state sets.

UnionStateSet{N, S1, S2} <: AbstractStateSet{N}

Lazy union A ∪ B of two state sets.

cells_on_segment(grid, a, b)

Positions of every grid cell whose closure the straight segment from a to b passes through, in traversal order. Boundary crossings are enumerated exactly (one interval per pair of consecutive crossing times, quantized at the interval midpoint), so each segment point lies in the closure of a returned cell.

This is the sound validation for multi-cell steps of integrator-type dynamics: their inter-sample trajectory is exactly this segment, so a transition whose swept cells are all admissible cannot cross an excluded region between samples — lifting the one-cell-per-step restriction of intersample_safe_time_step.

cells_where(pred, grid, region, incl_mode = INNER)

The CellUnion of the cells of region (discretized with incl_mode) whose position satisfies pred(pos). Supports do-block syntax; convert a position to its center with get_coord_by_pos(grid, pos):

blocked = MP.cells_where(grid, X) do pos
    is_infeasible(MP.get_coord_by_pos(grid, pos))
end

get_pos_by_coord(grid::Grid{N, T}, x::SVector{N, T}) -> NTuple{N, Int}

Returns the discrete position (grid indices) corresponding to a coordinate x.

• The cell (0,0) is centered between -h/2 and +h/2.
• h is the length of a grid cell in each dimension.

image_blocked_cells(g, gradient_bound, grid, region, obstacles, incl_mode = INNER)

Sound pullback of constraints living on a nonlinear image of the state: the CellUnion of every cell of region in which some point might map into one of the obstacles (a LazySet or a vector of them) under g.

The test is center-based and certified by a Lipschitz bound: with |∂gⱼ/∂xᵢ| ≤ gradient_bound[i], the image of any point of a cell stays within dev = Σᵢ gradient_bound[i] · hᵢ/2 (per component) of the image of its center, so a cell whose center image clears every obstacle by dev is certified feasible — a kept cell never maps into an obstacle. Conservative (the deviation ball is over-approximated by a box).

intersample_safe_time_step(grid, velocity_bound)

Largest sampling time τ such that a system whose velocity satisfies |ẋᵢ| ≤ velocity_bound[i] moves by at most one cell of grid per axis per step: τ = minᵢ hᵢ / velocity_bound[i].

Together with OUTER obstacle carving, respecting this bound guarantees that the continuous trajectory between consecutive samples stays inside the union of the two (certified admissible) cells, closing the inter-sample soundness gap of grid abstractions over domains with holes. Axes with a zero velocity bound are unconstrained.

is_lattice_exact(state_grid, input_grid, tstep; rtol = 1e-9)

For integrator dynamics ẋ = u, check that every input-grid point u translates the state grid exactly onto itself in one step: tstep .* u must be a per-axis integer multiple of the state-grid step (checked on the input grid's step and origin, which spans all its points).

When this holds, the exact reach set of a cell is again a single cell, so the abstraction is deterministic and exact (a bisimulation) — in particular the CENTER_SIMULATION approximation mode, unsound in general, becomes exact for such systems.

swept_input_filter(grid, tstep, blocked)

(x, u) -> Bool predicate keeping a transition only when every cell crossed by the inter-sample segment from x to x + tstep · u avoids the blocked cells (a CellUnion or an iterable of grid positions).

For integrator dynamics ẋ = u the inter-sample trajectory is that segment, so wiring this as the abstraction's state_input_filter restores inter-sample soundness for multi-cell steps, lifting the one-cell-per-step speed cap of intersample_safe_time_step; set the solver's intersample_checked attribute alongside, so the multi-cell jump warning knows the sweep is covered.