From 9620759992f686be23f09423b36d60de09c48c85 Mon Sep 17 00:00:00 2001 From: schillic Date: Sat, 15 Jun 2019 14:42:49 +0200 Subject: [PATCH 1/2] add concrete zonotope algorithm in manual --- docs/src/man/reach_zonotopes.md | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/docs/src/man/reach_zonotopes.md b/docs/src/man/reach_zonotopes.md index bf6f5a02e7..1812444f3c 100644 --- a/docs/src/man/reach_zonotopes.md +++ b/docs/src/man/reach_zonotopes.md @@ -29,12 +29,20 @@ in the time interval ``t ∈ [0, T]``, where: Given a step size ``δ``, `Algorithm1` returns a sequence of sets that overapproximates the states reachable by any trajectory of this IVP. +We present the algorithm parametric in the option to compute the sets in a lazy +or in a concrete way. +If the parameter `lazy` is `true`, the implementation constructs a `LinearMap` +wrapper (represented as a multiplication `*` of a matrix and a set) and a +`MinkowskiSum` wrapper (represented as a sum `⊕` of two sets). +If the parameter `lazy` is `false`, the implementation calls the concrete +counterparts `linear_map` and `minkowski_sum`. + ## Algorithm ```@example example_reach_zonotopes using Plots, LazySets, LinearAlgebra, SparseArrays -function Algorithm1(A, X0, δ, μ, T) +function Algorithm1(A, X0, δ, μ, T; lazy::Bool=false) # bloating factors Anorm = norm(A, Inf) α = (exp(δ * Anorm) - 1 - δ * Anorm) / norm(X0, Inf) @@ -54,13 +62,17 @@ function Algorithm1(A, X0, δ, μ, T) ϕm = (I-ϕ) / 2 c = X0.center Q1_generators = hcat(ϕp * X0.generators, ϕm * c, ϕm * X0.generators) - Q[1] = Zonotope(ϕp * c, Q1_generators) ⊕ BallInf(zeros(n), α + β) + Q[1] = lazy ? + Zonotope(ϕp * c, Q1_generators) ⊕ BallInf(zeros(n), α + β) : + minkowski_sum(Zonotope(ϕp * c, Q1_generators), BallInf(zeros(n), α + β)) R[1] = Q[1] # set recurrence for [δ, 2δ], ..., [(N-1)δ, Nδ] ballβ = BallInf(zeros(n), β) for i in 2:N - Q[i] = ϕ * Q[i-1] ⊕ ballβ + Q[i] = lazy ? + ϕ * Q[i-1] ⊕ ballβ : + minkowski_sum(linear_map(ϕ, Q[i-1]), ballβ) R[i] = Q[i] end return R From 43b3997f182bd47fa09a1f9131899b718bbd9e50 Mon Sep 17 00:00:00 2001 From: schillic Date: Tue, 18 Jun 2019 08:37:49 +0200 Subject: [PATCH 2/2] generalize minkowski_sum to AbstractZonotope --- docs/src/lib/interfaces.md | 1 + docs/src/lib/representations.md | 1 - src/AbstractZonotope.jl | 25 +++++++++++++++++++++++++ src/Zonotope.jl | 20 -------------------- 4 files changed, 26 insertions(+), 21 deletions(-) diff --git a/docs/src/lib/interfaces.md b/docs/src/lib/interfaces.md index e17fb1531f..fbee0c4a48 100644 --- a/docs/src/lib/interfaces.md +++ b/docs/src/lib/interfaces.md @@ -221,6 +221,7 @@ This interface defines the following functions: ngens(Z::AbstractZonotope) genmat_fallback(Z::AbstractZonotope{N}) where {N<:Real} generators_fallback(Z::AbstractZonotope{N}) where {N<:Real} +minkowski_sum(::AbstractZonotope{N}, ::AbstractZonotope{N}) where {N<:Real} ``` ##### Hyperrectangle diff --git a/docs/src/lib/representations.md b/docs/src/lib/representations.md index 830151782f..ccf85dcb9a 100644 --- a/docs/src/lib/representations.md +++ b/docs/src/lib/representations.md @@ -688,7 +688,6 @@ center(::Zonotope{N}) where {N<:Real} order(::Zonotope) generators(Z::Zonotope) genmat(Z::Zonotope) -minkowski_sum(::Zonotope{N}, ::Zonotope{N}) where {N<:Real} linear_map(::AbstractMatrix{N}, ::Zonotope{N}) where {N<:Real} translate(::Zonotope{N}, ::AbstractVector{N}) where {N<:Real} scale(::Real, ::Zonotope) diff --git a/src/AbstractZonotope.jl b/src/AbstractZonotope.jl index abb534be5b..d0606ded1d 100644 --- a/src/AbstractZonotope.jl +++ b/src/AbstractZonotope.jl @@ -136,3 +136,28 @@ An integer representing the number of generators. function ngens(Z::AbstractZonotope)::Int return length(generators(Z)) end + +""" + minkowski_sum(Z1::AbstractZonotope{N}, Z2::AbstractZonotope{N}) + where {N<:Real} + +Concrete Minkowski sum of a pair of zonotopic sets. + +### Input + +- `Z1` -- zonotopic set +- `Z2` -- zonotopic set + +### Output + +A `Zonotope` corresponding to the concrete Minkowski sum of `Z1` and `Z2`. + +### Algorithm + +The resulting zonotope is obtained by summing up the centers and concatenating +the generators of `Z1` and `Z2`. +""" +function minkowski_sum(Z1::AbstractZonotope{N}, + Z2::AbstractZonotope{N}) where {N<:Real} + return Zonotope(center(Z1) + center(Z2), [genmat(Z1) genmat(Z2)]) +end diff --git a/src/Zonotope.jl b/src/Zonotope.jl index 4419a7882d..3e37abc3fb 100644 --- a/src/Zonotope.jl +++ b/src/Zonotope.jl @@ -4,7 +4,6 @@ import Base: rand, export Zonotope, order, - minkowski_sum, linear_map, scale, ngens, @@ -388,25 +387,6 @@ function order(Z::Zonotope)::Rational return ngens(Z) // dim(Z) end -""" - minkowski_sum(Z1::Zonotope{N}, Z2::Zonotope{N}) where {N<:Real} - -Concrete Minkowski sum of a pair of zonotopes. - -### Input - -- `Z1` -- one zonotope -- `Z2` -- another zonotope - -### Output - -The zonotope obtained by summing the centers and concatenating the generators -of ``Z_1`` and ``Z_2``. -""" -function minkowski_sum(Z1::Zonotope{N}, Z2::Zonotope{N}) where {N<:Real} - return Zonotope(Z1.center + Z2.center, [Z1.generators Z2.generators]) -end - """ linear_map(M::AbstractMatrix{N}, Z::Zonotope{N}) where {N<:Real}