Commit c3d6a1f7 authored by Bentriou Mahmoud's avatar Bentriou Mahmoud
Browse files

Change of types: String => Symbol for locations, constants,

variableautomaton. It improves performance.

Tests of Cosmos doesn't pass on the bounds (with a parameter equal to
zero). It's a problem of design (there are issues for cosmos too).
parent 667eebf5
......@@ -2,154 +2,128 @@
function create_automaton_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, str_obs::String)
@assert str_obs in m.g
# Locations
locations = ["l0", "l1", "l2", "l3"]
locations = [:l0, :l1, :l2, :l3]
## Invariant predicates
true_inv_predicate = (A::LHA, S:: StateLHA) -> return true
Λ_F = Dict("l0" => true_inv_predicate, "l1" => true_inv_predicate,
"l2" => true_inv_predicate, "l3" => true_inv_predicate)
Λ_F = Dict(:l0 => true_inv_predicate, :l1 => true_inv_predicate,
:l2 => true_inv_predicate, :l3 => true_inv_predicate)
## Init and final loc
locations_init = ["l0"]
locations_final = ["l2"]
locations_init = [:l0]
locations_final = [:l2]
#S.n <=> S.values[A.map_var_automaton_idx["n"]]
#S.n <=> S.values[A.map_var_automaton_idx[:n]]
#P <=> xn[map_var_model_idx[constants[str_O]] with str_O = "P". On stock str_O dans constants
# P = get_value(A, x, str_obs)
## Map of automaton variables
map_var_automaton_idx = Dict{VariableAutomaton,Int}("n" => 1, "d" => 2, "isabs" => 3)
map_var_automaton_idx = Dict{VariableAutomaton,Int}(:n => 1, :d => 2, :isabs => 3)
## Flow of variables
flow = Dict{VariableAutomaton,Vector{Float64}}("l0" => [0.0,0.0,0.0],
"l1" => [0.0,0.0,0.0],
"l2" => [0.0,0.0,0.0],
"l3" => [0.0,0.0,0.0])
flow = Dict{Location,Vector{Float64}}(:l0 => [0.0,0.0,0.0],
:l1 => [0.0,0.0,0.0],
:l2 => [0.0,0.0,0.0],
:l3 => [0.0,0.0,0.0])
## Edges
map_edges = Dict{Tuple{Location,Location}, Vector{Edge}}()
map_edges = Dict{Location, Dict{Location, Vector{Edge}}}()
for loc in locations
map_edges[loc] = Dict{Location, Vector{Edge}}()
end
istrue(val::Float64) = convert(Bool, val)
# l0 loc : we construct the edges of the form l0 => (..)
# "cc" as check_constraints
tuple = ("l0", "l1")
tuple = (:l0, :l1)
cc_aut_F_l0l1_1(A::LHA, S::StateLHA) = true
us_aut_F_l0l1_1!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l1";
S["n"] = get_value(A, x, str_obs);
S["d"] = Inf;
S["isabs"] = m.isabsorbing(m.p,x))
(S.loc = :l1;
S[:n] = get_value(A, x, str_obs);
S[:d] = Inf;
S[:isabs] = m.isabsorbing(m.p,x))
edge1 = Edge([nothing], cc_aut_F_l0l1_1, us_aut_F_l0l1_1!)
map_edges[tuple] = [edge1]
map_edges[:l0][:l1] = [edge1]
# l1 loc : we construct the edges of the form l1 => (..)
tuple = ("l1", "l2")
tuple = (:l1, :l2)
cc_aut_F_l1l2_1(A::LHA, S::StateLHA) =
S.time >= A.constants.t1 &&
(A.constants.x1 <= S["n"] <= A.constants.x2)
S.time >= A.constants[:t1] &&
(A.constants[:x1] <= S[:n] <= A.constants[:x2])
us_aut_F_l1l2_1!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2";
S["d"] = 0)
(S.loc = :l2;
S[:d] = 0)
edge1 = Edge([nothing], cc_aut_F_l1l2_1, us_aut_F_l1l2_1!)
cc_aut_F_l1l2_4(A::LHA, S::StateLHA) =
S.time >= A.constants.t1 &&
S["d"] == 0
S.time >= A.constants[:t1] &&
S[:d] == 0
us_aut_F_l1l2_4!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2")
(S.loc = :l2)
edge4 = Edge([nothing], cc_aut_F_l1l2_4, us_aut_F_l1l2_4!)
cc_aut_F_l1l2_2(A::LHA, S::StateLHA) =
(S.time >= A.constants.t2) &&
(S["n"] < A.constants.x1 || S["n"] > A.constants.x2)
(S.time >= A.constants[:t2]) &&
(S[:n] < A.constants[:x1] || S[:n] > A.constants[:x2])
us_aut_F_l1l2_2!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2";
S["d"] = min(abs(S["n"] - A.constants.x1), abs(S["n"] - A.constants.x2)))
(S.loc = :l2;
S[:d] = min(abs(S[:n] - A.constants[:x1]), abs(S[:n] - A.constants[:x2])))
edge2 = Edge([nothing], cc_aut_F_l1l2_2, us_aut_F_l1l2_2!)
cc_aut_F_l1l2_3(A::LHA, S::StateLHA) =
istrue(S["isabs"]) && S.time <= A.constants.t2
istrue(S[:isabs]) && S.time <= A.constants[:t2]
us_aut_F_l1l2_3!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2")
(S.loc = :l2)
edge3 = Edge([nothing], cc_aut_F_l1l2_3, us_aut_F_l1l2_3!)
map_edges[tuple] = [edge1, edge2, edge3, edge4]
#=
tuple = ("l1", "l2")
cc_aut_F_l1l2_1(A::LHA, S::StateLHA) =
(A.constants.x1 <= S["n"] <= A.constants.x2) &&
(A.constants.t1 <= S.time <= A.constants.t2)
us_aut_F_l1l2_1!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2";
S["d"] = 0)
edge1 = Edge([nothing], cc_aut_F_l1l2_1, us_aut_F_l1l2_1!)
map_edges[:l1][:l2] = [edge1, edge2, edge3, edge4]
cc_aut_F_l1l2_2(A::LHA, S::StateLHA) =
S["d"] > 0 && istrue(S["isabs"])
us_aut_F_l1l2_2!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2")
edge2 = Edge([nothing], cc_aut_F_l1l2_2, us_aut_F_l1l2_2!)
cc_aut_F_l1l2_4(A::LHA, S::StateLHA) =
S["d"] >= Inf && S.time >= A.constants.t2
us_aut_F_l1l2_4!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2";
S["d"] = min(abs(S["n"] - A.constants.x1), abs(S["n"] - A.constants.x2)));
edge4 = Edge([nothing], cc_aut_F_l1l2_4, us_aut_F_l1l2_4!)
cc_aut_F_l1l2_3(A::LHA, S::StateLHA) =
S["d"] == 0 &&
S.time >= A.constants.t1
us_aut_F_l1l2_3!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2")
edge3 = Edge([nothing], cc_aut_F_l1l2_3, us_aut_F_l1l2_3!)
map_edges[tuple] = [edge1, edge2, edge3, edge4]
=#
tuple = ("l1", "l3")
tuple = (:l1, :l3)
cc_aut_F_l1l3_1(A::LHA, S::StateLHA) =
(A.constants.x1 <= S["n"] <= A.constants.x2)
(A.constants[:x1] <= S[:n] <= A.constants[:x2])
us_aut_F_l1l3_1!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l3";
S["d"] = 0;)
(S.loc = :l3;
S[:d] = 0;)
edge1 = Edge([nothing], cc_aut_F_l1l3_1, us_aut_F_l1l3_1!)
cc_aut_F_l1l3_2(A::LHA, S::StateLHA) =
(S["n"] < A.constants.x1 || S["n"] > A.constants.x2) &&
(S.time <= A.constants.t1)
(S[:n] < A.constants[:x1] || S[:n] > A.constants[:x2]) &&
(S.time <= A.constants[:t1])
us_aut_F_l1l3_2!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l3";
S["d"] = min(sqrt((S.time - A.constants.t1)^2 + (S["n"] - A.constants.x2)^2),
sqrt((S.time - A.constants.t1)^2 + (S["n"] - A.constants.x1)^2)))
(S.loc = :l3;
S[:d] = min(sqrt((S.time - A.constants[:t1])^2 + (S[:n] - A.constants[:x2])^2),
sqrt((S.time - A.constants[:t1])^2 + (S[:n] - A.constants[:x1])^2)))
edge2 = Edge([nothing], cc_aut_F_l1l3_2, us_aut_F_l1l3_2!)
cc_aut_F_l1l3_3(A::LHA, S::StateLHA) =
(S["n"] < A.constants.x1 || S["n"] > A.constants.x2) &&
(A.constants.t1 <= S.time <= A.constants.t2)
(S[:n] < A.constants[:x1] || S[:n] > A.constants[:x2]) &&
(A.constants[:t1] <= S.time <= A.constants[:t2])
us_aut_F_l1l3_3!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l3";
S["d"] = min(S["d"], min(abs(S["n"] - A.constants.x1), abs(S["n"] - A.constants.x2))))
(S.loc = :l3;
S[:d] = min(S[:d], min(abs(S[:n] - A.constants[:x1]), abs(S[:n] - A.constants[:x2]))))
edge3 = Edge([nothing], cc_aut_F_l1l3_3, us_aut_F_l1l3_3!)
map_edges[tuple] = [edge1, edge2, edge3]
map_edges[:l1][:l3] = [edge1, edge2, edge3]
# l3 loc
tuple = ("l3", "l1")
tuple = (:l3, :l1)
cc_aut_F_l3l1_1(A::LHA, S::StateLHA) = true
us_aut_F_l3l1_1!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l1";
S["n"] = get_value(A, x, str_obs);
S["isabs"] = m.isabsorbing(m.p,x))
(S.loc = :l1;
S[:n] = get_value(A, x, str_obs);
S[:isabs] = m.isabsorbing(m.p,x))
edge1 = Edge(["ALL"], cc_aut_F_l3l1_1, us_aut_F_l3l1_1!)
tuple = ("l3", "l2")
map_edges[:l3][:l1] = [edge1]
tuple = (:l3, :l2)
cc_aut_F_l3l2_1(A::LHA, S::StateLHA) =
(S.time >= A.constants.t2)
(S.time >= A.constants[:t2])
us_aut_F_l3l2_1!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2")
edge2 = Edge([nothing], cc_aut_F_l3l2_1, us_aut_F_l3l2_1!)
map_edges[tuple] = [edge1, edge2]
(S.loc = :l2)
edge1 = Edge([nothing], cc_aut_F_l3l2_1, us_aut_F_l3l2_1!)
map_edges[:l3][:l2] = [edge1]
## Constants
constants = (x1 = x1, x2 = x2, t1 = t1, t2 = t2)
constants = Dict{Symbol,Float64}(:x1 => x1, :x2 => x2, :t1 => t1, :t2 => t2)
A = LHA(m.transitions, locations, Λ_F, locations_init, locations_final,
map_var_automaton_idx, flow, map_edges, constants, m.map_var_idx)
......
......@@ -2,191 +2,196 @@
function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, str_obs::String)
@assert str_obs in m.g
# Locations
locations = ["l0", "l1", "l2", "l3", "l4"]
locations = [:l0, :l1, :l2, :l3, :l4]
# Invariant predicates
true_inv_predicate = (A::LHA, S:: StateLHA) -> return true
Λ_F = Dict("l0" => true_inv_predicate, "l1" => true_inv_predicate,
"l2" => true_inv_predicate, "l3" => true_inv_predicate,
"l4" => true_inv_predicate)
Λ_F = Dict(:l0 => true_inv_predicate, :l1 => true_inv_predicate,
:l2 => true_inv_predicate, :l3 => true_inv_predicate,
:l4 => true_inv_predicate)
## Init and final loc
locations_init = ["l0"]
locations_final = ["l2"]
locations_init = [:l0]
locations_final = [:l2]
## Map of automaton variables
map_var_automaton_idx = Dict{VariableAutomaton,Int}("tprime" => 1, "in" => 2,
"n" => 3, "d" => 4, "isabs" => 5)
map_var_automaton_idx = Dict{VariableAutomaton,Int}(:tprime => 1, :in => 2,
:n => 3, :d => 4, :isabs => 5)
## Flow of variables
flow = Dict{VariableAutomaton,Vector{Float64}}("l0" => [0.0,0.0,0.0,0.0,0.0],
"l1" => [0.0,0.0,0.0,0.0,0.0],
"l2" => [0.0,0.0,0.0,0.0,0.0],
"l3" => [0.0,0.0,0.0,0.0,0.0],
"l4" => [1.0,0.0,0.0,0.0,0.0])
flow = Dict{Location,Vector{Float64}}(:l0 => [0.0,0.0,0.0,0.0,0.0],
:l1 => [0.0,0.0,0.0,0.0,0.0],
:l2 => [0.0,0.0,0.0,0.0,0.0],
:l3 => [0.0,0.0,0.0,0.0,0.0],
:l4 => [1.0,0.0,0.0,0.0,0.0])
## Edges
map_edges = Dict{Tuple{Location,Location}, Vector{Edge}}()
map_edges = Dict{Location, Dict{Location, Vector{Edge}}}()
for loc in locations
map_edges[loc] = Dict{Location, Vector{Edge}}()
end
istrue(val::Float64) = convert(Bool, val)
# l0 loc
tuple = ("l0", "l1")
tuple = (:l0, :l1)
cc_aut_G_l0l1_1(A::LHA, S::StateLHA) = true
us_aut_G_l0l1_1!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l1";
S["d"] = 0;
S["n"] = get_value(A, x, str_obs);
S["in"] = true;
S["isabs"] = m.isabsorbing(m.p,x))
(S.loc = :l1;
S[:d] = 0;
S[:n] = get_value(A, x, str_obs);
S[:in] = true;
S[:isabs] = m.isabsorbing(m.p,x))
edge1 = Edge([nothing], cc_aut_G_l0l1_1, us_aut_G_l0l1_1!)
map_edges[tuple] = [edge1]
map_edges[:l0][:l1] = [edge1]
# l1 loc
tuple = ("l1", "l3")
tuple = (:l1, :l3)
cc_aut_G_l1l3_1(A::LHA, S::StateLHA) =
S.time <= A.constants.t1 &&
S["n"] < A.constants.x1 || S["n"] > A.constants.x2
S.time <= A.constants[:t1] &&
S[:n] < A.constants[:x1] || S[:n] > A.constants[:x2]
us_aut_G_l1l3_1!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l3";
S["d"] = min(abs(A.constants.x1 - S["n"]), abs(A.constants.x2 - S["n"]));
S["in"] = false)
(S.loc = :l3;
S[:d] = min(abs(A.constants[:x1] - S[:n]), abs(A.constants[:x2] - S[:n]));
S[:in] = false)
edge1 = Edge([nothing], cc_aut_G_l1l3_1, us_aut_G_l1l3_1!)
cc_aut_G_l1l3_3(A::LHA, S::StateLHA) =
!istrue(S["in"]) &&
(A.constants.t1 <= S.time <= A.constants.t2) &&
(A.constants.x1 <= S["n"] <= A.constants.x2)
!istrue(S[:in]) &&
(A.constants[:t1] <= S.time <= A.constants[:t2]) &&
(A.constants[:x1] <= S[:n] <= A.constants[:x2])
us_aut_G_l1l3_3!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l3";
S["d"] = S["d"] * (S.time - A.constants.t1);
S["tprime"] = 0.0)
(S.loc = :l3;
S[:d] = S[:d] * (S.time - A.constants[:t1]);
S[:tprime] = 0.0)
edge3 = Edge([nothing], cc_aut_G_l1l3_3, us_aut_G_l1l3_3!)
cc_aut_G_l1l3_2(A::LHA, S::StateLHA) =
(S.time <= A.constants.t1) &&
(A.constants.x1 <= S["n"] <= A.constants.x2)
(S.time <= A.constants[:t1]) &&
(A.constants[:x1] <= S[:n] <= A.constants[:x2])
us_aut_G_l1l3_2!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l3";
S["d"] = 0;
S["in"] = false)
(S.loc = :l3;
S[:d] = 0;
S[:in] = false)
edge2 = Edge([nothing], cc_aut_G_l1l3_2, us_aut_G_l1l3_2!)
cc_aut_G_l1l3_4(A::LHA, S::StateLHA) =
istrue(S["in"]) &&
(A.constants.t1 <= S.time <= A.constants.t2) &&
(A.constants.x1 <= S["n"] <= A.constants.x2)
istrue(S[:in]) &&
(A.constants[:t1] <= S.time <= A.constants[:t2]) &&
(A.constants[:x1] <= S[:n] <= A.constants[:x2])
us_aut_G_l1l3_4!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l3";
S["tprime"] = 0.0)
(S.loc = :l3;
S[:tprime] = 0.0)
edge4 = Edge([nothing], cc_aut_G_l1l3_4, us_aut_G_l1l3_4!)
map_edges[tuple] = [edge1, edge2, edge3, edge4]
map_edges[:l1][:l3] = [edge1, edge2, edge3, edge4]
tuple = ("l1", "l4")
tuple = (:l1, :l4)
cc_aut_G_l1l4_1(A::LHA, S::StateLHA) =
!istrue(S["in"]) &&
(A.constants.t1 <= S.time <= A.constants.t2) &&
(S["n"] < A.constants.x1 || S["n"] > A.constants.x2)
!istrue(S[:in]) &&
(A.constants[:t1] <= S.time <= A.constants[:t2]) &&
(S[:n] < A.constants[:x1] || S[:n] > A.constants[:x2])
us_aut_G_l1l4_1!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l4";
S["d"] += S["d"] * (S.time - A.constants.t1))
(S.loc = :l4;
S[:d] += S[:d] * (S.time - A.constants[:t1]))
edge1 = Edge([nothing], cc_aut_G_l1l4_1, us_aut_G_l1l4_1!)
cc_aut_G_l1l4_2(A::LHA, S::StateLHA) =
istrue(S["in"]) &&
(A.constants.t1 <= S.time <= A.constants.t2) &&
(S["n"] < A.constants.x1 || S["n"] > A.constants.x2)
istrue(S[:in]) &&
(A.constants[:t1] <= S.time <= A.constants[:t2]) &&
(S[:n] < A.constants[:x1] || S[:n] > A.constants[:x2])
us_aut_G_l1l4_2!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l4")
(S.loc = :l4)
edge2 = Edge([nothing], cc_aut_G_l1l4_2, us_aut_G_l1l4_2!)
map_edges[tuple] = [edge1, edge2]
map_edges[:l1][:l4] = [edge1, edge2]
tuple = ("l1", "l2")
tuple = (:l1, :l2)
cc_aut_G_l1l2_1(A::LHA, S::StateLHA) =
istrue(S["in"]) &&
S.time >= A.constants.t2
istrue(S[:in]) &&
S.time >= A.constants[:t2]
us_aut_G_l1l2_1!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2")
(S.loc = :l2)
edge1 = Edge([nothing], cc_aut_G_l1l2_1, us_aut_G_l1l2_1!)
cc_aut_G_l1l2_2(A::LHA, S::StateLHA) =
!istrue(S["in"]) &&
S.time >= A.constants.t2
!istrue(S[:in]) &&
S.time >= A.constants[:t2]
us_aut_G_l1l2_2!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2";
S["d"] = S["d"] * (A.constants.t2 - A.constants.t1))
(S.loc = :l2;
S[:d] = S[:d] * (A.constants[:t2] - A.constants[:t1]))
edge2 = Edge([nothing], cc_aut_G_l1l2_2, us_aut_G_l1l2_2!)
cc_aut_G_l1l2_3(A::LHA, S::StateLHA) =
istrue(S["isabs"]) &&
S.time <= A.constants.t1
istrue(S[:isabs]) &&
S.time <= A.constants[:t1]
us_aut_G_l1l2_3!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2";
S["d"] = (A.constants.t2 - A.constants.t1) *
min(abs(A.constants.x1 - S["n"]), abs(A.constants.x2 - S["n"])))
(S.loc = :l2;
S[:d] = (A.constants[:t2] - A.constants[:t1]) *
min(abs(A.constants[:x1] - S[:n]), abs(A.constants[:x2] - S[:n])))
edge3 = Edge([nothing], cc_aut_G_l1l2_3, us_aut_G_l1l2_3!)
cc_aut_G_l1l2_4(A::LHA, S::StateLHA) =
istrue(S["isabs"]) &&
(A.constants.t1 <= S.time <= A.constants.t2)
istrue(S[:isabs]) &&
(A.constants[:t1] <= S.time <= A.constants[:t2])
us_aut_G_l1l2_4!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2";
S["d"] += (A.constants.t2 - S.time) *
min(abs(A.constants.x1 - S["n"]), abs(A.constants.x2 - S["n"])))
(S.loc = :l2;
S[:d] += (A.constants[:t2] - S.time) *
min(abs(A.constants[:x1] - S[:n]), abs(A.constants[:x2] - S[:n])))
edge4 = Edge([nothing], cc_aut_G_l1l2_4, us_aut_G_l1l2_4!)
map_edges[tuple] = [edge1, edge2, edge3, edge4]
map_edges[:l1][:l2] = [edge1, edge2, edge3, edge4]
# l3 loc
tuple = ("l3", "l1")
tuple = (:l3, :l1)
cc_aut_G_l3l1_1(A::LHA, S::StateLHA) = true
us_aut_G_l3l1_1!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l1";
S["n"] = get_value(A, x, str_obs);
S["isabs"] = m.isabsorbing(m.p,x))
(S.loc = :l1;
S[:n] = get_value(A, x, str_obs);
S[:isabs] = m.isabsorbing(m.p,x))
edge1 = Edge(["ALL"], cc_aut_G_l3l1_1, us_aut_G_l3l1_1!)
map_edges[tuple] = [edge1]
map_edges[:l3][:l1] = [edge1]
tuple = ("l3", "l2")
tuple = (:l3, :l2)
cc_aut_G_l3l2_2(A::LHA, S::StateLHA) =
istrue(S["in"]) &&
S.time >= A.constants.t2
istrue(S[:in]) &&
S.time >= A.constants[:t2]
us_aut_G_l3l2_2!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2";
S["d"] = S["d"] * (A.constants.t2 - A.constants.t1))
(S.loc = :l2;
S[:d] = S[:d] * (A.constants[:t2] - A.constants[:t1]))
edge2 = Edge([nothing], cc_aut_G_l3l2_2, us_aut_G_l3l2_2!)
cc_aut_G_l3l2_1(A::LHA, S::StateLHA) =
!istrue(S["in"]) &&
S.time >= A.constants.t2
!istrue(S[:in]) &&
S.time >= A.constants[:t2]
us_aut_G_l3l2_1!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2")
(S.loc = :l2)
edge1 = Edge([nothing], cc_aut_G_l3l2_1, us_aut_G_l3l2_1!)
map_edges[tuple] = [edge1, edge2]
map_edges[:l3][:l2] = [edge1, edge2]
# l4 loc
tuple = ("l4", "l1")
tuple = (:l4, :l1)
cc_aut_G_l4l1_1(A::LHA, S::StateLHA) = true
us_aut_G_l4l1_1!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l1";
S["d"] += S["tprime"] * min(abs(A.constants.x1 - S["n"]), abs(A.constants.x2 - S["n"]));
S["tprime"] = 0.0;
S["n"] = get_value(A, x, str_obs);
S["in"] = true;
S["isabs"] = m.isabsorbing(m.p,x))
(S.loc = :l1;
S[:d] += S[:tprime] * min(abs(A.constants[:x1] - S[:n]), abs(A.constants[:x2] - S[:n]));
S[:tprime] = 0.0;
S[:n] = get_value(A, x, str_obs);
S[:in] = true;
S[:isabs] = m.isabsorbing(m.p,x))
edge1 = Edge(["ALL"], cc_aut_G_l4l1_1, us_aut_G_l4l1_1!)
map_edges[tuple] = [edge1]
map_edges[:l4][:l1] = [edge1]
tuple = ("l4", "l2")
tuple = (:l4, :l2)
cc_aut_G_l4l2_1(A::LHA, S::StateLHA) =
(S.time >= A.constants.t2)
(S.time >= A.constants[:t2])
us_aut_G_l4l2_1!(A::LHA, S::StateLHA, x::Vector{Int}) =
(S.loc = "l2";
S["d"] += S["tprime"] * min(abs(A.constants.x1 - S["n"]), abs(A.constants.x2 - S["n"]));
S["tprime"] = 0.0)
(S.loc = :l2;
S[:d] += S[:tprime] * min(abs(A.constants[:x1] - S[:n]), abs(A.constants[:x2] - S[:n]));
S[:tprime] = 0.0)
edge1 = Edge([nothing], cc_aut_G_l4l2_1, us_aut_G_l4l2_1!)
map_edges[tuple] = [edge1]
map_edges[:l4][:l2] = [edge1]
## Constants
constants = (x1 = x1, x2 = x2, t1 = t1, t2 = t2)
constants = Dict{Symbol,Float64}(:x1 => x1, :x2 => x2, :t1 => t1, :t2 => t2)
A = LHA(m.transitions, locations, Λ_F, locations_init, locations_final,
map_var_automaton_idx, flow, map_edges, constants, m.map_var_idx)
......
......@@ -5,287 +5,299 @@ function create_automaton_G_and_F(m::ContinuousTimeModel, x1::Float64, x2::Float
@assert str_obs_G in m.g
@assert str_obs_F in m.g
# Locations
locations = ["l0G", "l1G", "l2G", "l3G", "l4G",
"l1F", "l2F", "l3F"]
locations = [:l0G, :l1G, :l2G, :l3G, :l4G,
:l1F, :l2F, :l3F]
# Invariant predicates
true_inv_predicate = (A::LHA, S:: StateLHA) -> return true
Λ_F = Dict("l0G" => true_inv_predicate, "l1G" => true_inv_predicate,
"l2G" => true_inv_predicate, "l3G" => true_inv_predicate,
"l4G" => true_inv_predicate,
"l1F" => true_inv_predicate,
"l2F" => true_inv_predicate, "l3F" => true_inv_predicate)
Λ_F = Dict(:l0G => true_inv_predicate, :l1G => true_inv_predicate,
:l2G => true_inv_predicate, :l3G => true_inv_predicate,