From b3e1e77190a3b2774297436434d5e4dab7b397d1 Mon Sep 17 00:00:00 2001
From: Mahmoud Bentriou <mahmoud.bentriou@centralesupelec.fr>
Date: Sun, 10 Jan 2021 13:20:41 +0100
Subject: [PATCH] pretty print lha + better semantic for true inv predicate
---
automata/automaton_F.jl | 2 +-
automata/automaton_G.jl | 2 +-
automata/automaton_G_and_F.jl | 2 +-
core/lha.jl | 31 +++++++++++++++++++++++++++++++
4 files changed, 34 insertions(+), 3 deletions(-)
diff --git a/automata/automaton_F.jl b/automata/automaton_F.jl
index bf4d4d7..3c59e86 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 = (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)
diff --git a/automata/automaton_G.jl b/automata/automaton_G.jl
index 2d439f4..76f7e62 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 = (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)
diff --git a/automata/automaton_G_and_F.jl b/automata/automaton_G_and_F.jl
index ff5e2f9..87c79b5 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 = (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,
diff --git a/core/lha.jl b/core/lha.jl
index 7b0823b..8bf648b 100644
--- a/core/lha.jl
+++ b/core/lha.jl
@@ -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")
--
GitLab