JuliaReach · schillic · Feb 24, 2019 · Feb 24, 2019 · Feb 24, 2019
diff --git a/...chSets/Properties/IntersectionProperty.jl → src/Properties/IntersectionProperty.jl b/...chSets/Properties/IntersectionProperty.jl → src/Properties/IntersectionProperty.jl
diff --git a/...ts/Properties/LinearConstraintProperty.jl → src/Properties/LinearConstraintProperty.jl b/...ts/Properties/LinearConstraintProperty.jl → src/Properties/LinearConstraintProperty.jl
diff --git a/src/Properties/Properties.jl b/src/Properties/Properties.jl
@@ -0,0 +1,26 @@
+__precompile__()
+"""
+Module for defining and checking properties.
+"""
+module Properties
+
+using LazySets
+
+# ==============================
+# Property struct and evaluation
+# ==============================
+include("Property.jl")
+export Property,
+       check_property
+
+include("LinearConstraintProperty.jl")
+export LinearConstraintProperty,
+       Clause
+
+include("IntersectionProperty.jl")
+export IntersectionProperty
+
+include("SubsetProperty.jl")
+export SubsetProperty
+
+end # module
diff --git a/src/ReachSets/Properties/Property.jl → src/Properties/Property.jl b/src/ReachSets/Properties/Property.jl → src/Properties/Property.jl
diff --git a/src/ReachSets/Properties/SubsetProperty.jl → src/Properties/SubsetProperty.jl b/src/ReachSets/Properties/SubsetProperty.jl → src/Properties/SubsetProperty.jl
diff --git a/src/ReachSets/Properties/CheckSolution.jl → src/ReachSets/CheckSolution.jl b/src/ReachSets/Properties/CheckSolution.jl → src/ReachSets/CheckSolution.jl
diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/check_property.jl b/src/ReachSets/ContinuousPost/BFFPSV18/check_property.jl
@@ -1,4 +1,5 @@
-import LazySets.CacheMinkowskiSum
+using LazySets: CacheMinkowskiSum
+import ..Properties: check_property
 
 """
     check_property(S, property, options)

diff --git a/src/ReachSets/ReachSets.jl b/src/ReachSets/ReachSets.jl
@@ -80,9 +80,9 @@ AUTHORS:
 """
 module ReachSets
 
-using ..Utils
-using LazySets, MathematicalSystems, HybridSystems
-using Expokit, Optim, ProgressMeter
+using ..Utils, ..Properties
+using LazySets, MathematicalSystems, HybridSystems, Expokit, Optim,
+      ProgressMeter
 
 # fix namespace conflicts with MathematicalSystems
 using LazySets: LinearMap
@@ -107,27 +107,10 @@ include("discretize.jl")
 
 export discretize
 
-# ==============================
-# 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")
+include("CheckSolution.jl")
 
 export CheckSolution
 
@@ -153,7 +136,7 @@ export available_algorithms_check,
 # ====================================================
 # Algorithms to find a threshold for property checking
 # ====================================================
-include("Properties/tune.jl")
+include("tune.jl")
 export tune_δ
 
 # =====================

diff --git a/src/ReachSets/Properties/tune.jl → src/ReachSets/tune.jl b/src/ReachSets/Properties/tune.jl → src/ReachSets/tune.jl
diff --git a/src/Reachability.jl b/src/Reachability.jl
@@ -16,11 +16,13 @@ include("Utils/Utils.jl")
 include("Options/dictionary.jl")
 include("Options/validation.jl")
 include("Options/default_options.jl")
+include("Properties/Properties.jl")
 include("ReachSets/ReachSets.jl")
 include("Transformations/Transformations.jl")
 
 @reexport using Reachability.Utils,
                 Reachability.ReachSets,
+                Reachability.Properties,
                 Reachability.Transformations
 
 export project,

diff --git a/test/Properties/unit_tune.jl b/test/Properties/unit_tune.jl
@@ -1,4 +1,4 @@
-using Reachability.ReachSets: BFFPSV18
+using Reachability.ReachSets: tune_δ
 
 #===== Projectile model =====
 We test the line plot!(x->x, x->-24*x+375, 0., 50., line=2., color="red", linestyle=:solid, legend=:none)
@@ -17,4 +17,4 @@ algorithm(N, δ) =
           op=BFFPSV18(:δ => δ, :vars => [1, 3], :partition=>[1:2, 3:4])
          ).satisfied
 
-Reachability.tune_δ(algorithm, time_horizon, prec, initial_δ)
+tune_δ(algorithm, time_horizon, prec, initial_δ)
diff --git a/test/ReachSets/unit_discretization.jl b/test/ReachSets/unit_discretization.jl
@@ -1,5 +1,3 @@
-import Reachability.ReachSets.discretize
-
 let # preventing global scope
     # ===================================================================
     # Discretization of a continuous-time system without input (ZeroSet)

diff --git a/test/Reachability/solve_continuous.jl b/test/Reachability/solve_continuous.jl
@@ -1,9 +1,6 @@
 # ===============================
 # Test minimal (default) options
 # ===============================
-using Reachability, MathematicalSystems
-using Reachability.ReachSets: BFFPSV18
-using LinearAlgebra, SparseArrays
 
 # linear ODE: x' = Ax
 A = [ 0.0509836  0.168159  0.95246   0.33644

diff --git a/test/Systems/alltests.jl b/test/Systems/alltests.jl
@@ -1,4 +1,2 @@
-using MathematicalSystems
-
 @time @testset "Systems.NonDeterministicInput" begin include("unit_NonDeterministicInput.jl") end
 @time @testset "Systems.System" begin include("unit_System.jl") end
diff --git a/test/runtests.jl b/test/runtests.jl
@@ -1,5 +1,6 @@
 #!/usr/bin/env julia
-using LazySets, Reachability, MathematicalSystems
+using LazySets, Reachability, MathematicalSystems,
+      LinearAlgebra, SparseArrays
 
 # fix namespace conflicts with MathematicalSystems
 import LazySets.LinearMap