section ‹Representing Test Suites as Sets of Input-Output Sequences› text ‹This theory describes the representation of test suites as sets of input-output sequences and defines a pass relation for this representation.› theory Test_Suite_IO imports Test_Suite Maximal_Path_Trie begin fun test_suite_to_io :: "('a,'b,'c) fsm ⇒ ('a,'b,'c,'d) test_suite ⇒ ('b × 'c) list set" where "test_suite_to_io M (Test_Suite prs tps rd_targets atcs) = (⋃ (q,P) ∈ prs . L P) ∪ (⋃{(λ io' . p_io p @ io') ` (set (prefixes (p_io pt))) | p pt . ∃ q P . (q,P) ∈ prs ∧ path P (initial P) p ∧ target (initial P) p = q ∧ pt ∈ tps q}) ∪ (⋃{(λ io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A) | p pt q A . ∃ P q' t1 t2 . (q,P) ∈ prs ∧ path P (initial P) p ∧ target (initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q,pt) ∧ (A,t1,t2) ∈ atcs (target q pt,q') })" lemma test_suite_to_io_language : assumes "implies_completeness T M m" shows "(test_suite_to_io M T) ⊆ L M" proof fix io assume "io ∈ test_suite_to_io M T" obtain prs tps rd_targets atcs where "T = Test_Suite prs tps rd_targets atcs" by (meson test_suite.exhaust) then obtain repetition_sets where repetition_sets_def: "implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets" using assms(1) unfolding implies_completeness_def by blast then have "implies_completeness (Test_Suite prs tps rd_targets atcs) M m" unfolding implies_completeness_def by blast have t2: "⋀ q P. (q, P) ∈ prs ⟹ is_preamble P M q" using implies_completeness_for_repetition_sets_simps(2)[OF repetition_sets_def] by blast have t5: "⋀q. q ∈ FSM.states M ⟹ (∃d∈set repetition_sets. q ∈ fst d)" using implies_completeness_for_repetition_sets_simps(4)[OF repetition_sets_def] by assumption have t6: "⋀ q. q ∈ fst ` prs ⟹ tps q ⊆ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m} ∧ fst ` (m_traversal_paths_with_witness M q repetition_sets m) ⊆ tps q" using implies_completeness_for_repetition_sets_simps(7)[OF repetition_sets_def] by assumption have t8: "⋀ d. d ∈ set repetition_sets ⟹ snd d ⊆ fst d" using implies_completeness_for_repetition_sets_simps(5,6)[OF repetition_sets_def] by blast from ‹io ∈ test_suite_to_io M T› consider (a) "io ∈ (⋃ (q,P) ∈ prs . L P)" | (b) "io ∈ (⋃{(λ io' . p_io p @ io') ` (set (prefixes (p_io pt))) | p pt . ∃ q P . (q,P) ∈ prs ∧ path P (initial P) p ∧ target (initial P) p = q ∧ pt ∈ tps q})" | (c) "io ∈ (⋃{(λ io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A) | p pt q A . ∃ P q' t1 t2 . (q,P) ∈ prs ∧ path P (initial P) p ∧ target (initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q,pt) ∧ (A,t1,t2) ∈ atcs (target q pt,q') })" unfolding ‹T = Test_Suite prs tps rd_targets atcs› test_suite_to_io.simps by blast then show "io ∈ L M" proof cases case a then obtain q P where "(q, P) ∈ prs" and "io ∈ L P" by blast have "is_submachine P M" using t2[OF ‹(q, P) ∈ prs›] unfolding is_preamble_def by blast show "io ∈ L M" using submachine_language[OF ‹is_submachine P M›] ‹io ∈ L P› by blast next case b then obtain p pt q P where "io ∈ (λ io' . p_io p @ io') ` (set (prefixes (p_io pt)))" and "(q,P) ∈ prs" and "path P (initial P) p" and "target (initial P) p = q" and "pt ∈ tps q" by blast then obtain io' where "io = p_io p @ io'" and "io' ∈ (set (prefixes (p_io pt)))" by blast then obtain io'' where "p_io pt = io' @ io''" and "io = p_io p @ io'" unfolding prefixes_set proof - assume a1: "io' ∈ {xs'. ∃xs''. xs' @ xs'' = p_io pt}" assume "⋀io''. ⟦p_io pt = io' @ io''; io = p_io p @ io'⟧ ⟹ thesis" then show ?thesis using a1 ‹io = p_io p @ io'› by moura qed have "q ∈ fst ` prs" using ‹(q,P) ∈ prs› by force have "is_submachine P M" using t2[OF ‹(q, P) ∈ prs›] unfolding is_preamble_def by blast then have "initial P = initial M" by auto have "path M (initial M) p" using submachine_path[OF ‹is_submachine P M› ‹path P (initial P) p›] unfolding ‹initial P = initial M› by assumption have "target (initial M) p = q" using ‹target (initial P) p = q› unfolding ‹initial P = initial M› by assumption obtain p2 d where "(pt @ p2, d) ∈ m_traversal_paths_with_witness M q repetition_sets m" using t6[OF ‹q ∈ fst ` prs›] ‹pt ∈ tps q› by blast then have "path M q (pt @ p2)" using m_traversal_paths_with_witness_set[OF t5 t8 path_target_is_state[OF ‹path M (initial M) p›], of m] unfolding ‹target (initial M) p = q› by blast then have "path M (initial M) (p@pt)" using ‹path M (initial M) p› ‹target (initial M) p = q› by auto then have "p_io p @ p_io pt ∈ L M" by (metis (mono_tags, lifting) language_intro map_append) then show "io ∈ L M" unfolding ‹io = p_io p @ io'› ‹p_io pt = io' @ io''› append.assoc[symmetric] using language_prefix[of "p_io p @ io'" io'' M "initial M"] by blast next case c then obtain p pt q A P q' t1 t2 where "io ∈ (λ io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A)" and "(q,P) ∈ prs" and "path P (initial P) p" and "target (initial P) p = q" and "pt ∈ tps q" and "q' ∈ rd_targets (q,pt)" and "(A,t1,t2) ∈ atcs (target q pt,q')" by blast obtain ioA where "io = p_io p @ p_io pt @ ioA" and "ioA ∈ (atc_to_io_set (from_FSM M (target q pt)) A)" using ‹io ∈ (λ io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A)› by blast then have "ioA ∈ L (from_FSM M (target q pt))" unfolding atc_to_io_set.simps by blast have "q ∈ fst ` prs" using ‹(q,P) ∈ prs› by force have "is_submachine P M" using t2[OF ‹(q, P) ∈ prs›] unfolding is_preamble_def by blast then have "initial P = initial M" by auto have "path M (initial M) p" using submachine_path[OF ‹is_submachine P M› ‹path P (initial P) p›] unfolding ‹initial P = initial M› by assumption have "target (initial M) p = q" using ‹target (initial P) p = q› unfolding ‹initial P = initial M› by assumption obtain p2 d where "(pt @ p2, d) ∈ m_traversal_paths_with_witness M q repetition_sets m" using t6[OF ‹q ∈ fst ` prs›] ‹pt ∈ tps q› by blast then have "path M q (pt @ p2)" using m_traversal_paths_with_witness_set[OF t5 t8 path_target_is_state[OF ‹path M (initial M) p›], of m] unfolding ‹target (initial M) p = q› by blast then have "path M (initial M) (p@pt)" using ‹path M (initial M) p› ‹target (initial M) p = q› by auto moreover have "(target q pt) = target (initial M) (p@pt)" using ‹target (initial M) p = q› by auto ultimately have "(target q pt) ∈ states M" using path_target_is_state by metis have "ioA ∈ LS M (target q pt)" using from_FSM_language[OF ‹(target q pt) ∈ states M›] ‹ioA ∈ L (from_FSM M (target q pt))› by blast then obtain pA where "path M (target q pt) pA" and "p_io pA = ioA" by auto then have "path M (initial M) (p @ pt @ pA)" using ‹path M (initial M) (p@pt)› unfolding ‹(target q pt) = target (initial M) (p@pt)› by auto then have "p_io p @ p_io pt @ ioA ∈ L M" unfolding ‹p_io pA = ioA›[symmetric] using language_intro by fastforce then show "io ∈ L M" unfolding ‹io = p_io p @ p_io pt @ ioA› by assumption qed qed lemma minimal_io_seq_to_failure : assumes "¬ (L M' ⊆ L M)" and "inputs M' = inputs M" and "completely_specified M" obtains io x y y' where "io@[(x,y)] ∈ L M" and "io@[(x,y')] ∉ L M" and "io@[(x,y')] ∈ L M'" proof - obtain ioF where "ioF ∈ L M'" and "ioF ∉ L M" using assms(1) by blast let ?prefs = "{ioF' ∈ set (prefixes ioF) . ioF' ∈ L M' ∧ ioF' ∉ L M}" have "finite ?prefs" using prefixes_finite by auto moreover have "?prefs ≠ {}" unfolding prefixes_set using ‹ioF ∈ L M'› ‹ioF ∉ L M› by auto ultimately obtain ioF' where "ioF' ∈ ?prefs" and "⋀ ioF'' . ioF'' ∈ ?prefs ⟹ length ioF' ≤ length ioF''" by (meson leI min_length_elem) then have "ioF' ∈ L M'" and "ioF' ∉ L M" by auto then have "ioF' ≠ []" by auto then have "ioF' = (butlast ioF')@[last ioF']" and "length (butlast ioF') < length ioF'" by auto then have "butlast ioF' ∉ ?prefs" using ‹⋀ ioF'' . ioF'' ∈ ?prefs ⟹ length ioF' ≤ length ioF''› leD by blast moreover have "butlast ioF' ∈ L M'" using ‹ioF' ∈ L M'› language_prefix[of "butlast ioF'" "[last ioF']" M' "initial M'"] unfolding ‹ioF' = (butlast ioF')@[last ioF']›[symmetric] by blast moreover have "butlast ioF' ∈ set (prefixes ioF)" using ‹ioF' = (butlast ioF')@[last ioF']› ‹ioF' ∈ ?prefs› prefixes_set proof - have "∃ps. (butlast ioF' @ [last ioF']) @ ps = ioF" using ‹ioF' = butlast ioF' @ [last ioF']› ‹ioF' ∈ {ioF' ∈ set (prefixes ioF). ioF' ∈ L M' ∧ ioF' ∉ L M}› unfolding prefixes_set by auto then show ?thesis using prefixes_set by fastforce qed ultimately have "butlast ioF' ∈ L M" by blast have *: "(butlast ioF')@[(fst (last ioF'), snd (last ioF'))] ∈ L M'" using ‹ioF' ∈ L M'› ‹ioF' = (butlast ioF')@[last ioF']› by auto have **: "(butlast ioF')@[(fst (last ioF'), snd (last ioF'))] ∉ L M" using ‹ioF' ∉ L M› ‹ioF' = (butlast ioF')@[last ioF']› by auto obtain p where "path M (initial M) p" and "p_io p = butlast ioF'" using ‹butlast ioF' ∈ L M› by auto moreover obtain t where "t ∈ transitions M" and "t_source t = target (initial M) p" and "t_input t = fst (last ioF')" proof - have "fst (last ioF') ∈ inputs M'" using language_io(1)[OF *, of "fst (last ioF')" "snd (last ioF')"] by simp then have "fst (last ioF') ∈ inputs M" using assms(2) by auto then show ?thesis using that ‹completely_specified M› path_target_is_state[OF ‹path M (initial M) p›] unfolding completely_specified.simps by blast qed ultimately have ***: "(butlast ioF')@[(fst (last ioF'), t_output t)] ∈ L M" proof - have "p_io (p @ [t]) ∈ L M" by (metis (no_types) ‹path M (FSM.initial M) p› ‹t ∈ FSM.transitions M› ‹t_source t = target (FSM.initial M) p› language_intro path_append single_transition_path) then show ?thesis by (simp add: ‹p_io p = butlast ioF'› ‹t_input t = fst (last ioF')›) qed show ?thesis using that[OF *** ** *] by assumption qed lemma observable_minimal_path_to_failure : assumes "¬ (L M' ⊆ L M)" and "observable M" and "observable M'" and "inputs M' = inputs M" and "completely_specified M" and "completely_specified M'" obtains p p' t t' where "path M (initial M) (p@[t])" and "path M' (initial M') (p'@[t'])" and "p_io p' = p_io p" and "t_input t' = t_input t" and "¬(∃ t'' . t'' ∈ transitions M ∧ t_source t'' = target (initial M) p ∧ t_input t'' = t_input t ∧ t_output t'' = t_output t')" proof - obtain io x y y' where "io@[(x,y)] ∈ L M" and "io@[(x,y')] ∉ L M" and "io@[(x,y')] ∈ L M'" using minimal_io_seq_to_failure[OF assms(1,4,5)] by blast obtain p t where "path M (initial M) (p@[t])" and "p_io p = io" and "t_input t = x" and "t_output t = y" using language_append_path_ob[OF ‹io@[(x,y)] ∈ L M›] by blast moreover obtain p' t' where "path M' (initial M') (p'@[t'])" and "p_io p' = io" and "t_input t' = x" and "t_output t' = y'" using language_append_path_ob[OF ‹io@[(x,y')] ∈ L M'›] by blast moreover have "¬(∃ t'' . t'' ∈ transitions M ∧ t_source t'' = target (initial M) p ∧ t_input t'' = t_input t ∧ t_output t'' = t_output t')" proof assume "∃t''. t'' ∈ FSM.transitions M ∧ t_source t'' = target (FSM.initial M) p ∧ t_input t'' = t_input t ∧ t_output t'' = t_output t'" then obtain t'' where "t'' ∈ FSM.transitions M" and "t_source t'' = target (FSM.initial M) p" and "t_input t'' = x" and "t_output t'' = y'" unfolding ‹t_input t = x› ‹t_output t' = y'› by blast then have "path M (initial M) (p@[t''])" using ‹path M (initial M) (p@[t])› by (meson path_append_elim path_append_transition) moreover have "p_io (p@[t'']) = io@[(x,y')]" using ‹p_io p = io› ‹t_input t'' = x› ‹t_output t'' = y'› by auto ultimately have "io@[(x,y')] ∈ L M" using language_state_containment by (metis (mono_tags, lifting)) then show "False" using ‹io@[(x,y')] ∉ L M› by blast qed ultimately show ?thesis using that[of p t p' t'] by force qed lemma test_suite_to_io_pass : assumes "implies_completeness T M m" and "observable M" and "observable M'" and "inputs M' = inputs M" and "inputs M ≠ {}" and "completely_specified M" and "completely_specified M'" shows "pass_io_set M' (test_suite_to_io M T) = passes_test_suite M T M'" proof - obtain prs tps rd_targets atcs where "T = Test_Suite prs tps rd_targets atcs" by (meson test_suite.exhaust) then obtain repetition_sets where repetition_sets_def: "implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets" using assms(1) unfolding implies_completeness_def by blast then have "implies_completeness (Test_Suite prs tps rd_targets atcs) M m" unfolding implies_completeness_def by blast then have test_suite_language_prop: "test_suite_to_io M (Test_Suite prs tps rd_targets atcs) ⊆ L M" using test_suite_to_io_language by blast have t1: "(initial M, initial_preamble M) ∈ prs" using implies_completeness_for_repetition_sets_simps(1)[OF repetition_sets_def] by assumption have t2: "⋀ q P. (q, P) ∈ prs ⟹ is_preamble P M q" using implies_completeness_for_repetition_sets_simps(2)[OF repetition_sets_def] by blast have t3: "⋀ q1 q2 A d1 d2. (A, d1, d2) ∈ atcs (q1, q2) ⟹ (A, d2, d1) ∈ atcs (q2, q1) ∧ is_separator M q1 q2 A d1 d2" using implies_completeness_for_repetition_sets_simps(3)[OF repetition_sets_def] by assumption have t5: "⋀q. q ∈ FSM.states M ⟹ (∃d∈set repetition_sets. q ∈ fst d)" using implies_completeness_for_repetition_sets_simps(4)[OF repetition_sets_def] by assumption have t6: "⋀ q. q ∈ fst ` prs ⟹ tps q ⊆ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m} ∧ fst ` (m_traversal_paths_with_witness M q repetition_sets m) ⊆ tps q" using implies_completeness_for_repetition_sets_simps(7)[OF repetition_sets_def] by assumption have t7: "⋀ d. d ∈ set repetition_sets ⟹ fst d ⊆ FSM.states M" and t8: "⋀ d. d ∈ set repetition_sets ⟹ snd d ⊆ fst d" and t8': "⋀ d. d ∈ set repetition_sets ⟹ snd d = fst d ∩ fst ` prs" and t9: "⋀ d q1 q2. d ∈ set repetition_sets ⟹ q1 ∈ fst d ⟹ q2 ∈ fst d ⟹ q1 ≠ q2 ⟹ atcs (q1, q2) ≠ {}" using implies_completeness_for_repetition_sets_simps(5,6)[OF repetition_sets_def] by blast+ have "pass_io_set M' (test_suite_to_io M (Test_Suite prs tps rd_targets atcs)) ⟹ passes_test_suite M (Test_Suite prs tps rd_targets atcs) M'" proof - assume "pass_io_set M' (test_suite_to_io M (Test_Suite prs tps rd_targets atcs))" then have pass_io_prop: "⋀ io x y y' . io @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs) ⟹ io @ [(x, y')] ∈ L M' ⟹ io @ [(x, y')] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" unfolding pass_io_set_def by blast show "passes_test_suite M (Test_Suite prs tps rd_targets atcs) M'" proof (rule ccontr) assume "¬ passes_test_suite M (Test_Suite prs tps rd_targets atcs) M'" then consider (a) "¬ (∀q P io x y y'. (q, P) ∈ prs ⟶ io @ [(x, y)] ∈ L P ⟶ io @ [(x, y')] ∈ L M' ⟶ io @ [(x, y')] ∈ L P)" | (b) "¬ ((∀q P pP ioT pT x y y'. (q, P) ∈ prs ⟶ path P (FSM.initial P) pP ⟶ target (FSM.initial P) pP = q ⟶ pT ∈ tps q ⟶ ioT @ [(x, y)] ∈ set (prefixes (p_io pT)) ⟶ p_io pP @ ioT @ [(x, y')] ∈ L M' ⟶ (∃pT'. pT' ∈ tps q ∧ ioT @ [(x, y')] ∈ set (prefixes (p_io pT')))))" | (c) "¬ ((∀q P pP pT. (q, P) ∈ prs ⟶ path P (FSM.initial P) pP ⟶ target (FSM.initial P) pP = q ⟶ pT ∈ tps q ⟶ p_io pP @ p_io pT ∈ L M' ⟶ (∀q' A d1 d2 qT. q' ∈ rd_targets (q, pT) ⟶ (A, d1, d2) ∈ atcs (target q pT, q') ⟶ qT ∈ io_targets M' (p_io pP @ p_io pT) (FSM.initial M') ⟶ pass_separator_ATC M' A qT d2)))" unfolding passes_test_suite.simps by blast then show False proof cases case a then obtain q P io x y y' where "(q, P) ∈ prs" and "io @ [(x, y)] ∈ L P" and "io @ [(x, y')] ∈ L M'" and "io @ [(x, y')] ∉ L P" by blast have "is_preamble P M q" using t2[OF ‹(q, P) ∈ prs›] by assumption have "io @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" unfolding test_suite_to_io.simps using ‹(q, P) ∈ prs› ‹io @ [(x, y)] ∈ L P› by fastforce have "io @ [(x, y')] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" using pass_io_prop[OF ‹io @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)› ‹io @ [(x, y')] ∈ L M'›] by assumption then have "io @ [(x, y')] ∈ L M" using test_suite_language_prop by blast have "io @ [(x, y')] ∈ L P" using passes_test_suite_soundness_helper_1[OF ‹is_preamble P M q› ‹observable M› ‹io @ [(x, y)] ∈ L P› ‹io @ [(x, y')] ∈ L M›] by assumption then show "False" using ‹io @ [(x, y')] ∉ L P› by blast next case b then obtain q P pP ioT pT x y y' where "(q, P) ∈ prs" and "path P (FSM.initial P) pP" and "target (FSM.initial P) pP = q" and "pT ∈ tps q" and "ioT @ [(x, y)] ∈ set (prefixes (p_io pT))" and "p_io pP @ ioT @ [(x, y')] ∈ L M'" and "¬ (∃pT'. pT' ∈ tps q ∧ ioT @ [(x, y')] ∈ set (prefixes (p_io pT')))" by blast have "∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) pP ∧ target (FSM.initial P) pP = q ∧ pT ∈ tps q" using ‹(q, P) ∈ prs› ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› ‹pT ∈ tps q› by blast moreover have "p_io pP @ ioT @ [(x, y)] ∈ (@) (p_io pP) ` set (prefixes (p_io pT))" using ‹ioT @ [(x, y)] ∈ set (prefixes (p_io pT))› by auto ultimately have "p_io pP @ ioT @ [(x, y)] ∈ (⋃{(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q})" by blast then have "p_io pP @ ioT @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" unfolding test_suite_to_io.simps by blast then have *: "(p_io pP @ ioT) @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" by auto have **: "(p_io pP @ ioT) @ [(x, y')] ∈ L M'" using ‹p_io pP @ ioT @ [(x, y')] ∈ L M'› by auto have "(p_io pP @ ioT) @ [(x, y')] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" using pass_io_prop[OF * ** ] by assumption then have "(p_io pP @ ioT) @ [(x, y')] ∈ L M" using test_suite_language_prop by blast have "q ∈ states M" using is_preamble_is_state[OF t2[OF ‹(q, P) ∈ prs›]] by assumption have "q ∈ fst ` prs" using ‹(q, P) ∈ prs› by force obtain pT' d' where "(pT @ pT', d') ∈ m_traversal_paths_with_witness M q repetition_sets m" using t6[OF ‹q ∈ fst ` prs›] ‹pT ∈ tps q› by blast then have "path M q (pT @ pT')" and "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (pT @ pT'))) repetition_sets = Some d'" and "⋀ p' p''. (pT @ pT') = p' @ p'' ⟹ p'' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repetition_sets = None" using m_traversal_paths_with_witness_set[OF t5 t8 ‹q ∈ states M›, of m] by blast+ obtain ioT' where "p_io pT = ioT @ [(x,y)] @ ioT'" using prefixes_set_ob[OF ‹ioT @ [(x, y)] ∈ set (prefixes (p_io pT))›] unfolding prefixes_set append.assoc[symmetric] by blast let ?pt = "take (length (ioT @ [(x,y)])) pT" let ?p = "butlast ?pt" let ?t = "last ?pt" have "length ?pt > 0" using ‹p_io pT = ioT @ [(x,y)] @ ioT'› unfolding length_map[of "(λ t . (t_input t, t_output t))", symmetric] by auto then have "?pt = ?p @ [?t]" by auto moreover have "path M q ?pt" using ‹path M q (pT @ pT')› by (meson path_prefix path_prefix_take) ultimately have "path M q (?p@[?t])" by simp have "p_io ?p = ioT" proof - have "p_io ?pt = take (length (ioT @ [(x,y)])) (p_io pT)" by (simp add: take_map) then have "p_io ?pt = ioT @ [(x,y)]" using ‹p_io pT = ioT @ [(x,y)] @ ioT'› by auto then show ?thesis by (simp add: map_butlast) qed have "path M q ?p" using path_append_transition_elim[OF ‹path M q (?p@[?t])›] by blast have "is_submachine P M" using t2[OF ‹(q, P) ∈ prs›] unfolding is_preamble_def by blast then have "initial P = initial M" by auto have "path M (initial M) pP" using submachine_path[OF ‹is_submachine P M› ‹path P (initial P) pP›] unfolding ‹initial P = initial M› by assumption moreover have "target (initial M) pP = q" using ‹target (initial P) pP = q› unfolding ‹initial P = initial M› by assumption ultimately have "path M (initial M) (pP@?p)" using ‹path M q ?p› by auto have "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) ?p)) repetition_sets = None" proof - have *: "(pT @ pT') = ?p @ ([?t] @ (drop (length (ioT @ [(x,y)])) pT) @ pT')" using ‹?pt = ?p @ [?t]› by (metis append_assoc append_take_drop_id) have **: "([?t] @ (drop (length (ioT @ [(x,y)])) pT) @ pT') ≠ []" by simp show ?thesis using ‹⋀ p' p''. (pT @ pT') = p' @ p'' ⟹ p'' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repetition_sets = None›[OF * **] by assumption qed (* obtain paths from the transition ending in y' to get a transition from ?p *) obtain p' t' where "path M (FSM.initial M) (p' @ [t'])" and "p_io p' = p_io pP @ ioT" and "t_input t' = x" and "t_output t' = y'" using language_append_path_ob[OF ‹(p_io pP @ ioT) @ [(x, y')] ∈ L M›] by blast then have "path M (FSM.initial M) p'" and "t_source t' = target (initial M) p'" and "t' ∈ transitions M" by auto have "p' = pP @ ?p" using observable_path_unique[OF ‹observable M› ‹path M (FSM.initial M) p'› ‹path M (initial M) (pP@?p)›] ‹p_io ?p = ioT› unfolding ‹p_io p' = p_io pP @ ioT› by simp then have "t_source t' = target q ?p" unfolding ‹t_source t' = target (initial M) p'› using ‹target (initial M) pP = q› by auto obtain pTt' dt' where "(?p @ [t'] @ pTt', dt') ∈ m_traversal_paths_with_witness M q repetition_sets m" using m_traversal_path_extension_exist_for_transition[OF ‹completely_specified M› ‹q ∈ states M› ‹FSM.inputs M ≠ {}› t5 t8 ‹path M q ?p› ‹find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) ?p)) repetition_sets = None› ‹t' ∈ transitions M› ‹t_source t' = target q ?p›] by blast have "?p @ [t'] @ pTt' ∈ tps q" using t6[OF ‹q ∈ fst ` prs› ] ‹(?p @ [t'] @ pTt', dt') ∈ m_traversal_paths_with_witness M q repetition_sets m› by force moreover have "ioT @ [(x, y')] ∈ set (prefixes (p_io (?p @ [t'] @ pTt')))" proof - have "p_io (?p @ [t'] @ pTt') = ioT @ [(x,y')] @ p_io pTt'" using ‹p_io ?p = ioT› using ‹t_input t' = x› ‹t_output t' = y'› by auto then show ?thesis unfolding prefixes_set by force qed ultimately show "False" using ‹¬ (∃pT'. pT' ∈ tps q ∧ ioT @ [(x, y')] ∈ set (prefixes (p_io pT')))› by blast next case c then obtain q P pP pT q' A d1 d2 qT where "(q, P) ∈ prs" and "path P (FSM.initial P) pP" and "target (FSM.initial P) pP = q" and "pT ∈ tps q" and "p_io pP @ p_io pT ∈ L M'" and "q' ∈ rd_targets (q, pT)" and "(A, d1, d2) ∈ atcs (target q pT, q')" and "qT ∈ io_targets M' (p_io pP @ p_io pT) (FSM.initial M')" and "¬pass_separator_ATC M' A qT d2" by blast have "is_submachine P M" using t2[OF ‹(q, P) ∈ prs›] unfolding is_preamble_def by blast then have "initial P = initial M" by auto have "path M (initial M) pP" using submachine_path[OF ‹is_submachine P M› ‹path P (initial P) pP›] unfolding ‹initial P = initial M› by assumption have "target (initial M) pP = q" using ‹target (initial P) pP = q› unfolding ‹initial P = initial M› by assumption have "q ∈ states M" using is_preamble_is_state[OF t2[OF ‹(q, P) ∈ prs›]] by assumption have "q ∈ fst ` prs" using ‹(q, P) ∈ prs› by force obtain pT' d' where "(pT @ pT', d') ∈ m_traversal_paths_with_witness M q repetition_sets m" using t6[OF ‹q ∈ fst ` prs›] ‹pT ∈ tps q› by blast then have "path M q (pT @ pT')" and "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (pT @ pT'))) repetition_sets = Some d'" and "⋀ p' p''. (pT @ pT') = p' @ p'' ⟹ p'' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repetition_sets = None" using m_traversal_paths_with_witness_set[OF t5 t8 ‹q ∈ states M›, of m] by blast+ then have "path M q pT" by auto have "qT ∈ states M'" using ‹qT ∈ io_targets M' (p_io pP @ p_io pT) (FSM.initial M')› io_targets_states subset_iff by fastforce have "is_separator M (target q pT) q' A d1 d2" using t3[OF ‹(A, d1, d2) ∈ atcs (target q pT, q')›] by blast have "¬ pass_io_set (FSM.from_FSM M' qT) (atc_to_io_set (FSM.from_FSM M (target q pT)) A)" using ‹¬pass_separator_ATC M' A qT d2› pass_separator_pass_io_set_iff[OF ‹is_separator M (target q pT) q' A d1 d2› ‹observable M› ‹observable M'› path_target_is_state[OF ‹path M q pT›] ‹qT ∈ states M'› ‹inputs M' = inputs M› ‹completely_specified M›] by simp have "pass_io_set (FSM.from_FSM M' qT) (atc_to_io_set (FSM.from_FSM M (target q pT)) A)" proof - have "⋀ io x y y' . io @ [(x, y)] ∈ atc_to_io_set (FSM.from_FSM M (target q pT)) A ⟹ io @ [(x, y')] ∈ L (FSM.from_FSM M' qT) ⟹ io @ [(x, y')] ∈ atc_to_io_set (FSM.from_FSM M (target q pT)) A" proof - fix io x y y' assume "io @ [(x, y)] ∈ atc_to_io_set (FSM.from_FSM M (target q pT)) A" and "io @ [(x, y')] ∈ L (FSM.from_FSM M' qT)" (* subsets of test_suite_to_io *) define tmp where tmp_def : "tmp = (⋃ {(λio_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A |p pt q A. ∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')})" define tmp2 where tmp2_def : "tmp2 = ⋃ {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q}" have "∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) pP ∧ target (FSM.initial P) pP = q ∧ pT ∈ tps q ∧ q' ∈ rd_targets (q, pT) ∧ (A, t1, t2) ∈ atcs (target q pT, q')" using ‹(q, P) ∈ prs› ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› ‹pT ∈ tps q› ‹q' ∈ rd_targets (q, pT)› ‹(A, d1, d2) ∈ atcs (target q pT, q')› by blast then have "(λio_atc. p_io pP @ p_io pT @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pT)) A ⊆ tmp" unfolding tmp_def by blast then have "(λio_atc. p_io pP @ p_io pT @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pT)) A ⊆ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" unfolding test_suite_to_io.simps tmp_def[symmetric] tmp2_def[symmetric] by blast moreover have "(p_io pP @ p_io pT @ (io @ [(x, y)])) ∈ (λio_atc. p_io pP @ p_io pT @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pT)) A" using ‹io @ [(x, y)] ∈ atc_to_io_set (FSM.from_FSM M (target q pT)) A› by auto ultimately have "(p_io pP @ p_io pT @ (io @ [(x, y)])) ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" by blast then have *: "(p_io pP @ p_io pT @ io) @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" by simp have "io @ [(x, y')] ∈ LS M' qT" using ‹io @ [(x, y')] ∈ L (FSM.from_FSM M' qT)› ‹qT ∈ states M'› by (metis from_FSM_language) have **: "(p_io pP @ p_io pT @ io) @ [(x, y')] ∈ L M'" using io_targets_language_append[OF ‹qT ∈ io_targets M' (p_io pP @ p_io pT) (FSM.initial M')› ‹io @ [(x, y')] ∈ LS M' qT›] by simp have "(p_io pP @ p_io pT) @ (io @ [(x, y')]) ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" using pass_io_prop[OF * ** ] by simp then have "(p_io pP @ p_io pT) @ (io @ [(x, y')]) ∈ L M" using test_suite_language_prop by blast moreover have "target q pT ∈ io_targets M (p_io pP @ p_io pT) (initial M)" proof - have "target (initial M) (pP@pT) = target q pT" unfolding ‹target (initial M) pP = q›[symmetric] by auto moreover have "path M (initial M) (pP@pT)" using ‹path M (initial M) pP› ‹path M q pT› unfolding ‹target (initial M) pP = q›[symmetric] by auto moreover have "p_io (pP@pT) = (p_io pP @ p_io pT)" by auto ultimately show ?thesis unfolding io_targets.simps by (metis (mono_tags, lifting) mem_Collect_eq) qed ultimately have "io @ [(x, y')] ∈ LS M (target q pT)" using observable_io_targets_language[OF _ ‹observable M›, of "(p_io pP @ p_io pT)" "(io @ [(x, y')])" "initial M" "target q pT"] by blast then have "io @ [(x, y')] ∈ L (FSM.from_FSM M (target q pT))" unfolding from_FSM_language[OF path_target_is_state[OF ‹path M q pT›]] by assumption moreover have "io @ [(x, y')] ∈ L A" by (metis Int_iff ‹io @ [(x, y')] ∈ LS M (target q pT)› ‹io @ [(x, y)] ∈ atc_to_io_set (FSM.from_FSM M (target q pT)) A› ‹is_separator M (target q pT) q' A d1 d2› atc_to_io_set.simps is_separator_simps(9)) ultimately show "io @ [(x, y')] ∈ atc_to_io_set (FSM.from_FSM M (target q pT)) A" unfolding atc_to_io_set.simps by blast qed then show ?thesis unfolding pass_io_set_def by blast qed then show "False" using pass_separator_from_pass_io_set[OF ‹is_separator M (target q pT) q' A d1 d2› _ ‹observable M› ‹observable M'› path_target_is_state[OF ‹path M q pT›] ‹qT ∈ states M'› ‹inputs M' = inputs M› ‹completely_specified M›] ‹¬pass_separator_ATC M' A qT d2› by simp qed qed qed moreover have "passes_test_suite M (Test_Suite prs tps rd_targets atcs) M' ⟹ pass_io_set M' (test_suite_to_io M (Test_Suite prs tps rd_targets atcs))" proof - assume "passes_test_suite M (Test_Suite prs tps rd_targets atcs) M'" (* pass properties *) have pass1: "⋀ q P io x y y' . (q,P) ∈ prs ⟹ io@[(x,y)] ∈ L P ⟹ io@[(x,y')] ∈ L M' ⟹ io@[(x,y')] ∈ L P" using ‹passes_test_suite M (Test_Suite prs tps rd_targets atcs) M'› unfolding passes_test_suite.simps by meson have pass2: "⋀ q P pP ioT pT x y y' . (q,P) ∈ prs ⟹ path P (initial P) pP ⟹ target (initial P) pP = q ⟹ pT ∈ tps q ⟹ ioT@[(x,y)] ∈ set (prefixes (p_io pT)) ⟹ (p_io pP)@ioT@[(x,y')] ∈ L M' ⟹ (∃ pT' . pT' ∈ tps q ∧ ioT@[(x,y')] ∈ set (prefixes (p_io pT')))" using ‹passes_test_suite M (Test_Suite prs tps rd_targets atcs) M'› unfolding passes_test_suite.simps by blast have pass3: "⋀ q P pP pT q' A d1 d2 qT . (q,P) ∈ prs ⟹ path P (initial P) pP ⟹ target (initial P) pP = q ⟹ pT ∈ tps q ⟹ (p_io pP)@(p_io pT) ∈ L M' ⟹ q' ∈ rd_targets (q,pT) ⟹ (A,d1,d2) ∈ atcs (target q pT, q') ⟹ qT ∈ io_targets M' ((p_io pP)@(p_io pT)) (initial M') ⟹ pass_separator_ATC M' A qT d2" using ‹passes_test_suite M (Test_Suite prs tps rd_targets atcs) M'› unfolding passes_test_suite.simps by blast show "pass_io_set M' (test_suite_to_io M (Test_Suite prs tps rd_targets atcs))" proof (rule ccontr) assume "¬ pass_io_set M' (test_suite_to_io M (Test_Suite prs tps rd_targets atcs))" then obtain io x y y' where "io @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" and "io @ [(x, y')] ∈ L M'" and "io @ [(x, y')] ∉ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" unfolding pass_io_set_def by blast have preamble_prop: "⋀ q P . (q, P) ∈ prs ⟹ io @ [(x, y)] ∈ L P ⟹ False" proof - fix q P assume "(q, P)∈prs" and "io @ [(x, y)] ∈ L P" have "io @ [(x, y')] ∈ L P" using pass1[OF ‹(q, P)∈prs› ‹io @ [(x, y)] ∈ L P› ‹io @ [(x, y')] ∈ L M'› ] by assumption then have "io @ [(x, y')] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" unfolding test_suite_to_io.simps using ‹(q, P)∈prs› by blast then show "False" using ‹io @ [(x, y')] ∉ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)› by simp qed have traversal_path_prop : "⋀ pP pt q P . io @ [(x, y)] ∈ (@) (p_io pP) ` set (prefixes (p_io pt)) ⟹ (q, P) ∈ prs ⟹ path P (FSM.initial P) pP ⟹ target (FSM.initial P) pP = q ⟹ pt ∈ tps q ⟹ False" proof - fix pP pt q P assume "io @ [(x, y)] ∈ (@) (p_io pP) ` set (prefixes (p_io pt))" and "(q, P) ∈ prs" and "path P (FSM.initial P) pP" and "target (FSM.initial P) pP = q" and "pt ∈ tps q" obtain io' io'' where "io @ [(x, y)] = (p_io pP) @ io'" and "io'@io'' = p_io pt" using ‹io @ [(x, y)] ∈ (@) (p_io pP) ` set (prefixes (p_io pt))› unfolding prefixes_set by blast have "is_submachine P M" using t2[OF ‹(q, P) ∈ prs›] unfolding is_preamble_def by blast then have "initial P = initial M" by auto have "path M (initial M) pP" using submachine_path[OF ‹is_submachine P M› ‹path P (initial P) pP›] unfolding ‹initial P = initial M› by assumption have "target (initial M) pP = q" using ‹target (initial P) pP = q› unfolding ‹initial P = initial M› by assumption have "q ∈ states M" using is_preamble_is_state[OF t2[OF ‹(q, P) ∈ prs›]] by assumption have "q ∈ fst ` prs" using ‹(q, P) ∈ prs› by force show "False" proof (cases io' rule: rev_cases) case Nil then have "p_io pP = io @ [(x, y)]" using ‹io @ [(x, y)] = (p_io pP) @ io'› by auto show ?thesis using preamble_prop[OF ‹(q,P) ∈ prs› language_state_containment[OF ‹path P (FSM.initial P) pP› ‹p_io pP = io @ [(x, y)]›]] by assumption next case (snoc ioI xy) then have "xy = (x,y)" and "io = (p_io pP) @ ioI" using ‹io @ [(x, y)] = (p_io pP) @ io'› by auto then have "p_io pP @ ioI @ [(x, y')] ∈ L M'" using ‹io @ [(x, y')] ∈ L M'› by simp have "ioI @ [(x, y)] ∈ set (prefixes (p_io pt))" unfolding prefixes_set using ‹io' @ io'' = p_io pt› ‹xy = (x, y)› snoc by auto obtain pT' where "pT' ∈ tps q" and "ioI @ [(x, y')] ∈ set (prefixes (p_io pT'))" using pass2[OF ‹(q, P) ∈ prs› ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› ‹pt ∈ tps q› ‹ioI @ [(x, y)] ∈ set (prefixes (p_io pt))› ‹p_io pP @ ioI @ [(x, y')] ∈ L M'›] by blast have "io @ [(x, y')] ∈ (@) (p_io pP) ` set (prefixes (p_io pT'))" using ‹ioI @ [(x, y')] ∈ set (prefixes (p_io pT'))› unfolding ‹io = (p_io pP) @ ioI› by simp have "io @ [(x, y')] ∈ (⋃ {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q})" using ‹(q, P) ∈ prs› ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› ‹pT' ∈ tps q› ‹io @ [(x, y')] ∈ (@) (p_io pP) ` set (prefixes (p_io pT'))› by blast then have "io @ [(x, y')] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" unfolding test_suite_to_io.simps by blast then show "False" using ‹io @ [(x, y')] ∉ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)› by blast qed qed consider (a) "io @ [(x, y)] ∈ (⋃(q, P)∈prs. L P)" | (b) "io @ [(x, y)] ∈ (⋃ {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q})" | (c) "io @ [(x, y)] ∈ (⋃ {(λio_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A |p pt q A. ∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')})" using ‹io @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)› unfolding test_suite_to_io.simps by blast then show "False" proof cases case a then show ?thesis using preamble_prop by blast next case b then show ?thesis using traversal_path_prop by blast next case c then obtain pP pt q A P q' t1 t2 where "io @ [(x, y)] ∈ (λio_atc. p_io pP @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A" and "(q, P) ∈ prs" and "path P (FSM.initial P) pP" and "target (FSM.initial P) pP = q" and "pt ∈ tps q" and "q' ∈ rd_targets (q, pt)" and "(A, t1, t2) ∈ atcs (target q pt, q')" by blast obtain ioA where "io @ [(x, y)] = p_io pP @ p_io pt @ ioA" using ‹io @ [(x, y)] ∈ (λio_atc. p_io pP @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A› unfolding prefixes_set by blast show "False" proof (cases ioA rule: rev_cases) case Nil then have "io @ [(x, y)] = p_io pP @ p_io pt" using ‹io @ [(x, y)] = p_io pP @ p_io pt @ ioA› by simp then have "io @ [(x, y)] ∈ (@) (p_io pP) ` set (prefixes (p_io pt))" unfolding prefixes_set by blast show ?thesis using traversal_path_prop[OF ‹io @ [(x, y)] ∈ (@) (p_io pP) ` set (prefixes (p_io pt))› ‹(q, P) ∈ prs› ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› ‹pt ∈ tps q›] by assumption next case (snoc ioAI xy) then have "xy = (x,y)" and "io = p_io pP @ p_io pt @ ioAI" using ‹io @ [(x, y)] = p_io pP @ p_io pt @ ioA› by simp+ then have "p_io pP @ p_io pt @ ioAI @ [(x,y)] ∈ (λio_atc. p_io pP @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A" using ‹io @ [(x, y)] ∈ (λio_atc. p_io pP @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A› by auto then have "ioAI @ [(x,y)] ∈ atc_to_io_set (FSM.from_FSM M (target q pt)) A" by auto have "p_io pP @ p_io pt ∈ L M'" using ‹io @ [(x,y')] ∈ L M'› language_prefix[of "p_io pP @ p_io pt" "ioAI @ [(x, y')]" M' "initial M'"] unfolding ‹io = p_io pP @ p_io pt @ ioAI› by simp then obtain pt' where "path M' (initial M') pt'" and "p_io pt' = p_io pP @ p_io pt" by auto then have "target (initial M') pt' ∈ io_targets M' (p_io pP @ p_io pt) (FSM.initial M')" by fastforce have "pass_separator_ATC M' A (target (FSM.initial M') pt') t2" using pass3[OF ‹(q, P) ∈ prs› ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› ‹pt ∈ tps q› ‹p_io pP @ p_io pt ∈ L M'› ‹q' ∈ rd_targets (q, pt)› ‹(A, t1, t2) ∈ atcs (target q pt, q')› ‹target (initial M') pt' ∈ io_targets M' (p_io pP @ p_io pt) (FSM.initial M')›] by assumption have "is_separator M (target q pt) q' A t1 t2" using t3[OF ‹(A, t1, t2) ∈ atcs (target q pt, q')›] by blast have "is_submachine P M" using t2[OF ‹(q, P) ∈ prs›] unfolding is_preamble_def by blast then have "initial P = initial M" by auto have "path M (initial M) pP" using submachine_path[OF ‹is_submachine P M› ‹path P (initial P) pP›] unfolding ‹initial P = initial M› by assumption have "target (initial M) pP = q" using ‹target (initial P) pP = q› unfolding ‹initial P = initial M› by assumption have "q ∈ states M" using is_preamble_is_state[OF t2[OF ‹(q, P) ∈ prs›]] by assumption have "q ∈ fst ` prs" using ‹(q, P) ∈ prs› by force obtain pT' d' where "(pt @ pT', d') ∈ m_traversal_paths_with_witness M q repetition_sets m" using t6[OF ‹q ∈ fst ` prs›] ‹pt ∈ tps q› by blast then have "path M q (pt @ pT')" and "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (pt @ pT'))) repetition_sets = Some d'" and "⋀ p' p''. (pt @ pT') = p' @ p'' ⟹ p'' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repetition_sets = None" using m_traversal_paths_with_witness_set[OF t5 t8 ‹q ∈ states M›, of m] by blast+ then have "path M q pt" by auto have "target (initial M') pt' ∈ states M'" using ‹target (initial M') pt' ∈ io_targets M' (p_io pP @ p_io pt) (FSM.initial M')› io_targets_states using subset_iff by fastforce have "pass_io_set (FSM.from_FSM M' (target (FSM.initial M') pt')) (atc_to_io_set (FSM.from_FSM M (target q pt)) A)" using pass_io_set_from_pass_separator[OF ‹is_separator M (target q pt) q' A t1 t2› ‹pass_separator_ATC M' A (target (FSM.initial M') pt') t2› ‹observable M› ‹observable M'› path_target_is_state[OF ‹path M q pt›] ‹target (FSM.initial M') pt' ∈ FSM.states M'› ‹inputs M' = inputs M›] by assumption moreover note ‹ioAI @ [(x,y)] ∈ atc_to_io_set (FSM.from_FSM M (target q pt)) A› moreover have "ioAI @ [(x, y')] ∈ L (FSM.from_FSM M' (target (FSM.initial M') pt'))" using ‹io @ [(x,y')] ∈ L M'› unfolding ‹io = p_io pP @ p_io pt @ ioAI› by (metis (no_types, lifting) ‹target (FSM.initial M') pt' ∈ FSM.states M'› ‹target (FSM.initial M') pt' ∈ io_targets M' (p_io pP @ p_io pt) (FSM.initial M')› append_assoc assms(3) from_FSM_language observable_io_targets_language) ultimately have "ioAI @ [(x,y')] ∈ atc_to_io_set (FSM.from_FSM M (target q pt)) A" unfolding pass_io_set_def by blast (* subsets of test_suite_to_io *) define tmp where tmp_def : "tmp = (⋃ {(λio_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A |p pt q A. ∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')})" define tmp2 where tmp2_def : "tmp2 = ⋃ {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q}" have "∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) pP ∧ target (FSM.initial P) pP = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')" using ‹(q, P) ∈ prs› ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› ‹pt ∈ tps q› ‹q' ∈ rd_targets (q, pt)› ‹(A, t1, t2) ∈ atcs (target q pt, q')› by blast then have "(λio_atc. p_io pP @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A ⊆ tmp" unfolding tmp_def by blast then have "(λio_atc. p_io pP @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A ⊆ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" unfolding test_suite_to_io.simps tmp_def[symmetric] tmp2_def[symmetric] by blast moreover have "(p_io pP @ p_io pt @ (ioAI @ [(x, y')])) ∈ (λio_atc. p_io pP @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A" using ‹ioAI @ [(x, y')] ∈ atc_to_io_set (FSM.from_FSM M (target q pt)) A› by auto ultimately have "(p_io pP @ p_io pt @ (ioAI @ [(x, y')])) ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" by blast then have "io @ [(x, y')] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" unfolding ‹io = p_io pP @ p_io pt @ ioAI› by auto then show "False" using ‹io @ [(x, y')] ∉ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)› by blast qed qed qed qed ultimately show ?thesis unfolding ‹T = Test_Suite prs tps rd_targets atcs› by blast qed lemma test_suite_to_io_finite : assumes "implies_completeness T M m" and "is_finite_test_suite T" shows "finite (test_suite_to_io M T)" proof - obtain prs tps rd_targets atcs where "T = Test_Suite prs tps rd_targets atcs" by (meson test_suite.exhaust) then obtain repetition_sets where repetition_sets_def: "implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets" using assms(1) unfolding implies_completeness_def by blast then have "implies_completeness (Test_Suite prs tps rd_targets atcs) M m" unfolding implies_completeness_def by blast then have test_suite_language_prop: "test_suite_to_io M (Test_Suite prs tps rd_targets atcs) ⊆ L M" using test_suite_to_io_language by blast have f1: "(finite prs)" and f2: "⋀ q p . q ∈ fst ` prs ⟹ finite (rd_targets (q,p))" and f3: "⋀ q q' . finite (atcs (q,q'))" using assms(2) unfolding ‹T = Test_Suite prs tps rd_targets atcs› is_finite_test_suite.simps by blast+ have t1: "(initial M, initial_preamble M) ∈ prs" using implies_completeness_for_repetition_sets_simps(1)[OF repetition_sets_def] by assumption have t2: "⋀ q P. (q, P) ∈ prs ⟹ is_preamble P M q" using implies_completeness_for_repetition_sets_simps(2)[OF repetition_sets_def] by blast have t3: "⋀ q1 q2 A d1 d2. (A, d1, d2) ∈ atcs (q1, q2) ⟹ (A, d2, d1) ∈ atcs (q2, q1) ∧ is_separator M q1 q2 A d1 d2" using implies_completeness_for_repetition_sets_simps(3)[OF repetition_sets_def] by assumption have t5: "⋀q. q ∈ FSM.states M ⟹ (∃d∈set repetition_sets. q ∈ fst d)" using implies_completeness_for_repetition_sets_simps(4)[OF repetition_sets_def] by assumption have t6: "⋀ q. q ∈ fst ` prs ⟹ tps q ⊆ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m} ∧ fst ` (m_traversal_paths_with_witness M q repetition_sets m) ⊆ tps q" using implies_completeness_for_repetition_sets_simps(7)[OF repetition_sets_def] by assumption have t7: "⋀ d. d ∈ set repetition_sets ⟹ fst d ⊆ FSM.states M" and t8: "⋀ d. d ∈ set repetition_sets ⟹ snd d ⊆ fst d" and t8': "⋀ d. d ∈ set repetition_sets ⟹ snd d = fst d ∩ fst ` prs" and t9: "⋀ d q1 q2. d ∈ set repetition_sets ⟹ q1 ∈ fst d ⟹ q2 ∈ fst d ⟹ q1 ≠ q2 ⟹ atcs (q1, q2) ≠ {}" using implies_completeness_for_repetition_sets_simps(5,6)[OF repetition_sets_def] by blast+ have f4: "⋀ q . q ∈ fst ` prs ⟹ finite (tps q)" proof - fix q assume "q ∈ fst ` prs" then have "tps q ⊆ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m}" using t6 by blast moreover have "{p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m} ⊆ (⋃ p2 ∈ fst ` m_traversal_paths_with_witness M q repetition_sets m . set (prefixes p2))" proof fix p1 assume "p1 ∈ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m}" then obtain p2 d where "(p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m" by blast then have "p1@p2 ∈ fst ` m_traversal_paths_with_witness M q repetition_sets m" by force moreover have "p1 ∈ set (prefixes (p1@p2))" unfolding prefixes_set by blast ultimately show "p1 ∈ (⋃ p2 ∈ fst ` m_traversal_paths_with_witness M q repetition_sets m . set (prefixes p2))" by blast qed ultimately have "tps q ⊆ (⋃ p2 ∈ fst ` m_traversal_paths_with_witness M q repetition_sets m . set (prefixes p2))" by simp moreover have "finite (⋃ p2 ∈ fst ` m_traversal_paths_with_witness M q repetition_sets m . set (prefixes p2))" proof - have "finite (fst ` m_traversal_paths_with_witness M q repetition_sets m)" using m_traversal_paths_with_witness_finite[of M q repetition_sets m] by auto moreover have "⋀ p2 . finite (set (prefixes p2))" by auto ultimately show ?thesis by blast qed ultimately show "finite (tps q)" using finite_subset by blast qed then have f4' : "⋀ q P . (q,P) ∈ prs ⟹ finite (tps q)" by force define T1 where T1_def : "T1 = (⋃(q, P)∈prs. L P)" define T2 where T2_def : "T2 = ⋃{(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q}" define T3 where T3_def : "T3 = ⋃ {(λio_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A |p pt q A. ∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')}" have "test_suite_to_io M T = T1 ∪ T2 ∪ T3" unfolding ‹T = Test_Suite prs tps rd_targets atcs› test_suite_to_io.simps T1_def T2_def T3_def by simp moreover have "finite T1" proof - have "⋀ q P . (q, P)∈prs ⟹ finite (L P)" proof - fix q P assume "(q, P)∈prs" have "acyclic P" using t2[OF ‹(q, P)∈prs›] unfolding is_preamble_def by blast then show "finite (L P)" using acyclic_alt_def by blast qed then show ?thesis using f1 unfolding T1_def by auto qed moreover have "finite T2" proof - have *: "T2 = (⋃ (p,pt) ∈ {(p,pt) | p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q} . ((@) (p_io p) ` set (prefixes (p_io pt))))" unfolding T2_def by auto have "⋀ p pt . finite ((@) (p_io p) ` set (prefixes (p_io pt)))" by auto moreover have "finite {(p,pt) | p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q}" proof - have "{(p,pt) | p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q} ⊆ (⋃ (q,P) ∈ prs . {p . path P (initial P) p} × (tps q))" by auto moreover have "finite (⋃ (q,P) ∈ prs . {p . path P (initial P) p} × (tps q))" proof - note ‹finite prs› moreover have "⋀ q P . (q,P) ∈ prs ⟹ finite ({p . path P (initial P) p} × (tps q))" proof - fix q P assume "(q,P) ∈ prs" have "acyclic P" using t2[OF ‹(q, P)∈prs›] unfolding is_preamble_def by blast then have "finite {p . path P (initial P) p}" using acyclic_paths_finite[of P "initial P"] unfolding acyclic.simps by (metis (no_types, lifting) Collect_cong) then show "finite ({p . path P (initial P) p} × (tps q))" using f4'[OF ‹(q,P) ∈ prs›] by simp qed ultimately show ?thesis by force qed ultimately show ?thesis by (meson rev_finite_subset) qed ultimately show ?thesis unfolding * by auto qed moreover have "finite T3" proof - have scheme: "⋀ f P . (⋃ {f a b c d | a b c d . P a b c d}) = (⋃ (a,b,c,d) ∈ {(a,b,c,d) | a b c d . P a b c d} . f a b c d)" by blast have *: "T3 = (⋃ (p,pt,q,A) ∈ {(p, pt, q, A) | p pt q A . ∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')} . (λio_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A)" unfolding T3_def scheme by blast have "{(p, pt, q, A) | p pt q A . ∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')} ⊆ (⋃ (q,P) ∈ prs . ⋃ pt ∈ tps q . ⋃ q' ∈ rd_targets (q, pt) . (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A}))" by blast moreover have "finite (⋃ (q,P) ∈ prs . ⋃ pt ∈ tps q . ⋃ q' ∈ rd_targets (q, pt) . (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A}))" proof - note ‹finite prs› moreover have "⋀ q P . (q,P) ∈ prs ⟹ finite (⋃ pt ∈ tps q . ⋃ q' ∈ rd_targets (q, pt) . (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A}))" proof - fix q P assume "(q,P) ∈ prs" then have "q ∈ fst ` prs" by force have "finite (tps q)" using f4'[OF ‹(q,P) ∈ prs›] by assumption moreover have "⋀ pt . pt ∈ tps q ⟹ finite (⋃ q' ∈ rd_targets (q, pt) . (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A}))" proof - fix pt assume "pt ∈ tps q" have "finite (rd_targets (q,pt))" using f2[OF ‹q ∈ fst ` prs›] by blast moreover have "⋀ q' . q' ∈ rd_targets (q, pt) ⟹ finite (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A})" proof - fix q' assume "q' ∈ rd_targets (q, pt)" have "finite (atcs (target q pt, q'))" using f3 by blast moreover have "finite {p . path P (initial P) p}" proof - have "acyclic P" using t2[OF ‹(q, P)∈prs›] unfolding is_preamble_def by blast then show ?thesis using acyclic_paths_finite[of P "initial P"] unfolding acyclic.simps by (metis (no_types, lifting) Collect_cong) qed ultimately show "finite (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A})" by force qed ultimately show "finite (⋃ q' ∈ rd_targets (q, pt) . (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A}))" by force qed ultimately show "finite (⋃ pt ∈ tps q . ⋃ q' ∈ rd_targets (q, pt) . (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A}))" by force qed ultimately show ?thesis by force qed ultimately have "finite {(p, pt, q, A) | p pt q A . ∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')}" by (meson rev_finite_subset) moreover have "⋀ p pt q A . (p,pt,q,A) ∈ {(p, pt, q, A) | p pt q A . ∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt