Reachability.jl icon indicating copy to clipboard operation
Reachability.jl copied to clipboard

Check whether use_precise_ρ still works

Open schillic opened this issue 6 years ago • 3 comments

schillic avatar Oct 04 '19 12:10 schillic

@schillic @mforets It doesn't work and ρ_helper always takes default implementation of the use_precise_ρ. Any suggestions on why it happens?

kpotomkin avatar Dec 03 '19 18:12 kpotomkin

It would be helpful to have an example (model, branches, etc.) for debugging.

schillic avatar Dec 06 '19 16:12 schillic

This is the default implementation:

https://github.com/JuliaReach/Reachability.jl/blob/156e5f5a3fb38176de897625044dc3574fedfee5/src/ReachSets/DiscretePost/DiscretePost.jl#L100-L104

We override this policy for LazyDiscretePost:

https://github.com/JuliaReach/Reachability.jl/blob/156e5f5a3fb38176de897625044dc3574fedfee5/src/ReachSets/DiscretePost/LazyDiscretePost.jl#L203-L214

So the question is whether you use LazyDiscretePost or a different operator. What is your expected result?

schillic avatar Dec 10 '19 09:12 schillic