Different exponentiation methods in discretization

[mforets]

Having the second option seems unreasonable because we could already use the concrete matrix exponential in the discretization.

If i recall correctly, that option was a workaround for the fact that we use the same "exp_method" in the calculation of two different problems: ϕ and Phi2Aabs. But the latter is more costly than the former, since it is 3 times bigger. So the idea was to do lazy computations for the discretization and then transform to concrete ϕ in the iteration.

The code in that part (https://github.com/JuliaReach/Reachability.jl/pull/503) is now:

    # compute matrix ϕ = exp(Aδ)
    ϕ = exp_Aδ(A, δ, exp_method=exp_method)

    # compute the transformation matrix to bloat the initial states
    Phi2Aabs = Φ₂(abs.(A), δ, exp_method=exp_method)

And it still doesn't let to choose between different exponentiation methods in ϕ and in Phi2Aabs.

I think that we can continue like this, and eventually add this option if needed.

Originally posted by @mforets in https://github.com/JuliaReach/Reachability.jl/issues/465#issuecomment-469673331

[schillic]

So the idea was to do lazy computations for the discretization and then transform to concrete ϕ in the iteration.

Yes, this was the idea of a very naive me. If the full matrix is computed from the lazy matrix, then there is no reason to compute it lazily in the first place. If that really was faster than computing the concrete matrix directly, then exp would do that internally already.