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 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