Commit 51eee9c4 authored by Bentriou Mahmoud's avatar Bentriou Mahmoud
Browse files

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.
parent 8bd094c8
......@@ -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]
......
......@@ -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"]) &&
......
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
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
......@@ -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)
......
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
......@@ -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
......
......@@ -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 , #);
......
......@@ -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});
......
@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