Merge pull request #480 from JuliaReach/schillic/447

#473 - Checking different safety properties in different locations

src/Options/default_options.jl

@@ -13,7 +13,8 @@ Supported options:
 - `:verbosity`     -- controls logging output
 - `:logfile`       -- name of a log file
 - `:mode`          -- main analysis mode
-- `:property`      -- a safety property
+- `:property`      -- `nothing`, a safety property, or a mapping from a location
+                      to a safety property
 - `:T`             -- time horizon; alias `:time_horizon`
 - `:ε_proj`        -- error bound for the approximation of the states during
                       projection
@@ -91,7 +92,7 @@ function validate_solver_options_and_add_default_values!(options::Options)::Opti
                 error("No property has been defined.")
             end
         elseif key == :property
-            expected_type = Union{Property, Nothing}
+            expected_type = Union{Nothing, Property, Dict{Int, Property}}
         elseif key == :T
             expected_type = Float64
             domain_constraints = (v::Float64  ->  v > 0.)

src/solve.jl

@@ -139,6 +139,7 @@ function solve!(system::InitialValueProblem{<:HybridSystem,
     time_horizon = options[:T]
     max_jumps = options[:max_jumps]
     inout_map = nothing
+    property = options[:mode] == "check" ? options[:property] : nothing
 
     # waiting_list entries:
     # - (discrete) location
@@ -179,11 +180,24 @@ function solve!(system::InitialValueProblem{<:HybridSystem,
         options_copy = copy(options)
         options_copy.dict[:T] = time_horizon - X0.t_start
         options_copy.dict[:project_reachset] = false
+        if property != nothing
+            # TODO temporary hack, to be resolved in #447
+            options_copy[:mode] = "reach"
+        end
         reach_tube = solve!(ContinuousSystem(loc.A, X0.X, loc.U),
                             options_copy,
                             op=opC,
                             invariant=source_invariant)
         inout_map = reach_tube.options[:inout_map]  # TODO temporary hack
+        if property != nothing
+            # get the property for the current location
+            property_loc = property isa Dict ? property[loc] : property
+            for (i, reach_set) in enumerate(reach_tube.Xk)
+                if !check_property(reach_set.X, property_loc)
+                    return CheckSolution(false, i, options)
+                end
+            end
+        end
 
         # add the very first initial approximation
         if passed_list != nothing &&
@@ -212,6 +226,9 @@ function solve!(system::InitialValueProblem{<:HybridSystem,
         post(opD, HS, waiting_list, passed_list, loc_id, Rsets, count_Rsets,
              jumps, options)
     end
+    if options[:mode] == "check"
+        return CheckSolution(true, -1, options)
+    end
 
     # Projection
     options[:inout_map] = inout_map