Theory H_Method_Implementations
section ‹Implementations of the H-Method›
theory H_Method_Implementations
imports Intermediate_Frameworks Pair_Framework "../Distinguishability" Test_Suite_Representations "../OFSM_Tables_Refined" "HOL-Library.List_Lexorder"
begin
subsection ‹Using the H-Framework›
definition h_method_via_h_framework :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ bool ⇒ bool ⇒ ('b×'c) prefix_tree" where
"h_method_via_h_framework = h_framework_dynamic (λ M V t X l . False)"
definition h_method_via_h_framework_lists :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ bool ⇒ bool ⇒ (('b×'c) × bool) list list" where
"h_method_via_h_framework_lists M m completeInputTraces useInputHeuristic = sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M (initial M) (h_method_via_h_framework M m completeInputTraces useInputHeuristic))"
lemma h_method_via_h_framework_completeness_and_finiteness :
fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
fixes M2 :: "('e,'b,'c) fsm"
assumes "observable M1"
and "observable M2"
and "minimal M1"
and "minimal M2"
and "size_r M1 ≤ m"
and "size M2 ≤ m"
and "inputs M2 = inputs M1"
and "outputs M2 = outputs M1"
shows "(L M1 = L M2) ⟷ ((L M1 ∩ set (h_method_via_h_framework M1 m completeInputTraces useInputHeuristic)) = (L M2 ∩ set (h_method_via_h_framework M1 m completeInputTraces useInputHeuristic)))"
and "finite_tree (h_method_via_h_framework M1 m completeInputTraces useInputHeuristic)"
using h_framework_dynamic_completeness_and_finiteness[OF assms]
unfolding h_method_via_h_framework_def
by blast+
lemma h_method_via_h_framework_lists_completeness :
fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
fixes M2 :: "('d,'b,'c) fsm"
assumes "observable M1"
and "observable M2"
and "minimal M1"
and "minimal M2"
and "size_r M1 ≤ m"
and "size M2 ≤ m"
and "inputs M2 = inputs M1"
and "outputs M2 = outputs M1"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (initial M2)) (h_method_via_h_framework_lists M1 m completeInputTraces useInputHeuristic)"
using h_framework_dynamic_lists_completeness[OF assms]
unfolding h_method_via_h_framework_lists_def h_framework_dynamic_lists_def h_method_via_h_framework_def
by blast
subsection ‹Using the Pair-Framework›
subsubsection ‹Selection of Distinguishing Traces›
fun add_distinguishing_sequence_if_required :: "('a ⇒ 'a ⇒ ('b × 'c) list) ⇒ ('a,'b::linorder,'c::linorder) fsm ⇒ (('b×'c) list × 'a) × (('b×'c) list × 'a) ⇒ ('b×'c) prefix_tree ⇒ ('b×'c) prefix_tree" where
"add_distinguishing_sequence_if_required dist_fun M ((α,q1), (β,q2)) t = (if intersection_is_distinguishing M (after t α) q1 (after t β) q2
then empty
else insert empty (dist_fun q1 q2))"
lemma add_distinguishing_sequence_if_required_distinguishes :
assumes "observable M"
and "minimal M"
and "α ∈ L M"
and "β ∈ L M"
and "after_initial M α ≠ after_initial M β"
and "⋀ q1 q2 . q1 ∈ states M ⟹ q2 ∈ states M ⟹ q1 ≠ q2 ⟹ distinguishes M q1 q2 (dist_fun q1 q2)"
shows "∃ io ∈ set ((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β)) . distinguishes M (after_initial M α) (after_initial M β) io"
proof (cases "intersection_is_distinguishing M (after t α) (after_initial M α) (after t β) (after_initial M β)")
case True
then have "(add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t = empty"
by auto
then have "set ((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β)) = (set (after t α) ∩ set (after t β))"
using Prefix_Tree.set_empty
by (metis Int_insert_right inf.absorb_iff2 inf_bot_right insert_is_Un set_Nil sup_absorb2)
moreover have "∃ io ∈ (set (after t α) ∩ set (after t β)) . distinguishes M (after_initial M α) (after_initial M β) io"
using True unfolding intersection_is_distinguishing_correctness[OF assms(1) after_is_state[OF assms(1,3)] after_is_state[OF assms(1,4)]]
by auto
ultimately show ?thesis
by blast
next
case False
then have "set ((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t) = set (insert empty (dist_fun (after_initial M α) (after_initial M β)))"
by auto
then have "dist_fun (after_initial M α) (after_initial M β) ∈ set ((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β))"
unfolding insert_set by auto
then show ?thesis
using assms(6)[OF after_is_state[OF assms(1,3)] after_is_state[OF assms(1,4)] assms(5)] by blast
qed
lemma add_distinguishing_sequence_if_required_finite :
"finite_tree ((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t)"
proof (cases "intersection_is_distinguishing M (after t α) (after_initial M α) (after t β) (after_initial M β)")
case True
then have "((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t) = empty"
by auto
then show ?thesis
using empty_finite_tree by simp
next
case False
then have "((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t) = (insert empty (dist_fun (after_initial M α) (after_initial M β)))"
by auto
then show ?thesis
using insert_finite_tree[OF empty_finite_tree] by metis
qed
fun add_distinguishing_sequence_and_complete_if_required :: "('a ⇒ 'a ⇒ ('b × 'c) list) ⇒ bool ⇒ ('a::linorder,'b::linorder,'c::linorder) fsm ⇒ (('b×'c) list × 'a) × (('b×'c) list × 'a) ⇒ ('b×'c) prefix_tree ⇒ ('b×'c) prefix_tree" where
"add_distinguishing_sequence_and_complete_if_required distFun completeInputTraces M ((α,q1), (β,q2)) t =
(if intersection_is_distinguishing M (after t α) q1 (after t β) q2
then empty
else let w = distFun q1 q2;
T = insert empty w
in if completeInputTraces
then let T1 = from_list (language_for_input M q1 (map fst w));
T2 = from_list (language_for_input M q2 (map fst w))
in Prefix_Tree.combine T (Prefix_Tree.combine T1 T2)
else T)"
lemma add_distinguishing_sequence_and_complete_if_required_distinguishes :
assumes "observable M"
and "minimal M"
and "α ∈ L M"
and "β ∈ L M"
and "after_initial M α ≠ after_initial M β"
and "⋀ q1 q2 . q1 ∈ states M ⟹ q2 ∈ states M ⟹ q1 ≠ q2 ⟹ distinguishes M q1 q2 (dist_fun q1 q2)"
shows "∃ io ∈ set ((add_distinguishing_sequence_and_complete_if_required dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β)) . distinguishes M (after_initial M α) (after_initial M β) io"
proof (cases "intersection_is_distinguishing M (after t α) (after_initial M α) (after t β) (after_initial M β)")
case True
then have "(add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t = empty"
by auto
then have "set ((add_distinguishing_sequence_if_required dist_fun M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β)) = (set (after t α) ∩ set (after t β))"
using Prefix_Tree.set_empty
by (metis Int_insert_right inf.absorb_iff2 inf_bot_right insert_is_Un set_Nil sup_absorb2)
moreover have "∃ io ∈ (set (after t α) ∩ set (after t β)) . distinguishes M (after_initial M α) (after_initial M β) io"
using True unfolding intersection_is_distinguishing_correctness[OF assms(1) after_is_state[OF assms(1,3)] after_is_state[OF assms(1,4)]]
by auto
ultimately show ?thesis
by blast
next
case False
then have "set (insert empty (dist_fun (after_initial M α) (after_initial M β))) ⊆ set ((add_distinguishing_sequence_and_complete_if_required dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t)"
using combine_set[of "insert empty (dist_fun (after_initial M α) (after_initial M β))"]
unfolding add_distinguishing_sequence_and_complete_if_required.simps Let_def
by (cases c; fastforce)
moreover have "dist_fun (after_initial M α) (after_initial M β) ∈ set (insert empty (dist_fun (after_initial M α) (after_initial M β)))"
unfolding insert_set by auto
ultimately have "dist_fun (after_initial M α) (after_initial M β) ∈ set ((add_distinguishing_sequence_and_complete_if_required dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β))"
by blast
then show ?thesis
using assms(6)[OF after_is_state[OF assms(1,3)] after_is_state[OF assms(1,4)] assms(5)]
by (meson distinguishes_def)
qed
lemma add_distinguishing_sequence_and_complete_if_required_finite :
"finite_tree ((add_distinguishing_sequence_and_complete_if_required dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t)"
proof (cases "intersection_is_distinguishing M (after t α) (after_initial M α) (after t β) (after_initial M β)")
case True
then have "((add_distinguishing_sequence_and_complete_if_required dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t) = empty"
by auto
then show ?thesis
using empty_finite_tree by simp
next
case False
define w where w: "w = dist_fun (after_initial M α) (after_initial M β)"
define T where T: "T = insert empty w"
define T1 where T1: "T1 = from_list (language_for_input M (after_initial M α) (map fst w))"
define T2 where T2: "T2 = from_list (language_for_input M (after_initial M β) (map fst w))"
have "finite_tree T"
using insert_finite_tree[OF empty_finite_tree]
unfolding T by auto
moreover have "finite_tree (Prefix_Tree.combine T (Prefix_Tree.combine T1 T2))"
using combine_finite_tree[OF ‹finite_tree T› combine_finite_tree[OF from_list_finite_tree from_list_finite_tree]]
unfolding T1 T2
by auto
ultimately show ?thesis
using False
unfolding add_distinguishing_sequence_and_complete_if_required.simps w T T1 T2 Let_def
by presburger
qed
function find_cheapest_distinguishing_trace :: "('a,'b::linorder,'c::linorder) fsm ⇒ ('a ⇒ 'a ⇒ ('b × 'c) list) ⇒ ('b×'c) list ⇒ ('b×'c) prefix_tree ⇒ 'a ⇒ ('b×'c) prefix_tree ⇒ 'a ⇒ (('b×'c) list × nat × nat)" where
"find_cheapest_distinguishing_trace M distFun ios (PT m1) q1 (PT m2) q2 =
(let
f = (λ (ω,l,w) (x,y) . if (x,y) ∉ list.set ios then (ω,l,w) else
(let
w1L = if (PT m1) = empty then 0 else 1;
w1C = if (x,y) ∈ dom m1 then 0 else 1;
w1 = min w1L w1C;
w2L = if (PT m2) = empty then 0 else 1;
w2C = if (x,y) ∈ dom m2 then 0 else 1;
w2 = min w2L w2C;
w' = w1 + w2
in
case h_obs M q1 x y of
None ⇒ (case h_obs M q2 x y of
None ⇒ (ω,l,w) |
Some _ ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w)) |
Some q1' ⇒ (case h_obs M q2 x y of
None ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w) |
Some q2' ⇒ (if q1' = q2'
then (ω,l,w)
else (case m1 (x,y) of
None ⇒ (case m2 (x,y) of
None ⇒ let ω' = distFun q1' q2';
l' = 2 + 2 * length ω'
in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w) |
Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2'
in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w)) |
Some t1' ⇒ (case m2 (x,y) of
None ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2'
in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w) |
Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2'
in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w)))))))
in
foldl f (distFun q1 q2, 0, 3) ios)"
by pat_completeness auto
termination
proof -
let ?f = "(λ(M, dF, ios, t1, q1, t2, q2). height_over ios t1 + height_over ios t2)"
have "⋀(M::('a,'b::linorder,'c::linorder) fsm)
(distFun :: ('a ⇒ 'a ⇒ ('b × 'c) list))
(ios :: ('b×'c) list)
m1 (q1::'a) m2 (q2::'a) x y t2' q1' q2'.
¬ (x, y) ∉ list.set ios ⟹
m1 (x, y) = None ⟹
m2 (x, y) = Some t2' ⟹
((M, distFun, ios, Prefix_Tree.empty, q1', t2', q2'), M, distFun, ios,
PT m1, q1, PT m2, q2)
∈ measure (λ(M, dF, ios, t1, q1, t2, q2). height_over ios t1 + height_over ios t2)"
proof -
fix M::"('a,'b::linorder,'c::linorder) fsm"
fix distFun :: "('a ⇒ 'a ⇒ ('b × 'c) list)"
fix ios :: "('b×'c) list"
fix m1 m2 :: "('b×'c) ⇀ ('b×'c) prefix_tree"
fix t2'
fix q1 q2 q1' q2' :: 'a
fix x
fix y
assume "m1 (x, y) = None"
assume "m2 (x, y) = Some t2'"
assume "¬ (x, y) ∉ list.set ios"
define pre where "pre = (M, distFun, ios, PT m1, q1, PT m2, q2)"
define post where "post = (M, distFun, ios, Prefix_Tree.empty::('b×'c) prefix_tree, q1', t2', q2')"
have "height_over ios empty ≤ height_over ios (PT m1)"
unfolding height_over.simps height_over_empty by auto
then have "?f post < ?f pre"
unfolding pre_def post_def case_prod_conv
by (meson ‹¬ (x, y) ∉ list.set ios› ‹m2 (x, y) = Some t2'› add_le_less_mono height_over_subtree_less)
then show "((M, distFun, ios, Prefix_Tree.empty, q1', t2', q2'), M, distFun, ios,
PT m1, q1, PT m2, q2)
∈ measure (λ(M, dF, ios, t1, q1, t2, q2). height_over ios t1 + height_over ios t2)"
unfolding pre_def[symmetric] post_def[symmetric]
by simp
qed
moreover have "⋀(M::('a,'b::linorder,'c::linorder) fsm)
(distFun :: ('a ⇒ 'a ⇒ ('b × 'c) list))
(ios :: ('b×'c) list)
m1 (q1::'a) m2 (q2::'a) x y t1' q1' q2'.
¬ (x, y) ∉ list.set ios ⟹
m1 (x, y) = Some t1' ⟹
m2 (x, y) = None ⟹
((M, distFun, ios, t1', q1', empty, q2'), M, distFun, ios,
PT m1, q1, PT m2, q2)
∈ measure (λ(M, dF, ios, t1, q1, t2, q2). height_over ios t1 + height_over ios t2)"
proof -
fix M::"('a,'b::linorder,'c::linorder) fsm"
fix distFun :: "('a ⇒ 'a ⇒ ('b × 'c) list)"
fix ios :: "('b×'c) list"
fix m1 m2 :: "('b×'c) ⇀ ('b×'c) prefix_tree"
fix t1'
fix q1 q2 q1' q2' :: 'a
fix x :: 'b
fix y :: 'c
assume "m1 (x, y) = Some t1'"
assume "m2 (x, y) = None"
assume "¬ (x, y) ∉ list.set ios"
define pre where "pre = (M, distFun, ios, PT m1, q1, PT m2, q2)"
define post where "post = (M, distFun, ios, t1', q1', Prefix_Tree.empty::('b×'c) prefix_tree, q2')"
have "height_over ios empty ≤ height_over ios (PT m2)"
unfolding height_over.simps height_over_empty by auto
then have "?f post < ?f pre"
unfolding pre_def post_def case_prod_conv
by (meson ‹¬ (x, y) ∉ list.set ios› ‹m1 (x, y) = Some t1'› add_mono_thms_linordered_field(3) height_over_subtree_less)
then show "((M, distFun, ios, t1', q1', Prefix_Tree.empty, q2'), M, distFun, ios,
PT m1, q1, PT m2, q2)
∈ measure (λ(M, dF, ios, t1, q1, t2, q2). height_over ios t1 + height_over ios t2)"
unfolding pre_def[symmetric] post_def[symmetric]
by simp
qed
moreover have "⋀(M::('a,'b::linorder,'c::linorder) fsm)
(distFun :: ('a ⇒ 'a ⇒ ('b × 'c) list))
(ios :: ('b×'c) list)
m1 (q1::'a) m2 (q2::'a) x y t1' t2' q1' q2'.
¬ (x, y) ∉ list.set ios ⟹
m1 (x, y) = Some t1' ⟹
m2 (x, y) = Some t2' ⟹
((M, distFun, ios, t1', q1', t2', q2'), M, distFun, ios,
PT m1, q1, PT m2, q2)
∈ measure (λ(M, dF, ios, t1, q1, t2, q2). height_over ios t1 + height_over ios t2)"
proof -
fix M::"('a,'b::linorder,'c::linorder) fsm"
fix distFun :: "('a ⇒ 'a ⇒ ('b × 'c) list)"
fix ios :: "('b×'c) list"
fix m1 m2 :: "('b×'c) ⇀ ('b×'c) prefix_tree"
fix t1' t2' :: "('b×'c) prefix_tree"
fix q1 q2 q1' q2' :: 'a
fix x :: 'b
fix y :: 'c
define pre where "pre = (M, distFun, ios, PT m1, q1, PT m2, q2)"
define post where "post = (M, distFun, ios, t1', q1', t2', q2')"
assume "m1 (x, y) = Some t1'"
moreover assume "m2 (x, y) = Some t2'"
moreover assume "¬ (x, y) ∉ list.set ios"
ultimately have "?f post < ?f pre"
unfolding pre_def post_def case_prod_conv
by (meson add_less_mono height_over_subtree_less)
then show "((M, distFun, ios, t1', q1',t2', q2'), M, distFun, ios,
PT m1, q1, PT m2, q2)
∈ measure (λ(M, dF, ios, t1, q1, t2, q2). height_over ios t1 + height_over ios t2)"
unfolding pre_def[symmetric] post_def[symmetric]
by simp
qed
ultimately show ?thesis
by (relation "measure (λ (M,dF,ios,t1,q1,t2,q2) . height_over ios t1 + height_over ios t2)"; simp)
qed
lemma find_cheapest_distinguishing_trace_alt_def :
"find_cheapest_distinguishing_trace M distFun ios (PT m1) q1 (PT m2) q2 =
(let
f = (λ (ω,l,w) (x,y).
(let
w1L = if (PT m1) = empty then 0 else 1;
w1C = if (x,y) ∈ dom m1 then 0 else 1;
w1 = min w1L w1C;
w2L = if (PT m2) = empty then 0 else 1;
w2C = if (x,y) ∈ dom m2 then 0 else 1;
w2 = min w2L w2C;
w' = w1 + w2
in
case h_obs M q1 x y of
None ⇒ (case h_obs M q2 x y of
None ⇒ (ω,l,w) |
Some _ ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w)) |
Some q1' ⇒ (case h_obs M q2 x y of
None ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w) |
Some q2' ⇒ (if q1' = q2'
then (ω,l,w)
else (case m1 (x,y) of
None ⇒ (case m2 (x,y) of
None ⇒ let ω' = distFun q1' q2';
l' = 2 + 2 * length ω'
in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w) |
Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2'
in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w)) |
Some t1' ⇒ (case m2 (x,y) of
None ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2'
in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w) |
Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2'
in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w)))))))
in
foldl f (distFun q1 q2, 0, 3) ios)"
(is "find_cheapest_distinguishing_trace M distFun ios (PT m1) q1 (PT m2) q2 = ?find_cheapest_distinguishing_trace")
proof -
define f' where "f' = (λ (ω,l,w) (x,y) .
(let
w1L = if (PT m1) = empty then 0 else 1;
w1C = if (x,y) ∈ dom m1 then 0 else 1;
w1 = min w1L w1C;
w2L = if (PT m2) = empty then 0 else 1;
w2C = if (x,y) ∈ dom m2 then 0 else 1;
w2 = min w2L w2C;
w' = w1 + w2
in
case h_obs M q1 x y of
None ⇒ (case h_obs M q2 x y of
None ⇒ (ω,l,w) |
Some _ ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w)) |
Some q1' ⇒ (case h_obs M q2 x y of
None ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w) |
Some q2' ⇒ (if q1' = q2'
then (ω,l,w)
else (case m1 (x,y) of
None ⇒ (case m2 (x,y) of
None ⇒ let ω' = distFun q1' q2';
l' = 2 + 2 * length ω'
in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w) |
Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2'
in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w)) |
Some t1' ⇒ (case m2 (x,y) of
None ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2'
in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w) |
Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2'
in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w)))))))"
define f where "f = (λ (ω,l,w) (x,y) . if (x,y) ∉ list.set ios then (ω,l,w) else
(let
w1L = if (PT m1) = empty then 0 else 1;
w1C = if (x,y) ∈ dom m1 then 0 else 1;
w1 = min w1L w1C;
w2L = if (PT m2) = empty then 0 else 1;
w2C = if (x,y) ∈ dom m2 then 0 else 1;
w2 = min w2L w2C;
w' = w1 + w2
in
case h_obs M q1 x y of
None ⇒ (case h_obs M q2 x y of
None ⇒ (ω,l,w) |
Some _ ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w)) |
Some q1' ⇒ (case h_obs M q2 x y of
None ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w) |
Some q2' ⇒ (if q1' = q2'
then (ω,l,w)
else (case m1 (x,y) of
None ⇒ (case m2 (x,y) of
None ⇒ let ω' = distFun q1' q2';
l' = 2 + 2 * length ω'
in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w) |
Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2'
in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w)) |
Some t1' ⇒ (case m2 (x,y) of
None ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2'
in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w) |
Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2'
in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w)))))))"
then have "f = (λ y x . if x ∉ list.set ios then y else f' y x)"
unfolding f'_def by fast
moreover have "find_cheapest_distinguishing_trace M distFun ios (PT m1) q1 (PT m2) q2 = foldl f (distFun q1 q2, 0, 3) ios"
unfolding find_cheapest_distinguishing_trace.simps f_def[symmetric] by auto
ultimately have "find_cheapest_distinguishing_trace M distFun ios (PT m1) q1 (PT m2) q2 = foldl (λ y x . if x ∉ list.set ios then y else f' y x) (distFun q1 q2, 0, 3) ios"
by auto
then show ?thesis
unfolding f'_def[symmetric]
using foldl_elem_check[of ios "list.set ios"]
by auto
qed
lemma find_cheapest_distinguishing_trace_code[code] :
"find_cheapest_distinguishing_trace M distFun ios (MPT m1) q1 (MPT m2) q2 =
(let
f = (λ (ω,l,w) (x,y) .
(let
w1L = if is_leaf (MPT m1) then 0 else 1;
w1C = if (x,y) ∈ Mapping.keys m1 then 0 else 1;
w1 = min w1L w1C;
w2L = if is_leaf (MPT m2) then 0 else 1;
w2C = if(x,y) ∈ Mapping.keys m2 then 0 else 1;
w2 = min w2L w2C;
w' = w1 + w2
in
case h_obs M q1 x y of
None ⇒ (case h_obs M q2 x y of
None ⇒ (ω,l,w) |
Some _ ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w)) |
Some q1' ⇒ (case h_obs M q2 x y of
None ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w) |
Some q2' ⇒ (if q1' = q2'
then (ω,l,w)
else (case Mapping.lookup m1 (x,y) of
None ⇒ (case Mapping.lookup m2 (x,y) of
None ⇒ let ω' = distFun q1' q2';
l' = 2 + 2 * length ω'
in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w) |
Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2'
in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w)) |
Some t1' ⇒ (case Mapping.lookup m2 (x,y) of
None ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2'
in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w) |
Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2'
in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w)))))))
in
foldl f (distFun q1 q2, 0, 3) ios)"
unfolding find_cheapest_distinguishing_trace_alt_def MPT_def
by (simp add: keys_dom_lookup)
lemma find_cheapest_distinguishing_trace_is_distinguishing_trace :
assumes "observable M"
and "minimal M"
and "q1 ∈ states M"
and "q2 ∈ states M"
and "q1 ≠ q2"
and "⋀ q1 q2 . q1 ∈ states M ⟹ q2 ∈ states M ⟹ q1 ≠ q2 ⟹ distinguishes M q1 q2 (distFun q1 q2)"
shows "distinguishes M q1 q2 (fst (find_cheapest_distinguishing_trace M distFun ios t1 q1 t2 q2))"
using assms(3,4,5)
proof (induction "height_over ios t1 + height_over ios t2" arbitrary: t1 q1 t2 q2 rule: less_induct)
case less
obtain m1 where "t1 = PT m1"
using prefix_tree.exhaust by blast
obtain m2 where "t2 = PT m2"
using prefix_tree.exhaust by blast
define f where "f = (λ (ω,l,w) (x,y) .
(let
w1L = if (PT m1) = empty then 0 else 1;
w1C = if (x,y) ∈ dom m1 then 0 else 1;
w1 = min w1L w1C;
w2L = if (PT m2) = empty then 0 else 1;
w2C = if (x,y) ∈ dom m2 then 0 else 1;
w2 = min w2L w2C;
w' = w1 + w2
in
case h_obs M q1 x y of
None ⇒ (case h_obs M q2 x y of
None ⇒ (ω,l,w) |
Some _ ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w)) |
Some q1' ⇒ (case h_obs M q2 x y of
None ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w) |
Some q2' ⇒ (if q1' = q2'
then (ω,l,w)
else (case m1 (x,y) of
None ⇒ (case m2 (x,y) of
None ⇒ let ω' = distFun q1' q2';
l' = 2 + 2 * length ω'
in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w) |
Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2'
in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w)) |
Some t1' ⇒ (case m2 (x,y) of
None ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2'
in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w) |
Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2'
in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w)))))))"
then have "find_cheapest_distinguishing_trace M distFun ios t1 q1 t2 q2 = foldl f (distFun q1 q2, 0, 3) ios"
unfolding ‹t1 = PT m1› ‹t2 = PT m2›
unfolding find_cheapest_distinguishing_trace_alt_def Let_def
by fast
define ios' where "ios'=ios"
have "list.set ios' ⊆ list.set ios ⟹ distinguishes M q1 q2 (fst (foldl f (distFun q1 q2, 0, 3) ios'))"
proof (induction ios' rule: rev_induct)
case Nil
then show ?case using assms(6)[OF less.prems] by auto
next
case (snoc xy ios')
obtain x y where "xy = (x,y)"
using prod.exhaust by metis
moreover obtain ω l w where "(foldl f (distFun q1 q2, 0, 3) ios') = (ω,l,w)"
using prod.exhaust by metis
ultimately have "foldl f (distFun q1 q2, 0, 3) (ios'@[xy]) = f (ω,l,w) (x,y)"
by auto
have "distinguishes M q1 q2 ω"
using ‹(foldl f (distFun q1 q2, 0, 3) ios') = (ω,l,w)› snoc by auto
have "(x,y) ∈ list.set ios"
using snoc.prems unfolding ‹xy = (x,y)› by auto
define w1L where "w1L = (if (PT m1) = empty then 0 else 1::nat)"
define w1C where "w1C = (if (x,y) ∈ dom m1 then 0 else 1::nat)"
define w1 where "w1 = min w1L w1C"
define w2L where "w2L = (if (PT m2) = empty then 0 else 1::nat)"
define w2C where "w2C = (if (x,y) ∈ dom m2 then 0 else 1::nat)"
define w2 where "w2 = min w2L w2C"
define w' where "w' = w1 + w2"
have *:"f (ω,l,w) (x,y) = (case h_obs M q1 x y of
None ⇒ (case h_obs M q2 x y of
None ⇒ (ω,l,w) |
Some _ ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w)) |
Some q1' ⇒ (case h_obs M q2 x y of
None ⇒ if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w) |
Some q2' ⇒ (if q1' = q2'
then (ω,l,w)
else (case m1 (x,y) of
None ⇒ (case m2 (x,y) of
None ⇒ let ω' = distFun q1' q2';
l' = 2 + 2 * length ω'
in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w) |
Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2'
in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w)) |
Some t1' ⇒ (case m2 (x,y) of
None ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2'
in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w) |
Some t2' ⇒ let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2'
in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w))))))"
unfolding w1_def w2_def w'_def w1L_def w1C_def w2L_def w2C_def
unfolding f_def case_prod_conv Let_def
by fast
have "distinguishes M q1 q2 (fst (f (ω,l,w) (x,y)))"
proof (cases "h_obs M q1 x y")
case None
then show ?thesis proof (cases "h_obs M q2 x y")
case None
have "f (ω,l,w) (x,y) = (ω,l,w)"
unfolding *
unfolding ‹h_obs M q1 x y = None› None by auto
then show ?thesis
using ‹distinguishes M q1 q2 ω› by auto
next
case (Some a)
have "f (ω,l,w) (x,y) = (if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w))"
unfolding * None Some by auto
moreover have "distinguishes M q1 q2 [(x,y)]"
using distinguishes_sym[OF h_obs_distinguishes[OF assms(1) Some None]] .
ultimately show ?thesis
using ‹distinguishes M q1 q2 ω› by auto
qed
next
case (Some q1')
then have "q1' ∈ states M"
by (meson h_obs_state)
show ?thesis proof (cases "h_obs M q2 x y")
case None
have "f (ω,l,w) (x,y) = (if w' = 0 ∨ w' ≤ w then ([(x,y)],w1C+w2C,w') else (ω,l,w))"
unfolding * None Some by auto
moreover have "distinguishes M q1 q2 [(x,y)]"
using h_obs_distinguishes[OF assms(1) Some None] .
ultimately show ?thesis
using ‹distinguishes M q1 q2 ω› by auto
next
case (Some q2')
then have "q2' ∈ states M"
by (meson h_obs_state)
show ?thesis proof (cases "q1' = q2'")
case True
have "f (ω,l,w) (x,y) = (ω,l,w)"
unfolding *
unfolding ‹h_obs M q1 x y = Some q1'› Some True by auto
then show ?thesis
using ‹distinguishes M q1 q2 ω› by auto
next
case False
have dist': "⋀ ω . distinguishes M q1' q2' ω ⟹ distinguishes M q1 q2 ((x,y)#ω)"
using distinguishes_after_prepend[OF assms(1), of q1 x y q2]
using ‹h_obs M q1 x y = Some q1'› ‹h_obs M q2 x y = Some q2'›
unfolding after_h_obs[OF assms(1) ‹h_obs M q1 x y = Some q1'›]
unfolding after_h_obs[OF assms(1) ‹h_obs M q2 x y = Some q2'›]
by auto
show ?thesis proof (cases "m1 (x,y)")
case None
show ?thesis proof (cases "m2 (x,y)")
case None
have **: "f (ω,l,w) (x,y) = (let ω' = distFun q1' q2'; l' = 2 + 2 * length ω'
in if (w' < w) ∨ (w' = w ∧ l' < l) then ((x,y)#ω',l',w') else (ω,l,w))"
unfolding *
unfolding ‹h_obs M q1 x y = Some q1'› ‹h_obs M q2 x y = Some q2'› ‹m1 (x, y) = None› ‹m2 (x, y) = None›
using False
by auto
have "distinguishes M q1' q2' (distFun q1' q2')"
using ‹q1' ∈ states M› ‹q2' ∈ states M› assms(6) False by blast
then have "distinguishes M q1 q2 ((x,y)#(distFun q1' q2'))"
using dist' by auto
then show ?thesis
using ‹distinguishes M q1 q2 ω›
unfolding ** Let_def by auto
next
case (Some t2')
have **: "f (ω,l,w) (x,y) = (let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2'
in if (w'' + w1 < w) ∨ (w'' + w1 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w1) else (ω,l,w))"
unfolding *
unfolding ‹h_obs M q1 x y = Some q1'› ‹h_obs M q2 x y = Some q2'› ‹m1 (x, y) = None› ‹m2 (x, y) = Some t2'›
using False
by auto
obtain ω'' l'' w'' where ***:"find_cheapest_distinguishing_trace M distFun ios Prefix_Tree.empty q1' t2' q2' = (ω'', l'', w'')"
using prod.exhaust by metis
have "distinguishes M q1' q2' (fst (find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2'))"
proof -
have "height_over ios empty + height_over ios t2' < height_over ios t1 + height_over ios t2"
using height_over_subtree_less[of m2 "(x,y)", OF ‹m2 (x,y) = Some t2'› ‹(x,y) ∈ list.set ios› ]
unfolding height_over_empty ‹t2 = PT m2›[symmetric]
by (simp add: ‹t1 = PT m1›)
then show ?thesis
using less.hyps[OF _ ‹q1' ∈ states M› ‹q2' ∈ states M› False]
by blast
qed
then have "distinguishes M q1 q2 ((x,y)#(fst (find_cheapest_distinguishing_trace M distFun ios empty q1' t2' q2')))"
using dist' by blast
then show ?thesis
using ‹distinguishes M q1 q2 ω›
unfolding ** *** Let_def fst_conv case_prod_conv by auto
qed
next
case (Some t1')
show ?thesis proof (cases "m2 (x,y)")
case None
have **: "f (ω,l,w) (x,y) = (let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2'
in if (w'' + w2 < w) ∨ (w'' + w2 = w ∧ l''+1 < l) then ((x,y)#ω'',l''+1,w''+w2) else (ω,l,w))"
unfolding *
unfolding ‹h_obs M q1 x y = Some q1'› ‹h_obs M q2 x y = Some q2'› ‹m1 (x, y) = Some t1'› ‹m2 (x, y) = None›
using False
by auto
obtain ω'' l'' w'' where ***:"find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2' = (ω'', l'', w'')"
using prod.exhaust by metis
have "distinguishes M q1' q2' (fst (find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2'))"
proof -
have "height_over ios t1' + height_over ios empty < height_over ios t1 + height_over ios t2"
using height_over_subtree_less[of m1 "(x,y)", OF ‹m1 (x,y) = Some t1'› ‹(x,y) ∈ list.set ios› ]
unfolding height_over_empty ‹t1 = PT m1›[symmetric]
by (simp add: ‹t2 = PT m2›)
then show ?thesis
using less.hyps[OF _ ‹q1' ∈ states M› ‹q2' ∈ states M› False]
by blast
qed
then have "distinguishes M q1 q2 ((x,y)#(fst (find_cheapest_distinguishing_trace M distFun ios t1' q1' empty q2')))"
using dist' by blast
then show ?thesis
using ‹distinguishes M q1 q2 ω›
unfolding ** *** Let_def fst_conv case_prod_conv by auto
next
case (Some t2')
have **: "f (ω,l,w) (x,y) = (let (ω'',l'',w'') = find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2'
in if (w'' < w) ∨ (w'' = w ∧ l'' < l) then ((x,y)#ω'',l'',w'') else (ω,l,w))"
unfolding *
unfolding ‹h_obs M q1 x y = Some q1'› ‹h_obs M q2 x y = Some q2'› ‹m1 (x, y) = Some t1'› ‹m2 (x, y) = Some t2'›
using False
by auto
obtain ω'' l'' w'' where ***:"find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2' = (ω'', l'', w'')"
using prod.exhaust by metis
have "distinguishes M q1' q2' (fst (find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2'))"
proof -
have "height_over ios t1' + height_over ios t2' < height_over ios t1 + height_over ios t2"
using height_over_subtree_less[of m1 "(x,y)", OF ‹m1 (x,y) = Some t1'› ‹(x,y) ∈ list.set ios› ]
using height_over_subtree_less[of m2 "(x,y)", OF ‹m2 (x,y) = Some t2'› ‹(x,y) ∈ list.set ios› ]
unfolding ‹t1 = PT m1›[symmetric] ‹t2 = PT m2›[symmetric]
by auto
then show ?thesis
using less.hyps[OF _ ‹q1' ∈ states M› ‹q2' ∈ states M› False]
by blast
qed
then have "distinguishes M q1 q2 ((x,y)#(fst (find_cheapest_distinguishing_trace M distFun ios t1' q1' t2' q2')))"
using dist' by blast
then show ?thesis
using ‹distinguishes M q1 q2 ω›
unfolding ** *** Let_def fst_conv case_prod_conv by auto
qed
qed
qed
qed
qed
then show ?case
unfolding ‹foldl f (distFun q1 q2, 0, 3) (ios'@[xy]) = f (ω,l,w) (x,y)› .
qed
then show ?case
unfolding ‹find_cheapest_distinguishing_trace M distFun ios t1 q1 t2 q2 = foldl f (distFun q1 q2, 0, 3) ios›
‹ios' = ios›
by blast
qed
fun add_cheapest_distinguishing_trace :: "('a ⇒ 'a ⇒ ('b × 'c) list) ⇒ bool ⇒ ('a::linorder,'b::linorder,'c::linorder) fsm ⇒ (('b×'c) list × 'a) × (('b×'c) list × 'a) ⇒ ('b×'c) prefix_tree ⇒ ('b×'c) prefix_tree" where
"add_cheapest_distinguishing_trace distFun completeInputTraces M ((α,q1), (β,q2)) t =
(let w = (fst (find_cheapest_distinguishing_trace M distFun (List.product (inputs_as_list M) (outputs_as_list M)) (after t α) q1 (after t β) q2));
T = insert empty w
in if completeInputTraces
then let T1 = complete_inputs_to_tree M q1 (outputs_as_list M) (map fst w);
T2 = complete_inputs_to_tree M q2 (outputs_as_list M) (map fst w)
in Prefix_Tree.combine T (Prefix_Tree.combine T1 T2)
else T)"
lemma add_cheapest_distinguishing_trace_distinguishes :
assumes "observable M"
and "minimal M"
and "α ∈ L M"
and "β ∈ L M"
and "after_initial M α ≠ after_initial M β"
and "⋀ q1 q2 . q1 ∈ states M ⟹ q2 ∈ states M ⟹ q1 ≠ q2 ⟹ distinguishes M q1 q2 (dist_fun q1 q2)"
shows "∃ io ∈ set ((add_cheapest_distinguishing_trace dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β)) . distinguishes M (after_initial M α) (after_initial M β) io"
proof -
define w where "w = (fst (find_cheapest_distinguishing_trace M dist_fun (List.product (inputs_as_list M) (outputs_as_list M)) (after t α) (after_initial M α) (after t β) (after_initial M β)))"
have "set (insert empty w) ⊆ set ((add_cheapest_distinguishing_trace dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t)"
using combine_set[of "insert empty w"] w_def
unfolding add_cheapest_distinguishing_trace.simps Let_def
by (cases c; fastforce)
moreover have "w ∈ set (insert empty w)"
unfolding insert_set by auto
ultimately have "w ∈ set ((add_cheapest_distinguishing_trace dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β))"
by blast
moreover have "distinguishes M (after_initial M α) (after_initial M β) w"
using find_cheapest_distinguishing_trace_is_distinguishing_trace[OF assms(1,2) after_is_state[OF assms(1,3)] after_is_state[OF assms(1,4)] assms(5,6)]
unfolding w_def
by blast
ultimately show ?thesis
by blast
qed
lemma add_cheapest_distinguishing_trace_finite :
"finite_tree ((add_cheapest_distinguishing_trace dist_fun c M) ((α,after_initial M α),(β,after_initial M β)) t)"
proof -
define w where w: "w = (fst (find_cheapest_distinguishing_trace M dist_fun (List.product (inputs_as_list M) (outputs_as_list M)) (after t α) (after_initial M α) (after t β) (after_initial M β)))"
define T where T: "T = insert empty w"
define T1 where T1: "T1 = complete_inputs_to_tree M (after_initial M α) (outputs_as_list M) (map fst w)"
define T2 where T2: "T2 = complete_inputs_to_tree M (after_initial M β) (outputs_as_list M) (map fst w)"
have "finite_tree T"
using insert_finite_tree[OF empty_finite_tree]
unfolding T by auto
moreover have "finite_tree (Prefix_Tree.combine T (Prefix_Tree.combine T1 T2))"
using combine_finite_tree[OF ‹finite_tree T› combine_finite_tree[OF complete_inputs_to_tree_finite_tree complete_inputs_to_tree_finite_tree]]
unfolding T1 T2
by auto
ultimately show ?thesis
unfolding add_cheapest_distinguishing_trace.simps w T T1 T2 Let_def
by presburger
qed
subsubsection ‹Implementation›
definition h_method_via_pair_framework :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ ('b×'c) prefix_tree" where
"h_method_via_pair_framework M m = pair_framework_h_components M m (add_distinguishing_sequence_if_required (get_distinguishing_sequence_from_ofsm_tables M))"
lemma h_method_via_pair_framework_completeness_and_finiteness :
assumes "observable M"
and "observable I"
and "minimal M"
and "size I ≤ m"
and "m ≥ size_r M"
and "inputs I = inputs M"
and "outputs I = outputs M"
shows "(L M = L I) ⟷ (L M ∩ set (h_method_via_pair_framework M m) = L I ∩ set (h_method_via_pair_framework M m))"
and "finite_tree (h_method_via_pair_framework M m)"
using pair_framework_h_components_completeness_and_finiteness[OF assms(1,2,3,5,4,6,7), where get_separating_traces="(add_distinguishing_sequence_if_required (get_distinguishing_sequence_from_ofsm_tables M))", OF add_distinguishing_sequence_if_required_distinguishes[OF assms(1,3), where dist_fun="(get_distinguishing_sequence_from_ofsm_tables M)"] add_distinguishing_sequence_if_required_finite[where dist_fun="(get_distinguishing_sequence_from_ofsm_tables M)"] ]
using get_distinguishing_sequence_from_ofsm_tables_distinguishes[OF assms(1,3)]
unfolding h_method_via_pair_framework_def[symmetric]
by blast+
definition h_method_via_pair_framework_2 :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ bool ⇒ ('b×'c) prefix_tree" where
"h_method_via_pair_framework_2 M m c = pair_framework_h_components M m (add_distinguishing_sequence_and_complete_if_required (get_distinguishing_sequence_from_ofsm_tables M) c)"
lemma h_method_via_pair_framework_2_completeness_and_finiteness :
assumes "observable M"
and "observable I"
and "minimal M"
and "size I ≤ m"
and "m ≥ size_r M"
and "inputs I = inputs M"
and "outputs I = outputs M"
shows "(L M = L I) ⟷ (L M ∩ set (h_method_via_pair_framework_2 M m c) = L I ∩ set (h_method_via_pair_framework_2 M m c))"
and "finite_tree (h_method_via_pair_framework_2 M m c)"
using pair_framework_h_components_completeness_and_finiteness[OF assms(1,2,3,5,4,6,7), where get_separating_traces="(add_distinguishing_sequence_and_complete_if_required (get_distinguishing_sequence_from_ofsm_tables M) c)", OF add_distinguishing_sequence_and_complete_if_required_distinguishes[OF assms(1,3), where dist_fun="(get_distinguishing_sequence_from_ofsm_tables M)"] add_distinguishing_sequence_and_complete_if_required_finite[where dist_fun="(get_distinguishing_sequence_from_ofsm_tables M)"] ]
using get_distinguishing_sequence_from_ofsm_tables_distinguishes[OF assms(1,3)]
unfolding h_method_via_pair_framework_2_def[symmetric]
by blast+
definition h_method_via_pair_framework_3 :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ bool ⇒ bool ⇒ ('b×'c) prefix_tree" where
"h_method_via_pair_framework_3 M m c1 c2 = pair_framework_h_components_2 M m (add_cheapest_distinguishing_trace (get_distinguishing_sequence_from_ofsm_tables M) c2) c1"
lemma h_method_via_pair_framework_3_completeness_and_finiteness :
assumes "observable M"
and "observable I"
and "minimal M"
and "size I ≤ m"
and "m ≥ size_r M"
and "inputs I = inputs M"
and "outputs I = outputs M"
shows "(L M = L I) ⟷ (L M ∩ set (h_method_via_pair_framework_3 M m c1 c2) = L I ∩ set (h_method_via_pair_framework_3 M m c1 c2))"
and "finite_tree (h_method_via_pair_framework_3 M m c1 c2)"
using pair_framework_h_components_2_completeness_and_finiteness[OF assms(1,2,3,5,4,6,7), where get_separating_traces="(add_cheapest_distinguishing_trace (get_distinguishing_sequence_from_ofsm_tables M) c2)", OF add_cheapest_distinguishing_trace_distinguishes[OF assms(1,3), where dist_fun="(get_distinguishing_sequence_from_ofsm_tables M)"] add_cheapest_distinguishing_trace_finite[where dist_fun="(get_distinguishing_sequence_from_ofsm_tables M)"] ]
using get_distinguishing_sequence_from_ofsm_tables_distinguishes[OF assms(1,3)]
unfolding h_method_via_pair_framework_3_def[symmetric]
by blast+
definition h_method_via_pair_framework_lists :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ (('b×'c) × bool) list list" where
"h_method_via_pair_framework_lists M m = sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M (initial M) (h_method_via_pair_framework M m))"
lemma h_method_implementation_lists_completeness :
assumes "observable M"
and "observable I"
and "minimal M"
and "size I ≤ m"
and "m ≥ size_r M"
and "inputs I = inputs M"
and "outputs I = outputs M"
shows "(L M = L I) ⟷ list_all (passes_test_case I (initial I)) (h_method_via_pair_framework_lists M m)"
unfolding h_method_via_pair_framework_lists_def
h_method_via_pair_framework_completeness_and_finiteness(1)[OF assms]
passes_test_cases_from_io_tree[OF assms(1,2) fsm_initial fsm_initial h_method_via_pair_framework_completeness_and_finiteness(2)[OF assms]]
by blast
subsubsection ‹Code Equations›
lemma h_method_via_pair_framework_code[code] :
"h_method_via_pair_framework M m = (let
tables = (compute_ofsm_tables M (size M - 1));
distMap = mapping_of (map (λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2))
(filter (λ qq . fst qq ≠ snd qq) (List.product (states_as_list M) (states_as_list M))));
distHelper = (λ q1 q2 . if q1 ∈ states M ∧ q2 ∈ states M ∧ q1 ≠ q2 then the (Mapping.lookup distMap (q1,q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2);
distFun = add_distinguishing_sequence_if_required distHelper
in pair_framework_h_components M m distFun)"
unfolding h_method_via_pair_framework_def
apply (subst get_distinguishing_sequence_from_ofsm_tables_precomputed[of M])
unfolding Let_def
by presburger
lemma h_method_via_pair_framework_2_code[code] :
"h_method_via_pair_framework_2 M m c = (let
tables = (compute_ofsm_tables M (size M - 1));
distMap = mapping_of (map (λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2))
(filter (λ qq . fst qq ≠ snd qq) (List.product (states_as_list M) (states_as_list M))));
distHelper = (λ q1 q2 . if q1 ∈ states M ∧ q2 ∈ states M ∧ q1 ≠ q2 then the (Mapping.lookup distMap (q1,q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2);
distFun = add_distinguishing_sequence_and_complete_if_required distHelper c
in pair_framework_h_components M m distFun)"
unfolding h_method_via_pair_framework_2_def
apply (subst get_distinguishing_sequence_from_ofsm_tables_precomputed[of M])
unfolding Let_def
by presburger
lemma h_method_via_pair_framework_3_code[code] :
"h_method_via_pair_framework_3 M m c1 c2 = (let
tables = (compute_ofsm_tables M (size M - 1));
distMap = mapping_of (map (λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2))
(filter (λ qq . fst qq ≠ snd qq) (List.product (states_as_list M) (states_as_list M))));
distHelper = (λ q1 q2 . if q1 ∈ states M ∧ q2 ∈ states M ∧ q1 ≠ q2 then the (Mapping.lookup distMap (q1,q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2);
distFun = add_cheapest_distinguishing_trace distHelper c2
in pair_framework_h_components_2 M m distFun c1)"
unfolding h_method_via_pair_framework_3_def
apply (subst get_distinguishing_sequence_from_ofsm_tables_precomputed[of M])
unfolding Let_def
by presburger
end