From 575ef32473760b7cfa15f81c225cb76e058b6368 Mon Sep 17 00:00:00 2001 From: Mahmoud Bentriou <mahmoud.bentriou@centralesupelec.fr> Date: Sat, 23 Jan 2021 04:38:18 +0100 Subject: [PATCH] 1) LHA now have names. 2) Period automaton executes well and was runned on the doping 3way oscillator model. Not stattistically tested yet --- automata/automaton_F.jl | 70 ++++++------- automata/automaton_G.jl | 2 +- automata/automaton_G_and_F.jl | 178 +++++++++++++++++----------------- core/common.jl | 4 +- core/lha.jl | 6 +- 5 files changed, 131 insertions(+), 129 deletions(-) diff --git a/automata/automaton_F.jl b/automata/automaton_F.jl index caea4d0..4c8dc99 100644 --- a/automata/automaton_F.jl +++ b/automata/automaton_F.jl @@ -37,97 +37,97 @@ function create_automaton_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1 # l0 loc : we construct the edges of the form l0 => (..) # "cc" as check_constraints tuple = (:l0, :l1) - cc_aut_F_l0l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true - us_aut_F_l0l1_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l0l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true + @everywhere us_aut_F_l0l1_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l1; - S[:n] = get_value(S, x, sym_obs); + S[:n] = get_value(S, x, $(Meta.quot(sym_obs))); S[:d] = Inf; - S[:isabs] = getfield(Main, sym_isabs_func)(p, x)) - edge1 = Edge([nothing], cc_aut_F_l0l1_1, us_aut_F_l0l1_1!) + S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x)) + edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l0l1_1), getfield(Main, :us_aut_F_l0l1_1!)) map_edges[:l0][:l1] = [edge1] # l1 loc : we construct the edges of the form l1 => (..) tuple = (:l1, :l2) - cc_aut_F_l1l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l1l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = getfield(S, :time) >= constants[:t1] && (constants[:x1] <= S[:n] <= constants[:x2]) - us_aut_F_l1l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l1l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2; S[:d] = 0) - edge1 = Edge([nothing], cc_aut_F_l1l2_1, us_aut_F_l1l2_1!) + edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l1l2_1), getfield(Main, :us_aut_F_l1l2_1!)) - cc_aut_F_l1l2_4(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l1l2_4(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = getfield(S, :time) >= constants[:t1] && S[:d] == 0 - us_aut_F_l1l2_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l1l2_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2) - edge4 = Edge([nothing], cc_aut_F_l1l2_4, us_aut_F_l1l2_4!) + edge4 = Edge([nothing], getfield(Main, :cc_aut_F_l1l2_4), getfield(Main, :us_aut_F_l1l2_4!)) - cc_aut_F_l1l2_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l1l2_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (getfield(S, :time) >= constants[:t2]) && (S[:n] < constants[:x1] || S[:n] > constants[:x2]) - us_aut_F_l1l2_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l1l2_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2; S[:d] = min(abs(S[:n] - constants[:x1]), abs(S[:n] - constants[:x2]))) - edge2 = Edge([nothing], cc_aut_F_l1l2_2, us_aut_F_l1l2_2!) + edge2 = Edge([nothing], getfield(Main, :cc_aut_F_l1l2_2), getfield(Main, :us_aut_F_l1l2_2!)) - cc_aut_F_l1l2_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l1l2_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = istrue(S[:isabs]) && getfield(S, :time) <= constants[:t2] - us_aut_F_l1l2_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l1l2_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2) - edge3 = Edge([nothing], cc_aut_F_l1l2_3, us_aut_F_l1l2_3!) + edge3 = Edge([nothing], getfield(Main, :cc_aut_F_l1l2_3), getfield(Main, :us_aut_F_l1l2_3!)) map_edges[:l1][:l2] = [edge1, edge2, edge3, edge4] tuple = (:l1, :l3) - cc_aut_F_l1l3_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l1l3_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (constants[:x1] <= S[:n] <= constants[:x2]) - us_aut_F_l1l3_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l1l3_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l3; S[:d] = 0;) - edge1 = Edge([nothing], cc_aut_F_l1l3_1, us_aut_F_l1l3_1!) + edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l1l3_1), getfield(Main, :us_aut_F_l1l3_1!)) - cc_aut_F_l1l3_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l1l3_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S[:n] < constants[:x1] || S[:n] > constants[:x2]) && (getfield(S, :time) <= constants[:t1]) - us_aut_F_l1l3_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l1l3_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l3; S[:d] = min(sqrt((getfield(S, :time) - constants[:t1])^2 + (S[:n] - constants[:x2])^2), sqrt((getfield(S, :time) - constants[:t1])^2 + (S[:n] - constants[:x1])^2))) - edge2 = Edge([nothing], cc_aut_F_l1l3_2, us_aut_F_l1l3_2!) + edge2 = Edge([nothing], getfield(Main, :cc_aut_F_l1l3_2), getfield(Main, :us_aut_F_l1l3_2!)) - cc_aut_F_l1l3_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l1l3_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S[:n] < constants[:x1] || S[:n] > constants[:x2]) && (constants[:t1] <= getfield(S, :time) <= constants[:t2]) - us_aut_F_l1l3_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l1l3_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l3; S[:d] = min(S[:d], min(abs(S[:n] - constants[:x1]), abs(S[:n] - constants[:x2])))) - edge3 = Edge([nothing], cc_aut_F_l1l3_3, us_aut_F_l1l3_3!) + edge3 = Edge([nothing], getfield(Main, :cc_aut_F_l1l3_3), getfield(Main, :us_aut_F_l1l3_3!)) map_edges[:l1][:l3] = [edge1, edge2, edge3] # l3 loc tuple = (:l3, :l1) - cc_aut_F_l3l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true - us_aut_F_l3l1_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l3l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true + @everywhere us_aut_F_l3l1_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l1; - S[:n] = get_value(S, x, sym_obs); - S[:isabs] = getfield(Main, sym_isabs_func)(p, x)) - edge1 = Edge([:ALL], cc_aut_F_l3l1_1, us_aut_F_l3l1_1!) + S[:n] = get_value(S, x, $(Meta.quot(sym_obs))); + S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x)) + edge1 = Edge([:ALL], getfield(Main, :cc_aut_F_l3l1_1), getfield(Main, :us_aut_F_l3l1_1!)) map_edges[:l3][:l1] = [edge1] tuple = (:l3, :l2) - cc_aut_F_l3l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l3l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (getfield(S, :time) >= constants[:t2]) - us_aut_F_l3l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l3l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2) - edge1 = Edge([nothing], cc_aut_F_l3l2_1, us_aut_F_l3l2_1!) + edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l3l2_1), getfield(Main, :us_aut_F_l3l2_1!)) map_edges[:l3][:l2] = [edge1] ## Constants constants = Dict{Symbol,Float64}(:x1 => x1, :x2 => x2, :t1 => t1, :t2 => t2) - A = LHA(m.transitions, locations, Λ_F, locations_init, locations_final, + A = LHA("F property", m.transitions, locations, Λ_F, locations_init, locations_final, map_var_automaton_idx, flow, map_edges, constants, m.map_var_idx) return A end diff --git a/automata/automaton_G.jl b/automata/automaton_G.jl index e0d2bce..2bbc48b 100644 --- a/automata/automaton_G.jl +++ b/automata/automaton_G.jl @@ -195,7 +195,7 @@ function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1 ## Constants constants = Dict{Symbol,Float64}(:x1 => x1, :x2 => x2, :t1 => t1, :t2 => t2) - A = LHA(m.transitions, locations, Λ_F, locations_init, locations_final, + A = LHA("G property", m.transitions, locations, Λ_F, locations_init, locations_final, map_var_automaton_idx, flow, map_edges, constants, m.map_var_idx) return A diff --git a/automata/automaton_G_and_F.jl b/automata/automaton_G_and_F.jl index f17caf2..346976c 100644 --- a/automata/automaton_G_and_F.jl +++ b/automata/automaton_G_and_F.jl @@ -46,253 +46,253 @@ function create_automaton_G_and_F(m::ContinuousTimeModel, x1::Float64, x2::Float # l0G loc tuple = (:l0G, :l1G) - cc_aut_G_l0Gl1G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true - us_aut_G_l0Gl1G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_G_l0Gl1G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true + @everywhere us_aut_G_l0Gl1G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l1G; S[:d] = 0; - S[:n] = get_value(S, x, sym_obs_G); + S[:n] = get_value(S, x, $(Meta.quot(sym_obs_G))); S[:in] = true; - S[:isabs] = getfield(Main, sym_isabs_func)(p, x)) - edge1 = Edge([nothing], cc_aut_G_l0Gl1G_1, us_aut_G_l0Gl1G_1!) + S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x)) + edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l0Gl1G_1), getfield(Main, :us_aut_G_l0Gl1G_1!)) map_edges[:l0G][:l1G] = [edge1] # l1G loc tuple = (:l1G, :l3G) - cc_aut_G_l1Gl3G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_G_l1Gl3G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = getfield(S, :time) <= constants[:t1] && S[:n] < constants[:x1] || S[:n] > constants[:x2] - us_aut_G_l1Gl3G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_G_l1Gl3G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l3G; S[:d] = min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])); S[:in] = false) - edge1 = Edge([nothing], cc_aut_G_l1Gl3G_1, us_aut_G_l1Gl3G_1!) + edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l1Gl3G_1), getfield(Main, :us_aut_G_l1Gl3G_1!)) - cc_aut_G_l1Gl3G_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_G_l1Gl3G_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = !istrue(S[:in]) && (constants[:t1] <= getfield(S, :time) <= constants[:t2]) && (constants[:x1] <= S[:n] <= constants[:x2]) - us_aut_G_l1Gl3G_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_G_l1Gl3G_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l3G; S[:d] = S[:d] * (getfield(S, :time) - constants[:t1]); S[:tprime] = 0.0) - edge3 = Edge([nothing], cc_aut_G_l1Gl3G_3, us_aut_G_l1Gl3G_3!) + edge3 = Edge([nothing], getfield(Main, :cc_aut_G_l1Gl3G_3), getfield(Main, :us_aut_G_l1Gl3G_3!)) - cc_aut_G_l1Gl3G_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_G_l1Gl3G_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (getfield(S, :time) <= constants[:t1]) && (constants[:x1] <= S[:n] <= constants[:x2]) - us_aut_G_l1Gl3G_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_G_l1Gl3G_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l3G; S[:d] = 0; S[:in] = false) - edge2 = Edge([nothing], cc_aut_G_l1Gl3G_2, us_aut_G_l1Gl3G_2!) + edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l1Gl3G_2), getfield(Main, :us_aut_G_l1Gl3G_2!)) - cc_aut_G_l1Gl3G_4(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_G_l1Gl3G_4(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = istrue(S[:in]) && (constants[:t1] <= getfield(S, :time) <= constants[:t2]) && (constants[:x1] <= S[:n] <= constants[:x2]) - us_aut_G_l1Gl3G_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_G_l1Gl3G_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l3G; S[:tprime] = 0.0) - edge4 = Edge([nothing], cc_aut_G_l1Gl3G_4, us_aut_G_l1Gl3G_4!) + edge4 = Edge([nothing], getfield(Main, :cc_aut_G_l1Gl3G_4), getfield(Main, :us_aut_G_l1Gl3G_4!)) map_edges[:l1G][:l3G] = [edge1, edge2, edge3, edge4] tuple = (:l1G, :l4G) - cc_aut_G_l1Gl4G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_G_l1Gl4G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = !istrue(S[:in]) && (constants[:t1] <= getfield(S, :time) <= constants[:t2]) && (S[:n] < constants[:x1] || S[:n] > constants[:x2]) - us_aut_G_l1Gl4G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_G_l1Gl4G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l4G; S[:d] += S[:d] * (getfield(S, :time) - constants[:t1])) - edge1 = Edge([nothing], cc_aut_G_l1Gl4G_1, us_aut_G_l1Gl4G_1!) + edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l1Gl4G_1), getfield(Main, :us_aut_G_l1Gl4G_1!)) - cc_aut_G_l1Gl4G_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_G_l1Gl4G_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = istrue(S[:in]) && (constants[:t1] <= getfield(S, :time) <= constants[:t2]) && (S[:n] < constants[:x1] || S[:n] > constants[:x2]) - us_aut_G_l1Gl4G_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_G_l1Gl4G_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l4G) - edge2 = Edge([nothing], cc_aut_G_l1Gl4G_2, us_aut_G_l1Gl4G_2!) + edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l1Gl4G_2), getfield(Main, :us_aut_G_l1Gl4G_2!)) map_edges[:l1G][:l4G] = [edge1, edge2] tuple = (:l1G, :l2G) - cc_aut_G_l1Gl2G_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_G_l1Gl2G_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = istrue(S[:isabs]) && getfield(S, :time) <= constants[:t1] - us_aut_G_l1Gl2G_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_G_l1Gl2G_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2G; S[:d] = (constants[:t2] - constants[:t1]) * min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n]))) - edge3 = Edge([nothing], cc_aut_G_l1Gl2G_3, us_aut_G_l1Gl2G_3!) - cc_aut_G_l1Gl2G_4(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + edge3 = Edge([nothing], getfield(Main, :cc_aut_G_l1Gl2G_3), getfield(Main, :us_aut_G_l1Gl2G_3!)) + @everywhere cc_aut_G_l1Gl2G_4(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = istrue(S[:isabs]) && (constants[:t1] <= getfield(S, :time) <= constants[:t2]) - us_aut_G_l1Gl2G_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_G_l1Gl2G_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2G; S[:d] += (constants[:t2] - getfield(S, :time)) * min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n]))) - edge4 = Edge([nothing], cc_aut_G_l1Gl2G_4, us_aut_G_l1Gl2G_4!) - cc_aut_G_l1Gl2G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + edge4 = Edge([nothing], getfield(Main, :cc_aut_G_l1Gl2G_4), getfield(Main, :us_aut_G_l1Gl2G_4!)) + @everywhere cc_aut_G_l1Gl2G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = istrue(S[:in]) && getfield(S, :time) >= constants[:t2] - us_aut_G_l1Gl2G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_G_l1Gl2G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2G) - edge1 = Edge([nothing], cc_aut_G_l1Gl2G_1, us_aut_G_l1Gl2G_1!) - cc_aut_G_l1Gl2G_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l1Gl2G_1), getfield(Main, :us_aut_G_l1Gl2G_1!)) + @everywhere cc_aut_G_l1Gl2G_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = !istrue(S[:in]) && getfield(S, :time) >= constants[:t2] - us_aut_G_l1Gl2G_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_G_l1Gl2G_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2G; S[:d] = S[:d] * (constants[:t2] - constants[:t1])) - edge2 = Edge([nothing], cc_aut_G_l1Gl2G_2, us_aut_G_l1Gl2G_2!) + edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l1Gl2G_2), getfield(Main, :us_aut_G_l1Gl2G_2!)) map_edges[:l1G][:l2G] = [edge3, edge4, edge1, edge2] # l3G loc tuple = (:l3G, :l1G) - cc_aut_G_l3Gl1G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true - us_aut_G_l3Gl1G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_G_l3Gl1G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true + @everywhere us_aut_G_l3Gl1G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l1G; - S[:n] = get_value(S, x, sym_obs_G); - S[:isabs] = getfield(Main, sym_isabs_func)(p, x)) - edge1 = Edge([:ALL], cc_aut_G_l3Gl1G_1, us_aut_G_l3Gl1G_1!) + S[:n] = get_value(S, x, $(Meta.quot(sym_obs_G))); + S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x)) + edge1 = Edge([:ALL], getfield(Main, :cc_aut_G_l3Gl1G_1), getfield(Main, :us_aut_G_l3Gl1G_1!)) map_edges[:l3G][:l1G] = [edge1] tuple = (:l3G, :l2G) - cc_aut_G_l3Gl2G_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_G_l3Gl2G_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = istrue(S[:in]) && getfield(S, :time) >= constants[:t2] - us_aut_G_l3Gl2G_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_G_l3Gl2G_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2G; S[:d] = S[:d] * (constants[:t2] - constants[:t1])) - edge2 = Edge([nothing], cc_aut_G_l3Gl2G_2, us_aut_G_l3Gl2G_2!) + edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l3Gl2G_2), getfield(Main, :us_aut_G_l3Gl2G_2!)) - cc_aut_G_l3Gl2G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_G_l3Gl2G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = !istrue(S[:in]) && getfield(S, :time) >= constants[:t2] - us_aut_G_l3Gl2G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_G_l3Gl2G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2G) - edge1 = Edge([nothing], cc_aut_G_l3Gl2G_1, us_aut_G_l3Gl2G_1!) + edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l3Gl2G_1), getfield(Main, :us_aut_G_l3Gl2G_1!)) map_edges[:l3G][:l2G] = [edge1, edge2] # l4G loc tuple = (:l4G, :l1G) - cc_aut_G_l4Gl1G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true - us_aut_G_l4Gl1G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_G_l4Gl1G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true + @everywhere us_aut_G_l4Gl1G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l1G; S[:d] += S[:tprime] * min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])); S[:tprime] = 0.0; - S[:n] = get_value(S, x, sym_obs_G); + S[:n] = get_value(S, x, $(Meta.quot(sym_obs_G))); S[:in] = true; - S[:isabs] = getfield(Main, sym_isabs_func)(p, x)) - edge1 = Edge([:ALL], cc_aut_G_l4Gl1G_1, us_aut_G_l4Gl1G_1!) + S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x)) + edge1 = Edge([:ALL], getfield(Main, :cc_aut_G_l4Gl1G_1), getfield(Main, :us_aut_G_l4Gl1G_1!)) map_edges[:l4G][:l1G] = [edge1] tuple = (:l4G, :l2G) - cc_aut_G_l4Gl2G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_G_l4Gl2G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (getfield(S, :time) >= constants[:t2]) - us_aut_G_l4Gl2G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_G_l4Gl2G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2G; S[:d] += S[:tprime] * min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])); S[:tprime] = 0.0) - edge1 = Edge([nothing], cc_aut_G_l4Gl2G_1, us_aut_G_l4Gl2G_1!) + edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l4Gl2G_1), getfield(Main, :us_aut_G_l4Gl2G_1!)) map_edges[:l4G][:l2G] = [edge1] # Connection between the two automata: l2G => l1F tuple = (:l2G, :l1F) - cc_aut_F_l2Gl1F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true - us_aut_F_l2Gl1F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l2Gl1F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true + @everywhere us_aut_F_l2Gl1F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l1F; - S[:n] = get_value(S, x, sym_obs_F); + S[:n] = get_value(S, x, $(Meta.quot(sym_obs_F))); S[:dprime] = Inf; - S[:isabs] = getfield(Main, sym_isabs_func)(p, x)) - edge1 = Edge([nothing], cc_aut_F_l2Gl1F_1, us_aut_F_l2Gl1F_1!) + S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x)) + edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l2Gl1F_1), getfield(Main, :us_aut_F_l2Gl1F_1!)) map_edges[:l2G][:l1F] = [edge1] # l1F loc : we construct the edges of the form l1F => (..) tuple = (:l1F, :l2F) - cc_aut_F_l1Fl2F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l1Fl2F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = getfield(S, :time) >= constants[:t3] && (constants[:x3] <= S[:n] <= constants[:x4]) - us_aut_F_l1Fl2F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l1Fl2F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2F; S[:dprime] = 0) - edge1 = Edge([nothing], cc_aut_F_l1Fl2F_1, us_aut_F_l1Fl2F_1!) + edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l1Fl2F_1), getfield(Main, :us_aut_F_l1Fl2F_1!)) - cc_aut_F_l1Fl2F_4(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l1Fl2F_4(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = getfield(S, :time) >= constants[:t3] && S[:dprime] == 0 - us_aut_F_l1Fl2F_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l1Fl2F_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2F) - edge4 = Edge([nothing], cc_aut_F_l1Fl2F_4, us_aut_F_l1Fl2F_4!) + edge4 = Edge([nothing], getfield(Main, :cc_aut_F_l1Fl2F_4), getfield(Main, :us_aut_F_l1Fl2F_4!)) - cc_aut_F_l1Fl2F_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l1Fl2F_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (getfield(S, :time) >= constants[:t4]) && (S[:n] < constants[:x3] || S[:n] > constants[:x4]) - us_aut_F_l1Fl2F_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l1Fl2F_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2F; S[:dprime] = min(abs(S[:n] - constants[:x3]), abs(S[:n] - constants[:x4])); S[:d] += S[:dprime]) - edge2 = Edge([nothing], cc_aut_F_l1Fl2F_2, us_aut_F_l1Fl2F_2!) + edge2 = Edge([nothing], getfield(Main, :cc_aut_F_l1Fl2F_2), getfield(Main, :us_aut_F_l1Fl2F_2!)) - cc_aut_F_l1Fl2F_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l1Fl2F_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = istrue(S[:isabs]) && getfield(S, :time) <= constants[:t4] - us_aut_F_l1Fl2F_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l1Fl2F_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2F; S[:d] += S[:dprime]) - edge3 = Edge([nothing], cc_aut_F_l1Fl2F_3, us_aut_F_l1Fl2F_3!) + edge3 = Edge([nothing], getfield(Main, :cc_aut_F_l1Fl2F_3), getfield(Main, :us_aut_F_l1Fl2F_3!)) map_edges[:l1F][:l2F] = [edge1, edge4, edge3, edge2] tuple = (:l1F, :l3F) - cc_aut_F_l1Fl3F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l1Fl3F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (constants[:x3] <= S[:n] <= constants[:x4]) - us_aut_F_l1Fl3F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l1Fl3F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l3F; S[:dprime] = 0;) - edge1 = Edge([nothing], cc_aut_F_l1Fl3F_1, us_aut_F_l1Fl3F_1!) + edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l1Fl3F_1), getfield(Main, :us_aut_F_l1Fl3F_1!)) - cc_aut_F_l1Fl3F_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l1Fl3F_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S[:n] < constants[:x3] || S[:n] > constants[:x4]) && (getfield(S, :time) <= constants[:t3]) - us_aut_F_l1Fl3F_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l1Fl3F_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l3F; S[:dprime] = min(sqrt((getfield(S, :time) - constants[:t3])^2 + (S[:n] - constants[:x4])^2), sqrt((getfield(S, :time) - constants[:t3])^2 + (S[:n] - constants[:x3])^2))) - edge2 = Edge([nothing], cc_aut_F_l1Fl3F_2, us_aut_F_l1Fl3F_2!) + edge2 = Edge([nothing], getfield(Main, :cc_aut_F_l1Fl3F_2), getfield(Main, :us_aut_F_l1Fl3F_2!)) - cc_aut_F_l1Fl3F_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l1Fl3F_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S[:n] < constants[:x3] || S[:n] > constants[:x4]) && (constants[:t3] <= getfield(S, :time) <= constants[:t4]) - us_aut_F_l1Fl3F_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l1Fl3F_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l3F; S[:dprime] = min(S[:dprime], min(abs(S[:n] - constants[:x3]), abs(S[:n] - constants[:x4])))) - edge3 = Edge([nothing], cc_aut_F_l1Fl3F_3, us_aut_F_l1Fl3F_3!) + edge3 = Edge([nothing], getfield(Main, :cc_aut_F_l1Fl3F_3), getfield(Main, :us_aut_F_l1Fl3F_3!)) map_edges[:l1F][:l3F] = [edge1, edge2, edge3] # l3F loc tuple = (:l3F, :l1F) - cc_aut_F_l3Fl1F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true - us_aut_F_l3Fl1F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l3Fl1F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true + @everywhere us_aut_F_l3Fl1F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l1F; - S[:n] = get_value(S, x, sym_obs_F); - S[:isabs] = getfield(Main, sym_isabs_func)(p, x)) - edge1 = Edge([:ALL], cc_aut_F_l3Fl1F_1, us_aut_F_l3Fl1F_1!) + S[:n] = get_value(S, x, $(Meta.quot(sym_obs_F))); + S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x)) + edge1 = Edge([:ALL], getfield(Main, :cc_aut_F_l3Fl1F_1), getfield(Main, :us_aut_F_l3Fl1F_1!)) map_edges[:l3F][:l1F] = [edge1] tuple = (:l3F, :l2F) - cc_aut_F_l3Fl2F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere cc_aut_F_l3Fl2F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (getfield(S, :time) >= constants[:t4]) - us_aut_F_l3Fl2F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = + @everywhere us_aut_F_l3Fl2F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = (S.loc = :l2F) - edge1 = Edge([nothing], cc_aut_F_l3Fl2F_1, us_aut_F_l3Fl2F_1!) + edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l3Fl2F_1), getfield(Main, :us_aut_F_l3Fl2F_1!)) map_edges[:l3F][:l2F] = [edge1] @@ -300,7 +300,7 @@ function create_automaton_G_and_F(m::ContinuousTimeModel, x1::Float64, x2::Float 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, + A = LHA("G and F property", m.transitions, locations, Λ_F, locations_init, locations_final, map_var_automaton_idx, flow, map_edges, constants, m.map_var_idx) return A end diff --git a/core/common.jl b/core/common.jl index 86cd7b9..b0f8360 100644 --- a/core/common.jl +++ b/core/common.jl @@ -45,6 +45,7 @@ struct Edge end struct LHA + name::String transitions::Vector{Transition} locations::Vector{Location} Λ::Dict{Location,Function} @@ -112,9 +113,10 @@ function ContinuousTimeModel(dim_state::Int, dim_params::Int, map_var_idx::Dict{ return new_model end -LHA(A::LHA, map_var::Dict{VariableModel,Int}) = LHA(A.transitions, A.locations, A.Λ, +LHA(A::LHA, map_var::Dict{VariableModel,Int}) = LHA(A.name, 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) diff --git a/core/lha.jl b/core/lha.jl index ce13e7c..6b9a083 100644 --- a/core/lha.jl +++ b/core/lha.jl @@ -17,8 +17,7 @@ setindex!(S::StateLHA, val::Int, var::VariableAutomaton) = S[var] = convert(Floa setindex!(S::StateLHA, val::Bool, var::VariableAutomaton) = S[var] = convert(Float64, val) function Base.show(io::IO, A::LHA) - print(io, "LHA\n") - print(io, "- locations : $(join(A.locations,','))\n") + print(io, "$(A.name) automaton (LHA)\n") print(io, "- initial locations : $(join(A.locations_init,','))\n") print(io, "- final locations : $(join(A.locations_final,','))\n") print(io, "- labeling prop Λ :\n") @@ -159,7 +158,7 @@ function next_state!(Snplus1::StateLHA, A::LHA, turns = 0 if verbose - println("#####") + println("##### Begin next_state!") @show xnplus1, tnplus1, tr_nplus1 @show Sn @show Snplus1 @@ -262,6 +261,7 @@ function next_state!(Snplus1::StateLHA, A::LHA, error("Unpredicted behavior automaton") end end + if verbose println("##### End next_state!") end end # For tests purposes -- GitLab