## Where communities thrive

• Join over 1.5M+ people
• Join over 100K+ communities
• Free without limits
##### Activity
• May 16 15:02
• May 15 09:10

mforets on gh-pages

build based on 006c239 (compare)

• May 15 09:08

mforets on gh-pages

build based on cffc4ea (compare)

• May 15 09:02

github-actions[bot] on v0.18.3

• May 15 09:01
JuliaTagBot commented #376
• May 15 08:38
JuliaRegistrator commented on 006c239
• May 15 08:38
schillic commented on 006c239
• May 15 08:37

github-actions[bot] on gh-pages

delete history (compare)

• May 15 08:37

schillic on master

Update Project.toml (compare)

• May 15 08:37

schillic on issubset

• May 15 08:37

schillic on master

extend issubset to unions add _is_intersection_empty for … Merge pull request #630 from Ju… (compare)

• May 15 08:37
schillic closed #630
• May 15 08:37

mforets on gh-pages

build based on 5f5181a (compare)

• May 15 08:02
schillic edited #630
• May 15 08:01
schillic synchronize #630
• May 15 08:01

schillic on issubset

extend issubset to unions add _is_intersection_empty for … (compare)

• May 14 17:37

mforets on gh-pages

build based on fce866f (compare)

• May 14 17:32
schillic review_requested #630
• May 14 17:07
schillic opened #630
• May 14 17:01

schillic on issubset

Marcelo Forets
@mforets

so, basically, im saying

sol=solve(prob,
T = 6.0,
alg=GLGM06(δ=1e-4))

uses some defaults that are most of the time not the good ones for each problem and one has to manually tune it

ideally, one should use different defaults per transition, not just a global one
BTW if you are interested to contribute to JuliaReach and dig further on these matters as part of your Master's thesis or your own interest, take a look at our Google Summer of Code project proposals. we have put a proposal in line with this discussion
and two more on the same page
repolaa
@repolaa
Interesting, maybe next year since I'm still in my first year. Thanks a lot for the help!
repolaa
@repolaa
I have an update: my professor was able to get it to work, at least partially. Here is the code https://github.com/repolaa/pursuer-evader/blob/main/PursuitGame.jl
There is a sequence of messages "glp_simplex: unable to recover undefined or non-optimal solution" that we believe happens when there is a reset, but the algorithm goes on to solve the evolution of the system and with initial conditions 20, 10, 2 it reaches the escape condition correctly. My professor had to split the transition that leads to the escape state into two separate transitions because the framework apparently doesn't allow to handle logical conditions like e==0 OR e==40. Can you confirm if this is the case? Anyhow I said partially because if you change initial conditions and put, for example, 20, 1, 2, then at a certain point the solver "goes crazy". The problem is that the system is not well-defined. Since it seems that JuliaReach does not directly handle dynamic systems on circular spaces, we introduced autotransitions to reset the value of the variable p and make it go from 0 to 40 and vice versa. With initial condition 20, 1, 2 it happens that during the simulation (exactly after 2 seconds) p assumes value zero. At that point the autotransition resets this value to 40 but there is the other guard of the other autotransition that gets enabled and resets the value to 0 and so on. Hence continuous resets, as evidenced by the sequence of messages. I look forward to hearing from you. Thanks again.
Christian Schilling
@schillic

hi @repolaa,

• indeed, we currently do not support non-convex sets. it is on the list, but it still requires many things and will probably not be supported too soon
• yes, since you have guards e == 0 and e == 40, these will be enabled once you set the value there. so the fact that the solver considers those immediate transitions is correct with the semantics of hybrid automata. you can get around that by introducing a new clock t that you reset to 0 on each transition and then you require on these transitions in the guards that t is larger than some positive ε (say, t > 1e-2). I guess you need to choose ε > δ for this to work properly
• strict inequalities (<) are (I think) treated the same way as non-strict ones. so the condition 0. < e, e < 40. should always hold and you can just drop it
• side note: you can use ConstrainedLinearMap for a ConstrainedAffineMap with zero vector

sorry about the errors you got before. I will look at them in a few weeks, but you caught me at a busy time

repolaa
@repolaa
No problem, thank you very much.
repolaa
@repolaa
Hello again. I'm trying a different approach to solve the problem I had and I have a question. I have simplified the problem by letting the variables e and p assume values on a straight line and by writing the enabling conditions for the transitions taking into account that the line is actually a circumference so that multiples of 40 correspond to zero. To do this I am using the mod operation in the conditions. What I get now is the following error:
ArgumentError: Cannot convert Sym to Float64 since Sym is symbolic and Float64 is concrete. Use substitute to replace the symbolic unwraps.
Is the library unable to handle the mod operation symbolically? Here is the updated code https://github.com/repolaa/pursuer-evader/blob/main/PursuitGame.jl
Thanks in advance for any help.
Marcelo Forets
@mforets
Hmm LazySets cannot handle sets like
var = @variables e p clock

Pol = HPolyhedron([6*mod(e, 40) - 5*mod(p, 40) < 40., clock == 2.], var)
This would entail that the constraints defining Pol are also variables?
The right approach seems to define a new set representation that can handle mod?
do you need Pol to be parametric, can't you just define a function closure?
that is, Pol(e, p, clock) = ... which instantiates a polyhedron given some values for the variables
Marcelo Forets
@mforets

The pursuit-evasion game I'm working on is taken from the book Principles of Cyber-Physical Systems by Professor Rajeev Alur.

Would be of great value to add examples from this book to the JuliaReach docs! Do you have pdf version?

repolaa
@repolaa
@mforets I only have an excerpt with pages describing the Pursuit Game I'm working on, but I don't know if it would be legal to share.
Marcelo Forets
@mforets
:thumbsup: no problem
Marcelo Forets
@mforets

I found it :)

for that model, they cite

[AHW97] R. Alur, T.A. Henzinger, and H. Wong-Toi. Symbolic analysis of hybrid systems. In Proceedings of th 37th IEEE Conference on Decision and Control, 1997.

repolaa
@repolaa
Great :) By the way if I manage to solve the problem feel free to add it to the JuliaReach docs
Marcelo Forets
@mforets
:thumbsup: As I commented before, idk if one can currently implement an elegant/simple solution with the current status, but it is certainly possible to build it by combining the base tools provided by the packages. The hybrid solve API is quite difficult to get right and we really haven't paid too much attention to improve it recently, although I acknowledge it is one aspect that, if improved, can potentially bring new users.

By the way if I manage to solve the problem feel free to add it to the JuliaReach docs

That would be awesome; feel free to open issues / open PRs yourself or ask for further help in case of doubts.

repolaa
@repolaa
Yes, thank you so much for all the help you are giving me.
Christian Schilling
@schillic
i finally had time to check the problems with the original pursuit game:
• LGG09 must be used with full dimensions for (almost all) hybrid systems (as already mentioned before); the error message was not helpful and i opened JuliaReach/ReachabilityAnalysis.jl#612
• unions in the guards are currently not supported; when splitting the transitions into two separate transitions (which is equivalent), the analysis terminates with the above plot
Marcelo Forets
@mforets
sweet
repolaa
@repolaa
@schillic Great, thank you very much
Christian Schilling
@schillic
@repolaa no problem, it is nice to have such reports to improve the tool! a few comments:
• as you probably noticed, i only ran the experiment for 0.1 time units, so when i said the analysis terminates i was not completely honest :sweat_smile:
• with a longer time horizon i expect that there would actually be termination problems with this problem's structure because at the boundary you can go back and forth all the time
• did you know that we also have a simulator? maybe this can help even if reachability analysis does not work
• i doubt that we can support this modulo structure that you proposed, but i think you can model this idea with invariants $(e <= 40)$ and transitions with resets $(guard e == 40, reset e := 0)$
repolaa
@repolaa
Yes, it does go back and forth all the time. I did not know about the simulator, I'll look into it. Thanks again
Christian Schilling
@schillic
for simulations see here
repolaa
@repolaa
Sweet, I was trying to find it
Marcelo Forets
@mforets
i mean finding issues / problems / bugs on the first place is great
we will start making some (open) devs calls, i thought about putting @repolaa's problem on the discussion list
maybe for next week, or the week after
feel free to join, will publish connection details later
dfcaporale
@dfcaporale
:thumbsup:
Marcelo Forets
@mforets
FYI The next dev call will take place on monday 11th/04, 11am CET
Marcelo Forets
@mforets
Future dev calls are managed in the juliareach.dev calendar.
If someone else wants an invitation link to see the calendar just drop me a message.
pastankaitis
@pastankaitis
Hi all, is there a function for computing volume of the reachset? (I don't seem to find)
Christian Schilling
@schillic
hi @pastankaitis, no we do not have that implemented at the moment (JuliaReach/LazySets.jl#2111). but i think we can now use Polyhedra for that. i will try to add this feature
pastankaitis
@pastankaitis
@schillic Thanks!
Christian Schilling
@schillic
@pastankaitis: the new release of LazySets has that method now. you should be able to do volume(set(R)) for a reach set R
pastankaitis
@pastankaitis
@schillic Thank you very much!!
ga72kud
@ga72kud
hi everyone, if I have a (non-) convex set X and I want to compute the support function for a predefined certain direction. how would I do that? I found the function support_function in the API in Lazy Sets.jl
I compute a set of LazySets Q = Vector{LazySet{Float64}}(undef, N)
and for each one I want to compute the support function. It seems I have to convert it to Reach Solution. I get following error LoadError: MethodError: no method matching ρ(::BallInf{Float64, Vector{Float64}})
Closest candidates are:
ρ(::Any, !Matched::ReachabilityAnalysis.ReachSolution{FT, ST}
ga72kud
@ga72kud
what I am trying to do is to find the maximal expansion of a set in the direction of a predefined vector (which I understand as support function)
Christian Schilling
@schillic
hi @ga72kud
ρ(::BallInf{Float64, Vector{Float64}}) indeed does not exist. you need to pass two arguments: ρ(d, X) the first argument is the direction d. the second argument is the set X.
ga72kud
@ga72kud
Hi, @schillic thank you for the quick reply. I will try it. thank you!