From 3345cd81d5abb1469e660759332f696eed08bfd5 Mon Sep 17 00:00:00 2001 From: schillic Date: Wed, 20 Feb 2019 21:01:42 +0100 Subject: [PATCH 1/2] allow dict for property --- src/Options/default_options.jl | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Options/default_options.jl b/src/Options/default_options.jl index 35a84f64..d536debb 100644 --- a/src/Options/default_options.jl +++ b/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.) From 89bcb6fe9ec5177cd901c8092e8a990e122f46df Mon Sep 17 00:00:00 2001 From: schillic Date: Thu, 21 Feb 2019 11:22:18 +0100 Subject: [PATCH 2/2] simple property checking in hybrid setting --- src/solve.jl | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/solve.jl b/src/solve.jl index dd5c2771..bb3ae276 100644 --- a/src/solve.jl +++ b/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