Add in sol

[mforets]

No description provided.

[goretkin]

From doing ?in

  in(item, collection) -> Bool
  ∈(item, collection) -> Bool
  ∋(collection, item) -> Bool

  Determine whether an item is in the given collection, in the sense that it is == to one of the values generated by iterating over the collection. Returns a Bool value,
  except if item is missing or collection contains missing but not item, in which case missing is returned (three-valued logic
  (https://en.wikipedia.org/wiki/Three-valued_logic), matching the behavior of any and ==).

  Some collections follow a slightly different definition. For example, Sets check whether the item isequal to one of the elements. Dicts look for key=>value pairs, and the
  key is compared using isequal. To test for the presence of a key in a dictionary, use haskey or k in keys(dict). For these collections, the result is always a Bool and
  never missing.

  To determine whether an item is not in a given collection, see :∉. You may also negate the in by doing !(a in b) which is logically similar to "not in".

  When broadcasting with in.(items, collection) or items .∈ collection, both item and collection are broadcasted over, which is often not what is intended. For example, if
  both arguments are vectors (and the dimensions match), the result is a vector indicating whether each value in collection items is in the value at the corresponding
  position in collection. To get a vector indicating whether each value in items is in collection, wrap collection in a tuple or a Ref like this: in.(items, Ref(collection))
  or items .∈ Ref(collection).

The point about == or isequal is besides the point here, in my opinion, but just to clarify:

julia> NaN ∈ [1, NaN]
false

julia> NaN ∈ Set([1, NaN])
true

To help explain, I'll define

my_in(element, collection) = any(==(element),  collection)

which perhaps is more clear as

my_in(element, collection) = any( element == x for x in collection)

and "consistency", and following the documentation of in, means that one of two should be the case:

1. my_in errors
2. my_in returns the same answer as in

If the definitions at

ReachabilityAnalysis.jl/src/Flowpipes/solutions.jl

Lines 88 to 99 in b877a7d

	# iteration and indexing iterator interface
	array(sol::ReachSolution) = array(sol.F)
	Base.iterate(sol::ReachSolution) = iterate(sol.F)
	Base.iterate(sol::ReachSolution, state) = iterate(sol.F, state)
	Base.length(sol::ReachSolution) = length(sol.F)
	Base.first(sol::ReachSolution) = first(sol.F)
	Base.last(sol::ReachSolution) = last(sol.F)
	Base.firstindex(sol::ReachSolution) = 1
	Base.lastindex(sol::ReachSolution) = length(sol.F)
	Base.getindex(sol::ReachSolution, i::Int) = getindex(sol.F, i)
	Base.getindex(sol::ReachSolution, i::Number) = getindex(sol.F, i)
	Base.getindex(sol::ReachSolution, I::AbstractVector) = getindex(sol.F, I)

remain, then there will be an inconsistency. my_in will not error, and will return a different answer from in.

Note that a type does not need to define iterate in order to define in, and that is useful for uncountable sets. That's the case for e.g.

julia> in([0.0, 0.0], Hyperrectangle([0.0, 0.0], [1.0, 1.0]))
true

julia> my_in([0.0, 0.0], Hyperrectangle([0.0, 0.0], [1.0, 1.0]))
ERROR: MethodError: no method matching iterate(::Hyperrectangle{Float64,Array{Float64,1},Array{Float64,1}})

There are some tricky cases where this consistency is broken for some other good. For example, for whatever reason (sometime I think it's good, sometimes I think it's the absolute worst) <:Number in julia is iterable and indexable:

julia> collect(3)
0-dimensional Array{Int64,0}:
3

julia> 3 in 3
true

julia> length(3)
1

that itself doesn't pose a problem since

julia> my_in(3, 3)
true

But Interval of IntervalArithmetic.jl wants to both be set and a <:Number:

julia> supertypes(typeof(Interval(0,1)))
(Interval{Float64}, AbstractInterval{Float64}, Real, Number, Any)

and so

julia> in(0.5, Interval(0, 1))
true

julia> my_in(0.5, Interval(0, 1))
false

Since the type in question here has no reason to be <:Number, then this inconsistency can easily be avoided.

[mforets]

There are some tricky cases where this consistency is broken for some other good.

indeed, i acknowledge that implementing the iterator interface AND at the same time working with dense sets of R^n is prone to mistakes, and there was one fixed in this PR, because the in fallback didn't make sense.

on the other hand, there are many benefits of X[k] where X is a flowpipe (or a solution), as it is natural in math to speak of the k-th reach-set Xk of a sequence.

(conversation continued on gitter)

[goretkin]

Sorry if I am belaboring the point. I should probably open a separate issue to discuss this.

Code like

ReachabilityAnalysis.jl/src/Flowpipes/flowpipes.jl

Line 466 in cd24f50

Base.:⊆(F::Flowpipe, X::LazySet) = all(R ⊆ X for R in F)

and

ReachabilityAnalysis.jl/src/Flowpipes/flowpipes.jl

Lines 478 to 485 in cd24f50

	# membership test
	function ∈(x::AbstractVector{N}, fp::Flowpipe{N, <:AbstractLazyReachSet{N}}) where {N}
	return any(R -> x ∈ set(R), array(fp))
	end
	function ∈(x::AbstractVector{N}, fp::VT) where {N, RT<:AbstractLazyReachSet{N}, VT<:AbstractVector{RT}}
	return any(R -> x ∈ set(R), fp)
	end

makes me especially nervous to have a definition of iterate that is not consistent with in. Not only does in in that context means iteration (even though syntactically, the in or ∈ in the context of a for expression and the function Base.in are unrelated: https://github.com/JuliaLang/julia/blob/4b739e711a7241f48ec0525e97c44cc870a9af99/src/julia-parser.scm#L1696-L1717), but also because it's where the iteration meaning and the geometric meaning are used together, and can easily cause confusion.

The line

Base.:⊆(F::Flowpipe, X::LazySet) = all(R ⊆ X for R in F)

reads to me like

F is contained in X iff each thing in F is contained in X

or

but that is not what it really means.

[mforets]

Here ⊆(F::Flowpipe, X::LazySet) means that F is contained in X, and the implementation relies on R ⊆ X which uses dispatch on a reach-set and a set. Pleas note that there is a typo in the lef-hand side of the LaTeX equation of your comment.

I don't see an issue with this definition. We should document uses of ∈ and ⊆ in the library though, such docs are still missing.

[goretkin]

Thanks for catching the typo. Yeah, there is nothing incorrect about the code, sorry if I communicated otherwise. It's the punning on "in" that occurs in the same line of code that is a conceptual issue, which can be more easily seen in the [corrected] latex.

…

On Thu, Nov 26, 2020, 6:36 AM Marcelo Forets ***@***.***> wrote: Here ⊆(F::Flowpipe, X::LazySet) means that F is contained in X, and the implementation relies on R ⊆ X which uses dispatch on a reach-set and a set. Pleas note that there is a typo in the lef-hand side of the LaTeX equation of your comment. I don't see an issue with this definition. We should document uses of ∈ and ⊆ in the library though, that is still missing. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#373 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAEN3M56TMSP3UNDYTLZNM3SRY4UZANCNFSM4UBLTHMA> .

[mforets]

yes, indeed R ⊆ X for R in F is just iterating over F. to me it comes natural as i've seen it so many times, but i understand your point. if it helps, note that in the source code i always use in for iteration and ∈ for membership checks.