diff --git a/automata/automaton_F.jl b/automata/automaton_F.jl index 756c19534fca0ab9d96809d7c78b74f9c52f8a7f..a38d49282b5ea5b373f5fbf30ddae3799dd48582 100644 --- a/automata/automaton_F.jl +++ b/automata/automaton_F.jl @@ -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) diff --git a/automata/automaton_G.jl b/automata/automaton_G.jl index 0eec8d731926e4486485d713b310678afa5a2798..e2608f951a986ee1d7bb0474bb84af840440bc4b 100644 --- a/automata/automaton_G.jl +++ b/automata/automaton_G.jl @@ -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) diff --git a/automata/automaton_G_and_F.jl b/automata/automaton_G_and_F.jl index e9b91c476a2660bb15f7ae5ece778dc921c5c731..f3ab84cf512c0976b777ff8562213a3be9d8c776 100644 --- a/automata/automaton_G_and_F.jl +++ b/automata/automaton_G_and_F.jl @@ -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, + :l4G => true_inv_predicate, + :l1F => true_inv_predicate, + :l2F => true_inv_predicate, :l3F => true_inv_predicate) ## Init and final loc - locations_init = ["l0G"] - locations_final = ["l2F"] + locations_init = [:l0G] + locations_final = [:l2F] ## Map of automaton variables - map_var_automaton_idx = Dict{VariableAutomaton,Int}("tprime" => 1, "in" => 2, - "n" => 3, "d" => 4, - "dprime" => 5, "isabs" => 6) + map_var_automaton_idx = Dict{VariableAutomaton,Int}(:tprime => 1, :in => 2, + :n => 3, :d => 4, + :dprime => 5, :isabs => 6) ## Flow of variables - flow = Dict{VariableAutomaton,Vector{Float64}}("l0G" => [0.0,0.0,0.0,0.0,0.0,0.0], - "l1G" => [0.0,0.0,0.0,0.0,0.0,0.0], - "l2G" => [0.0,0.0,0.0,0.0,0.0,0.0], - "l3G" => [0.0,0.0,0.0,0.0,0.0,0.0], - "l4G" => [1.0,0.0,0.0,0.0,0.0,0.0], - "l1F" => [0.0,0.0,0.0,0.0,0.0,0.0], - "l2F" => [0.0,0.0,0.0,0.0,0.0,0.0], - "l3F" => [0.0,0.0,0.0,0.0,0.0,0.0]) + flow = Dict{Location,Vector{Float64}}(:l0G => [0.0,0.0,0.0,0.0,0.0,0.0], + :l1G => [0.0,0.0,0.0,0.0,0.0,0.0], + :l2G => [0.0,0.0,0.0,0.0,0.0,0.0], + :l3G => [0.0,0.0,0.0,0.0,0.0,0.0], + :l4G => [1.0,0.0,0.0,0.0,0.0,0.0], + :l1F => [0.0,0.0,0.0,0.0,0.0,0.0], + :l2F => [0.0,0.0,0.0,0.0,0.0,0.0], + :l3F => [0.0,0.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) # l0G loc - tuple = ("l0G", "l1G") + tuple = (:l0G, :l1G) cc_aut_G_l0Gl1G_1(A::LHA, S::StateLHA) = true us_aut_G_l0Gl1G_1!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l1G"; - S["d"] = 0; - S["n"] = get_value(A, x, str_obs_G); - S["in"] = true; - S["isabs"] = m.isabsorbing(m.p,x)) + (S.loc = :l1G; + S[:d] = 0; + S[:n] = get_value(A, x, str_obs_G); + S[:in] = true; + S[:isabs] = m.isabsorbing(m.p,x)) edge1 = Edge([nothing], cc_aut_G_l0Gl1G_1, us_aut_G_l0Gl1G_1!) - map_edges[tuple] = [edge1] + map_edges[:l0G][:l1G] = [edge1] # l1G loc - tuple = ("l1G", "l3G") + tuple = (:l1G, :l3G) cc_aut_G_l1Gl3G_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_l1Gl3G_1!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l3G"; - S["d"] = min(abs(A.constants.x1 - S["n"]), abs(A.constants.x2 - S["n"])); - S["in"] = false) + (S.loc = :l3G; + S[:d] = min(abs(A.constants[:x1] - S[:n]), abs(A.constants[:x2] - S[:n])); + S[:in] = false) edge1 = Edge([nothing], cc_aut_G_l1Gl3G_1, us_aut_G_l1Gl3G_1!) cc_aut_G_l1Gl3G_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_l1Gl3G_3!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l3G"; - S["d"] = S["d"] * (S.time - A.constants.t1); - S["tprime"] = 0.0) + (S.loc = :l3G; + S[:d] = S[:d] * (S.time - A.constants[:t1]); + S[:tprime] = 0.0) edge3 = Edge([nothing], cc_aut_G_l1Gl3G_3, us_aut_G_l1Gl3G_3!) cc_aut_G_l1Gl3G_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_l1Gl3G_2!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l3G"; - S["d"] = 0; - S["in"] = false) + (S.loc = :l3G; + S[:d] = 0; + S[:in] = false) edge2 = Edge([nothing], cc_aut_G_l1Gl3G_2, us_aut_G_l1Gl3G_2!) cc_aut_G_l1Gl3G_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_l1Gl3G_4!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l3G"; - S["tprime"] = 0.0) + (S.loc = :l3G; + S[:tprime] = 0.0) edge4 = Edge([nothing], cc_aut_G_l1Gl3G_4, us_aut_G_l1Gl3G_4!) - map_edges[tuple] = [edge1, edge2, edge3, edge4] + map_edges[:l1G][:l3G] = [edge1, edge2, edge3, edge4] - tuple = ("l1G", "l4G") + tuple = (:l1G, :l4G) cc_aut_G_l1Gl4G_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_l1Gl4G_1!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l4G"; - S["d"] += S["d"] * (S.time - A.constants.t1)) + (S.loc = :l4G; + S[:d] += S[:d] * (S.time - A.constants[:t1])) edge1 = Edge([nothing], cc_aut_G_l1Gl4G_1, us_aut_G_l1Gl4G_1!) + cc_aut_G_l1Gl4G_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_l1Gl4G_2!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l4G") + (S.loc = :l4G) edge2 = Edge([nothing], cc_aut_G_l1Gl4G_2, us_aut_G_l1Gl4G_2!) - map_edges[tuple] = [edge1, edge2] + + map_edges[:l1G][:l4G] = [edge1, edge2] - tuple = ("l1G", "l2G") + tuple = (:l1G, :l2G) + cc_aut_G_l1Gl2G_3(A::LHA, S::StateLHA) = + istrue(S[:isabs]) && + S.time <= A.constants[:t1] + us_aut_G_l1Gl2G_3!(A::LHA, S::StateLHA, x::Vector{Int}) = + (S.loc = :l2G; + 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_l1Gl2G_3, us_aut_G_l1Gl2G_3!) + cc_aut_G_l1Gl2G_4(A::LHA, S::StateLHA) = + istrue(S[:isabs]) && + (A.constants[:t1] <= S.time <= A.constants[:t2]) + us_aut_G_l1Gl2G_4!(A::LHA, S::StateLHA, x::Vector{Int}) = + (S.loc = :l2G; + 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_l1Gl2G_4, us_aut_G_l1Gl2G_4!) cc_aut_G_l1Gl2G_1(A::LHA, S::StateLHA) = - istrue(S["in"]) && - S.time >= A.constants.t2 + istrue(S[:in]) && + S.time >= A.constants[:t2] us_aut_G_l1Gl2G_1!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l2G") + (S.loc = :l2G) edge1 = Edge([nothing], cc_aut_G_l1Gl2G_1, us_aut_G_l1Gl2G_1!) cc_aut_G_l1Gl2G_2(A::LHA, S::StateLHA) = - !istrue(S["in"]) && - S.time >= A.constants.t2 + !istrue(S[:in]) && + S.time >= A.constants[:t2] us_aut_G_l1Gl2G_2!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l2G"; - S["d"] = S["d"] * (A.constants.t2 - A.constants.t1)) + (S.loc = :l2G; + S[:d] = S[:d] * (A.constants[:t2] - A.constants[:t1])) edge2 = Edge([nothing], cc_aut_G_l1Gl2G_2, us_aut_G_l1Gl2G_2!) - cc_aut_G_l1Gl2G_3(A::LHA, S::StateLHA) = - istrue(S["isabs"]) && - S.time <= A.constants.t1 - us_aut_G_l1Gl2G_3!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l2G"; - 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_l1Gl2G_3, us_aut_G_l1Gl2G_3!) - cc_aut_G_l1Gl2G_4(A::LHA, S::StateLHA) = - istrue(S["isabs"]) && - (A.constants.t1 <= S.time <= A.constants.t2) - us_aut_G_l1Gl2G_4!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l2G"; - 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_l1Gl2G_4, us_aut_G_l1Gl2G_4!) - - map_edges[tuple] = [edge1, edge2, edge3, edge4] + + map_edges[:l1G][:l2G] = [edge3, edge4, edge1, edge2] # l3G loc - tuple = ("l3G", "l1G") + tuple = (:l3G, :l1G) cc_aut_G_l3Gl1G_1(A::LHA, S::StateLHA) = true us_aut_G_l3Gl1G_1!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l1G"; - S["n"] = get_value(A, x, str_obs_G); - S["isabs"] = m.isabsorbing(m.p,x)) + (S.loc = :l1G; + S[:n] = get_value(A, x, str_obs_G); + S[:isabs] = m.isabsorbing(m.p,x)) edge1 = Edge(["ALL"], cc_aut_G_l3Gl1G_1, us_aut_G_l3Gl1G_1!) - map_edges[tuple] = [edge1] + map_edges[:l3G][:l1G] = [edge1] - tuple = ("l3G", "l2G") + tuple = (:l3G, :l2G) cc_aut_G_l3Gl2G_2(A::LHA, S::StateLHA) = - istrue(S["in"]) && - S.time >= A.constants.t2 + istrue(S[:in]) && + S.time >= A.constants[:t2] us_aut_G_l3Gl2G_2!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l2G"; - S["d"] = S["d"] * (A.constants.t2 - A.constants.t1)) + (S.loc = :l2G; + S[:d] = S[:d] * (A.constants[:t2] - A.constants[:t1])) edge2 = Edge([nothing], cc_aut_G_l3Gl2G_2, us_aut_G_l3Gl2G_2!) + cc_aut_G_l3Gl2G_1(A::LHA, S::StateLHA) = - !istrue(S["in"]) && - S.time >= A.constants.t2 + !istrue(S[:in]) && + S.time >= A.constants[:t2] us_aut_G_l3Gl2G_1!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l2G") + (S.loc = :l2G) edge1 = Edge([nothing], cc_aut_G_l3Gl2G_1, us_aut_G_l3Gl2G_1!) - map_edges[tuple] = [edge1, edge2] + map_edges[:l3G][:l2G] = [edge1, edge2] # l4G loc - tuple = ("l4G", "l1G") + tuple = (:l4G, :l1G) cc_aut_G_l4Gl1G_1(A::LHA, S::StateLHA) = true us_aut_G_l4Gl1G_1!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l1G"; - 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_G); - S["in"] = true; - S["isabs"] = m.isabsorbing(m.p,x)) + (S.loc = :l1G; + 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_G); + S[:in] = true; + S[:isabs] = m.isabsorbing(m.p,x)) edge1 = Edge(["ALL"], cc_aut_G_l4Gl1G_1, us_aut_G_l4Gl1G_1!) - map_edges[tuple] = [edge1] + + map_edges[:l4G][:l1G] = [edge1] - tuple = ("l4G", "l2G") + tuple = (:l4G, :l2G) cc_aut_G_l4Gl2G_1(A::LHA, S::StateLHA) = - (S.time >= A.constants.t2) + (S.time >= A.constants[:t2]) us_aut_G_l4Gl2G_1!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l2G"; - S["d"] += S["tprime"] * min(abs(A.constants.x1 - S["n"]), abs(A.constants.x2 - S["n"])); - S["tprime"] = 0.0) + (S.loc = :l2G; + 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_l4Gl2G_1, us_aut_G_l4Gl2G_1!) - - map_edges[tuple] = [edge1] + + map_edges[:l4G][:l2G] = [edge1] # Connection between the two automata: l2G => l1F - tuple = ("l2G", "l1F") + tuple = (:l2G, :l1F) cc_aut_F_l2Gl1F_1(A::LHA, S::StateLHA) = true us_aut_F_l2Gl1F_1!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l1F"; - S["n"] = get_value(A, x, str_obs_F); - S["dprime"] = Inf; - S["isabs"] = m.isabsorbing(m.p,x)) + (S.loc = :l1F; + S[:n] = get_value(A, x, str_obs_F); + S[:dprime] = Inf; + S[:isabs] = m.isabsorbing(m.p,x)) edge1 = Edge([nothing], cc_aut_F_l2Gl1F_1, us_aut_F_l2Gl1F_1!) - map_edges[tuple] = [edge1] + map_edges[:l2G][:l1F] = [edge1] # l1F loc : we construct the edges of the form l1F => (..) - tuple = ("l1F", "l2F") + tuple = (:l1F, :l2F) cc_aut_F_l1Fl2F_1(A::LHA, S::StateLHA) = - S.time >= A.constants.t3 && - (A.constants.x3 <= S["n"] <= A.constants.x4) + S.time >= A.constants[:t3] && + (A.constants[:x3] <= S[:n] <= A.constants[:x4]) us_aut_F_l1Fl2F_1!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l2F"; - S["dprime"] = 0) + (S.loc = :l2F; + S[:dprime] = 0) edge1 = Edge([nothing], cc_aut_F_l1Fl2F_1, us_aut_F_l1Fl2F_1!) cc_aut_F_l1Fl2F_4(A::LHA, S::StateLHA) = - S.time >= A.constants.t3 && - S["dprime"] == 0 + S.time >= A.constants[:t3] && + S[:dprime] == 0 us_aut_F_l1Fl2F_4!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l2F") + (S.loc = :l2F) edge4 = Edge([nothing], cc_aut_F_l1Fl2F_4, us_aut_F_l1Fl2F_4!) cc_aut_F_l1Fl2F_2(A::LHA, S::StateLHA) = - (S.time >= A.constants.t4) && - (S["n"] < A.constants.x3 || S["n"] > A.constants.x4) + (S.time >= A.constants[:t4]) && + (S[:n] < A.constants[:x3] || S[:n] > A.constants[:x4]) us_aut_F_l1Fl2F_2!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l2F"; - S["dprime"] = min(abs(S["n"] - A.constants.x3), abs(S["n"] - A.constants.x4)); - S["d"] += S["dprime"]) + (S.loc = :l2F; + S[:dprime] = min(abs(S[:n] - A.constants[:x3]), abs(S[:n] - A.constants[:x4])); + S[:d] += S[:dprime]) edge2 = Edge([nothing], cc_aut_F_l1Fl2F_2, us_aut_F_l1Fl2F_2!) cc_aut_F_l1Fl2F_3(A::LHA, S::StateLHA) = - istrue(S["isabs"]) && S.time <= A.constants.t4 + istrue(S[:isabs]) && S.time <= A.constants[:t4] us_aut_F_l1Fl2F_3!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l2F"; - S["d"] += S["dprime"]) + (S.loc = :l2F; + S[:d] += S[:dprime]) edge3 = Edge([nothing], cc_aut_F_l1Fl2F_3, us_aut_F_l1Fl2F_3!) - map_edges[tuple] = [edge1, edge2, edge3, edge4] + map_edges[:l1F][:l2F] = [edge1, edge4, edge3, edge2] - tuple = ("l1F", "l3F") + tuple = (:l1F, :l3F) cc_aut_F_l1Fl3F_1(A::LHA, S::StateLHA) = - (A.constants.x3 <= S["n"] <= A.constants.x4) + (A.constants[:x3] <= S[:n] <= A.constants[:x4]) us_aut_F_l1Fl3F_1!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l3F"; - S["dprime"] = 0;) + (S.loc = :l3F; + S[:dprime] = 0;) edge1 = Edge([nothing], cc_aut_F_l1Fl3F_1, us_aut_F_l1Fl3F_1!) cc_aut_F_l1Fl3F_2(A::LHA, S::StateLHA) = - (S["n"] < A.constants.x3 || S["n"] > A.constants.x4) && - (S.time <= A.constants.t3) + (S[:n] < A.constants[:x3] || S[:n] > A.constants[:x4]) && + (S.time <= A.constants[:t3]) us_aut_F_l1Fl3F_2!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l3F"; - S["dprime"] = min(sqrt((S.time - A.constants.t3)^2 + (S["n"] - A.constants.x4)^2), - sqrt((S.time - A.constants.t3)^2 + (S["n"] - A.constants.x3)^2))) + (S.loc = :l3F; + S[:dprime] = min(sqrt((S.time - A.constants[:t3])^2 + (S[:n] - A.constants[:x4])^2), + sqrt((S.time - A.constants[:t3])^2 + (S[:n] - A.constants[:x3])^2))) edge2 = Edge([nothing], cc_aut_F_l1Fl3F_2, us_aut_F_l1Fl3F_2!) cc_aut_F_l1Fl3F_3(A::LHA, S::StateLHA) = - (S["n"] < A.constants.x3 || S["n"] > A.constants.x4) && - (A.constants.t3 <= S.time <= A.constants.t4) + (S[:n] < A.constants[:x3] || S[:n] > A.constants[:x4]) && + (A.constants[:t3] <= S.time <= A.constants[:t4]) us_aut_F_l1Fl3F_3!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l3F"; - S["dprime"] = min(S["dprime"], min(abs(S["n"] - A.constants.x3), abs(S["n"] - A.constants.x4)))) + (S.loc = :l3F; + S[:dprime] = min(S[:dprime], min(abs(S[:n] - A.constants[:x3]), abs(S[:n] - A.constants[:x4])))) edge3 = Edge([nothing], cc_aut_F_l1Fl3F_3, us_aut_F_l1Fl3F_3!) - map_edges[tuple] = [edge1, edge2, edge3] + + map_edges[:l1F][:l3F] = [edge1, edge2, edge3] # l3F loc - tuple = ("l3F", "l1F") + tuple = (:l3F, :l1F) cc_aut_F_l3Fl1F_1(A::LHA, S::StateLHA) = true us_aut_F_l3Fl1F_1!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l1F"; - S["n"] = get_value(A, x, str_obs_F); - S["isabs"] = m.isabsorbing(m.p,x)) + (S.loc = :l1F; + S[:n] = get_value(A, x, str_obs_F); + S[:isabs] = m.isabsorbing(m.p,x)) edge1 = Edge(["ALL"], cc_aut_F_l3Fl1F_1, us_aut_F_l3Fl1F_1!) - tuple = ("l3F", "l2F") + + map_edges[:l3F][:l1F] = [edge1] + + tuple = (:l3F, :l2F) cc_aut_F_l3Fl2F_1(A::LHA, S::StateLHA) = - (S.time >= A.constants.t4) + (S.time >= A.constants[:t4]) us_aut_F_l3Fl2F_1!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l2F") - edge2 = Edge([nothing], cc_aut_F_l3Fl2F_1, us_aut_F_l3Fl2F_1!) - map_edges[tuple] = [edge1, edge2] + (S.loc = :l2F) + edge1 = Edge([nothing], cc_aut_F_l3Fl2F_1, us_aut_F_l3Fl2F_1!) + + map_edges[:l3F][:l2F] = [edge1] ## Constants - constants = (x1 = x1, x2 = x2, t1 = t1, t2 = t2, - x3 = x3, x4 = x4, t3 = t3, t4 = t4) + constants = Dict{Symbol,Float64}(:x1 => x1, :x2 => x2, :t1 => t1, :t2 => t2, + :x3 => x3, :x4 => x4, :t3 => t3, :t4 => t4) A = LHA(m.transitions, locations, Λ_F, locations_init, locations_final, map_var_automaton_idx, flow, map_edges, constants, m.map_var_idx) diff --git a/core/common.jl b/core/common.jl index 3687ff7e0522422b12a0f67611d8b80285f1d243..1cac6188991537f583efef5b19cd5b03c8ff8982 100644 --- a/core/common.jl +++ b/core/common.jl @@ -6,22 +6,24 @@ abstract type Model end abstract type AbstractTrajectory end const Transition = Union{String,Nothing} -const Location = String -const VariableAutomaton = String +const Location = Symbol +const VariableAutomaton = Symbol +const VariableModel = String +const ParameterModel = String mutable struct ContinuousTimeModel <: Model name::String dim_state::Int # state space dim dim_params::Int # parameter space dim - map_var_idx::Dict{String,Int} # maps variable str to index in the state space - _map_obs_var_idx::Dict{String,Int} # maps variable str to index in the observed state space - map_param_idx::Dict{String,Int} # maps parameter str to index in the parameter space - transitions::Vector{Transition} + map_var_idx::Dict{VariableModel,Int} # maps variable str to index in the state space + _map_obs_var_idx::Dict{VariableModel,Int} # maps variable str to index in the observed state space + map_param_idx::Dict{ParameterModel,Int} # maps parameter str to index in the parameter space + transitions::Vector{<:Transition} p::Vector{Float64} x0::Vector{Int} t0::Float64 f!::Function - g::Vector{String} # of dimension dim_obs_state + g::Vector{VariableModel} # of dimension dim_obs_state _g_idx::Vector{Int} # of dimension dim_obs_state isabsorbing::Function time_bound::Float64 @@ -33,26 +35,26 @@ struct Trajectory <: AbstractTrajectory m::ContinuousTimeModel values::Vector{Vector{Int}} times::Vector{Float64} - transitions::Vector{Transition} + transitions::Vector{<:Transition} end struct Edge - transitions::Vector{Transition} + transitions::Vector{<:Transition} check_constraints::Function update_state!::Function end struct LHA - transitions::Vector{Transition} + transitions::Vector{<:Transition} locations::Vector{Location} Λ::Dict{Location,Function} locations_init::Vector{Location} locations_final::Vector{Location} map_var_automaton_idx::Dict{VariableAutomaton,Int} # nvar keys : str_var => idx in values flow::Dict{Location,Vector{Float64}} # output of length nvar - map_edges::Dict{Tuple{Location,Location},Vector{Edge}} - constants::NamedTuple - map_var_model_idx::Dict{String,Int} # of dim d (of a model) + map_edges::Dict{Location, Dict{Location,Vector{Edge}}} + constants::Dict{Symbol,Float64} + map_var_model_idx::Dict{VariableModel,Int} # of dim d (of a model) end mutable struct StateLHA @@ -72,21 +74,21 @@ struct SynchronizedTrajectory <: AbstractTrajectory sm::SynchronizedModel values::Vector{Vector{Int}} times::Vector{Float64} - transitions::Vector{Transition} + transitions::Vector{<:Transition} end struct ParametricModel m::Model - params::Vector{String} + params::Vector{ParameterModel} distribution::Distribution _param_idx::Vector{Int} end # Constructors -function ContinuousTimeModel(dim_state::Int, dim_params::Int, map_var_idx::Dict, map_param_idx::Dict, transitions::Vector{String}, +function ContinuousTimeModel(dim_state::Int, dim_params::Int, map_var_idx::Dict, map_param_idx::Dict, transitions::Vector{<:Transition}, p::Vector{Float64}, x0::Vector{Int}, t0::Float64, f!::Function, isabsorbing::Function; - g::Vector{String} = keys(map_var_idx), time_bound::Float64 = Inf, + g::Vector{VariableModel} = keys(map_var_idx), time_bound::Float64 = Inf, buffer_size::Int = 10, estim_min_states::Int = 50, name::String = "Unnamed") dim_obs_state = length(g) _map_obs_var_idx = Dict() @@ -108,15 +110,15 @@ function ContinuousTimeModel(dim_state::Int, dim_params::Int, map_var_idx::Dict, return new_model end -LHA(A::LHA, map_var::Dict{String,Int}) = LHA(A.transitions, A.locations, A.Λ, +LHA(A::LHA, map_var::Dict{VariableModel,Int}) = LHA(A.transitions, A.locations, A.Λ, A.locations_init, A.locations_final, A.map_var_automaton_idx, A.flow, A.map_edges, A.constants, map_var) Base.:*(m::ContinuousTimeModel, A::LHA) = SynchronizedModel(m, A) Base.:*(A::LHA, m::ContinuousTimeModel) = SynchronizedModel(m, A) -function ParametricModel(am::Model, priors::Tuple{String,UnivariateDistribution}...) +function ParametricModel(am::Model, priors::Tuple{ParameterModel,UnivariateDistribution}...) m = get_proba_model(am) - params = String[] + params = ParameterModel[] distributions = Distribution{Univariate,Continuous}[] _param_idx = zeros(Int, 0) for prior in priors @@ -131,7 +133,7 @@ function ParametricModel(am::Model, priors::Tuple{String,UnivariateDistribution} return ParametricModel(am, params, product_distribution(distributions), _param_idx) end -function ParametricModel(am::Model, params::Vector{String}, distribution::MultivariateDistribution) +function ParametricModel(am::Model, params::Vector{ParameterModel}, distribution::MultivariateDistribution) m = get_proba_model(am) _param_idx = zeros(Int, 0) for str_p in params diff --git a/core/lha.jl b/core/lha.jl index 81c4387c2e31dfe83256c4cdbd5dc85a1bfac4bd..412b8809627210a82585884fb5e77f5152d166ed 100644 --- a/core/lha.jl +++ b/core/lha.jl @@ -4,7 +4,9 @@ get_value(A::LHA, x::Vector{Int}, var::String) = x[A.map_var_model_idx[var]] copy(S::StateLHA) = StateLHA(S.A, S.loc, S.values, S.time) # Not overring getproperty, setproperty to avoid a conversion Symbol => String for the dict key -getindex(S::StateLHA, var::VariableAutomaton) = (S.values)[(S.A).map_var_automaton_idx[var]] +function getindex(S::StateLHA, var::VariableAutomaton) + return (S.values)[(S.A).map_var_automaton_idx[var]] +end getindex(S::StateLHA, l_var::Vector{VariableAutomaton}) = [S[var] for var in l_var] setindex!(S::StateLHA, val::Float64, var::VariableAutomaton) = (S.values)[(S.A).map_var_automaton_idx[var]] = val @@ -46,7 +48,7 @@ isaccepted(S::StateLHA) = (S.loc in (S.A).locations_final) # Methods for synchronize / read the trajectory function init_state(A::LHA, x0::Vector{Int}, t0::Float64) - S0 = StateLHA(A, "", zeros(length_var(A)), t0) + S0 = StateLHA(A, :init, zeros(length_var(A)), t0) for loc in A.locations_init if A.Λ[loc](A,S0) S0.loc = loc @@ -56,30 +58,41 @@ function init_state(A::LHA, x0::Vector{Int}, t0::Float64) return S0 end +function _push_edge!(edge_candidates::Vector{Edge}, edge::Edge, nbr_candidates::Int) + if nbr_candidates < 2 + edge_candidates[nbr_candidates+1] = edge + else + push!(edge_candidates, edge) + end +end + function _find_edge_candidates!(edge_candidates::Vector{Edge}, current_loc::Location, A::LHA, Snplus1::StateLHA, only_asynchronous::Bool) - for loc in A.locations - tuple_edges = (current_loc, loc) - if haskey(A.map_edges, tuple_edges) - for edge in A.map_edges[tuple_edges] - if edge.check_constraints(A, Snplus1) - if edge.transitions[1] == nothing - push!(edge_candidates, edge) - end - if !only_asynchronous && edge.transitions[1] != nothing - push!(edge_candidates, edge) - end + nbr_candidates = 0 + edges_from_current_loc = A.map_edges[current_loc] + for target_loc in keys(edges_from_current_loc) + for edge in edges_from_current_loc[target_loc] + if edge.check_constraints(A, Snplus1) + if edge.transitions[1] == nothing + _push_edge!(edge_candidates, edge, nbr_candidates) + nbr_candidates += 1 + return nbr_candidates + end + if !only_asynchronous && edge.transitions[1] != nothing + _push_edge!(edge_candidates, edge, nbr_candidates) + nbr_candidates += 1 end end end end + return nbr_candidates end -function _get_edge_index(edge_candidates::Vector{Edge}, +function _get_edge_index(edge_candidates::Vector{Edge}, nbr_candidates::Int, detected_event::Bool, tr_nplus1::Transition) ind_edge = 0 bool_event = detected_event - for i in eachindex(edge_candidates) + for i = 1:nbr_candidates edge = edge_candidates[i] # Asynchronous edge detection: we fire it if edge.transitions[1] == nothing @@ -87,7 +100,7 @@ function _get_edge_index(edge_candidates::Vector{Edge}, end # Synchronous detection if !detected_event && tr_nplus1 != nothing - if (length(edge.transitions) == 1 && edge.transitions[1] == "ALL") || + if (edge.transitions[1] == "ALL") || (tr_nplus1 in edge.transitions) ind_edge = i bool_event = true @@ -101,7 +114,7 @@ function next_state!(Snplus1::StateLHA, A::LHA, xnplus1::Vector{Int}, tnplus1::Float64, tr_nplus1::Transition, Sn::StateLHA; verbose::Bool = false) # En fait d'apres observation de Cosmos, après qu'on ait lu la transition on devrait stop. - edge_candidates = Edge[] + edge_candidates = Vector{Edge}(undef, 2) first_round::Bool = true detected_event::Bool = false turns = 0 @@ -117,14 +130,15 @@ function next_state!(Snplus1::StateLHA, A::LHA, # First, we check the asynchronous transitions while first_round || length(edge_candidates) > 0 turns += 1 - edge_candidates = empty!(edge_candidates) + #edge_candidates = empty!(edge_candidates) current_loc = Snplus1.loc # Save all edges that satisfies transition predicate (asynchronous ones) - _find_edge_candidates!(edge_candidates, current_loc, A, Snplus1, true) + nbr_candidates = _find_edge_candidates!(edge_candidates, current_loc, A, Snplus1, true) # Search the one we must chose, here the event is nothing because # we're not processing yet the next event - ind_edge, detected_event = _get_edge_index(edge_candidates, detected_event, nothing) + ind_edge, detected_event = _get_edge_index(edge_candidates, nbr_candidates, detected_event, nothing) # Update the state with the chosen one (if it exists) + # Should be xn here if ind_edge > 0 edge_candidates[ind_edge].update_state!(A, Snplus1, xnplus1) end @@ -132,7 +146,7 @@ function next_state!(Snplus1::StateLHA, A::LHA, if verbose @show turns @show edge_candidates - @show ind_edge, detected_event + @show ind_edge, detected_event, nbr_candidates println("After update") @show Snplus1 end @@ -171,17 +185,17 @@ function next_state!(Snplus1::StateLHA, A::LHA, first_round = true while first_round || length(edge_candidates) > 0 turns += 1 - edge_candidates = empty!(edge_candidates) + #edge_candidates = empty!(edge_candidates) current_loc = Snplus1.loc # Save all edges that satisfies transition predicate (synchronous ones) - _find_edge_candidates!(edge_candidates, current_loc, A, Snplus1, false) + nbr_candidates =_find_edge_candidates!(edge_candidates, current_loc, A, Snplus1, false) # Search the one we must chose - ind_edge, detected_event = _get_edge_index(edge_candidates, detected_event, tr_nplus1) + ind_edge, detected_event = _get_edge_index(edge_candidates, nbr_candidates, detected_event, tr_nplus1) # Update the state with the chosen one (if it exists) if verbose @show turns @show edge_candidates - @show ind_edge, detected_event + @show ind_edge, detected_event, nbr_candidates end if ind_edge > 0 edge_candidates[ind_edge].update_state!(A, Snplus1, xnplus1) diff --git a/core/model.jl b/core/model.jl index d99120eab18d70503c4251b56c51ab4560cf16a2..afdd0edcd3ca89eac276e7ebaf96d8e0a780cadd 100644 --- a/core/model.jl +++ b/core/model.jl @@ -341,17 +341,17 @@ end Distribute over workers the computation of the mean value of a LHA over `nbr_sim` simulations of the model. """ -function distribute_mean_value_lha(sm::SynchronizedModel, str_var::Union{String,Vector{String}}, nbr_sim::Int) +function distribute_mean_value_lha(sm::SynchronizedModel, sym_var::Union{VariableAutomaton,Vector{VariableAutomaton}}, nbr_sim::Int) sum_val = @distributed (+) for i = 1:nbr_sim - volatile_simulate(sm)[str_var] + volatile_simulate(sm)[sym_var] end return sum_val / nbr_sim end -function mean_value_lha(sm::SynchronizedModel, str_var::String, nbr_sim::Int) +function mean_value_lha(sm::SynchronizedModel, sym_var::VariableAutomaton, nbr_sim::Int) sum_val = 0.0 for i = 1:nbr_sim - sum_val += volatile_simulate(sm)[str_var] + sum_val += volatile_simulate(sm)[sym_var] end return sum_val / nbr_sim end diff --git a/tests/automata/read_trajectory_last_state_F.jl b/tests/automata/read_trajectory_last_state_F.jl index 2ad39be631c3a5692d7f9fbb00a3537953fbb36b..6076e49c822da2e8a58478c0197de4b691fc3c72 100644 --- a/tests/automata/read_trajectory_last_state_F.jl +++ b/tests/automata/read_trajectory_last_state_F.jl @@ -12,7 +12,7 @@ A_F = create_automaton_F(SIR, x1, x2, t1, t2, "I") # <: LHA function test_last_state(A::LHA, m::ContinuousTimeModel) σ = simulate(m) Send = read_trajectory(A, σ) - test = (get_state_from_time(σ, Send.time)[2] == Send["n"]) && (Send["d"] == 0) + test = (get_state_from_time(σ, Send.time)[2] == Send[:n]) && (Send[:d] == 0) if !test @show Send @show get_state_from_time(σ, Send.time) diff --git a/tests/automata/read_trajectory_last_state_G.jl b/tests/automata/read_trajectory_last_state_G.jl index 8578c0a8ef430bcf0817658156105985c7ec188d..93881442f7e98933c47cc1300be49cac2c494199 100644 --- a/tests/automata/read_trajectory_last_state_G.jl +++ b/tests/automata/read_trajectory_last_state_G.jl @@ -12,7 +12,7 @@ A_G = create_automaton_G(ER, x1, x2, t1, t2, "P") # <: LHA function test_last_state(A::LHA, m::ContinuousTimeModel) σ = simulate(m) Send = read_trajectory(A, σ) - test = (get_state_from_time(σ, Send.time)[4] == Send["n"]) && (Send["d"] == 0) + test = (get_state_from_time(σ, Send.time)[4] == Send[:n]) && (Send[:d] == 0) if !test @show Send @show get_state_from_time(σ, Send.time) diff --git a/tests/automata/sync_simulate_last_state_F.jl b/tests/automata/sync_simulate_last_state_F.jl index ae6ed61f2b6267cbf4b1fcb8e4dc3067246a940b..96fd11e8b822df3560c6c8630ad8fb6a1308a049 100644 --- a/tests/automata/sync_simulate_last_state_F.jl +++ b/tests/automata/sync_simulate_last_state_F.jl @@ -11,7 +11,7 @@ sync_SIR = A_F * SIR function test_last_state(A::LHA, m::SynchronizedModel) σ = simulate(m) - test = (get_state_from_time(σ, (σ.state_lha_end).time)[1] == (σ.state_lha_end)["n"]) && ((σ.state_lha_end)["d"] == 0) + test = (get_state_from_time(σ, (σ.state_lha_end).time)[1] == (σ.state_lha_end)[:n]) && ((σ.state_lha_end)[:d] == 0) if !test @show σ.state_lha_end @show times(σ)[end] @@ -19,7 +19,7 @@ function test_last_state(A::LHA, m::SynchronizedModel) @show times(σ)[end-1] @show σ[end-1] @show get_state_from_time(σ, (σ.state_lha_end).time)[1] - @show (σ.state_lha_end)["n"], (σ.state_lha_end)["d"] + @show (σ.state_lha_end)[:n], (σ.state_lha_end)[:d] error("Ouch") end return test diff --git a/tests/automata/sync_simulate_last_state_G.jl b/tests/automata/sync_simulate_last_state_G.jl index d05d3caed9d4a3053e8c05eef262806a300c5560..e7e9ba78774507d084c7219914ad31565fee3a15 100644 --- a/tests/automata/sync_simulate_last_state_G.jl +++ b/tests/automata/sync_simulate_last_state_G.jl @@ -11,7 +11,7 @@ sync_ER = A_G * ER function test_last_state(A::LHA, m::SynchronizedModel) σ = simulate(m) - test = (get_state_from_time(σ, (σ.state_lha_end).time)[1] == (σ.state_lha_end)["n"]) && ((σ.state_lha_end)["d"] == 0) + test = (get_state_from_time(σ, (σ.state_lha_end).time)[1] == (σ.state_lha_end)[:n]) && ((σ.state_lha_end)[:d] == 0) return test end diff --git a/tests/cosmos/distance_F/ER_1D.jl b/tests/cosmos/distance_F/ER_1D.jl index e95f0d0d851f74a2969eb6e1d04dc5fb54b43150..e1917f742d0ebac5cedba54ecbee9e069bf86b48 100644 --- a/tests/cosmos/distance_F/ER_1D.jl +++ b/tests/cosmos/distance_F/ER_1D.jl @@ -52,7 +52,7 @@ for exp in l_exp # MarkovProcesses estimation set_param!(ER, "k3", convert(Float64, k3)) sync_ER = ER*A_F - l_dist_pkg[i] = distribute_mean_value_lha(sync_ER, "d", nb_sim) + l_dist_pkg[i] = distribute_mean_value_lha(sync_ER, :d, nb_sim) nb_accepts_pkg = distribute_prob_accept_lha(sync_ER, nb_sim) #@info "About accepts" nb_sim nb_accepted nb_accepts_pkg test = isapprox(l_dist_cosmos[i], l_dist_pkg[i]; atol = width*1.01) || diff --git a/tests/cosmos/distance_G/ER_R5.jl b/tests/cosmos/distance_G/ER_R5.jl index db892d9c6fe919007ff5e0df6457717557e097ea..4820cfcc54ce9340f3fc36b4ae599e1bca16574b 100644 --- a/tests/cosmos/distance_G/ER_R5.jl +++ b/tests/cosmos/distance_G/ER_R5.jl @@ -47,7 +47,7 @@ for i = 1:nb_k1 set_param!(ER, "k1", convert(Float64, k1)) set_param!(ER, "k2", convert(Float64, k2)) sync_ER = ER*A_G - mat_dist_pkg[i,j] = distribute_mean_value_lha(sync_ER, "d", nb_sim) + mat_dist_pkg[i,j] = distribute_mean_value_lha(sync_ER, :d, nb_sim) nb_accepts_pkg = distribute_prob_accept_lha(sync_ER, nb_sim) #@info "About accepts" nb_sim nb_accepted nb_accepts_pkg test = isapprox(mat_dist_cosmos[i,j], mat_dist_pkg[i,j]; atol = width*1.01) diff --git a/tests/cosmos/distance_G_F/ER_R6.jl b/tests/cosmos/distance_G_F/ER_R6.jl index 6dd069fdc3bbcd42e6e56bbe030c788acfab88e7..da19cf0a48c10c773c8c40f355fe858281be9cc1 100644 --- a/tests/cosmos/distance_G_F/ER_R6.jl +++ b/tests/cosmos/distance_G_F/ER_R6.jl @@ -51,7 +51,7 @@ for i = 1:nb_k1 set_param!(ER, "k1", convert(Float64, k1)) set_param!(ER, "k2", convert(Float64, k2)) sync_ER = ER*A_G_F - mat_dist_pkg[i,j], mat_dist_prime_pkg[i,j] = distribute_mean_value_lha(sync_ER, ["d","dprime"], nb_sim) + mat_dist_pkg[i,j], mat_dist_prime_pkg[i,j] = distribute_mean_value_lha(sync_ER, [:d,:dprime], nb_sim) nb_accepts_pkg = distribute_prob_accept_lha(sync_ER, nb_sim) #@info "Computed distances" mat_dist_pkg[i,j] mat_dist_prime_pkg[i,j] mat_dist_cosmos[i,j] mat_dist_prime_cosmos[i,j] #@info "About accepts" nb_sim nb_accepted nb_accepts_pkg