From b1c40b0f55435e903a1bf9a0cc8e2b9cc5088e5b Mon Sep 17 00:00:00 2001
From: Mahmoud Bentriou <mahmoud.bentriou@centralesupelec.fr>
Date: Mon, 25 Jan 2021 09:29:46 +0100
Subject: [PATCH] Supplementary checks on automata + small fix on unit tests
---
automata/automaton_F.jl | 4 ++++
automata/automaton_G.jl | 6 +++++-
automata/automaton_G_and_F.jl | 16 ++++++++++++----
automata/euclidean_distance_automaton.jl | 5 +++--
automata/period_automaton.jl | 4 ++++
tests/automata/two_automata.jl | 17 ++++++++++++++++-
tests/dist_lp/dist_sim_sir.jl | 2 +-
7 files changed, 45 insertions(+), 9 deletions(-)
diff --git a/automata/automaton_F.jl b/automata/automaton_F.jl
index 203b8b9..b18b37e 100644
--- a/automata/automaton_F.jl
+++ b/automata/automaton_F.jl
@@ -72,7 +72,11 @@ istrue(S[:isabs]) && getfield(S, :time) <= constants[:t2]
(S.loc = :l2)
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 (x1 <= x2) "x1 > x2 impossible for F automaton."
+ @assert (t1 <= t2) "t1 > t2 impossible for F automaton."
+
# Locations
locations = [:l0, :l1, :l2, :l3]
diff --git a/automata/automaton_G.jl b/automata/automaton_G.jl
index 2caa939..b07a479 100644
--- a/automata/automaton_G.jl
+++ b/automata/automaton_G.jl
@@ -118,7 +118,11 @@ getfield(S, :time) >= constants[:t2]
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
+ # 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 = [:l0, :l1, :l2, :l3, :l4]
diff --git a/automata/automaton_G_and_F.jl b/automata/automaton_G_and_F.jl
index 0e3c286..bd42caf 100644
--- a/automata/automaton_G_and_F.jl
+++ b/automata/automaton_G_and_F.jl
@@ -1,9 +1,12 @@
@everywhere istrue(val::Float64) = convert(Bool, val)
-# Invariant predicate functions
+## Invariant predicate functions
+
@everywhere true_inv_predicate(x::Vector{Int}) = true
+## Edges check constraint and update state functions
+
# l0G loc
# l0G => l1G
@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]
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)
-
- @assert sym_obs_G in m.g
- @assert sym_obs_F in m.g
+ # Requirements for the automaton
+ @assert sym_obs_G in m.g && sym_obs_F in m.g "$(sym_obs_G) or $(sym_obs_F) are not observed."
+ @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 = [:l0G, :l1G, :l2G, :l3G, :l4G,
:l1F, :l2F, :l3F]
diff --git a/automata/euclidean_distance_automaton.jl b/automata/euclidean_distance_automaton.jl
index 703b222..7b64a18 100644
--- a/automata/euclidean_distance_automaton.jl
+++ b/automata/euclidean_distance_automaton.jl
@@ -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
-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 length(timeline) == length(observations)
+ @assert length(timeline) == length(observations) "Timeline and observations vectors don't have the same length"
nbr_observations = length(observations)
# Locations
diff --git a/automata/period_automaton.jl b/automata/period_automaton.jl
index fe6d7f4..653efe7 100644
--- a/automata/period_automaton.jl
+++ b/automata/period_automaton.jl
@@ -136,7 +136,11 @@ S[:n] == constants[:N]
function create_period_automaton(m::ContinuousTimeModel, L::Float64, H::Float64, N::Int, sym_obs::VariableModel;
initT::Float64 = 0.0)
+ # Requirements for the automaton
@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)
nbr_rand = rand(1:1000)
basename_func = "$(replace(m.name, ' '=>'_'))_$(nbr_rand)"
diff --git a/tests/automata/two_automata.jl b/tests/automata/two_automata.jl
index 3796cde..c4c86a9 100644
--- a/tests/automata/two_automata.jl
+++ b/tests/automata/two_automata.jl
@@ -3,12 +3,27 @@ using MarkovProcesses
load_model("SIR")
load_model("ER")
+load_automaton("automaton_F")
+load_automaton("automaton_G")
+load_automaton("automaton_G_and_F")
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)
+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)
+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_ER)
diff --git a/tests/dist_lp/dist_sim_sir.jl b/tests/dist_lp/dist_sim_sir.jl
index 728a4ec..35559ef 100644
--- a/tests/dist_lp/dist_sim_sir.jl
+++ b/tests/dist_lp/dist_sim_sir.jl
@@ -7,7 +7,7 @@ SIR.time_bound = time_bound
test_all = true
for p = 1:2
- nb_sim = 10
+ local nb_sim = 10
for i = 1:nb_sim
let σ1, σ2, test, test2
σ1 = simulate(SIR)
--
GitLab