section ‹Adaptive Test Cases› text ‹An ATC is a single input, acyclic, observable FSM, which is equivalent to a tree whose non-leaf states are labeled with inputs and whose edges are labeled with outputs.› theory Adaptive_Test_Case imports State_Separator begin definition is_ATC :: "('a,'b,'c) fsm ⇒ bool" where "is_ATC M = (single_input M ∧ acyclic M ∧ observable M)" lemma is_ATC_from : assumes "t ∈ transitions A" and "t_source t ∈ reachable_states A" and "is_ATC A" shows "is_ATC (from_FSM A (t_target t))" using from_FSM_single_input[of A] from_FSM_acyclic[OF reachable_states_next[OF assms(2,1)]] from_FSM_observable[of A] assms(3) unfolding is_ATC_def by fast subsection ‹Applying Adaptive Test Cases› (* FSM M passes ATC A if and only if the parallel execution of M and A does not visit a fail_state in A and M produces no output not allowed in A *) fun pass_ATC' :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ 'd set ⇒ nat ⇒ bool" where "pass_ATC' M A fail_states 0 = (¬ (initial A ∈ fail_states))" | "pass_ATC' M A fail_states (Suc k) = ((¬ (initial A ∈ fail_states)) ∧ (∀ x ∈ inputs A . h A (initial A,x) ≠ {} ⟶ (∀ (yM,qM) ∈ h M (initial M,x) . ∃ (yA,qA) ∈ h A (initial A,x) . yM = yA ∧ pass_ATC' (from_FSM M qM) (from_FSM A qA) fail_states k)))" (* Applies pass_ATC' for a depth of at most (size A) (i.e., an upper bound on the length of paths in A) *) fun pass_ATC :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ 'd set ⇒ bool" where "pass_ATC M A fail_states = pass_ATC' M A fail_states (size A)" lemma pass_ATC'_initial : assumes "pass_ATC' M A FS k" shows "initial A ∉ FS" using assms by (cases k; auto) lemma pass_ATC'_io : assumes "pass_ATC' M A FS k" and "is_ATC A" and "observable M" and "(inputs A) ⊆ (inputs M)" and "io@[ioA] ∈ L A" and "io@[ioM] ∈ L M" and "fst ioA = fst ioM" and "length (io@[ioA]) ≤ k" shows "io@[ioM] ∈ L A" and "io_targets A (io@[ioM]) (initial A) ∩ FS = {}" proof - have "io@[ioM] ∈ L A ∧ io_targets A (io@[ioM]) (initial A) ∩ FS = {}" using assms proof (induction k arbitrary: io A M) case 0 then show ?case by auto next case (Suc k) then show ?case proof (cases io) case Nil obtain tA where "tA ∈ transitions A" and "t_source tA = initial A" and "t_input tA = fst ioA" and "t_output tA = snd ioA" using Nil ‹io@[ioA] ∈ L A› by auto then have "fst ioA ∈ (inputs A)" using fsm_transition_input by fastforce have "(t_output tA,t_target tA) ∈ h A (initial A,t_input tA)" using ‹tA ∈ transitions A› ‹t_source tA = initial A› unfolding h_simps by (metis (no_types, lifting) case_prodI mem_Collect_eq prod.collapse) then have "h A (initial A,fst ioA) ≠ {}" unfolding ‹t_input tA = fst ioA› by blast then have *: "⋀ yM qM . (yM,qM) ∈ h M (initial M,fst ioA) ⟹ (∃ (yA,qA) ∈ h A (initial A,fst ioA) . yM = yA ∧ pass_ATC' (from_FSM M qM) (from_FSM A qA) FS k)" using Suc.prems(1) pass_ATC'_initial[OF Suc.prems(1)] unfolding pass_ATC'.simps using ‹fst ioA ∈ FSM.inputs A› by auto obtain tM where "tM ∈ transitions M" and "t_source tM = initial M" and "t_input tM = fst ioA" and "t_output tM = snd ioM" using Nil ‹io@[ioM] ∈ L M› ‹fst ioA = fst ioM› by auto have "(t_output tM,t_target tM) ∈ h M (initial M,fst ioA)" using ‹tM ∈ transitions M› ‹t_source tM = initial M› ‹t_input tM = fst ioA› unfolding h_simps by (metis (mono_tags, lifting) case_prodI mem_Collect_eq prod.collapse) obtain tA' where "tA' ∈ transitions A" and "t_source tA' = initial A" and "t_input tA' = fst ioA" and "t_output tA' = snd ioM" and "pass_ATC' (from_FSM M (t_target tM)) (from_FSM A (t_target tA')) FS k" using *[OF ‹(t_output tM,t_target tM) ∈ h M (initial M,fst ioA)›] unfolding h.simps ‹t_output tM = snd ioM› by fastforce then have "path A (initial A) [tA']" using single_transition_path[OF ‹tA' ∈ transitions A›] by auto moreover have "p_io [tA'] = [ioM]" using ‹t_input tA' = fst ioA› ‹t_output tA' = snd ioM› unfolding ‹fst ioA = fst ioM› by auto ultimately have "[ioM] ∈ LS A (initial A)" unfolding LS.simps by (metis (mono_tags, lifting) mem_Collect_eq) then have "io @ [ioM] ∈ LS A (initial A)" using Nil by auto have "target (initial A) [tA'] = t_target tA'" by auto then have "t_target tA' ∈ io_targets A [ioM] (initial A)" unfolding io_targets.simps using ‹path A (initial A) [tA']› ‹p_io [tA'] = [ioM]› by (metis (mono_tags, lifting) mem_Collect_eq) then have "io_targets A (io @ [ioM]) (initial A) = {t_target tA'}" using observable_io_targets[OF _ ‹io @ [ioM] ∈ LS A (initial A)›] ‹is_ATC A› Nil unfolding is_ATC_def by (metis append_self_conv2 singletonD) moreover have "t_target tA' ∉ FS" using pass_ATC'_initial[OF ‹pass_ATC' (from_FSM M (t_target tM)) (from_FSM A (t_target tA')) FS k›] unfolding from_FSM_simps(1)[OF fsm_transition_target[OF ‹tA' ∈ transitions A›]] by assumption ultimately have "io_targets A (io @ [ioM]) (initial A) ∩ FS = {}" by auto then show ?thesis using ‹io @ [ioM] ∈ LS A (initial A)› by auto next case (Cons io' io'') have "[io'] ∈ L A" using Cons ‹io@[ioA] ∈ L A› by (metis append.left_neutral append_Cons language_prefix) then obtain tA where "tA ∈ transitions A" and "t_source tA = initial A" and "t_input tA = fst io'" and "t_output tA = snd io'" by auto then have "fst io' ∈ (inputs A)" using fsm_transition_input by metis have "(t_output tA,t_target tA) ∈ h A (initial A,t_input tA)" using ‹tA ∈ transitions A› ‹t_source tA = initial A› unfolding h_simps by (metis (no_types, lifting) case_prodI mem_Collect_eq prod.collapse) then have "h A (initial A,fst io') ≠ {}" unfolding ‹t_input tA = fst io'› by blast then have *: "⋀ yM qM . (yM,qM) ∈ h M (initial M,fst io') ⟹ (∃ (yA,qA) ∈ h A (initial A,fst io') . yM = yA ∧ pass_ATC' (from_FSM M qM) (from_FSM A qA) FS k)" using Suc.prems(1) pass_ATC'_initial[OF Suc.prems(1)] unfolding pass_ATC'.simps using ‹fst io' ∈ FSM.inputs A› by auto obtain tM where "tM ∈ transitions M" and "t_source tM = initial M" and "t_input tM = fst io'" and "t_output tM = snd io'" using Cons ‹io@[ioM] ∈ L M› ‹fst ioA = fst ioM› by auto have "(t_output tM,t_target tM) ∈ h M (initial M,fst io')" using ‹tM ∈ transitions M› ‹t_source tM = initial M› ‹t_input tM = fst io'› unfolding h_simps by (metis (mono_tags, lifting) case_prodI mem_Collect_eq prod.collapse) obtain tA' where "tA' ∈ transitions A" and "t_source tA' = initial A" and "t_input tA' = fst io'" and "t_output tA' = snd io'" and "pass_ATC' (from_FSM M (t_target tM)) (from_FSM A (t_target tA')) FS k" using *[OF ‹(t_output tM,t_target tM) ∈ h M (initial M,fst io')›] unfolding h.simps ‹t_output tM = snd io'› by fastforce then have "tA = tA'" using ‹is_ATC A› unfolding is_ATC_def observable.simps by (metis ‹tA ∈ transitions A› ‹t_input tA = fst io'› ‹t_output tA = snd io'› ‹t_source tA = initial A› prod.collapse) then have "pass_ATC' (from_FSM M (t_target tM)) (from_FSM A (t_target tA)) FS k" using ‹pass_ATC' (from_FSM M (t_target tM)) (from_FSM A (t_target tA')) FS k› by auto have "(inputs (from_FSM A (t_target tA))) ⊆ (inputs (from_FSM M (t_target tM)))" using Suc.prems(4) unfolding from_FSM_simps(2)[OF fsm_transition_target[OF ‹tM ∈ transitions M›]] from_FSM_simps(2)[OF fsm_transition_target[OF ‹tA ∈ transitions A›]] by assumption have "length (io'' @ [ioA]) ≤ k" using Cons ‹length (io @ [ioA]) ≤ Suc k› by auto have "(io' # (io''@[ioA])) ∈ LS A (t_source tA)" using ‹t_source tA = initial A› ‹io@[ioA] ∈ L A› Cons by auto have "io'' @ [ioA] ∈ LS (from_FSM A (t_target tA)) (initial (from_FSM A (t_target tA)))" using observable_language_next[OF ‹(io' # (io''@[ioA])) ∈ LS A (t_source tA)›] ‹is_ATC A› ‹tA ∈ transitions A› ‹t_input tA = fst io'› ‹t_output tA = snd io'› using is_ATC_def by blast have "(io' # (io''@[ioM])) ∈ LS M (t_source tM)" using ‹t_source tM = initial M› ‹io@[ioM] ∈ L M› Cons by auto have "io'' @ [ioM] ∈ LS (from_FSM M (t_target tM)) (initial (from_FSM M (t_target tM)))" using observable_language_next[OF ‹(io' # (io''@[ioM])) ∈ LS M (t_source tM)›] ‹observable M› ‹tM ∈ transitions M› ‹t_input tM = fst io'› ‹t_output tM = snd io'› by blast have "observable (from_FSM M (t_target tM))" using from_FSM_observable[OF ‹observable M›] by blast have "is_ATC (FSM.from_FSM A (t_target tA))" using is_ATC_from[OF ‹tA ∈ transitions A› _ ‹is_ATC A›] reachable_states_initial unfolding ‹t_source tA = initial A› by blast have "io'' @ [ioM] ∈ LS (from_FSM A (t_target tA)) (initial (from_FSM A (t_target tA)))" and "io_targets (from_FSM A (t_target tA)) (io'' @ [ioM]) (initial (from_FSM A (t_target tA))) ∩ FS = {}" using Suc.IH[OF ‹pass_ATC' (from_FSM M (t_target tM)) (from_FSM A (t_target tA)) FS k› ‹is_ATC (FSM.from_FSM A (t_target tA))› ‹observable (from_FSM M (t_target tM))› ‹(inputs (from_FSM A (t_target tA))) ⊆ (inputs (from_FSM M (t_target tM)))› ‹io'' @ [ioA] ∈ LS (from_FSM A (t_target tA)) (initial (from_FSM A (t_target tA)))› ‹io'' @ [ioM] ∈ LS (from_FSM M (t_target tM)) (initial (from_FSM M (t_target tM)))› ‹fst ioA = fst ioM› ‹length (io'' @ [ioA]) ≤ k›] by blast+ then obtain pA where "path (from_FSM A (t_target tA)) (initial (from_FSM A (t_target tA))) pA" and "p_io pA = io'' @ [ioM]" by auto have "path A (initial A) (tA#pA)" using ‹path (from_FSM A (t_target tA)) (initial (from_FSM A (t_target tA))) pA› ‹tA ∈ transitions A› by (metis ‹t_source tA = initial A› cons from_FSM_path_initial fsm_transition_target) moreover have "p_io (tA#pA) = io' # io'' @ [ioM]" using ‹t_input tA = fst io'› ‹t_output tA = snd io'› ‹p_io pA = io'' @ [ioM]› by auto ultimately have "io' # io'' @ [ioM] ∈ L A" unfolding LS.simps by (metis (mono_tags, lifting) mem_Collect_eq) then have "io @ [ioM] ∈ L A" using Cons by auto have "observable A" using Suc.prems(2) is_ATC_def by blast have "io_targets A (io @ [ioM]) (FSM.initial A) ∩ FS = {}" proof - have "⋀ p . path A (FSM.initial A) p ⟹ p_io p = (io' # io'') @ [ioM] ⟹ p = tA # (tl p)" using ‹observable A› unfolding observable.simps using ‹tA ∈ transitions A› ‹t_source tA = initial A› ‹t_input tA = fst io'› ‹t_output tA = snd io'› by fastforce have "⋀ q . q ∈ io_targets A (io @ [ioM]) (FSM.initial A) ⟹ q ∈ io_targets (from_FSM A (t_target tA)) (io'' @ [ioM]) (initial (from_FSM A (t_target tA)))" proof - fix q assume "q ∈ io_targets A (io @ [ioM]) (FSM.initial A)" then obtain p where "q = target (FSM.initial A) p" and "path A (FSM.initial A) p" and "p_io p = (io' # io'') @ [ioM]" unfolding io_targets.simps Cons by blast then have "p = tA # (tl p)" using ‹⋀ p . path A (FSM.initial A) p ⟹ p_io p = (io' # io'') @ [ioM] ⟹ p = tA # (tl p)› by blast have "path A (FSM.initial A) (tA#(tl p))" using ‹path A (FSM.initial A) p› ‹p = tA # (tl p)› by simp then have "path (from_FSM A (t_target tA)) (initial (from_FSM A (t_target tA))) (tl p)" by (meson from_FSM_path_initial fsm_transition_target path_cons_elim) moreover have "p_io (tl p) = (io'') @ [ioM]" using ‹p_io p = (io' # io'') @ [ioM]› ‹p = tA # (tl p)› by auto moreover have "q = target (initial (from_FSM A (t_target tA))) (tl p)" using ‹q = target (FSM.initial A) p› ‹p = tA # (tl p)› unfolding target.simps visited_states.simps from_FSM_simps[OF fsm_transition_target[OF ‹tA ∈ transitions A›]] by (cases p; auto) ultimately show "q ∈ io_targets (from_FSM A (t_target tA)) (io'' @ [ioM]) (initial (from_FSM A (t_target tA)))" unfolding io_targets.simps by blast qed moreover have "⋀ q . q ∈ io_targets (from_FSM A (t_target tA)) (io'' @ [ioM]) (initial (from_FSM A (t_target tA))) ⟹ q ∈ io_targets A (io @ [ioM]) (FSM.initial A)" proof - fix q assume "q ∈ io_targets (from_FSM A (t_target tA)) (io'' @ [ioM]) (initial (from_FSM A (t_target tA)))" then obtain p where "q = target (FSM.initial (FSM.from_FSM A (t_target tA))) p" and "path (FSM.from_FSM A (t_target tA)) (FSM.initial (FSM.from_FSM A (t_target tA))) p" and "p_io p = io'' @ [ioM]" unfolding io_targets.simps Cons by blast have "q = target (FSM.initial A) (tA#p)" unfolding ‹q = target (FSM.initial (FSM.from_FSM A (t_target tA))) p› from_FSM_simps[OF fsm_transition_target[OF ‹tA ∈ transitions A›]] by auto moreover have "path A (initial A) (tA#p)" using ‹path (FSM.from_FSM A (t_target tA)) (FSM.initial (FSM.from_FSM A (t_target tA))) p› unfolding from_FSM_path_initial[OF fsm_transition_target[OF ‹tA ∈ transitions A›], symmetric] using ‹tA ∈ transitions A› ‹t_source tA = initial A› cons by fastforce moreover have "p_io (tA#p) = io @ [ioM]" using ‹p_io p = io'' @ [ioM]› ‹t_input tA = fst io'› ‹t_output tA = snd io'› unfolding Cons by simp ultimately show "q ∈ io_targets A (io @ [ioM]) (FSM.initial A)" unfolding io_targets.simps by fastforce qed ultimately show ?thesis using ‹io_targets (from_FSM A (t_target tA)) (io'' @ [ioM]) (initial (from_FSM A (t_target tA))) ∩ FS = {}› by blast qed then show ?thesis using ‹io @ [ioM] ∈ L A› by simp qed qed then show "io@[ioM] ∈ L A" and "io_targets A (io@[ioM]) (initial A) ∩ FS = {}" by simp+ qed lemma pass_ATC_io : assumes "pass_ATC M A FS" and "is_ATC A" and "observable M" and "(inputs A) ⊆ (inputs M)" and "io@[ioA] ∈ L A" and "io@[ioM] ∈ L M" and "fst ioA = fst ioM" shows "io@[ioM] ∈ L A" and "io_targets A (io@[ioM]) (initial A) ∩ FS = {}" proof - have "acyclic A" using ‹is_ATC A› is_ATC_def by blast then have "length (io @ [ioA]) ≤ (size A)" using ‹io@[ioA] ∈ L A› unfolding LS.simps using acyclic_path_length_limit unfolding acyclic.simps by fastforce show "io@[ioM] ∈ L A" and "io_targets A (io@[ioM]) (initial A) ∩ FS = {}" using pass_ATC'_io[OF _ assms(2-7) ‹length (io @ [ioA]) ≤ (size A)›] using assms(1) by simp+ qed lemma pass_ATC_io_explicit_io_tuple : assumes "pass_ATC M A FS" and "is_ATC A" and "observable M" and "(inputs A) ⊆ (inputs M)" and "io@[(x,y)] ∈ L A" and "io@[(x,y')] ∈ L M" shows "io@[(x,y')] ∈ L A" and "io_targets A (io@[(x,y')]) (initial A) ∩ FS = {}" apply (metis pass_ATC_io(1) assms fst_conv) by (metis pass_ATC_io(2) assms fst_conv) lemma pass_ATC_io_fail_fixed_io : assumes "is_ATC A" and "observable M" and "(inputs A) ⊆ (inputs M)" and "io@[ioA] ∈ L A" and "io@[ioM] ∈ L M" and "fst ioA = fst ioM" and "io@[ioM] ∉ L A ∨ io_targets A (io@[ioM]) (initial A) ∩ FS ≠ {}" shows "¬pass_ATC M A FS" proof - consider (a) "io@[ioM] ∉ L A" | (b) "io_targets A (io@[ioM]) (initial A) ∩ FS ≠ {}" using assms(7) by blast then show ?thesis proof (cases) case a then show ?thesis using pass_ATC_io(1)[OF _ assms(1-6)] by blast next case b then show ?thesis using pass_ATC_io(2)[OF _ assms(1-6)] by blast qed qed lemma pass_ATC'_io_fail : assumes "¬pass_ATC' M A FS k " and "is_ATC A" and "observable M" and "(inputs A) ⊆ (inputs M)" shows "initial A ∈ FS ∨ (∃ io ioA ioM . io@[ioA] ∈ L A ∧ io@[ioM] ∈ L M ∧ fst ioA = fst ioM ∧ (io@[ioM] ∉ L A ∨ io_targets A (io@[ioM]) (initial A) ∩ FS ≠ {}))" using assms proof (induction k arbitrary: M A) case 0 then show ?case by auto next case (Suc k) then show ?case proof (cases "initial A ∈ FS") case True then show ?thesis by auto next case False then obtain x where "x ∈ inputs A" and "h A (FSM.initial A, x) ≠ {}" and "¬(∀(yM, qM)∈h M (initial M, x). ∃(yA, qA)∈h A (FSM.initial A, x). yM = yA ∧ pass_ATC' (FSM.from_FSM M qM) (FSM.from_FSM A qA) FS k)" using Suc.prems(1) unfolding pass_ATC'.simps by fastforce obtain tM where "tM ∈ transitions M" and "t_source tM = initial M" and "t_input tM = x" and "¬(∃(yA, qA)∈h A (FSM.initial A, x). t_output tM = yA ∧ pass_ATC' (FSM.from_FSM M (t_target tM)) (FSM.from_FSM A qA) FS k)" using ‹¬(∀(yM, qM)∈h M (initial M, x). ∃(yA, qA)∈h A (FSM.initial A, x). yM = yA ∧ pass_ATC' (FSM.from_FSM M qM) (FSM.from_FSM A qA) FS k)› unfolding h.simps by auto have "¬ (∃ tA . tA ∈ transitions A ∧ t_source tA = initial A ∧ t_input tA = x ∧ t_output tA = t_output tM ∧ pass_ATC' (FSM.from_FSM M (t_target tM)) (FSM.from_FSM A (t_target tA)) FS k)" using ‹¬(∃(yA, qA)∈h A (FSM.initial A, x). t_output tM = yA ∧ pass_ATC' (FSM.from_FSM M (t_target tM)) (FSM.from_FSM A qA) FS k)› unfolding h.simps by force moreover have "∃ tA . tA ∈ transitions A ∧ t_source tA = initial A ∧ t_input tA = x" using ‹h A (FSM.initial A, x) ≠ {}› unfolding h.simps by force ultimately consider (a) "⋀ tA . tA ∈ transitions A ⟹ t_source tA = initial A ⟹ t_input tA = x ⟹ t_output tM ≠ t_output tA" | (b) "∃ tA . tA ∈ transitions A ∧ t_source tA = initial A ∧ t_input tA = x ∧ t_output tA = t_output tM ∧ ¬pass_ATC' (FSM.from_FSM M (t_target tM)) (FSM.from_FSM A (t_target tA)) FS k" by force then show ?thesis proof cases case a then have "[(x,t_output tM)] ∉ L A" unfolding LS.simps by fastforce moreover have "∃ y . [(x,y)] ∈ L A" using ‹h A (FSM.initial A, x) ≠ {}› unfolding h.simps LS.simps proof - obtain pp :: "'d × 'b × 'c × 'd" where f1: "pp ∈ FSM.transitions A ∧ t_source pp = FSM.initial A ∧ t_input pp = x" using ‹∃tA. tA ∈ FSM.transitions A ∧ t_source tA = FSM.initial A ∧ t_input tA = x› by blast then have "path A (FSM.initial A) [pp]" by (metis single_transition_path) then have "(t_input pp, t_output pp) # p_io ([]::('d × 'b × 'c × _) list) ∈ {p_io ps |ps. path A (FSM.initial A) ps}" by force then show "∃c. [(x, c)] ∈ {p_io ps |ps. path A (FSM.initial A) ps}" using f1 by force qed moreover have "[(x,t_output tM)] ∈ L M" unfolding LS.simps using ‹tM ∈ transitions M› ‹t_input tM = x› ‹t_source tM = initial M› proof - have "∃ps. p_io [tM] = p_io ps ∧ path M (FSM.initial M) ps" by (metis (no_types) ‹tM ∈ FSM.transitions M› ‹t_source tM = FSM.initial M› single_transition_path) then show "[(x, t_output tM)] ∈ {p_io ps |ps. path M (FSM.initial M) ps}" by (simp add: ‹t_input tM = x›) qed ultimately have "(∃io ioA ioM. io @ [ioA] ∈ L A ∧ io @ [ioM] ∈ L M ∧ fst ioA = fst ioM ∧ (io @ [ioM] ∉ L A))" by (metis append_self_conv2 fst_conv) then show ?thesis by blast next case b then obtain t' where "t' ∈ transitions A" and "t_source t' = initial A" and "t_input t' = x" and "t_output t' = t_output tM" and "¬pass_ATC' (FSM.from_FSM M (t_target tM)) (FSM.from_FSM A (t_target t')) FS k" by blast have "is_ATC (FSM.from_FSM A (t_target t'))" using is_ATC_from[OF ‹t' ∈ transitions A› _ ‹is_ATC A›] reachable_states_initial unfolding ‹t_source t' = initial A› by blast have "(inputs (from_FSM A (t_target t'))) ⊆ (inputs (from_FSM M (t_target tM)))" by (simp add: Suc.prems(4) ‹t' ∈ FSM.transitions A› ‹tM ∈ FSM.transitions M› fsm_transition_target) let ?ioM = "(x,t_output tM)" let ?ioA = "(x,t_output t')" consider (b1) "initial (from_FSM A (t_target t')) ∈ FS" | (b2) "(∃io ioA ioM. io @ [ioA] ∈ LS (from_FSM A (t_target t')) (initial (from_FSM A (t_target t'))) ∧ io @ [ioM] ∈ LS (from_FSM M (t_target tM)) (initial (from_FSM M (t_target tM))) ∧ fst ioA = fst ioM ∧ (io @ [ioM] ∉ LS (from_FSM A (t_target t')) (initial (from_FSM A (t_target t'))) ∨ io_targets (from_FSM A (t_target t')) (io @ [ioM]) (initial (from_FSM A (t_target t'))) ∩ FS ≠ {}))" using Suc.IH[OF ‹¬pass_ATC' (FSM.from_FSM M (t_target tM)) (FSM.from_FSM A (t_target t')) FS k› ‹is_ATC (FSM.from_FSM A (t_target t'))› from_FSM_observable[OF ‹observable M›] ‹(inputs (from_FSM A (t_target t'))) ⊆ (inputs (from_FSM M (t_target tM)))›] by blast then show ?thesis proof cases case b1 (* analogous to case a *) have "[?ioA] ∈ L A" unfolding LS.simps proof - have "∃ps. [(x, t_output t')] = p_io ps ∧ path A (t_source t') ps" using ‹t' ∈ FSM.transitions A› ‹t_input t' = x› by force then show "[(x, t_output t')] ∈ {p_io ps |ps. path A (FSM.initial A) ps}" by (simp add: ‹t_source t' = FSM.initial A›) qed have "[?ioM] ∈ L M" unfolding LS.simps proof - have "path M (FSM.initial M) [tM]" by (metis ‹tM ∈ FSM.transitions M› ‹t_source tM = FSM.initial M› single_transition_path) then have "∃ps. [(x, t_output tM)] = p_io ps ∧ path M (FSM.initial M) ps" using ‹t_input tM = x› by force then show "[(x, t_output tM)] ∈ {p_io ps |ps. path M (FSM.initial M) ps}" by simp qed have "p_io [t'] = [(x, t_output tM)]" using ‹t_input t' = x› ‹t_output t' = t_output tM› by auto moreover have "target (initial A) [t'] = t_target t'" using ‹t_source t' = initial A› by auto ultimately have "t_target t' ∈ io_targets A [(x,t_output tM)] (initial A)" unfolding io_targets.simps using single_transition_path[OF ‹t' ∈ transitions A›] by (metis (mono_tags, lifting) ‹t_source t' = initial A› mem_Collect_eq) then have "initial (from_FSM A (t_target t')) ∈ io_targets A [(x,t_output tM)] (initial A)" unfolding io_targets.simps from_FSM_simps[OF fsm_transition_target[OF ‹t' ∈ transitions A›]] by simp then have "io_targets A ([] @ [?ioM]) (initial A) ∩ FS ≠ {}" using b1 by (metis IntI append_Nil empty_iff) then have "∃ io ioA ioM . io@[ioA] ∈ L A ∧ io@[ioM] ∈ L M ∧ fst ioA = fst ioM ∧ io_targets A (io @ [ioM]) (initial A) ∩ FS ≠ {}" using ‹[?ioA] ∈ L A› ‹[?ioM] ∈ L M› by (metis ‹t_output t' = t_output tM› append.left_neutral) then show ?thesis by blast next case b2 (* obtain io ioA ioM and prepend (x,t_output tM) *) then obtain io ioA ioM where "io @ [ioA] ∈ LS (from_FSM A (t_target t')) (initial (from_FSM A (t_target t')))" and "io @ [ioM] ∈ LS (from_FSM M (t_target tM)) (initial (from_FSM M (t_target tM)))" and "fst ioA = fst ioM" and "(io @ [ioM] ∉ LS (from_FSM A (t_target t')) (initial (from_FSM A (t_target t'))) ∨ io_targets (from_FSM A (t_target t')) (io @ [ioM]) (initial (from_FSM A (t_target t'))) ∩ FS ≠ {})" by blast have "observable A" using Suc.prems(2) is_ATC_def by blast have "(?ioM # io) @ [ioA] ∈ L A" using language_state_prepend_transition[OF ‹io @ [ioA] ∈ LS (from_FSM A (t_target t')) (initial (from_FSM A (t_target t')))› ‹t' ∈ transitions A›] using ‹t_input t' = x› ‹t_source t' = initial A› ‹t_output t' = t_output tM› by simp moreover have "(?ioM # io) @ [ioM] ∈ L M" using language_state_prepend_transition[OF ‹io @ [ioM] ∈ L (from_FSM M (t_target tM))› ‹tM ∈ transitions M›] using ‹t_input tM = x› ‹t_source tM = initial M› by simp moreover have "((?ioM # io) @ [ioM] ∉ L A ∨ io_targets A ((?ioM # io) @ [ioM]) (initial A) ∩ FS ≠ {})" proof - consider (f1) "io @ [ioM] ∉ L (from_FSM A (t_target t'))" | (f2) "io_targets (from_FSM A (t_target t')) (io @ [ioM]) (initial (from_FSM A (t_target t'))) ∩ FS ≠ {}" using ‹(io @ [ioM] ∉ LS (from_FSM A (t_target t')) (initial (from_FSM A (t_target t'))) ∨ io_targets (from_FSM A (t_target t')) (io @ [ioM]) (initial (from_FSM A (t_target t'))) ∩ FS ≠ {})› by blast then show ?thesis proof cases case f1 have "p_io [t'] = [(x, t_output tM)]" using ‹t_input t' = x› ‹t_output t' = t_output tM› by auto moreover have "target (initial A) [t'] = t_target t'" using ‹t_source t' = initial A› by auto ultimately have "t_target t' ∈ io_targets A [?ioM] (initial A)" unfolding io_targets.simps using single_transition_path[OF ‹t' ∈ transitions A›] by (metis (mono_tags, lifting) ‹t_source t' = initial A› mem_Collect_eq) show ?thesis using observable_io_targets_language[of "[(x, t_output tM)]" "io@[ioM]" A "initial A" "t_target t'", OF _ ‹observable A› ‹t_target t' ∈ io_targets A [?ioM] (initial A)›] f1 by (metis ‹observable A› ‹t' ∈ FSM.transitions A› ‹t_input t' = x› ‹t_output t' = t_output tM› ‹t_source t' = FSM.initial A› append_Cons fst_conv observable_language_next snd_conv) next case f2 have "io_targets A (p_io [t'] @ io @ [ioM]) (t_source t') = io_targets A ([?ioM] @ io @ [ioM]) (t_source t')" using ‹t_input t' = x› ‹t_output t' = t_output tM› by auto moreover have "io_targets A (io @ [ioM]) (t_target t') = io_targets (from_FSM A (t_target t')) (io @ [ioM]) (initial (from_FSM A (t_target t')))" unfolding io_targets.simps using from_FSM_path_initial[OF fsm_transition_target[OF ‹t' ∈ transitions A›]] by auto ultimately have "io_targets A ([?ioM] @ io @ [ioM]) (t_source t') = io_targets (from_FSM A (t_target t')) (io @ [ioM]) (initial (from_FSM A (t_target t')))" using observable_io_targets_next[OF ‹observable A› ‹t' ∈ transitions A›, of "io @ [ioM]"] by auto then show ?thesis using f2 ‹t_source t' = initial A› by auto qed qed ultimately show ?thesis using ‹fst ioA = fst ioM› by blast qed qed qed qed lemma pass_ATC_io_fail : assumes "¬pass_ATC M A FS" and "is_ATC A" and "observable M" and "(inputs A) ⊆ (inputs M)" shows "initial A ∈ FS ∨ (∃ io ioA ioM . io@[ioA] ∈ L A ∧ io@[ioM] ∈ L M ∧ fst ioA = fst ioM ∧ (io@[ioM] ∉ L A ∨ io_targets A (io@[ioM]) (initial A) ∩ FS ≠ {}))" using pass_ATC'_io_fail[OF _ assms(2-4)] using assms(1) by auto lemma pass_ATC_fail : assumes "is_ATC A" and "observable M" and "(inputs A) ⊆ (inputs M)" and "io@[(x,y)] ∈ L A" and "io@[(x,y')] ∈ L M" and "io@[(x,y')] ∉ L A" shows "¬ pass_ATC M A FS" using assms(6) pass_ATC_io_explicit_io_tuple(1)[OF _ assms(1,2,3,4,5)] by blast lemma pass_ATC_reduction : assumes "L M2 ⊆ L M1" and "is_ATC A" and "observable M1" and "observable M2" and "(inputs A) ⊆ (inputs M1)" and "(inputs M2) = (inputs M1)" and "pass_ATC M1 A FS" shows "pass_ATC M2 A FS" proof (rule ccontr) assume "¬ pass_ATC M2 A FS" have "(inputs A) ⊆ (inputs M2)" using assms(5,6) by blast have "initial A ∉ FS" using ‹pass_ATC M1 A FS› by (cases "size A"; auto) then show "False" using pass_ATC_io_fail[OF ‹¬ pass_ATC M2 A FS› assms(2,4) ‹(inputs A) ⊆ (inputs M2)›] using assms(1) assms(2) assms(3) assms(5) assms(7) pass_ATC_io_fail_fixed_io by blast qed lemma pass_ATC_fail_no_reduction : assumes "is_ATC A" and "observable T" and "observable M" and "(inputs A) ⊆ (inputs M)" and "(inputs T) = (inputs M)" and "pass_ATC M A FS" and "¬pass_ATC T A FS" shows "¬ (L T ⊆ L M)" using pass_ATC_reduction[OF _ assms(1,3,2,4,5,6)] assms(7) by blast subsection ‹State Separators as Adaptive Test Cases› fun pass_separator_ATC :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ 'a ⇒ 'd ⇒ bool" where "pass_separator_ATC M S q1 t2 = pass_ATC (from_FSM M q1) S {t2}" lemma separator_is_ATC : assumes "is_separator M q1 q2 A t1 t2" and "observable M" and "q1 ∈ states M" shows "is_ATC A" unfolding is_ATC_def using is_separator_simps(1,2,3)[OF assms(1)] by blast lemma pass_separator_ATC_from_separator_left : assumes "observable M" and "q1 ∈ states M" and "q2 ∈ states M" and "is_separator M q1 q2 A t1 t2" shows "pass_separator_ATC M A q1 t2" proof (rule ccontr) assume "¬ pass_separator_ATC M A q1 t2" then have "¬ pass_ATC (from_FSM M q1) A {t2}" by auto have "is_ATC A" using separator_is_ATC[OF assms(4,1,2)] by assumption have "initial A ∉ {t2}" using separator_initial(2)[OF assms(4)] by blast then obtain io ioA ioM where "io @ [ioA] ∈ L A" "io @ [ioM] ∈ LS M q1" "fst ioA = fst ioM" "io @ [ioM] ∉ L A ∨ io_targets A (io @ [ioM]) (initial A) ∩ {t2} ≠ {}" using pass_ATC_io_fail[OF ‹¬ pass_ATC (from_FSM M q1) A {t2}› ‹is_ATC A› from_FSM_observable[OF ‹observable M›] ] using is_separator_simps(16)[OF assms(4)] using from_FSM_language[OF ‹q1 ∈ states M›] unfolding from_FSM_simps[OF ‹q1 ∈ states M›] by blast then obtain x ya ym where "io @ [(x,ya)] ∈ L A" "io @ [(x,ym)] ∈ LS M q1" "io @ [(x,ym)] ∉ L A ∨ io_targets A (io @ [(x,ym)]) (initial A) ∩ {t2} ≠ {}" by (metis fst_eqD old.prod.exhaust) have "io @ [(x,ym)] ∈ L A" using is_separator_simps(9)[OF assms(4) ‹io @ [(x,ym)] ∈ LS M q1› ‹io @ [(x,ya)] ∈ L A›] by assumption have "t1 ≠ t2" using is_separator_simps(15)[OF assms(4)] by assumption consider (a) "io @ [(x, ym)] ∈ LS M q1 - LS M q2" | (b) "io @ [(x, ym)] ∈ LS M q1 ∩ LS M q2" using ‹io @ [(x,ym)] ∈ LS M q1› by blast then have "io_targets A (io @ [(x,ym)]) (initial A) ∩ {t2} = {}" proof (cases) case a show ?thesis using separator_language(1)[OF assms(4) ‹io @ [(x,ym)] ∈ L A› a] ‹t1 ≠ t2› by auto next case b show ?thesis using separator_language(3)[OF assms(4) ‹io @ [(x,ym)] ∈ L A› b] ‹t1 ≠ t2› by auto qed then show "False" using ‹io @ [(x,ym)] ∈ L A› using ‹io @ [(x,ym)] ∉ L A ∨ io_targets A (io @ [(x,ym)]) (initial A) ∩ {t2} ≠ {}› by blast qed lemma pass_separator_ATC_from_separator_right : assumes "observable M" and "q1 ∈ states M" and "q2 ∈ states M" and "is_separator M q1 q2 A t1 t2" shows "pass_separator_ATC M A q2 t1" using assms(1-3) is_separator_sym[OF assms(4)] pass_separator_ATC_from_separator_left by metis lemma pass_separator_ATC_path_left : assumes "pass_separator_ATC S A s1 t2" and "observable S" and "observable M" and "s1 ∈ states S" and "q1 ∈ states M" and "q2 ∈ states M" and "is_separator M q1 q2 A t1 t2" and "(inputs S) = (inputs M)" and "q1 ≠ q2" and "path A (initial A) pA" and "path S s1 pS" and "p_io pA = p_io pS" shows "target (initial A) pA ≠ t2" and "∃ pM . path M q1 pM ∧ p_io pM = p_io pA" proof - have "pass_ATC (from_FSM S s1) A {t2}" using ‹pass_separator_ATC S A s1 t2› by auto have "is_ATC A" using separator_is_ATC[OF assms(7,3,5)] by assumption have "observable (from_FSM S s1)" using from_FSM_observable[OF assms(2)] by assumption have "(inputs A) ⊆ (inputs (from_FSM S s1))" using is_separator_simps(16)[OF assms(7)] ‹(inputs S) = (inputs M)› unfolding from_FSM_simps[OF ‹s1 ∈ states S›] by blast have "target (initial A) pA ≠ t2 ∧ (∃ pM . path M q1 pM ∧ p_io pM = p_io pA)" proof (cases pA rule: rev_cases) case Nil then have "target (initial A) pA ≠ t2" using separator_initial(2)[OF assms(7)] by auto moreover have "(∃ pM . path M q1 pM ∧ p_io pM = p_io pA)" unfolding Nil using ‹q1 ∈ states M› by auto ultimately show ?thesis by auto next case (snoc ys y) then have "p_io pA = (p_io ys)@[(t_input y,t_output y)]" by auto then have *: "(p_io ys)@[(t_input y,t_output y)] ∈ L A" using language_state_containment[OF ‹path A (initial A) pA›] by blast then have "p_io pS = (p_io ys)@[(t_input y,t_output y)]" using ‹p_io pA = (p_io ys)@[(t_input y,t_output y)]› ‹p_io pA = p_io pS› by auto then have **: "(p_io ys)@[(t_input y,t_output y)] ∈ L (from_FSM S s1)" using language_state_containment[OF ‹path S s1 pS›] unfolding from_FSM_language[OF ‹s1 ∈ states S›] by blast have "io_targets A ((p_io ys)@[(t_input y,t_output y)]) (initial A) ∩ {t2} = {}" using pass_ATC_io(2)[OF ‹pass_ATC (from_FSM S s1) A {t2}› ‹is_ATC A› ‹observable (from_FSM S s1)› ‹(inputs A) ⊆ (inputs (from_FSM S s1))› * **] unfolding fst_conv by auto then have "target (initial A) pA ≠ t2" using ‹p_io pA = (p_io ys)@[(t_input y,t_output y)]› ‹path A (initial A) pA› unfolding io_targets.simps by blast have "p_io ys @ [(t_input y, t_output y)] ∈ LS M q1" using separator_language(2,4)[OF assms(7) ‹(p_io ys)@[(t_input y,t_output y)] ∈ L A›] using ‹io_targets A ((p_io ys)@[(t_input y,t_output y)]) (initial A) ∩ {t2} = {}› by blast then have "∃ pM . path M q1 pM ∧ p_io pM = p_io pA" using ‹p_io pA = (p_io ys)@[(t_input y,t_output y)]› by auto then show ?thesis using ‹target (initial A) pA ≠ t2› by auto qed then show "target (initial A) pA ≠ t2" and "∃ pM . path M q1 pM ∧ p_io pM = p_io pA" by blast+ qed lemma pass_separator_ATC_path_right : assumes "pass_separator_ATC S A s2 t1" and "observable S" and "observable M" and "s2 ∈ states S" and "q1 ∈ states M" and "q2 ∈ states M" and "is_separator M q1 q2 A t1 t2" and "(inputs S) = (inputs M)" and "q1 ≠ q2" and "path A (initial A) pA" and "path S s2 pS" and "p_io pA = p_io pS" shows "target (initial A) pA ≠ t1" and "∃ pM . path M q2 pM ∧ p_io pM = p_io pA" using pass_separator_ATC_path_left[OF assms(1-4,6,5) is_separator_sym[OF assms(7)] assms(8) _ assms(10-12)] assms(9) by blast+ lemma pass_separator_ATC_fail_no_reduction : assumes "observable S" and "observable M" and "s1 ∈ states S" and "q1 ∈ states M" and "q2 ∈ states M" and "is_separator M q1 q2 A t1 t2" and "(inputs S) = (inputs M)" and "¬pass_separator_ATC S A s1 t2" shows "¬ (LS S s1 ⊆ LS M q1)" proof assume "LS S s1 ⊆ LS M q1" have "is_ATC A" using separator_is_ATC[OF assms(6,2,4)] by assumption have *: "(inputs A) ⊆ (inputs (from_FSM M q1))" using is_separator_simps(16)[OF assms(6)] unfolding is_submachine.simps canonical_separator_simps from_FSM_simps[OF ‹q1 ∈ states M›] by auto have "pass_ATC (from_FSM M q1) A {t2}" using pass_separator_ATC_from_separator_left[OF assms(2,4,5,6)] by auto have "¬ pass_ATC (from_FSM S s1) A {t2}" using ‹¬pass_separator_ATC S A s1 t2› by auto moreover have "pass_ATC (from_FSM S s1) A {t2}" using pass_ATC_reduction[OF _ ‹is_ATC A› from_FSM_observable[OF ‹observable M›] from_FSM_observable[OF ‹observable S›] *] using ‹LS S s1 ⊆ LS M q1› ‹pass_ATC (from_FSM M q1) A {t2}› unfolding from_FSM_language[OF assms(3)] from_FSM_language[OF assms(4)] using ‹L (FSM.from_FSM S s1) = LS S s1› assms(3) assms(4) assms(7) by auto ultimately show "False" by simp qed lemma pass_separator_ATC_pass_left : assumes "observable S" and "observable M" and "s1 ∈ states S" and "q1 ∈ states M" and "q2 ∈ states M" and "is_separator M q1 q2 A t1 t2" and "(inputs S) = (inputs M)" and "path A (initial A) p" and "p_io p ∈ LS S s1" and "q1 ≠ q2" and "pass_separator_ATC S A s1 t2" shows "target (initial A) p ≠ t2" and "target (initial A) p = t1 ∨ (target (initial A) p ≠ t1 ∧ target (initial A) p ≠ t2)" (* useless? *) proof - from ‹p_io p ∈ LS S s1› obtain pS where "path S s1 pS" and "p_io p = p_io pS" by auto then show "target (initial A) p ≠ t2" using pass_separator_ATC_path_left[OF assms(11,1-7,10,8)] by simp obtain pM where "path M q1 pM" and "p_io pM = p_io p" using pass_separator_ATC_path_left[OF assms(11,1-7,10,8) ‹path S s1 pS› ‹p_io p = p_io pS›] by blast then have "p_io p ∈ LS M q1" unfolding LS.simps by force then show "target (initial A) p = t1 ∨ (target (initial A) p ≠ t1 ∧ target (initial A) p ≠ t2)" using separator_path_targets(1,3,4)[OF assms(6,8)] by blast qed lemma pass_separator_ATC_pass_right : assumes "observable S" and "observable M" and "s2 ∈ states S" and "q1 ∈ states M" and "q2 ∈ states M" and "is_separator M q1 q2 A t1 t2" and "(inputs S) = (inputs M)" and "path A (initial A) p" and "p_io p ∈ LS S s2" and "q1 ≠ q2" and "pass_separator_ATC S A s2 t1" shows "target (initial A) p ≠ t1" and "target (initial A) p = t2 ∨ (target (initial A) p ≠ t2 ∧ target (initial A) p ≠ t2)" using pass_separator_ATC_pass_left[OF assms(1,2,3,5,4) is_separator_sym[OF assms(6)] assms(7-9) _ assms(11)] assms(10) by blast+ lemma pass_separator_ATC_completely_specified_left : assumes "observable S" and "observable M" and "s1 ∈ states S" and "q1 ∈ states M" and "q2 ∈ states M" and "is_separator M q1 q2 A t1 t2" and "(inputs S) = (inputs M)" and "q1 ≠ q2" and "pass_separator_ATC S A s1 t2" and "completely_specified S" shows "∃ p . path A (initial A) p ∧ p_io p ∈ LS S s1 ∧ target (initial A) p = t1" and "¬ (∃ p . path A (initial A) p ∧ p_io p ∈ LS S s1 ∧ target (initial A) p = t2)" proof - have p1: "pass_ATC (from_FSM S s1) A {t2}" using assms(9) by auto have p2: "is_ATC A" using separator_is_ATC[OF assms(6,2,4)] by assumption have p3: "observable (from_FSM S s1)" using from_FSM_observable[OF assms(1)] by assumption have p4: "(inputs A) ⊆ (inputs (from_FSM S s1))" using is_separator_simps(16)[OF assms(6)] unfolding from_FSM_simps[OF ‹s1 ∈ states S›] is_submachine.simps canonical_separator_simps assms(7) by auto have "t1 ≠ t2" and "observable A" using is_separator_simps(15,3)[OF assms(6)] by linarith+ have path_ext: "⋀ p . path A (initial A) p ⟹ p_io p ∈ LS S s1 ⟹ (target (initial A) p ≠ t2) ∧ (target (initial A) p = t1 ∨ (∃ t . path A (initial A) (p@[t]) ∧ p_io (p@[t]) ∈ LS S s1))" proof - fix p assume "path A (initial A) p" and "p_io p ∈ LS S s1" consider (a) "target (initial A) p = t1" | (b) "target (initial A) p ≠ t1 ∧ target (initial A) p ≠ t2" using pass_separator_ATC_pass_left(2)[OF assms(1,2,3,4,5,6,7) ‹path A (initial A) p› ‹p_io p ∈ LS S s1› assms(8,9)] by blast then have "target (initial A) p = t1 ∨ (∃ t . path A (initial A) (p@[t]) ∧ p_io (p@[t]) ∈ LS S s1)" proof cases case a then show ?thesis by blast next case b let ?t3 = "target (initial A) p" have "?t3 ≠ t1" and "?t3 ≠ t2" using b by auto moreover have "?t3 ∈ reachable_states A" using ‹path A (initial A) p› reachable_states_intro by blast ultimately have "¬ deadlock_state A ?t3" using is_separator_simps(8)[OF assms(6)] by blast then obtain tt where "tt ∈ transitions A" and "t_source tt = ?t3" by auto then have "path A (initial A) (p@[tt])" using ‹path A (initial A) p› using path_append_transition by metis moreover have "p_io (p@[tt]) = (p_io p)@[(t_input tt, t_output tt)]" by auto ultimately have "(p_io p)@[(t_input tt,t_output tt)] ∈ L A" using language_state_containment[of A "initial A" "p@[tt]"] by metis let ?x = "t_input tt" have "?x ∈ (inputs S)" using ‹tt ∈ transitions A› is_separator_simps(16)[OF assms(6)] assms(7) by auto then obtain y where "(p_io p)@[(?x,y)] ∈ LS S s1" using completely_specified_language_extension[OF ‹completely_specified S› ‹s1 ∈ states S› ‹p_io p ∈ LS S s1› ] by auto then have "p_io p @ [(?x, y)] ∈ LS A (initial A)" using pass_ATC_io_explicit_io_tuple(1)[OF p1 p2 p3 p4 ‹(p_io p)@[(t_input tt,t_output tt)] ∈ L A›] unfolding from_FSM_language[OF ‹s1 ∈ states S›] by auto then obtain tt' where "path A (initial A) (p@[tt'])" and "t_input tt' = ?x" and "t_output tt' = y" using language_path_append_transition_observable[OF _ ‹path A (initial A) p› ‹observable A›] by blast then have "p_io (p @ [tt']) ∈ LS S s1" using ‹(p_io p)@[(?x,y)] ∈ LS S s1› by auto then show ?thesis using ‹path A (initial A) (p@[tt'])› by meson qed moreover have "target (initial A) p ≠ t2" using pass_separator_ATC_pass_left(1)[OF assms(1,2,3,4,5,6,7) ‹path A (initial A) p› ‹p_io p ∈ LS S s1› assms(8,9)] by assumption ultimately show "(target (initial A) p ≠ t2) ∧ (target (initial A) p = t1 ∨ (∃ t . path A (initial A) (p@[t]) ∧ p_io (p@[t]) ∈ LS S s1))" by simp qed (* largest path that satisfies (path A (initial A) p) and (p_io p ∈ LS T t1) cannot be extended further and must thus target (Inr q1) *) have "acyclic A" using ‹is_ATC A› is_ATC_def by auto then have "finite {p . path A (initial A) p}" using acyclic_paths_finite[of A "initial A"] unfolding acyclic.simps by (metis (no_types, lifting) Collect_cong) then have "finite {p . path A (initial A) p ∧ p_io p ∈ LS S s1}" by auto have "[] ∈ {p . path A (initial A) p ∧ p_io p ∈ LS S s1}" using ‹s1 ∈ states S› by auto then have "{p . path A (initial A) p ∧ p_io p ∈ LS S s1} ≠ {}" by blast have scheme: "⋀ S . finite S ⟹ S ≠ {} ⟹ ∃ x ∈ S . ∀ y ∈ S . length y ≤ length x" by (meson leI max_length_elem) obtain p where "p ∈ {p . path A (initial A) p ∧ p_io p ∈ LS S s1}" and "⋀ p' . p' ∈ {p . path A (initial A) p ∧ p_io p ∈ LS S s1} ⟹ length p' ≤ length p" using scheme[OF ‹finite {p . path A (initial A) p ∧ p_io p ∈ LS S s1}› ‹{p . path A (initial A) p ∧ p_io p ∈ LS S s1} ≠ {}›] by blast then have "path A (initial A) p" and "p_io p ∈ LS S s1" and "⋀ p' . path A (initial A) p' ⟹ p_io p' ∈ LS S s1 ⟹ length p' ≤ length p" by blast+ have "target (initial A) p = t1" using path_ext[OF ‹path A (initial A) p› ‹p_io p ∈ LS S s1›] ‹⋀ p' . path A (initial A) p' ⟹ p_io p' ∈ LS S s1 ⟹ length p' ≤ length p› by (metis (no_types, lifting) Suc_n_not_le_n length_append_singleton) then show "∃p. path A (initial A) p ∧ p_io p ∈ LS S s1 ∧ target (initial A) p = t1" using ‹path A (initial A) p› ‹p_io p ∈ LS S s1› by blast show "∄p. path A (initial A) p ∧ p_io p ∈ LS S s1 ∧ target (initial A) p = t2" using path_ext by blast qed lemma pass_separator_ATC_completely_specified_right : assumes "observable S" and "observable M" and "s2 ∈ states S" and "q1 ∈ states M" and "q2 ∈ states M" and "is_separator M q1 q2 A t1 t2" and "(inputs S) = (inputs M)" and "q1 ≠ q2" and "pass_separator_ATC S A s2 t1" and "completely_specified S" shows "∃ p . path A (initial A) p ∧ p_io p ∈ LS S s2 ∧ target (initial A) p = t2" and "¬ (∃ p . path A (initial A) p ∧ p_io p ∈ LS S s2 ∧ target (initial A) p = t1)" using pass_separator_ATC_completely_specified_left[OF assms(1,2,3,5,4) is_separator_sym[OF assms(6)] assms(7) _ assms(9,10)] assms(8) by blast+ lemma pass_separator_ATC_reduction_distinction : assumes "observable M" and "observable S" and "(inputs S) = (inputs M)" and "pass_separator_ATC S A s1 t2" and "pass_separator_ATC S A s2 t1" and "q1 ∈ states M" and "q2 ∈ states M" and "q1 ≠ q2" and "s1 ∈ states S" and "s2 ∈ states S" and "is_separator M q1 q2 A t1 t2" and "completely_specified S" shows "s1 ≠ s2" proof - (* As s1 passes A against t2, t1 must be reached during application, while at the same time t2 is never reached *) have "∃p. path A (initial A) p ∧ p_io p ∈ LS S s1 ∧ target (initial A) p = t1" using pass_separator_ATC_completely_specified_left[OF assms(2,1,9,6,7,11,3,8,4,12)] by blast (* As s2 passes A against t1, t2 must be reached during application, while at the same time t1 is never reached *) moreover have "¬ (∃p. path A (initial A) p ∧ p_io p ∈ LS S s2 ∧ target (initial A) p = t1)" using pass_separator_ATC_completely_specified_right[OF assms(2,1,10,6,7,11,3,8,5,12)] by blast (* Thus it is not possible for (s1 = s2) to hold *) ultimately show "s1 ≠ s2" by blast qed lemma pass_separator_ATC_failure_left : assumes "observable M" and "observable S" and "(inputs S) = (inputs M)" and "is_separator M q1 q2 A t1 t2" and "¬ pass_separator_ATC S A s1 t2" and "q1 ∈ states M" and "q2 ∈ states M" and "q1 ≠ q2" and "s1 ∈ states S" shows "LS S s1 - LS M q1 ≠ {}" proof - have p1: "is_ATC A" using separator_is_ATC[OF assms(4,1,6)] by assumption have p2: "observable (from_FSM S s1)" using from_FSM_observable[OF assms(2)] by assumption have p3: "observable (from_FSM M q1)" using from_FSM_observable[OF assms(1)] by assumption have p4: "(inputs A) ⊆ (inputs (from_FSM M q1))" using is_separator_simps(16)[OF assms(4)] unfolding from_FSM_simps[OF ‹q1 ∈ states M›] is_submachine.simps canonical_separator_simps assms(3) by auto have p5: "(inputs (from_FSM S s1)) = (inputs (from_FSM M q1))" using assms(3,6,9) by simp have p6: "pass_ATC (from_FSM M q1) A {t2}" using pass_separator_ATC_from_separator_left[OF assms(1,6,7,4)] by auto have p7: "¬ pass_ATC (from_FSM S s1) A {t2}" using assms(5) by auto show ?thesis using pass_ATC_fail_no_reduction[OF p1 p2 p3 p4 p5 p6 p7] unfolding from_FSM_language[OF ‹q1 ∈ states M›] from_FSM_language[OF ‹s1 ∈ states S›] by blast qed lemma pass_separator_ATC_failure_right : assumes "observable M" and "observable S" and "(inputs S) = (inputs M)" and "is_separator M q1 q2 A t1 t2" and "¬ pass_separator_ATC S A s2 t1" and "q1 ∈ states M" and "q2 ∈ states M" and "q1 ≠ q2" and "s2 ∈ states S" shows "LS S s2 - LS M q2 ≠ {}" using pass_separator_ATC_failure_left[OF assms(1-3) is_separator_sym[OF assms(4)] assms(5,7,6) _ assms(9)] assms(8) by blast subsection ‹ATCs Represented as Sets of IO Sequences› fun atc_to_io_set :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ ('b × 'c) list set" where "atc_to_io_set M A = L M ∩ L A" lemma atc_to_io_set_code : assumes "acyclic A" shows "atc_to_io_set M A = acyclic_language_intersection M A" using acyclic_language_intersection_completeness[OF assms] unfolding atc_to_io_set.simps by blast lemma pass_io_set_from_pass_separator : assumes "is_separator M q1 q2 A t1 t2" and "pass_separator_ATC S A s1 t2" and "observable M" and "observable S" and "q1 ∈ states M" and "s1 ∈ states S" and "(inputs S) = (inputs M)" shows "pass_io_set (from_FSM S s1) (atc_to_io_set (from_FSM M q1) A)" proof (rule ccontr) assume "¬ pass_io_set (from_FSM S s1) (atc_to_io_set (from_FSM M q1) A)" then obtain io x y y' where "io@[(x,y)] ∈ (atc_to_io_set (from_FSM M q1) A)" and "io@[(x,y')] ∈ L (from_FSM S s1)" and "io@[(x,y')] ∉ (atc_to_io_set (from_FSM M q1) A)" unfolding pass_io_set_def by blast have "is_ATC A" using separator_is_ATC[OF assms(1,3,5)] by assumption then have "acyclic A" unfolding is_ATC_def by auto have "observable (from_FSM S s1)" using from_FSM_observable[OF ‹observable S›] by assumption have "(inputs A) ⊆ (inputs (from_FSM S s1))" by (metis (no_types) assms(1) assms(6) assms(7) from_FSM_simps(2) is_separator_simps(16)) obtain y'' where "io @ [(x, y'')] ∈ LS A (initial A)" using ‹io@[(x,y)] ∈ (atc_to_io_set (from_FSM M q1) A)› unfolding atc_to_io_set.simps by blast have "pass_ATC (from_FSM S s1) A {t2}" using ‹pass_separator_ATC S A s1 t2› by auto then have "io @ [(x, y')] ∈ L A" using pass_ATC_fail[OF ‹is_ATC A› ‹observable (from_FSM S s1)› ‹(inputs A) ⊆ (inputs (from_FSM S s1))› ‹io @ [(x, y'')] ∈ LS A (initial A)› ‹io@[(x,y')] ∈ L (from_FSM S s1)›, of "{t2}" ] by auto have "io_targets A (io @ [(x, y')]) (initial A) ∩ {t2} = {}" using pass_ATC_io(2)[OF ‹pass_ATC (from_FSM S s1) A {t2}› ‹is_ATC A› ‹observable (from_FSM S s1)› ‹(inputs A) ⊆ (inputs (from_FSM S s1))› ‹io @ [(x, y')] ∈ L A› ‹io@[(x,y')] ∈ L (from_FSM S s1)›] unfolding fst_conv by blast then have "io @ [(x, y')] ∈ LS M q1" using separator_language(1,3,4)[OF assms(1) ‹io @ [(x, y')] ∈ L A›] by (metis UnE Un_Diff_cancel ‹io @ [(x, y')] ∈ LS A (initial A)› assms(1) disjoint_insert(2) is_separator_sym separator_language(1) singletonI) then show "False" using ‹io @ [(x, y')] ∈ L A› ‹io@[(x,y')] ∉ (atc_to_io_set (from_FSM M q1) A)› unfolding atc_to_io_set.simps from_FSM_language[OF ‹q1 ∈ states M›] by blast qed lemma separator_language_last_left : assumes "is_separator M q1 q2 A t1 t2" and "completely_specified M" and "q1 ∈ states M" and "io @ [(x, y)] ∈ L A" obtains y'' where "io@[(x,y'')] ∈ L A ∩ LS M q1" proof - obtain p t where "path A (initial A) (p@[t])" and "p_io (p@[t]) = io@[(x,y)]" using language_initial_path_append_transition[OF ‹io @ [(x, y)] ∈ L A›] by blast then have "¬ deadlock_state A (target (initial A) p)" unfolding deadlock_state.simps by fastforce have "path A (initial A) p" using ‹path A (initial A) (p@[t])› by auto have "p_io p ∈ LS M q1" using separator_path_targets(1,2,4)[OF assms(1) ‹path A (initial A) p›] using is_separator_simps(4,5)[OF assms(1)] using ‹¬ deadlock_state A (target (initial A) p)› by fastforce then have "io ∈ LS M q1" using ‹p_io (p@[t]) = io@[(x,y)]› by auto have "x ∈ (inputs A)" using ‹io @ [(x, y)] ∈ L A› language_io(1) by (metis in_set_conv_decomp) then have "x ∈ (inputs M)" using is_separator_simps(16)[OF assms(1)] by blast then obtain y'' where "io@[(x,y'')] ∈ LS M q1" using completely_specified_language_extension[OF ‹completely_specified M› ‹q1 ∈ states M› ‹io ∈ LS M q1›] by blast then have "io@[(x,y'')] ∈ L A ∩ LS M q1" using is_separator_simps(9)[OF assms(1) _ ‹io @ [(x, y)] ∈ L A›] by blast then show ?thesis using that by blast qed lemma separator_language_last_right : assumes "is_separator M q1 q2 A t1 t2" and "completely_specified M" and "q2 ∈ states M" and "io @ [(x, y)] ∈ L A" obtains y'' where "io@[(x,y'')] ∈ L A ∩ LS M q2" using separator_language_last_left[OF is_separator_sym[OF assms(1)] assms(2,3,4)] by blast lemma pass_separator_from_pass_io_set : assumes "is_separator M q1 q2 A t1 t2" and "pass_io_set (from_FSM S s1) (atc_to_io_set (from_FSM M q1) A)" and "observable M" and "observable S" and "q1 ∈ states M" and "s1 ∈ states S" and "(inputs S) = (inputs M)" and "completely_specified M" shows "pass_separator_ATC S A s1 t2" proof (rule ccontr) assume "¬ pass_separator_ATC S A s1 t2" then have "¬ pass_ATC (from_FSM S s1) A {t2}" by auto have "is_ATC A" using separator_is_ATC[OF assms(1,3,5)] by assumption then have "acyclic A" unfolding is_ATC_def by auto have "observable (from_FSM S s1)" using from_FSM_observable[OF ‹observable S›] by assumption have "(inputs A) ⊆ (inputs (from_FSM S s1))" using assms(1) assms(6) assms(7) is_separator_simps(16) by fastforce obtain io x y y' where "io @ [(x,y)] ∈ L A" "io @ [(x,y')] ∈ L (from_FSM S s1)" "(io @ [(x,y')] ∉ L A ∨ io_targets A (io @ [(x,y')]) (initial A) ∩ {t2} ≠ {})" using pass_ATC_io_fail[OF ‹¬ pass_ATC (from_FSM S s1) A {t2}› ‹is_ATC A› ‹observable (from_FSM S s1)› ‹(inputs A) ⊆ (inputs (from_FSM S s1))›] using separator_initial(2)[OF assms(1)] using prod.exhaust fst_conv by (metis empty_iff insert_iff) show "False" proof (cases "io_targets A (io @ [(x,y')]) (initial A) ∩ {t2} ≠ {}") case True then have "io @ [(x,y')] ∈ L A" unfolding io_targets.simps LS.simps by force have "io @ [(x,y')] ∈ LS M q2 - LS M q1" proof - have "t2 ≠ t1" by (metis (full_types) ‹is_separator M q1 q2 A t1 t2› is_separator_simps(15)) then show ?thesis using True separator_language[OF assms(1) ‹io @ [(x,y')] ∈ L A›] by blast qed then have "io @ [(x,y')] ∉ LS M q1" by blast obtain y'' where "io @ [(x, y'')] ∈ LS M q1 ∩ L A" using separator_language_last_left[OF assms(1,8,5) ‹io @ [(x,y)] ∈ L A›] by blast then have "io @ [(x, y')] ∈ LS M q1 ∩ LS A (initial A)" using ‹pass_io_set (from_FSM S s1) (atc_to_io_set (from_FSM M q1) A)› using ‹io @ [(x,y')] ∈ L (from_FSM S s1)› unfolding pass_io_set_def atc_to_io_set.simps from_FSM_language[OF ‹q1 ∈ states M›] by blast then show "False" using ‹io @ [(x,y')] ∉ LS M q1› by blast next case False then have "io @ [(x,y')] ∉ L A" using ‹(io @ [(x,y')] ∉ L A ∨ io_targets A (io @ [(x,y')]) (initial A) ∩ {t2} ≠ {})› by blast obtain y'' where "io @ [(x, y'')] ∈ LS M q1 ∩ L A" using separator_language_last_left[OF assms(1,8,5) ‹io @ [(x,y)] ∈ L A›] by blast then have "io @ [(x, y')] ∈ L A" using ‹pass_io_set (from_FSM S s1) (atc_to_io_set (from_FSM M q1) A)› using ‹io @ [(x,y')] ∈ L (from_FSM S s1)› unfolding pass_io_set_def atc_to_io_set.simps from_FSM_language[OF ‹q1 ∈ states M›] by blast then show "False" using ‹io @ [(x,y')] ∉ L A› by blast qed qed lemma pass_separator_pass_io_set_iff: assumes "is_separator M q1 q2 A t1 t2" and "observable M" and "observable S" and "q1 ∈ states M" and "s1 ∈ states S" and "(inputs S) = (inputs M)" and "completely_specified M" shows "pass_separator_ATC S A s1 t2