schillic on exponential_map
add concretize for ExponentialM… (compare)
schillic on exponential_map
concrete exponential map (compare)
mforets on 366
schillic on gh-pages
build based on eba7e06 (compare)
github-actions[bot] on v1.52.0
mforets on mforets-patch-2
mforets on master
Update Project.toml (#2878) (compare)
schillic on gh-pages
build based on 6d8ce83 (compare)
mforets on mforets-patch-2
Update Project.toml (compare)
mforets on mforets-patch-2
@taylorize
works, please substitute all right-hand sides which are numeric constants with zero(u[1])
or one(u[1])
. For example,
@taylorize function stable!(du, u, p, t)
#differential equations for the stable water tank mode
du[1] = zero(u[1])
du[2] = zero(u[1])
du[3] = zero(u[1])
return du
end
and for the filling mode,
@taylorize function filling!(du, u, p, t)
d_in, d_out, h = u
#differential equations for the filling water tank mode
du[1] = one(u[1])
du[2] = zero(u[1])
du[3] = d_in
return du
end
etc
# transition "stable" -> "normal"
add_transition!(automaton, 1, 2, 1)
#guard_1 = HalfSpace(h >= 0, var)
t1 = @map(h -> h, dim: 3)
# transition "normal" -> "filling"
add_transition!(automaton, 2, 3, 2)
guard_2 = HalfSpace(h <= V_saf_min, var)
t2 = @map(h -> h, dim: 3, h ∈ guard_2)
# transition "normal" -> "emptying"
add_transition!(automaton, 2, 3, 2)
guard_3 = HalfSpace(h >= V_saf_max, var)
t3 = @map(h -> h, dim: 3, h ∈ guard_3)
add_transition!
annotations, the integer arguments correspond to the source (resp target nodes), while the final argument is just a label (tag) for the transition.
2, 3, 2
should be repeated. It is possible to have more than one transition between the same pair of source/node modes, but from your comment in the code, and given thatmodes=[stable_mode, normal_mode, filling_mode, emptying_mode]
# transition "stable" -> "normal"
add_transition!(automaton, 1, 2, 1)
#guard_1 = HalfSpace(h >= 0, var)
t1 = @map(h -> h, dim: 3)
# transition "normal" -> "filling"
add_transition!(automaton, 2, 3, 2)
guard_2 = HalfSpace(h <= V_saf_min, var)
t2 = @map(h -> h, dim: 3, h ∈ guard_2)
# transition "normal" -> "emptying"
add_transition!(automaton, 2, 4, 3)
guard_3 = HalfSpace(h >= V_saf_max, var)
t3 = @map(h -> h, dim: 3, h ∈ guard_3)
Does that make sense?
Another thing that I noticed is that the automaton begins at the "stable" mode, and the dynamics is zero, so I'm not sure that it will eventually take a transition. I may be wrong, but perhaps it's good if you revise the model with my previous comments, then we continue discussing how to obtain the reachability solution.
@map
macro with a constrained set is ignored, in fact there is an unresolved issue about that (https://github.com/JuliaReach/MathematicalSystems.jl/issues/198#issuecomment-909562237)
ConstrainedIdentityMap
(https://juliareach.github.io/MathematicalSystems.jl/latest/lib/types/#MathematicalSystems.ConstrainedIdentityMap).
# transition "stable" -> "normal"
add_transition!(automaton, 1, 2, 1)
guard_1 = Universe(3)
t1 = ConstrainedIdentityMap(3, guard_1)
# transition "normal" -> "filling"
add_transition!(automaton, 2, 3, 2)
guard_2 = HalfSpace(h <= V_saf_min, var)
t2 = ConstrainedIdentityMap(3, guard_2)
# transition "normal" -> "emptying"
add_transition!(automaton, 2, 4, 3)
guard_3 = HalfSpace(h >= V_saf_max, var)
t3 = ConstrainedIdentityMap(3, guard_3)
In case you still prefer to use the nonlinear solver TMJets, seems like it hits a corner case if every equation is zero, as in the stable!(du, u, p, t)
case. I tried with zero(u[1]) + eps(Float64)
and it works, it may be useful to debug what is going on in that special case.. but I would suggest to re-write the model and use linear solvers in the current case. That requires to manually write each coefficient matrix like:
A = zeros(3, 3)
stable_mode = @system(h' = A*h, h ∈ X) # water tank mode stable
etc.