Theory Adaptive_Test_Case

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 ⟷ pass_io_set (from_FSM S s1) (atc_to_io_set (from_FSM M q1) A)"
  using pass_separator_from_pass_io_set[OF assms(1) _ assms(2-7)]
        pass_io_set_from_pass_separator[OF assms(1) _ assms(2-6)] by blast


lemma pass_separator_pass_io_set_maximal_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 ⟷ pass_io_set_maximal (from_FSM S s1) (remove_proper_prefixes (atc_to_io_set (from_FSM M q1) A))"
proof -

  have "is_ATC A"
    using separator_is_ATC[OF assms(1,2,4)]  by assumption
  then have "acyclic A" 
    unfolding is_ATC_def by auto
  then have "finite (L A)"
    unfolding acyclic_alt_def by assumption
  then have *: "finite (atc_to_io_set (from_FSM M q1) A)"
    unfolding atc_to_io_set.simps by blast

  have **: "⋀io' io''. io' @ io'' ∈ atc_to_io_set (from_FSM M q1) A ⟹ io' ∈ atc_to_io_set (from_FSM M q1) A"
    unfolding atc_to_io_set.simps
    using language_prefix[of _ _ "from_FSM M q1" "initial (from_FSM M q1)"]
    using language_prefix[of _ _ "A" "initial A"] by blast

  show ?thesis  
    unfolding pass_separator_pass_io_set_iff[OF assms] remove_proper_prefixes_def
    using pass_io_set_maximal_from_pass_io_set[of "(atc_to_io_set (from_FSM M q1) A)" "(from_FSM S s1)", OF * ] ** by blast
qed
  


end