Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • Jun 22 08:53

    schillic on gh-pages

    build based on 6c26d09 (compare)

  • Jun 22 08:38

    schillic on master

    Update CI-status badge (compare)

  • Jun 21 16:29

    mforets on gh-pages

    build based on 6c729af (compare)

  • Jun 21 16:25

    mforets on gh-pages

    build based on bb98ff2 (compare)

  • Jun 21 16:04

    github-actions[bot] on v0.14.17

    (compare)

  • Jun 21 16:02
    JuliaTagBot commented #376
  • Jun 21 15:46

    github-actions[bot] on gh-pages

    delete history (compare)

  • Jun 21 15:46
    JuliaRegistrator commented #111
  • Jun 21 15:46
    mforets commented #111
  • Jun 21 15:45

    mforets on master

    Update Project.toml (compare)

  • Jun 21 15:45

    mforets on common_solve

    (compare)

  • Jun 21 15:45

    mforets on master

    use common solve Merge pull request #522 from Ju… (compare)

  • Jun 21 15:45
    mforets closed #522
  • Jun 21 15:45
    mforets closed #417
  • Jun 21 14:49

    mforets on gh-pages

    build based on 7758751 (compare)

  • Jun 21 14:21

    schillic on gh-pages

    build based on 410bdbb (compare)

  • Jun 21 14:06
    schillic updated the wiki
  • Jun 21 14:05
    mforets opened #522
  • Jun 21 14:03

    schillic on 2745

    (compare)

  • Jun 21 14:03

    schillic on master

    complement check for half-spaces conversion from HPolyhedron to … ishyperplanar function and 3 more (compare)

that method is used to overapproximate the intersection between an n-ary cartesian product (.. of any array of lazysets, it could be made of sets or operation or both), and a polyhedron, and the output should be an n-ary cartesian product
also, having sets to be on the same footing as lazy operations (in the sense that both subtype LazySet) has turned out to be extremely useful
Marcelo Forets
@mforets
here is one case where @fix would be nice:
julia> using LazySets, SparseArrays, Expokit

julia> A = sprandn(1000, 1000, 0.1); X = rand(Hyperrectangle, dim=1000);

julia> typeof(A * X)
LinearMap{Float64,Hyperrectangle{Float64,Array{Float64,1},Array{Float64,1}},Float64,SparseMatrixCSC{Float64,Int64}}

julia> typeof(exp(Matrix(A)) * X) # computes exp(A) eagerly
LinearMap{Float64,Hyperrectangle{Float64,Array{Float64,1},Array{Float64,1}},Float64,Array{Float64,2}}

julia> typeof(SparseMatrixExp(A) * X)  # lazy matrix exponential on sets
ExponentialMap{Float64,Hyperrectangle{Float64,Array{Float64,1},Array{Float64,1}}}

julia> @fix exp(A) * X # should have the same effect
Marcelo Forets
@mforets
This is even more convenient for cases with several terms eg. inv(A)^2 * (exp(A) - I) * X
then the idea is to dispatch on the support function of that beast; it works by composing the support function rule of every lazy operator
Gustavo Goretkin
@goretkin

what i don't see is.. if the approach is composable? one of the key advantages of using lazy set types is that we can dispatch on a composition of operations, for example

If I understand what you mean about composing, then it's something I'm trying to figure out now. There's a PR that gives one solution. And I wrote a small book (:-/) about it with a geometric set example here: https://github.com/goretkin/FixArgs.jl/issues/16#issuecomment-738457696 . In summary: a "ring" (annulus) is a setdiff of two Discs. In LazySets.jl you would probably introduce a LazyDiff struct.

also, having sets to be on the same footing as lazy operations (in the sense that both subtype LazySet) has turned out to be extremely useful

Yeah, that's probably something you would have to give up. I think giving it up might not be so bad if you wanted to use a trait like IsLazySet. But now we're talking about adding even more generality.

Both being a subtype of LazySet helps somewhere with dispatching? Or does it help in a different way?

Marcelo Forets
@mforets
yes, i guess that's what i have in mind , that the construction helps with dispatch. for example suppose there's a new operation Foo(A, B, X, ..) where the arguments are arrays or lazysets. if we let Foo <: LazySet and we know how to compute the support function, i.e. implement ρ(d::AbstractVector, F::Foo) where ρ(d,F)=maxxFoo(...)dTx\rho(d, F) = \max_{x \in Foo(...)} d^T x, then we can reuse a lot of code that has been written generically using support functions.
This includes, say overapproximate(::Foo, something), or composing eg. ρ(d,AFoo(..)Foo(...))\rho(d, A * Foo(..) \oplus Foo(...))
note that A * Foo(..) just works and is again a lazyset (the lazy linear map of a Foo object)
Gustavo Goretkin
@goretkin

https://github.com/JuliaReach/LazySets.jl/blob/master/src/Approximations/overapproximate.jl#L1202

I dug into this at https://github.com/goretkin/FixArgs.jl/issues/21#issuecomment-739122718 There are some features that FixArgs.jl needs still, but I hope it helps to see what the composition looks like

Gustavo Goretkin
@goretkin

I am not sure if there are places where the annotation ::LazySet prevents an ambiguity (current or future). For example:

https://github.com/JuliaReach/LazySets.jl/blob/53f21cb9c26355e7f218578e5b4036c3ff0091fe/src/Approximations/overapproximate.jl#L81-L96

written instead as

overapproximate(S,
                         ::Type{<:HPolygon},
                         ε::Real=Inf)
Gustavo Goretkin
@goretkin

Binding the value of N is a separate problem, but I think fixable. Same with constraints, like ensuring two LazySets have the same N.

Alternatively, maybe there could be something like

struct LazySet2{N, T<:FixArgs.Fix} <: LazySet{N}
    _::T   # it is possible to avoid naming a field when there is only one. access with `lazyset2._`. 
end
Marcelo Forets
@mforets
I am not sure if there are places where the annotation ::LazySet
This sometimes prevents piracy eg Plots and Polyhedra export several names that are also used in LazySets
Gustavo Goretkin
@goretkin

This sometimes prevents piracy eg Plots and Polyhedra export several names that are also used in LazySets

Oh, of course, good point.

Gustavo Goretkin
@goretkin
well, wait. To make sure I understand, it's not because of name collisions, right? We're talking about controlling dispatch, which is the only thing that types in julia are arguably for
So e.g. defining RecipesBase.@recipe function somefunction(arg1::LazySet) end)

So assuming that something like LazySet2 (but with a better name) is the right solution (I am not sure), then there is still a need to encode the information that is encoded by the type hierarchy now, e.g.

abstract type AbstractAffineMap{N, S<:LazySet{N}} <: LazySet{N} end

and

struct LinearMap{N<:Real, S<:LazySet{N}, NM, MAT<:AbstractMatrix{NM}} <: AbstractAffineMap{N, S}

Gustavo Goretkin
@goretkin
I mentioned them before. The only solution to this is "traits". In fact, if plot recipes used traits, then you probably don't even need LazySets. I'm not sure if LazySets.jl uses anything traits-like already. I (and lots of other julia people) use "traits" specifically to mean things that can control dispatch. So
isoperationtype(::Type{<:AbstractAffineMap}) = true is not a trait by this definition, since julia can't dispatch on true or false. But it can, however, dispatch on Val{true} and Val{false} (and for that matter, Val{true}() and Val{false}() as well)
Gustavo Goretkin
@goretkin
Marcelo Forets
@mforets
:thumbsup: LazySets does not use traits, but we have planned to do so for extending the type hierarchy with sets representations which are not convex
Marcelo Forets
@mforets
what is a good way to write a list of equations with documenter?
it uses aligned
Marcelo Forets
@mforets
Christian Schilling
@schillic
:+1:
Marcelo Forets
@mforets
FYI yesterday I added some mathematical details on LGG09 algorithm : https://juliareach.github.io/ReachabilityAnalysis.jl/dev/lib/algorithms/LGG09/#Homogeneous-case-1
Marcelo Forets
@mforets
Christian Schilling
@schillic
:+1:
Peng Yu
@yupbank
image.png
hello firends, wondering if i get some help around understanding this operation
Marcelo Forets
@mforets
hi
Peng Yu
@yupbank

For a discrete set GRnG \subset \mathbb{R}^n .
It is testing condition: zG\forall z \in G if zz spans a ray of cone(G)\operatorname{cone}(G).

Isn't it always true for all elements of GG ?

Marcelo Forets
@mforets
im not familiar with all the details of the paper (i think we have it referenced in a LazySets issue, but the method hasn't been implemented)
i see that line 8 comes from applying Proposition 4.3
what is ξ(x)\xi(x) by the way
it is the subset of GG that sums to xx
Peng Yu
@yupbank
yeah, in the every first iteration, it would be \emptyset
it’s picking yx+Gy \in x+G and then test yxy-x, which can be simiplified into zG z \in G and then test zz
Christian Schilling
@schillic
Marcelo Forets
@mforets
interesting, thx
. The ultimate goal is to scale up to large NeuralODE controllers for complicated CPS or biological tasks
i think there are some Julia people interested in these topics
Marcelo Forets
@mforets
theyseem to consider only singleton initial conditions?
Christian Schilling
@schillic
i haven't checked it. could be