Skip to content
Snippets Groups Projects
Commit b1c40b0f authored by Bentriou Mahmoud's avatar Bentriou Mahmoud
Browse files

Supplementary checks on automata + small fix on unit tests

parent db00da08
No related branches found
No related tags found
No related merge requests found
...@@ -72,7 +72,11 @@ istrue(S[:isabs]) && getfield(S, :time) <= constants[:t2] ...@@ -72,7 +72,11 @@ istrue(S[:isabs]) && getfield(S, :time) <= constants[:t2]
(S.loc = :l2) (S.loc = :l2)
function create_automaton_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, sym_obs::VariableModel) function create_automaton_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, sym_obs::VariableModel)
# Requirements for the automaton
@assert sym_obs in m.g "$(sym_obs) is not observed." @assert sym_obs in m.g "$(sym_obs) is not observed."
@assert (x1 <= x2) "x1 > x2 impossible for F automaton."
@assert (t1 <= t2) "t1 > t2 impossible for F automaton."
# Locations # Locations
locations = [:l0, :l1, :l2, :l3] locations = [:l0, :l1, :l2, :l3]
......
...@@ -118,7 +118,11 @@ getfield(S, :time) >= constants[:t2] ...@@ -118,7 +118,11 @@ getfield(S, :time) >= constants[:t2]
S[:tprime] = 0.0) S[:tprime] = 0.0)
function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, sym_obs::VariableModel) function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, sym_obs::VariableModel)
@assert sym_obs in m.g # Requirements for the automaton
@assert sym_obs in m.g "$(sym_obs) is not observed."
@assert (x1 <= x2) "x1 > x2 impossible for G automaton."
@assert (t1 <= t2) "t1 > t2 impossible for G automaton."
# Locations # Locations
locations = [:l0, :l1, :l2, :l3, :l4] locations = [:l0, :l1, :l2, :l3, :l4]
......
@everywhere istrue(val::Float64) = convert(Bool, val) @everywhere istrue(val::Float64) = convert(Bool, val)
# Invariant predicate functions ## Invariant predicate functions
@everywhere true_inv_predicate(x::Vector{Int}) = true @everywhere true_inv_predicate(x::Vector{Int}) = true
## Edges check constraint and update state functions
# l0G loc # l0G loc
# l0G => l1G # l0G => l1G
@everywhere cc_aut_G_l0Gl1G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true @everywhere cc_aut_G_l0Gl1G_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
...@@ -185,9 +188,14 @@ istrue(S[:isabs]) && getfield(S, :time) <= constants[:t4] ...@@ -185,9 +188,14 @@ istrue(S[:isabs]) && getfield(S, :time) <= constants[:t4]
function create_automaton_G_and_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, sym_obs_G::VariableModel, 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) x3::Float64, x4::Float64, t3::Float64, t4::Float64, sym_obs_F::VariableModel)
# Requirements for the automaton
@assert sym_obs_G in m.g @assert sym_obs_G in m.g && sym_obs_F in m.g "$(sym_obs_G) or $(sym_obs_F) are not observed."
@assert sym_obs_F in m.g @assert (x1 <= x2) "x1 > x2 impossible for G and F automaton."
@assert (t1 <= t2) "t1 > t2 impossible for G and F automaton."
@assert (x3 <= x4) "x3 > x3 impossible for G and F automaton."
@assert (t3 <= t4) "t3 > t4 impossible for G and F automaton."
@assert (t2 <= t3) "t3 > t2 impossible for G and F automaton."
# Locations # Locations
locations = [:l0G, :l1G, :l2G, :l3G, :l4G, locations = [:l0G, :l1G, :l2G, :l3G, :l4G,
:l1F, :l2F, :l3F] :l1F, :l2F, :l3F]
......
...@@ -20,9 +20,10 @@ S[:idx] >= constants[:nbr_obs] + 1 ...@@ -20,9 +20,10 @@ S[:idx] >= constants[:nbr_obs] + 1
@everywhere cc_eucl_dist_aut_l1l1_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true @everywhere cc_eucl_dist_aut_l1l1_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
function create_euclidean_distance_automaton(m::ContinuousTimeModel, timeline::Vector{Float64}, observations::Vector{Float64}, sym_obs::VariableModel) function create_euclidean_distance_automaton(m::ContinuousTimeModel, timeline::AbstractVector{Float64}, observations::AbstractVector{Float64}, sym_obs::VariableModel)
# Requirements for the automaton
@assert sym_obs in m.g "$(sym_obs) is not observed." @assert sym_obs in m.g "$(sym_obs) is not observed."
@assert length(timeline) == length(observations) @assert length(timeline) == length(observations) "Timeline and observations vectors don't have the same length"
nbr_observations = length(observations) nbr_observations = length(observations)
# Locations # Locations
......
...@@ -136,7 +136,11 @@ S[:n] == constants[:N] ...@@ -136,7 +136,11 @@ S[:n] == constants[:N]
function create_period_automaton(m::ContinuousTimeModel, L::Float64, H::Float64, N::Int, sym_obs::VariableModel; function create_period_automaton(m::ContinuousTimeModel, L::Float64, H::Float64, N::Int, sym_obs::VariableModel;
initT::Float64 = 0.0) initT::Float64 = 0.0)
# Requirements for the automaton
@assert sym_obs in m.g "$(sym_obs) is not observed." @assert sym_obs in m.g "$(sym_obs) is not observed."
@assert (L < H) "L >= H impossible for period automaton."
@assert (N >= 1) "N < 1 impossible for period automaton."
N = convert(Float64, N) N = convert(Float64, N)
nbr_rand = rand(1:1000) nbr_rand = rand(1:1000)
basename_func = "$(replace(m.name, ' '=>'_'))_$(nbr_rand)" basename_func = "$(replace(m.name, ' '=>'_'))_$(nbr_rand)"
......
...@@ -3,12 +3,27 @@ using MarkovProcesses ...@@ -3,12 +3,27 @@ using MarkovProcesses
load_model("SIR") load_model("SIR")
load_model("ER") load_model("ER")
load_automaton("automaton_F")
load_automaton("automaton_G")
load_automaton("automaton_G_and_F")
new_SIR = deepcopy(SIR) 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) new_ER = deepcopy(ER)
observe_all!(new_SIR)
observe_all!(new_ER)
sync_SIR = new_SIR * create_automaton_F(new_SIR, 0.0, 0.0, 100.0, 110.0, :I)
sync_ER = new_ER * create_automaton_F(new_ER, 0.0, 100.0, 4.0, 5.0, :P) sync_ER = new_ER * create_automaton_F(new_ER, 0.0, 100.0, 4.0, 5.0, :P)
simulate(sync_SIR)
simulate(sync_ER)
sync_SIR = new_SIR * create_automaton_G(new_SIR, 1.0, Inf, 0.0, 100.0, :I)
sync_ER = new_ER * create_automaton_G(new_ER, 50.0, 100.0, 0.0, 5.0, :E)
simulate(sync_SIR)
simulate(sync_ER)
sync_SIR = new_SIR * create_automaton_G_and_F(new_SIR, 1.0, Inf, 0.0, 100.0, :I, 0.0, Inf, 100.0, 110.0, :I)
sync_ER = new_ER * create_automaton_G_and_F(new_ER, 50.0, 100.0, 0.0, 5.0, :E, 40.0, 100.0, 5.0, 6.0, :P)
simulate(sync_SIR) simulate(sync_SIR)
simulate(sync_ER) simulate(sync_ER)
......
...@@ -7,7 +7,7 @@ SIR.time_bound = time_bound ...@@ -7,7 +7,7 @@ SIR.time_bound = time_bound
test_all = true test_all = true
for p = 1:2 for p = 1:2
nb_sim = 10 local nb_sim = 10
for i = 1:nb_sim for i = 1:nb_sim
let σ1, σ2, test, test2 let σ1, σ2, test, test2
σ1 = simulate(SIR) σ1 = simulate(SIR)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment