search

JuliaReach / Reachability.jl

Reachability and Safety of Nondeterministic Dynamical Systems
MIT License
50 stars 4 forks source link

Check whether use_precise_ρ still works #693

Open schillic opened 4 years ago

kpotomkin commented 4 years ago

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

schillic commented 4 years ago

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

schillic commented 4 years ago

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?