schillic on abstractinterval
generalize to AbstractInterval (compare)
mforets on gh-pages
build based on 17b25d7 (compare)
mforets on lgg09_symbol
mforets on master
add test Update LGG09.jl Merge pull request #555 from Ju… (compare)
mforets on gh-pages
build based on 93fab9b (compare)
mforets on gh-pages
build based on 3947b22 (compare)
mforets on lgg09_symbol
Update LGG09.jl (compare)
mforets on homogeneize
mforets on master
update homog methods updates homog Merge pull request #556 from Ju… (compare)
schillic on exponential_map
concrete exponential map add concretize for ExponentialM… (compare)
mforets on gh-pages
build based on ba9fb8a (compare)
mforets on gh-pages
build based on 5c7deae (compare)
@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)