Quelle  State_Cover.thy

section ‹State Cover›

text ‹This theory introduces a simple depth-first strategy for computing state covers.›


theory State_Cover
imports FSM 
begin

subsection ‹Basic Definitions›

type_synonym ('a,'b) state_cover = "('a × 'b) list set"
type_synonym ('a,'b,'c) state_cover_assignment = "'a ==> ('b × 'c) list"

fun is_state_cover :: "('a,'b,'c) fsm ==> ('b,'c) state_cover ==> bool" where
  "is_state_cover M SC = ([] ∈ SC ∧ (∀ q ∈ reachable_states M . ∃ io ∈ SC . q ∈ io_targets M io (initial M)))"

fun is_state_cover_assignment :: "('a,'b,'c) fsm ==> ('a,'b,'c) state_cover_assignment ==> bool" where
  "is_state_cover_assignment M f = (f (initial M) = [] ∧ (∀ q ∈ reachable_states M . q ∈ io_targets M (f q) (initial M)))"

lemma state_cover_assignment_from_state_cover :
  assumes "is_state_cover M SC"
obtains f where "is_state_cover_assignment M f"
            and "∧ q . q ∈ reachable_states M ==> f q ∈ SC"
proof -
  define f where f: "f = (λ q . (if q = initial M then [] else (SOME io . io ∈ SC ∧ q ∈ io_targets M io (initial M))))"

  have "f (initial M) = []"
    using f by auto
  moreover have "∧ q . q ∈ reachable_states M ==> f q ∈ SC ∧ q ∈ io_targets M (f q) (initial M)"
  proof -
    fix q assume "q ∈ reachable_states M"
    show "f q ∈ SC ∧ q ∈ io_targets M (f q) (initial M)"
    proof (cases "q = initial M")
      case True
      have "q ∈ io_targets M (f q) (FSM.initial M)"
        unfolding True ‹f (initial M) = []› by auto
      then show ?thesis
        using True assms ‹f (initial M) = []› by auto         
    next
      case False
      then have "f q = (SOME io . io ∈ SC ∧ q ∈ io_targets M io (initial M))"
        using f by auto
      moreover have "∃ io . io ∈ SC ∧ q ∈ io_targets M io (initial M)"
        using assms ‹q ∈ reachable_states M›
        by (meson is_state_cover.simps)     
      ultimately show ?thesis
        by (metis (no_types, lifting) someI_ex)         
    qed
  qed
  ultimately show ?thesis using that[of f]
    by (meson is_state_cover_assignment.elims(3))
qed

lemma is_state_cover_assignment_language :
  assumes "is_state_cover_assignment M V"
  and     "q ∈ reachable_states M"
shows "V q ∈ L M"
  using assms io_targets_language
  by (metis is_state_cover_assignment.simps) 

lemma is_state_cover_assignment_observable_after :
  assumes "observable M"
  and     "is_state_cover_assignment M V"
  and     "q ∈ reachable_states M"
shows "after_initial M (V q) = q"
proof -
  have "q ∈ io_targets M (V q) (initial M)"
    using assms(2,3)
    by auto 
  then have "io_targets M (V q) (initial M) = {q}"
    using observable_io_targets[OF assms(1) io_targets_language[OF ‹q ∈ io_targets M (V q) (initial M)›]]
    by (metis singletonD) 

  then obtain p where "path M (initial M) p" and "p_io p = V q" and "target (initial M) p = q"
    unfolding io_targets.simps
    by blast
  then show "after_initial M (V q) = q"
    using after_path[OF assms(1), of "initial M" p]
    by simp
qed

lemma non_initialized_state_cover_assignment_from_non_initialized_state_cover :
  assumes "∧ q . q ∈ reachable_states M ==> ∃ io ∈ L M ∩ SC . q ∈ io_targets M io (initial M)"
obtains f where "∧ q . q ∈ reachable_states M ==> q ∈ io_targets M (f q) (initial M)"
            and "∧ q . q ∈ reachable_states M ==> f q ∈ L M ∩ SC"
proof -
  define f where f: "f = (λ q . (SOME io . io ∈ L M ∩ SC ∧ q ∈ io_targets M io (initial M)))"

  have "∧ q . q ∈ reachable_states M ==> f q ∈ L M ∩ SC ∧ q ∈ io_targets M (f q) (initial M)"
  proof -
    fix q assume "q ∈ reachable_states M"
    show "f q ∈ L M ∩ SC ∧ q ∈ io_targets M (f q) (initial M)"
    proof -
      have "f q = (SOME io . io ∈ L M ∩ SC ∧ q ∈ io_targets M io (initial M))"
        using f by auto
      moreover have "∃ io . io ∈ L M ∩ SC ∧ q ∈ io_targets M io (initial M)"
        using assms ‹q ∈ reachable_states M›
        by (meson Int_iff)    
      ultimately show ?thesis
        by (metis (no_types, lifting) someI_ex)         
    qed
  qed
  then show ?thesis using that[of f]
    by blast
qed

lemma state_cover_assignment_inj :
  assumes "is_state_cover_assignment M V"
  and     "observable M"
  and     "q1 ∈ reachable_states M"
  and     "q2 ∈ reachable_states M"
  and     "q1 ≠ q2"
shows "V q1 ≠ V q2"
proof (rule ccontr)
  assume "¬ V q1 ≠ V q2" 

  then have "io_targets M (V q1) (initial M) = io_targets M (V q2) (initial M)"
    by auto
  then have "q1 = q2"
    using assms(2)
  proof -
    have f1: "∀a f. a ∉ FSM.states (f::('a, 'b, 'c) fsm) ∨ FSM.initial (FSM.from_FSM f a) = a"
      by (meson from_FSM_simps(1))
    obtain ff :: "('a ==> ('b × 'c) list) ==> ('a, 'b, 'c) fsm ==> ('a, 'b, 'c) fsm" and pps :: "('a ==> ('b × 'c) list) ==> ('a, 'b, 'c) fsm ==> 'a ==> ('b × 'c) list" where
      f2: "M = ff V M ∧ V = pps V M ∧ pps V M (FSM.initial (ff V M)) = [] ∧ (∀a. a ∉ reachable_states (ff V M) ∨ a ∈ io_targets (ff V M) (pps V M a) (FSM.initial (ff V M)))"
      using assms(1) by fastforce
    then have f3: "q2 ∈ FSM.states (ff V M)"
      by (simp add: ‹q2 ∈ reachable_states M› reachable_state_is_state)
    then have f4: "∃ps. FSM.initial (FSM.from_FSM M q2) = target (FSM.initial (ff V M)) ps ∧ path (ff V M) (FSM.initial (ff V M)) ps ∧ p_io ps = V q2"
      using f2 ‹q2 ∈ reachable_states M› assms(1) by auto
    have "q1 ∈ {target (FSM.initial M) ps |ps. path M (FSM.initial M) ps ∧ p_io ps = V q2}"
      by (metis (no_types) ‹io_targets M (V q1) (FSM.initial M) = io_targets M (V q2) (FSM.initial M)› ‹q1 ∈ reachable_states M› assms(1) io_targets.simps is_state_cover_assignment.simps)
    then have "∃ps. FSM.initial (FSM.from_FSM M q1) = target (FSM.initial (ff V M)) ps ∧ path (ff V M) (FSM.initial (ff V M)) ps ∧ p_io ps = V q2"
      using f2 by (simp add: ‹q1 ∈ reachable_states M› reachable_state_is_state)
    then show ?thesis
      using f4 f3 f2 f1 by (metis (no_types) ‹observable M› ‹q1 ∈ reachable_states M› observable_path_io_target reachable_state_is_state singletonD singletonI)
  qed 
  then show "False"
    using ‹q1 ≠ q2› by blast
qed


lemma state_cover_assignment_card :
  assumes "is_state_cover_assignment M V"
  and     "observable M"
shows "card (V ` reachable_states M) = card (reachable_states M)"
proof -  
  have "inj_on V (reachable_states M)"
    using state_cover_assignment_inj[OF assms] by (meson inj_onI)

  then have "card (reachable_states M) ≤ card (V ` reachable_states M)"
    using fsm_states_finite restrict_to_reachable_states_simps(2)
    by (simp add: card_image) 
  moreover have "card (V ` reachable_states M) ≤ card (reachable_states M)"
    using fsm_states_finite  
    using card_image_le
    by (metis restrict_to_reachable_states_simps(2)) 
  ultimately show ?thesis by simp
qed


lemma state_cover_assignment_language :
  assumes "is_state_cover_assignment M V"
  shows "V ` reachable_states M ⊆ L M"
  using assms unfolding is_state_cover_assignment.simps
  using language_io_target_append by fastforce 


fun is_minimal_state_cover :: "('a,'b,'c) fsm ==> ('b,'c) state_cover ==> bool" where
  "is_minimal_state_cover M SC = (∃ f . (SC = f ` reachable_states M) ∧ (is_state_cover_assignment M f))"

lemma minimal_state_cover_is_state_cover :
  assumes "is_minimal_state_cover M SC"
  shows "is_state_cover M SC"
proof -
  obtain f where "f (initial M) = []" and "(SC = f ` reachable_states M)" and "(∧ q . q ∈ reachable_states M ==> q ∈ io_targets M (f q) (initial M))"
    using assms by auto

  show ?thesis unfolding is_state_cover.simps ‹(SC = f ` reachable_states M)›
  proof -
    have "f ` FSM.reachable_states M ⊆ L M" 
    proof 
      fix io assume "io ∈ f ` FSM.reachable_states M"
      then obtain q where "q ∈ reachable_states M" and "io = f q"
        by blast
      then have "q ∈ io_targets M (f q) (initial M)"
        using ‹(∧ q . q ∈ reachable_states M ==> q ∈ io_targets M (f q) (initial M))› by blast
      then show "io ∈ L M"
        unfolding ‹io = f q › by force
    qed

    moreover have "∀q∈FSM.reachable_states M. ∃io∈f ` FSM.reachable_states M. q ∈ io_targets M io (FSM.initial M)"
      using ‹(∧ q . q ∈ reachable_states M ==> q ∈ io_targets M (f q) (initial M))› by blast

    ultimately show "[] ∈ f ` FSM.reachable_states M ∧ (∀q∈FSM.reachable_states M. ∃io∈f ` FSM.reachable_states M. q ∈ io_targets M io (FSM.initial M))"
      using ‹f (initial M) = []› reachable_states_initial by force
  qed
qed

lemma state_cover_assignment_after :
  assumes "observable M" 
  and     "is_state_cover_assignment M V"
  and     "q ∈ reachable_states M"
shows "V q ∈ L M" and "after_initial M (V q) = q" 
proof -
  have "V q ∈ L M ∧ after_initial M (V q) = q"
  using assms(3) proof (induct rule: reachable_states_induct)
    case init
    have "V (FSM.initial M) = []"
      using assms(2) 
      by auto
    then show ?case 
      by auto      
  next
    case (transition t)
    then have "t_target t ∈ reachable_states M"
      using reachable_states_next 
      by metis
    then have "t_target t ∈ io_targets M (V (t_target t)) (FSM.initial M)"
      using assms(2) 
      unfolding is_state_cover_assignment.simps
      by auto
    then obtain p where "path M (initial M) p" and "target (initial M) p = t_target t" and "p_io p = V (t_target t)"
      by auto
    then have "V (t_target t) ∈ L M"
      by force
    then show ?case 
      using after_path[OF assms(1) ‹path M (initial M) p›]
      unfolding ‹p_io p = V (t_target t)› ‹target (initial M) p = t_target t›
      by simp
  qed
  then show "V q ∈ L M" and "after_initial M (V q) = q" 
    by simp+
qed

(* transitions considered covered by a state cover in the SPY and SPYH-Methods *)
definition covered_transitions :: "('a,'b,'c) fsm ==> ('a,'b,'c) state_cover_assignment ==> ('b × 'c) list ==> ('a,'b,'c) transition set" where
  "covered_transitions M V α = (let
    ts = the_elem (paths_for_io M (initial M) α)
  in
    List.set (filter (λt . ((V (t_source t)) @ [(t_input t, t_output t)]) = (V (t_target t))) ts))"


subsection ‹State Cover Computation›


fun reaching_paths_up_to_depth :: "('a::linorder,'b::linorder,'c::linorder) fsm ==> 'a set ==> 'a set ==> ('a ==> ('a,'b,'c) path option) ==> nat ==> ('a ==> ('a,'b,'c) path option)" where 
  "reaching_paths_up_to_depth M nexts dones assignment 0 = assignment" |
  "reaching_paths_up_to_depth M nexts dones assignment (Suc k) = (let
      usable_transitions = filter (λ t . t_source t ∈ nexts ∧ t_target t ∉ dones ∧ t_target t ∉ nexts) (transitions_as_list M);
      targets = map t_target usable_transitions;
      transition_choice = Map.empty(targets [↦] usable_transitions);
      assignment' = assignment(targets [↦] (map (λq' . case transition_choice q' of Some t ==> (case assignment (t_source t) of Some p ==> p@[t])) targets));
      nexts' = set targets;
      dones' = nexts ∪ dones
    in reaching_paths_up_to_depth M nexts' dones' assignment' k)"



lemma reaching_paths_up_to_depth_set : 
  assumes "nexts = {q . (∃ p . path M (initial M) p ∧ target (initial M) p = q ∧ length p = n) ∧ (∄ p . path M (initial M) p ∧ target (initial M) p = q ∧ length p < n)}"
      and "dones = {q . ∃ p . path M (initial M) p ∧ target (initial M) p = q ∧ length p < n}"
      and "∧ q . assignment q = None = (∄p . path M (initial M) p ∧ target (initial M) p = q ∧ length p ≤ n)"
      and "∧ q p . assignment q = Some p ==> path M (initial M) p ∧ target (initial M) p = q ∧ length p ≤ n"
      and "dom assignment = nexts ∪ dones"
  shows "((reaching_paths_up_to_depth M nexts dones assignment k) q = None) = (∄p . path M (initial M) p ∧ target (initial M) p = q ∧ length p ≤ n+k)"
    and "((reaching_paths_up_to_depth M nexts dones assignment k) q = Some p) ==> path M (initial M) p ∧ target (initial M) p = q ∧ length p ≤ n+k"
    and "q ∈ nexts ∪ dones ==> (reaching_paths_up_to_depth M nexts dones assignment k) q = assignment q"
proof -
  have "(((reaching_paths_up_to_depth M nexts dones assignment k) q = None) = (∄p . path M (initial M) p ∧ target (initial M) p = q ∧ length p ≤ n+k))
        ∧ (((reaching_paths_up_to_depth M nexts dones assignment k) q = Some p) ⟶ path M (initial M) p ∧ target (initial M) p = q ∧ length p ≤ n+k)
        ∧ (q ∈ nexts ∪ dones ⟶ (reaching_paths_up_to_depth M nexts dones assignment k) q = assignment q)"
  using assms proof (induction k arbitrary: n q nexts dones assignment)
    case 0

    have *:"((reaching_paths_up_to_depth M nexts dones assignment 0) q) = assignment q"
      by auto
    show ?case 
      unfolding * using "0.prems"(3,4)[of q] by simp
  next
    case (Suc k)

    define usable_transitions where d1: "usable_transitions = filter (λ t . t_source t ∈ nexts ∧ t_target t ∉ dones ∧ t_target t ∉ nexts) (transitions_as_list M)"
    moreover define targets where d2: "targets = map t_target usable_transitions"
    moreover define transition_choice where d3: "transition_choice = Map.empty(targets [↦] usable_transitions)"
    moreover define assignment' where d4: "assignment' = assignment(targets [↦] (map (λq' . case transition_choice q' of Some t ==> (case assignment (t_source t) of Some p ==> p@[t])) targets))"
    ultimately have d5: "reaching_paths_up_to_depth M nexts dones assignment (Suc k) = reaching_paths_up_to_depth M (set targets) (nexts ∪ dones) assignment' k"
      unfolding reaching_paths_up_to_depth.simps Let_def by force

    let ?nexts' = "(set targets)"
    let ?dones' = "(nexts ∪ dones)"

    have p1: "?nexts' = {q. (∃p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p = Suc n) ∧
                            (∄p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p < Suc n)}" (is "?nexts' = ?PS")
    proof -
      have "∧ q . q ∈ ?nexts' ==> q ∈ ?PS"
      proof -
        fix q assume "q ∈ ?nexts'"
        then obtain t where "t ∈ transitions M"
                        and "t_source t ∈ nexts" 
                        and "t_target t = q"
                        and "t_target t ∉ dones"
                        and "t_target t ∉ nexts"
          unfolding d2 d1 using transitions_as_list_set[of M] by force                        

        obtain p where "path M (initial M) p" and "target (initial M) p = t_source t" and "length p = n"
          using ‹t_source t ∈ nexts› unfolding Suc.prems by blast
        then have "path M (initial M) (p@[t])" and "target (initial M) (p@[t]) = q"
          unfolding ‹t_target t = q›[symmetric] using ‹t ∈ transitions M› by auto
        then have "(∃p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p = Suc n)"
          using ‹length p = n› by (metis length_append_singleton)  
        moreover have "(∄p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p < Suc n)"
          using ‹t_target t ∉ dones› ‹t_target t ∉ nexts› unfolding ‹t_target t = q› Suc.prems
          using less_antisym by blast 
        ultimately show "q ∈ ?PS"
          by blast
      qed
      moreover have "∧ q . q ∈ ?PS ==> q ∈ ?nexts'" 
      proof -
        fix q assume "q ∈ ?PS"
        then obtain p where "path M (initial M) p" and "target (initial M) p = q" and "length p = Suc n"
          by auto

        let ?p = "butlast p"
        let ?t = "last p"


        have "p = ?p@[?t]"
          using ‹length p = Suc n›
          by (metis append_butlast_last_id list.size(3) nat.simps(3)) 
        then have "path M (initial M) (?p@[?t])" 
          using ‹path M (initial M) p› by auto

        have "path M (FSM.initial M) ?p"
             "?t ∈ FSM.transitions M"
             "t_source ?t = target (FSM.initial M) ?p"
          using path_append_transition_elim[OF ‹path M (initial M) (?p@[?t])›] by blast+

        have "t_target ?t = q"
          using ‹target (initial M) p = q› ‹p = ?p@[?t]› unfolding target.simps visited_states.simps
          by (metis (no_types, lifting) last_ConsR last_map map_is_Nil_conv snoc_eq_iff_butlast) 
        moreover have "t_source ?t ∈ nexts"
        proof -
          have "length ?p = n"
            using ‹p = ?p@[?t]› ‹length p = Suc n› by auto
          then have "(∃ p . path M (initial M) p ∧ target (initial M) p = t_source ?t ∧ length p = n)"
            using ‹path M (FSM.initial M) ?p› ‹t_source ?t = target (FSM.initial M) ?p›
            by metis 
          moreover have "(∄ p . path M (initial M) p ∧ target (initial M) p = t_source ?t ∧ length p < n)"
          proof 
            assume "∃p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = t_source ?t ∧ length p < n"
            then obtain p' where "path M (FSM.initial M) p'" and "target (FSM.initial M) p' = t_source ?t" and "length p' < n"
              by blast
            then have "path M (initial M) (p'@[?t])" and "length (p'@[?t]) < Suc n"
              using ‹?t ∈ FSM.transitions M› by auto
            moreover have "target (initial M) (p'@[?t]) = q"
              using ‹t_target ?t = q› by auto
            ultimately show "False"
              using ‹q ∈ ?PS›
              by (metis (mono_tags, lifting) mem_Collect_eq)
          qed
          ultimately show ?thesis
            unfolding Suc.prems by blast
        qed
        moreover have "q ∉ dones" and "q ∉ nexts"
          unfolding Suc.prems using ‹q ∈ ?PS›
          using less_SucI by blast+
        ultimately have "t_source ?t ∈ nexts ∧ t_target ?t ∉ dones ∧ t_target ?t ∉ nexts"
          by simp
        then show "q ∈ ?nexts'"
          unfolding d2 d1 using transitions_as_list_set[of M] ‹?t ∈ FSM.transitions M› ‹t_target ?t = q›
          by auto 
      qed
      ultimately show ?thesis
        by blast
    qed

    have p2: "?dones' = {q. ∃p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p < Suc n}" (is "?dones' = ?PS")
    proof -
      have "∧ q . q ∈ ?dones' ==> q ∈ ?PS" 
        unfolding Suc.prems
        using less_SucI by blast 
      moreover have "∧ q . q ∈ ?PS ==> q ∈ ?dones'"
      proof -
        fix q assume "q ∈ ?PS"
        show "q ∈ ?dones'" proof (cases "∃p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p < n")
          case True
          then show ?thesis unfolding Suc.prems by blast
        next
          case False

          obtain p where *: "path M (FSM.initial M) p ∧ target (FSM.initial M) p = q" and "length p < Suc n" 
            using ‹q ∈ ?PS› by blast
          then have "length p = n"
            using False by force

          then show ?thesis 
            using * False unfolding Suc.prems by blast
        qed
      qed
      ultimately show ?thesis
        by blast
    qed

    have p3: "(∧q. (assignment' q = None) = (∄p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ Suc n))"
    and  p4: "(∧q p. assignment' q = Some p ==> path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ Suc n)"
    and  p5: "dom assignment' = ?nexts' ∪ ?dones'"
    proof -

      have "dom transition_choice = set targets"
        unfolding d3 d2 by auto

      show "dom assignment' = ?nexts' ∪ ?dones'"
        by (simp add: ‹dom assignment = nexts ∪ dones› d4)

      have helper: "∧ f P (n::nat) . {x . (∃ y . P x y ∧ f y = n) ∧ (∄ y . P x y ∧ f y < n)} ∪ {x . (∃ y . P x y ∧ f y < n)}= {x . (∃ y . P x y ∧ f y ≤ n)}"
        by force
      
      have dom': "dom assignment' = {q. ∃p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ Suc n}"
        unfolding ‹dom assignment' = ?nexts' ∪ ?dones'› p1 p2 
        using helper[of "λ q p . path M (FSM.initial M) p ∧ target (FSM.initial M) p = q" length "Suc n"] by force 


      have *: "∧ q . q ∈ ?nexts' ==> ∃ p . assignment' q = Some p ∧ path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ Suc n"
      proof -
        fix q assume "q ∈ ?nexts'"
        then obtain t where "transition_choice q = Some t" 
          using ‹dom transition_choice = set targets› d2 d3 by blast 
        then have "t ∈ set usable_transitions" 
              and "t_target t = q"
              and "q ∈ set targets"
          unfolding d3 d2 using map_upds_map_set_left[of t_target usable_transitions q t] by auto
        then have "t_source t ∈ nexts" and "t ∈ transitions M"
          unfolding d1 using transitions_as_list_set[of M] by auto
        then obtain p where "assignment (t_source t) = Some p"
          using Suc.prems(1,3,4)
          by fastforce
        then have "path M (FSM.initial M) p ∧ target (FSM.initial M) p = t_source t ∧ length p ≤ n"
          using Suc.prems(4) by blast
        then have "path M (FSM.initial M) (p@[t]) ∧ target (FSM.initial M) (p@[t]) = q ∧ length (p@[t]) ≤ Suc n"
          using ‹t ∈ transitions M› ‹t_target t = q› by auto
        moreover have "assignment' q = Some (p@[t])" 
        proof -
          have "assignment' q = [targets [↦] (map (λq' . case transition_choice q' of Some t ==> (case assignment (t_source t) of Some p ==> p@[t])) targets)] q"
            unfolding d4 using map_upds_overwrite[OF ‹q ∈ set targets›, of "map (λq' . case transition_choice q' of Some t ==> (case assignment (t_source t) of Some p ==> p@[t])) targets" assignment]
            by auto
          also have "… = Some (case transition_choice q of Some t ==> case assignment (t_source t) of Some p ==> p @ [t])"
            using map_upds_map_set_right[OF ‹q ∈ set targets›] by auto
          also have "… = Some (p@[t])"
            using ‹transition_choice q = Some t›  ‹assignment (t_source t) = Some p› by simp
          finally show ?thesis .
        qed
        ultimately show "∃ p . assignment' q = Some p ∧ path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ Suc n"
          by simp
      qed      
      
      show "(∧q. (assignment' q = None) = (∄p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ Suc n))"
        using dom' by blast
      
      show "(∧q p. assignment' q = Some p ==> path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ Suc n)"
      proof - 
        fix q p assume "assignment' q = Some p"

        show "path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ Suc n"
        proof (cases "q ∈ ?nexts'")
          case True
          show ?thesis using *[OF True] ‹assignment' q = Some p›
            by simp 
        next
          case False
          moreover have "∧ q . assignment q ≠ assignment' q ==> q ∈ ?nexts'"
            unfolding d4
            by (metis (no_types) map_upds_apply_nontin) 
          ultimately have "assignment' q = assignment q"
            by force
          then show ?thesis 
            using Suc.prems(4) ‹assignment' q = Some p›
            by (simp add: le_SucI) 
        qed
      qed
    qed


    have "∧ q . (reaching_paths_up_to_depth M (set targets) (nexts ∪ dones) assignment' k q = None) =
          (∄p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ n + Suc k) ∧
          (reaching_paths_up_to_depth M (set targets) (nexts ∪ dones) assignment' k q = Some p ⟶
           path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ n + Suc k)"
      using Suc.IH[OF p1 p2 p3 p4 p5] by auto

    moreover have "(q ∈ nexts ∪ dones ⟶ reaching_paths_up_to_depth M nexts dones assignment (Suc k) q = assignment q)"
    proof - 
      have "∧ q . (q ∈ set targets ∪ (nexts ∪ dones) ==> reaching_paths_up_to_depth M (set targets) (nexts ∪ dones) assignment' k q = assignment' q)"
        using Suc.IH[OF p1 p2 p3 p4 p5] by auto
      moreover have "∧ q . assignment q ≠ assignment' q ==> q ∈ ?nexts'"
        unfolding d4
        by (metis (no_types) map_upds_apply_nontin) 
      ultimately show ?thesis
        unfolding d5
        by (metis (mono_tags, lifting) Un_iff mem_Collect_eq p1 p2) 
    qed
    ultimately show ?case
      unfolding d5 by blast
  qed

  then show "((reaching_paths_up_to_depth M nexts dones assignment k) q = None) = (∄p . path M (initial M) p ∧ target (initial M) p = q ∧ length p ≤ n+k)"
        and "((reaching_paths_up_to_depth M nexts dones assignment k) q = Some p) ==> path M (initial M) p ∧ target (initial M) p = q ∧ length p ≤ n+k" 
        and "q ∈ nexts ∪ dones ==> (reaching_paths_up_to_depth M nexts dones assignment k) q = assignment q"
    by blast+
qed



fun get_state_cover_assignment :: "('a::linorder,'b::linorder,'c::linorder) fsm ==> ('a,'b,'c) state_cover_assignment" where
  "get_state_cover_assignment M = (let
      path_assignments = reaching_paths_up_to_depth M {initial M} {} [initial M ↦ []] (size M -1)
    in (λ q . case path_assignments q of Some p ==> p_io p | None ==> []))"



lemma get_state_cover_assignment_is_state_cover_assignment : 
  "is_state_cover_assignment M (get_state_cover_assignment M)"
  unfolding is_state_cover_assignment.simps
proof 

  define path_assignments where "path_assignments = reaching_paths_up_to_depth M {initial M} {} [initial M ↦ []] (size M -1)"
  then have *:"∧ q . get_state_cover_assignment M q = (case path_assignments q of Some p ==> p_io p | None ==> [])"
    by auto
    

  have c1: " {FSM.initial M} =
    {q. (∃p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p = 0) ∧
      (∄p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p < 0)}" 
    by auto
  have c2:  "{} = {q. ∃p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p < 0}"
    by auto
  have c3: "(∧q. ([FSM.initial M ↦ []] q = None) =
        (∄p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ 0))" by auto
  have c4: "(∧q p. [FSM.initial M ↦ []] q = Some p ==>
          path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ 0)"
    by (metis (no_types, lifting) c3 le_zero_eq length_0_conv map_upd_Some_unfold option.discI) 
  have c5: "dom [FSM.initial M ↦ []] = {FSM.initial M} ∪ {}"
    by simp

  have p1: "∧ q . (path_assignments q = None) =
                   (∄p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ (FSM.size M - 1))"
   and p2: "∧ q p . path_assignments q = Some p ==>
                     path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ (FSM.size M - 1)"
   and p3: "path_assignments (initial M) = Some []"
    unfolding ‹path_assignments = reaching_paths_up_to_depth M {initial M} {} [initial M ↦ []] (size M -1)›
    using reaching_paths_up_to_depth_set[OF c1 c2 c3 c4 c5] by auto

  show "get_state_cover_assignment M (FSM.initial M) = []"
    unfolding * p3 by auto

  show "∀q∈reachable_states M. q ∈ io_targets M (get_state_cover_assignment M q) (FSM.initial M)"
  proof 
    fix q assume "q ∈ reachable_states M"
    then have "q ∈ reachable_k M (FSM.initial M) (FSM.size M - 1)"
      using reachable_k_states by metis
    then obtain p where "target (initial M) p = q" and "path M (initial M) p" and "length p ≤ size M - 1"
      by auto
    then have "path_assignments q ≠ None"
      using p1 by fastforce
    then obtain p' where "get_state_cover_assignment M q = p_io p'"
                     and "path M (FSM.initial M) p'" and "target (FSM.initial M) p' = q"
      using p2 unfolding * by force
    then show "q ∈ io_targets M (get_state_cover_assignment M q) (initial M)" 
      unfolding io_targets.simps unfolding ‹get_state_cover_assignment M q = p_io p'› by blast
  qed
qed



subsection ‹Computing Reachable States via State Cover Computation›


lemma restrict_to_reachable_states[code]:
  "restrict_to_reachable_states M = (let
      path_assignments = reaching_paths_up_to_depth M {initial M} {} [initial M ↦ []] (size M -1)
    in filter_states M (λ q . path_assignments q ≠ None))"
proof -
  define path_assignments where "path_assignments = reaching_paths_up_to_depth M {initial M} {} [initial M ↦ []] (size M -1)"    
  then have *: "(let
      path_assignments = reaching_paths_up_to_depth M {initial M} {} [initial M ↦ []] (size M -1)
    in filter_states M (λ q . path_assignments q ≠ None)) = filter_states M (λ q . path_assignments q ≠ None)"
    by simp

  have c1: " {FSM.initial M} =
    {q. (∃p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p = 0) ∧
      (∄p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p < 0)}" 
    by auto
  have c2:  "{} = {q. ∃p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p < 0}"
    by auto
  have c3: "(∧q. ([FSM.initial M ↦ []] q = None) =
        (∄p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ 0))" by auto
  have c4: "(∧q p. [FSM.initial M ↦ []] q = Some p ==>
          path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ 0)"
    by (metis (no_types, lifting) c3 le_zero_eq length_0_conv map_upd_Some_unfold option.discI) 
  have c5: "dom [FSM.initial M ↦ []] = {FSM.initial M} ∪ {}"
    by simp

  have p1: "∧ q . (path_assignments q = None) =
                   (∄p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ (FSM.size M - 1))"
   and p2: "∧ q p . path_assignments q = Some p ==>
                     path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ (FSM.size M - 1)"
   and p3: "path_assignments (initial M) = Some []"
    unfolding ‹path_assignments = reaching_paths_up_to_depth M {initial M} {} [initial M ↦ []] (size M -1)›
    using reaching_paths_up_to_depth_set[OF c1 c2 c3 c4 c5] by auto


  have "∧ q . path_assignments q ≠ None ⟷ q ∈ reachable_states M"
  proof 
    show "∧q. path_assignments q ≠ None ==> q ∈ reachable_states M"
      using p2 unfolding reachable_states_def
      by blast 
    show "∧q. q ∈ reachable_states M ==> path_assignments q ≠ None"
    proof -
      fix q assume "q ∈ reachable_states M"
      then have "q ∈ reachable_k M (FSM.initial M) (FSM.size M - 1)"
        using reachable_k_states by metis
      then obtain p where "target (initial M) p = q" and "path M (initial M) p" and "length p ≤ size M - 1"
        by auto
      then show "path_assignments q ≠ None"
        using p1 by fastforce
    qed
  qed
  then show ?thesis
    unfolding restrict_to_reachable_states.simps * by simp
qed

lemma reachable_states_refined[code] : 
  "reachable_states M = (let
      path_assignments = reaching_paths_up_to_depth M {initial M} {} [initial M ↦ []] (size M -1)
    in Set.filter (λ q . path_assignments q ≠ None) (states M))"
proof -
  define path_assignments where "path_assignments = reaching_paths_up_to_depth M {initial M} {} [initial M ↦ []] (size M -1)"    
  then have *: "(let
      path_assignments = reaching_paths_up_to_depth M {initial M} {} [initial M ↦ []] (size M -1)
    in Set.filter (λ q . path_assignments q ≠ None) (states M)) = Set.filter (λ q . path_assignments q ≠ None) (states M)"
    by simp

  have c1: " {FSM.initial M} =
    {q. (∃p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p = 0) ∧
      (∄p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p < 0)}" 
    by auto
  have c2:  "{} = {q. ∃p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p < 0}"
    by auto
  have c3: "(∧q. ([FSM.initial M ↦ []] q = None) =
        (∄p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ 0))" by auto
  have c4: "(∧q p. [FSM.initial M ↦ []] q = Some p ==>
          path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ 0)"
    by (metis (no_types, lifting) c3 le_zero_eq length_0_conv map_upd_Some_unfold option.discI) 
  have c5: "dom [FSM.initial M ↦ []] = {FSM.initial M} ∪ {}"
    by simp

  have p1: "∧ q . (path_assignments q = None) =
                   (∄p. path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ (FSM.size M - 1))"
   and p2: "∧ q p . path_assignments q = Some p ==>
                     path M (FSM.initial M) p ∧ target (FSM.initial M) p = q ∧ length p ≤ (FSM.size M - 1)"
   and p3: "path_assignments (initial M) = Some []"
    unfolding ‹path_assignments = reaching_paths_up_to_depth M {initial M} {} [initial M ↦ []] (size M -1)›
    using reaching_paths_up_to_depth_set[OF c1 c2 c3 c4 c5] by auto


  have "∧ q . path_assignments q ≠ None ⟷ q ∈ reachable_states M"
  proof 
    show "∧q. path_assignments q ≠ None ==> q ∈ reachable_states M"
      using p2 unfolding reachable_states_def
      by blast 
    show "∧q. q ∈ reachable_states M ==> path_assignments q ≠ None"
    proof -
      fix q assume "q ∈ reachable_states M"
      then have "q ∈ reachable_k M (FSM.initial M) (FSM.size M - 1)"
        using reachable_k_states by metis
      then obtain p where "target (initial M) p = q" and "path M (initial M) p" and "length p ≤ size M - 1"
        by auto
      then show "path_assignments q ≠ None"
        using p1 by fastforce
    qed
  qed
  then show ?thesis
    unfolding * using reachable_state_is_state by force
qed


lemma minimal_sequence_to_failure_from_state_cover_assignment_ob :
  assumes "L M ≠ L I"
  and     "is_state_cover_assignment M V"
  and     "(L M ∩ (V ` reachable_states M)) = (L I ∩ (V ` reachable_states M))"
obtains ioT ioX where "ioT ∈ (V ` reachable_states M)"
                  and "ioT @ ioX ∈ (L M - L I) ∪ (L I - L M)"
                  and "∧ io q . q ∈ reachable_states M ==> (V q)@io ∈ (L M - L I) ∪ (L I - L M) ==> length ioX ≤ length io"
proof -

  let ?exts = "{io . ∃ q ∈ reachable_states M . (V q)@io ∈ (L M - L I) ∪ (L I - L M)}"
  define exMin where exMin: "exMin = arg_min length (λ io . io ∈ ?exts)"
  
  have "V (initial M) = []"
    using assms(2) by auto
  moreover have "∃ io . io ∈ (L M - L I) ∪ (L I - L M)"
    using assms(1) by blast 
  ultimately have "?exts ≠ {}"
    using reachable_states_initial by (metis (mono_tags, lifting) append_self_conv2 empty_iff mem_Collect_eq) 
  then have "exMin ∈ ?exts ∧ (∀ io' . io' ∈ ?exts ⟶ length exMin ≤ length io')"
    using exMin arg_min_nat_lemma by (metis (no_types, lifting) all_not_in_conv)
  then show ?thesis 
    using that by blast
qed


end