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