:combine_invariant_guard option takes intersection with invariant twice - Githubissues

JuliaReach / Reachability.jl

Reachability and Safety of Nondeterministic Dynamical Systems

MIT License

50 stars 4 forks source link

:combine_invariant_guard option takes intersection with invariant twice #557

Closed schillic closed 5 years ago

schillic commented 5 years ago

~The LazyDiscretePost operator offers the option :combine_invariant_guard, but we take the (lazy or concrete) intersection with the invariant in an earlier step independent of this option.~ Sorry, everything is correct here. But the implementation is really subtle... https://github.com/JuliaReach/Reachability.jl/blob/3cc0b1aa599b2f93a3a4d06df5db528f47c73f83/src/ReachSets/DiscretePost/LazyDiscretePost.jl#L152-L156