From 00b622f3b497c98a0f44e73455edbee73d256bac Mon Sep 17 00:00:00 2001
From: Mahmoud Bentriou <mahmoud.bentriou@centralesupelec.fr>
Date: Mon, 25 Jan 2021 01:58:41 +0100
Subject: [PATCH] 1) Detection of a bug when two synchronized models with two
different automata and proba moels are differents. This bug was introduced
after we change the structure of automata in order to better distributed
programming. It leads to a restructuration of automata. In fine, the
structure is more stable and consistent. It is possible it is more
computationally efficient, but for now it is not well tested.
2) Creation of functions that collects data along with a timeline
over a trajectory + unit test vectorize.
3) Very small fix in plots and abc smc.
---
algorithms/abc_smc.jl | 4 +-
automata/automaton_F.jl | 183 ++++++------
automata/automaton_G.jl | 292 ++++++++++---------
automata/automaton_G_and_F.jl | 493 ++++++++++++++++++---------------
core/MarkovProcesses.jl | 3 +-
core/plots.jl | 16 +-
core/trajectory.jl | 43 +++
tests/automata/two_automata.jl | 16 ++
tests/run_automata.jl | 1 +
tests/run_unit.jl | 2 +
tests/unit/vectorize.jl | 58 ++++
11 files changed, 672 insertions(+), 439 deletions(-)
create mode 100644 tests/automata/two_automata.jl
create mode 100644 tests/unit/vectorize.jl
diff --git a/algorithms/abc_smc.jl b/algorithms/abc_smc.jl
index 2667bce..098ce7e 100644
--- a/algorithms/abc_smc.jl
+++ b/algorithms/abc_smc.jl
@@ -165,12 +165,12 @@ function _abc_smc(pm::ParametricModel, nbr_particles::Int, alpha::Float64,
normalize!(wl_current, 1)
@info "End"
end
+ current_time = time()
@info "After this step, time spent and number of simulations" steptime=(current_time-begin_time_ite) step_nbr_sim
mat_p_old = copy(mat_p)
wl_old = copy(wl_current)
fill!(l_nbr_sim, 0)
flush(stdout)
- current_time = time()
old_epsilon = epsilon
end
@@ -273,13 +273,13 @@ function _distributed_abc_smc(pm::ParametricModel, nbr_particles::Int, alpha::Fl
normalize!(wl_current, 1)
@info "End"
end
+ current_time = time()
@info "After this step, time spent and number of simulations" steptime=(current_time-begin_time_ite) step_nbr_sim
mat_p_old = mat_p
wl_old = wl_current
vec_dist = convert(Array, d_vec_dist)
fill!(l_nbr_sim, 0)
flush(stdout)
- current_time = time()
old_epsilon = epsilon
end
diff --git a/automata/automaton_F.jl b/automata/automaton_F.jl
index 4c8dc99..203b8b9 100644
--- a/automata/automaton_F.jl
+++ b/automata/automaton_F.jl
@@ -1,13 +1,84 @@
+@everywhere istrue(val::Float64) = convert(Bool, val)
+
+# Invariant predicates functions
+@everywhere true_inv_predicate(x::Vector{Int}) = true
+
+# Check constraints and update state functions
+
+# l0 loc : we construct the edges of the form l0 => (..)
+# "cc" as check_constraints and "us" as update_state
+# l0 => l1
+@everywhere cc_aut_F_l0l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
+# us_aut_F_l0l1_1! inside create_automaton_F
+
+# l1 loc
+# l1 => l2
+@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])
+@everywhere us_aut_F_l1l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2;
+ S[:d] = 0)
+
+@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
+@everywhere us_aut_F_l1l2_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2)
+
+@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])
+@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])))
+
+@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]
+@everywhere us_aut_F_l1l2_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2)
+
+# l1 => l3
+@everywhere cc_aut_F_l1l3_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(constants[:x1] <= S[:n] <= constants[:x2])
+@everywhere us_aut_F_l1l3_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l3;
+ S[:d] = 0;)
+
+@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])
+@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)))
+
+@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])
+@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]))))
+
+# l3 loc
+# l3 => l1
+@everywhere cc_aut_F_l3l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
+
+# l3 => l2
+@everywhere cc_aut_F_l3l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(getfield(S, :time) >= constants[:t2])
+@everywhere us_aut_F_l3l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2)
+
function create_automaton_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, sym_obs::VariableModel)
@assert sym_obs in m.g "$(sym_obs) is not observed."
# Locations
locations = [:l0, :l1, :l2, :l3]
## Invariant predicates
- true_inv_predicate(x::Vector{Int}) = true
- Λ_F = Dict(:l0 => true_inv_predicate, :l1 => true_inv_predicate,
- :l2 => true_inv_predicate, :l3 => true_inv_predicate)
+ Λ_F = Dict(:l0 => getfield(Main, :true_inv_predicate), :l1 => getfield(Main, :true_inv_predicate),
+ :l2 => getfield(Main, :true_inv_predicate), :l3 => getfield(Main, :true_inv_predicate))
## Init and final loc
locations_init = [:l0]
@@ -30,97 +101,53 @@ function create_automaton_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
for loc in locations
map_edges[loc] = Dict{Location, Vector{Edge}}()
end
- istrue(val::Float64) = convert(Bool, val)
sym_isabs_func = Symbol(m.isabsorbing)
-
- # l0 loc : we construct the edges of the form l0 => (..)
- # "cc" as check_constraints
- tuple = (:l0, :l1)
- @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, $(Meta.quot(sym_obs)));
- S[:d] = Inf;
- 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!))
+ idx_obs_var = getfield(m, :map_var_idx)[sym_obs]
+ nbr_rand = rand(1:1000)
+ basename_func = "$(replace(m.name, ' '=>'_'))_$(nbr_rand)"
+ basename_func = replace(basename_func, '-'=>'_')
+
+ # l0 loc
+ # l0 => l1
+ sym_func_us_l0l1_1 = Symbol("us_aut_F_$(basename_func)_l0l1_1!")
+ str_us_l0l1_1 = "
+ @everywhere $(sym_func_us_l0l1_1)(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = \n
+ (S.loc = :l1; \n
+ S[:n] = x[$(idx_obs_var)];\n
+ S[:d] = Inf; \n
+ S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))"
+ eval(Meta.parse(str_us_l0l1_1))
+ edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l0l1_1), getfield(Main, sym_func_us_l0l1_1))
map_edges[:l0][:l1] = [edge1]
- # l1 loc : we construct the edges of the form l1 => (..)
- tuple = (:l1, :l2)
- @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])
- @everywhere us_aut_F_l1l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2;
- S[:d] = 0)
+ # l1 loc
+ # l1 => l2
edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l1l2_1), getfield(Main, :us_aut_F_l1l2_1!))
-
- @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
- @everywhere us_aut_F_l1l2_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2)
- edge4 = Edge([nothing], getfield(Main, :cc_aut_F_l1l2_4), getfield(Main, :us_aut_F_l1l2_4!))
-
- @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])
- @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], getfield(Main, :cc_aut_F_l1l2_2), getfield(Main, :us_aut_F_l1l2_2!))
-
- @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]
- @everywhere us_aut_F_l1l2_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2)
edge3 = Edge([nothing], getfield(Main, :cc_aut_F_l1l2_3), getfield(Main, :us_aut_F_l1l2_3!))
-
+ edge4 = Edge([nothing], getfield(Main, :cc_aut_F_l1l2_4), getfield(Main, :us_aut_F_l1l2_4!))
map_edges[:l1][:l2] = [edge1, edge2, edge3, edge4]
- tuple = (:l1, :l3)
- @everywhere cc_aut_F_l1l3_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (constants[:x1] <= S[:n] <= constants[:x2])
- @everywhere us_aut_F_l1l3_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l3;
- S[:d] = 0;)
+ # l1 => l3
edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l1l3_1), getfield(Main, :us_aut_F_l1l3_1!))
-
- @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])
- @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], getfield(Main, :cc_aut_F_l1l3_2), getfield(Main, :us_aut_F_l1l3_2!))
-
- @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])
- @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], 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)
- @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, $(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!))
+ # l3 => l1
+ sym_func_us_l3l1_1 = Symbol("us_aut_F_$(basename_func)_l0l1_1!")
+ str_us_l3l1_1 =
+ "@everywhere $(sym_func_us_l3l1_1)(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = \n
+ (S.loc = :l1;\n
+ S[:n] = x[$(idx_obs_var)];\n
+ S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))"
+ eval(Meta.parse(str_us_l3l1_1))
+ edge1 = Edge([:ALL], getfield(Main, :cc_aut_F_l3l1_1), getfield(Main, sym_func_us_l3l1_1))
map_edges[:l3][:l1] = [edge1]
-
- tuple = (:l3, :l2)
- @everywhere cc_aut_F_l3l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (getfield(S, :time) >= constants[:t2])
- @everywhere us_aut_F_l3l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2)
+ # l3 => l2
edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l3l2_1), getfield(Main, :us_aut_F_l3l2_1!))
map_edges[:l3][:l2] = [edge1]
diff --git a/automata/automaton_G.jl b/automata/automaton_G.jl
index 2bbc48b..2caa939 100644
--- a/automata/automaton_G.jl
+++ b/automata/automaton_G.jl
@@ -1,11 +1,128 @@
+@everywhere istrue(val::Float64) = convert(Bool, val)
+
+# Invariant predicate functions
+@everywhere true_inv_predicate(x::Vector{Int}) = true
+
+# l0 loc
+# l0 => l1
+@everywhere cc_aut_G_l0l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
+
+# l1 => l3
+@everywhere cc_aut_G_l1l3_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]
+@everywhere us_aut_G_l1l3_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l3;
+ S[:d] = min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n]));
+ S[:in] = false)
+
+@everywhere cc_aut_G_l1l3_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(getfield(S, :time) <= constants[:t1]) &&
+(constants[:x1] <= S[:n] <= constants[:x2])
+@everywhere us_aut_G_l1l3_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l3;
+ S[:d] = 0;
+ S[:in] = false)
+
+@everywhere cc_aut_G_l1l3_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])
+@everywhere us_aut_G_l1l3_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l3;
+ S[:d] = S[:d] * (getfield(S, :time) - constants[:t1]);
+ S[:tprime] = 0.0)
+
+@everywhere cc_aut_G_l1l3_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])
+@everywhere us_aut_G_l1l3_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l3;
+ S[:tprime] = 0.0)
+
+# l1 => l4
+@everywhere cc_aut_G_l1l4_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])
+@everywhere us_aut_G_l1l4_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l4;
+ S[:d] += S[:d] * (getfield(S, :time) - constants[:t1]))
+
+@everywhere cc_aut_G_l1l4_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])
+@everywhere us_aut_G_l1l4_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l4)
+
+
+# l1 => l2
+@everywhere cc_aut_G_l1l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+istrue(S[:in]) &&
+getfield(S, :time) >= constants[:t2]
+@everywhere us_aut_G_l1l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2)
+
+@everywhere cc_aut_G_l1l2_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+!istrue(S[:in]) &&
+getfield(S, :time) >= constants[:t2]
+@everywhere us_aut_G_l1l2_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2;
+ S[:d] = S[:d] * (constants[:t2] - constants[:t1]))
+
+@everywhere cc_aut_G_l1l2_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+istrue(S[:isabs]) &&
+getfield(S, :time) <= constants[:t1]
+@everywhere us_aut_G_l1l2_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2;
+ S[:d] = (constants[:t2] - constants[:t1]) *
+min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])))
+
+@everywhere cc_aut_G_l1l2_4(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+istrue(S[:isabs]) &&
+(constants[:t1] <= getfield(S, :time) <= constants[:t2])
+@everywhere us_aut_G_l1l2_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2;
+ S[:d] += (constants[:t2] - getfield(S, :time)) *
+min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])))
+
+# l3 => l1
+@everywhere cc_aut_G_l3l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
+
+# l4 => l1
+@everywhere cc_aut_G_l4l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
+
+# l2 => l1
+@everywhere cc_aut_G_l3l2_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+istrue(S[:in]) &&
+getfield(S, :time) >= constants[:t2]
+@everywhere us_aut_G_l3l2_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2;
+ S[:d] = S[:d] * (constants[:t2] - constants[:t1]))
+
+@everywhere cc_aut_G_l3l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+!istrue(S[:in]) &&
+getfield(S, :time) >= constants[:t2]
+@everywhere us_aut_G_l3l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2)
+
+# l4 => l2
+@everywhere cc_aut_G_l4l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(getfield(S, :time) >= constants[:t2])
+@everywhere us_aut_G_l4l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2;
+ S[:d] += S[:tprime] * min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n]));
+ S[:tprime] = 0.0)
+
function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, sym_obs::VariableModel)
@assert sym_obs in m.g
# Locations
locations = [:l0, :l1, :l2, :l3, :l4]
# Invariant predicates
- @everywhere true_inv_predicate(x::Vector{Int}) = true
Λ_F = Dict(:l0 => getfield(Main, :true_inv_predicate), :l1 => getfield(Main, :true_inv_predicate),
:l2 => getfield(Main, :true_inv_predicate), :l3 => getfield(Main, :true_inv_predicate),
:l4 => getfield(Main, :true_inv_predicate))
@@ -30,166 +147,81 @@ function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
for loc in locations
map_edges[loc] = Dict{Location, Vector{Edge}}()
end
- @everywhere istrue(val::Float64) = convert(Bool, val)
sym_isabs_func = Symbol(m.isabsorbing)
+ idx_obs_var = getfield(m, :map_var_idx)[sym_obs]
+ nbr_rand = rand(1:1000)
+ basename_func = "$(replace(m.name, ' '=>'_'))_$(nbr_rand)"
+ basename_func = replace(basename_func, '-'=>'_')
# l0 loc
- tuple = (:l0, :l1)
- @everywhere cc_aut_G_l0l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
- @everywhere us_aut_G_l0l1_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l1;
- S[:d] = 0;
- S[:n] = get_value(S, x, $(Meta.quot(sym_obs)));
- S[:in] = true;
- S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))
- edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l0l1_1), getfield(Main, :us_aut_G_l0l1_1!))
+ # l0 => l1
+ sym_func_us_l0l1_1 = Symbol("us_aut_G_$(basename_func)_l0l1_1!")
+ str_us_l0l1_1 = "
+ @everywhere $(sym_func_us_l0l1_1)(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = \n
+ (S.loc = :l1; \n
+ S[:d] = 0; \n
+ S[:n] = x[$(idx_obs_var)]; \n
+ S[:in] = true; \n
+ S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))"
+ eval(Meta.parse(str_us_l0l1_1))
+ edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l0l1_1), getfield(Main, sym_func_us_l0l1_1))
map_edges[:l0][:l1] = [edge1]
# l1 loc
- tuple = (:l1, :l3)
- @everywhere cc_aut_G_l1l3_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]
- @everywhere us_aut_G_l1l3_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l3;
- S[:d] = min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n]));
- S[:in] = false)
+ # l1 => l3
edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l1l3_1), getfield(Main, :us_aut_G_l1l3_1!))
-
- @everywhere cc_aut_G_l1l3_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])
- @everywhere us_aut_G_l1l3_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l3;
- S[:d] = S[:d] * (getfield(S, :time) - constants[:t1]);
- S[:tprime] = 0.0)
- edge3 = Edge([nothing], getfield(Main, :cc_aut_G_l1l3_3), getfield(Main, :us_aut_G_l1l3_3!))
-
- @everywhere cc_aut_G_l1l3_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (getfield(S, :time) <= constants[:t1]) &&
- (constants[:x1] <= S[:n] <= constants[:x2])
- @everywhere us_aut_G_l1l3_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l3;
- S[:d] = 0;
- S[:in] = false)
edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l1l3_2), getfield(Main, :us_aut_G_l1l3_2!))
-
- @everywhere cc_aut_G_l1l3_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])
- @everywhere us_aut_G_l1l3_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l3;
- S[:tprime] = 0.0)
+ edge3 = Edge([nothing], getfield(Main, :cc_aut_G_l1l3_3), getfield(Main, :us_aut_G_l1l3_3!))
edge4 = Edge([nothing], getfield(Main, :cc_aut_G_l1l3_4), getfield(Main, :us_aut_G_l1l3_4!))
-
map_edges[:l1][:l3] = [edge1, edge2, edge3, edge4]
- tuple = (:l1, :l4)
- @everywhere cc_aut_G_l1l4_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])
- @everywhere us_aut_G_l1l4_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l4;
- S[:d] += S[:d] * (getfield(S, :time) - constants[:t1]))
+ # l1 => l4
edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l1l4_1), getfield(Main, :us_aut_G_l1l4_1!))
- @everywhere cc_aut_G_l1l4_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])
- @everywhere us_aut_G_l1l4_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l4)
edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l1l4_2), getfield(Main, :us_aut_G_l1l4_2!))
-
map_edges[:l1][:l4] = [edge1, edge2]
-
- tuple = (:l1, :l2)
- @everywhere cc_aut_G_l1l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- istrue(S[:in]) &&
- getfield(S, :time) >= constants[:t2]
- @everywhere us_aut_G_l1l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2)
+
+ # l1 => l2
edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l1l2_1), getfield(Main, :us_aut_G_l1l2_1!))
- @everywhere cc_aut_G_l1l2_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- !istrue(S[:in]) &&
- getfield(S, :time) >= constants[:t2]
- @everywhere us_aut_G_l1l2_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2;
- S[:d] = S[:d] * (constants[:t2] - constants[:t1]))
edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l1l2_2), getfield(Main, :us_aut_G_l1l2_2!))
- @everywhere cc_aut_G_l1l2_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- istrue(S[:isabs]) &&
- getfield(S, :time) <= constants[:t1]
- @everywhere us_aut_G_l1l2_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2;
- S[:d] = (constants[:t2] - constants[:t1]) *
- min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])))
edge3 = Edge([nothing], getfield(Main, :cc_aut_G_l1l2_3), getfield(Main, :us_aut_G_l1l2_3!))
- @everywhere cc_aut_G_l1l2_4(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- istrue(S[:isabs]) &&
- (constants[:t1] <= getfield(S, :time) <= constants[:t2])
- @everywhere us_aut_G_l1l2_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2;
- S[:d] += (constants[:t2] - getfield(S, :time)) *
- min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])))
edge4 = Edge([nothing], getfield(Main, :cc_aut_G_l1l2_4), getfield(Main, :us_aut_G_l1l2_4!))
-
map_edges[:l1][:l2] = [edge1, edge2, edge3, edge4]
# l3 loc
- tuple = (:l3, :l1)
- @everywhere cc_aut_G_l3l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
- @everywhere us_aut_G_l3l1_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l1;
- 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_G_l3l1_1), getfield(Main, :us_aut_G_l3l1_1!))
-
+ # l3 => l1
+ sym_func_us_l3l1_1 = Symbol("us_aut_G_$(basename_func)_l3l1_1!")
+ str_us_l3l1_1 = "
+ @everywhere $(sym_func_us_l3l1_1)(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+ (S.loc = :l1;
+ S[:n] = x[$(idx_obs_var)];
+ S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))"
+ eval(Meta.parse(str_us_l3l1_1))
+ edge1 = Edge([:ALL], getfield(Main, :cc_aut_G_l3l1_1), getfield(Main, sym_func_us_l3l1_1))
map_edges[:l3][:l1] = [edge1]
- tuple = (:l3, :l2)
- @everywhere cc_aut_G_l3l2_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- istrue(S[:in]) &&
- getfield(S, :time) >= constants[:t2]
- @everywhere us_aut_G_l3l2_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2;
- S[:d] = S[:d] * (constants[:t2] - constants[:t1]))
- edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l3l2_2), getfield(Main, :us_aut_G_l3l2_2!))
- @everywhere cc_aut_G_l3l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- !istrue(S[:in]) &&
- getfield(S, :time) >= constants[:t2]
- @everywhere us_aut_G_l3l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2)
+ # l3 => l2
edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l3l2_1), getfield(Main, :us_aut_G_l3l2_1!))
-
+ edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l3l2_2), getfield(Main, :us_aut_G_l3l2_2!))
map_edges[:l3][:l2] = [edge1, edge2]
# l4 loc
- tuple = (:l4, :l1)
- @everywhere cc_aut_G_l4l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
- @everywhere us_aut_G_l4l1_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l1;
- 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, $(Meta.quot(sym_obs)));
- S[:in] = true;
- S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))
- edge1 = Edge([:ALL], getfield(Main, :cc_aut_G_l4l1_1), getfield(Main, :us_aut_G_l4l1_1!))
-
+ # l4 => l1
+ sym_func_us_l4l1_1 = Symbol("us_aut_G_$(basename_func)_l4l1_1!")
+ str_us_l4l1_1 = "
+ @everywhere $(sym_func_us_l4l1_1)(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = \n
+ (S.loc = :l1; \n
+ S[:d] += S[:tprime] * min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])); \n
+ S[:tprime] = 0.0; \n
+ S[:n] = x[$(idx_obs_var)]; \n
+ S[:in] = true; \n
+ S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))"
+ eval(Meta.parse(str_us_l4l1_1))
+ edge1 = Edge([:ALL], getfield(Main, :cc_aut_G_l4l1_1), getfield(Main, sym_func_us_l4l1_1))
map_edges[:l4][:l1] = [edge1]
- tuple = (:l4, :l2)
- @everywhere cc_aut_G_l4l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (getfield(S, :time) >= constants[:t2])
- @everywhere us_aut_G_l4l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2;
- S[:d] += S[:tprime] * min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n]));
- S[:tprime] = 0.0)
+ # l4 => l2
edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l4l2_1), getfield(Main, :us_aut_G_l4l2_1!))
-
map_edges[:l4][:l2] = [edge1]
## Constants
diff --git a/automata/automaton_G_and_F.jl b/automata/automaton_G_and_F.jl
index 346976c..0e3c286 100644
--- a/automata/automaton_G_and_F.jl
+++ b/automata/automaton_G_and_F.jl
@@ -1,4 +1,188 @@
+@everywhere istrue(val::Float64) = convert(Bool, val)
+
+# Invariant predicate functions
+@everywhere true_inv_predicate(x::Vector{Int}) = true
+
+# l0G loc
+# l0G => l1G
+@everywhere cc_aut_G_l0Gl1G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
+
+# l1G loc
+# l1G => l3G
+@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]
+@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)
+
+@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])
+@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)
+
+@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])
+@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)
+
+@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])
+@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)
+
+# l1G => l4G
+@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])
+@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]))
+
+@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])
+@everywhere us_aut_G_l1Gl4G_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l4G)
+
+# l1G => l2G
+@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]
+@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])))
+
+@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])
+@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])))
+
+@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]
+@everywhere us_aut_G_l1Gl2G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2G)
+
+@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]
+@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]))
+
+# l3G loc
+# l3G => l1G
+@everywhere cc_aut_G_l3Gl1G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
+
+# l3G => l2G
+@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]
+@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]))
+
+@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]
+@everywhere us_aut_G_l3Gl2G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2G)
+
+# l4G loc
+# l4G => l1G
+@everywhere cc_aut_G_l4Gl1G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
+
+# l4G => l2G
+@everywhere cc_aut_G_l4Gl2G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(getfield(S, :time) >= constants[:t2])
+@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)
+
+# Connection between the two automata: l2G => l1F
+@everywhere cc_aut_F_l2Gl1F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
+
+# l1F loc : we construct the edges of the form l1F => (..)
+# l1F => l2F
+@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])
+@everywhere us_aut_F_l1Fl2F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2F;
+ S[:dprime] = 0)
+
+@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
+@everywhere us_aut_F_l1Fl2F_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2F)
+
+@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])
+@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])
+
+@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]
+@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])
+
+# l1F => l3F
+@everywhere cc_aut_F_l1Fl3F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(constants[:x3] <= S[:n] <= constants[:x4])
+@everywhere us_aut_F_l1Fl3F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l3F;
+ S[:dprime] = 0;)
+
+@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])
+@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)))
+
+@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])
+@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]))))
+
+# l3F loc
+# l3F => l1F
+@everywhere cc_aut_F_l3Fl1F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
+
+# l3F => l2F
+@everywhere cc_aut_F_l3Fl2F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(getfield(S, :time) >= constants[:t4])
+@everywhere us_aut_F_l3Fl2F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
+(S.loc = :l2F)
+
function create_automaton_G_and_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, sym_obs_G::VariableModel,
x3::Float64, x4::Float64, t3::Float64, t4::Float64, sym_obs_F::VariableModel)
@@ -9,13 +193,12 @@ function create_automaton_G_and_F(m::ContinuousTimeModel, x1::Float64, x2::Float
:l1F, :l2F, :l3F]
# Invariant predicates
- true_inv_predicate(x::Vector{Int}) = 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 => getfield(Main, :true_inv_predicate), :l1G => getfield(Main, :true_inv_predicate),
+ :l2G => getfield(Main, :true_inv_predicate), :l3G => getfield(Main, :true_inv_predicate),
+ :l4G => getfield(Main, :true_inv_predicate),
+ :l1F => getfield(Main, :true_inv_predicate),
+ :l2F => getfield(Main, :true_inv_predicate), :l3F => getfield(Main, :true_inv_predicate))
+
## Init and final loc
locations_init = [:l0G]
locations_final = [:l2F]
@@ -40,266 +223,130 @@ function create_automaton_G_and_F(m::ContinuousTimeModel, x1::Float64, x2::Float
for loc in locations
map_edges[loc] = Dict{Location, Vector{Edge}}()
end
- istrue(val::Float64) = convert(Bool, val)
-
- sym_isabs_func = Symbol(m.isabsorbing)
+ sym_isabs_func = Symbol(m.isabsorbing)
+ idx_obs_var_F = getfield(m, :map_var_idx)[sym_obs_F]
+ idx_obs_var_G = getfield(m, :map_var_idx)[sym_obs_G]
+ nbr_rand = rand(1:1000)
+ basename_func = "$(replace(m.name, ' '=>'_'))_$(nbr_rand)"
+ basename_func = replace(basename_func, '-'=>'_')
+
# l0G loc
- tuple = (:l0G, :l1G)
- @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, $(Meta.quot(sym_obs_G)));
- S[:in] = true;
- 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!))
+ # l0G => l1G
+ sym_func_us_l0Gl1G_1 = Symbol("us_aut_G_$(basename_func)_l0Gl1G_1!")
+ str_us_l0Gl1G_1 = "
+ @everywhere $(sym_func_us_l0Gl1G_1)(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = \n
+ (S.loc = :l1G; \n
+ S[:d] = 0; \n
+ S[:n] = x[$(idx_obs_var_G)]; \n
+ S[:in] = true; \n
+ S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))"
+ eval(Meta.parse(str_us_l0Gl1G_1))
+ edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l0Gl1G_1), getfield(Main, sym_func_us_l0Gl1G_1))
map_edges[:l0G][:l1G] = [edge1]
- # l1G loc
- tuple = (:l1G, :l3G)
- @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]
- @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)
+ # l1G => l3G
edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l1Gl3G_1), getfield(Main, :us_aut_G_l1Gl3G_1!))
-
- @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])
- @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], getfield(Main, :cc_aut_G_l1Gl3G_3), getfield(Main, :us_aut_G_l1Gl3G_3!))
-
- @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])
- @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], getfield(Main, :cc_aut_G_l1Gl3G_2), getfield(Main, :us_aut_G_l1Gl3G_2!))
-
- @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])
- @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)
+ edge3 = Edge([nothing], getfield(Main, :cc_aut_G_l1Gl3G_3), getfield(Main, :us_aut_G_l1Gl3G_3!))
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)
- @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])
- @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], getfield(Main, :cc_aut_G_l1Gl4G_1), getfield(Main, :us_aut_G_l1Gl4G_1!))
- @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])
- @everywhere us_aut_G_l1Gl4G_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l4G)
+ # l1G => l4G
+ edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l1Gl4G_1), getfield(Main, :us_aut_G_l1Gl4G_1!))
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)
- @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]
- @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], 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])
- @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], 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]
- @everywhere us_aut_G_l1Gl2G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2G)
+
+ # l1G => l2G
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]
- @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], getfield(Main, :cc_aut_G_l1Gl2G_2), getfield(Main, :us_aut_G_l1Gl2G_2!))
-
+ edge3 = Edge([nothing], getfield(Main, :cc_aut_G_l1Gl2G_3), getfield(Main, :us_aut_G_l1Gl2G_3!))
+ edge4 = Edge([nothing], getfield(Main, :cc_aut_G_l1Gl2G_4), getfield(Main, :us_aut_G_l1Gl2G_4!))
map_edges[:l1G][:l2G] = [edge3, edge4, edge1, edge2]
# l3G loc
- tuple = (:l3G, :l1G)
- @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, $(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!))
+ # l3G => l1G
+ sym_func_us_l3Gl1G_1 = Symbol("us_aut_G_$(basename_func)_l3Gl1G_1!")
+ str_us_l3Gl1G_1 = "
+ @everywhere $(sym_func_us_l3Gl1G_1)(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = \n
+ (S.loc = :l1G; \n
+ S[:n] = x[$(idx_obs_var_G)]; \n
+ S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))"
+ eval(Meta.parse(str_us_l3Gl1G_1))
+ edge1 = Edge([:ALL], getfield(Main, :cc_aut_G_l3Gl1G_1), getfield(Main, sym_func_us_l3Gl1G_1))
map_edges[:l3G][:l1G] = [edge1]
-
- tuple = (:l3G, :l2G)
- @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]
- @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], getfield(Main, :cc_aut_G_l3Gl2G_2), getfield(Main, :us_aut_G_l3Gl2G_2!))
- @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]
- @everywhere us_aut_G_l3Gl2G_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2G)
+ # l3G => l2G
edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l3Gl2G_1), getfield(Main, :us_aut_G_l3Gl2G_1!))
-
+ edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l3Gl2G_2), getfield(Main, :us_aut_G_l3Gl2G_2!))
map_edges[:l3G][:l2G] = [edge1, edge2]
- # l4G loc
- tuple = (:l4G, :l1G)
- @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, $(Meta.quot(sym_obs_G)));
- S[:in] = true;
- 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!))
-
+ # l4 loc
+ # l4G => l1G
+ sym_func_us_l4Gl1G_1 = Symbol("us_aut_G_$(basename_func)_l4Gl1G_1!")
+ str_us_l4Gl1G_1 = "
+ @everywhere $(sym_func_us_l4Gl1G_1)(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = \n
+ (S.loc = :l1G; \n
+ S[:d] += S[:tprime] * min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])); \n
+ S[:tprime] = 0.0; \n
+ S[:n] = x[$(idx_obs_var_G)]; \n
+ S[:in] = true; \n
+ S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))"
+ eval(Meta.parse(str_us_l4Gl1G_1))
+ edge1 = Edge([:ALL], getfield(Main, :cc_aut_G_l4Gl1G_1), getfield(Main, sym_func_us_l4Gl1G_1))
map_edges[:l4G][:l1G] = [edge1]
- tuple = (:l4G, :l2G)
- @everywhere cc_aut_G_l4Gl2G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (getfield(S, :time) >= constants[:t2])
- @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)
+ # l4G => l2G
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)
- @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, $(Meta.quot(sym_obs_F)));
- S[:dprime] = Inf;
- 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!))
+
+ # l2G loc
+ # l2G => l1F : Transition from autF to autG
+ sym_func_us_l2Gl1F_1 = Symbol("us_aut_G_$(basename_func)_l2Gl1F_1!")
+ str_us_l2Gl1F_1 = "
+ @everywhere $(sym_func_us_l2Gl1F_1)(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = \n
+ (S.loc = :l1F; \n
+ S[:n] = x[$(idx_obs_var_F)];\n
+ S[:dprime] = Inf; \n
+ S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))"
+ eval(Meta.parse(str_us_l2Gl1F_1))
+ edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l2Gl1F_1), getfield(Main, sym_func_us_l2Gl1F_1))
map_edges[:l2G][:l1F] = [edge1]
- # l1F loc : we construct the edges of the form l1F => (..)
- tuple = (:l1F, :l2F)
- @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])
- @everywhere us_aut_F_l1Fl2F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2F;
- S[:dprime] = 0)
+ # l1F loc
+ # l1F => l3F
edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l1Fl2F_1), getfield(Main, :us_aut_F_l1Fl2F_1!))
-
- @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
- @everywhere us_aut_F_l1Fl2F_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2F)
- edge4 = Edge([nothing], getfield(Main, :cc_aut_F_l1Fl2F_4), getfield(Main, :us_aut_F_l1Fl2F_4!))
-
- @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])
- @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], getfield(Main, :cc_aut_F_l1Fl2F_2), getfield(Main, :us_aut_F_l1Fl2F_2!))
-
- @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]
- @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], getfield(Main, :cc_aut_F_l1Fl2F_3), getfield(Main, :us_aut_F_l1Fl2F_3!))
-
+ edge4 = Edge([nothing], getfield(Main, :cc_aut_F_l1Fl2F_4), getfield(Main, :us_aut_F_l1Fl2F_4!))
map_edges[:l1F][:l2F] = [edge1, edge4, edge3, edge2]
- tuple = (:l1F, :l3F)
- @everywhere cc_aut_F_l1Fl3F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (constants[:x3] <= S[:n] <= constants[:x4])
- @everywhere us_aut_F_l1Fl3F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l3F;
- S[:dprime] = 0;)
+ # l1F => l3F
edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l1Fl3F_1), getfield(Main, :us_aut_F_l1Fl3F_1!))
-
- @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])
- @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], getfield(Main, :cc_aut_F_l1Fl3F_2), getfield(Main, :us_aut_F_l1Fl3F_2!))
-
- @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])
- @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], 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)
- @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, $(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!))
-
+ # l3F => l1F
+ sym_func_us_l3Fl1F_1 = Symbol("us_aut_G_$(basename_func)_l3Fl1F_1!")
+ str_us_l3Fl1F_1 = "
+ @everywhere $(sym_func_us_l3Fl1F_1)(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = \n
+ (S.loc = :l1F;\n
+ S[:n] = x[$(idx_obs_var_F)];\n
+ S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))"
+ eval(Meta.parse(str_us_l3Fl1F_1))
+ edge1 = Edge([:ALL], getfield(Main, :cc_aut_F_l3Fl1F_1), getfield(Main, sym_func_us_l3Fl1F_1))
map_edges[:l3F][:l1F] = [edge1]
-
- tuple = (:l3F, :l2F)
- @everywhere cc_aut_F_l3Fl2F_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (getfield(S, :time) >= constants[:t4])
- @everywhere us_aut_F_l3Fl2F_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
- (S.loc = :l2F)
- edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l3Fl2F_1), getfield(Main, :us_aut_F_l3Fl2F_1!))
-
+
+ # l3F => l2F
+ edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l3Fl2F_1), getfield(Main, :us_aut_F_l3Fl2F_1!))
map_edges[:l3F][:l2F] = [edge1]
## Constants
constants = Dict{Symbol,Float64}(:x1 => x1, :x2 => x2, :t1 => t1, :t2 => t2,
:x3 => x3, :x4 => x4, :t3 => t3, :t4 => t4)
-
+
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
diff --git a/core/MarkovProcesses.jl b/core/MarkovProcesses.jl
index f6e5d04..3485e75 100644
--- a/core/MarkovProcesses.jl
+++ b/core/MarkovProcesses.jl
@@ -18,7 +18,8 @@ export LHA, StateLHA, Edge, Location, VariableAutomaton
# Trajectory related methods
export +, -, δ, dist_lp
-export get_obs_var, length_states, length_obs_var, get_state_from_time
+export get_obs_var, length_states, length_obs_var
+export get_state_from_time, get_var_from_time, vectorize
export isbounded, times, transitions
export check_consistency, issteadystate, isaccepted
diff --git a/core/plots.jl b/core/plots.jl
index 64f9d22..1af2193 100644
--- a/core/plots.jl
+++ b/core/plots.jl
@@ -22,7 +22,7 @@ function plot(σ::AbstractTrajectory, vars::VariableModel...; plot_transitions::
end
# Plots
- p = plot(title = "Trajectory of $(σ.m.name) model", palette = :lightrainbow, background_color_legend=:transparent, dpi = 480)
+ p = plot(title = "Trajectory of $(σ.m.name) model", palette = :lightrainbow, legend = :outertopright, background_color_legend=:transparent, dpi = 480)
for var in to_plot
@assert var in get_obs_var(σ)
plot!(p, times(σ), σ[var],
@@ -76,8 +76,8 @@ function plot!(A::LHA)
end
# For tests purposes
-function plot_periodic_trajectory(A::LHA, σ::SynchronizedTrajectory, sym_obs::Symbol; verbose = false)
- @assert (σ.m).dim_state == σ.m.dim_obs_state # Model should be entirely obserbed
+function plot_periodic_trajectory(A::LHA, σ::SynchronizedTrajectory, sym_obs::Symbol; verbose = false, filename::String = "")
+ @assert sym_obs in get_obs_var(σ) "Variable is not observed in the model"
@assert A.name in ["Period"]
A_new = LHA(A, (σ.m)._map_obs_var_idx)
p_sim = (σ.m).p
@@ -111,15 +111,21 @@ function plot_periodic_trajectory(A::LHA, σ::SynchronizedTrajectory, sym_obs::S
loc_to_color(loc::Symbol) = colors_loc[loc]
for loc in A.locations
idx_locations = findall(x->x==loc, locations_trajectory)
- label_state = (loc in [:low, :mid, :high]) ? "State $sym_obs ($loc loc)" : ""
+ label_state = (loc in [:low, :mid, :high]) ? "$sym_obs ($loc loc)" : ""
scatter!(p, times(σ)[idx_locations], σ[sym_obs][idx_locations], color = colors_loc[loc],
markersize = 1.0, markershape = :cross,
- label = label_state)
+ label = label_state, xlabel = "Time", ylabel = "Species $sym_obs")
end
annot_n = [(times(σ)[idx_n[i]], σ[sym_obs][idx_n[i]] - 10, text("n = $(values_n[i])", 6, :bottom)) for i = eachindex(idx_n)]
scatter!(p, times(σ)[idx_n], σ[sym_obs][idx_n], annotations = annot_n,
markershape = :utriangle, markersize = 3, label = "n")
hline!(p, [A.constants[:L], A.constants[:H]], label = "L, H", color = :grey; linestyle = :dot)
+
+ if filename == ""
+ display(p)
+ else
+ png(p, filename)
+ end
end
export plot, plot!, plot_periodic_trajectory
diff --git a/core/trajectory.jl b/core/trajectory.jl
index b3a763f..c875281 100644
--- a/core/trajectory.jl
+++ b/core/trajectory.jl
@@ -149,6 +149,29 @@ function _riemann_sum(f::Function, t_begin::Real, t_end::Real, step::Float64)
return res
end
+function vectorize(σ::AbstractTrajectory, sym_var::Symbol,
+ timeline::AbstractVector{Float64})
+ times_var = times(σ)
+ time_end = isbounded(σ) ? times_var[end] : Inf
+ @assert timeline[end] <= time_end "Trajectory is bounded and timeline is out of bounds."
+ states_var = σ[sym_var]
+ nbr_states = length(states_var)
+ nbr_points = length(timeline)
+ trajectory_points = zeros(nbr_points)
+ index_timeline = 1
+ for i = eachindex(states_var)
+ next_transition_time = (i < nbr_states) ? times_var[i+1] : time_end*1.01
+ while index_timeline <= nbr_points && timeline[index_timeline] < next_transition_time
+ trajectory_points[index_timeline] = states_var[i]
+ index_timeline += 1
+ end
+ if index_timeline > nbr_points
+ break
+ end
+ end
+ return trajectory_points
+end
+
function check_consistency(σ::AbstractTrajectory)
test_length_var = true
for i = 1:σ.m.dim_obs_state
@@ -218,6 +241,26 @@ function get_state_from_time(σ::AbstractTrajectory, t::Float64)
end
error("Unexpected behavior")
end
+# Operation σ@t
+function get_var_from_time(σ::AbstractTrajectory, sym_var::Symbol, t::Float64)
+ @assert t >= 0.0
+ l_t = times(σ)
+ if t == l_t[end] return σ[sym_var][end] end
+ if t > l_t[end]
+ if !isbounded(σ)
+ return σ[sym_var][end]
+ else
+ error("This trajectory is bounded and you're accessing out of the bounds")
+ end
+ end
+ for i in eachindex(l_t)
+ if l_t[i] <= t < l_t[i+1]
+ return σ[sym_var][i]
+ end
+ end
+ error("Unexpected behavior")
+end
+
function getproperty(σ::SynchronizedTrajectory, sym::Symbol)
if sym == :sm
return getfield(σ, :sm)
diff --git a/tests/automata/two_automata.jl b/tests/automata/two_automata.jl
new file mode 100644
index 0000000..3796cde
--- /dev/null
+++ b/tests/automata/two_automata.jl
@@ -0,0 +1,16 @@
+
+using MarkovProcesses
+
+load_model("SIR")
+load_model("ER")
+
+new_SIR = deepcopy(SIR)
+sync_SIR = new_SIR * create_automaton_F(new_SIR, 0.0, Inf, 100.0, 110.0, :I)
+new_ER = deepcopy(ER)
+sync_ER = new_ER * create_automaton_F(new_ER, 0.0, 100.0, 4.0, 5.0, :P)
+
+simulate(sync_SIR)
+simulate(sync_ER)
+
+return true
+
diff --git a/tests/run_automata.jl b/tests/run_automata.jl
index 6f33f17..9046876 100644
--- a/tests/run_automata.jl
+++ b/tests/run_automata.jl
@@ -8,5 +8,6 @@ using Test
@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/two_automata.jl")
end
diff --git a/tests/run_unit.jl b/tests/run_unit.jl
index 55d5bf3..deb8bb1 100644
--- a/tests/run_unit.jl
+++ b/tests/run_unit.jl
@@ -42,5 +42,7 @@ using Test
@test include("unit/simulate_sir_bounded.jl")
@test include("unit/simulate_er.jl")
@test include("unit/square_wave_oscillator.jl")
+
+ @test include("unit/vectorize.jl")
end
diff --git a/tests/unit/vectorize.jl b/tests/unit/vectorize.jl
new file mode 100644
index 0000000..e4f243b
--- /dev/null
+++ b/tests/unit/vectorize.jl
@@ -0,0 +1,58 @@
+
+using MarkovProcesses
+load_model("ER")
+
+test_all = true
+
+# Unbounded
+tml = 0:0.1:10.0
+σ = simulate(ER)
+vec_traj = vectorize(σ, :P, tml)
+idx = 0
+for i = eachindex(vec_traj)
+ local test = convert(Int, vec_traj[i]) == get_var_from_time(σ, :P, tml[i])
+ global test_all = test_all && test
+ if !test
+ @show tml[i], convert(Int, vec_traj[i]), get_var_from_time(σ, :P, tml[i])
+ end
+end
+
+# Bounded
+set_time_bound!(ER, 2.0)
+tml = 0:0.1:2.0
+σ = simulate(ER)
+vec_traj = vectorize(σ, :P, tml)
+for i = eachindex(vec_traj)
+ local test = convert(Int, vec_traj[i]) == get_var_from_time(σ, :P, tml[i])
+ global test_all = test_all && test
+ if !test
+ @show tml[i], convert(Int, vec_traj[i]), get_var_from_time(σ, :P, tml[i])
+ end
+end
+
+set_time_bound!(ER, 1.0)
+tml = 0:0.02:0.9
+σ = simulate(ER)
+vec_traj = vectorize(σ, :P, tml)
+for i = eachindex(vec_traj)
+ local test = convert(Int, vec_traj[i]) == get_var_from_time(σ, :P, tml[i])
+ global test_all = test_all && test
+ if !test
+ @show tml[i], convert(Int, vec_traj[i]), get_var_from_time(σ, :P, tml[i])
+ end
+end
+
+set_time_bound!(ER, 2.0)
+tml = 0.5:0.1:2.0
+σ = simulate(ER)
+vec_traj = vectorize(σ, :P, tml)
+for i = eachindex(vec_traj)
+ local test = convert(Int, vec_traj[i]) == get_var_from_time(σ, :P, tml[i])
+ global test_all = test_all && test
+ if !test
+ @show tml[i], convert(Int, vec_traj[i]), get_var_from_time(σ, :P, tml[i])
+ end
+end
+
+return test_all
+
--
GitLab