Commit 575ef324 authored by Bentriou Mahmoud's avatar Bentriou Mahmoud
Browse files

1) LHA now have names. 2) Period automaton executes well and was runned on the...

1) LHA now have names. 2) Period automaton executes well and was runned on the doping 3way oscillator model. Not stattistically tested yet
parent ed25af50
......@@ -37,97 +37,97 @@ function create_automaton_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
# l0 loc : we construct the edges of the form l0 => (..)
# "cc" as check_constraints
tuple = (:l0, :l1)
cc_aut_F_l0l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
us_aut_F_l0l1_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@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, sym_obs);
S[:n] = get_value(S, x, $(Meta.quot(sym_obs)));
S[:d] = Inf;
S[:isabs] = getfield(Main, sym_isabs_func)(p, x))
edge1 = Edge([nothing], cc_aut_F_l0l1_1, us_aut_F_l0l1_1!)
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!))
map_edges[:l0][:l1] = [edge1]
# l1 loc : we construct the edges of the form l1 => (..)
tuple = (:l1, :l2)
cc_aut_F_l1l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@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])
us_aut_F_l1l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@everywhere us_aut_F_l1l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
(S.loc = :l2;
S[:d] = 0)
edge1 = Edge([nothing], cc_aut_F_l1l2_1, us_aut_F_l1l2_1!)
edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l1l2_1), getfield(Main, :us_aut_F_l1l2_1!))
cc_aut_F_l1l2_4(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@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
us_aut_F_l1l2_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@everywhere us_aut_F_l1l2_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
(S.loc = :l2)
edge4 = Edge([nothing], cc_aut_F_l1l2_4, us_aut_F_l1l2_4!)
edge4 = Edge([nothing], getfield(Main, :cc_aut_F_l1l2_4), getfield(Main, :us_aut_F_l1l2_4!))
cc_aut_F_l1l2_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@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])
us_aut_F_l1l2_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@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], cc_aut_F_l1l2_2, us_aut_F_l1l2_2!)
edge2 = Edge([nothing], getfield(Main, :cc_aut_F_l1l2_2), getfield(Main, :us_aut_F_l1l2_2!))
cc_aut_F_l1l2_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@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]
us_aut_F_l1l2_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@everywhere us_aut_F_l1l2_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
(S.loc = :l2)
edge3 = Edge([nothing], cc_aut_F_l1l2_3, us_aut_F_l1l2_3!)
edge3 = Edge([nothing], getfield(Main, :cc_aut_F_l1l2_3), getfield(Main, :us_aut_F_l1l2_3!))
map_edges[:l1][:l2] = [edge1, edge2, edge3, edge4]
tuple = (:l1, :l3)
cc_aut_F_l1l3_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@everywhere cc_aut_F_l1l3_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
(constants[:x1] <= S[:n] <= constants[:x2])
us_aut_F_l1l3_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@everywhere us_aut_F_l1l3_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
(S.loc = :l3;
S[:d] = 0;)
edge1 = Edge([nothing], cc_aut_F_l1l3_1, us_aut_F_l1l3_1!)
edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l1l3_1), getfield(Main, :us_aut_F_l1l3_1!))
cc_aut_F_l1l3_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@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])
us_aut_F_l1l3_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@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], cc_aut_F_l1l3_2, us_aut_F_l1l3_2!)
edge2 = Edge([nothing], getfield(Main, :cc_aut_F_l1l3_2), getfield(Main, :us_aut_F_l1l3_2!))
cc_aut_F_l1l3_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@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])
us_aut_F_l1l3_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@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], cc_aut_F_l1l3_3, us_aut_F_l1l3_3!)
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)
cc_aut_F_l3l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
us_aut_F_l3l1_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@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, sym_obs);
S[:isabs] = getfield(Main, sym_isabs_func)(p, x))
edge1 = Edge([:ALL], cc_aut_F_l3l1_1, us_aut_F_l3l1_1!)
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!))
map_edges[:l3][:l1] = [edge1]
tuple = (:l3, :l2)
cc_aut_F_l3l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@everywhere cc_aut_F_l3l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
(getfield(S, :time) >= constants[:t2])
us_aut_F_l3l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
@everywhere us_aut_F_l3l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) =
(S.loc = :l2)
edge1 = Edge([nothing], cc_aut_F_l3l2_1, us_aut_F_l3l2_1!)
edge1 = Edge([nothing], getfield(Main, :cc_aut_F_l3l2_1), getfield(Main, :us_aut_F_l3l2_1!))
map_edges[:l3][:l2] = [edge1]
## Constants
constants = Dict{Symbol,Float64}(:x1 => x1, :x2 => x2, :t1 => t1, :t2 => t2)
A = LHA(m.transitions, locations, Λ_F, locations_init, locations_final,
A = LHA("F property", m.transitions, locations, Λ_F, locations_init, locations_final,
map_var_automaton_idx, flow, map_edges, constants, m.map_var_idx)
return A
end
......
......@@ -195,7 +195,7 @@ function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
## Constants
constants = Dict{Symbol,Float64}(:x1 => x1, :x2 => x2, :t1 => t1, :t2 => t2)
A = LHA(m.transitions, locations, Λ_F, locations_init, locations_final,
A = LHA("G property", m.transitions, locations, Λ_F, locations_init, locations_final,
map_var_automaton_idx, flow, map_edges, constants, m.map_var_idx)
return A
......
This diff is collapsed.
......@@ -45,6 +45,7 @@ struct Edge
end
struct LHA
name::String
transitions::Vector{Transition}
locations::Vector{Location}
Λ::Dict{Location,Function}
......@@ -112,9 +113,10 @@ function ContinuousTimeModel(dim_state::Int, dim_params::Int, map_var_idx::Dict{
return new_model
end
LHA(A::LHA, map_var::Dict{VariableModel,Int}) = LHA(A.transitions, A.locations, A.Λ,
LHA(A::LHA, map_var::Dict{VariableModel,Int}) = LHA(A.name, A.transitions, A.locations, A.Λ,
A.locations_init, A.locations_final, A.map_var_automaton_idx, A.flow,
A.map_edges, A.constants, map_var)
Base.:*(m::ContinuousTimeModel, A::LHA) = SynchronizedModel(m, A)
Base.:*(A::LHA, m::ContinuousTimeModel) = SynchronizedModel(m, A)
......
......@@ -17,8 +17,7 @@ setindex!(S::StateLHA, val::Int, var::VariableAutomaton) = S[var] = convert(Floa
setindex!(S::StateLHA, val::Bool, var::VariableAutomaton) = S[var] = convert(Float64, val)
function Base.show(io::IO, A::LHA)
print(io, "LHA\n")
print(io, "- locations : $(join(A.locations,','))\n")
print(io, "$(A.name) automaton (LHA)\n")
print(io, "- initial locations : $(join(A.locations_init,','))\n")
print(io, "- final locations : $(join(A.locations_final,','))\n")
print(io, "- labeling prop Λ :\n")
......@@ -159,7 +158,7 @@ function next_state!(Snplus1::StateLHA, A::LHA,
turns = 0
if verbose
println("#####")
println("##### Begin next_state!")
@show xnplus1, tnplus1, tr_nplus1
@show Sn
@show Snplus1
......@@ -262,6 +261,7 @@ function next_state!(Snplus1::StateLHA, A::LHA,
error("Unpredicted behavior automaton")
end
end
if verbose println("##### End next_state!") end
end
# For tests purposes
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment