#495 - Remove witness field from properties

docs/make.jl

@@ -13,6 +13,7 @@ makedocs(
         "User interface" => "lib/interface.md",
         "Systems" => "lib/systems.md",
         "Algorithms" => "lib/algorithms.md",
+        "Properties" => "lib/properties.md",
         "Transformations" => "lib/transformations.md",
         "Discretization" => "lib/discretize.md",
         "Distributed computations" => "lib/distributed.md"],

docs/src/lib/properties.md

@@ -0,0 +1,37 @@
+# Properties
+
+This module provides representations of (safety) properties.
+
+```@contents
+Pages = ["properties.md"]
+Depth = 3
+```
+
+```@meta
+CurrentModule = Reachability.Properties
+```
+
+## General property interface
+
+```@docs
+Property
+```
+
+### Boolean combination of properties
+
+```@docs
+Conjunction
+check(::Conjunction, ::LazySet{N}) where {N<:Real}
+Disjunction
+check(::Disjunction, ::LazySet{N}) where {N<:Real}
+```
+
+### Specific properties
+
+
+```@docs
+SafeStatesProperty
+check(::SafeStatesProperty, ::LazySet)
+BadStatesProperty
+check(::BadStatesProperty, ::LazySet)
+```

src/Properties/BadStatesProperty.jl

@@ -0,0 +1,55 @@
+"""
+    BadStatesProperty{N<:Real} <: Property
+
+Type that represents a safety property characterized by a set of bad states.
+The property is satisfied by a given set of states if the intersection with the
+set of bad states is empty.
+
+### Fields
+
+- `bad`     -- convex set representing the bad states
+- `witness` -- witness point (empty vector if not set)
+
+### Notes
+
+The following formula characterizes whether a set ``X`` satisfies a safety
+property characterized by a set of bad states 𝑃:
+
+```math
+    X \\models 𝑃 \\iff X ∩ 𝑃.\\texttt{bad} = ∅
+```
+"""
+mutable struct BadStatesProperty{N<:Real} <: Property
+    bad::LazySet
+    witness::Vector{N}
+
+    BadStatesProperty{N}(bad::LazySet) where {N<:Real} = new(bad, N[])
+end
+
+# type-less convenience constructor
+BadStatesProperty(bad::LazySet{N}) where {N<:Real} =
+    BadStatesProperty{N}(bad)
+
+"""
+    check(𝑃::BadStatesProperty, X::LazySet; witness::Bool=false)
+
+Checks whether a convex set is disjoint from the set of bad states.
+
+### Input
+
+- `𝑃`       -- safety property with bad states
+- `X`       -- convex set
+- `witness` -- (optional, default: `false`) flag for returning a counterexample
+               if the property is violated
+
+### Output
+
+Let ``Y`` be the bad states represented by 𝑃.
+* 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 ∩ Y``
+"""
+@inline function check(𝑃::BadStatesProperty, X::LazySet; witness::Bool=false)
+    return isdisjoint(X, 𝑃.bad, witness)
+end

src/Properties/Conjunction.jl

@@ -0,0 +1,56 @@
+"""
+    Conjunction <: Property
+
+Type that represents a conjunction of properties.
+
+### Fields
+
+- `conjuncts` -- vector of properties
+
+### Notes
+
+The following formula characterizes whether a set ``X`` satisfies a disjunction
+``𝑃 = 𝑃_1 ∧ 𝑃_2 ∧ … ∧ 𝑃_m``:
+
+```math
+    X \\models 𝑃 \\iff X \\models 𝑃_j \\text{ for all } 1 ≤ j ≤ m
+```
+"""
+struct Conjunction <: Property
+    conjuncts::Vector{Property}
+end
+
+"""
+    check(𝑃::Conjunction, X::LazySet{N}; witness::Bool=false) where {N<:Real}
+
+Check whether a convex set satisfies a conjunction of properties.
+
+### Input
+
+- `𝑃`       -- conjunction of properties
+- `X`       -- convex set
+- `witness` -- (optional, default: `false`) flag for returning a counterexample
+               if the property is violated
+
+### Output
+
+* If `witness` option is deactivated: `true` iff `X` satisfies the property `𝑃`
+* If `witness` option is activated:
+  * `(true, [])` iff `X` satisfies the property `𝑃`
+  * `(false, v)` iff `X` does not satisfy the property `𝑃` with witness `v`
+
+### Notes
+
+By convention, the empty conjunction is equivalent to `true` and hence is
+satisfied by any set.
+"""
+function check(𝑃::Conjunction, X::LazySet{N};
+               witness::Bool=false) where {N<:Real}
+    for conjunct in 𝑃.conjuncts
+        result = check(conjunct, X; witness=witness)
+        if (witness && !result[1]) || !result
+            return result
+        end
+    end
+    return witness ? (true, N[]) : true
+end

src/Properties/Disjunction.jl

@@ -0,0 +1,95 @@
+"""
+    Disjunction <: Property
+
+Type that represents a disjunction of properties.
+
+### Fields
+
+- `disjuncts` -- vector of properties (elements are reordered by this type)
+- `reorder`   -- flag to indicate whether shuffling is allowed
+
+### Notes
+
+The following formula characterizes whether a set ``X`` satisfies a disjunction
+``𝑃 = 𝑃_1 ∨ 𝑃_2 ∨ … ∨ 𝑃_m``:
+
+```math
+    X \\models 𝑃 \\iff X \\models 𝑃_j \\text{ for some } 1 ≤ j ≤ m
+```
+
+If the `reorder` flag is set, the disjuncts may be reordered after each call to
+[`check`](@ref check(𝑃::Disjunction, X::LazySet{N}) where {N<:Real}) as a
+heuristics to make subsequent checks faster.
+"""
+struct Disjunction <: Property
+    disjuncts::Vector{Property}
+    reorder::Bool
+end
+
+# default constructor with activated reordering
+Disjunction(disjuncts::Vector{<:Property}) = Disjunction(disjuncts, true)
+
+"""
+    check(𝑃::Disjunction, X::LazySet{N}; witness::Bool=false) where {N<:Real}
+
+Check whether a convex set satisfies a disjunction of properties.
+
+### Input
+
+- `𝑃`       -- disjunction of properties
+- `X`       -- convex set
+- `witness` -- (optional, default: `false`) flag for returning a counterexample
+               if the property is violated
+
+### Output
+
+* If `witness` option is deactivated: `true` iff `X` satisfies the property `𝑃`
+* If `witness` option is activated:
+  * `(true, [])` iff `X` satisfies the property `𝑃`
+  * `(false, v)` iff `X` does not satisfy the property `𝑃` with witness `v`;
+    note that `v == N[]` if 𝑃 is the empty disjunction
+
+### Notes
+
+By convention, the empty disjunction is equivalent to `false` and hence is
+satisfied by no set.
+
+If the `𝑃.reorder` flag is set, the disjuncts may be reordered as a heuristics
+to make subsequent checks faster.
+Since we check satisfaction from left to right, we move the disjunct for which
+satisfaction was established to the front.
+
+To be consistent with other propertes, the `witness` option only returns *one*
+counterexample, namely for the left-most disjunct in the `disjuncts` vector.
+We deactivate witness production for checking the remaining disjuncts.
+"""
+function check(𝑃::Disjunction, X::LazySet{N};
+               witness::Bool=false) where {N<:Real}
+    v = N[]
+    create_witness = witness
+    for (i, conjunct) in enumerate(𝑃.disjuncts)
+        result = check(conjunct, X; witness=create_witness)
+        if (create_witness && result[1]) || result
+            _reorder!(𝑃, i)
+            return witness ? (true, N[]) : true
+        elseif create_witness
+            v = result[2]
+            # deactivate witness production for remaining checks
+            create_witness = false
+        end
+    end
+    return witness ? (false, v) : false
+end
+
+function _reorder!(𝑃::Disjunction, i::Int)
+    if !𝑃.reorder || i == 1
+        return nothing
+    end
+    first = 𝑃.disjuncts[i]
+    while i > 1
+        𝑃.disjuncts[i] = 𝑃.disjuncts[i-1]
+        i -= 1
+    end
+    𝑃.disjuncts[1] = first
+    return nothing
+end

src/Properties/Properties.jl

@@ -11,16 +11,17 @@ using LazySets
 # ==============================
 include("Property.jl")
 export Property,
-       check_property
+       check
 
-include("LinearConstraintProperty.jl")
-export LinearConstraintProperty,
-       Clause
+include("Conjunction.jl")
+include("Disjunction.jl")
+export Conjunction,
+       Disjunction
 
-include("IntersectionProperty.jl")
-export IntersectionProperty
+include("BadStatesProperty.jl")
+export BadStatesProperty
 
-include("SubsetProperty.jl")
-export SubsetProperty
+include("SafeStatesProperty.jl")
+export SafeStatesProperty
 
 end # module