Add @ivp macro

[mforets]

Proposal: add @ivp for initial-value problem, that behaves like @system but additionally receives the initial condition, eg.

julia> @ivp(x' = -x, x(0) ∈ Interval(-1.0, 1.0))

[ueliwechsler]

What about extending the @system macro with an additional property? Which does create a IVP if there is a state(0) ∈ set structure?

julia> @system(x' = -x, x(0) ∈ Interval(-1.0, 1.0))

[mforets]

Ok, good idea 👍 . InitialValueProblem are also systems.

We can extend @system as a first step, but i still consider adding @ivp, macro which requires x(0) ∈ ... to be present. Usage within reachability problems would be:

P = @ivp x' = -x, x(0) ∈ Interval(-1.0, 1.0)
solve(P, T=1.0)

[ueliwechsler]

So, the @ivp macro would basically be @system with an additional check, for the property state(0)?

[mforets]

Yes, that's exactly what i have in mind so far. So we can re-use as much as the existing functionality of @system as possible.

[schillic]

If you want to parse an expression as S, I, it mainly depends on how the parser binds the comma.
@icp x' = Ax, X, Y can be parsed as either

• S being x' = Ax, X and I being Y (that is what you want here) or
• S being x' = Ax and I being X, Y.

[mforets]

Not sure i'm following -- what is I here? For what it's worth, "native" Julia parsing for @ivp x' = Ax, X, Y is an assignment operation, x' = (....).

[schillic]

what is I here?

My impression is that you want @ivp to match the pattern S, I where S is a system definition and I is a definition of the initial states.

[mforets]

Ok. I thought about that too, it could be useful. But for @ivp i was proposing to start with

P = @ivp x' = -x, x(0) ∈ Interval(-1.0, 1.0)

which would re-use the @system stuff.

We can try to make this work in a later stage:

S = @system x' = x 
P = @ivp S, x(0) ∈ Interval(-1.0, 1.0)

or even

S = @system x' = x
X0 = Interval(-1.0, 1.0) 
P = @ivp S, X0

[schillic]

I was not talking about the system being a variable. This is just the pattern matching when you break up your expression into subexpressions, which I assumed you would want to do in order to find the subexpression that you call @system for.

[schillic]

The problem is resolved by using the pattern S, X0 ∈ SET.

[ueliwechsler]

How should the macro look at the end?

We can try to make this work in a later stage:

S = @system x' = x 
P = @ivp S, x(0) ∈ Interval(-1.0, 1.0)

or even

S = @system x' = x
X0 = Interval(-1.0, 1.0) 
P = @ivp S, X0

If this is the wanted representation of the @ivp macro, it would be easier to have it independent of the @system macro. In this case, it would take an AbstractSystem as first argument and the initial state as second. It should be relatively easy to implement.

However, if you would like to have something like @ivp x' = -x, x(0) ∈ Interval(-1.0, 1.0) we should use the structure from @system. Unless, we can write it like this @ivp @system(x' = -x), Interval(-1.0, 1.0)

[mforets]

I think that @ivp x' = -x, x(0) ∈ Interval(-1.0, 1.0) , or i should say @ivp(x' = -x, x(0) ∈ Interval(-1.0, 1.0)) for now, would be nice to have and the work needed is "epsilon-close" from the current status of the package. I will continue writing documentation/examples for reachability stuff with that new macro notation. The other ideas are 2epsilon or more work so i would reconsider them later ;)

Also, i prefer to not restrict the macros too much (at least on this initial stage, and then we see what use arises).

[schillic]

Here is something to start with (I am not experienced with this stuff):

macro ivp(expr)
    parsed = Meta.parse(string(expr))
    @capture(parsed, (system_, x0_(0) ∈ X0_))
end

This only works with the second version (@ivp(...)).

[ueliwechsler]

So I am still not sure, if I get it right. But one version would be

using MathematicalSystems
using MacroTools

sys = @system(x⁺ = ones(2,2)x)
x0 = [1,2]

macro ivp(expr...)
    return  esc(Expr(:call, IVP, eval(expr[1]), eval(expr[2])))
end

@ivp sys, x0 #IVP(sys,x0)

But this is basically the same as IVP(sys, x0) 😅

Here is something to start with (I am not experienced with this stuf):

macro ivp(expr)
    parsed = Meta.parse(string(expr))
    @capture(parsed, (system_, x0_(0) ∈ X0_))
end

From my experience, it's sometimes really hard to get your head around macros so for me, it's often a lot of trial and error.

You can leave out the string parse step and just write

macro ivp(expr)
    @capture(parsed, (system_, x0_(0) ∈ X0_))
end

because expr is already parsed as an expression when entering the macro.

This code could then be used to write the macro as

macro ivp(expr)
    @capture(expr, (system_, x0_(0) ∈ X0_))
    return  esc(Expr(:call, IVP, eval(system), eval(X0)))
end

@ivp sys, x(0) ∈ 3 # IVP(sys, 3)

[mforets]

Thanks for having a look into this feature. Our first version is concerned with #137 (comment) and i added a test in the branch #147.
About the @ivp macro, i have created a separate test, #148. We can do them in any order. Feel free to commit on top of those branches in case you want to send code.

[ueliwechsler]

I'd like to ask for clarification on how the macro should look like because this defines the complexity of the implementation siginifcantly.

The first version would be:

S = @system x' = x 
P = @ivp S, x(0) ∈ Interval(-1.0, 1.0)
# or
P = @ivp S, Interval(-1.0, 1.0)

this is the easist implementation and totally independent of @system and the solution is already here

The second version would be

P = @ivp x' = -x, x(0) ∈ Interval(-1.0, 1.0)

but without changing the @system macro. Because we just call the @system macro from within the @ivp macro

and the third version would be

P = @ivp x' = -x, x(0) ∈ Interval(-1.0, 1.0)

but also changing the @system macro to allow for @system x' = -x, x(0) ∈ Interval(-1.0, 1.0) to work.

After considering the option, I prefer the first version. We could theoretically still have the option to add an initial state option to the @system macro. If we use version 3, @ivp would basically do the same as the @system macro which is a bit redundant.

Also, the second and the third version become quite unpractical for more invovled system definitions, consider e.g.

@ivp x' = rand(2,2)*x+rand(2,1)*u  + w, w∈W, x∈X, u∈U, x(0) ∈ Interval(-1.0, 1.0)

compared to

sys = @system x' = rand(2,2)*x+rand(2,1)*u + w, w∈W, x∈X, u∈U,
ivp = @ivp sys, x(0) ∈ Interval(-1.0, 1.0)

[mforets]

The behavior of a new @ivp macro that i'd like to propose in this issue is the one in #148 => your versions 2-3 in the last comment.

On the other hand, i like to allow @system to parse an initial state, since IVPs are also system; the behavior is #147 . This is your version 3.

Yes, there's some redundancy in having these 2 ways macros. But i think that is not bad, at least in this preliminary phase. @system is more general, it produces many kinds of systems, while @ivp only produces initial-value problems. It is these latter kind of problems that are accepted in a solve function in reachability.

In either case, i didn't think about the implementation yet, but extending the @system macro or refactoring it a bit sounds good.