rename check_property -> check

src/Properties/IntersectionProperty.jl

@@ -1,14 +1,14 @@
 """
     IntersectionProperty{N<:Real} <: Property
 
-Type that represents a safety property characterized with a set of bad states.
-A safety property is satisfied by a given set of states if the intersection with
-the set of bad states is empty.
+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)
+- `bad`     -- convex set representing the bad states
+- `witness` -- witness point (empty vector if not set)
 """
 mutable struct IntersectionProperty{N<:Real} <: Property
     bad::LazySet
@@ -18,28 +18,28 @@ mutable struct IntersectionProperty{N<:Real} <: Property
 end
 
 # type-less convenience constructor
-IntersectionProperty(bad::LazySet{N}) where {N} = IntersectionProperty{N}(bad)
+IntersectionProperty(bad::LazySet{N}) where {N<:Real} =
+    IntersectionProperty{N}(bad)
 
 """
-    check_property(set::LazySet, prop::IntersectionProperty)::Bool
+    check(prop::IntersectionProperty, set::LazySet)::Bool
 
-Checks whether a convex set satisfies a safety property.
+Checks whether a convex set is disjoint from the set of bad states.
 
 ### Input
 
-- ``set``  -- convex set
-- ``prop`` -- safety property with bad states
+- `set`  -- convex set
+- `prop` -- safety property with bad states
 
 ### Output
 
-`true` iff the safety property is satisfied for the given set of states.
-This is the case iff the set of states does not intersect with the bad states.
+`true` iff the given set of states does not intersect with the bad states.
 """
-@inline function check_property(set::LazySet, prop::IntersectionProperty)::Bool
-    nonempty_intersection, witness = is_intersection_empty(set, prop.bad, true)
-    if nonempty_intersection
+@inline function check(prop::IntersectionProperty, set::LazySet)::Bool
+    empty_intersection, witness = is_intersection_empty(set, prop.bad, true)
+    if !empty_intersection
         # store violation witness
         prop.witness = witness
     end
-    return !nonempty_intersection
+    return empty_intersection
 end

src/Properties/LinearConstraintProperty.jl

@@ -5,7 +5,7 @@ Type that represents a disjunction of linear constraints.
 
 ### Fields
 
-- ``atoms`` -- a vector of linear constraints
+- `atoms` -- a vector of linear constraints
 """
 struct Clause{N<:Real}
     atoms::AbstractVector{LinearConstraint{N}}
@@ -23,7 +23,7 @@ disjunctions of linear constraints.
 
 ### Fields
 
-- ``clauses`` -- a vector of `Clause` objects
+- `clauses` -- a vector of `Clause` objects
 """
 struct LinearConstraintProperty{N<:Real} <: Property
     clauses::AbstractVector{Clause{N}}
@@ -39,21 +39,20 @@ LinearConstraintProperty(linComb::AbstractVector{N}, bound::N) where {N<:Real} =
     LinearConstraintProperty{N}([Clause(LinearConstraint{N}(linComb, bound))])
 
 """
-    check_property(set::LazySet, prop::LinearConstraintProperty)::Bool
+    check(prop::LinearConstraintProperty, set::LazySet)::Bool
 
 Checks whether a convex set satisfies a property of linear constraints.
 
 ### Input
 
-- ``set``  -- convex set
-- ``prop`` -- property of linear constraints
+- `set`  -- convex set
+- `prop` -- property of linear constraints
 
 ### Output
 
 `true` iff the convex set satisfies the property of linear constraints.
 """
-@inline function check_property(set::LazySet, prop::LinearConstraintProperty
-                               )::Bool
+@inline function check(prop::LinearConstraintProperty, set::LazySet)::Bool
     @assert (length(prop.clauses) > 0) "empty properties are not allowed"
     for clause in prop.clauses
         @assert (length(clause.atoms) > 0) "empty clauses are not allowed"

src/Properties/Properties.jl

@@ -11,7 +11,7 @@ using LazySets
 # ==============================
 include("Property.jl")
 export Property,
-       check_property
+       check
 
 include("LinearConstraintProperty.jl")
 export LinearConstraintProperty,

src/Properties/Property.jl

@@ -1,9 +1,7 @@
 """
 Abstract supertype of properties that can be checked.
 
-Every concrete subtype should provide the following functions:
-  - `inout_map_property(::Property, ::AbstractVector{<:AbstractVector{Int}},
-                        ::AbstractVector{Int}, ::Int)::Property`
-  - `check_property(::LazySet, ::Property)::Bool`
+Every concrete subtype should provide the following function:
+  - `check(::Property, args...)::Bool`
 """
 abstract type Property end

src/Properties/SubsetProperty.jl

@@ -1,14 +1,14 @@
 """
     SubsetProperty{N<:Real} <: Property
 
-Type that represents a safety property characterized with a set of safe states.
-A safety property is satisfied by a given set of states if the set of states is
-fully contained in the set of safe states.
+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)
+- `safe`    -- convex set representing the safe states
+- `witness` -- witness point (empty vector if not set)
 """
 mutable struct SubsetProperty{N<:Real} <: Property
     safe::LazySet
@@ -18,24 +18,23 @@ mutable struct SubsetProperty{N<:Real} <: Property
 end
 
 # type-less convenience constructor
-SubsetProperty(safe::LazySet{N}) where {N} = SubsetProperty{N}(safe)
+SubsetProperty(safe::LazySet{N}) where {N<:Real} = SubsetProperty{N}(safe)
 
 """
-    check_property(set::LazySet, prop::SubsetProperty)::Bool
+    check(prop::SubsetProperty, set::LazySet)::Bool
 
-Checks whether a convex set satisfies a safety property.
+Checks whether a convex set is contained in the set of safe states.
 
 ### Input
 
-- ``set``  -- convex set
-- ``prop`` -- safety property with safe states
+- `set`  -- convex set
+- `prop` -- safety property with safe states
 
 ### Output
 
-`true` iff the safety property is satisfied for the given set of states.
-This is the case iff the set of states is a subset of the safe states.
+`true` iff the given set of states is a subset of the set of safe states.
 """
-@inline function check_property(set::LazySet, prop::SubsetProperty)::Bool
+@inline function check(prop::SubsetProperty, set::LazySet)::Bool
     is_subset, witness = ⊆(set, prop.safe, true)
     if !is_subset
         # store violation witness

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,5 +1,4 @@
 using LazySets: CacheMinkowskiSum
-import ..Properties: check_property
 
 """
     check_property(S, property, options)
@@ -78,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)