#264 - Merge Properties module into ReachSets

src/Properties/check_blocks.jl → src/ReachSets/Properties/check_blocks.jl

@@ -23,17 +23,6 @@ OUTPUT:
 The first time index where the property is violated, and 0 if the property is satisfied.
 =#
 
-# helper functions
-@inline proj(bi::UnitRange{Int}, n::Int) =
-         sparse(1:length(bi), bi, ones(length(bi)), length(bi), n)
-@inline proj(bi::Int, n::Int) = sparse([1], [bi], ones(1), 1, n)
-@inline row(ϕpowerk::AbstractMatrix, bi::UnitRange{Int}) = ϕpowerk[bi, :]
-@inline row(ϕpowerk::AbstractMatrix, bi::Int) = ϕpowerk[[bi], :]
-@inline row(ϕpowerk::SparseMatrixExp, bi::UnitRange{Int}) = get_rows(ϕpowerk, bi)
-@inline row(ϕpowerk::SparseMatrixExp, bi::Int) = Matrix(get_row(ϕpowerk, bi))
-@inline block(ϕpowerk_πbi::AbstractMatrix, bj::UnitRange{Int}) = ϕpowerk_πbi[:, bj]
-@inline block(ϕpowerk_πbi::AbstractMatrix, bj::Int) = ϕpowerk_πbi[:, [bj]]
-
 # sparse
 function check_blocks(ϕ::SparseMatrixCSC{NUM, Int},
                        Xhat0::Vector{<:LazySet{NUM}},

src/Properties/check_property.jl → src/ReachSets/Properties/check_property.jl

@@ -13,7 +13,7 @@ Interface to property checking algorithms for an LTI system.
 ### Notes
 
 A dictionary with available algorithms is available via
-`Properties.available_algorithms`.
+`available_algorithms_check`.
 """
 function check_property(S::IVP{<:AbstractDiscreteSystem},
                         options::Options
@@ -164,7 +164,7 @@ function check_property(S::IVP{<:AbstractDiscreteSystem},
     # call the adequate function with the given arguments list
     info("- Computing successors")
     tic()
-    answer = available_algorithms[algorithm_backend]["func"](args...)
+    answer = available_algorithms_check[algorithm_backend]["func"](args...)
     tocc()
 
     # return the result

src/ReachSets/ReachSets.jl

@@ -107,6 +107,53 @@ include("inout_map_reach.jl")
 
 export inout_map_reach
 
+# ==============================
+# Property struct and evaluation
+# ==============================
+include("Properties/Property.jl")
+export Property,
+       inout_map_property
+
+include("Properties/LinearConstraintProperty.jl")
+export LinearConstraintProperty,
+       Clause
+
+include("Properties/IntersectionProperty.jl")
+export IntersectionProperty
+
+include("Properties/SubsetProperty.jl")
+export SubsetProperty
+
+# ==========================
+# Property checking results
+# ==========================
+include("Properties/CheckSolution.jl")
+
+export CheckSolution
+
+# =============================
+# Property checking algorithms
+# =============================
+
+# dictionary of registered algorithms
+available_algorithms_check = Dict{String, Dict{String, Any}}()
+
+# "explicit" backends
+include("Properties/check_blocks.jl")
+push!(available_algorithms_check, "explicit_blocks"=>Dict("func"=>check_blocks,
+                                                    "is_explicit"=>true))
+
+include("Properties/check_property.jl")
+
+export available_algorithms_check,
+       check_property
+
+# ====================================================
+# Algorithms to find a threshold for property checking
+# ====================================================
+include("Properties/tune.jl")
+export tune_δ
+
 # =====================
 # Reachability results
 # =====================

src/Reachability.jl

@@ -11,16 +11,14 @@ include("logging.jl")
 include("Utils/Utils.jl")
 include("options.jl")
 include("ReachSets/ReachSets.jl")
-include("Properties/Properties.jl")
 include("Transformations/Transformations.jl")
 
 @reexport using Reachability.Utils
 
 using Reachability.ReachSets,
-      Reachability.Properties,
       Reachability.Transformations
 
-export Properties, LinearConstraintProperty, Clause,
+export LinearConstraintProperty, Clause,
        IntersectionProperty,
        SubsetProperty,
        Transformations

test/Properties/unit_tune.jl

@@ -13,4 +13,4 @@ algorithm(N, δ) = solve(S, :mode => "check", :partition=>[1:2, 3:4],
                            :T => time_horizon,
                            :property=>LinearConstraintProperty([24., 0., 1, 0],  375.)).satisfied
 
-Properties.tune_δ(algorithm, time_horizon, precision, initial_δ)
+Reachability.tune_δ(algorithm, time_horizon, precision, initial_δ)