From cb1bb43dcc3b298b84d224d133b91f45a0150155 Mon Sep 17 00:00:00 2001 From: schillic Date: Tue, 15 May 2018 22:39:10 +0200 Subject: [PATCH 1/6] add AbstractDirections type --- src/Approximations/Approximations.jl | 1 + src/Approximations/template_directions.jl | 13 +++++++++++++ 2 files changed, 14 insertions(+) create mode 100644 src/Approximations/template_directions.jl diff --git a/src/Approximations/Approximations.jl b/src/Approximations/Approximations.jl index 7884389a2f..c04e30aa4e 100644 --- a/src/Approximations/Approximations.jl +++ b/src/Approximations/Approximations.jl @@ -29,6 +29,7 @@ const DIR_SOUTH(N) = [zero(N), -one(N)] include("iterative_refinement.jl") include("box_approximations.jl") +include("template_directions.jl") include("overapproximate.jl") include("decompositions.jl") diff --git a/src/Approximations/template_directions.jl b/src/Approximations/template_directions.jl new file mode 100644 index 0000000000..b6b2dddb09 --- /dev/null +++ b/src/Approximations/template_directions.jl @@ -0,0 +1,13 @@ +import LazySets.dim + +""" + AbstractDirections{N} + +Abstract type for template direction representations. + +### Notes + +All subtypes should implement the standard iterator methods from `Base` and the +function `dim(d<:AbstractDirections)::Int`. +""" +abstract type AbstractDirections{N} end From ab6595537665276e993fe4fdcdd9e5d73805af7e Mon Sep 17 00:00:00 2001 From: schillic Date: Tue, 15 May 2018 22:39:38 +0200 Subject: [PATCH 2/6] add BoxDirections type --- src/Approximations/Approximations.jl | 3 +- src/Approximations/template_directions.jl | 67 +++++++++++++++++++++++ 2 files changed, 69 insertions(+), 1 deletion(-) diff --git a/src/Approximations/Approximations.jl b/src/Approximations/Approximations.jl index c04e30aa4e..fce9e6d0ae 100644 --- a/src/Approximations/Approximations.jl +++ b/src/Approximations/Approximations.jl @@ -16,7 +16,8 @@ export approximate, norm, overapproximate, radius, - symmetric_interval_hull + symmetric_interval_hull, + BoxDirections const TOL(N::Type{Float64}) = eps(N) const TOL(N::Type{Float32}) = eps(N) diff --git a/src/Approximations/template_directions.jl b/src/Approximations/template_directions.jl index b6b2dddb09..1f370a10a9 100644 --- a/src/Approximations/template_directions.jl +++ b/src/Approximations/template_directions.jl @@ -11,3 +11,70 @@ All subtypes should implement the standard iterator methods from `Base` and the function `dim(d<:AbstractDirections)::Int`. """ abstract type AbstractDirections{N} end + +# box directions + +""" + UnitVector{T} <: AbstractVector{T} + +A lazy unit vector with arbitrary one-element. + +### Fields + +- `i` -- index of non-zero entry +- `n` -- vector length +- `v` -- non-zero entry +""" +struct UnitVector{T} <: AbstractVector{T} + i::Int + n::Int + v::T +end + +function Base.getindex(e::UnitVector{T}, i::Int) where T + @boundscheck @assert 1 <= i <= e.n + return i == e.i ? e.v : zero(T) +end + +Base.size(e::UnitVector) = (e.n,) + +""" + BoxDirections{N} <: AbstractDirections{N} + +Box direction representation. + +### Fields + +- `n` -- dimension +""" +struct BoxDirections{N} <: AbstractDirections{N} + n::Int +end + +# constructor for type Float64 +BoxDirections(n::Int) = BoxDirections{Float64}(n) + +Base.eltype(::Type{BoxDirections{N}}) where N = AbstractVector{N} +Base.start(bd::BoxDirections) = 1 +Base.next(bd::BoxDirections{N}, state) where N = ( + UnitVector{N}(abs(state), bd.n, convert(N, sign(state))), # value + state == bd.n ? -bd.n : state + 1) # next state +Base.done(bd::BoxDirections, state) = state == 0 +Base.length(bd::BoxDirections) = 2*bd.n + +""" + dim(bd::BoxDirections)::Int + +Returns the dimension of the generated directions. + +### Input + +- `bd` -- box direction representation + +### Output + +The dimension of the generated directions. +""" +function dim(bd::BoxDirections)::Int + return bd.n +end From b15ebbea4af7ebcd9caf058521ceb6bb905eb4f0 Mon Sep 17 00:00:00 2001 From: schillic Date: Tue, 15 May 2018 23:37:34 +0200 Subject: [PATCH 3/6] add OctDirections type --- src/Approximations/Approximations.jl | 3 +- src/Approximations/template_directions.jl | 63 +++++++++++++++++++++++ 2 files changed, 65 insertions(+), 1 deletion(-) diff --git a/src/Approximations/Approximations.jl b/src/Approximations/Approximations.jl index fce9e6d0ae..c20916f33d 100644 --- a/src/Approximations/Approximations.jl +++ b/src/Approximations/Approximations.jl @@ -17,7 +17,8 @@ export approximate, overapproximate, radius, symmetric_interval_hull, - BoxDirections + BoxDirections, + OctDirections const TOL(N::Type{Float64}) = eps(N) const TOL(N::Type{Float32}) = eps(N) diff --git a/src/Approximations/template_directions.jl b/src/Approximations/template_directions.jl index 1f370a10a9..5a6bf91e36 100644 --- a/src/Approximations/template_directions.jl +++ b/src/Approximations/template_directions.jl @@ -78,3 +78,66 @@ The dimension of the generated directions. function dim(bd::BoxDirections)::Int return bd.n end + +# octagon directions + +""" + OctDirections{N} <: AbstractDirections{N} + +Octagon direction representation. + +### Fields + +- `n` -- dimension + +### Notes + +Octagon 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; then it enumerates all +box directions. +""" +struct OctDirections{N} <: AbstractDirections{N} + n::Int +end + +# constructor for type Float64 +OctDirections(n::Int) = OctDirections{Float64}(n) + +Base.eltype(::Type{OctDirections{N}}) where N = AbstractVector{N} +Base.start(od::OctDirections{N}) where N = ones(N, od.n) +function Base.next(od::OctDirections{N}, state::AbstractVector) where N + i = 1 + while i <= od.n && state[i] < 0 + state[i] = -state[i] + i = i+1 + end + if i > od.n + return (copy(state), 1) + else + state[i] = -state[i] + return (copy(state), state) + end +end +function Base.next(od::OctDirections{N}, state::Int) where N + return next(BoxDirections{N}(od.n), state) +end +Base.done(od::OctDirections, state) = state == 0 +Base.length(od::OctDirections) = 2^od.n + 2*od.n + +""" + dim(od::OctDirections)::Int + +Returns the dimension of the generated directions. + +### Input + +- `od` -- octagon direction representation + +### Output + +The dimension of the generated directions. +""" +function dim(od::OctDirections)::Int + return od.n +end From 2943141e31c6f0d82c4080039e18ff05f78edecc Mon Sep 17 00:00:00 2001 From: schillic Date: Wed, 16 May 2018 09:15:08 +0200 Subject: [PATCH 4/6] add overapproximate function for template directions --- src/Approximations/overapproximate.jl | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/src/Approximations/overapproximate.jl b/src/Approximations/overapproximate.jl index 0ef772ba6d..21fb70d0ab 100644 --- a/src/Approximations/overapproximate.jl +++ b/src/Approximations/overapproximate.jl @@ -121,6 +121,31 @@ function overapproximate(S::ConvexHull{N, Zonotope{N}, Zonotope{N}}, return Zonotope(center, generators) end +""" + overapproximate(X::LazySet, dir::AbstractDirections)::HPolytope + +Overapproximating a set with template directions. + +### Input + +- `X` -- set +- `dir` -- direction representation + +### Output + +A `HPolytope` overapproximating the set `X` with the directions from `dir`. +""" +function overapproximate(X::LazySet{N}, + dir::AbstractDirections{N})::HPolytope{N} where N + halfspaces = Vector{LazySets.LinearConstraint{N}}() + sizehint!(halfspaces, length(dir)) + H = HPolytope(halfspaces) + for d in dir + addconstraint!(H, LazySets.LinearConstraint(d, ρ(d, X))) + end + return H +end + @require IntervalArithmetic begin """ From fb7f2a0f61f9a768aeffa5b6df51d032855e39ac Mon Sep 17 00:00:00 2001 From: schillic Date: Wed, 16 May 2018 10:24:37 +0200 Subject: [PATCH 5/6] add unit tests for template directions --- test/runtests.jl | 1 + test/unit_template_directions.jl | 36 ++++++++++++++++++++++++++++++++ 2 files changed, 37 insertions(+) create mode 100644 test/unit_template_directions.jl diff --git a/test/runtests.jl b/test/runtests.jl index 03b183cf6a..960de46f08 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -37,6 +37,7 @@ include("to_N.jl") # Algorithms for approximation of convex sets using support vectors # ================================================================= @time @testset "LazySets.Approximations.overapproximation" begin include("unit_overapproximate.jl") end +@time @testset "LazySets.Approximations.template_directions" begin include("unit_template_directions.jl") end @time @testset "LazySets.Approximations.box_approximation" begin include("unit_box_approximation.jl") end @time @testset "LazySets.Approximations.ballinf_approximation" begin include("unit_ballinf_approximation.jl") end @time @testset "LazySets.Approximations.radiusdiameter" begin include("unit_radiusdiameter.jl") end diff --git a/test/unit_template_directions.jl b/test/unit_template_directions.jl new file mode 100644 index 0000000000..2cf6b8e5ab --- /dev/null +++ b/test/unit_template_directions.jl @@ -0,0 +1,36 @@ +import LazySets.Approximations, + Approximations.UnitVector, + Approximations.BoxDirections, + Approximations.OctDirections, + Approximations.overapproximate + +for N in [Float64, Float32, Rational{Int}] + # unit vector + for n in 1:3 + for i in 1:n + e = UnitVector(i, n, one(N)) + for j in 1:n + @test e[j] == (i == j ? one(N) : zero(N)) + end + end + end + + # template direction approximation + for n in 2:3 + B = BallInf(zeros(N, n), N(2.)) + A = 2.*eye(N, n) + ones(N, n, n) + X = A * B + + # box directions + dir = BoxDirections{N}(n) + @test dim(dir) == n + box = overapproximate(X, dir) + @test length(dir) == length(box.constraints) == 2*n + + # octagon directions + dir = OctDirections{N}(n) + @test dim(dir) == n + oct = overapproximate(X, dir) + @test length(dir) == length(oct.constraints) == 2^n + 2*n + end +end From 52ff26b2dec72df02b3c5cfd23adc785faa41d85 Mon Sep 17 00:00:00 2001 From: schillic Date: Wed, 16 May 2018 17:56:05 +0200 Subject: [PATCH 6/6] fix oct directions in 1D case --- src/Approximations/template_directions.jl | 8 ++++++-- test/unit_template_directions.jl | 4 ++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/Approximations/template_directions.jl b/src/Approximations/template_directions.jl index 5a6bf91e36..2a9142ab58 100644 --- a/src/Approximations/template_directions.jl +++ b/src/Approximations/template_directions.jl @@ -113,7 +113,11 @@ function Base.next(od::OctDirections{N}, state::AbstractVector) where N i = i+1 end if i > od.n - return (copy(state), 1) + if od.n == 1 + return (copy(state), 0) # finish here to avoid duplicates + else + return (copy(state), 1) # continue with box directions + end else state[i] = -state[i] return (copy(state), state) @@ -123,7 +127,7 @@ function Base.next(od::OctDirections{N}, state::Int) where N return next(BoxDirections{N}(od.n), state) end Base.done(od::OctDirections, state) = state == 0 -Base.length(od::OctDirections) = 2^od.n + 2*od.n +Base.length(od::OctDirections) = od.n == 1 ? 2 : 2^od.n + 2*od.n """ dim(od::OctDirections)::Int diff --git a/test/unit_template_directions.jl b/test/unit_template_directions.jl index 2cf6b8e5ab..8b1c5c75e7 100644 --- a/test/unit_template_directions.jl +++ b/test/unit_template_directions.jl @@ -16,7 +16,7 @@ for N in [Float64, Float32, Rational{Int}] end # template direction approximation - for n in 2:3 + for n in 1:3 B = BallInf(zeros(N, n), N(2.)) A = 2.*eye(N, n) + ones(N, n, n) X = A * B @@ -31,6 +31,6 @@ for N in [Float64, Float32, Rational{Int}] dir = OctDirections{N}(n) @test dim(dir) == n oct = overapproximate(X, dir) - @test length(dir) == length(oct.constraints) == 2^n + 2*n + @test length(dir) == length(oct.constraints) == (n == 1 ? 2 : 2^n + 2*n) end end