/
exact_sum.jl
49 lines (34 loc) · 1.31 KB
/
exact_sum.jl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
export exact_sum, ⊞
"""
exact_sum(P1::SparsePolynomialZonotope, P2::SparsePolynomialZonotope)
Compute the exact sum of sparse polyomial zonotopes ``P₁`` and ``P₂``.
### Input
- `P1` -- sparse polynomial zonotope
- `P2` -- sparse polynomial zonotope
### Output
A `SparsePolynomialZonotope` representing the exact sum ``P₁ ⊞ P₂``.
### Algorithm
This method implements Proposition 3.1.20 in [1].
[1] Kochdumper, Niklas. *Extensions of polynomial zonotopes and their application
to verification of cyber-physical systems.* PhD diss., Technische Universität
München, 2022.
"""
function exact_sum(P1::SparsePolynomialZonotope, P2::SparsePolynomialZonotope)
if indexvector(P1) != indexvector(P2)
throw(ArgumentError("the exact sum is currently only implemented for " *
"sparse polynomial zonotopes with the same index vector"))
end
c = center(P1) + center(P2)
G = hcat(genmat_dep(P1), genmat_dep(P2))
GI = hcat(genmat_indep(P1), genmat_indep(P2))
E = hcat(expmat(P1), expmat(P2))
idx = indexvector(P1)
return SparsePolynomialZonotope(c, G, GI, E, idx)
end
"""
⊞(X::LazySet, Y::LazySet)
Unicode alias constructor for the (concrete) `exact_sum` function.
### Notes
Write `\\boxplus[TAB]` to enter this symbol.
"""
const ⊞ = exact_sum