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)

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
Marcelo Forets
@mforets
nice thing is that we have almost every model in the benchmark already in Julia
Christian Schilling
@schillic
:)
Marcelo Forets
@mforets
r: initial radius in each dimension
that should be the specification of X0 around the points in the Appendix
im surprised that some of the results of Flow* are so coarse
Screenshot from 2020-12-18 08-30-04.png
that's what i get for the Brusselator example in their setting
Christian Schilling
@schillic
with Flow*?
Marcelo Forets
@mforets
with JuliaReach