Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Check the property after intersection reach_set with invariant #692

Merged
merged 2 commits into from
Oct 4, 2019
Merged

Check the property after intersection reach_set with invariant #692

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f78912d
Check the property after intersection reach_set with invariant
kpotomkin Oct 4, 2019
f08db36
remove extra spacing
kpotomkin Oct 4, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
41 changes: 21 additions & 20 deletions src/solve.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand All @@ -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
Expand Down