Commit b3e1e771 authored by Bentriou Mahmoud's avatar Bentriou Mahmoud
Browse files

pretty print lha + better semantic for true inv predicate

parent 608d99b5
......@@ -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 = (x::Vector{Int}) -> return true
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)
......
......@@ -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 = (x::Vector{Int}) -> return true
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,
:l4 => true_inv_predicate)
......
......@@ -9,7 +9,7 @@ function create_automaton_G_and_F(m::ContinuousTimeModel, x1::Float64, x2::Float
:l1F, :l2F, :l3F]
# Invariant predicates
true_inv_predicate = (x::Vector{Int}) -> return true
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,
......
......@@ -16,6 +16,37 @@ getindex(S::StateLHA, l_var::Vector{VariableAutomaton}) = [S[var] for var in l_v
setindex!(S::StateLHA, val::Int, var::VariableAutomaton) = S[var] = convert(Float64, val)
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, "- initial locations : $(join(A.locations_init,','))\n")
print(io, "- final locations : $(join(A.locations_final,','))\n")
print(io, "- labeling prop Λ :\n")
for loc in keys(A.Λ)
print(io, "* $loc: $(Symbol(A.Λ[loc]))\n")
end
print(io, "- variables :\n")
for (var, idx) in A.map_var_automaton_idx
print(io, "* $var (index = $idx in variables space)\n")
end
print(io, "- flow :\n")
for (loc, flow_loc) in A.flow
print(io, "* $loc: $flow_loc\n")
end
print(io, "- edges :\n")
for from_loc in keys(A.map_edges)
for to_loc in keys(A.map_edges[from_loc])
edges = A.map_edges[from_loc][to_loc]
print(io, "* $from_loc => $to_loc ($(length(edges))): $(join(edges,','))\n")
end
end
print(io, "- constants :\n")
for (name_constant, val_constant) in A.constants
print(io, "* $name_constant: $val_constant\n")
end
print(io, "- transitions : $(join(A.transitions,','))\n")
end
function Base.show(io::IO, S::StateLHA)
print(io, "State of LHA\n")
print(io, "- location: $(S.loc)\n")
......
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