#474 - Revise 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)
+Disjunction
+check(::Disjunction, ::LazySet)
+```
+
+### 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)::Bool
+
+Checks whether a convex set is disjoint from the set of bad states.
+
+### Input
+
+- `𝑃` -- safety property with bad states
+- `X` -- convex set
+
+### Output
+
+`true` iff the given set of states does not intersect with the set of bad
+states.
+"""
+@inline function check(𝑃::BadStatesProperty, X::LazySet)::Bool
+    empty_intersection, witness = is_intersection_empty(X, 𝑃.bad, true)
+    if !empty_intersection
+        # store violation witness
+        𝑃.witness = witness
+    end
+    return empty_intersection
+end

src/Properties/Conjunction.jl

@@ -0,0 +1,44 @@
+"""
+    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)::Bool
+
+Check whether a convex set satisfies a conjunction of properties.
+
+### Input
+
+- `𝑃` -- conjunction of properties
+- `X` -- convex set
+
+### Output
+
+`true` iff `X` satisfies the conjunction of properties `𝑃`.
+"""
+function check(𝑃::Conjunction, X::LazySet)::Bool
+    for conjunct in 𝑃.conjuncts
+        if !check(conjunct, X)
+            return false
+        end
+    end
+    return true
+end

src/Properties/Disjunction.jl

@@ -0,0 +1,74 @@
+"""
+    Disjunction <: Property
+
+Type that represents a disjunction of properties.
+
+### Fields
+
+- `disjuncts` -- vector of properties (elements are reorder 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(𝑃::Disjunction, X::LazySet)`](@ref) 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)::Bool
+
+Check whether a convex set satisfies a disjunction of properties.
+
+### Input
+
+- `𝑃` -- disjunction of properties
+- `X` -- convex set
+
+### Output
+
+`true` iff `X` satisfies the disjunction of properties `𝑃`.
+
+### Notes
+
+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.
+"""
+function check(𝑃::Disjunction, X::LazySet)::Bool
+    for (i, conjunct) in enumerate(𝑃.disjuncts)
+        if check(conjunct, X)
+            _reorder!(𝑃, i)
+            return true
+        end
+    end
+    return 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

@@ -0,0 +1,27 @@
+__precompile__()
+"""
+Module for defining and checking properties.
+"""
+module Properties
+
+using LazySets
+
+# ==============================
+# Property struct and evaluation
+# ==============================
+include("Property.jl")
+export Property,
+       check
+
+include("Conjunction.jl")
+include("Disjunction.jl")
+export Conjunction,
+       Disjunction
+
+include("BadStatesProperty.jl")
+export BadStatesProperty
+
+include("SafeStatesProperty.jl")
+export SafeStatesProperty
+
+end # module

src/Properties/Property.jl

@@ -0,0 +1,7 @@
+"""
+Abstract supertype of properties that can be checked.
+
+Every concrete subtype should provide the following function:
+  - `check(𝑃::Property, X::LazySet)::Bool`
+"""
+abstract type Property end

src/Properties/SafeStatesProperty.jl

@@ -0,0 +1,53 @@
+"""
+    SafeStatesProperty{N<:Real} <: Property
+
+Type that represents a safety property characterized by a set of safe states.
+The property is satisfied by a given set of states ``X`` if ``X`` is fully
+contained in the set of safe states.
+
+### Fields
+
+- `safe`    -- convex set representing the safe 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 safe states 𝑃:
+
+```math
+    X \\models 𝑃 \\iff X ⊆ 𝑃.\\texttt{safe}
+```
+"""
+mutable struct SafeStatesProperty{N<:Real} <: Property
+    safe::LazySet
+    witness::Vector{N}
+
+    SafeStatesProperty{N}(safe::LazySet) where {N<:Real} = new(safe, N[])
+end
+
+# type-less convenience constructor
+SafeStatesProperty(safe::LazySet{N}) where {N<:Real} = SafeStatesProperty{N}(safe)
+
+"""
+    check(𝑃::SafeStatesProperty, X::LazySet)::Bool
+
+Checks whether a convex set is contained in the set of safe states.
+
+### Input
+
+- `𝑃` -- safety property with safe states
+- `X` -- convex set
+
+### Output
+
+`true` iff the given set of states is a subset of the set of safe states.
+"""
+@inline function check(𝑃::SafeStatesProperty, X::LazySet)::Bool
+    is_subset, witness = ⊆(X, 𝑃.safe, true)
+    if !is_subset
+        # store violation witness
+        𝑃.witness = witness
+    end
+    return is_subset
+end

src/ReachSets/ContinuousPost/BFFPSV18/check_blocks.jl

@@ -36,7 +36,7 @@ function check_blocks(ϕ::SparseMatrixCSC{NUM, Int},
                        prop::Property
                        )::Int where {NUM}
     violation_index = 0
-    if !check_property(CartesianProductArray(Xhat0[blocks]), prop)
+    if !check(prop, CartesianProductArray(Xhat0[blocks]))
         if eager_checking
             return 1
         end
@@ -74,7 +74,7 @@ function check_blocks(ϕ::SparseMatrixCSC{NUM, Int},
             Xhatk[i] = (U == nothing ? Xhatk_bi : Xhatk_bi + Whatk[i])
         end
 
-        if !check_property(CartesianProductArray(Xhatk), prop)
+        if !check(prop, CartesianProductArray(Xhatk))
             if eager_checking
                 return k
             elseif violation_index == 0
@@ -113,7 +113,7 @@ function check_blocks(ϕ::AbstractMatrix{NUM},
                        prop::Property
                        )::Int where {NUM}
     violation_index = 0
-    if !check_property(CartesianProductArray(Xhat0[blocks]), prop)
+    if !check(prop, CartesianProductArray(Xhat0[blocks]))
         if eager_checking
             return 1
         end
@@ -153,7 +153,7 @@ function check_blocks(ϕ::AbstractMatrix{NUM},
             Xhatk[i] = MinkowskiSumArray(arr)
         end
 
-        if !check_property(CartesianProductArray(Xhatk), prop)
+        if !check(prop, CartesianProductArray(Xhatk))
             if eager_checking
                 return k
             elseif violation_index == 0
@@ -194,7 +194,7 @@ function check_blocks(ϕ::SparseMatrixExp{NUM},
                        prop::Property
                        )::Int where {NUM}
     violation_index = 0
-    if !check_property(CartesianProductArray(Xhat0[blocks]), prop)
+    if !check(prop, CartesianProductArray(Xhat0[blocks]))
         if eager_checking
             return 1
         end
@@ -237,7 +237,7 @@ function check_blocks(ϕ::SparseMatrixExp{NUM},
             end
         end
 
-        if !check_property(CartesianProductArray(Xhatk), prop)
+        if !check(prop, CartesianProductArray(Xhatk))
             if eager_checking
                 return k
             elseif violation_index == 0
@@ -269,7 +269,7 @@ function check_blocks(ϕ::SparseMatrixExp{NUM},
                        prop::Property
                        )::Int where {NUM}
     violation_index = 0
-    if !check_property(CartesianProductArray(Xhat0[blocks]), prop)
+    if !check(prop, CartesianProductArray(Xhat0[blocks]))
         if eager_checking
             return 1
         end
@@ -313,7 +313,7 @@ function check_blocks(ϕ::SparseMatrixExp{NUM},
             end
         end
 
-        if !check_property(CartesianProductArray(Xhatk), prop)
+        if !check(prop, CartesianProductArray(Xhatk))
             if eager_checking
                 return k
             elseif violation_index == 0

src/ReachSets/ContinuousPost/BFFPSV18/check_property.jl

@@ -1,4 +1,4 @@
-import LazySets.CacheMinkowskiSum
+using LazySets: CacheMinkowskiSum
 
 """
     check_property(S, property, options)
@@ -77,7 +77,7 @@ function check_property(S::IVP{<:AbstractDiscreteSystem},
         else
             Xhat0_mod = CartesianProductArray(Xhat0)
         end
-        return check_property(Xhat0_mod, property) ? 0 : 1
+        return check(property, Xhat0_mod) ? 0 : 1
     end
     push!(args, Xhat0)