Theory State_Preamble
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 -
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
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))"
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))"
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
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')"
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) ∉ L M"
proof
assume "((p_io pP') @ ?io) ∈ L M"
then obtain pCntr where "path M (initial M) pCntr" and "p_io pCntr = (p_io pP') @ (p_io ?p) @ [last io]"
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 io]"
using path_io_split[OF ‹path M (initial M) pCntr› ‹p_io pCntr = (p_io pP') @ (p_io ?p) @ [last io]›]
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) = (t_target (p ! i))"
using ‹target (initial M) pP' = (t_target (p ! i))› by auto
then have "path M (t_target (p ! i)) ?pCntr23"
using ‹path M (target (initial M) ?pCntr1) ?pCntr23›
by simp
have "path M q (take (Suc i) p)"
using ‹path M q p›
by (metis append_take_drop_id path_prefix)
then have "path M q ((take (Suc i) p) @ ?pCntr23)"
using ‹path M (target (initial M) ?pCntr1) ?pCntr23›
unfolding ‹(target (initial M) ?pCntr1) = (t_target (p ! i))›
unfolding ‹t_target (p ! i) = target q (take (Suc i) p)›
by auto
then have "path M (initial M) (pP @ ((take (Suc i) p) @ ?pCntr23))"
using ‹path M (initial M) pP› ‹target (initial M) pP = q›
by auto
moreover have "p_io (pP @ ((take (Suc i) p) @ ?pCntr23)) = p_io pP @ io"
using ‹io ≠ []› ‹p_io (drop (length (p_io pP')) pCntr) = p_io (drop (Suc i) p) @ [last io]› ‹p_io p = p_io (take (Suc i) p) @ p_io (drop (Suc i) p)› append_butlast_last_id assms(4)
by fastforce
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') @ ?io) ∈ L M'"
proof -
have "i < length (butlast p')"
using ‹i < length (butlast io)› unfolding ‹p_io p' = io›[symmetric]
using length_map[of "(λ t . (t_input t, t_output t))"]
by simp
then have "butlast p' ! i = last (take (Suc i) (butlast p'))"
by (simp add: nth_butlast take_last_index)
moreover have "(take (Suc i) (butlast p')) ≠ []"
by (metis Zero_not_Suc ‹i < length (butlast p')› list.size(3) not_less0 take_eq_Nil)
ultimately have "(target q' (take (Suc i) (butlast p'))) = t_target ((butlast p') ! i)"
unfolding target.simps visited_states.simps
by (simp add: last_map)
moreover have "(butlast p') ! i = p' ! i"
using ‹i < length (butlast p')›
by (simp add: nth_butlast)
ultimately have "(target q' (take (Suc i) (butlast p'))) = t_target (p' ! i)"
by simp
have "p' = (take (Suc i) (butlast p')) @ ?p' @ [last p']"
by (metis ‹p' = butlast p' @ [last p']› append.assoc append_take_drop_id)
then have "path M' (target q' (take (Suc i) (butlast p'))) (?p' @ [last p'])"
by (metis assms(6) path_suffix)
then have "path M' (t_target (p' ! i)) (?p' @ [last p'])"
unfolding ‹(target q' (take (Suc i) (butlast p'))) = t_target (p' ! i)› by assumption
moreover have "p_io (?p' @ [last p']) = ?io"
by (metis (no_types, lifting) ‹io ≠ []› ‹p' = butlast p' @ [last p']› ‹p_io (butlast p') = butlast io› append_butlast_last_id assms(4) assms(7) drop_map map_append same_append_eq)
ultimately have "?io ∈ LS M' (t_target (p' ! i))"
by (metis (mono_tags, lifting) language_state_containment)
show "((p_io pP') @ ?io) ∈ L M'"
using language_io_target_append[OF ‹t_target (p' ! i) ∈ io_targets M' (p_io pP') (FSM.initial M')› ‹?io ∈ LS M' (t_target (p' ! i))›]
by assumption
qed
have *: "⋀ xs x . butlast (xs @ [x]) = xs" by auto
have "sequence_to_failure_extending_preamble_path M M' PS pP' ?io"
unfolding sequence_to_failure_extending_preamble_path_def
using ‹t_target (p ! i) ∈ states M› assms(10-12) p1 p2 p3
unfolding * by blast
then have "length io ≤ length ?io"
using ‹⋀ p' io' . sequence_to_failure_extending_preamble_path M M' PS p' io' ⟹ length io ≤ length io'›
by blast
then show "False"
using is_shorter
by simp
qed
end