JuliaReach/Lobby

Calculating Reachable states of Dynamical Systems in Julia

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

https://julialang.org/jsoc/gsoc/juliareach/#improving_the_hybrid_systems_reachability_api

and two more on the same page

more info on

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!

Where communities thrive

People

Repo info

Activity