section ‹State Preambles› text ‹This theory defines state preambles. A state preamble @{text "P"} of some state @{text "q"} of some FSM @{text "M"} is an acyclic single-input submachine of @{text "M"} that contains for each of its states and defined inputs in that state all transitions of @{text "M"} and has @{text "q"} as its only deadlock state. That is, @{text "P"} represents a strategy of reaching @{text "q"} in every complete submachine of @{text "M"}. In testing, preambles are used to reach states in the SUT that must conform to a single known state in the specification.› theory State_Preamble imports "../Product_FSM" Backwards_Reachability_Analysis begin definition is_preamble :: "('a,'b,'c) fsm ⇒ ('a,'b,'c) fsm ⇒ 'a ⇒ bool" where "is_preamble S M q = ( acyclic S ∧ single_input S ∧ is_submachine S M ∧ q ∈ reachable_states S ∧ deadlock_state S q ∧ (∀ q' ∈ reachable_states S . (q = q' ∨ ¬ deadlock_state S q') ∧ (∀ x ∈ inputs M . (∃ t ∈ transitions S . t_source t = q' ∧ t_input t = x) ⟶ (∀ t' ∈ transitions M . t_source t' = q' ∧ t_input t' = x ⟶ t' ∈ transitions S))))" fun definitely_reachable :: "('a,'b,'c) fsm ⇒ 'a ⇒ bool" where "definitely_reachable M q = (∃ S . is_preamble S M q)" subsection ‹Basic Properties› lift_definition initial_preamble :: "('a,'b,'c) fsm ⇒ ('a,'b,'c) fsm" is FSM_Impl.initial_singleton by auto lemma initial_preamble_simps[simp] : "initial (initial_preamble M) = initial M" "states (initial_preamble M) = {initial M}" "inputs (initial_preamble M) = inputs M" "outputs (initial_preamble M) = outputs M" "transitions (initial_preamble M) = {}" by (transfer; auto)+ lemma is_preamble_initial : "is_preamble (initial_preamble M) M (initial M)" proof - have "acyclic (initial_preamble M)" by (metis acyclic_code empty_iff initial_preamble_simps(5)) moreover have "single_input (initial_preamble M)" by auto moreover have "is_submachine (initial_preamble M) M" by (simp add: fsm_initial) moreover have "(initial M) ∈ reachable_states (initial_preamble M)" unfolding reachable_states_def using reachable_states_intro by auto moreover have "deadlock_state (initial_preamble M) (initial M)" by simp ultimately show ?thesis unfolding is_preamble_def using reachable_state_is_state by force qed lemma is_preamble_next : assumes "is_preamble S M q" and "q ≠ initial M" and "t ∈ transitions S" and "t_source t = initial M" shows "is_preamble (from_FSM S (t_target t)) (from_FSM M (t_target t)) q" (is "is_preamble ?S ?M q") proof - have "acyclic S" and "single_input S" and "is_submachine S M" and "q ∈ reachable_states S" and "deadlock_state S q" and *: "(∀ q' ∈ reachable_states S . (q = q' ∨ ¬ deadlock_state S q') ∧ (∀ x ∈ inputs M . (∃ t ∈ transitions S . t_source t = q' ∧ t_input t = x) ⟶ (∀ t' ∈ transitions M . t_source t' = q' ∧ t_input t' = x ⟶ t' ∈ transitions S)))" using assms(1) unfolding is_preamble_def by linarith+ have "t_target t ∈ states S" using assms(3) fsm_transition_target by metis have "t_target t ∈ states M" using ‹is_submachine S M› ‹t_target t ∈ FSM.states S› by auto have is_acyclic: "acyclic ?S" using from_FSM_path_initial[OF ‹t_target t ∈ states S›] unfolding acyclic.simps from_FSM_simps[OF ‹t_target t ∈ states S›] using acyclic_paths_from_reachable_states[OF ‹acyclic S›, of "[t]" "t_target t"] by (metis ‹is_submachine S M› assms(3) assms(4) is_submachine.elims(2) prod.collapse single_transition_path target_single_transition) have is_single_input: "single_input ?S" using ‹single_input S› unfolding single_input.simps from_FSM_simps[OF ‹t_target t ∈ states S›] by blast have "initial ?S = initial ?M" by (simp add: ‹t_target t ∈ FSM.states M› ‹t_target t ∈ FSM.states S›) moreover have "inputs ?S = inputs ?M" using ‹is_submachine S M› by (simp add: ‹t_target t ∈ FSM.states M› ‹t_target t ∈ FSM.states S›) moreover have "outputs ?S = outputs ?M" using ‹is_submachine S M› by (simp add: ‹t_target t ∈ FSM.states M› ‹t_target t ∈ FSM.states S›) moreover have "transitions ?S ⊆ transitions ?M" using ‹is_submachine S M› by (simp add: ‹t_target t ∈ FSM.states M› ‹t_target t ∈ FSM.states S›) ultimately have is_sub : "is_submachine ?S ?M" using ‹is_submachine S M› ‹t_target t ∈ FSM.states M› ‹t_target t ∈ FSM.states S› by auto have contains_q : "q ∈ reachable_states ?S" proof - obtain qd where "qd ∈ reachable_states ?S" and "deadlock_state ?S qd" using is_acyclic using acyclic_deadlock_reachable by blast have "qd ∈ reachable_states S" by (metis (no_types, lifting) ‹is_submachine S M› ‹qd ∈ reachable_states (FSM.from_FSM S (t_target t))› assms(3) assms(4) from_FSM_reachable_states in_mono is_submachine.elims(2) prod.collapse reachable_states_intro single_transition_path target_single_transition) then have "deadlock_state S qd" using ‹deadlock_state ?S qd› unfolding deadlock_state.simps by (simp add: ‹t_target t ∈ FSM.states S›) then have "qd = q" using * ‹qd ∈ reachable_states S› by fastforce then show ?thesis using ‹qd ∈ reachable_states ?S› by auto qed have has_deadlock_q : "deadlock_state ?S q" using * by (metis ‹deadlock_state S q› ‹t_target t ∈ FSM.states S› deadlock_state.simps from_FSM_simps(4)) have has_states_prop_1: "⋀ q' . q' ∈ reachable_states ?S ⟹ deadlock_state ?S q' ⟹ q = q'" proof - fix q' assume "q' ∈ reachable_states ?S" and "deadlock_state ?S q'" have "q' ∈ reachable_states S" by (metis (no_types, lifting) ‹is_submachine S M› ‹q' ∈ reachable_states (FSM.from_FSM S (t_target t))› assms(3) assms(4) from_FSM_reachable_states in_mono is_submachine.elims(2) prod.collapse reachable_states_intro single_transition_path target_single_transition) then have "deadlock_state S q'" using ‹deadlock_state ?S q'› unfolding deadlock_state.simps using ‹q' ∈ reachable_states ?S› by (simp add: ‹t_target t ∈ FSM.states S›) then show "q = q'" using * ‹q' ∈ reachable_states S› by fastforce qed moreover have has_states_prop_2: "⋀ x t t' q' . q' ∈ reachable_states ?S ⟹ t ∈ transitions ?S ⟹ t_source t = q' ⟹ t_input t = x ⟹ t' ∈ transitions ?M ⟹ t_source t' = q' ⟹ t_input t' = x ⟹ t' ∈ transitions ?S" proof - fix x tS tM q' assume "q' ∈ reachable_states ?S" and "tS ∈ transitions ?S" and "t_source tS = q'" and "t_input tS = x" and "tM ∈ transitions ?M" and "t_source tM = q'" and "t_input tM = x" have "q' ∈ reachable_states S" by (metis (no_types, lifting) ‹is_submachine S M› ‹q' ∈ reachable_states (FSM.from_FSM S (t_target t))› assms(3) assms(4) from_FSM_reachable_states in_mono is_submachine.elims(2) prod.collapse reachable_states_intro single_transition_path target_single_transition) have "tS ∈ transitions S" using ‹tS ∈ transitions ?S› by (simp add: ‹t_target t ∈ FSM.states S›) have "tM ∈ transitions M" using ‹tM ∈ transitions ?M› using ‹t_target t ∈ FSM.states M› by (simp add: ‹t_target t ∈ FSM.states S›) have "t_source tS ∈ states (from_FSM S (t_target t))" using ‹tS ∈ transitions ?S› by auto have "t_source tM ∈ states (from_FSM M (t_target t))" using ‹tM ∈ transitions ?M› by auto have "q' ∈ reachable_states ?M" using ‹q' ∈ reachable_states ?S› submachine_path[OF ‹is_submachine ?S ?M›] unfolding reachable_states_def proof - assume "q' ∈ {target (FSM.initial (FSM.from_FSM S (t_target t))) p |p. path (FSM.from_FSM S (t_target t)) (FSM.initial (FSM.from_FSM S (t_target t))) p}" then show "q' ∈ {target (FSM.initial (FSM.from_FSM M (t_target t))) ps |ps. path (FSM.from_FSM M (t_target t)) (FSM.initial (FSM.from_FSM M (t_target t))) ps}" using ‹FSM.initial (FSM.from_FSM S (t_target t)) = FSM.initial (FSM.from_FSM M (t_target t))› ‹⋀q p. path (FSM.from_FSM S (t_target t)) q p ⟹ path (FSM.from_FSM M (t_target t)) q p› by fastforce qed show "tM ∈ transitions ?S" using * ‹q' ∈ reachable_states S› ‹tM ∈ FSM.transitions M› ‹tS ∈ FSM.transitions S› ‹t_input tM = x› ‹t_input tS = x› ‹t_source tM = q'› ‹t_source tS = q'› ‹t_target t ∈ FSM.states S› by fastforce qed show ?thesis unfolding is_preamble_def using is_acyclic is_single_input is_sub contains_q has_deadlock_q has_states_prop_1 using has_states_prop_2 by blast qed lemma observable_preamble_paths : assumes "is_preamble P M q'" and "observable M" and "path M q p" and "p_io p ∈ LS P q" and "q ∈ reachable_states P" shows "path P q p" using assms(3,4,5) proof (induction p arbitrary: q rule: list.induct) case Nil then show ?case by auto next case (Cons t p) have "is_submachine P M" and *: "⋀ q' x t t' . q'∈reachable_states P ⟹ x∈FSM.inputs M ⟹ t∈FSM.transitions P ⟹ t_source t = q' ⟹ t_input t = x ⟹ t'∈FSM.transitions M ⟹ t_source t' = q' ⟹ t_input t' = x ⟹ t' ∈ FSM.transitions P" using assms(1) unfolding is_preamble_def by blast+ have "observable P" using submachine_observable[OF ‹is_submachine P M› ‹observable M›] by blast obtain t' where "t'∈FSM.transitions P" and "t_source t' = q" and "t_input t' = t_input t" using ‹p_io (t # p) ∈ LS P q› by auto have "t_source t = q" and "t ∈ transitions M" and "t_input t ∈ inputs M" using ‹path M q (t # p)› by auto have "t ∈ transitions P" using *[OF ‹q ∈ reachable_states P› ‹t_input t ∈ inputs M› ‹t'∈FSM.transitions P› ‹t_source t' = q› ‹t_input t' = t_input t› ‹t ∈ transitions M› ‹t_source t = q›] by auto have "path M (t_target t) p" using ‹path M q (t # p)› by auto moreover have "p_io p ∈ LS P (t_target t)" proof - have f1: "t_input t = fst (t_input t, t_output t)" by (metis fst_conv) have f2: "t_output t = snd (t_input t, t_output t)" by auto have f3: "(t_input t, t_output t) # p_io p ∈ LS P (t_source t)" using Cons.prems(2) ‹t_source t = q› by fastforce have "L (FSM.from_FSM P (t_target t)) = LS P (t_target t)" by (meson ‹t ∈ FSM.transitions P› from_FSM_language fsm_transition_target) then show ?thesis using f3 f2 f1 ‹observable P› ‹t ∈ FSM.transitions P› observable_language_next by blast qed moreover have "t_target t ∈ reachable_states P" using ‹t ∈ transitions P› ‹t_source t = q› ‹q ∈ reachable_states P› by (meson reachable_states_next) ultimately have "path P (t_target t) p" using Cons.IH by blast then show ?case using ‹t ∈ transitions P› ‹t_source t = q› by auto qed lemma preamble_pass_path : assumes "is_preamble P M q" and "⋀ io x y y' . io@[(x,y)] ∈ L P ⟹ io@[(x,y')] ∈ L M' ⟹ io@[(x,y')] ∈ L P" and "completely_specified M'" and "inputs M' = inputs M" obtains p where "path P (initial P) p" and "target (initial P) p = q" and "p_io p ∈ L M'" proof - (* get the longest paths p such that p_io p is still in L M' *) let ?ps = "{p . path P (initial P) p ∧ p_io p ∈ L M'}" have "?ps ≠ {}" proof - have "[] ∈ ?ps" by auto then show ?thesis by blast qed moreover have "finite ?ps" proof - have "acyclic P" using assms(1) unfolding is_preamble_def by blast have "finite {p. path P (FSM.initial P) p}" using acyclic_finite_paths_from_reachable_state[OF ‹acyclic P›, of "[]" "initial P"] by auto then show ?thesis by simp qed ultimately obtain p where "p ∈ ?ps" and "⋀ p' . p' ∈ ?ps ⟹ length p' ≤ length p" by (meson leI max_length_elem) then have "path P (initial P) p" and "p_io p ∈ L M'" by blast+ show ?thesis proof (cases "target (initial P) p = q") case True then show ?thesis using that[OF ‹path P (initial P) p› _ ‹p_io p ∈ L M'›] by blast next case False (* if p does not target the sole deadlock state q, then it can be extended *) then have "¬ deadlock_state P (target (initial P) p)" using reachable_states_intro[OF ‹path P (initial P) p›] assms(1) unfolding is_preamble_def by fastforce then obtain t where "t ∈ transitions P" and "t_source t = target (initial P) p" by auto then have "path P (initial P) (p@[t])" using ‹path P (initial P) p› path_append_transition by simp have "(p_io p) @ [(t_input t, t_output t)] ∈ L P" using language_intro[OF ‹path P (initial P) (p@[t])›] by simp have "t_input t ∈ inputs M'" using assms(1,4) fsm_transition_input[OF ‹t ∈ transitions P›] unfolding is_preamble_def is_submachine.simps by blast obtain p' where "path M' (initial M') p'" and "p_io p' = p_io p" using ‹p_io p ∈ L M'› by auto obtain t' where "t' ∈ transitions M'" and "t_source t' = target (initial M') p'" and "t_input t' = t_input t" using ‹completely_specified M'› ‹t_input t ∈ inputs M'› path_target_is_state[OF ‹path M' (initial M') p'›] unfolding completely_specified.simps by blast then have "path M' (initial M') (p'@[t'])" using ‹path M' (initial M') p'› path_append_transition by simp have "(p_io p) @ [(t_input t, t_output t')] ∈ L M'" using language_intro[OF ‹path M' (initial M') (p'@[t'])›] unfolding ‹p_io p' = p_io p›[symmetric] ‹t_input t' = t_input t›[symmetric] by simp have "(p_io p) @ [(t_input t, t_output t')] ∈ L P" using assms(2)[OF ‹(p_io p) @ [(t_input t, t_output t)] ∈ L P› ‹(p_io p) @ [(t_input t, t_output t')] ∈ L M'›] by assumption then obtain pt' where "path P (initial P) pt'" and "p_io pt' = (p_io p) @ [(t_input t, t_output t')]" by auto then have "pt' ∈ ?ps" using ‹(p_io p) @ [(t_input t, t_output t')] ∈ L M'› by auto then have "length pt' ≤ length p" using ‹⋀ p' . p' ∈ ?ps ⟹ length p' ≤ length p› by blast moreover have "length pt' > length p" using ‹p_io pt' = (p_io p) @ [(t_input t, t_output t')]› unfolding length_map[of "(λ t . (t_input t, t_output t))", symmetric] by simp ultimately have "False" by simp then show ?thesis by simp qed qed lemma preamble_maximal_io_paths : assumes "is_preamble P M q" and "observable M" and "path P (initial P) p" and "target (initial P) p = q" shows "∄io' . io' ≠ [] ∧ p_io p @ io' ∈ L P" proof - have "deadlock_state P q" and "is_submachine P M" using assms(1) unfolding is_preamble_def by blast+ have "observable P" using ‹observable M› ‹is_submachine P M› using submachine_observable by blast show "∄io' . io' ≠ [] ∧ p_io p @ io' ∈ L P" proof assume "∃io'. io' ≠ [] ∧ p_io p @ io' ∈ L P" then obtain io' where "io' ≠ []" and "p_io p @ io' ∈ L P" by blast obtain p1 p2 where "path P (FSM.initial P) p1" and "path P (target (FSM.initial P) p1) p2" and "p_io p1 = p_io p" and "p_io p2 = io'" using language_state_split[OF ‹p_io p @ io' ∈ L P›] by blast have "p1 = p" using observable_path_unique[OF ‹observable P› ‹path P (FSM.initial P) p1› ‹path P (FSM.initial P) p› ‹p_io p1 = p_io p›] by assumption have "io' ∈ LS P q" using ‹path P (target (FSM.initial P) p1) p2› ‹p_io p2 = io'› unfolding ‹p1 = p› assms(4) by auto then show "False" using ‹io' ≠ []› ‹deadlock_state P q› unfolding deadlock_state_alt_def by blast qed qed lemma preamble_maximal_io_paths_rev : assumes "is_preamble P M q" and "observable M" and "io ∈ L P" and "∄io' . io' ≠ [] ∧ io @ io' ∈ L P" obtains p where "path P (initial P) p" and "p_io p = io" and "target (initial P) p = q" proof - have "acyclic P" and "deadlock_state P q" and "is_submachine P M" and "⋀ q' . q'∈reachable_states P ⟹ (q = q' ∨ ¬ deadlock_state P q')" using assms(1) unfolding is_preamble_def by blast+ have "observable P" using ‹observable M› ‹is_submachine P M› using submachine_observable by blast obtain p where "path P (initial P) p" and "p_io p = io" using ‹io ∈ L P› by auto moreover have "target (initial P) p = q" proof (rule ccontr) assume "target (FSM.initial P) p ≠ q" then have "¬ deadlock_state P (target (FSM.initial P) p)" using ‹⋀ q' . q'∈reachable_states P ⟹ (q = q' ∨ ¬ deadlock_state P q')›[OF reachable_states_intro[OF ‹path P (initial P) p›]] by simp then obtain t where "t ∈ transitions P" and "t_source t = target (initial P) p" by auto then have "path P (initial P) (p @ [t])" using path_append_transition[OF ‹path P (initial P) p›] by auto then have "p_io (p@[t]) ∈ L P" unfolding LS.simps by (metis (mono_tags, lifting) mem_Collect_eq) then have "io @ [(t_input t, t_output t)] ∈ L P" using ‹p_io p = io› by auto then show "False" using assms(4) by auto qed ultimately show ?thesis using that by blast qed lemma is_preamble_is_state : assumes "is_preamble P M q" shows "q ∈ states M" using assms unfolding is_preamble_def by (meson nil path_nil_elim reachable_state_is_state submachine_path) subsection ‹Calculating State Preambles via Backwards Reachability Analysis› fun d_states :: "('a::linorder,'b::linorder,'c) fsm ⇒ 'a ⇒ ('a × 'b) list" where "d_states M q = (if q = initial M then [] else select_inputs (h M) (initial M) (inputs_as_list M) (removeAll q (removeAll (initial M) (states_as_list M))) {q} [])" lemma d_states_index_properties : assumes "i < length (d_states M q)" shows "fst (d_states M q ! i) ∈ (states M - {q})" "fst (d_states M q ! i) ≠ q" "snd (d_states M q ! i) ∈ inputs M" "(∀ qx' ∈ set (take i (d_states M q)) . fst (d_states M q ! i) ≠ fst qx')" "(∃ t ∈ transitions M . t_source t = fst (d_states M q ! i) ∧ t_input t = snd (d_states M q ! i))" "(∀ t ∈ transitions M . (t_source t = fst (d_states M q ! i) ∧ t_input t = snd (d_states M q ! i)) ⟶ (t_target t = q ∨ (∃ qx' ∈ set (take i (d_states M q)) . fst qx' = (t_target t))))" proof - have combined_goals : "fst (d_states M q ! i) ∈ (states M - {q}) ∧ fst (d_states M q ! i) ≠ q ∧ snd (d_states M q ! i) ∈ inputs M ∧ (∀ qx' ∈ set (take i (d_states M q)) . fst (d_states M q ! i) ≠ fst qx') ∧ (∃ t ∈ transitions M . t_source t = fst (d_states M q ! i) ∧ t_input t = snd (d_states M q ! i)) ∧ (∀ t ∈ transitions M . (t_source t = fst (d_states M q ! i) ∧ t_input t = snd (d_states M q ! i)) ⟶ (t_target t = q ∨ (∃ qx' ∈ set (take i (d_states M q)) . fst qx' = (t_target t))))" proof (cases "q = initial M") case True then have "d_states M q = []" by auto then have "False" using assms by auto then show ?thesis by simp next case False then have *: "d_states M q = select_inputs (h M) (initial M) (inputs_as_list M) (removeAll q (removeAll (initial M) (states_as_list M))) {q} []" by auto have "initial M ∈ states M" by auto then have "insert (FSM.initial M) (set (removeAll q (removeAll (FSM.initial M) (states_as_list M)))) = states M - {q}" using states_as_list_set False by auto have "i < length (select_inputs (h M) (FSM.initial M) (inputs_as_list M) (removeAll q (removeAll (FSM.initial M) (states_as_list M))) {q} [])" using assms * by simp moreover have "length [] ≤ i" by auto moreover have "distinct (map fst [])" by auto moreover have "{q} = {q} ∪ set (map fst [])" by auto moreover have "initial M ∉ {q}" using False by auto moreover have "distinct (removeAll q (removeAll (FSM.initial M) (states_as_list M)))" using states_as_list_distinct by (simp add: distinct_removeAll) moreover have "FSM.initial M ∉ set (removeAll q (removeAll (FSM.initial M) (states_as_list M)))" by auto moreover have "set (removeAll q (removeAll (FSM.initial M) (states_as_list M))) ∩ {q} = {}" by auto moreover show ?thesis using select_inputs_index_properties[OF calculation] unfolding *[symmetric] inputs_as_list_set ‹insert (FSM.initial M) (set (removeAll q (removeAll (FSM.initial M) (states_as_list M)))) = states M - {q}› by blast qed then show "fst (d_states M q ! i) ∈ (states M - {q})" "fst (d_states M q ! i) ≠ q" "snd (d_states M q ! i) ∈ inputs M" "(∀ qx' ∈ set (take i (d_states M q)) . fst (d_states M q ! i) ≠ fst qx')" "(∃ t ∈ transitions M . t_source t = fst (d_states M q ! i) ∧ t_input t = snd (d_states M q ! i))" "(∀ t ∈ transitions M . (t_source t = fst (d_states M q ! i) ∧ t_input t = snd (d_states M q ! i)) ⟶ (t_target t = q ∨ (∃ qx' ∈ set (take i (d_states M q)) . fst qx' = (t_target t))))" by blast+ qed lemma d_states_distinct : "distinct (map fst (d_states M q))" proof - have *: "⋀ i q . i < length (map fst (d_states M q)) ⟹ q ∈ set (take i (map fst (d_states M q))) ⟹ ((map fst (d_states M q)) ! i) ≠ q" using d_states_index_properties(2,4) by fastforce then have "(⋀i. i < length (map fst (d_states M q)) ⟹ map fst (d_states M q) ! i ∉ set (take i (map fst (d_states M q))))" proof - fix i :: nat assume a1: "i < length (map fst (d_states M q))" then have "∀p. p ∉ set (take i (d_states M q)) ∨ fst (d_states M q ! i) ≠ fst p" by (metis (no_types) d_states_index_properties(4) length_map) then show "map fst (d_states M q) ! i ∉ set (take i (map fst (d_states M q)))" using a1 by (metis (no_types) length_map list_map_source_elem nth_map take_map) qed then show ?thesis using list_distinct_prefix[of "map fst (d_states M q)"] by blast qed lemma d_states_states : "set (map fst (d_states M q)) ⊆ states M - {q}" using d_states_index_properties(1)[of _ M q] list_property_from_index_property[of "map fst (d_states M q)" "λq' . q' ∈ states M - {q}"] by (simp add: subsetI) lemma d_states_size : assumes "q ∈ states M" shows "length (d_states M q) ≤ size M - 1" proof - show ?thesis using d_states_states[of M q] d_states_distinct[of M q] fsm_states_finite[of M] assms by (metis card_Diff_singleton_if card_mono distinct_card finite_Diff length_map size_def) qed lemma d_states_initial : assumes "qx ∈ set (d_states M q)" and "fst qx = initial M" shows "(last (d_states M q)) = qx" using assms(1) select_inputs_initial[of qx "h M" "initial M" _ _ _ "[]", OF _ assms(2)] by (cases "q = initial M"; auto) lemma d_states_q_noncontainment : shows "¬(∃ qqx ∈ set (d_states M q) . fst qqx = q)" using d_states_index_properties(2) by (metis in_set_conv_nth) lemma d_states_acyclic_paths' : fixes M :: "('a::linorder,'b::linorder,'c) fsm" assumes "path (filter_transitions M (λ t . (t_source t, t_input t) ∈ set (d_states M q))) q' p" and "target q' p = q'" and "p ≠ []" shows "False" proof - from ‹p ≠ []› obtain p' t' where "p = t'#p'" using list.exhaust by blast then have "path (filter_transitions M (λ t . (t_source t, t_input t) ∈ set (d_states M q))) q' (p@[t'])" using assms(1,2) by fastforce define f :: "('a × 'b × 'c × 'a) ⇒ nat" where f_def: "f = (λ t . the (find_index (λ qx . fst qx = t_source t ∧ snd qx = t_input t) (d_states M q)))" have f_prop: "⋀ t . t ∈ set (p@[t']) ⟹ (f t < length (d_states M q)) ∧ ((d_states M q) ! (f t) = (t_source t, t_input t)) ∧ (∀ j < f t . fst (d_states M q ! j) ≠ t_source t)" proof - fix t assume "t ∈ set (p@[t'])" then have "t ∈ set p" using ‹p = t'#p'› by auto then have "t ∈ transitions M" and "(t_source t, t_input t) ∈ set (d_states M q)" using assms(1) path_transitions by fastforce+ then have "∃ qx ∈ set (d_states M q) . (λ qx . fst qx = t_source t ∧ snd qx = t_input t) qx" by (meson fst_conv snd_conv) then have "find_index (λ qx . fst qx = t_source t ∧ snd qx = t_input t) (d_states M q) ≠ None" by (simp add: find_index_exhaustive) then obtain i where *: "find_index (λ qx . fst qx = t_source t ∧ snd qx = t_input t) (d_states M q) = Some i" by auto have "f t < length (d_states M q)" unfolding f_def using find_index_index(1)[OF *] unfolding * by simp moreover have "((d_states M q) ! (f t) = (t_source t, t_input t))" unfolding f_def using find_index_index(2)[OF *] by (metis "*" option.sel prod.collapse) moreover have "∀ j < f t . fst (d_states M q ! j) ≠ t_source t" unfolding f_def using find_index_index(3)[OF *] unfolding * using d_states_distinct[of M q] by (metis (mono_tags, lifting) calculation(1) calculation(2) distinct_conv_nth fst_conv length_map less_imp_le less_le_trans not_less nth_map option.sel snd_conv) ultimately show "(f t < length (d_states M q)) ∧ ((d_states M q) ! (f t) = (t_source t, t_input t)) ∧ (∀ j < f t . fst (d_states M q ! j) ≠ t_source t)" by simp qed have *: "⋀ i . Suc i < length (p@[t']) ⟹ f ((p@[t']) ! i) > f ((p@[t']) ! (Suc i))" proof - fix i assume "Suc i < length (p@[t'])" then have "(p@[t']) ! i ∈ set (p@[t'])" and "(p@[t']) ! (Suc i) ∈ set (p@[t'])" using Suc_lessD nth_mem by blast+ then have "(p@[t']) ! i ∈ transitions M" and "(p@[t']) ! Suc i ∈ transitions M" using path_transitions[OF ‹path (filter_transitions M (λ t . (t_source t, t_input t) ∈ set (d_states M q))) q' (p@[t'])›] using filter_transitions_simps(5) by blast+ have "f ((p@[t']) ! i) < length (d_states M q)" and "(d_states M q) ! (f ((p@[t']) ! i)) = (t_source ((p@[t']) ! i), t_input ((p@[t']) ! i))" and "(∀j<f ((p@[t']) ! i). fst (d_states M q ! j) ≠ t_source ((p@[t']) ! i))" using f_prop[OF ‹(p@[t']) ! i ∈ set (p@[t'])›] by auto have "f ((p@[t']) ! Suc i) < length (d_states M q)" and "(d_states M q) ! (f ((p@[t']) ! Suc i)) = (t_source ((p@[t']) ! Suc i), t_input ((p@[t']) ! Suc i))" and "(∀j<f ((p@[t']) ! Suc i). fst (d_states M q ! j) ≠ t_source ((p@[t']) ! Suc i))" using f_prop[OF ‹(p@[t']) ! Suc i ∈ set (p@[t'])›] by auto have "t_target ((p@[t']) ! i) = t_source ((p@[t']) ! Suc i)" using ‹Suc i < length (p@[t'])› ‹path (filter_transitions M (λ t . (t_source t, t_input t) ∈ set (d_states M q))) q' (p@[t'])› by (simp add: path_source_target_index) then have "t_target ((p@[t']) ! i) ≠ q" using d_states_index_properties(2)[OF ‹f ((p@[t']) ! Suc i) < length (d_states M q)›] unfolding ‹(d_states M q) ! (f ((p@[t']) ! Suc i)) = (t_source ((p@[t']) ! Suc i), t_input ((p@[t']) ! Suc i))› by auto then have "(∃qx'∈set (take (f ((p@[t']) ! i)) (d_states M q)). fst qx' = t_target ((p@[t']) ! i))" using d_states_index_properties(6)[OF ‹f ((p@[t']) ! i) < length (d_states M q)›] unfolding ‹(d_states M q) ! (f ((p@[t']) ! i)) = (t_source ((p@[t']) ! i), t_input ((p@[t']) ! i))› fst_conv snd_conv using ‹(p@[t']) ! i ∈ transitions M› by blast then have "(∃qx'∈set (take (f ((p@[t']) ! i)) (d_states M q)). fst qx' = t_source ((p@[t']) ! Suc i))" unfolding ‹t_target ((p@[t']) ! i) = t_source ((p@[t']) ! Suc i)› by assumption then obtain j where "fst (d_states M q ! j) = t_source ((p@[t']) ! Suc i)" and "j < f ((p@[t']) ! i)" by (metis (no_types, lifting) ‹f ((p@[t']) ! i) < length (d_states M q)› in_set_conv_nth leD length_take min_def_raw nth_take) then show "f ((p@[t']) ! i) > f ((p@[t']) ! (Suc i))" using ‹(∀j<f ((p@[t']) ! Suc i). fst (d_states M q ! j) ≠ t_source ((p@[t']) ! Suc i))› using leI le_less_trans by blast qed have "⋀ i j . j < i ⟹ i < length (p@[t']) ⟹ f ((p@[t']) ! j) > f ((p@[t']) ! i)" using list_index_fun_gt[of "p@[t']" f] * by blast then have "f t' < f t'" unfolding ‹p = t'#p'› by fastforce then show "False" by auto qed lemma d_states_acyclic_paths : fixes M :: "('a::linorder,'b::linorder,'c) fsm" assumes "path (filter_transitions M (λ t . (t_source t, t_input t) ∈ set (d_states M q))) q' p" (is "path ?FM q' p") shows "distinct (visited_states q' p)" proof (rule ccontr) assume "¬ distinct (visited_states q' p)" obtain i j where p1:"take j (drop i p) ≠ []" and p2:"target (target q' (take i p)) (take j (drop i p)) = (target q' (take i p))" and p3:"path ?FM (target q' (take i p)) (take j (drop i p))" using cycle_from_cyclic_path[OF assms ‹¬ distinct (visited_states q' p)›] by blast show "False" using d_states_acyclic_paths'[OF p3 p2 p1] by assumption qed lemma d_states_induces_state_preamble_helper_acyclic : shows "acyclic (filter_transitions M (λ t . (t_source t, t_input t) ∈ set (d_states M q)))" unfolding acyclic.simps using d_states_acyclic_paths by force lemma d_states_induces_state_preamble_helper_single_input : shows "single_input (filter_transitions M (λ t . (t_source t, t_input t) ∈ set (d_states M q)))" (is "single_input ?FM") unfolding single_input.simps filter_transitions_simps by (metis (no_types, lifting) d_states_distinct eq_key_imp_eq_value mem_Collect_eq) lemma d_states_induces_state_preamble : assumes "∃ qx ∈ set (d_states M q) . fst qx = initial M" shows "is_preamble (filter_transitions M (λ t . (t_source t, t_input t) ∈ set (d_states M q))) M q" (is "is_preamble ?S M q") proof (cases "q = initial M") case True then have "d_states M q = []" by auto then show ?thesis using assms(1) by auto next case False have is_acyclic: "acyclic ?S" using d_states_induces_state_preamble_helper_acyclic[of M q] by presburger have is_single_input: "single_input ?S" using d_states_induces_state_preamble_helper_single_input[of M q] by presburger have is_sub : "is_submachine ?S M" unfolding is_submachine.simps filter_transitions_simps by blast have has_deadlock_q : "deadlock_state ?S q" using d_states_q_noncontainment[of M q] unfolding deadlock_state.simps by fastforce have "⋀ q' . q' ∈ reachable_states ?S ⟹ q' ≠ q ⟹ ¬ deadlock_state ?S q'" proof - fix q' assume "q' ∈ reachable_states ?S" and "q' ≠ q" then obtain p where "path ?S (initial ?S) p" and "target (initial ?S) p = q'" unfolding reachable_states_def by auto have "∃ qx ∈ set (d_states M q) . fst qx = q'" proof (cases p rule: rev_cases) case Nil then show ?thesis using assms(1) ‹target (initial ?S) p = q'› unfolding filter_transitions_simps by simp next case (snoc p' t) then have "t ∈ transitions ?S" and "t_target t = q'" using ‹path ?S (initial ?S) p› ‹target (initial ?S) p = q'› by auto then have "(t_source t, t_input t) ∈ set (d_states M q)" by simp then obtain i where "i < length (d_states M q)" and "d_states M q ! i = (t_source t, t_input t)" by (meson in_set_conv_nth) have "t ∈ transitions M" using ‹t ∈ transitions ?S› using is_sub by auto then show ?thesis using ‹t_target t = q'› ‹q' ≠ q› using d_states_index_properties(6)[OF ‹i < length (d_states M q)›] unfolding ‹d_states M q ! i = (t_source t, t_input t)› fst_conv snd_conv by (metis in_set_takeD) qed then obtain qx where "qx ∈ set (d_states M q)" and "fst qx = q'" by blast then have "(∃ t ∈ transitions M . t_source t = fst qx ∧ t_input t = snd qx)" using d_states_index_properties(5)[of _ M q] by (metis in_set_conv_nth) then have "(∃ t ∈ transitions ?S . t_source t = fst qx ∧ t_input t = snd qx)" using ‹qx ∈ set (d_states M q)› by fastforce then show "¬ deadlock_state ?S q'" unfolding deadlock_state.simps using ‹fst qx = q'› by blast qed then have has_states_prop_1 : "⋀ q' . q' ∈ reachable_states ?S ⟹ (q = q' ∨ ¬ deadlock_state ?S q')" by blast have has_states_prop_2 : "⋀ q' x t t'. q' ∈ reachable_states ?S ⟹ x ∈ inputs M ⟹ t ∈ transitions ?S ⟹ t_source t = q' ⟹ t_input t = x ⟹ t'∈ transitions M ⟹ t_source t' = q' ⟹ t_input t' = x ⟹ t' ∈ transitions ?S" by simp have contains_q : "q ∈ reachable_states ?S" using ‹⋀q'. ⟦q' ∈ reachable_states ?S; q' ≠ q⟧ ⟹ ¬ deadlock_state ?S q'› acyclic_deadlock_reachable is_acyclic by blast show ?thesis unfolding is_preamble_def using is_acyclic is_single_input is_sub contains_q has_deadlock_q has_states_prop_1 has_states_prop_2 by blast qed fun calculate_state_preamble_from_input_choices :: "('a::linorder,'b::linorder,'c) fsm ⇒ 'a ⇒ ('a,'b,'c) fsm option" where "calculate_state_preamble_from_input_choices M q = (if q = initial M then Some (initial_preamble M) else (let DS = (d_states M q); DSS = set DS in (case DS of [] ⇒ None | _ ⇒ if fst (last DS) = initial M then Some (filter_transitions M (λ t . (t_source t, t_input t) ∈ DSS)) else None)))" lemma calculate_state_preamble_from_input_choices_soundness : assumes "calculate_state_preamble_from_input_choices M q = Some S" shows "is_preamble S M q" proof (cases "q = initial M") case True then have "S = initial_preamble M" using assms by auto then show ?thesis using is_preamble_initial[of M] True by presburger next case False then have "S = (filter_transitions M (λ t . (t_source t, t_input t) ∈ set (d_states M q)))" and "length (d_states M q) ≠ 0" and "fst (last (d_states M q)) = initial M" using assms by (cases "(d_states M q)"; cases "fst (last (d_states M q)) = initial M"; simp)+ then have "∃ qx ∈ set (d_states M q) . fst qx = initial M" by auto then show ?thesis using d_states_induces_state_preamble unfolding ‹S = (filter_transitions M (λ t . (t_source t, t_input t) ∈ set (d_states M q)))› by blast qed lemma calculate_state_preamble_from_input_choices_exhaustiveness : assumes "∃ S . is_preamble S M q" shows "calculate_state_preamble_from_input_choices M q ≠ None" proof (cases "q = initial M") case True then show ?thesis by auto next case False obtain S where "is_preamble S M q" using assms by blast then have "acyclic S" and "single_input S" and "is_submachine S M" and "q ∈ reachable_states S" and "⋀ q' . q' ∈ reachable_states S ⟹ (q = q' ∨ ¬ deadlock_state S q')" and *: "⋀ q' x . q' ∈ reachable_states S ⟹ x ∈ inputs M ⟹ (∃ t ∈ transitions S . t_source t = q' ∧ t_input t = x) ⟹ (∀ t' ∈ transitions M . t_source t' = q' ∧ t_input t' = x ⟶ t' ∈ transitions S)" unfolding is_preamble_def by blast+ have p1: "(⋀q x. q ∈ reachable_states S ⟹ h S (q, x) ≠ {} ⟹ h S (q, x) = h M (q, x))" proof - fix q x assume "q ∈ reachable_states S" and "h S (q, x) ≠ {}" then have "x ∈ inputs M" using ‹is_submachine S M› fsm_transition_input by force have "(∃ t ∈ transitions S . t_source t = q ∧ t_input t = x)" using ‹h S (q, x) ≠ {}› by fastforce have "⋀ y q'' . (y,q'') ∈ h S (q,x) ⟹ (y,q'') ∈ h M (q,x)" using ‹is_submachine S M› by force moreover have "⋀ y q'' . (y,q'') ∈ h M (q,x) ⟹ (y,q'') ∈ h S (q,x)" using *[OF ‹q ∈ reachable_states S› ‹x ∈ inputs M› ‹(∃ t ∈ transitions S . t_source t = q ∧ t_input t = x)›] unfolding h.simps by force ultimately show "h S (q, x) = h M (q, x)" by force qed have p2: "⋀q'. q' ∈ reachable_states S ⟹ deadlock_state S q' ⟹ q' ∈ {q} ∪ set (map fst [])" using ‹⋀ q' . q' ∈ reachable_states S ⟹ (q = q' ∨ ¬ deadlock_state S q')› by fast have "q ∈ states M" using ‹q ∈ reachable_states S› submachine_reachable_subset[OF ‹is_submachine S M›] by (meson assms is_preamble_is_state) then have p3: "states M = insert (FSM.initial S) (set (removeAll q (removeAll (initial M) (states_as_list M))) ∪ {q} ∪ set (map fst []))" using states_as_list_set[of M] fsm_initial[of M] unfolding submachine_simps[OF ‹is_submachine S M›] by auto have p4: "initial S ∉ set (removeAll q (removeAll (initial M) (states_as_list M))) ∪ {q} ∪ set (map fst [])" using False unfolding submachine_simps[OF ‹is_submachine S M›] by force have "fst (last (d_states M q)) = FSM.initial M" and "length (d_states M q) > 0" using False select_inputs_from_submachine[OF ‹single_input S› ‹acyclic S› ‹is_submachine S M› p1 p2 p3 p4] unfolding d_states.simps submachine_simps[OF ‹is_submachine S M›] by auto have "(d_states M q) ≠ []" using ‹length (d_states M q) > 0› by auto then obtain dl dl' where "(d_states M q) = dl # dl'" using list.exhaust by blast then have "(fst (last (dl#dl')) = FSM.initial M) = True" using ‹fst (last (d_states M q)) = FSM.initial M› by simp then show ?thesis using False unfolding calculate_state_preamble_from_input_choices.simps Let_def ‹(d_states M q) = dl # dl'› by auto qed subsection ‹Minimal Sequences to Failures extending Preambles› definition sequence_to_failure_extending_preamble_path :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ ('a × ('a,'b,'c) fsm) set ⇒ ('a×'b×'c×'a) list ⇒ ('b × 'c) list ⇒ bool" where "sequence_to_failure_extending_preamble_path M M' PS p io = (∃ q P . q ∈ states M ∧ (q,P) ∈ PS ∧ path P (initial P) p ∧ target (initial P) p = q ∧ ((p_io p) @ butlast io) ∈ L M ∧ ((p_io p) @ io) ∉ L M ∧ ((p_io p) @ io) ∈ L M')" lemma sequence_to_failure_extending_preamble_ex : assumes "(initial M, (initial_preamble M)) ∈ PS" (is "(initial M,?P) ∈ PS") and "¬ L M' ⊆ L M" obtains p io where "sequence_to_failure_extending_preamble_path M M' PS p io" proof - obtain io where "io ∈ L M' - L M" using ‹¬ L M' ⊆ L M› by auto obtain j where "take j io ∈ L M" and "take (Suc j) io ∉ L M" proof - have "∃ j . take j io ∈ L M ∧ take (Suc j) io ∉ L M" proof (rule ccontr) assume "∄j. take j io ∈ LS M (initial M) ∧ take (Suc j) io ∉ LS M (initial M)" then have *: "⋀ j . take j io ∈ LS M (initial M) ⟹ take (Suc j) io ∈ LS M (initial M)" by blast have "⋀ j . take j io ∈ LS M (initial M)" proof - fix j show "take j io ∈ LS M (initial M)" using * by (induction j; auto) qed then have "take (length io) io ∈ L M" by blast then show "False" using ‹io ∈ L M' - L M› by auto qed then show ?thesis using that by blast qed have "⋀ i . take i io ∈ L M'" proof - fix i show "take i io ∈ L M'" using ‹io ∈ L M' - L M› language_prefix[of "take i io" "drop i io" M' "initial M'"] by auto qed let ?io = "take (Suc j) io" have "initial M ∈ states M" by auto moreover note ‹(initial M, (initial_preamble M)) ∈ PS› moreover have "path ?P (initial ?P) []" by force moreover have "((p_io []) @ butlast ?io) ∈ L M" using ‹take j io ∈ L M› unfolding List.list.map(1) append_Nil by (metis Diff_iff One_nat_def ‹io ∈ LS M' (initial M') - LS M (initial M)› butlast_take diff_Suc_Suc minus_nat.diff_0 not_less_eq_eq take_all) moreover have "((p_io []) @ ?io) ∉ L M" using ‹take (Suc j) io ∉ L M› by auto moreover have "((p_io []) @ ?io) ∈ L M'" using ‹⋀ i . take i io ∈ L M'› by auto ultimately have "sequence_to_failure_extending_preamble_path M M' PS [] ?io" unfolding sequence_to_failure_extending_preamble_path_def by force then show ?thesis using that by blast qed definition minimal_sequence_to_failure_extending_preamble_path :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ ('a × ('a,'b,'c) fsm) set ⇒ ('a×'b×'c×'a) list ⇒ ('b × 'c) list ⇒ bool" where "minimal_sequence_to_failure_extending_preamble_path M M' PS p io = ((sequence_to_failure_extending_preamble_path M M' PS p io) ∧ (∀ p' io' . sequence_to_failure_extending_preamble_path M M' PS p' io' ⟶ length io ≤ length io'))" lemma minimal_sequence_to_failure_extending_preamble_ex : assumes "(initial M, (initial_preamble M)) ∈ PS" (is "(initial M,?P) ∈ PS") and "¬ L M' ⊆ L M" obtains p io where "minimal_sequence_to_failure_extending_preamble_path M M' PS p io" proof - let ?ios = "{io . ∃ p . sequence_to_failure_extending_preamble_path M M' PS p io}" let ?io_min = "arg_min length (λio . io ∈ ?ios)" have "?ios ≠ {}" using sequence_to_failure_extending_preamble_ex[OF assms] by blast then have "?io_min ∈ ?ios" and "(∀ io' ∈ ?ios . length ?io_min ≤ length io')" by (meson arg_min_nat_lemma some_in_eq)+ obtain p where "sequence_to_failure_extending_preamble_path M M' PS p ?io_min" using ‹?io_min ∈ ?ios› by auto moreover have "(∀ p' io' . sequence_to_failure_extending_preamble_path M M' PS p' io' ⟶ length ?io_min ≤ length io')" using ‹(∀ io' ∈ ?ios . length ?io_min ≤ length io')› by blast ultimately show ?thesis using that[of p ?io_min] unfolding minimal_sequence_to_failure_extending_preamble_path_def by blast qed lemma minimal_sequence_to_failure_extending_preamble_no_repetitions_along_path : assumes "minimal_sequence_to_failure_extending_preamble_path M M' PS pP io" and "observable M" and "path M (target (initial M) pP) p" and "p_io p = butlast io" and "q' ∈ io_targets M' (p_io pP) (initial M')" and "path M' q' p'" and "p_io p' = io" and "i < j" and "j < length (butlast io)" and "⋀ q P. (q, P) ∈ PS ⟹ is_preamble P M q" shows "t_target (p ! i) ≠ t_target (p ! j) ∨ t_target (p' ! i) ≠ t_target (p' ! j)" proof (rule ccontr) assume "¬ (t_target (p ! i) ≠ t_target (p ! j) ∨ t_target (p' ! i) ≠ t_target (p' ! j))" (* cut the loop and create a shorter path with the same target as p (p') *) then have "t_target (p ! i) = t_target (p ! j)" and "t_target (p' ! i) = t_target (p' ! j)" by blast+ have "sequence_to_failure_extending_preamble_path M M' PS pP io" and "⋀ p' io' . sequence_to_failure_extending_preamble_path M M' PS p' io' ⟹ length io ≤ length io'" using ‹minimal_sequence_to_failure_extending_preamble_path M M' PS pP io› unfolding minimal_sequence_to_failure_extending_preamble_path_def by blast+ obtain q P where "(q,P) ∈ PS" and "path P (initial P) pP" and "target (initial P) pP = q" and "((p_io pP) @ butlast io) ∈ L M" and "((p_io pP) @ io) ∉ L M" and "((p_io pP) @ io) ∈ L M'" using ‹sequence_to_failure_extending_preamble_path M M' PS pP io› unfolding sequence_to_failure_extending_preamble_path_def by blast have "is_preamble P M q" using ‹(q,P) ∈ PS› ‹⋀ q P. (q, P) ∈ PS ⟹ is_preamble P M q› by blast then have "q ∈ states M" unfolding is_preamble_def by (metis ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› path_target_is_state submachine_path) have "initial P = initial M" using ‹is_preamble P M q› unfolding is_preamble_def by auto have "path M (initial M) pP" using ‹is_preamble P M q› unfolding is_preamble_def using submachine_path_initial using ‹path P (FSM.initial P) pP› by blast have "target (initial M) pP = q" using ‹target (initial P) pP = q› unfolding ‹initial P = initial M› by assumption then have "path M q p" using ‹path M (target (initial M) pP) p› by auto have "io ≠ []" using ‹((p_io pP) @ butlast io) ∈ L M› ‹((p_io pP) @ io) ∉ L M› by auto then have "length p' > 0" using ‹p_io p' = io› by auto then have "p' = (butlast p')@[last p']" by auto then have "path M' q' ((butlast p')@[last p'])" using ‹path M' q' p'› by simp then have "path M' q' (butlast p')" and "(last p') ∈ transitions M'" and "t_source (last p') = target q' (butlast p')" by auto have "p_io (butlast p') = butlast io" using ‹p' = (butlast p')@[last p']› ‹p_io p' = io› using map_butlast by auto let ?p = "((take (Suc i) p) @ (drop (Suc j) p))" let ?pCut = "(drop (Suc i) (take (Suc j) p))" (* the loop cut out of p *) let ?p' = "((take (Suc i) (butlast p')) @ (drop (Suc j) (butlast p')))" have "j < length p" using ‹j < length (butlast io)› ‹p_io p = butlast io› by (metis (no_types, lifting) length_map) have "j < length (butlast p')" using ‹j < length (butlast io)› ‹p_io p' = io› ‹p' = (butlast p')@[last p']› by auto then have "t_target ((butlast p') ! i) = t_target ((butlast p') ! j)" using ‹t_target (p' ! i) = t_target (p' ! j)› by (simp add: ‹i < j› dual_order.strict_trans nth_butlast) have "path M q ?p" and "target q ?p = target q p" and "length ?p < length p" and "path M (target q (take (Suc i) p)) ?pCut" and "target (target q (take (Suc i) p)) ?pCut = target q (take (Suc i) p)" using path_loop_cut[OF ‹path M q p› ‹t_target (p ! i) = t_target (p ! j)› ‹i < j› ‹j < length p›] by blast+ have "path M' q' ?p'" and "target q' ?p' = target q' (butlast p')" and "length ?p' < length (butlast p')" using path_loop_cut[OF ‹path M' q' (butlast p')› ‹t_target ((butlast p') ! i) = t_target ((butlast p') ! j)› ‹i < j› ‹j < length (butlast p')›] by blast+ have "path M' q' (?p'@[last p'])" using ‹t_source (last p') = target q' (butlast p')› using path_append_transition[OF ‹path M' q' ?p'› ‹(last p') ∈ transitions M'›] unfolding ‹target q' ?p' = target q' (butlast p')› by simp have "p_io ?p' = p_io ?p" using ‹p_io p = butlast io› ‹p_io (butlast p') = butlast io› by (metis (no_types, lifting) drop_map map_append take_map) have min_prop: "length (p_io (?p'@[last p'])) < length io" using ‹length ?p' < length (butlast p')› ‹p_io p' = io› unfolding length_map[of "(λ t . (t_input t, t_output t))"] by auto (* show that the shorter path would constitute a shorter seq to a failure, contradicting the minimality assumption on io *) have "q ∈ io_targets M (p_io pP) (initial M)" using ‹path M (initial M) pP› ‹target (initial M) pP = q› unfolding io_targets.simps by blast have "((p_io pP) @ (p_io ?p)) ∈ L M" using language_io_target_append[OF ‹q ∈ io_targets M (p_io pP) (initial M)›, of "p_io ?p"] ‹path M q ?p› unfolding LS.simps by blast then have p1: "((p_io pP) @ butlast (p_io (?p' @ [last p']))) ∈ L M" unfolding ‹p_io ?p' = p_io ?p›[symmetric] by (metis (no_types, lifting) butlast_snoc map_butlast) have p2: "((p_io pP) @ (p_io (?p' @ [last p']))) ∉ L M" proof assume "((p_io pP) @ (p_io (?p' @ [last p']))) ∈ L M" then obtain pCntr where "path M (initial M) pCntr" and "p_io pCntr = (p_io pP) @ (p_io (?p' @ [last p']))" by auto let ?pCntr1 = "(take (length (p_io pP)) pCntr)" let ?pCntr23 = "(drop (length (p_io pP)) pCntr)" have "path M (initial M) ?pCntr1" and "p_io ?pCntr1 = p_io pP" and "path M (target (initial M) ?pCntr1) ?pCntr23" and "p_io ?pCntr23 = p_io (?p' @ [last p'])" using path_io_split[OF ‹path M (initial M) pCntr› ‹p_io pCntr = (p_io pP) @ (p_io (?p' @ [last p']))›] by blast+ let ?pCntr2 = "(take (length (p_io (take (Suc i) (butlast p') @ drop (Suc j) (butlast p')))) (drop (length (p_io pP)) pCntr))" let ?pCntr3 = "(drop (length (p_io (take (Suc i) (butlast p') @ drop (Suc j) (butlast p')))) (drop (length (p_io pP)) pCntr))" have "p_io ?pCntr23 = p_io ?p' @ p_io [last p']" using ‹p_io ?pCntr23 = p_io (?p' @ [last p'])› by auto have "path M (target (initial M) ?pCntr1) ?pCntr2" and "p_io ?pCntr2 = p_io ?p'" and "path M (target (target (initial M) ?pCntr1) ?pCntr2) ?pCntr3" and "p_io ?pCntr3 = p_io [last p']" using path_io_split[OF ‹path M (target (initial M) ?pCntr1) ?pCntr23› ‹p_io ?pCntr23 = p_io ?p' @ p_io [last p']›] by blast+ have "?pCntr1 = pP" using observable_path_unique[OF ‹observable M› ‹path M (initial M) ?pCntr1› ‹path M (initial M) pP› ‹p_io ?pCntr1 = p_io pP›] by assumption then have "(target (initial M) ?pCntr1) = q" using ‹target (initial M) pP = q› by auto then have "path M q ?pCntr2" and "path M (target q ?pCntr2) ?pCntr3" using ‹path M (target (initial M) ?pCntr1) ?pCntr2› ‹path M (target (target (initial M) ?pCntr1) ?pCntr2) ?pCntr3› by auto have "?pCntr2 = ?p" using observable_path_unique[OF ‹observable M› ‹path M q ?pCntr2› ‹path M q ?p› ] ‹p_io ?pCntr2 = p_io ?p'› unfolding ‹p_io ?p' = p_io ?p› by blast then have "(target q ?pCntr2) = (target q ?p)" by auto then have "(target q ?pCntr2) = (target q p)" using ‹target q ?p = target q p› by auto have "p_io ?pCntr3 = [last io]" using ‹p_io ?pCntr3 = p_io [last p']› by (metis (mono_tags, lifting) ‹io ≠ []› assms(7) last_map list.simps(8) list.simps(9)) have "path M (initial M) (pP @ p @ ?pCntr3)" using ‹path M (initial M) pP› ‹target (initial M) pP = q› ‹path M q p› ‹path M (target q ?pCntr2) ?pCntr3› unfolding ‹(target q ?pCntr2) = (target q p)› by auto moreover have "p_io (pP @ p @ ?pCntr3) = ((p_io pP) @ io)" using ‹p_io p = butlast io› ‹p_io ?pCntr3 = [last io]› by (simp add: ‹io ≠ []›) ultimately have "((p_io pP) @ io) ∈ L M" by (metis (mono_tags, lifting) language_state_containment) then show "False" using ‹((p_io pP) @ io) ∉ L M› by simp qed have p3: "((p_io pP) @ (p_io (?p' @ [last p']))) ∈ L M'" using language_io_target_append[OF ‹q' ∈ io_targets M' (p_io pP) (initial M')›, of "(p_io (?p' @ [last p']))"] using ‹path M' q' (?p'@[last p'])› unfolding LS.simps by (metis (mono_tags, lifting) mem_Collect_eq) have "sequence_to_failure_extending_preamble_path M M' PS pP (p_io (?p' @ [last p']))" unfolding sequence_to_failure_extending_preamble_path_def using ‹q ∈ states M› ‹(q,P) ∈ PS› ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› p1 p2 p3 by blast show "False" using ‹⋀ p' io' . sequence_to_failure_extending_preamble_path M M' PS p' io' ⟹ length io ≤ length io'›[OF ‹sequence_to_failure_extending_preamble_path M M' PS pP (p_io (?p' @ [last p']))›] min_prop by simp qed lemma minimal_sequence_to_failure_extending_preamble_no_repetitions_with_other_preambles : assumes "minimal_sequence_to_failure_extending_preamble_path M M' PS pP io" and "observable M" and "path M (target (initial M) pP) p" and "p_io p = butlast io" and "q' ∈ io_targets M' (p_io pP) (initial M')" and "path M' q' p'" and "p_io p' = io" and "⋀ q P. (q, P) ∈ PS ⟹ is_preamble P M q" and "i < length (butlast io)" and "(t_target (p ! i), P') ∈ PS" and "path P' (initial P') pP'" and "target (initial P') pP' = t_target (p ! i)" shows "t_target (p' ! i) ∉ io_targets M' (p_io pP') (initial M')" proof assume "t_target (p' ! i) ∈ io_targets M' (p_io pP') (FSM.initial M')" (* Contradiction: (drop (Suc i) io) after (p_io pP') is a shorter sequence to a failure than io *) have "sequence_to_failure_extending_preamble_path M M' PS pP io" and "⋀ p' io' . sequence_to_failure_extending_preamble_path M M' PS p' io' ⟹ length io ≤ length io'" using ‹minimal_sequence_to_failure_extending_preamble_path M M' PS pP io› unfolding minimal_sequence_to_failure_extending_preamble_path_def by blast+ obtain q P where "(q,P) ∈ PS" and "path P (initial P) pP" and "target (initial P) pP = q" and "((p_io pP) @ butlast io) ∈ L M" and "((p_io pP) @ io) ∉ L M" and "((p_io pP) @ io) ∈ L M'" using ‹sequence_to_failure_extending_preamble_path M M' PS pP io› unfolding sequence_to_failure_extending_preamble_path_def by blast have "is_preamble P M q" using ‹(q,P) ∈ PS› ‹⋀ q P. (q, P) ∈ PS ⟹ is_preamble P M q› by blast then have "q ∈ states M" unfolding is_preamble_def by (metis ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› path_target_is_state submachine_path) have "initial P = initial M" using ‹is_preamble P M q› unfolding is_preamble_def by auto have "path M (initial M) pP" using ‹is_preamble P M q› unfolding is_preamble_def using submachine_path_initial using ‹path P (FSM.initial P) pP› by blast have "target (initial M) pP = q" using ‹target (initial P) pP = q› unfolding ‹initial P = initial M› by assumption then have "path M q p" using ‹path M (target (initial M) pP) p› by auto have "is_preamble P' M (t_target (p ! i))" using ‹(t_target (p ! i), P') ∈ PS› ‹⋀ q P. (q, P) ∈ PS ⟹ is_preamble P M q› by blast then have "(t_target (p ! i)) ∈ states M" unfolding is_preamble_def by (metis ‹path P' (initial P') pP'› ‹target (initial P') pP' = t_target (p ! i)› path_target_is_state submachine_path) have "initial P' = initial M" using ‹is_preamble P' M (t_target (p ! i))› unfolding is_preamble_def by auto have "path M (initial M) pP'" using ‹is_preamble P' M (t_target (p ! i))› unfolding is_preamble_def using submachine_path_initial using ‹path P' (initial P') pP'› by blast have "target (initial M) pP' = t_target (p ! i)" using ‹target (initial P') pP' = t_target (p ! i)› unfolding ‹initial P' = initial M› by simp have "io ≠ []" using ‹((p_io pP) @ butlast io) ∈ L M› ‹((p_io pP) @ io) ∉ L M› by auto then have "length p' > 0" using ‹p_io p' = io› by auto then have "p' = (butlast p')@[last p']" by auto then have "path M' q' ((butlast p')@[last p'])" using ‹path M' q' p'› by simp then have "path M' q' (butlast p')" and "(last p') ∈ transitions M'" and "t_source (last p') = target q' (butlast p')" by auto have "p_io (butlast p') = butlast io" using ‹p' = (butlast p')@[last p']› ‹p_io p' = io› using map_butlast by auto have "butlast io ≠ []" using assms(9) by fastforce let ?p = "(drop (Suc i) p)" let ?p' = "(drop (Suc i) (butlast p'))" have "i < length p" using ‹i < length (butlast io)› unfolding ‹p_io p = butlast io›[symmetric] length_map[of "(λ t . (t_input t, t_output t))"] by assumption then have "p ! i = last (take (Suc i) p)" by (simp add: take_last_index) then have "t_target (p ! i) = target q (take (Suc i) p)" unfolding target.simps visited_states.simps by (metis (no_types, lifting) ‹i < length p› gr_implies_not0 last_ConsR length_0_conv length_map nth_map old.nat.distinct(2) take_eq_Nil take_last_index take_map) have "p = (take (Suc i) p @ ?p)" by simp then have "p_io p = (p_io (take (Suc i) p)) @ (p_io ?p)" by (metis map_append) have "(length (p_io (take (Suc i) p))) = Suc i" using ‹i < length p› unfolding length_map[of "(λ t . (t_input t, t_output t))"] by auto have "path M (t_target (p ! i)) ?p" using path_io_split(3)[OF ‹path M q p› ‹p_io p = (p_io (take (Suc i) p)) @ (p_io ?p)›] unfolding ‹(length (p_io (take (Suc i) p))) = Suc i› ‹t_target (p ! i) = target q (take (Suc i) p)› by assumption then have "path M (initial M) (pP' @ ?p)" using ‹path M (initial M) pP'› ‹target (initial M) pP' = t_target (p ! i)› by (simp add: path_append) let ?io = "(p_io ?p) @ [last io]" have is_shorter: "length ?io < length io" proof - have "p_io ?p = drop (Suc i) (butlast io)" by (metis assms(4) drop_map) moreover have "length (drop (Suc i) (butlast io)) < length (butlast io)" using assms(9) by auto ultimately have "length (p_io ?p) < length (butlast io)" by simp then show ?thesis by auto qed have p1: "((p_io pP') @ (p_io ?p)) ∈ L M" using ‹path M (initial M) (pP' @ ?p)› by (metis (mono_tags, lifting) language_state_containment map_append) have p2: "((p_io pP') @ ?io