#1413 - Add concrete version of zonotope algorithm to manual

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

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)

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

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

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}