Template directions

AbstractDirections{N, VN}

Abstract type for representations of direction vectors.

Notes

This type is parameterized by N and VN, where:

• N stands for the numeric type
• VN stands for the vector type with coefficients of type N

Each implementing subtype is an iterator over a set of directions. For that they implement the standard iterator methods from Base, namely Base.length (returns the number of directions) and Base.iterate. Moreover, the following methods should be implemented:

• dim – return the ambient dimension of the vectors
• eltype – return the type of each vector

Optionally, subtypes may implement:

• isbounding – (defaults to false) return true if an overapproximation with the direction vectors results in a bounded set, given a bounded input set, and false otherwise
• isnormalized – (defaults to false) is true if each direction vector has norm one w.r.t. the usual vector 2-norm

isbounding(ad::AbstractDirections)
isbounding(ad::Type{<:AbstractDirections})

Check whether an overapproximation with a set of direction vectors results in a bounded set, given a bounded input set.

Input

• ad – direction vectors or a subtype of AbstractDirections

Output

Given a bounded set $X$, we can construct an outer polyhedral approximation of $X$ by using the direction vectors ad as normal vectors of the facets. If this function returns true, then the result is again guaranteed to be a bounded set (i.e., a polytope). Note that the result does not depend on the specific shape of $X$, as long as $X$ is bounded.

Notes

By default, this function returns false in order to be conservative. Custom subtypes of AbstractDirections should hence add a method for this function.

The function can be applied to an instance of an AbstractDirections subtype or to the subtype itself. By default, the check on the instance falls back to the check on the subtype.

isnormalized(ad::AbstractDirections)
isnormalized(ad::Type{<:AbstractDirections})

Check whether the given direction vectors are normalized with respect to the 2-norm.

Input

• ad – direction vectors or a subtype of AbstractDirections

Output

true if the 2-norm of each element in ad is one and false otherwise.

Notes

By default, this function returns false in order to be conservative. Custom subtypes of AbstractDirections should hence add a method for this function.

The function can be applied to an instance of an AbstractDirections subtype or to the subtype itself. By default, the check on the instance falls back to the check on the subtype.

project(S::LazySet,
        block::AbstractVector{Int},
        directions::Type{<:AbstractDirections},
        [n]::Int;
        [kwargs...]
       )

Project a high-dimensional set to a given block using direction vectors.

Input

• S – set
• block – block structure - a vector with the dimensions of interest
• directions – direction vectors
• n – (optional, default: dim(S)) ambient dimension of the set S

Output

The polyhedral overapproximation of the projection of S in the given directions.

BoxDirections{N, VN} <: AbstractDirections{N, VN}

Box directions representation.

Fields

• n – dimension

Notes

Box directions can be seen as the vectors where only one entry is ±1, and all other entries are 0. In dimension $n$, there are $2n$ such directions.

The default vector representation used in this template is a ReachabilityBase.Arrays.SingleEntryVector, although other implementations can be used such as a regular Vector and a SparseVector.

Examples

The template can be constructed by passing the dimension. For example, in dimension two:

julia> dirs = BoxDirections(2)
BoxDirections{Float64, ReachabilityBase.Arrays.SingleEntryVector{Float64}}(2)

julia> length(dirs)
4

By default, each direction is represented as a SingleEntryVector, i.e., a vector with only one non-zero element,

julia> eltype(dirs)
ReachabilityBase.Arrays.SingleEntryVector{Float64}

In two dimensions, the directions defined by BoxDirections are normal to the facets of a box.

julia> collect(dirs)
4-element Vector{ReachabilityBase.Arrays.SingleEntryVector{Float64}}:
 [1.0, 0.0]
 [0.0, 1.0]
 [0.0, -1.0]
 [-1.0, 0.0]

The numeric type can be specified as well:

julia> dirs = BoxDirections{Rational{Int}}(10)
BoxDirections{Rational{Int64}, ReachabilityBase.Arrays.SingleEntryVector{Rational{Int64}}}(10)

julia> length(dirs)
20

DiagDirections{N, VN} <: AbstractDirections{N, VN}

Diagonal directions representation.

Fields

• n – dimension

Notes

Diagonal directions are vectors where all entries are ±1. In dimension $n$, there are in total $2^n$ such directions.

Examples

The template can be constructed by passing the dimension. For example, in dimension two:

julia> dirs = DiagDirections(2)
DiagDirections{Float64, Vector{Float64}}(2)

julia> length(dirs) # number of directions
4

By default, each direction is represented as a regular Vector:

julia> eltype(dirs)
Vector{Float64} (alias for Array{Float64, 1})

In two dimensions, the directions defined by DiagDirections are normal to the facets of a ball in the 1-norm.

julia> collect(dirs)
4-element Vector{Vector{Float64}}:
 [1.0, 1.0]
 [-1.0, 1.0]
 [1.0, -1.0]
 [-1.0, -1.0]

The numeric type can be specified as well:

julia> dirs = DiagDirections{Rational{Int}}(10)
DiagDirections{Rational{Int64}, Vector{Rational{Int64}}}(10)

julia> length(dirs)
1024

OctDirections{N, VN} <: AbstractDirections{N, VN}

Octagon directions representation.

Fields

• n – dimension

Notes

Octagon directions consist of all vectors that are zero almost everywhere except in two dimensions $i$, $j$ (possibly $i = j$) where it is $±1$. In dimension $n$, there are $2n^2$ such directions.

Examples

The template can be constructed by passing the dimension. For example, in dimension two:

julia> dirs = OctDirections(2)
OctDirections{Float64, SparseArrays.SparseVector{Float64, Int64}}(2)

julia> length(dirs) # number of directions
8

By default, the directions are represented as sparse vectors:

julia> eltype(dirs)
SparseArrays.SparseVector{Float64, Int64}

In two dimensions, the directions are normal to the facets of an octagon.

julia> first(dirs)
2-element SparseArrays.SparseVector{Float64, Int64} with 2 stored entries:
  [1]  =  1.0
  [2]  =  1.0

julia> Vector.(collect(dirs))
8-element Vector{Vector{Float64}}:
 [1.0, 1.0]
 [1.0, -1.0]
 [-1.0, 1.0]
 [-1.0, -1.0]
 [1.0, 0.0]
 [0.0, 1.0]
 [0.0, -1.0]
 [-1.0, 0.0]

The numeric type can be specified as well:

julia> dirs = OctDirections{Rational{Int}}(10)
OctDirections{Rational{Int64}, SparseArrays.SparseVector{Rational{Int64}, Int64}}(10)

julia> length(dirs)
200

BoxDiagDirections{N, VN} <: AbstractDirections{N, VN}

Box-diagonal directions representation.

Fields

• n – dimension

Notes

Box-diagonal directions can be seen as the union of diagonal directions (all entries are ±1) and box directions (one entry is ±1, all other entries are 0). The iterator first enumerates all diagonal directions, and then all box directions. In dimension $n$, there are in total $2^n + 2n$ such directions.

Examples

The template can be constructed by passing the dimension. For example, in dimension two:

julia> dirs = BoxDiagDirections(2)
BoxDiagDirections{Float64, Vector{Float64}}(2)

julia> length(dirs) # number of directions
8

By default, each direction is represented as a regular vector:

julia> eltype(dirs)
Vector{Float64} (alias for Array{Float64, 1})

In two dimensions, the directions are normal to the facets of an octagon, i.e., the template coincides with OctDirections.

julia> collect(dirs)
8-element Vector{Vector{Float64}}:
 [1.0, 1.0]
 [-1.0, 1.0]
 [1.0, -1.0]
 [-1.0, -1.0]
 [1.0, 0.0]
 [0.0, 1.0]
 [0.0, -1.0]
 [-1.0, 0.0]

The numeric type can be specified as well:

julia> dirs = BoxDiagDirections{Rational{Int}}(10)
BoxDiagDirections{Rational{Int64}, Vector{Rational{Int64}}}(10)

julia> length(dirs)
1044

PolarDirections{N<:AbstractFloat, VN<:AbstractVector{N}} <: AbstractDirections{N, VN}

Polar directions representation.

Fields

• Nφ – length of the partition of the polar angle
• stack – list of computed directions

Notes

The PolarDirections constructor computes a sample of the unit sphere in $ℝ^2$, which is parameterized by the polar angle $φ ∈ Dφ := [0, 2π]$; see the Wikipedia entry on the polar coordinate system for details. The resulting directions are stored in stack.

The integer argument $Nφ$ defines how many samples of $Dφ$ are taken. The Cartesian components of each direction are obtained with

\[[cos(φᵢ), sin(φᵢ)].\]

Examples

The integer passed as an argument is used to discretize $φ$:

julia> pd = PolarDirections(2);

julia> pd.stack
2-element Vector{Vector{Float64}}:
 [1.0, 0.0]
 [-1.0, 1.2246467991473532e-16]

julia> length(pd)
2

SphericalDirections{N<:AbstractFloat, VN<:AbstractVector{N}} <: AbstractDirections{N, VN}

Spherical directions representation.

Fields

• Nθ – length of the partition of the azimuthal angle
• Nφ – length of the partition of the polar angle
• stack – list of computed directions

Notes

The SphericalDirections constructor provides a sample of the unit sphere in $ℝ^3$, which is parameterized by the azimuthal and polar angles $θ ∈ Dθ := [0, π]$ and $φ ∈ Dφ := [0, 2π]$ respectively; see the Wikipedia entry on the spherical coordinate system for details.

The integer arguments $Nθ$ and $Nφ$ define how many samples along the domains $Dθ$ and $Dφ$ are respectively taken. The Cartesian components of each direction are obtained with

\[[sin(θᵢ)*cos(φᵢ), sin(θᵢ)*sin(φᵢ), cos(θᵢ)].\]

The north and south poles are treated separately so that those points are not considered more than once.

Examples

The template can be built in different ways. If you pass only one integer, the same value is used to discretize both $θ$ and $φ$:

julia> sd = SphericalDirections(3);

julia> sd.Nθ, sd.Nφ
(3, 3)

julia> length(sd)
4

Pass two integers to control the discretization in $θ$ and in $φ$ separately:

julia> sd = SphericalDirections(4, 5);

julia> length(sd)
10

julia> sd = SphericalDirections(4, 8);

julia> length(sd)
16

CustomDirections{N, VN<:AbstractVector{N}} <: AbstractDirections{N, VN}

User-defined direction vectors.

Fields

• directions – list of direction vectors
• n – (optional; default: computed from directions) dimension
• check_boundedness – (optional; default: true) flag to check boundedness
• check_normalization – (optional; default: true) flag to check whether all directions are normalized

Notes

This struct is a wrapper for a list of user-defined directions. There are fields for the list of directions, their dimension, and (boolean) cache fields for the boundedness and normalization properties. The latter are checked by default upon construction.

To check boundedness, we construct the polyhedron with constraints $d·x <= 1$ for each direction $d$ and check if this set is bounded. (Note that the bound $1$ is arbitrary and that this set may be empty, which however implies boundedness.)

The dimension will also be determined automatically, unless the empty vector is passed (in which case the optional argument n needs to be specified).

Examples

Create a template with box directions in dimension two:

julia> dirs = CustomDirections([[1.0, 0.0], [-1.0, 0.0], [0.0, 1.0], [0.0, -1.0]]);

julia> dirs.directions
4-element Vector{Vector{Float64}}:
 [1.0, 0.0]
 [-1.0, 0.0]
 [0.0, 1.0]
 [0.0, -1.0]

julia> LazySets.Approximations.isbounding(dirs)
true

julia> LazySets.Approximations.isnormalized(dirs)
true