Theory Modest_MDP
section ‹Isabelel Model of the Modest MDP Data Structure›
theory Modest_MDP
imports Graph_Impl SharedNat "../lib/More_B_Assn"
begin
subsection ‹Miscellaneous›
lemma Id_list_set_rel: "⟨Id⟩list_set_rel = {(xs, set xs) | xs. distinct xs}"
unfolding list_set_rel_def
apply(auto simp: br_def )
done
lemma Id_list_set_relI: "distinct xs ⟹ X = set xs ⟹ (xs, X) ∈ ⟨Id⟩list_set_rel"
unfolding list_set_rel_def
apply(auto simp: br_def )
done
lemma nth_to_list_all: "(⋀i. i < length xs ⟹ P (xs!i)) ⟹ list_all P xs"
apply(induction xs rule: rev_induct)
apply auto
apply (metis less_SucI nth_append_first)
by (metis lessI nth_append_length)
lemma list_all_to_nth: "list_all P xs ⟹ i < length xs ⟹ P (xs!i)"
apply(induction xs rule: rev_induct)
apply auto
by (metis less_Suc_eq nth_append_first nth_append_length)
subsection ‹Intermediate Level Model›
text ‹We start by defining a graph model based on lists and (tuples) of natural numbers›
type_synonym modest_graph = "(nat × nat) list × (nat × nat) list × nat list"
text ‹The modest data structure contains three lists respresenting States, Transitions and
Branches. The list of states is a triple (tuple in this representation) which respectively
contains the number of transitions, first index in the list of transitions and the exitrate
(NaN for MDP's, so it is not modelled).
The list of transitions similarly is a tuple which contains respectively the number of branches
that the transition has as well as the first index in the branch list.
The list of branches contains a tuple (single value in this representation) with the transition
probability and the index of the successor state in the state list
›
abbreviation(input) "ind ≡ shared_right"
abbreviation(input) "cnt ≡ shared_left"
abbreviation(input) "lid ≡ shared_right"
abbreviation(input) "uid ≡ shared_sum"
definition "in_intv sn i = (lid sn ≤ i ∧ i < uid sn)"
definition "sn_intv sn = Collect (in_intv sn)"
definition "ls_intv sn = [lid sn..<uid sn]"
lemma sn_intv_alt: "sn_intv sn = {lid sn..<uid sn}"
unfolding sn_intv_def in_intv_def
by auto
lemma in_intv_lbD: "in_intv sn i ⟹ lid sn ≤ i"
unfolding in_intv_def
by blast
lemma in_intv_ubD: "in_intv sn i ⟹ i < uid sn"
unfolding in_intv_def
by blast
lemma sn_intv_member[simp]: "i ∈ sn_intv sn ⟷ in_intv sn i"
by (auto simp: in_intv_def sn_intv_def)
lemma in_intvI: "lid sn ≤ i ⟹ i < uid sn ⟹ in_intv sn i"
apply(fold sn_intv_member)
unfolding sn_intv_alt
by simp
lemma finite_sn_intv[simp]: "finite (sn_intv sn)"
unfolding sn_intv_alt
by simp
lemma set_ls_intv[simp]: "set (ls_intv sn) = sn_intv sn"
unfolding ls_intv_def sn_intv_alt by simp
lemma distinct_ls_intv[simp]: "distinct (ls_intv sn)"
unfolding ls_intv_def
by simp
locale modest_graph_def =
fixes SS :: "modest_graph"
begin
definition "S = (λ (S,T,B). S) SS"
definition "T = (λ (S,T,B). T) SS"
definition "B = (λ (S,T,B). B) SS"
definition "α = {(u,v)| u v. (∃ i j. in_intv (S!u) i ∧ in_intv (T!i) j ∧ v = B!j ∧ u < length S)}"
definition "graph_structure_branches i = {(u,v)| u v. (∃ j. in_intv (S!u) i ∧ in_intv (T!i) j ∧ v = B!j ∧ u < length S)}"
definition "graph_structure_edges = {(u,v)| u v. (∃ i j. in_intv (S!u) i ∧ in_intv (T!i) j ∧ v = B!j ∧ u < length S)}"
definition "graph_structure_branch_index_list t = ls_intv (T!t)"
lemma distinct_graph_structure_branch_index_list[simp]: "distinct (graph_structure_branch_index_list t)"
unfolding graph_structure_branch_index_list_def by simp
definition "graph_structure_edge_index_list s = fold (λ t a. a @ (ls_intv (T ! t))) (ls_intv (S ! s)) []"
lemma "graph_structure_edge_index_list s = fold (λ t a. a @ graph_structure_branch_index_list t) (ls_intv (S ! s)) []"
unfolding graph_structure_edge_index_list_def graph_structure_branch_index_list_def
by simp
lemma indep_succs: "u < length S ⟹ (u,v) ∈ α ⟷ (u,v) ∈ graph_structure_edges"
unfolding α_def graph_structure_edges_def
by blast
lemma indep_succs_branchesD: "u < length S ⟹ in_intv (S ! u) i ⟹ (u,v) ∈ graph_structure_branches i ⟹ (u,v) ∈ α"
unfolding α_def graph_structure_branches_def apply auto done
lemma indep_succs_branches: "u < length S ⟹ (u,v) ∈ ⋃(graph_structure_branches ` sn_intv (S ! u)) ⟷ (u,v) ∈ α"
unfolding α_def graph_structure_branches_def sn_intv_def apply auto done
lemma graph_structure_branches_to_edges: "(⋃i ∈ sn_intv (S!u). (graph_structure_branches i) `` {u}) = graph_structure_edges `` {u}"
unfolding graph_structure_branches_def graph_structure_edges_def sn_intv_def
apply auto
done
lemma indep_graph_structure_edges: "u < length S ⟹ α `` {u} = graph_structure_edges `` {u}"
using indep_succs
by auto
end
lemma SS_sel_simps[simp]:
"modest_graph_def.S (S,T,B) = S"
"modest_graph_def.T (S,T,B) = T"
"modest_graph_def.B (S,T,B) = B"
unfolding modest_graph_def.S_def modest_graph_def.T_def modest_graph_def.B_def
by auto
lemmas unfolded_indep_succs = modest_graph_def.indep_succs[of _ "(_,_,_)", simplified]
subsubsection ‹Invariant›
locale modest_graph_invar = modest_graph_def SS for N⇩s SS +
assumes NS_DEF: "N⇩s = length S"
assumes S_in_bound: "∀i < length S. uid (S!i) < length T"
assumes T_in_bound: "∀i < length T. uid (T!i) < length B"
assumes B_in_bound: "∀i < length B. B!i < length S"
assumes T_nonempty: "∀i < length S. cnt (S!i) > 0"
assumes B_nonempty: "∀i < length T. cnt (T!i) > 0"
assumes T_is_succ: "∀i < length T. ∃j < length S. lid (S!j) ≤ i ∧ i < uid (S!j)"
assumes B_is_succ: "∀i < length B. ∃j < length T. lid (T!j) ≤ i ∧ i < uid (T!j)"
assumes S_intv_disj: "∀ i < length S. (∀ j < i. sn_intv (S ! i) ∩ sn_intv (S ! j) = {})"
assumes T_intv_disj: "∀ i < length T. (∀ j < i. sn_intv (T ! i) ∩ sn_intv (T ! j) = {})"
begin
lemma succ_in_bound:
assumes "(u,v) ∈ α"
shows "v < length S"
proof -
obtain i j where "lid (S!u) ≤ i" and IU:"i < uid (S!u)" and "lid (T!i) ≤ j" and JU:"j < uid (T!i)" and V_DEF: "v = B!j" and UU: "u < length S"
using assms
unfolding α_def in_intv_def
by blast
hence "j < length B"
using S_in_bound T_in_bound order.strict_trans
by blast
then show ?thesis
using B_in_bound
unfolding NS_DEF V_DEF
by fast
qed
lemma edge_from_transistionD:
assumes IB: "i < length S"
assumes JB: "in_intv (S ! i) j"
assumes KB: "in_intv (T ! j) k"
shows "(i, B ! k) ∈ α"
using S_in_bound T_in_bound B_in_bound
unfolding α_def
using assms
by blast
lemma graph_structure_edgesD:
assumes IB: "i < length S"
assumes JB: "in_intv (S ! i) j"
assumes KB: "in_intv (T ! j) k"
shows "(i, B ! k) ∈ graph_structure_edges"
unfolding graph_structure_edges_def
using assms
by blast
lemma graph_structure_branchesD:
assumes IB: "i < length S"
assumes JB: "in_intv (S ! i) j"
assumes KB: "in_intv (T ! j) k"
shows "(i, B ! k) ∈ graph_structure_branches j"
unfolding graph_structure_branches_def
using assms
by blast
lemma T_in_boundD: "v < length S ⟹ t < uid (S ! v) ⟹ t < length T"
using S_in_bound
by auto
lemma B_in_boundD: "t < length T ⟹ b < uid (T ! t) ⟹ b < length B"
using T_in_bound
by auto
lemma S_in_boundI: "b < length B ⟹ B ! b < length S"
using B_in_bound
by auto
lemma T_in_bound_intvD: "v < length S ⟹ in_intv (S ! v) t ⟹ t < length T"
by(auto elim!: T_in_boundD dest: in_intv_ubD)
lemma B_in_bound_intvD: "t < length T ⟹ in_intv (T ! t) b ⟹ b < length B"
by(auto elim!: B_in_boundD dest: in_intv_ubD)
lemma graph_structure_branches_to_B:
assumes IB: "v < length S"
assumes JB: "in_intv (S ! v) t"
assumes "b = T ! t"
shows "(graph_structure_branches t) `` {v} = (!) B ` sn_intv b"
unfolding graph_structure_branches_def
apply (auto simp: assms)
done
lemma "distinct (graph_structure_edge_index_list s)"
unfolding graph_structure_edge_index_list_def oops
end
subsubsection ‹Refinement to Graph›
definition "modest_graph_rel N = br modest_graph_def.α (modest_graph_invar N)"
subsubsection ‹Finding Successor Nodes›
context modest_graph_def
begin
definition "get_transitions_of_state v =
do{
ASSERT(v < length S);
let r = S ! v;
ASSERT(shared_sum r ≤ length T);
RETURN r
}"
definition "get_branches_of_transition t =
do{
ASSERT(t < length T);
let r = T ! t;
ASSERT(shared_sum r ≤ length B);
RETURN r
}"
definition "get_successor_of_branch b =
do{
ASSERT(b < length B);
let r = B ! b;
ASSERT (r < length S);
RETURN r
}"
definition modest_graph_structure_inner_succs :: "nat ⇒ nat list ⇒ nat list nres" where "modest_graph_structure_inner_succs it succs =
do{
t ← get_branches_of_transition it;
FOREACH (sn_intv t) (λ it2 succs.
do{
ASSERT(it2 ∈ sn_intv t);
b ← get_successor_of_branch it2;
ASSERT(Suc (length succs) ≤ length B);
RETURN (op_list_append succs b)
}) succs
}"
definition modest_graph_succ :: "nat ⇒ nat list nres" where "modest_graph_succ v =
do{
s ← get_transitions_of_state v;
FOREACH (sn_intv s) (λit succs. do {
ASSERT(it ∈ sn_intv s);
modest_graph_structure_inner_succs it succs
}) []
}"
end
context modest_graph_invar
begin
lemma get_transitions_of_state_refine:
assumes "v < length S"
shows "get_transitions_of_state v ≤ SPEC (λ r. r = S ! v ∧ shared_sum r ≤ length T)"
unfolding get_transitions_of_state_def
apply(refine_vcg)
using S_in_bound assms
apply auto
done
lemma get_branches_of_transition_refine:
assumes "t < length T"
shows "get_branches_of_transition t ≤ SPEC (λ r. r = T ! t)"
unfolding get_branches_of_transition_def
apply(refine_vcg)
using T_in_bound assms
apply auto
done
lemma get_successor_of_branch_refine:
assumes "b < length B"
shows "get_successor_of_branch b ≤ SPEC (λ r. r = B ! b)"
unfolding get_successor_of_branch_def
apply(refine_vcg)
using B_in_bound assms
apply auto
done
lemma modest_graph_structure_inner_succs_refine':
fixes it
defines "s⇩0 ≡ sn_intv (T!it)"
assumes XS_IN_B: "∀ x ∈ set xs. x < length B"
assumes SUCC_EQ: "succs = map ((!) B) xs" "distinct xs" "set xs ∩ s⇩0 = {}"
assumes ITB: "in_intv (S!v) it"
assumes VB: "v < length S"
shows "modest_graph_structure_inner_succs it succs ≤ SPEC (λ succs2.
∃xs⇩2. succs2 = map ((!) B) (xs@xs⇩2) ∧ distinct xs⇩2 ∧ set xs⇩2 = s⇩0)"
proof -
have aux1: "Suc (length xs + length xs⇩2) ≤ length B"
if "j ∈ tbd" "tbd ⊆ sn_intv (T ! it)" "in_intv (T ! it) j" "distinct xs⇩2" "set xs⇩2 = s⇩0 - tbd"
for j tbd xs⇩2
proof -
have 1: "distinct (xs@xs⇩2)" using SUCC_EQ that(4) that(5) by fastforce
have 2: "set (xs@xs⇩2) ⊆ {0..<length B} - {j}"
using XS_IN_B SUCC_EQ that apply (auto simp: s⇩0_def)
by (meson B_in_bound_intvD ITB T_in_bound_intvD VB)
have "j<length B"
using B_in_bound_intvD ITB T_in_bound_intvD VB that(3) by blast
then have "length (xs@xs⇩2) < length B"
using distinct_card[OF 1] card_mono[OF _ 2]
by auto
thus ?thesis by simp
qed
show ?thesis
unfolding modest_graph_structure_inner_succs_def
apply(refine_vcg get_branches_of_transition_refine)
using S_in_bound VB ITB[THEN in_intv_ubD] apply fastforce
apply(refine_vcg get_successor_of_branch_refine FOREACH_rule[where I="(λ tbd succs2.
∃xs⇩2. succs2 = map ((!) B) (xs@xs⇩2) ∧ distinct xs⇩2 ∧ set xs⇩2 = s⇩0 - tbd)"])
subgoal using ITB VB by (auto simp: assms)
subgoal using ITB VB by (auto simp: assms)
subgoal by blast
subgoal using B_in_bound_intvD ITB T_in_bound_intvD VB sn_intv_member by blast
subgoal by (clarsimp simp: aux1)
apply clarsimp
subgoal for a b j tbd xs⇩2
apply (rule exI[where x="xs⇩2@[j]"])
by (auto simp: s⇩0_def)
subgoal by (auto simp: sn_intv_alt)
done
qed
lemma T_intv_disj': "in_intv (T!i) x ⟹ in_intv (T!j) x ⟹ i<length T ⟹ j<length T ⟹ i=j"
using T_intv_disj
by (cases i j rule: linorder_cases; fastforce)
lemma modest_graph_structure_succs_refine:
assumes VB: "v < length S"
shows "modest_graph_succ v ≤ SPEC (λ succs2. (∀x ∈ set succs2. x < length S) ∧ (set succs2) = graph_structure_edges `` {v})"
unfolding modest_graph_succ_def
apply(refine_vcg get_transitions_of_state_refine)
apply(simp add: VB)
apply(refine_vcg FOREACH_rule[where I="(λ tbd succs2. ∃xs.
succs2 = map ((!) B) xs ∧ distinct xs ∧ set xs = (⋃it∈sn_intv (S!v) - tbd. sn_intv (T!it)))"])
subgoal by simp
subgoal by simp
subgoal by auto
apply clarsimp
subgoal for i tbd xs⇩2
apply(refine_vcg modest_graph_structure_inner_succs_refine'[where xs=xs⇩2 and v=v])
subgoal by (auto simp: assms) (meson B_in_bound_intvD T_in_bound_intvD VB)
subgoal by (auto simp: assms)
subgoal
apply auto
by (metis T_in_bound_intvD VB T_intv_disj')
subgoal by (auto simp: assms)
apply clarsimp
subgoal for ys⇩2
apply (rule exI[where x="xs⇩2@ys⇩2"])
apply auto
by (metis T_in_bound_intvD T_intv_disj' VB)
done
apply clarsimp
subgoal for xs j i
by (meson B_in_bound B_in_bound_intvD T_in_bound_intvD VB)
apply clarsimp
subgoal for xs
unfolding graph_structure_edges_def
apply auto
subgoal using VB by blast
subgoal by (meson UN_I image_eqI sn_intv_member)
done
done
lemma modest_graph_succ_refine_aux:
assumes VB: "v < length S"
shows "modest_graph_succ v ≤ SPEC(λ succs. (∀x ∈ set succs. x < length S) ∧ set succs = α `` {v})"
apply(refine_vcg modest_graph_structure_succs_refine)
using VB apply (auto simp: α_def )[2]
using indep_graph_structure_edges[of v, simplified]
apply (auto simp: assms)
done
end
subsection ‹Concrete Model›
text ‹We use arrays for the lists, and bit-packed machine words for the elements›
text ‹Small array, i.e., the length is bounded by size_T. While this is true for all practical arrays,
it's not guaranteed by the Isabelle-LLVM model, which keeps integers and pointers separate.
›
abbreviation "small_array_assn A ≡ b_assn (IICF_Array.array_assn A) (λxs. length xs < max_snat len_size_T)"
abbreviation "edge_assn' N ≡ b_assn shared_nat_assn (λ x. shared_sum x < N)"
definition modest_graph_bound :: "nat ⇒ (nat × nat) list × (nat × nat) list × nat list ⇒ bool" where
"modest_graph_bound N = (λ (S,T,B).
list_all (λx. shared_sum x < length T) S ∧
list_all (λx. shared_sum x < length B) T ∧
list_all (λx. x < length S) B ∧
N = length S)"
type_synonym modest_graphi = "
shared_nat ptr
× shared_nat ptr
× size_t ptr
"
subsubsection ‹Refinement Assertions›
definition modest_graph_assn_aux :: "modest_graph ⇒ modest_graphi ⇒ assn"
where "modest_graph_assn_aux =
small_array_assn shared_nat_assn
×⇩a small_array_assn shared_nat_assn
×⇩a small_array_assn size_assn "
lemma modest_graph_assn_boundsD:
assumes "rdomp modest_graph_assn_aux (S, B, T)"
shows "length S < max_snat 64" and "length B < max_snat 64" and "length T < max_snat 64"
using assms unfolding modest_graph_assn_aux_def
apply (auto dest: )
done
subsubsection ‹Primitive Operations›
text ‹Unfortunately, we need some boilerplate to convert the implicit state fixed in the locale to an explicit tuple.›
definition "modest_get_transitions_of_state = (λ (S, T, B) v.
do {
ASSERT (v < length S);
r ← b_assn_open_block S (λS. RETURN (S ! v));
ASSERT (shared_sum r ≤ length T);
RETURN r
})"
lemma modest_get_transitions_of_state_alt: "modest_get_transitions_of_state = modest_graph_def.get_transitions_of_state"
unfolding modest_get_transitions_of_state_def modest_graph_def.get_transitions_of_state_def b_assn_open_block_def
by (auto simp: Let_def)
definition "modest_get_branches_of_transition = (λ (S, T, B) v .
do {
ASSERT (v < length T);
r ← b_assn_open_block T (λT. RETURN (T ! v));
ASSERT (shared_sum r ≤ length B);
RETURN r
})"
lemma modest_get_branches_of_transition_alt: "modest_get_branches_of_transition = modest_graph_def.get_branches_of_transition"
unfolding modest_graph_def.get_branches_of_transition_def modest_get_branches_of_transition_def b_assn_open_block_def
by (auto simp: Let_def)
definition "modest_get_successor_of_branch = (λ(S, T, B) v.
do {
ASSERT (v < length B);
r ← b_assn_open_block B (λB. RETURN (B ! v));
ASSERT (r < length S);
RETURN r
})"
lemma modest_get_successor_of_branch_alt: "modest_get_successor_of_branch = modest_graph_def.get_successor_of_branch"
unfolding modest_graph_def.get_successor_of_branch_def modest_get_successor_of_branch_def b_assn_open_block_def
by (auto simp: Let_def)
text ‹The actual refinement to LLVM is then straightforward, using Sepref›
sepref_def get_transitions_of_state_ll
is "uncurry modest_get_transitions_of_state" :: "modest_graph_assn_aux⇧k *⇩a size_assn⇧k →⇩a shared_nat_assn"
unfolding modest_get_transitions_of_state_def modest_graph_assn_aux_def
apply sepref
done
sepref_def get_branches_of_transition_ll
is "uncurry modest_get_branches_of_transition" :: "modest_graph_assn_aux⇧k *⇩a size_assn⇧k →⇩a shared_nat_assn"
unfolding modest_get_branches_of_transition_def modest_graph_assn_aux_def
apply sepref
done
sepref_def get_successor_of_branch_ll
is "uncurry modest_get_successor_of_branch" :: "modest_graph_assn_aux⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding modest_get_successor_of_branch_def modest_graph_assn_aux_def
apply sepref
done
subsubsection ‹Successor Function›
text ‹We make one more refinement step to express the foreach-loops as for-loops (nfoldli [_..<_])›
definition "modest_graph_succ_nfoldli = (λ G v.
do {
s ← modest_get_transitions_of_state G v;
nfoldli [shared_right s..<shared_sum s] (λ_. True) (λ it succs. do{
ASSERT (it < shared_sum s);
t ← modest_get_branches_of_transition G it;
nfoldli [shared_right t..<shared_sum t] (λ_. True) (λ it2 succs.
do{
ASSERT(it2 < shared_sum t);
b ← modest_get_successor_of_branch G it2;
ASSERT(Suc (length succs) ≤ length (modest_graph_def.B G));
RETURN (op_list_append succs b)
}) succs
}) []
})"
lemma modest_graph_structure_succs_nfoldli_refine_aux:
assumes INV: "modest_graph_invar N (S,T,B)"
assumes VB: "v < length S"
shows "modest_graph_succ_nfoldli (S,T,B) v ≤ ⇓Id (modest_graph_def.modest_graph_succ (S,T,B) v)"
unfolding modest_graph_succ_nfoldli_def modest_graph_def.modest_graph_succ_def modest_graph_def.modest_graph_structure_inner_succs_def
apply (refine_vcg)
apply(auto simp: modest_get_transitions_of_state_alt intro: Id_refine)[]
apply (refine_rcg LFO_refine[where A=Id and R=Id])
apply(auto simp: sn_intv_alt modest_get_branches_of_transition_alt modest_get_successor_of_branch_alt
intro: Id_list_set_relI Id_refine)
done
lemma modest_graph_succ_refine: "(modest_graph_succ_nfoldli, mop_graph_succ) ∈ modest_graph_rel N → node_rel' N → ⟨⟨node_rel' N⟩list_rel⟩nres_rel"
unfolding mop_graph_succ_def modest_graph_rel_def
apply (refine_vcg)
subgoal for gi g ui u
apply (cases gi)
apply clarsimp
apply (rule order_trans[OF modest_graph_structure_succs_nfoldli_refine_aux])
apply(auto simp: in_br_conv modest_graph_invar_def)[2]
apply simp
apply (rule order_trans[OF modest_graph_invar.modest_graph_succ_refine_aux])
apply (auto simp: in_br_conv modest_graph_invar_def)[2]
subgoal for S T B
apply (clarsimp simp: in_br_conv b_rel_list_rel intro!: nth_to_list_all dest!: nth_mem)
using modest_graph_invar.succ_in_bound[of N "(S,T,B)", simplified ]
modest_graph_invar.NS_DEF[of N "(S,T,B)", simplified ]
by(auto simp: pw_le_iff refine_pw_simps list_all_iff)
done
done
text ‹The actual refinement to LLVM is, again, straightforward›
sepref_def modest_graph_succ_ll is "uncurry modest_graph_succ_nfoldli" :: "(modest_graph_assn_aux)⇧k *⇩a (snat_assn' TYPE(node_T))⇧k →⇩a stack_assn' TYPE(size_T) (snat_assn' TYPE(node_T))"
supply [[goals_limit = 3]]
supply [sepref_bounds_dest] = modest_graph_assn_boundsD shared_nat_rel_snat_boundD
unfolding modest_graph_succ_nfoldli_def singleton_list_append
unfolding stack_fold_custom_empty[where 'l = size_T] nfoldli_upt_by_while list_all_length
apply (annot_snat_const "TYPE(size_T)")
apply sepref
done
subsection ‹Combining Concrete and Intermediate Level Refinements›
definition "modest_graph_assn N = hr_comp modest_graph_assn_aux (modest_graph_rel N)"
context
notes [fcomp_norm_unfold] = modest_graph_assn_def[symmetric] stack_node_assn_shift_bound
begin
lemmas mop_Modest_graph_succ_hnr[sepref_fr_rules] = modest_graph_succ_ll.refine[FCOMP modest_graph_succ_refine]
end
end