From 51eee9c4f2b2858c9a6a6d7f1f0cf251917165ea Mon Sep 17 00:00:00 2001 From: Mahmoud Bentriou <mahmoud.bentriou@centralesupelec.fr> Date: Mon, 7 Dec 2020 13:59:08 +0100 Subject: [PATCH] Automaton G and F works and is statistically tested with Cosmos. Fix about behavior of automata when the initial state is absorbing or the parameters are equal to zero. Add of supplementary unit tests. --- automata/automaton_F.jl | 2 +- automata/automaton_G.jl | 3 +- automata/automaton_G_F.jl | 124 ---------- automata/automaton_G_and_F.jl | 288 ++++++++++++++++++++++ core/lha.jl | 14 +- tests/automata/absorbing_x0_p.jl | 34 +++ tests/cosmos/distance_F/ER_1D.jl | 3 +- tests/cosmos/distance_F/dist_F_ER.lha | 2 +- tests/cosmos/distance_G/dist_G_ER.lha | 2 +- tests/cosmos/distance_G_F/ER_R6.jl | 75 ++++++ tests/cosmos/distance_G_F/dist_G_F_ER.lha | 83 +++++++ tests/run_automata.jl | 3 +- tests/run_cosmos.jl | 2 + tests/run_unit.jl | 3 +- tests/unit/models_exps_er_2d.jl | 17 ++ tests/unit/prints.jl | 8 + 16 files changed, 530 insertions(+), 133 deletions(-) delete mode 100644 automata/automaton_G_F.jl create mode 100644 automata/automaton_G_and_F.jl create mode 100644 tests/automata/absorbing_x0_p.jl create mode 100644 tests/cosmos/distance_G_F/ER_R6.jl create mode 100644 tests/cosmos/distance_G_F/dist_G_F_ER.lha create mode 100644 tests/unit/models_exps_er_2d.jl create mode 100644 tests/unit/prints.jl diff --git a/automata/automaton_F.jl b/automata/automaton_F.jl index 7ec52a5..0a64bd1 100644 --- a/automata/automaton_F.jl +++ b/automata/automaton_F.jl @@ -36,8 +36,8 @@ function create_automaton_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1 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["d"] = Inf; 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] diff --git a/automata/automaton_G.jl b/automata/automaton_G.jl index 9e1ed81..13572fc 100644 --- a/automata/automaton_G.jl +++ b/automata/automaton_G.jl @@ -120,7 +120,8 @@ function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1 S.time <= A.constants["t1"] us_aut_G_l1l2_3!(A::LHA, S::StateLHA, x::Vector{Int}) = (S.loc = "l2"; - S["d"] = S["d"] * (A.constants["t2"] - A.constants["t1"])) + S["d"] = (A.constants["t2"] - A.constants["t1"]) * + min(abs(A.constants["x1"] - S["n"]), abs(A.constants["x1"] - 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"]) && diff --git a/automata/automaton_G_F.jl b/automata/automaton_G_F.jl deleted file mode 100644 index d00c25b..0000000 --- a/automata/automaton_G_F.jl +++ /dev/null @@ -1,124 +0,0 @@ - -function create_automaton_G_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, x3::Float64, x4::Float64, - t1::Float64, t2::Float64, t1::Float64, t2::Float64, str_obs::String) - @assert str_obs in m.g - # Locations - 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) - - ## Init and final loc - locations_init = ["l0"] - locations_final = ["l2"] - - ## Map of automaton variables - map_var_automaton_idx = Dict{VariableAutomaton,Int}("t'" => 1, "in" => 2, - "n" => 3, "d" => 4) - - ## Flow of variables - flow = Dict{VariableAutomaton,Vector{Float64}}("l0" => [0.0,0.0,0.0,0.0], - "l1" => [0.0,0.0,0.0,0.0], - "l2" => [0.0,0.0,0.0,0.0], - "l3" => [0.0,0.0,0.0,0.0], - "l4" => [1.0,0.0,0.0,0.0]) - - ## Edges - map_edges = Dict{Tuple{Location,Location}, Vector{Edge}}() - - isin(val::Float64) = convert(Bool, val) - - # l0 loc - 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) - edge1 = Edge([nothing], cc_aut_G_l0l1_1, us_aut_G_l0l1_1!) - map_edges[tuple] = [edge1] - - # l1 loc - 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"])) - 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) - edge1 = Edge([nothing], cc_aut_G_l1l3_1, us_aut_G_l1l3_1!) - cc_aut_G_l1l3_2(A::LHA, S::StateLHA) = - (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) - edge2 = Edge([nothing], cc_aut_G_l1l3_2, us_aut_G_l1l3_2!) - cc_aut_G_l1l3_3(A::LHA, S::StateLHA) = - (!isin(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["t'"] = 0.0) - edge3 = Edge([nothing], cc_aut_G_l1l3_3, us_aut_G_l1l3_3!) - cc_aut_G_l1l3_4(A::LHA, S::StateLHA) = - (isin(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["t'"] = 0.0) - edge4 = Edge([nothing], cc_aut_G_l1l3_4, us_aut_G_l1l3_4!) - map_edges[tuple] = [edge1, edge2, edge3, edge4] - - tuple = ("l1", "l4") - cc_aut_G_l1l4_1(A::LHA, S::StateLHA) = - (!isin(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"])) - edge1 = Edge([nothing], cc_aut_G_l1l4_1, us_aut_G_l1l4_1!) - cc_aut_G_l1l4_2(A::LHA, S::StateLHA) = - (isin(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") - edge2 = Edge([nothing], cc_aut_G_l1l4_2, us_aut_G_l1l4_2!) - map_edges[tuple] = [edge1, edge2] - - tuple = ("l1", "l2") - cc_aut_G_l1l2_1(A::LHA, S::StateLHA) = (isin(S["in"]) && S.time >= A.constants["t2"]) - us_aut_G_l1l2_1!(A::LHA, S::StateLHA, x::Vector{Int}) = (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) = (!isin(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"])) - edge2 = Edge([nothing], cc_aut_G_l1l2_2, us_aut_G_l1l2_2!) - map_edges[tuple] = [edge1, edge2] - - # l3 loc - 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)) - edge1 = Edge(["ALL"], cc_aut_G_l3l1_1, us_aut_G_l3l1_1!) - map_edges[tuple] = [edge1] - - tuple = ("l3", "l2") - cc_aut_G_l3l2_1(A::LHA, S::StateLHA) = (isin(S["in"]) && S.time >= A.constants["t2"]) - us_aut_G_l3l2_1!(A::LHA, S::StateLHA, x::Vector{Int}) = (S.loc = "l2") - edge1 = Edge([nothing], cc_aut_G_l3l2_1, us_aut_G_l3l2_1!) - cc_aut_G_l3l2_2(A::LHA, S::StateLHA) = (!isin(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"])) - edge2 = Edge([nothing], cc_aut_G_l3l2_2, us_aut_G_l3l2_2!) - map_edges[tuple] = [edge1, edge2] - - # l4 loc - 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["t'"] * min(abs(A.constants["x1"] - S["n"]), abs(A.constants["x2"] - S["n"])); - S["t'"] = 0.0; S["n"] = get_value(A, x, str_obs); S["in"] = true) - edge1 = Edge(["ALL"], cc_aut_G_l4l1_1, us_aut_G_l4l1_1!) - map_edges[tuple] = [edge1] - - tuple = ("l4", "l2") - cc_aut_G_l4l2_1(A::LHA, S::StateLHA) = (S.time >= A.constants["t2"]) - us_aut_G_l4l2_1!(A::LHA, S::StateLHA, x::Vector{Int}) = - (S.loc = "l2"; S["d"] += S["t'"] * min(abs(A.constants["x1"] - S["n"]), abs(A.constants["x2"] - S["n"])); S["t'"] = 0.0) - edge1 = Edge([nothing], cc_aut_G_l4l2_1, us_aut_G_l4l2_1!) - map_edges[tuple] = [edge1] - - ## Constants - constants = Dict{String,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) - return A -end - -export create_automaton_G - diff --git a/automata/automaton_G_and_F.jl b/automata/automaton_G_and_F.jl new file mode 100644 index 0000000..a6af4e9 --- /dev/null +++ b/automata/automaton_G_and_F.jl @@ -0,0 +1,288 @@ + +function create_automaton_G_and_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, str_obs_G::String, + x3::Float64, x4::Float64, t3::Float64, t4::Float64, str_obs_F::String) + + @assert str_obs_G in m.g + @assert str_obs_F in m.g + # Locations + 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) + + ## Init and final loc + 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) + + ## 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]) + + ## Edges + map_edges = Dict{Tuple{Location,Location}, Vector{Edge}}() + + istrue(val::Float64) = convert(Bool, val) + + # l0G loc + 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)) + edge1 = Edge([nothing], cc_aut_G_l0Gl1G_1, us_aut_G_l0Gl1G_1!) + map_edges[tuple] = [edge1] + + # l1G loc + 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"] + 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) + 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"]) + 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) + 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"]) + us_aut_G_l1Gl3G_2!(A::LHA, S::StateLHA, x::Vector{Int}) = + (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"]) + us_aut_G_l1Gl3G_4!(A::LHA, S::StateLHA, x::Vector{Int}) = + (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] + + 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"]) + us_aut_G_l1Gl4G_1!(A::LHA, S::StateLHA, x::Vector{Int}) = + (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"]) + us_aut_G_l1Gl4G_2!(A::LHA, S::StateLHA, x::Vector{Int}) = + (S.loc = "l4G") + edge2 = Edge([nothing], cc_aut_G_l1Gl4G_2, us_aut_G_l1Gl4G_2!) + map_edges[tuple] = [edge1, edge2] + + tuple = ("l1G", "l2G") + cc_aut_G_l1Gl2G_1(A::LHA, S::StateLHA) = + istrue(S["in"]) && + S.time >= A.constants["t2"] + us_aut_G_l1Gl2G_1!(A::LHA, S::StateLHA, x::Vector{Int}) = + (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"] + 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"])) + 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["x1"] - 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["x1"] - S["n"]))) + edge4 = Edge([nothing], cc_aut_G_l1Gl2G_4, us_aut_G_l1Gl2G_4!) + + map_edges[tuple] = [edge1, edge2, edge3, edge4] + + # l3G loc + 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)) + edge1 = Edge(["ALL"], cc_aut_G_l3Gl1G_1, us_aut_G_l3Gl1G_1!) + map_edges[tuple] = [edge1] + + tuple = ("l3G", "l2G") + cc_aut_G_l3Gl2G_2(A::LHA, S::StateLHA) = + 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"])) + 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"] + us_aut_G_l3Gl2G_1!(A::LHA, S::StateLHA, x::Vector{Int}) = + (S.loc = "l2G") + edge1 = Edge([nothing], cc_aut_G_l3Gl2G_1, us_aut_G_l3Gl2G_1!) + + map_edges[tuple] = [edge1, edge2] + + # l4G loc + 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)) + edge1 = Edge(["ALL"], cc_aut_G_l4Gl1G_1, us_aut_G_l4Gl1G_1!) + map_edges[tuple] = [edge1] + + tuple = ("l4G", "l2G") + cc_aut_G_l4Gl2G_1(A::LHA, S::StateLHA) = + (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) + edge1 = Edge([nothing], cc_aut_G_l4Gl2G_1, us_aut_G_l4Gl2G_1!) + + map_edges[tuple] = [edge1] + + # Connection between the two automata: 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)) + edge1 = Edge([nothing], cc_aut_F_l2Gl1F_1, us_aut_F_l2Gl1F_1!) + map_edges[tuple] = [edge1] + + # l1F loc : we construct the edges of the form l1F => (..) + tuple = ("l1F", "l2F") + cc_aut_F_l1Fl2F_1(A::LHA, S::StateLHA) = + (A.constants["x3"] <= S["n"] <= A.constants["x4"]) && + (A.constants["t3"] <= S.time <= A.constants["t4"]) + us_aut_F_l1Fl2F_1!(A::LHA, S::StateLHA, x::Vector{Int}) = + (S.loc = "l2F"; + S["dprime"] = 0) + edge1 = Edge([nothing], cc_aut_F_l1Fl2F_1, us_aut_F_l1Fl2F_1!) + + cc_aut_F_l1Fl2F_2(A::LHA, S::StateLHA) = + S["dprime"] > 0 && + (S.time > A.constants["t4"] || istrue(S["isabs"])) + us_aut_F_l1Fl2F_2!(A::LHA, S::StateLHA, x::Vector{Int}) = + (S.loc = "l2F"; + 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) = + S["dprime"] == 0 && + S.time >= A.constants["t3"] + us_aut_F_l1Fl2F_3!(A::LHA, S::StateLHA, x::Vector{Int}) = + (S.loc = "l2F") + edge3 = Edge([nothing], cc_aut_F_l1Fl2F_3, us_aut_F_l1Fl2F_3!) + + map_edges[tuple] = [edge1, edge2, edge3] + + tuple = ("l1F", "l3F") + cc_aut_F_l1Fl3F_1(A::LHA, S::StateLHA) = + (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;) + 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"]) + 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))) + 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"]) + 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"])))) + edge3 = Edge([nothing], cc_aut_F_l1Fl3F_3, us_aut_F_l1Fl3F_3!) + map_edges[tuple] = [edge1, edge2, edge3] + + # l3F loc + 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)) + edge1 = Edge(["ALL"], cc_aut_F_l3Fl1F_1, us_aut_F_l3Fl1F_1!) + tuple = ("l3F", "l2F") + cc_aut_F_l3Fl2F_1(A::LHA, S::StateLHA) = + (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] + + ## Constants + constants = Dict{String,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) + return A +end + +export create_automaton_G_and_F + diff --git a/core/lha.jl b/core/lha.jl index a9920ec..e1686b0 100644 --- a/core/lha.jl +++ b/core/lha.jl @@ -12,11 +12,20 @@ setindex!(S::StateLHA, val::Bool, var::VariableAutomaton) = (S.values)[(S.A).map function Base.show(io::IO, S::StateLHA) print(io, "State of LHA\n") print(io, "- location: $(S.loc)\n") - print(io, "- time: $(S.time)\n") print(io, "- variables:\n") for (var, idx) in (S.A).map_var_automaton_idx print(io, "* $var = $(S.values[idx]) (idx = $idx)\n") end + print(io, "- time: $(S.time)") +end + +function Base.show(io::IO, E::Edge) + print(io, "(Edge: ") + print(io, (E.transitions[1] == nothing) ? "Asynchronous #, " : ("Synchronized with " * join(E.transitions,',') * ", ")) + print(io, Symbol(E.check_constraints)) + print(io, ", ") + print(io, Symbol(E.update_state!)) + print(io, ")") end function Base.copyto!(Sdest::StateLHA, Ssrc::StateLHA) @@ -88,7 +97,7 @@ function next_state!(Snplus1::StateLHA, A::LHA, # En fait d'apres observation de Cosmos, après qu'on ait lu la transition on devrait stop. edge_candidates = Edge[] first_round::Bool = true - detected_event::Bool = (tr_nplus1 == nothing) ? true : false + detected_event::Bool = false turns = 0 if verbose @@ -174,6 +183,7 @@ function next_state!(Snplus1::StateLHA, A::LHA, first_round = false if verbose println("After update") + @show detected_event @show Snplus1 end if (ind_edge == 0 || detected_event) diff --git a/tests/automata/absorbing_x0_p.jl b/tests/automata/absorbing_x0_p.jl new file mode 100644 index 0000000..c670842 --- /dev/null +++ b/tests/automata/absorbing_x0_p.jl @@ -0,0 +1,34 @@ + +using MarkovProcesses + +load_model("ER") +observe_all!(ER) +load_automaton("automaton_F") +load_automaton("automaton_G") +load_automaton("automaton_G_and_F") +A_F_R1 = create_automaton_F(ER, 50.0, 75.0, 0.025, 0.05, "P") +A_G_R5 = create_automaton_G(ER, 50.0, 100.0, 0.0, 0.8, "E") +x1, x2, t1, t2 = 50.0, 100.0, 0.0, 0.8 +x3, x4, t3, t4 = 30.0, 100.0, 0.8, 0.9 +A_G_F_R6 = create_automaton_G_and_F(ER, x1, x2, t1, t2, "E", + x3, x4, t3, t4, "P") + +set_param!(ER, [0.0,0.0,0.0]) +test_all = true +for A in [A_F_R1, A_G_R5, A_G_F_R6] + local sync = A*ER + local σ, σ2 = simulate(sync), simulate(sync) + global test_all = test_all && isaccepted(σ) && isaccepted(σ2) +end + +set_param!(ER, [1.0,1.0,1.0]) +set_x0!(ER, [0, 0, 0, 5]) +test_all = true +for A in [A_F_R1, A_G_R5, A_G_F_R6] + local sync = A*ER + local σ, σ2 = simulate(sync), simulate(sync) + global test_all = test_all && isaccepted(σ) && isaccepted(σ2) +end + +return true + diff --git a/tests/cosmos/distance_F/ER_1D.jl b/tests/cosmos/distance_F/ER_1D.jl index 3b9176f..49b98c7 100644 --- a/tests/cosmos/distance_F/ER_1D.jl +++ b/tests/cosmos/distance_F/ER_1D.jl @@ -55,7 +55,8 @@ for exp in l_exp 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) + test = isapprox(l_dist_cosmos[i], l_dist_pkg[i]; atol = width*1.01) || + (mat_dist_cosmos[i,j] == 9997999 && mat_dist_pkg[i,j] == Inf) test2 = nb_accepts_pkg == (nb_sim / nb_accepted) global test_all = test_all && test && test2 if !test diff --git a/tests/cosmos/distance_F/dist_F_ER.lha b/tests/cosmos/distance_F/dist_F_ER.lha index 47cd3fb..ebc9518 100644 --- a/tests/cosmos/distance_F/dist_F_ER.lha +++ b/tests/cosmos/distance_F/dist_F_ER.lha @@ -24,7 +24,7 @@ Locations={ }; Edges={ -((l0,l1), #, t>=0, {n=P,test_abs=k_1*(E*S)+k_2*ES}); +((l0,l1), #, t>=0, {n=P,test_abs=k_1*(E*S)+k_2*ES,d=9997999}); ((l1,l2),#, n>=x1 & n<=x2 & t>=t1 & t<=t2 ,{d=0}); ((l1,l2),#, t>=t2 , #); diff --git a/tests/cosmos/distance_G/dist_G_ER.lha b/tests/cosmos/distance_G/dist_G_ER.lha index 8b45dcc..7b7e700 100644 --- a/tests/cosmos/distance_G/dist_G_ER.lha +++ b/tests/cosmos/distance_G/dist_G_ER.lha @@ -46,7 +46,7 @@ Edges={ ((l1,l2), #, in=1 & t>=t2, #); ((l1,l2), #, in=0 & t>=t2, {d=d*(t2-t1)}); -((l1,l2), #, test_abs=0 & t<=t1, {d=d*(t2-t1)}); +((l1,l2), #, test_abs=0 & t<=t1, {d=min(((n-x1)^2)^0.5,((n-x2)^2)^0.5)*(t2-t1)}); ((l1,l2), #, test_abs=0 & t>=t1 & t<=t2, {d=d+(t2-t)*min(((n-x1)^2)^0.5,((n-x2)^2)^0.5)}); ((l3,l1), ALL, t>=0, {n=E,test_abs=k_1*(E*S)+k_2*ES}); diff --git a/tests/cosmos/distance_G_F/ER_R6.jl b/tests/cosmos/distance_G_F/ER_R6.jl new file mode 100644 index 0000000..921a4c8 --- /dev/null +++ b/tests/cosmos/distance_G_F/ER_R6.jl @@ -0,0 +1,75 @@ + +@everywhere begin + using MarkovProcesses + import Distributed: nworkers + absolute_path = get_module_path() * "/tests/cosmos/" + # Values x1, x2 t1, t2 + str_model = "ER" + load_model(str_model) + model = ER + observe_all!(ER) + ER.buffer_size = 100 + ER.estim_min_states = 7000 + load_automaton("automaton_G_and_F") + width = 0.2 + level = 0.95 + x1, x2, t1, t2 = 50.0, 100.0, 0.0, 0.8 + x3, x4, t3, t4 = 30.0, 100.0, 0.8, 0.9 + A_G_F = create_automaton_G_and_F(model, x1, x2, t1, t2, "E", + x3, x4, t3, t4, "P") + l_k1 = 0.0:0.5:1.5 + l_k2 = 0:40:100 +end + +test_all = true +nb_k1 = length(l_k1) +nb_k2 = length(l_k2) +mat_dist_cosmos = zeros(nb_k1,nb_k2) +mat_dist_pkg = zeros(nb_k1,nb_k2) +mat_full_k1 = zeros(nb_k1,nb_k2) +mat_full_k2 = zeros(nb_k1,nb_k2) +for i = 1:nb_k1 + for j = 1:nb_k2 + # Cosmos estimation + k1 = l_k1[i] + k2 = l_k2[j] + command = `Cosmos $(absolute_path * "models/" * str_model * ".gspn") + $(absolute_path * "distance_G_F/dist_G_F_" * str_model * ".lha") --njob $(nworkers()) + --const k_1=$(k1),k_2=$(k2),x1=$x1,x2=$x2,t1=$t1,t2=$t2 + --level $(level) --width $(width) + --verbose 0` + run(pipeline(command, stderr=devnull)) + dict_values = cosmos_get_values("Result_dist_G_F_$(str_model).res") + mat_dist_cosmos[i,j] = dict_values["Estimated value"] + nb_sim = dict_values["Total paths"] + nb_accepted = dict_values["Accepted paths"] + nb_sim = convert(Int, nb_sim) + # MarkovProcesses estimation + 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] = distribute_mean_value_lha(sync_ER, "d", nb_sim) + nb_accepts_pkg = distribute_prob_accept_lha(sync_ER, nb_sim) + #@info "Computed distances" mat_dist_pkg[i,j] mat_dist_cosmos[i,j] + #@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)) || + (mat_dist_cosmos[i,j] == 9997999 && mat_dist_pkg[i,j] == Inf) + test2 = nb_accepts_pkg == (nb_sim / nb_accepted) + if !test + @info "Distances too different" (k1,k2) mat_dist_pkg[i,j] mat_dist_cosmos[i,j] + end + if !test2 + @info "Different proportion of accepted trajectories" nb_sim nb_accepted nb_accepts_pkg + end + global test_all = test_all && test && test2 + end +end + +@info "Distances R6 pkg" mat_dist_pkg +@info "Distances R6 Cosmos" mat_dist_cosmos + +rm("Result_dist_G_F_$(str_model).res") +rm("Result.res") + +return test_all + diff --git a/tests/cosmos/distance_G_F/dist_G_F_ER.lha b/tests/cosmos/distance_G_F/dist_G_F_ER.lha new file mode 100644 index 0000000..9dadbc4 --- /dev/null +++ b/tests/cosmos/distance_G_F/dist_G_F_ER.lha @@ -0,0 +1,83 @@ + +NbVariables = 7; +NbLocations = 8; + +const int x1 = 50; +const int x2 = 100; +const int x3 = 30; +const int x4 = 100; + +const double t1 = 0.0; +const double t2 = 0.8; +const double t3 = 0.8; +const double t4 = 0.9; + +VariablesList = {t, tprime, d, dprime, n, in, test_abs}; + +LocationsList = {l0G, l1G, l2G, l3G, l4G, l1F, l2F, l3F}; + +AVG(Last(t)); +AVG(Last(d)); + +InitialLocations={l0G}; +FinalLocations={l2F}; + +Locations={ +(l0G, TRUE , (t:1)); +(l1G, TRUE , (t:1)); +(l2G, TRUE , (t:1)); +(l3G, TRUE , (t:1)); +(l4G, TRUE , (t:1,tprime:1)); +(l1F, TRUE , (t:1)); +(l2F, TRUE , (t:1)); +(l3F, TRUE , (t:1)); +}; + +Edges={ +% G automaton +((l0G,l1G), #, t>=0, {n=E,d=0,in=1,test_abs=k_1*(E*S)+k_2*ES}); + +((l1G,l3G), #, t<=t1 & n<=x1-1, {d=min(((n-x1)^2)^0.5,((n-x2)^2)^0.5),in=0}); +((l1G,l3G), #, t<=t1 & n>=x2+1, {d=min(((n-x1)^2)^0.5,((n-x2)^2)^0.5),in=0}); +((l1G,l3G), #, in=0 & t>=t1 & t<=t2 & n>=x1 & n<=x2, {d=d*(t-t1),tprime=0}); +((l1G,l3G), #, t<=t1 & n>=x1 & n<=x2, {d=0,in=0}); +((l1G,l3G), #, in=1 & t>=t1 & t<=t2 & n>=x1 & n<=x2, {tprime=0}); + +((l1G,l4G), #, in=0 & t>=t1 & t<=t2 & n<=x1-1, {d=d+d*(t-t1)}); +((l1G,l4G), #, in=0 & t>=t1 & t<=t2 & n>=x2+1, {d=d+d*(t-t1)}); +((l1G,l4G), #, in=1 & t>=t1 & t<=t2 & n<=x1-1, #); +((l1G,l4G), #, in=1 & t>=t1 & t<=t2 & n>=x2+1, #); + +((l1G,l2G), #, in=1 & t>=t2, #); +((l1G,l2G), #, in=0 & t>=t2, {d=d*(t2-t1)}); +((l1G,l2G), #, test_abs=0 & t<=t1, {d=min(((n-x1)^2)^0.5,((n-x2)^2)^0.5)*(t2-t1)}); +((l1G,l2G), #, test_abs=0 & t>=t1 & t<=t2, {d=d+(t2-t)*min(((n-x1)^2)^0.5,((n-x2)^2)^0.5)}); + +((l3G,l1G), ALL, t>=0, {n=E,test_abs=k_1*(E*S)+k_2*ES}); + +((l3G,l2G), #, in=1 & t>=t2, {d=d*(t2-t1)}); +((l3G,l2G), #, in=0 & t>=t2, #); + +((l4G,l1G), ALL, t>=0, {d=d+tprime*min(((n-x1)^2)^0.5,((n-x2)^2)^0.5),tprime=0,n=E,in=1,test_abs=k_1*(E*S)+k_2*ES}); + +((l4G,l2G), #, t>=t2, {d=d+tprime*min(((n-x1)^2)^0.5,((n-x2)^2)^0.5)}); + +% From G to F automaton +((l2G,l1F), #, t>=0, {n=P,test_abs=k_1*(E*S)+k_2*ES,dprime=9997999}); + +((l1F,l2F), #, n>=x3 & n<=x4 & t>=t3 & t<=t4, {dprime=0}); +((l1F,l2F), #, t>=t4, {d=d+dprime}); +((l1F,l2F), #, test_abs=0 , {d=d+dprime}); +((l1F,l2F), #, dprime=0 & t>=t3, #); + +((l1F,l3F), #, n>=x3 & n<=x4, {dprime=0}); +((l1F,l3F), #, t<=t3 & n<=x3-1, {dprime=min(((t-t3)^2+(n-x4)^2)^0.5,((t-t3)^2+(n-x3)^2)^0.5)}); +((l1F,l3F), #, t<=t3 & n>=x4+1, {dprime=min(((t-t3)^2+(n-x4)^2)^0.5,((t-t3)^2+(n-x3)^2)^0.5)}); +((l1F,l3F), #, n<=x3-1 & t >= t3 & t<=t4, {dprime=min(dprime,min(((n-x3)^2)^0.5,((n-x4)^2)^0.5))}); +((l1F,l3F), #, n>=x4+1 & t >= t3 & t<=t4, {dprime=min(dprime,min( ((n-x3)^2)^0.5, ((n-x4)^2)^0.5 ) ) }); + +((l3F,l1F), ALL, t>=0, {n=P,test_abs=k_1*(E*S)+k_2*ES}); + +((l3F,l2F), #, t>=t4 ,#); +}; + diff --git a/tests/run_automata.jl b/tests/run_automata.jl index e94f7c5..6f33f17 100644 --- a/tests/run_automata.jl +++ b/tests/run_automata.jl @@ -2,10 +2,11 @@ using Test @testset "Automata tests" begin + @test include("automata/absorbing_x0_p.jl") + @test include("automata/accept_R5.jl") @test include("automata/read_trajectory_last_state_F.jl") @test include("automata/read_trajectory_last_state_G.jl") @test include("automata/sync_simulate_last_state_F.jl") @test include("automata/sync_simulate_last_state_G.jl") - @test include("automata/accept_R5.jl") end diff --git a/tests/run_cosmos.jl b/tests/run_cosmos.jl index b42c650..6523e52 100644 --- a/tests/run_cosmos.jl +++ b/tests/run_cosmos.jl @@ -4,7 +4,9 @@ using Test @testset "Cosmos tests" begin test_ER_1D = include("cosmos/distance_F/ER_1D.jl") test_ER_R5 = include("cosmos/distance_G/ER_R5.jl") + test_ER_R6 = include("cosmos/distance_G_F/ER_R6.jl") @test test_ER_1D @test test_ER_R5 + @test test_ER_R6 end diff --git a/tests/run_unit.jl b/tests/run_unit.jl index c37422c..fe64702 100644 --- a/tests/run_unit.jl +++ b/tests/run_unit.jl @@ -29,8 +29,9 @@ using Test @test include("unit/macro_network_model.jl") @test include("unit/model_prior.jl") @test include("unit/models_exps_er_1d.jl") + @test include("unit/models_exps_er_2d.jl") @test include("unit/observe_all.jl") - + @test include("unit/prints.jl") @test include("unit/set_param.jl") @test include("unit/set_x0.jl") diff --git a/tests/unit/models_exps_er_2d.jl b/tests/unit/models_exps_er_2d.jl new file mode 100644 index 0000000..09e04a8 --- /dev/null +++ b/tests/unit/models_exps_er_2d.jl @@ -0,0 +1,17 @@ + +using MarkovProcesses + +load_model("ER") +observe_all!(ER) +load_automaton("automaton_F") +load_automaton("automaton_G") +load_automaton("automaton_G_and_F") + +x1, x2, t1, t2 = 50.0, 100.0, 0.0, 0.8 +A_G_R5 = create_automaton_G(ER, x1, x2, t1, t2, "E") +x3, x4, t3, t4 = 30.0, 100.0, 0.8, 0.9 +A_G_F_R6 = create_automaton_G_and_F(ER, x1, x2, t1, t2, "E", + x3, x4, t3, t4, "P") + +return true + diff --git a/tests/unit/prints.jl b/tests/unit/prints.jl new file mode 100644 index 0000000..87c3a17 --- /dev/null +++ b/tests/unit/prints.jl @@ -0,0 +1,8 @@ + +using MarkovProcesses + +load_model("SIR") +println(SIR) + +return true + -- GitLab