Combine ai2 #133
Combine ai2 #133
Conversation
src/reachability/ai2.jl
Outdated
| return overapproximate(Rectification(Ẑ), T) | ||
| end | ||
|
|
||
|
|
||
| # extend lazysets convex_hull to a vector of polytopes | ||
| function LazySets.convex_hull(sets::Vector{<:AbstractPolytope}; backend = CDDLib.Library()) |
There was a problem hiding this comment.
In LazySets there is a function that does this: JuliaReach/LazySets.jl#2215
There was a problem hiding this comment.
Not quite. It returns a vector of vertices and we want a Polytope (we could do VPolytope(...) at the end though). Also, in hrep, I think it's more efficient not to go to vrep, no?
There was a problem hiding this comment.
The problem here is that you are doing a convex_hull every loop, while that implementation only does once, so, if there are more than two polytopes, I think that it will be faster even after the conversion, and it will scale much better with more polytopes and dimensions.
There was a problem hiding this comment.
Hmm, this could be. I didn't think so since I assumed convex_hull of two polytopes of the same type does not convert, and therefore it should be more efficient. Since the code in LazySets defers to Polyhedra, do you know if this is the case or not?
There was a problem hiding this comment.
The function used is removehredundancy() here, so it does not convert to v-rep.
I did a benchmark with two polygons:
julia> @btime convert(HPolytope, VPolytope(convex_hull(UnionSetArray([$H, $H]))));
331.000 ns (4620 allocations: 310.05 KiB)
julia> @btime convex_hull($H, $H);
1.072 ms (14202 allocations: 864.63 KiB)So it seems to me that the implementation in LazySets is faster even in 2D and two polytopes
There was a problem hiding this comment.
Computing Pch in Polyhedra requires vrep I think. The Polyhedra documentation suggests it is only possible in vrep: https://juliapolyhedra.github.io/Polyhedra.jl/latest/utilities/#Polyhedra.convexhull
Therefore your method is better after all (probably much better)
There was a problem hiding this comment.
By the way, I have recently noticed printouts from the LP solver used by LazySets (or lower in the stack) which were not there in prior package versions. Do you know which issue/s or update/s these new messages are related to? An example is:
julia> convex_hull(UnionSetArray([hp, hp]))
glp_simplex: unable to recover undefined or non-optimal solution
glp_simplex: unable to recover undefined or non-optimal solution
glp_simplex: unable to recover undefined or non-optimal solution
glp_simplex: unable to recover undefined or non-optimal solution
glp_simplex: unable to recover undefined or non-optimal solution
glp_simplex: unable to recover undefined or non-optimal solution
3-element Array{Array{Float64,1},1}:
[-0.36626701868929534, 1.1382211150524333, -0.6787710912863433]
[0.36968831822766857, -0.7100424633428055, -0.1920207505884401]
[-1.9245657296871925, 0.42914282672330284, -0.7531344058289536]There was a problem hiding this comment.
I don't know where they originate but there are issues that mentions it(JuliaReach/LazySets.jl#2278 (comment) and JuliaReach/LazySets.jl#861 (comment))
|
Hmm... It seems tests are failing due to Box or Ai2z being too overapproximate (returning :violated for :holds). But in your PRs the tests passed just fine. Do you see anywhere where I made a mistake @SebastianGuadalupe? |
I run the test locally and it doesn't seems to be a problem of being too overapproximate, the resulting set does not include the expected result, my guess is that the problem is in the affine map? |
I believe you also used affine_map in Ai2z, no? In the travis tests, that is the first failure case encountered. Very strange indeed! |
|
I think I found the issue... I unwittingly removed definitions for identity activation. I'll check on my end if that's it. |
|
Yes, that is the error, I just found it too |
|
Great to see |
|
Indeed, I consider that to be a design mistake. I figured I might as well fix it here than in another PR 🤷♂️ |
@SebastianGuadalupe here I try to consolidate the 3 methods of Ai2 into one Ai2{T}