Skip to content

Commit

Permalink
make Reachability result always return reach set
Browse files Browse the repository at this point in the history
  • Loading branch information
tomerarnon committed Jul 28, 2020
1 parent 3eabff8 commit 1a3c300
Showing 1 changed file with 3 additions and 8 deletions.
11 changes: 3 additions & 8 deletions src/reachability/utils/reachability.jl
Expand Up @@ -18,20 +18,15 @@ function check_inclusion(reach::Vector{<:LazySet}, output)
for poly in reach
issubset(poly, output) || return ReachabilityResult(:violated, reach)
end
return ReachabilityResult(:holds, similar(reach, 0))
return ReachabilityResult(:holds, reach)
end

function check_inclusion(reach::P, output) where P<:LazySet
if issubset(reach, output)
return ReachabilityResult(:holds, P[])
end
return ReachabilityResult(:violated, [reach])
return ReachabilityResult(issubset(reach, output) ? :holds : :violated, [reach])
end

# return a vector so that append! is consistent with the relu forward_partition
forward_partition(act::Id, input::AbstractPolytope) = [input]

forward_partition(act::Id, input::Zonotope) = input
forward_partition(act::Id, input) = [input]

function forward_partition(act::ReLU, input::HPolytope)
n = dim(input)
Expand Down

0 comments on commit 1a3c300

Please sign in to comment.