Skip to content

Commit

Permalink
Merge pull request #692 from JuliaReach/property_check_inv
Browse files Browse the repository at this point in the history
Check the property after intersection reach_set with invariant
schillic authored Oct 4, 2019
2 parents fbbdc72 + f08db36 commit 5bd9bc8
Showing 1 changed file with 21 additions and 20 deletions.
41 changes: 21 additions & 20 deletions src/solve.jl
Original file line number Diff line number Diff line change
@@ -173,6 +173,26 @@ function solve!(system::InitialValueProblem{<:HybridSystem,
property_loc = property isa Dict ?
get(property, loc_id, nothing) :
property

# add the very first initial approximation
if passed_list != nothing &&
(!isassigned(passed_list, loc_id) || isempty(passed_list[loc_id]))
reach_set = reach_tube.Xk[1]
# TODO For lazy X0 the fixpoint check is likely to fail, so we
# currently ignore that. In general, we want to add an
# *underapproximation*, which we currently do not support.
X = set(reach_set)
if !(X isa CartesianProductArray) || !(array(X)[1] isa CH)
Xoa = overapproximate(X)
ti, tf = time_start(reach_set), time_end(reach_set)
passed_list[loc_id] = [ReachSet{LazySet{N}}(Xoa, ti, tf)]
end
end

# count_Rsets counts the number of new reach sets added to Rsets
count_Rsets = tube⋂inv!(opD, reach_tube.Xk, loc.X, Rsets,
[time_start(X0), time_end(X0)])

if property_loc != nothing
if opD isa DecomposedDiscretePost
temp_vars = opD.options[:temp_vars]
@@ -190,33 +210,14 @@ function solve!(system::InitialValueProblem{<:HybridSystem,
end
end
else
for (i, reach_set) in enumerate(reach_tube.Xk)
for (i, reach_set) in enumerate(Rsets[length(Rsets) - count_Rsets + 1 : end])
if !check(property_loc, set(reach_set))
return CheckSolution(false, i, options)
end
end
end
end

# add the very first initial approximation
if passed_list != nothing &&
(!isassigned(passed_list, loc_id) || isempty(passed_list[loc_id]))
reach_set = reach_tube.Xk[1]
# TODO For lazy X0 the fixpoint check is likely to fail, so we
# currently ignore that. In general, we want to add an
# *underapproximation*, which we currently do not support.
X = set(reach_set)
if !(X isa CartesianProductArray) || !(array(X)[1] isa CH)
Xoa = overapproximate(X)
ti, tf = time_start(reach_set), time_end(reach_set)
passed_list[loc_id] = [ReachSet{LazySet{N}}(Xoa, ti, tf)]
end
end

# count_Rsets counts the number of new reach sets added to Rsets
count_Rsets = tube⋂inv!(opD, reach_tube.Xk, loc.X, Rsets,
[time_start(X0), time_end(X0)])

if jumps == max_jumps
continue
end

0 comments on commit 5bd9bc8

Please sign in to comment.