diff --git a/automata/automaton_F.jl b/automata/automaton_F.jl index e0ff0e5cf228f049ab093d3e68ba9bd025fe5df8..bf4d4d7c66b2577a34aa5cfa385768ccc205a738 100644 --- a/automata/automaton_F.jl +++ b/automata/automaton_F.jl @@ -5,7 +5,7 @@ function create_automaton_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1 locations = [:l0, :l1, :l2, :l3] ## Invariant predicates - true_inv_predicate = (A::LHA, S:: StateLHA) -> return true + true_inv_predicate = (x::Vector{Int}) -> return true Λ_F = Dict(:l0 => true_inv_predicate, :l1 => true_inv_predicate, :l2 => true_inv_predicate, :l3 => true_inv_predicate) diff --git a/automata/automaton_G.jl b/automata/automaton_G.jl index 007d714c13d8e32a30d166f061deaf21fea22e30..2d439f45890d9ae9985cdf20d73b4403032c93af 100644 --- a/automata/automaton_G.jl +++ b/automata/automaton_G.jl @@ -5,7 +5,7 @@ function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1 locations = [:l0, :l1, :l2, :l3, :l4] # Invariant predicates - true_inv_predicate = (A::LHA, S:: StateLHA) -> return true + true_inv_predicate = (x::Vector{Int}) -> return true Λ_F = Dict(:l0 => true_inv_predicate, :l1 => true_inv_predicate, :l2 => true_inv_predicate, :l3 => true_inv_predicate, :l4 => true_inv_predicate) diff --git a/automata/automaton_G_and_F.jl b/automata/automaton_G_and_F.jl index f8b1c2bf2b97be4621365d92a0848c9bb6939e2e..ff5e2f9d5f8fdc3893131b6f0d7b80c7caeb729e 100644 --- a/automata/automaton_G_and_F.jl +++ b/automata/automaton_G_and_F.jl @@ -9,7 +9,7 @@ function create_automaton_G_and_F(m::ContinuousTimeModel, x1::Float64, x2::Float :l1F, :l2F, :l3F] # Invariant predicates - true_inv_predicate = (A::LHA, S:: StateLHA) -> return true + true_inv_predicate = (x::Vector{Int}) -> return true Λ_F = Dict(:l0G => true_inv_predicate, :l1G => true_inv_predicate, :l2G => true_inv_predicate, :l3G => true_inv_predicate, :l4G => true_inv_predicate, diff --git a/core/lha.jl b/core/lha.jl index 245d6079a1e646a8949d630ba2b23f76311f58c6..7b0823bb8904622ff38b523dd081d930798ed085 100644 --- a/core/lha.jl +++ b/core/lha.jl @@ -53,13 +53,14 @@ isaccepted(S::StateLHA) = (getfield(S, :loc) in getfield(getfield(S, :A), :locat function init_state(A::LHA, x0::Vector{Int}, t0::Float64) S0 = StateLHA(A, :init, zeros(length_var(A)), t0) for loc in getfield(A, :locations_init) - if A.Λ[loc](A,S0) + if A.Λ[loc](x0) S0.loc = loc break end end return S0 end + # A push! method implementend by myself because I know in most cases the edge candidates # are not greater than 2 function _push_edge!(edge_candidates::Vector{Edge}, edge::Edge, nbr_candidates::Int) @@ -71,13 +72,14 @@ function _push_edge!(edge_candidates::Vector{Edge}, edge::Edge, nbr_candidates:: end function _find_edge_candidates!(edge_candidates::Vector{Edge}, - edges_from_current_loc::Dict{Location,Vector{Edge}}, + edges_from_current_loc::Dict{Location,Vector{Edge}}, + Λ::Dict{Location,Function}, Snplus1::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, only_asynchronous::Bool) nbr_candidates = 0 for target_loc in keys(edges_from_current_loc) for edge in edges_from_current_loc[target_loc] - if getfield(edge, :check_constraints)(Snplus1, constants, x) + if Λ[target_loc](x) && getfield(edge, :check_constraints)(Snplus1, constants, x) if edge.transitions[1] == nothing _push_edge!(edge_candidates, edge, nbr_candidates) nbr_candidates += 1 @@ -139,7 +141,7 @@ function next_state!(Snplus1::StateLHA, A::LHA, current_loc = getfield(Snplus1, :loc) edges_from_current_loc = getfield(A, :map_edges)[current_loc] # Save all edges that satisfies transition predicate (asynchronous ones) - nbr_candidates = _find_edge_candidates!(edge_candidates, edges_from_current_loc, Snplus1, constants, xn, true) + nbr_candidates = _find_edge_candidates!(edge_candidates, edges_from_current_loc, getfield(A, :Λ), Snplus1, constants, xn, true) # Search the one we must chose, here the event is nothing because # we're not processing yet the next event ind_edge, detected_event = _get_edge_index(edge_candidates, nbr_candidates, detected_event, nothing) @@ -194,7 +196,7 @@ function next_state!(Snplus1::StateLHA, A::LHA, current_loc = getfield(Snplus1, :loc) edges_from_current_loc = getfield(A, :map_edges)[current_loc] # Save all edges that satisfies transition predicate (synchronous ones) - nbr_candidates = _find_edge_candidates!(edge_candidates, edges_from_current_loc, Snplus1, constants, xnplus1, false) + nbr_candidates = _find_edge_candidates!(edge_candidates, edges_from_current_loc, getfield(A, :Λ), Snplus1, constants, xnplus1, false) # Search the one we must chose ind_edge, detected_event = _get_edge_index(edge_candidates, nbr_candidates, detected_event, tr_nplus1) # Update the state with the chosen one (if it exists)