GitHub

Subset Check

The function ⊆ checks whether a set is a subset of another set. It can optionally produce a witness if the subset relation does not hold. The operator can be used in infix notation (X ⊆ Y).

Note

issubset can be used as an alternative name to ⊆.

Examples

We use the following four sets for illustration.

using LazySets, LazySets.Approximations, Plots
B1 = Ball1(-ones(2), 1.)
B2 = Ball2(ones(2), 1.)
BI = BallInf(zeros(2), 1.)
H = Hyperrectangle(ones(2), ones(2))
sets = [B1, B2, BI, H]

function plot_sets(sets)
    for S in sets
        println(S)
        plot!(S, 1e-2, fillalpha=0.1)
    end
end

function plot_points(points, prefix)
    for i in eachindex(points)
        p = points[i]
        num_occur = length(findfirst(x -> x == p, points[1:i]))
        x = p[1]
        y = p[2]
        if num_occur == 1
            x += 0.15
        elseif num_occur == 2
            y += 0.15
        elseif num_occur == 3
            x -= 0.15
        else
            y -= 0.15
        end
        plot!(Singleton(p))
        plot!(annotations=(x, y, text("$(prefix)$(i)")))
    end
end

plot1 = plot()
plot_sets(sets)
plot1
Example block output
println(B1 ⊆ B2)
w1 = ⊆(B1, B2, true)[2]
println(B1 ⊆ BI)
w2 = ⊆(B1, BI, true)[2]
println(B1 ⊆ H)
w3 = ⊆(B1, H, true)[2]
# 'B2 ⊆ B1' is not supported yet
# w11 = ⊆(B2, B1, true)[2]
println(B2 ⊆ BI)
w4 = ⊆(B2, BI, true)[2]
println(B2 ⊆ H)
println(BI ⊆ B1)
w5 = ⊆(BI, B1, true)[2]
println(BI ⊆ B2)
w6 = ⊆(BI, B2, true)[2]
println(BI ⊆ H)
w7 = ⊆(BI, H, true)[2]
println(H ⊆ B1)
w8 = ⊆(H, B1, true)[2]
println(H ⊆ B2)
w9 = ⊆(H, B2, true)[2]
println(H ⊆ BI)
w10 = ⊆(H, BI, true)[2];
2-element Vector{Float64}:
 2.0
 1.0
witnesses = [w1, w2, w3, w4, w5, w6, w7, w8, w9, w10]

plot1 = plot()
plot_sets(sets)
plot_points(witnesses, "w")
plot1
Example block output

Methods

Base.issubset — Function
issubset(X::LazySet, Y::LazySet, [witness]::Bool=false, args...)

Alias for ⊆ (inclusion check).

Input

  • X – set
  • Y – set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $X ⊆ Y$
  • If witness option is activated:
    • (true, []) iff $X ⊆ Y$
    • (false, v) iff $X ⊈ Y$ and $v ∈ X \setminus Y$

Notes

For more documentation see ⊆.

source
Base.:⊆ — Function
⊆(X::LazySet, P::LazySet, [witness]::Bool=false)

Check whether a set is contained in a polyhedral set, and if not, optionally compute a witness.

Input

  • X – inner set
  • Y – outer polyhedral set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $X ⊆ P$
  • If witness option is activated:
    • (true, []) iff $X ⊆ P$
    • (false, v) iff $X ⊈ P$ and $v ∈ X \setminus P$

Notes

We require that constraints_list(P) is available.

Algorithm

We check inclusion of X in every constraint of P.

source
Base.:⊆ — Function
⊆(S::LazySet, H::AbstractHyperrectangle, [witness]::Bool=false)

Check whether a set is contained in a hyperrectangular set, and if not, optionally compute a witness.

Input

  • S – inner set
  • H – outer hyperrectangular set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $S ⊆ H$
  • If witness option is activated:
    • (true, []) iff $S ⊆ H$
    • (false, v) iff $S ⊈ H$ and $v ∈ S ∖ H$

Algorithm

$S ⊆ H$ iff $\operatorname{ihull}(S) ⊆ H$, where $\operatorname{ihull}$ is the interval-hull operator.

source
Base.:⊆ — Function
⊆(P::AbstractPolytope, S::LazySet, [witness]::Bool=false;
  [algorithm]="constraints")

Check whether a polytopic set is contained in a convex set, and if not, optionally compute a witness.

Input

  • P – inner polytopic set

  • S – outer convex set

  • witness – (optional, default: false) compute a witness if activated

  • algorithm – (optional, default: "constraints") algorithm for the inclusion check; available options are:

    • "constraints", using the list of constraints of S (requires that S is polyhedral) and support-function evaluations of S

    • "vertices", using the list of vertices of P and membership evaluations of S

Output

  • If witness option is deactivated: true iff $P ⊆ S$
  • If witness option is activated:
    • (true, []) iff $P ⊆ S$
    • (false, v) iff $P ⊈ S$ and $v ∈ P ∖ S$

Algorithm

  • "vertices":

Since $S$ is convex, $P ⊆ S$ iff $v ∈ S$ for all vertices $v$ of $P$.

source
Base.:⊆ — Function
⊆(X::LazySet, P::LazySet, [witness]::Bool=false)

Check whether a set is contained in a polyhedral set, and if not, optionally compute a witness.

Input

  • X – inner set
  • Y – outer polyhedral set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $X ⊆ P$
  • If witness option is activated:
    • (true, []) iff $X ⊆ P$
    • (false, v) iff $X ⊈ P$ and $v ∈ X \setminus P$

Notes

We require that constraints_list(P) is available.

Algorithm

We check inclusion of X in every constraint of P.

source
⊆(S::LazySet, H::AbstractHyperrectangle, [witness]::Bool=false)

Check whether a set is contained in a hyperrectangular set, and if not, optionally compute a witness.

Input

  • S – inner set
  • H – outer hyperrectangular set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $S ⊆ H$
  • If witness option is activated:
    • (true, []) iff $S ⊆ H$
    • (false, v) iff $S ⊈ H$ and $v ∈ S ∖ H$

Algorithm

$S ⊆ H$ iff $\operatorname{ihull}(S) ⊆ H$, where $\operatorname{ihull}$ is the interval-hull operator.

source
⊆(P::AbstractPolytope, S::LazySet, [witness]::Bool=false;
  [algorithm]="constraints")

Check whether a polytopic set is contained in a convex set, and if not, optionally compute a witness.

Input

  • P – inner polytopic set

  • S – outer convex set

  • witness – (optional, default: false) compute a witness if activated

  • algorithm – (optional, default: "constraints") algorithm for the inclusion check; available options are:

    • "constraints", using the list of constraints of S (requires that S is polyhedral) and support-function evaluations of S

    • "vertices", using the list of vertices of P and membership evaluations of S

Output

  • If witness option is deactivated: true iff $P ⊆ S$
  • If witness option is activated:
    • (true, []) iff $P ⊆ S$
    • (false, v) iff $P ⊈ S$ and $v ∈ P ∖ S$

Algorithm

  • "vertices":

Since $S$ is convex, $P ⊆ S$ iff $v ∈ S$ for all vertices $v$ of $P$.

source
⊆(X::LazySet, P::AbstractPolyhedron, [witness]::Bool=false)

Check whether a convex set is contained in a polyhedral set, and if not, optionally compute a witness.

Input

  • X – inner convex set
  • P – outer polyhedral set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $X ⊆ P$
  • If witness option is activated:
    • (true, []) iff $X ⊆ P$
    • (false, v) iff $X ⊈ P$ and $v ∈ P ∖ X$

Algorithm

Since $X$ is convex, we can compare the support function of $X$ and $P$ in each direction of the constraints of $P$.

For witness generation, we use a support vector in the first direction where the above check fails.

source
Base.:⊆ — Method
⊆(X::LazySet, P::LazySet, [witness]::Bool=false)

Check whether a set is contained in a polyhedral set, and if not, optionally compute a witness.

Input

  • X – inner set
  • Y – outer polyhedral set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $X ⊆ P$
  • If witness option is activated:
    • (true, []) iff $X ⊆ P$
    • (false, v) iff $X ⊈ P$ and $v ∈ X \setminus P$

Notes

We require that constraints_list(P) is available.

Algorithm

We check inclusion of X in every constraint of P.

source
⊆(S::LazySet, H::AbstractHyperrectangle, [witness]::Bool=false)

Check whether a set is contained in a hyperrectangular set, and if not, optionally compute a witness.

Input

  • S – inner set
  • H – outer hyperrectangular set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $S ⊆ H$
  • If witness option is activated:
    • (true, []) iff $S ⊆ H$
    • (false, v) iff $S ⊈ H$ and $v ∈ S ∖ H$

Algorithm

$S ⊆ H$ iff $\operatorname{ihull}(S) ⊆ H$, where $\operatorname{ihull}$ is the interval-hull operator.

source
⊆(P::AbstractPolytope, S::LazySet, [witness]::Bool=false;
  [algorithm]="constraints")

Check whether a polytopic set is contained in a convex set, and if not, optionally compute a witness.

Input

  • P – inner polytopic set

  • S – outer convex set

  • witness – (optional, default: false) compute a witness if activated

  • algorithm – (optional, default: "constraints") algorithm for the inclusion check; available options are:

    • "constraints", using the list of constraints of S (requires that S is polyhedral) and support-function evaluations of S

    • "vertices", using the list of vertices of P and membership evaluations of S

Output

  • If witness option is deactivated: true iff $P ⊆ S$
  • If witness option is activated:
    • (true, []) iff $P ⊆ S$
    • (false, v) iff $P ⊈ S$ and $v ∈ P ∖ S$

Algorithm

  • "vertices":

Since $S$ is convex, $P ⊆ S$ iff $v ∈ S$ for all vertices $v$ of $P$.

source
⊆(X::LazySet, P::AbstractPolyhedron, [witness]::Bool=false)

Check whether a convex set is contained in a polyhedral set, and if not, optionally compute a witness.

Input

  • X – inner convex set
  • P – outer polyhedral set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $X ⊆ P$
  • If witness option is activated:
    • (true, []) iff $X ⊆ P$
    • (false, v) iff $X ⊈ P$ and $v ∈ P ∖ X$

Algorithm

Since $X$ is convex, we can compare the support function of $X$ and $P$ in each direction of the constraints of $P$.

For witness generation, we use a support vector in the first direction where the above check fails.

source
⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, [witness]::Bool=false)

Check whether a zonotopic set is contained in a hyperrectangular set.

Input

  • Z – inner zonotopic set
  • H – outer hyperrectangular set
  • witness – (optional, default: false) compute a witness if activated (currently not supported)

Output

true iff $Z ⊆ H$.

Algorithm

The algorithm is based on Lemma 3.1 in [1].

[1] Mitchell, I. M., Budzis, J., & Bolyachevets, A. Invariant, viability and discriminating kernel under-approximation via zonotope scaling. HSCC 2019.

source
Base.:⊆ — Function
⊆(H1::AbstractHyperrectangle, H2::AbstractHyperrectangle,
  [witness]::Bool=false)

Check whether a given hyperrectangular set is contained in another hyperrectangular set, and if not, optionally compute a witness.

Input

  • H1 – inner hyperrectangular set
  • H2 – outer hyperrectangular set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $H1 ⊆ H2$
  • If witness option is activated:
    • (true, []) iff $H1 ⊆ H2$
    • (false, v) iff $H1 ⊈ H2$ and $v ∈ H1 ∖ H2$

Algorithm

$H1 ⊆ H2$ iff $c_1 + r_1 ≤ c_2 + r_2 ∧ c_1 - r_1 ≥ c_2 - r_2$ iff $r_1 - r_2 ≤ c_1 - c_2 ≤ -(r_1 - r_2)$, where $≤$ is taken component-wise.

source
Base.:⊆ — Function
⊆(X::LazySet, P::AbstractPolyhedron, [witness]::Bool=false)

Check whether a convex set is contained in a polyhedral set, and if not, optionally compute a witness.

Input

  • X – inner convex set
  • P – outer polyhedral set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $X ⊆ P$
  • If witness option is activated:
    • (true, []) iff $X ⊆ P$
    • (false, v) iff $X ⊈ P$ and $v ∈ P ∖ X$

Algorithm

Since $X$ is convex, we can compare the support function of $X$ and $P$ in each direction of the constraints of $P$.

For witness generation, we use a support vector in the first direction where the above check fails.

source
Base.:⊆ — Function
⊆(S::AbstractSingleton, X::LazySet, [witness]::Bool=false)

Check whether a given set with a single value is contained in another set, and if not, optionally compute a witness.

Input

  • S – inner set with a single value
  • X – outer set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $S ⊆ X$
  • If witness option is activated:
    • (true, []) iff $S ⊆ X$
    • (false, v) iff $S ⊈ X$ and $v ∈ S ∖ X$
source
Base.:⊆ — Function
⊆(X::LazySet, P::LazySet, [witness]::Bool=false)

Check whether a set is contained in a polyhedral set, and if not, optionally compute a witness.

Input

  • X – inner set
  • Y – outer polyhedral set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $X ⊆ P$
  • If witness option is activated:
    • (true, []) iff $X ⊆ P$
    • (false, v) iff $X ⊈ P$ and $v ∈ X \setminus P$

Notes

We require that constraints_list(P) is available.

Algorithm

We check inclusion of X in every constraint of P.

source
⊆(S::LazySet, H::AbstractHyperrectangle, [witness]::Bool=false)

Check whether a set is contained in a hyperrectangular set, and if not, optionally compute a witness.

Input

  • S – inner set
  • H – outer hyperrectangular set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $S ⊆ H$
  • If witness option is activated:
    • (true, []) iff $S ⊆ H$
    • (false, v) iff $S ⊈ H$ and $v ∈ S ∖ H$

Algorithm

$S ⊆ H$ iff $\operatorname{ihull}(S) ⊆ H$, where $\operatorname{ihull}$ is the interval-hull operator.

source
⊆(H1::AbstractHyperrectangle, H2::AbstractHyperrectangle,
  [witness]::Bool=false)

Check whether a given hyperrectangular set is contained in another hyperrectangular set, and if not, optionally compute a witness.

Input

  • H1 – inner hyperrectangular set
  • H2 – outer hyperrectangular set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $H1 ⊆ H2$
  • If witness option is activated:
    • (true, []) iff $H1 ⊆ H2$
    • (false, v) iff $H1 ⊈ H2$ and $v ∈ H1 ∖ H2$

Algorithm

$H1 ⊆ H2$ iff $c_1 + r_1 ≤ c_2 + r_2 ∧ c_1 - r_1 ≥ c_2 - r_2$ iff $r_1 - r_2 ≤ c_1 - c_2 ≤ -(r_1 - r_2)$, where $≤$ is taken component-wise.

source
⊆(P::AbstractPolytope, S::LazySet, [witness]::Bool=false;
  [algorithm]="constraints")

Check whether a polytopic set is contained in a convex set, and if not, optionally compute a witness.

Input

  • P – inner polytopic set

  • S – outer convex set

  • witness – (optional, default: false) compute a witness if activated

  • algorithm – (optional, default: "constraints") algorithm for the inclusion check; available options are:

    • "constraints", using the list of constraints of S (requires that S is polyhedral) and support-function evaluations of S

    • "vertices", using the list of vertices of P and membership evaluations of S

Output

  • If witness option is deactivated: true iff $P ⊆ S$
  • If witness option is activated:
    • (true, []) iff $P ⊆ S$
    • (false, v) iff $P ⊈ S$ and $v ∈ P ∖ S$

Algorithm

  • "vertices":

Since $S$ is convex, $P ⊆ S$ iff $v ∈ S$ for all vertices $v$ of $P$.

source
⊆(X::LazySet, P::AbstractPolyhedron, [witness]::Bool=false)

Check whether a convex set is contained in a polyhedral set, and if not, optionally compute a witness.

Input

  • X – inner convex set
  • P – outer polyhedral set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $X ⊆ P$
  • If witness option is activated:
    • (true, []) iff $X ⊆ P$
    • (false, v) iff $X ⊈ P$ and $v ∈ P ∖ X$

Algorithm

Since $X$ is convex, we can compare the support function of $X$ and $P$ in each direction of the constraints of $P$.

For witness generation, we use a support vector in the first direction where the above check fails.

source
⊆(S::AbstractSingleton, X::LazySet, [witness]::Bool=false)

Check whether a given set with a single value is contained in another set, and if not, optionally compute a witness.

Input

  • S – inner set with a single value
  • X – outer set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $S ⊆ X$
  • If witness option is activated:
    • (true, []) iff $S ⊆ X$
    • (false, v) iff $S ⊈ X$ and $v ∈ S ∖ X$
source
⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, [witness]::Bool=false)

Check whether a zonotopic set is contained in a hyperrectangular set.

Input

  • Z – inner zonotopic set
  • H – outer hyperrectangular set
  • witness – (optional, default: false) compute a witness if activated (currently not supported)

Output

true iff $Z ⊆ H$.

Algorithm

The algorithm is based on Lemma 3.1 in [1].

[1] Mitchell, I. M., Budzis, J., & Bolyachevets, A. Invariant, viability and discriminating kernel under-approximation via zonotope scaling. HSCC 2019.

source
Base.:⊆ — Function
⊆(S1::AbstractSingleton, S2::AbstractSingleton, witness::Bool=false)

Check whether a given set with a single value is contained in another set with a single value, and if not, optionally compute a witness.

Input

  • S1 – inner set with a single value
  • S2 – outer set with a single value
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $S1 ⊆ S2$ iff $S1 == S2$
  • If witness option is activated:
    • (true, []) iff $S1 ⊆ S2$
    • (false, v) iff $S1 ⊈ S2$ and $v ∈ S1 ∖ S2$
source
Base.:⊆ — Function
⊆(B1::Ball2, B2::Ball2, [witness]::Bool=false)

Check whether a ball in the 2-norm is contained in another ball in the 2-norm, and if not, optionally compute a witness.

Input

  • B1 – inner ball in the 2-norm
  • B2 – outer ball in the 2-norm
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $B1 ⊆ B2$
  • If witness option is activated:
    • (true, []) iff $B1 ⊆ B2$
    • (false, v) iff $B1 ⊈ B2$ and $v ∈ B1 ∖ B2$

Algorithm

$B1 ⊆ B2$ iff $‖ c_1 - c_2 ‖_2 + r_1 ≤ r_2$

source
Base.:⊆ — Function
⊆(B::Union{Ball2, Ballp}, S::AbstractSingleton, witness::Bool=false)

Check whether a ball in the 2-norm or p-norm is contained in a set with a single value, and if not, optionally compute a witness.

Input

  • B – inner ball in the 2-norm or p-norm
  • S – outer set with a single value
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $B ⊆ S$
  • If witness option is activated:
    • (true, []) iff $B ⊆ S$
    • (false, v) iff $B ⊈ S$ and $v ∈ B ∖ S$
source
Base.:⊆ — Function
⊆(L::LineSegment, S::LazySet, witness::Bool=false)

Check whether a line segment is contained in a convex set, and if not, optionally compute a witness.

Input

  • L – inner line segment
  • S – outer convex set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $L ⊆ S$
  • If witness option is activated:
    • (true, []) iff $L ⊆ S$
    • (false, v) iff $L ⊈ S$ and $v ∈ L ∖ S$

Algorithm

Since $S$ is convex, $L ⊆ S$ iff $p ∈ S$ and $q ∈ S$, where $p, q$ are the end points of $L$.

source
Base.:⊆ — Function
⊆(X::LazySet, P::LazySet, [witness]::Bool=false)

Check whether a set is contained in a polyhedral set, and if not, optionally compute a witness.

Input

  • X – inner set
  • Y – outer polyhedral set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $X ⊆ P$
  • If witness option is activated:
    • (true, []) iff $X ⊆ P$
    • (false, v) iff $X ⊈ P$ and $v ∈ X \setminus P$

Notes

We require that constraints_list(P) is available.

Algorithm

We check inclusion of X in every constraint of P.

source
⊆(S::LazySet, H::AbstractHyperrectangle, [witness]::Bool=false)

Check whether a set is contained in a hyperrectangular set, and if not, optionally compute a witness.

Input

  • S – inner set
  • H – outer hyperrectangular set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $S ⊆ H$
  • If witness option is activated:
    • (true, []) iff $S ⊆ H$
    • (false, v) iff $S ⊈ H$ and $v ∈ S ∖ H$

Algorithm

$S ⊆ H$ iff $\operatorname{ihull}(S) ⊆ H$, where $\operatorname{ihull}$ is the interval-hull operator.

source
⊆(P::AbstractPolytope, S::LazySet, [witness]::Bool=false;
  [algorithm]="constraints")

Check whether a polytopic set is contained in a convex set, and if not, optionally compute a witness.

Input

  • P – inner polytopic set

  • S – outer convex set

  • witness – (optional, default: false) compute a witness if activated

  • algorithm – (optional, default: "constraints") algorithm for the inclusion check; available options are:

    • "constraints", using the list of constraints of S (requires that S is polyhedral) and support-function evaluations of S

    • "vertices", using the list of vertices of P and membership evaluations of S

Output

  • If witness option is deactivated: true iff $P ⊆ S$
  • If witness option is activated:
    • (true, []) iff $P ⊆ S$
    • (false, v) iff $P ⊈ S$ and $v ∈ P ∖ S$

Algorithm

  • "vertices":

Since $S$ is convex, $P ⊆ S$ iff $v ∈ S$ for all vertices $v$ of $P$.

source
⊆(X::LazySet, P::AbstractPolyhedron, [witness]::Bool=false)

Check whether a convex set is contained in a polyhedral set, and if not, optionally compute a witness.

Input

  • X – inner convex set
  • P – outer polyhedral set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $X ⊆ P$
  • If witness option is activated:
    • (true, []) iff $X ⊆ P$
    • (false, v) iff $X ⊈ P$ and $v ∈ P ∖ X$

Algorithm

Since $X$ is convex, we can compare the support function of $X$ and $P$ in each direction of the constraints of $P$.

For witness generation, we use a support vector in the first direction where the above check fails.

source
⊆(L::LineSegment, S::LazySet, witness::Bool=false)

Check whether a line segment is contained in a convex set, and if not, optionally compute a witness.

Input

  • L – inner line segment
  • S – outer convex set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $L ⊆ S$
  • If witness option is activated:
    • (true, []) iff $L ⊆ S$
    • (false, v) iff $L ⊈ S$ and $v ∈ L ∖ S$

Algorithm

Since $S$ is convex, $L ⊆ S$ iff $p ∈ S$ and $q ∈ S$, where $p, q$ are the end points of $L$.

source
⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, [witness]::Bool=false)

Check whether a zonotopic set is contained in a hyperrectangular set.

Input

  • Z – inner zonotopic set
  • H – outer hyperrectangular set
  • witness – (optional, default: false) compute a witness if activated (currently not supported)

Output

true iff $Z ⊆ H$.

Algorithm

The algorithm is based on Lemma 3.1 in [1].

[1] Mitchell, I. M., Budzis, J., & Bolyachevets, A. Invariant, viability and discriminating kernel under-approximation via zonotope scaling. HSCC 2019.

source
Base.:⊆ — Function
⊆(x::Interval, y::Interval, [witness]::Bool=false)

Check whether an interval is contained in another interval.

Input

  • x – inner interval
  • y – outer interval
  • witness – (optional, default: false) compute a witness if activated

Output

true iff $x ⊆ y$.

source
Base.:⊆ — Function
⊆(x::Interval, U::UnionSet, [witness]::Bool=false)

Check whether an interval is contained in the union of two convex sets.

Input

  • x – inner interval
  • U – outer union of two convex sets

Output

true iff x ⊆ U.

Notes

This implementation assumes that U is a union of one-dimensional convex sets. Since these are equivalent to intervals, we convert to Intervals.

Algorithm

Let $U = a ∪ b$ where $a$ and $b$ are intervals and assume that the lower bound of $a$ is to the left of $b$. If the lower bound of $x$ is to the left of $a$, we have a counterexample. Otherwise we compute the set difference $y = x \ a$ and check whether $y ⊆ b$ holds.

source
Base.:⊆ — Function
⊆(∅::EmptySet, X::LazySet, witness::Bool=false)

Check whether the empty set is contained in another set.

Input

  • ∅ – inner empty set
  • X – outer set
  • witness – (optional, default: false) compute a witness if activated (ignored, just kept for interface reasons)

Output

true.

source
Base.:⊆ — Function
⊆(X::LazySet, ∅::EmptySet, [witness]::Bool=false)

Check whether a set is contained in the empty set.

Input

  • X – inner set
  • ∅ – outer empty set
  • witness – (optional, default: false) compute a witness if activated

Output

true iff X is empty.

Algorithm

We rely on isempty(X) for the emptiness check and on an_element(X) for witness production.

source
Base.:⊆ — Function
⊆(U::UnionSet, X::LazySet, [witness]::Bool=false)

Check whether a union of two convex sets is contained in another set.

Input

  • U – inner union of two convex sets
  • X – outer set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $\text{U} ⊆ X$
  • If witness option is activated:
    • (true, []) iff $\text{U} ⊆ X$
    • (false, v) iff $\text{U} \not\subseteq X$ and $v ∈ \text{U} ∖ X$
source
Base.:⊆ — Function
⊆(U::UnionSetArray, X::LazySet, [witness]::Bool=false)

Check whether a union of a finite number of convex sets is contained in another set.

Input

  • U – inner union of a finite number of convex sets
  • X – outer set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $\text{U} ⊆ X$
  • If witness option is activated:
    • (true, []) iff $\text{U} ⊆ X$
    • (false, v) iff $\text{U} \not\subseteq X$ and $v ∈ \text{U} ∖ X$
source
Base.:⊆ — Function
⊆(X::LazySet, U::Universe, [witness]::Bool=false)

Check whether a set is contained in a universe.

Input

  • X – inner set
  • U – outer universe
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true
  • If witness option is activated: (true, [])
source
Base.:⊆ — Function
⊆(U::Universe, X::LazySet, [witness]::Bool=false)

Check whether a universe is contained in another set, and otherwise optionally compute a witness.

Input

  • U – inner universe
  • X – outer set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $U ⊆ X$
  • If witness option is activated:
    • (true, []) iff $U ⊆ X$
    • (false, v) iff $U \not\subseteq X$ and $v ∈ U ∖ X$

Algorithm

We fall back to isuniversal(X).

source
Base.:⊆ — Function
⊆(X::LazySet, C::Complement, [witness]::Bool=false)

Check whether a set is contained in the complement of another set, and otherwise optionally compute a witness.

Input

  • X – inner set
  • C – outer complement of a set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $X ⊆ C$
  • If witness option is activated:
    • (true, []) iff $X ⊆ C$
    • (false, v) iff $X \not\subseteq C$ and $v ∈ X ∖ C$

Algorithm

We fall back to isdisjoint(X, C.X), which can be justified as follows.

\[ X ⊆ Y^C ⟺ X ∩ Y = ∅\]

source
Base.:⊆ — Function
⊆(X::CartesianProduct, Y::CartesianProduct, [witness]::Bool=false;
  check_block_equality::Bool=true)

Check whether a Cartesian product of two sets is contained in another Cartesian product of two sets, and otherwise optionally compute a witness.

Input

  • X – inner Cartesian product of two sets
  • Y – outer Cartesian product of two sets
  • witness – (optional, default: false) compute a witness if activated
  • check_block_equality – (optional, default: true) flag for checking that the block structure of the two sets is identical

Output

  • If witness option is deactivated: true iff $X ⊆ Y$
  • If witness option is activated:
    • (true, []) iff $X ⊆ Y$
    • (false, v) iff $X \not\subseteq Y$ and $v ∈ X ∖ Y$

Notes

This algorithm requires that the two Cartesian products share the same block structure. If check_block_equality is activated, we check this property and, if it does not hold, we use a fallback implementation based on conversion to constraint representation (assuming that the sets are polyhedral).

Algorithm

We check inclusion for each block of the Cartesian products.

For witness production, we obtain a witness in one of the blocks. We then construct a high-dimensional witness by obtaining any point in the other blocks (using an_element) and concatenating these (lower-dimensional) points.

source
Base.:⊆ — Function
⊆(X::CartesianProductArray, Y::CartesianProductArray, [witness]::Bool=false;
  check_block_equality::Bool=true)

Check whether a Cartesian product of finitely many sets is contained in another Cartesian product of finitely many sets, and otherwise optionally compute a witness.

Input

  • X – inner Cartesian product of finitely many sets
  • Y – outer Cartesian product of finitely many sets
  • witness – (optional, default: false) compute a witness if activated
  • check_block_equality – (optional, default: true) flag for checking that the block structure of the two sets is identical

Output

  • If witness option is deactivated: true iff $X ⊆ Y$
  • If witness option is activated:
    • (true, []) iff $X ⊆ Y$
    • (false, v) iff $X \not\subseteq Y$ and $v ∈ X ∖ Y$

Notes

This algorithm requires that the two Cartesian products share the same block structure. If check_block_equality is activated, we check this property and, if it does not hold, we use a fallback implementation based on conversion to constraint representation (assuming that the sets are polyhedral).

Algorithm

We check inclusion for each block of the Cartesian products.

For witness production, we obtain a witness in one of the blocks. We then construct a high-dimensional witness by obtaining any point in the other blocks (using an_element) and concatenating these (lower-dimensional) points.

source
Base.:⊆ — Function
⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, [witness]::Bool=false)

Check whether a zonotopic set is contained in a hyperrectangular set.

Input

  • Z – inner zonotopic set
  • H – outer hyperrectangular set
  • witness – (optional, default: false) compute a witness if activated (currently not supported)

Output

true iff $Z ⊆ H$.

Algorithm

The algorithm is based on Lemma 3.1 in [1].

[1] Mitchell, I. M., Budzis, J., & Bolyachevets, A. Invariant, viability and discriminating kernel under-approximation via zonotope scaling. HSCC 2019.

source
Base.:⊆ — Function
⊆(X::LazySet{N}, U::UnionSetArray, witness::Bool=false;
  filter_redundant_sets::Bool=true) where {N}

Check whether a set is contained in a union of a finite number of sets.

Input

  • X – inner set
  • U – outer union of a finite number of sets
  • witness – (optional, default: false) compute a witness if activated
  • filter_redundant_sets – (optional, default: true) ignore sets in U that do not intersect with X

Output

true iff $X ⊆ U$.

Algorithm

This implementation is general and successively removes parts from X that are covered by the sets in the union $U$ using the difference function. For the resulting subsets, this implementation relies on the methods isdisjoint, ⊆, and intersection.

As a preprocessing, this implementation checks if X is contained in any of the sets in U.

The filter_redundant_sets option controls whether sets in U that do not intersect with X should be ignored.

source

Strict subset check

IntervalArithmetic.:⊂ — Function
⊂(X::LazySet{N}, Y::LazySet, [witness]::Bool=false) where {N}

Strict inclusion check of a set in another set.

Input

  • X – first set
  • Y – second set
  • witness – (optional, default: false) compute a witness if activated

Output

  • If witness option is deactivated: true iff $X ⊂ Y$
  • If witness option is activated:
    • (true, v) iff $X ⊂ Y$ and $v ∈ Y \setminus X$
    • (false, []) iff not $X ⊂ Y$

Algorithm

We check inclusion of X in Y and then check inclusion of Y in X:

\[X ⊂ Y \Leftrightarrow X ⊆ Y \land ¬ (Y ⊆ X)\]

source