# Theory State_Cover

```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)
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›
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

declare [[code drop: reachable_states]]
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```