Theory FSM
theory FSM
imports
"Transition_Systems_and_Automata.Sequence_Zip"
"Transition_Systems_and_Automata.Transition_System"
"Transition_Systems_and_Automata.Transition_System_Extra"
"Transition_Systems_and_Automata.Transition_System_Construction"
begin
section ‹ Finite state machines ›
text ‹
We formalise finite state machines as a 4-tuples, omitting the explicit formulation of the state
set,as it can easily be calculated from the successor function.
This definition does not require the successor function to be restricted to the input or output
alphabet, which is later expressed by the property @{verbatim well_formed}, together with the
finiteness of the state set.
›
record ('in, 'out, 'state) FSM =
succ :: "('in × 'out) ⇒ 'state ⇒ 'state set"
inputs :: "'in set"
outputs :: "'out set"
initial :: "'state"
subsection ‹ FSMs as transition systems ›
text ‹
We interpret FSMs as transition systems with a singleton initial state set, based on
\<^cite>‹"Transition_Systems_and_Automata-AFP"›.
›
global_interpretation FSM : transition_system_initial
"λ a p. snd a"
"λ a p. snd a ∈ succ A (fst a) p"
"λ p. p = initial A"
for A
defines path = FSM.path
and run = FSM.run
and reachable = FSM.reachable
and nodes = FSM.nodes
by this
abbreviation "size_FSM M ≡ card (nodes M)"
notation
size_FSM ("(|_|)")
subsection ‹ Language ›
text ‹
The following definitions establish basic notions for FSMs similarly to those of nondeterministic
finite automata as defined in \<^cite>‹"Transition_Systems_and_Automata-AFP"›.
In particular, the language of an FSM state are the IO-parts of the paths in the FSM enabled from
that state.
›
abbreviation "target ≡ FSM.target"
abbreviation "states ≡ FSM.states"
abbreviation "trace ≡ FSM.trace"
abbreviation successors :: "('in, 'out, 'state, 'more) FSM_scheme ⇒ 'state ⇒ 'state set" where
"successors ≡ FSM.successors TYPE('in) TYPE('out) TYPE('more)"
lemma states_alt_def: "states r p = map snd r"
by (induct r arbitrary: p) (auto)
lemma trace_alt_def: "trace r p = smap snd r"
by (coinduction arbitrary: r p) (auto)
definition language_state :: "('in, 'out, 'state) FSM ⇒ 'state
⇒ ('in × 'out) list set" ("LS")
where
"language_state M q ≡ {map fst r |r . path M r q}"
text ‹
The language of an FSM is the language of its initial state.
›
abbreviation "L M ≡ LS M (initial M)"
lemma language_state_alt_def : "LS M q = {io | io tr . path M (io || tr) q ∧ length io = length tr}"
proof -
have "LS M q ⊆ { io | io tr . path M (io || tr) q ∧ length io = length tr }"
proof
fix xr assume xr_assm : "xr ∈ LS M q"
then obtain r where r_def : "map fst r = xr" "path M r q"
unfolding language_state_def by auto
then obtain xs ys where xr_split : "xr = xs || ys"
"length xs = length ys"
"length xs = length xr"
by (metis length_map zip_map_fst_snd)
then have "(xs || ys) ∈ { io | io tr . path M (io || tr) q ∧ length io = length tr }"
proof -
have f1: "xs || ys = map fst r"
by (simp add: r_def(1) xr_split(1))
then have f2: "path M ((xs || ys) || take (min (length (xs || ys)) (length (map snd r)))
(map snd r)) q"
by (simp add: r_def(2))
have "length (xs || ys) = length
(take (min (length (xs || ys)) (length (map snd r))) (map snd r))"
using f1 by force
then show ?thesis
using f2 by blast
qed
then show "xr ∈ { io | io tr . path M (io || tr) q ∧ length io = length tr }"
using xr_split by metis
qed
moreover have "{ io | io tr . path M (io || tr) q ∧ length io = length tr } ⊆ LS M q"
proof
fix xs assume xs_assm : "xs ∈ { io | io tr . path M (io || tr) q ∧ length io = length tr }"
then obtain ys where ys_def : "path M (xs || ys) q" "length xs = length ys"
by auto
then have "xs = map fst (xs || ys)"
by auto
then show "xs ∈ LS M q"
using ys_def unfolding language_state_def by blast
qed
ultimately show ?thesis
by auto
qed
lemma language_state[intro]:
assumes "path M (w || r) q" "length w = length r"
shows "w ∈ LS M q"
using assms unfolding language_state_def by force
lemma language_state_elim[elim]:
assumes "w ∈ LS M q"
obtains r
where "path M (w || r) q" "length w = length r"
using assms unfolding language_state_def by (force iff: split_zip_ex)
lemma language_state_split:
assumes "w1 @ w2 ∈ LS M q"
obtains tr1 tr2
where "path M (w1 || tr1) q" "length w1 = length tr1"
"path M (w2 || tr2) (target (w1 || tr1) q)" "length w2 = length tr2"
proof -
obtain tr where tr_def : "path M ((w1 @ w2) || tr) q" "length (w1 @ w2) = length tr"
using assms by blast
let ?tr1 = "take (length w1) tr"
let ?tr2 = "drop (length w1) tr"
have tr_split : "?tr1 @ ?tr2 = tr"
by auto
then show ?thesis
proof -
have f1: "length w1 + length w2 = length tr"
using tr_def(2) by auto
then have f2: "length w2 = length tr - length w1"
by presburger
then have "length w1 = length (take (length w1) tr)"
using f1 by (metis (no_types) tr_split diff_add_inverse2 length_append length_drop)
then show ?thesis
using f2 by (metis (no_types) FSM.path_append_elim length_drop that tr_def(1) zip_append1)
qed
qed
lemma language_state_prefix :
assumes "w1 @ w2 ∈ LS M q"
shows "w1 ∈ LS M q"
using assms by (meson language_state language_state_split)
lemma succ_nodes :
fixes A :: "('a,'b,'c) FSM"
and w :: "('a × 'b)"
assumes "q2 ∈ succ A w q1"
and "q1 ∈ nodes A"
shows "q2 ∈ nodes A"
proof -
obtain x y where "w = (x,y)"
by (meson surj_pair)
then have "q2 ∈ successors A q1"
using assms by auto
then have "q2 ∈ reachable A q1"
by blast
then have "q2 ∈ reachable A (initial A)"
using assms by blast
then show "q2 ∈ nodes A"
by blast
qed
lemma states_target_index :
assumes "i < length p"
shows "(states p q1) ! i = target (take (Suc i) p) q1"
using assms by auto
subsection ‹ Product machine for language intersection ›
text ‹
The following describes the construction of a product machine from two FSMs @{verbatim M1}
and @{verbatim M2} such that the language of the product machine is the intersection of the
language of @{verbatim M1} and the language of @{verbatim M2}.
›
definition product :: "('in, 'out, 'state1) FSM ⇒ ('in, 'out, 'state2) FSM ⇒
('in, 'out, 'state1 ×'state2) FSM" where
"product A B ≡
⦇
succ = λ a (p⇩1, p⇩2). succ A a p⇩1 × succ B a p⇩2,
inputs = inputs A ∪ inputs B,
outputs = outputs A ∪ outputs B,
initial = (initial A, initial B)
⦈"
lemma product_simps[simp]:
"succ (product A B) a (p⇩1, p⇩2) = succ A a p⇩1 × succ B a p⇩2"
"inputs (product A B) = inputs A ∪ inputs B"
"outputs (product A B) = outputs A ∪ outputs B"
"initial (product A B) = (initial A, initial B)"
unfolding product_def by simp+
lemma product_target[simp]:
assumes "length w = length r⇩1" "length r⇩1 = length r⇩2"
shows "target (w || r⇩1 || r⇩2) (p⇩1, p⇩2) = (target (w || r⇩1) p⇩1, target (w || r⇩2) p⇩2)"
using assms by (induct arbitrary: p⇩1 p⇩2 rule: list_induct3) (auto)
lemma product_path[iff]:
assumes "length w = length r⇩1" "length r⇩1 = length r⇩2"
shows "path (product A B) (w || r⇩1 || r⇩2) (p⇩1, p⇩2) ⟷ path A (w || r⇩1) p⇩1 ∧ path B (w || r⇩2) p⇩2"
using assms by (induct arbitrary: p⇩1 p⇩2 rule: list_induct3) (auto)
lemma product_language_state[simp]: "LS (product A B) (q1,q2) = LS A q1 ∩ LS B q2"
by (fastforce iff: split_zip)
lemma product_nodes :
"nodes (product A B) ⊆ nodes A × nodes B"
proof
fix q assume "q ∈ nodes (product A B)"
then show "q ∈ nodes A × nodes B"
proof (induction rule: FSM.nodes.induct)
case (initial p)
then show ?case by auto
next
case (execute p a)
then have "fst p ∈ nodes A" "snd p ∈ nodes B"
by auto
have "snd a ∈ (succ A (fst a) (fst p)) × (succ B (fst a) (snd p))"
using execute by auto
then have "fst (snd a) ∈ succ A (fst a) (fst p)"
"snd (snd a) ∈ succ B (fst a) (snd p)"
by auto
have "fst (snd a) ∈ nodes A"
using ‹fst p ∈ nodes A› ‹fst (snd a) ∈ succ A (fst a) (fst p)›
by (metis FSM.nodes.simps fst_conv snd_conv)
moreover have "snd (snd a) ∈ nodes B"
using ‹snd p ∈ nodes B› ‹snd (snd a) ∈ succ B (fst a) (snd p)›
by (metis FSM.nodes.simps fst_conv snd_conv)
ultimately show ?case
by (simp add: mem_Times_iff)
qed
qed
subsection ‹ Required properties ›
text ‹
FSMs used by the adaptive state counting algorithm are required to satisfy certain properties which
are introduced in here.
Most notably, the observability property (see function @{verbatim observable}) implies the
uniqueness of certain paths and hence allows for several stronger variations of previous results.
›
fun finite_FSM :: "('in, 'out, 'state) FSM ⇒ bool" where
"finite_FSM M = (finite (nodes M)
∧ finite (inputs M)
∧ finite (outputs M))"
fun observable :: "('in, 'out, 'state) FSM ⇒ bool" where
"observable M = (∀ t . ∀ s1 . ((succ M) t s1 = {})
∨ (∃ s2 . (succ M) t s1 = {s2}))"
fun completely_specified :: "('in, 'out, 'state) FSM ⇒ bool" where
"completely_specified M = (∀ s1 ∈ nodes M . ∀ x ∈ inputs M .
∃ y ∈ outputs M .
∃ s2 . s2 ∈ (succ M) (x,y) s1)"
fun well_formed :: "('in, 'out, 'state) FSM ⇒ bool" where
"well_formed M = (finite_FSM M
∧ (∀ s1 x y . (x ∉ inputs M ∨ y ∉ outputs M)
⟶ succ M (x,y) s1 = {})
∧ inputs M ≠ {}
∧ outputs M ≠ {})"
abbreviation "OFSM M ≡ well_formed M
∧ observable M
∧ completely_specified M"
lemma OFSM_props[elim!] :
assumes "OFSM M"
shows "well_formed M"
"observable M"
"completely_specified M" using assms by auto
lemma set_of_succs_finite :
assumes "well_formed M"
and "q ∈ nodes M"
shows "finite (succ M io q)"
proof (rule ccontr)
assume "infinite (succ M io q)"
moreover have "succ M io q ⊆ nodes M"
using assms by (simp add: subsetI succ_nodes)
ultimately have "infinite (nodes M)"
using infinite_super by blast
then show "False"
using assms by auto
qed
lemma well_formed_path_io_containment :
assumes "well_formed M"
and "path M p q"
shows "set (map fst p) ⊆ (inputs M × outputs M)"
using assms proof (induction p arbitrary: q)
case Nil
then show ?case by auto
next
case (Cons a p)
have "fst a ∈ (inputs M × outputs M)"
proof (rule ccontr)
assume "fst a ∉ inputs M × outputs M"
then have "fst (fst a) ∉ inputs M ∨ snd (fst a) ∉ outputs M"
by (metis SigmaI prod.collapse)
then have "succ M (fst a) q = {}"
using Cons by (metis prod.collapse well_formed.elims(2))
moreover have "(snd a) ∈ succ M (fst a) q"
using Cons by auto
ultimately show "False"
by auto
qed
moreover have "set (map fst p) ⊆ (inputs M × outputs M)"
using Cons by blast
ultimately show ?case
by auto
qed
lemma path_input_containment :
assumes "well_formed M"
and "path M p q"
shows "set (map fst (map fst p)) ⊆ inputs M"
using assms proof (induction p arbitrary: q rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc a p)
have "set (map fst (p @ [a])) ⊆ (inputs M × outputs M)"
using well_formed_path_io_containment[OF snoc.prems] by assumption
then have "(fst a) ∈ (inputs M × outputs M)"
by auto
then have "fst (fst a) ∈ inputs M"
by auto
moreover have "set (map fst (map fst p)) ⊆ inputs M"
using snoc.IH[OF snoc.prems(1)]
using snoc.prems(2) by blast
ultimately show ?case
by simp
qed
lemma path_state_containment :
assumes "path M p q"
and "q ∈ nodes M"
shows "set (map snd p) ⊆ nodes M"
using assms by (metis FSM.nodes_states states_alt_def)
lemma language_state_inputs :
assumes "well_formed M"
and "io ∈ language_state M q"
shows "set (map fst io) ⊆ inputs M"
proof -
obtain tr where "path M (io || tr) q" "length tr = length io"
using assms(2) by auto
show ?thesis
by (metis (no_types)
‹⋀thesis. (⋀tr. ⟦path M (io || tr) q; length tr = length io⟧ ⟹ thesis) ⟹ thesis›
assms(1) map_fst_zip path_input_containment)
qed
lemma set_of_paths_finite :
assumes "well_formed M"
and "q1 ∈ nodes M"
shows "finite { p . path M p q1 ∧ target p q1 = q2 ∧ length p ≤ k }"
proof -
let ?trs = "{ tr . set tr ⊆ nodes M ∧ length tr ≤ k }"
let ?ios = "{ io . set io ⊆ inputs M × outputs M ∧ length io ≤ k }"
let ?iotrs = "image (λ (io,tr) . io || tr) (?ios × ?trs)"
let ?paths = "{ p . path M p q1 ∧ target p q1 = q2 ∧ length p ≤ k }"
have "finite (inputs M × outputs M)"
using assms by auto
then have "finite ?ios"
using assms by (simp add: finite_lists_length_le)
moreover have "finite ?trs"
using assms by (simp add: finite_lists_length_le)
ultimately have "finite ?iotrs"
by auto
moreover have "?paths ⊆ ?iotrs"
proof
fix p assume p_assm : "p ∈ { p . path M p q1 ∧ target p q1 = q2 ∧ length p ≤ k }"
then obtain io tr where p_split : "p = io || tr ∧ length io = length tr"
using that by (metis (no_types) length_map zip_map_fst_snd)
then have "io ∈ ?ios"
using well_formed_path_io_containment
proof -
have f1: "path M p q1 ∧ target p q1 = q2 ∧ length p ≤ k"
using p_assm by force
then have "set io ⊆ inputs M × outputs M"
by (metis (no_types) assms(1) map_fst_zip p_split well_formed_path_io_containment)
then show ?thesis
using f1 by (simp add: p_split)
qed
moreover have "tr ∈ ?trs" using p_split
proof -
have f1: "path M (io || tr) q1 ∧ target (io || tr) q1 = q2
∧ length (io || tr) ≤ k" using ‹p ∈ {p. path M p q1
∧ target p q1 = q2 ∧ length p ≤ k}› p_split by force
then have f2: "length tr ≤ k" by (simp add: p_split)
have "set tr ⊆ nodes M"
using f1 by (metis (no_types) assms(2) length_map p_split path_state_containment
zip_eq zip_map_fst_snd)
then show ?thesis
using f2 by blast
qed
ultimately show "p ∈ ?iotrs"
using p_split by auto
qed
ultimately show ?thesis
using Finite_Set.finite_subset by blast
qed
lemma non_distinct_duplicate_indices :
assumes "¬ distinct xs"
shows "∃ i1 i2 . i1 ≠ i2 ∧ xs ! i1 = xs ! i2 ∧ i1 ≤ length xs ∧ i2 ≤ length xs"
using assms by (meson distinct_conv_nth less_imp_le)
lemma reaching_path_without_repetition :
assumes "well_formed M"
and "q2 ∈ reachable M q1"
and "q1 ∈ nodes M"
shows "∃ p . path M p q1 ∧ target p q1 = q2 ∧ distinct (q1 # states p q1)"
proof -
have shorten_nondistinct : "∀ p. (path M p q1 ∧ target p q1 = q2 ∧ ¬ distinct (q1 # states p q1))
⟶ (∃ p' . path M p' q1 ∧ target p' q1 = q2 ∧ length p' < length p)"
proof
fix p
show "(path M p q1 ∧ target p q1 = q2 ∧ ¬ distinct (q1 # states p q1))
⟶ (∃ p' . path M p' q1 ∧ target p' q1 = q2 ∧ length p' < length p)"
proof
assume assm : "path M p q1 ∧ target p q1 = q2 ∧ ¬ distinct (q1 # states p q1)"
then show "(∃p'. path M p' q1 ∧ target p' q1 = q2 ∧ length p' < length p)"
proof (cases "q1 ∈ set (states p q1)")
case True
have "∃ i1 . target (take i1 p) q1 = q1 ∧ i1 ≤ length p ∧ i1 > 0"
proof (rule ccontr)
assume "¬ (∃ i1. target (take i1 p) q1 = q1 ∧ i1 ≤ length p ∧ i1 > 0)"
then have "¬ (∃ i1 . (states p q1) ! i1 = q1 ∧ i1 ≤ length (states p q1))"
by (metis True in_set_conv_nth less_eq_Suc_le scan_length scan_nth zero_less_Suc)
then have "q1 ∉ set (states p q1)"
by (meson in_set_conv_nth less_imp_le)
then show "False"
using True by auto
qed
then obtain i1 where i1_def : "target (take i1 p) q1 = q1 ∧ i1 ≤ length p ∧ i1 > 0"
by auto
then have "path M (take i1 p) q1"
using assm by (metis FSM.path_append_elim append_take_drop_id)
moreover have "path M (drop i1 p) q1"
using i1_def by (metis FSM.path_append_elim append_take_drop_id assm)
ultimately have "path M (drop i1 p) q1 ∧ (target (drop i1 p) q1 = q2)"
using i1_def by (metis (no_types) append_take_drop_id assm fold_append o_apply)
moreover have "length (drop i1 p) < length p"
using i1_def by auto
ultimately show ?thesis
using assms by blast
next
case False
then have assm' : "path M p q1 ∧ target p q1 = q2 ∧ ¬ distinct (states p q1)"
using assm by auto
have "∃ i1 i2 . i1 ≠ i2 ∧ target (take i1 p) q1 = target (take i2 p) q1
∧ i1 ≤ length p ∧ i2 ≤ length p"
proof (rule ccontr)
assume "¬ (∃ i1 i2 . i1 ≠ i2 ∧ target (take i1 p) q1 = target (take i2 p) q1
∧ i1 ≤ length p ∧ i2 ≤ length p)"
then have "¬ (∃ i1 i2 . i1 ≠ i2 ∧ (states p q1) ! i1 = (states p q1) ! i2
∧ i1 ≤ length (states p q1) ∧ i2 ≤ length (states p q1))"
by (metis (no_types, lifting) Suc_leI assm' distinct_conv_nth nat.inject
scan_length scan_nth)
then have "distinct (states p q1)"
using non_distinct_duplicate_indices by blast
then show "False"
using assm' by auto
qed
then obtain i1 i2 where i_def : "i1 < i2 ∧ target (take i1 p) q1 = target (take i2 p) q1
∧ i1 ≤ length p ∧ i2 ≤ length p"
by (metis nat_neq_iff)
then have "path M (take i1 p) q1"
using assm by (metis FSM.path_append_elim append_take_drop_id)
moreover have "path M (drop i2 p) (target (take i2 p) q1)"
by (metis FSM.path_append_elim append_take_drop_id assm)
ultimately have "path M ((take i1 p) @ (drop i2 p)) q1
∧ (target ((take i1 p) @ (drop i2 p)) q1 = q2)"
using i_def assm
by (metis FSM.path_append append_take_drop_id fold_append o_apply)
moreover have "length ((take i1 p) @ (drop i2 p)) < length p"
using i_def by auto
ultimately have "path M ((take i1 p) @ (drop i2 p)) q1
∧ target ((take i1 p) @ (drop i2 p)) q1 = q2
∧ length ((take i1 p) @ (drop i2 p)) < length p"
by simp
then show ?thesis
using assms by blast
qed
qed
qed
obtain p where p_def : "path M p q1 ∧ target p q1 = q2"
using assms by auto
let ?paths = "{p' . (path M p' q1 ∧ target p' q1 = q2 ∧ length p' ≤ length p)}"
let ?minPath = "arg_min length (λ io . io ∈ ?paths)"
have "?paths ≠ empty"
using p_def by auto
moreover have "finite ?paths"
using assms by (simp add: set_of_paths_finite)
ultimately have minPath_def : "?minPath ∈ ?paths ∧ (∀ p' ∈ ?paths . length ?minPath ≤ length p')"
by (meson arg_min_nat_lemma equals0I)
moreover have "distinct (q1 # states ?minPath q1)"
proof (rule ccontr)
assume "¬ distinct (q1 # states ?minPath q1)"
then have "∃ p' . path M p' q1 ∧ target p' q1 = q2 ∧ length p' < length ?minPath"
using shorten_nondistinct minPath_def by blast
then show "False"
using minPath_def using arg_min_nat_le dual_order.strict_trans1 by auto
qed
ultimately show ?thesis by auto
qed
lemma observable_path_unique[simp] :
assumes "io ∈ LS M q"
and "observable M"
and "path M (io || tr1) q" "length io = length tr1"
and "path M (io || tr2) q" "length io = length tr2"
shows "tr1 = tr2"
proof (rule ccontr)
assume tr_assm : "tr1 ≠ tr2"
then have state_diff : "(states (io || tr1) q ) ≠ (states (io || tr2) q)"
by (metis assms(4) assms(6) map_snd_zip states_alt_def)
show "False"
using assms tr_assm proof (induction io arbitrary: q tr1 tr2)
case Nil
then show ?case using Nil
by simp
next
case (Cons io_hd io_tl)
then obtain tr1_hd tr1_tl tr2_hd tr2_tl where tr_split : "tr1 = tr1_hd # tr1_tl
∧ tr2 = tr2_hd # tr2_tl"
by (metis length_0_conv neq_Nil_conv)
have p1: "path M ([io_hd] || [tr1_hd]) q"
using Cons.prems tr_split by auto
have p2: "path M ([io_hd] || [tr2_hd]) q"
using Cons.prems tr_split by auto
have tr_hd_eq : "tr1_hd = tr2_hd"
using Cons.prems unfolding observable.simps
proof -
assume "∀t s1. succ M t s1 = {} ∨ (∃s2. succ M t s1 = {s2})"
then show ?thesis
by (metis (no_types) p1 p2 FSM.path_cons_elim empty_iff prod.sel(1) prod.sel(2) singletonD
zip_Cons_Cons)
qed
then show ?thesis
using Cons.IH Cons.prems(3) Cons.prems(4) Cons.prems(5) Cons.prems(6) Cons.prems(7) assms(2)
tr_split by auto
qed
qed
lemma observable_path_unique_ex[elim] :
assumes "observable M"
and "io ∈ LS M q"
obtains tr
where "{ t . path M (io || t) q ∧ length io = length t } = { tr }"
proof -
obtain tr where tr_def : "path M (io || tr) q" "length io = length tr"
using assms by auto
then have "{ t . path M (io || t) q ∧ length io = length t } ≠ {}"
by blast
moreover have "∀ t ∈ { t . path M (io || t) q ∧ length io = length t } . t = tr"
using assms tr_def by auto
ultimately show ?thesis
using that by moura
qed
lemma well_formed_product[simp] :
assumes "well_formed M1"
and "well_formed M2"
shows "well_formed (product M2 M1)" (is "well_formed ?PM")
unfolding well_formed.simps proof
have "finite (nodes M1)" "finite (nodes M2)"
using assms by auto
then have "finite (nodes M2 × nodes M1)"
by simp
moreover have "nodes ?PM ⊆ nodes M2 × nodes M1"
using product_nodes assms by blast
ultimately show "finite_FSM ?PM"
using infinite_subset assms by auto
next
have "inputs ?PM = inputs M2 ∪ inputs M1"
"outputs ?PM = outputs M2 ∪ outputs M1"
by auto
then show "(∀s1 x y. x ∉ inputs ?PM ∨ y ∉ outputs ?PM ⟶ succ ?PM (x, y) s1 = {})
∧ inputs ?PM ≠ {} ∧ outputs ?PM ≠ {}"
using assms by auto
qed
subsection ‹ States reached by a given IO-sequence ›
text ‹
Function @{verbatim io_targets} collects all states of an FSM reached from a given state by a
given IO-sequence.
Notably, for any observable FSM, this set contains at most one state.
›
fun io_targets :: "('in, 'out, 'state) FSM ⇒ 'state ⇒ ('in × 'out) list ⇒ 'state set" where
"io_targets M q io = { target (io || tr) q | tr . path M (io || tr) q ∧ length io = length tr }"
lemma io_target_implies_L :
assumes "q ∈ io_targets M (initial M) io"
shows "io ∈ L M"
proof -
obtain tr where "path M (io || tr) (initial M)"
"length tr = length io"
"target (io || tr) (initial M) = q"
using assms by auto
then show ?thesis by auto
qed
lemma io_target_from_path :
assumes "path M (w || tr) q"
and "length w = length tr"
shows "target (w || tr) q ∈ io_targets M q w"
using assms by auto
lemma io_targets_observable_singleton_ex :
assumes "observable M"
and "io ∈ LS M q1"
shows "∃ q2 . io_targets M q1 io = { q2 }"
proof -
obtain tr where tr_def : "{ t . path M (io || t) q1 ∧ length io = length t } = { tr }"
using assms observable_path_unique_ex by (metis (mono_tags, lifting))
then have "io_targets M q1 io = { target (io || tr) q1 }"
by fastforce
then show ?thesis
by blast
qed
lemma io_targets_observable_singleton_ob :
assumes "observable M"
and "io ∈ LS M q1"
obtains q2
where "io_targets M q1 io = { q2 }"
proof -
obtain tr where tr_def : "{ t . path M (io || t) q1 ∧ length io = length t } = { tr }"
using assms observable_path_unique_ex by (metis (mono_tags, lifting))
then have "io_targets M q1 io = { target (io || tr) q1 }"
by fastforce
then show ?thesis using that by blast
qed
lemma io_targets_elim[elim] :
assumes "p ∈ io_targets M q io"
obtains tr
where "target (io || tr) q = p ∧ path M (io || tr) q ∧ length io = length tr"
using assms unfolding io_targets.simps by force
lemma io_targets_reachable :
assumes "q2 ∈ io_targets M q1 io"
shows "q2 ∈ reachable M q1"
using assms unfolding io_targets.simps by blast
lemma io_targets_nodes :
assumes "q2 ∈ io_targets M q1 io"
and "q1 ∈ nodes M"
shows "q2 ∈ nodes M"
using assms by auto
lemma observable_io_targets_split :
assumes "observable M"
and "io_targets M q1 (vs @ xs) = {q3}"
and "io_targets M q1 vs = {q2}"
shows "io_targets M q2 xs = {q3}"
proof -
have "vs @ xs ∈ LS M q1"
using assms(2) by force
then obtain trV trX where tr_def :
"path M (vs || trV) q1" "length vs = length trV"
"path M (xs || trX) (target (vs || trV) q1)" "length xs = length trX"
using language_state_split[of vs xs M q1] by auto
then have tgt_V : "target (vs || trV) q1 = q2"
using assms(3) by auto
then have path_X : "path M (xs || trX) q2 ∧ length xs = length trX"
using tr_def by auto
have tgt_all : "target (vs @ xs || trV @ trX) q1 = q3"
proof -
have f1: "∃cs. q3 = target (vs @ xs || cs) q1
∧ path M (vs @ xs || cs) q1 ∧ length (vs @ xs) = length cs"
using assms(2) by auto
have "length (vs @ xs) = length trV + length trX"
by (simp add: tr_def(2) tr_def(4))
then have "length (vs @ xs) = length (trV @ trX)"
by simp
then show ?thesis
using f1 by (metis FSM.path_append ‹vs @ xs ∈ LS M q1› assms(1) observable_path_unique
tr_def(1) tr_def(2) tr_def(3) zip_append)
qed
then have "target ((vs || trV) @ (xs || trX)) q1 = q3"
using tr_def by simp
then have "target (xs || trX) q2 = q3"
using tgt_V by auto
then have "q3 ∈ io_targets M q2 xs"
using path_X by auto
then show ?thesis
by (metis (no_types) ‹observable M› path_X insert_absorb io_targets_observable_singleton_ex
language_state singleton_insert_inj_eq')
qed
lemma observable_io_target_unique_target :
assumes "observable M"
and "io_targets M q1 io = {q2}"
and "path M (io || tr) q1"
and "length io = length tr"
shows "target (io || tr) q1 = q2"
using assms by auto
lemma target_in_states :
assumes "length io = length tr"
and "length io > 0"
shows "last (states (io || tr) q) = target (io || tr) q"
proof -
have "0 < length tr"
using assms(1) assms(2) by presburger
then show ?thesis
by (simp add: FSM.target_alt_def assms(1) states_alt_def)
qed
lemma target_alt_def :
assumes "length io = length tr"
shows "length io = 0 ⟹ target (io || tr) q = q"
"length io > 0 ⟹ target (io || tr) q = last tr"
proof -
show "length io = 0 ⟹ target (io || tr) q = q" by simp
show "length io > 0 ⟹ target (io || tr) q = last tr"
by (metis assms last_ConsR length_greater_0_conv map_snd_zip scan_last states_alt_def)
qed
lemma obs_target_is_io_targets :
assumes "observable M"
and "path M (io || tr) q"
and "length io = length tr"
shows "io_targets M q io = {target (io || tr) q}"
by (metis assms(1) assms(2) assms(3) io_targets_observable_singleton_ex language_state
observable_io_target_unique_target)
lemma io_target_target :
assumes "io_targets M q1 io = {q2}"
and "path M (io || tr) q1"
and "length io = length tr"
shows "target (io || tr) q1 = q2"
proof -
have "target (io || tr) q1 ∈ io_targets M q1 io" using assms(2) assms(3) by auto
then show ?thesis using assms(1) by blast
qed
lemma index_last_take :
assumes "i < length xs"
shows "xs ! i = last (take (Suc i) xs)"
by (simp add: assms take_Suc_conv_app_nth)
lemma path_last_io_target :
assumes "path M (xs || tr) q"
and "length xs = length tr"
and "length xs > 0"
shows "last tr ∈ io_targets M q xs"
proof -
have "last tr = target (xs || tr) q"
by (metis assms(2) assms(3) map_snd_zip states_alt_def target_in_states)
then show ?thesis using assms(1) assms(2) by auto
qed
lemma path_prefix_io_targets :
assumes "path M (xs || tr) q"
and "length xs = length tr"
and "length xs > 0"
shows "last (take (Suc i) tr) ∈ io_targets M q (take (Suc i) xs)"
proof -
have "path M (take (Suc i) xs || take (Suc i) tr) q"
by (metis (no_types) FSM.path_append_elim append_take_drop_id assms(1) take_zip)
then show ?thesis
using assms(2) assms(3) path_last_io_target by fastforce
qed
lemma states_index_io_target :
assumes "i < length xs"
and "path M (xs || tr) q"
and "length xs = length tr"
and "length xs > 0"
shows "(states (xs || tr) q) ! i ∈ io_targets M q (take (Suc i) xs)"
proof -
have "(states (xs || tr) q) ! i = last (take (Suc i) (states (xs || tr) q))"
by (metis assms(1) assms(3) map_snd_zip states_alt_def index_last_take)
then have "(states (xs || tr) q) ! i = last (states (take (Suc i) xs || take (Suc i) tr) q)"
by (simp add: take_zip)
then have "(states (xs || tr) q) ! i = last (take (Suc i) tr)"
by (simp add: assms(3) states_alt_def)
moreover have "last (take (Suc i) tr) ∈ io_targets M q (take (Suc i) xs)"
by (meson assms(2) assms(3) assms(4) path_prefix_io_targets)
ultimately show ?thesis
by simp
qed
lemma observable_io_targets_append :
assumes "observable M"
and "io_targets M q1 vs = {q2}"
and "io_targets M q2 xs = {q3}"
shows "io_targets M q1 (vs@xs) = {q3}"
proof -
obtain trV where "path M (vs || trV) q1 ∧ length trV = length vs ∧ target (vs || trV) q1 = q2"
by (metis assms(2) io_targets_elim singletonI)
moreover obtain trX where "path M (xs || trX) q2 ∧ length trX = length xs
∧ target (xs || trX) q2 = q3"
by (metis assms(3) io_targets_elim singletonI)
ultimately have "path M (vs @ xs || trV @ trX) q1 ∧ length (trV @ trX) = length (vs @ xs)
∧ target (vs @ xs || trV @ trX) q1 = q3"
by auto
then show ?thesis
by (metis assms(1) obs_target_is_io_targets)
qed
lemma io_path_states_prefix :
assumes "observable M"
and "path M (io1 || tr1) q"
and "length tr1 = length io1"
and "path M (io2 || tr2) q"
and "length tr2 = length io2"
and "prefix io1 io2"
shows "tr1 = take (length tr1) tr2"
proof -
let ?tr1' = "take (length tr1) tr2"
let ?io1' = "take (length tr1) io2"
have "path M (?io1' || ?tr1') q"
by (metis FSM.path_append_elim append_take_drop_id assms(4) take_zip)
have "length ?tr1' = length ?io1'"
using assms (5) by auto
have "?io1' = io1"
proof -
have "∀ps psa. ¬ prefix (ps::('a × 'b) list) psa ∨ length ps ≤ length psa"
using prefix_length_le by blast
then have "length (take (length tr1) io2) = length io1"
using assms(3) assms(6) min.absorb2 by auto
then show ?thesis
by (metis assms(6) min.cobounded2 min_def_raw prefix_length_prefix
prefix_order.dual_order.antisym take_is_prefix)
qed
show "tr1 = ?tr1'"
by (metis ‹length (take (length tr1) tr2) = length (take (length tr1) io2)›
‹path M (take (length tr1) io2 || take (length tr1) tr2) q› ‹take (length tr1) io2 = io1›
assms(1) assms(2) assms(3) language_state observable_path_unique)
qed
lemma observable_io_targets_suffix :
assumes "observable M"
and "io_targets M q1 vs = {q2}"
and "io_targets M q1 (vs@xs) = {q3}"
shows "io_targets M q2 xs = {q3}"
proof -
have "prefix vs (vs@xs)"
by auto
obtain trV where "path M (vs || trV) q1 ∧ length trV = length vs ∧ target (vs || trV) q1 = q2"
by (metis assms(2) io_targets_elim singletonI)
moreover obtain trVX where "path M (vs@xs || trVX) q1
∧ length trVX = length (vs@xs) ∧ target (vs@xs || trVX) q1 = q3"
by (metis assms(3) io_targets_elim singletonI)
ultimately have "trV = take (length trV) trVX"
using io_path_states_prefix[OF assms(1) _ _ _ _ ‹prefix vs (vs@xs)›, of trV q1 trVX] by auto
show ?thesis
by (meson assms(1) assms(2) assms(3) observable_io_targets_split)
qed
lemma observable_io_target_is_singleton[simp] :
assumes "observable M"
and "p ∈ io_targets M q io"
shows "io_targets M q io = {p}"
proof -
have "io ∈ LS M q"
using assms(2) by auto
then obtain p' where "io_targets M q io = {p'}"
using assms(1) by (meson io_targets_observable_singleton_ex)
then show ?thesis
using assms(2) by simp
qed
lemma observable_path_prefix :
assumes "observable M"
and "path M (io || tr) q"
and "length io = length tr"
and "path M (ioP || trP) q"
and "length ioP = length trP"
and "prefix ioP io"
shows "trP = take (length ioP) tr"
proof -
have ioP_def : "ioP = take (length ioP) io"
using assms(6) by (metis append_eq_conv_conj prefixE)
then have "take (length ioP) (io || tr) = take (length ioP) io || take (length ioP) tr"
using take_zip by blast
moreover have "path M (take (length ioP) (io || tr)) q"
using assms by (metis FSM.path_append_elim append_take_drop_id)
ultimately have "path M (take (length ioP) io || take (length ioP) tr) q
∧ length (take (length ioP) io) = length (take (length ioP) tr)"
using assms(3) by auto
then have "path M (ioP || take (length ioP) tr) q ∧ length ioP = length (take (length ioP) tr)"
using assms(3) using ioP_def by auto
then show ?thesis
by (meson assms(1) assms(4) assms(5) language_state observable_path_unique)
qed
lemma io_targets_succ :
assumes "q2 ∈ io_targets M q1 [xy]"
shows "q2 ∈ succ M xy q1"
proof -
obtain tr where tr_def : "target ([xy] || tr) q1 = q2"
"path M ([xy] || tr) q1"
"length [xy] = length tr"
using assms by auto
have "length tr = Suc 0"
using ‹length [xy] = length tr› by auto
then obtain q2' where "tr = [q2']"
by (metis Suc_length_conv length_0_conv)
then have "target ([xy] || tr) q1 = q2'"
by auto
then have "q2' = q2"
using ‹target ([xy] || tr) q1 = q2› by simp
then have "path M ([xy] || [q2]) q1"
using tr_def(2) ‹tr = [q2']› by auto
then have "path M [(xy,q2)] q1"
by auto
show ?thesis
proof (cases rule: FSM.path.cases[of M "[(xy,q2)]" q1])
case nil
show ?case
using ‹path M [(xy,q2)] q1› by simp
next
case cons
show "snd (xy, q2) ∈ succ M (fst (xy, q2)) q1 ⟹ path M [] (snd (xy, q2))
⟹ q2 ∈ succ M xy q1"
by auto
qed
qed
subsection ‹ D-reachability ›
text ‹
A state of some FSM is d-reached (deterministically reached) by some input sequence if any sequence
in the language of the FSM with this input sequence reaches that state.
That state is then called d-reachable.
›
abbreviation "d_reached_by M p xs q tr ys ≡
((length xs = length ys ∧ length xs = length tr
∧ (path M ((xs || ys) || tr) p) ∧ target ((xs || ys) || tr) p = q)
∧ (∀ ys2 tr2 . (length xs = length ys2 ∧ length xs = length tr2
∧ path M ((xs || ys2) || tr2) p) ⟶ target ((xs || ys2) || tr2) p = q))"
fun d_reaches :: "('in, 'out, 'state) FSM ⇒ 'state ⇒ 'in list ⇒ 'state ⇒ bool" where
"d_reaches M p xs q = (∃ tr ys . d_reached_by M p xs q tr ys)"
fun d_reachable :: "('in, 'out, 'state) FSM ⇒ 'state ⇒ 'state set" where
"d_reachable M p = { q . (∃ xs . d_reaches M p xs q) }"
lemma d_reaches_unique[elim] :
assumes "d_reaches M p xs q1"
and "d_reaches M p xs q2"
shows "q1 = q2"
using assms unfolding d_reaches.simps by blast
lemma d_reaches_unique_cases[simp] : "{ q . d_reaches M (initial M) xs q } = {}
∨ (∃ q2 . { q . d_reaches M (initial M) xs q } = { q2 })"
unfolding d_reaches.simps by blast
lemma d_reaches_unique_obtain[simp] :
assumes "d_reaches M (initial M) xs q"
shows "{ p . d_reaches M (initial M) xs p } = { q }"
using assms unfolding d_reaches.simps by blast
lemma d_reaches_io_target :
assumes "d_reaches M p xs q"
and "length ys = length xs"
shows "io_targets M p (xs || ys) ⊆ {q}"
proof
fix q' assume "q' ∈ io_targets M p (xs || ys)"
then obtain trQ where "path M ((xs || ys) || trQ) p ∧ length (xs || ys) = length trQ"
by auto
moreover obtain trD ysD where "d_reached_by M p xs q trD ysD" using assms(1)
by auto
ultimately have "target ((xs || ys) || trQ) p = q"
by (simp add: assms(2))
then show "q' ∈ {q}"
using ‹d_reached_by M p xs q trD ysD› ‹q' ∈ io_targets M p (xs || ys)› assms(2) by auto
qed
lemma d_reachable_reachable : "d_reachable M p ⊆ reachable M p"
unfolding d_reaches.simps d_reachable.simps by blast
subsection ‹ Deterministic state cover ›
text ‹
The deterministic state cover of some FSM is a minimal set of input sequences such that every
d-reachable state of the FSM is d-reached by a sequence in the set and the set contains the
empty sequence (which d-reaches the initial state).
›
fun is_det_state_cover_ass :: "('in, 'out, 'state) FSM ⇒ ('state ⇒ 'in list) ⇒ bool" where
"is_det_state_cover_ass M f = (f (initial M) = [] ∧ (∀ s ∈ d_reachable M (initial M) .
d_reaches M (initial M) (f s) s))"
lemma det_state_cover_ass_dist :
assumes "is_det_state_cover_ass M f"
and "s1 ∈ d_reachable M (initial M)"
and "s2 ∈ d_reachable M (initial M)"
and "s1 ≠ s2"
shows "¬(d_reaches M (initial M) (f s2) s1)"
by (meson assms(1) assms(3) assms(4) d_reaches_unique is_det_state_cover_ass.simps)
lemma det_state_cover_ass_diff :
assumes "is_det_state_cover_ass M f"
and "s1 ∈ d_reachable M (initial M)"
and "s2 ∈ d_reachable M (initial M)"
and "s1 ≠ s2"
shows "f s1 ≠ f s2"
by (metis assms det_state_cover_ass_dist is_det_state_cover_ass.simps)
fun is_det_state_cover :: "('in, 'out, 'state) FSM ⇒ 'in list set ⇒ bool" where
"is_det_state_cover M V = (∃ f . is_det_state_cover_ass M f
∧ V = image f (d_reachable M (initial M)))"
lemma det_state_cover_d_reachable[elim] :
assumes "is_det_state_cover M V"
and "v ∈ V"
obtains q
where "d_reaches M (initial M) v q"
by (metis (no_types, opaque_lifting) assms(1) assms(2) image_iff is_det_state_cover.simps
is_det_state_cover_ass.elims(2))
lemma det_state_cover_card[simp] :
assumes "is_det_state_cover M V"
and "finite (nodes M)"
shows "card (d_reachable M (initial M)) = card V"
proof -
obtain f where f_def : "is_det_state_cover_ass M f ∧ V = image f (d_reachable M (initial M))"
using assms unfolding is_det_state_cover.simps by blast
then have card_f : "card V = card (image f (d_reachable M (initial M)))"
by simp
have "d_reachable M (initial M) ⊆ nodes M"
unfolding d_reachable.simps d_reaches.simps using d_reachable_reachable by blast
then have dr_finite : "finite (d_reachable M (initial M))"
using assms infinite_super by blast
then have card_le : "card (image f (d_reachable M (initial M))) ≤ card (d_reachable M (initial M))"
using card_image_le by blast
have "card (image f (d_reachable M (initial M))) = card (d_reachable M (initial M))"
by (meson card_image det_state_cover_ass_diff f_def inj_onI)
then show ?thesis using card_f by auto
qed
lemma det_state_cover_finite :
assumes "is_det_state_cover M V"
and "finite (nodes M)"
shows "finite V"
proof -
have "d_reachable M (initial M) ⊆ nodes M"
by auto
show "finite V" using det_state_cover_card[OF assms]
by (metis ‹d_reachable M (initial M) ⊆ nodes M› assms(1) assms(2) finite_imageI infinite_super
is_det_state_cover.simps)
qed
lemma det_state_cover_initial :
assumes "is_det_state_cover M V"
shows "[] ∈ V"
proof -
have "d_reached_by M (initial M) [] (initial M) [] []"
by (simp add: FSM.nil)
then have "d_reaches M (initial M) [] (initial M)"
by auto
have "initial M ∈ d_reachable M (initial M)"
by (metis (no_types) ‹d_reaches M (initial M) [] (initial M)› d_reachable.simps mem_Collect_eq)
then show ?thesis
by (metis (no_types, lifting) assms image_iff is_det_state_cover.elims(2)
is_det_state_cover_ass.simps)
qed
lemma det_state_cover_empty :
assumes "is_det_state_cover M V"
shows "[] ∈ V"
proof -
obtain f where f_def : "is_det_state_cover_ass M f ∧ V = f ` d_reachable M (initial M)"
using assms by auto
then have "f (initial M) = []"
by auto
moreover have "initial M ∈ d_reachable M (initial M)"
proof -
have "d_reaches M (initial M) [] (initial M)"
by auto
then show ?thesis
by (metis d_reachable.simps mem_Collect_eq)
qed
moreover have "f (initial M) ∈ V"
using f_def calculation by blast
ultimately show ?thesis
by auto
qed
subsection ‹ IO reduction ›
text ‹
An FSM is a reduction of another, if its language is a subset of the language of the latter FSM.
›
fun io_reduction :: "('in, 'out, 'state) FSM ⇒ ('in, 'out, 'state) FSM
⇒ bool" (infix "≼" 200)
where
"M1 ≼ M2 = (LS M1 (initial M1) ⊆ LS M2 (initial M2))"
lemma language_state_inclusion_of_state_reached_by_same_sequence :
assumes "LS M1 q1 ⊆ LS M2 q2"
and "observable M1"
and "observable M2"
and "io_targets M1 q1 io = { q1t }"
and "io_targets M2 q2 io = { q2t }"
shows "LS M1 q1t ⊆ LS M2 q2t"
proof
fix x assume "x ∈ LS M1 q1t"
obtain q1x where "io_targets M1 q1t x = {q1x}"
by (meson ‹x ∈ LS M1 q1t› assms(2) io_targets_observable_singleton_ex)
have "io ∈ LS M1 q1"
using assms(4) by auto
have "io@x ∈ LS M1 q1"
using observable_io_targets_append[OF assms(2) ‹io_targets M1 q1 io = { q1t }›
‹io_targets M1 q1t x = {q1x}›]
by (metis io_targets_elim language_state singletonI)
then have "io@x ∈ LS M2 q2"
using assms(1) by blast
then obtain q2x where "io_targets M2 q2 (io@x) = {q2x}"
by (meson assms(3) io_targets_observable_singleton_ex)
show "x ∈ LS M2 q2t"
using observable_io_targets_split[OF assms(3) ‹io_targets M2 q2 (io @ x) = {q2x}› assms(5)]
by auto
qed
subsection ‹ Language subsets for input sequences ›
text ‹
The following definitions describe restrictions of languages to only those IO-sequences that
exhibit a certain input sequence or whose input sequence is contained in a given set of
input sequences.
This allows to define the notion that some FSM is a reduction of another over a given set of
input sequences, but not necessarily over the entire language of the latter FSM.
›
fun language_state_for_input ::
"('in, 'out, 'state) FSM ⇒ 'state ⇒ 'in list ⇒ ('in × 'out) list set" where
"language_state_for_input M q xs = {(xs || ys) | ys . (length xs = length ys ∧ (xs || ys) ∈ LS M q)}"
fun language_state_for_inputs ::
"('in, 'out, 'state) FSM ⇒ 'state ⇒ 'in list set ⇒ ('in × 'out) list set"
("(LS⇩i⇩n _ _ _)" [1000,1000,1000]) where
"language_state_for_inputs M q ISeqs = {(xs || ys) | xs ys . (xs ∈ ISeqs
∧ length xs = length ys
∧ (xs || ys) ∈ LS M q)}"
abbreviation "L⇩i⇩n M TS ≡ LS⇩i⇩n M (initial M) TS"
abbreviation "io_reduction_on M1 TS M2 ≡ (L⇩i⇩n M1 TS ⊆ L⇩i⇩n M2 TS)"
notation
io_reduction_on ("(_ ≼⟦_⟧ _)" [1000,0,0] 61)
notation (latex output)
io_reduction_on ("(_ ≼⇘_⇙ _)" [1000,0,0] 61)
lemma language_state_for_input_alt_def :
"language_state_for_input M q xs = LS⇩i⇩n M q {xs}"
unfolding language_state_for_input.simps language_state_for_inputs.simps by blast
lemma language_state_for_inputs_alt_def :
"LS⇩i⇩n M q ISeqs = ⋃ (image (language_state_for_input M q) ISeqs)"
by auto
lemma language_state_for_inputs_in_language_state :
"LS⇩i⇩n M q T ⊆ language_state M q"
unfolding language_state_for_inputs.simps language_state_def
by blast
lemma language_state_for_inputs_map_fst :
assumes "io ∈ language_state M q"
and "map fst io ∈ T"
shows "io ∈ LS⇩i⇩n M q T"
proof -
let ?xs = "map fst io"
let ?ys = "map snd io"
have "?xs ∈ T ∧ length ?xs = length ?ys ∧ ?xs || ?ys ∈ language_state M q"
using assms(2,1) by auto
then have "?xs || ?ys ∈ LS⇩i⇩n M q T"
unfolding language_state_for_inputs.simps by blast
then show ?thesis
by simp
qed
lemma language_state_for_inputs_nonempty :
assumes "set xs ⊆ inputs M"
and "completely_specified M"
and "q ∈ nodes M"
shows "LS⇩i⇩n M q {xs} ≠ {}"
using assms proof (induction xs arbitrary: q)
case Nil
then show ?case by auto
next
case (Cons x xs)
then have "x ∈ inputs M"
by simp
then obtain y q' where x_step : "q' ∈ succ M (x,y) q"
using Cons(3,4) unfolding completely_specified.simps by blast
then have "path M ([(x,y)] || [q']) q ∧ length [q] = length [(x,y)]"
"target ([(x,y)] || [q']) q = q'"
by auto
then have "q' ∈ nodes M"
using Cons(4) by (metis FSM.nodes_target)
then have "LS⇩i⇩n M q' {xs} ≠ {}"
using Cons.prems Cons.IH by auto
then obtain ys where "length xs = length ys ∧ (xs || ys) ∈ LS M q'"
by auto
then obtain tr where "path M ((xs || ys) || tr) q' ∧ length tr = length (xs || ys)"
by auto
then have "path M ([(x,y)] @ (xs || ys) || [q'] @ tr) q
∧ length ([q'] @ tr) = length ([(x,y)] @ (xs || ys))"
by (simp add: FSM.path.intros(2) x_step)
then have "path M ((x#xs || y#ys) || [q'] @ tr) q ∧ length ([q'] @ tr) = length (x#xs || y#ys)"
by auto
then have "(x#xs || y#ys) ∈ LS M q"
by (metis language_state)
moreover have "length (x#xs) = length (y#ys)"
by (simp add: ‹length xs = length ys ∧ xs || ys ∈ LS M q'›)
ultimately have "(x#xs || y#ys) ∈ LS⇩i⇩n M q {x # xs}"
unfolding language_state_for_inputs.simps by blast
then show ?case by blast
qed
lemma language_state_for_inputs_map_fst_contained :
assumes "vs ∈ LS⇩i⇩n M q V"
shows "map fst vs ∈ V"
proof -
have "(map fst vs) || (map snd vs) = vs"
by auto
then have "(map fst vs) || (map snd vs) ∈ LS⇩i⇩n M q V"
using assms by auto
then show ?thesis by auto
qed
lemma language_state_for_inputs_empty :
assumes "[] ∈ V"
shows "[] ∈ LS⇩i⇩n M q V"
proof -
have "[] ∈ language_state_for_input M q []" by auto
then show ?thesis using language_state_for_inputs_alt_def by (metis UN_I assms)
qed
lemma language_state_for_input_empty[simp] :
"language_state_for_input M q [] = {[]}"
by auto
lemma language_state_for_input_take :
assumes "io ∈ language_state_for_input M q xs"
shows "take n io ∈ language_state_for_input M q (take n xs)"
proof -
obtain ys where "io = xs || ys" "length xs = length ys" "xs || ys ∈ language_state M q"
using assms by auto
then obtain p where "length p = length xs" "path M ((xs || ys) || p) q "
by auto
then have "path M (take n ((xs || ys) || p)) q"
by (metis FSM.path_append_elim append_take_drop_id)
then have "take n (xs || ys) ∈ language_state M q"
by (simp add: ‹length p = length xs› ‹length xs = length ys› language_state take_zip)
then have "(take n xs) || (take n ys) ∈ language_state M q"
by (simp add: take_zip)
have "take n io = (take n xs) || (take n ys)"
using ‹io = xs || ys› take_zip by blast
moreover have "length (take n xs) = length (take n ys)"
by (simp add: ‹length xs = length ys›)
ultimately show ?thesis
using ‹(take n xs) || (take n ys) ∈ language_state M q›
unfolding language_state_for_input.simps by blast
qed
lemma language_state_for_inputs_prefix :
assumes "vs@xs ∈ L⇩i⇩n M1 {vs'@xs'}"
and "length vs = length vs'"
shows "vs ∈ L⇩i⇩n M1 {vs'}"
proof -
have "vs@xs ∈ L M1"
using assms(1) by auto
then have "vs ∈ L M1"
by (meson language_state_prefix)
then have "vs ∈ L⇩i⇩n M1 {map fst vs}"
by (meson insertI1 language_state_for_inputs_map_fst)
moreover have "vs' = map fst vs"
by (metis append_eq_append_conv assms(1) assms(2) language_state_for_inputs_map_fst_contained
length_map map_append singletonD)
ultimately show ?thesis
by blast
qed
lemma language_state_for_inputs_union :
shows "LS⇩i⇩n M q T1 ∪ LS⇩i⇩n M q T2 = LS⇩i⇩n M q (T1 ∪ T2)"
unfolding language_state_for_inputs.simps by blast
lemma io_reduction_on_subset :
assumes "io_reduction_on M1 T M2"
and "T' ⊆ T"
shows "io_reduction_on M1 T' M2"
proof (rule ccontr)
assume "¬ io_reduction_on M1 T' M2"
then obtain xs' where "xs' ∈ T'" "¬ L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'}"
proof -
have f1: "∀ps P Pa. (ps::('a × 'b) list) ∉ P ∨ ¬ P ⊆ Pa ∨ ps ∈ Pa"
by blast
obtain pps :: "('a × 'b) list set ⇒ ('a × 'b) list set ⇒ ('a × 'b) list" where
"∀x0 x1. (∃v2. v2 ∈ x1 ∧ v2 ∉ x0) = (pps x0 x1 ∈ x1 ∧ pps x0 x1 ∉ x0)"
by moura
then have f2: "∀P Pa. pps Pa P ∈ P ∧ pps Pa P ∉ Pa ∨ P ⊆ Pa"
by (meson subsetI)
have f3: "∀ps f c A. (ps::('a × 'b) list) ∉ LS⇩i⇩n f (c::'c) A ∨ map fst ps ∈ A"
by (meson language_state_for_inputs_map_fst_contained)
then have "L⇩i⇩n M1 T' ⊆ L⇩i⇩n M1 T"
using f2 by (meson assms(2) language_state_for_inputs_in_language_state
language_state_for_inputs_map_fst set_rev_mp)
then show ?thesis
using f3 f2 f1 by (meson ‹¬ io_reduction_on M1 T' M2› assms(1)
language_state_for_inputs_in_language_state
language_state_for_inputs_map_fst)
qed
then have "xs' ∈ T"
using assms(2) by blast
have "¬ io_reduction_on M1 T M2"
proof -
have f1: "∀as. as ∉ T' ∨ as ∈ T"
using assms(2) by auto
obtain pps :: "('a × 'b) list set ⇒ ('a × 'b) list set ⇒ ('a × 'b) list" where
"∀x0 x1. (∃v2. v2 ∈ x1 ∧ v2 ∉ x0) = (pps x0 x1 ∈ x1 ∧ pps x0 x1 ∉ x0)"
by moura
then have "∀P Pa. (¬ P ⊆ Pa ∨ (∀ps. ps ∉ P ∨ ps ∈ Pa))
∧ (P ⊆ Pa ∨ pps Pa P ∈ P ∧ pps Pa P ∉ Pa)"
by blast
then show ?thesis
using f1 by (meson ‹¬ io_reduction_on M1 T' M2› language_state_for_inputs_in_language_state
language_state_for_inputs_map_fst language_state_for_inputs_map_fst_contained)
qed
then show "False"
using assms(1) by auto
qed
subsection ‹ Sequences to failures ›
text ‹
A sequence to a failure for FSMs @{verbatim M1} and @{verbatim M2} is a sequence such that any
proper prefix of it is contained in the languages of both @{verbatim M1} and @{verbatim M2}, while
the sequence itself is contained only in the language of A.
That is, if a sequence to a failure for @{verbatim M1} and @{verbatim M2} exists, then
@{verbatim M1} is not a reduction of @{verbatim M2}.
›
fun sequence_to_failure ::
"('in,'out,'state) FSM ⇒ ('in,'out,'state) FSM ⇒ ('in × 'out) list ⇒ bool" where
"sequence_to_failure M1 M2 xs = (
(butlast xs) ∈ (language_state M2 (initial M2) ∩ language_state M1 (initial M1))
∧ xs ∈ (language_state M1 (initial M1) - language_state M2 (initial M2)))"
lemma sequence_to_failure_ob :
assumes "¬ M1 ≼ M2"
and "well_formed M1"
and "well_formed M2"
obtains io
where "sequence_to_failure M1 M2 io"
proof -
let ?diff = "{ io . io ∈ language_state M1 (initial M1) ∧ io ∉ language_state M2 (initial M2)}"
have "?diff ≠ empty"
using assms by auto
moreover obtain io where io_def[simp] : "io = arg_min length (λ io . io ∈ ?diff)"
using assms by auto
ultimately have io_diff : "io ∈ ?diff"
using assms by (meson all_not_in_conv arg_min_natI)
then have "io ≠ []"
using assms io_def language_state by auto
then obtain io_init io_last where io_split[simp] : "io = io_init @ [io_last]"
by (metis append_butlast_last_id)
have io_init_inclusion : "io_init ∈ language_state M1 (initial M1)
∧ io_init ∈ language_state M2 (initial M2)"
proof (rule ccontr)
assume assm : "¬ (io_init ∈ language_state M1 (initial M1)
∧ io_init ∈ language_state M2 (initial M2))"
have "io_init @ [io_last] ∈ language_state M1 (initial M1)"
using io_diff io_split by auto
then have "io_init ∈ language_state M1 (initial M1)"
by (meson language_state language_state_split)
moreover have "io_init ∉ language_state M2 (initial M2)"
using assm calculation by auto
ultimately have "io_init ∈ ?diff"
by auto
moreover have "length io_init < length io"
using io_split by auto
ultimately have "io ≠ arg_min length (λ io . io ∈ ?diff)"
proof -
have "∃ps. ps ∈ {ps ∈ language_state M1 (initial M1).
ps ∉ language_state M2 (initial M2)} ∧ ¬ length io ≤ length ps"
using ‹io_init ∈ {io∈ language_state M1 (initial M1). io ∉ language_state M2 (initial M2)}›
‹length io_init < length io› linorder_not_less
by blast
then show ?thesis
by (meson arg_min_nat_le)
qed
then show "False" using io_def by simp
qed
then have "sequence_to_failure M1 M2 io"
using io_split io_diff by auto
then show ?thesis
using that by auto
qed
lemma sequence_to_failure_succ :
assumes "sequence_to_failure M1 M2 io"
shows "∀ q ∈ io_targets M2 (initial M2) (butlast io) . succ M2 (last io) q = {}"
proof
have "io ≠ []"
using assms by auto
fix q assume "q ∈ io_targets M2 (initial M2) (butlast io)"
then obtain tr where "q = target (butlast io || tr) (initial M2)"
and "path M2 (butlast io || tr) (initial M2)"
and "length (butlast io) = length tr"
unfolding io_targets.simps by auto
show "succ M2 (last io) q = {}"
proof (rule ccontr)
assume "succ M2 (last io) q ≠ {}"
then obtain q' where "q' ∈ succ M2 (last io) q"
by blast
then have "path M2 [(last io, q')] (target (butlast io || tr) (initial M2))"
using ‹q = target (butlast io || tr) (initial M2)› by auto
have "path M2 ((butlast io || tr) @ [(last io, q')]) (initial M2)"
using ‹path M2 (butlast io || tr) (initial M2)›
‹path M2 [(last io, q')] (target (butlast io || tr) (initial M2))› by auto
have "butlast io @ [last io] = io"
by (meson ‹io ≠ []› append_butlast_last_id)
have "path M2 (io || (tr@[q'])) (initial M2)"
proof -
have "path M2 ((butlast io || tr) @ ([last io] || [q'])) (initial M2)"
by (simp add: FSM.path_append ‹path M2 (butlast io || tr) (initial M2)›
‹path M2 [(last io, q')] (target (butlast io || tr) (initial M2))›)
then show ?thesis
by (metis (no_types) ‹butlast io @ [last io] = io›
‹length (butlast io) = length tr› zip_append)
qed
have "io ∈ L M2"
proof -
have "length tr + (0 + Suc 0) = length io"
by (metis ‹butlast io @ [last io] = io› ‹length (butlast io) = length tr›
length_append list.size(3) list.size(4))
then show ?thesis
using ‹path M2 (io || tr @ [q']) (initial M2)› by fastforce
qed
then show "False"
using assms by auto
qed
qed
lemma sequence_to_failure_non_nil :
assumes "sequence_to_failure M1 M2 xs"
shows "xs ≠ []"
proof
assume "xs = []"
then have "xs ∈ L M1 ∩ L M2"
by auto
then show "False" using assms by auto
qed
lemma sequence_to_failure_from_arbitrary_failure :
assumes "vs@xs ∈ L M1 - L M2"
and "vs ∈ L M2 ∩ L M1"
shows "∃ xs' . prefix xs' xs ∧ sequence_to_failure M1 M2 (vs@xs')"
using assms proof (induction xs rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc x xs)
have "vs @ xs ∈ L M1"
using snoc.prems(1) by (metis Diff_iff append.assoc language_state_prefix)
show ?case
proof (cases "vs@xs ∈ L M2")
case True
have "butlast (vs@xs@[x]) ∈ L M2 ∩ L M1"
using True ‹vs @ xs ∈ L M1› by (simp add: butlast_append)
then show ?thesis
using sequence_to_failure.simps snoc.prems by blast
next
case False
then have "vs@xs ∈ L M1 - L M2"
using ‹vs @ xs ∈ L M1› by blast
then obtain xs' where "prefix xs' xs" "sequence_to_failure M1 M2 (vs@xs')"
using snoc.prems(2) snoc.IH by blast
then show ?thesis
using prefix_snoc by auto
qed
qed
text ‹
The following lemma shows that if @{verbatim M1} is not a reduction of @{verbatim M2}, then a
minimal sequence to a failure exists that is of length at most the number of states in
@{verbatim M1} times the number of states in @{verbatim M2}.
›
lemma sequence_to_failure_length :
assumes "well_formed M1"
and "well_formed M2"
and "observable M1"
and "observable M2"
and "¬ M1 ≼ M2"
shows "∃ xs . sequence_to_failure M1 M2 xs ∧ length xs ≤ |M2| * |M1|"
proof -
obtain seq where "sequence_to_failure M1 M2 seq"
using assms sequence_to_failure_ob by blast
then have "seq ≠ []"
by auto
let ?bls = "butlast seq"
have "?bls ∈ L M1" "?bls ∈ L M2"
using ‹sequence_to_failure M1 M2 seq› by auto
then obtain tr1b tr2b where
"path M1 (?bls || tr1b) (initial M1)"
"length tr1b = length ?bls"
"path M2 (?bls || tr2b) (initial M2)"
"length ?bls = length tr2b"
by fastforce
then have "length tr2b = length tr1b"
by auto
let ?PM = "product M2 M1"
have "well_formed ?PM"
using well_formed_product[OF assms(1,2)] by assumption
have "path ?PM (?bls || tr2b || tr1b) (initial M2, initial M1)"
using product_path[OF ‹length ?bls = length tr2b› ‹length tr2b = length tr1b›,
of M2 M1 "initial M2" "initial M1"]
using ‹path M1 (butlast seq || tr1b) (initial M1)›
‹path M2 (butlast seq || tr2b) (initial M2)›
by blast
let ?q1b = "target (?bls || tr1b) (initial M1)"
let ?q2b = "target (?bls || tr2b) (initial M2)"
have "io_targets M2 (initial M2) ?bls = {?q2b}"
by (metis ‹length (butlast seq) = length tr2b› ‹path M2 (butlast seq || tr2b) (initial M2)›
assms(4) obs_target_is_io_targets)
have "io_targets M1 (initial M1) ?bls = {?q1b}"
by (metis ‹length tr1b = length (butlast seq)› ‹path M1 (butlast seq || tr1b) (initial M1)›
assms(3) obs_target_is_io_targets)
have "(?q2b, ?q1b) ∈ reachable (product M2 M1) (initial M2, initial M1)"
proof -
have "target (butlast seq || tr2b || tr1b) (initial M2, initial M1)
∈ reachable (product M2 M1) (initial M2, initial M1)"
using ‹path (product M2 M1) (butlast seq || tr2b || tr1b) (initial M2, initial M1)› by blast
then show ?thesis
using ‹length (butlast seq) = length tr2b› ‹length tr2b = length tr1b› by auto
qed
have "(initial M2, initial M1) ∈ nodes (product M2 M1)"
by (simp add: FSM.nodes.initial)
obtain p where repFreePath : "path (product M2 M1) p (initial M2, initial M1) ∧
target p (initial M2, initial M1) =
(?q2b,?q1b)"
"distinct ((initial M2, initial M1) # states p (initial M2, initial M1))"
using reaching_path_without_repetition[OF ‹well_formed ?PM›
‹(?q2b, ?q1b) ∈ reachable (product M2 M1) (initial M2, initial M1)›
‹(initial M2, initial M1) ∈ nodes (product M2 M1)›]
by blast
then have "set (states p (initial M2, initial M1)) ⊆ nodes ?PM"
by (simp add: FSM.nodes_states ‹(initial M2, initial M1) ∈ nodes (product M2 M1)›)
moreover have "(initial M2, initial M1) ∉ set (states p (initial M2, initial M1))"
using ‹distinct ((initial M2, initial M1) # states p (initial M2, initial M1))› by auto
ultimately have "set (states p (initial M2, initial M1)) ⊆ nodes ?PM - {(initial M2,initial M1)}"
by blast
moreover have "finite (nodes ?PM)"
using ‹well_formed ?PM› by auto
ultimately have "card (set (states p (initial M2, initial M1))) < card (nodes ?PM)"
by (metis ‹(initial M2, initial M1) ∈ nodes (product M2 M1)›
‹(initial M2, initial M1) ∉ set (states p (initial M2, initial M1))›
‹set (states p (initial M2, initial M1)) ⊆ nodes (product M2 M1)›
psubsetI psubset_card_mono)
moreover have "card (set (states p (initial M2, initial M1)))
= length (states p (initial M2, initial M1))"
using distinct_card repFreePath(2) by fastforce
ultimately have "length (states p (initial M2, initial M1)) < |?PM|"
by linarith
then have "length p < |?PM|"
by auto
let ?p1 = "map (snd ∘ snd) p"
let ?p2 = "map (fst ∘ snd) p"
let ?pIO = "map fst p"
have "p = ?pIO || ?p2 || ?p1"
by (metis map_map zip_map_fst_snd)
have "path M2 (?pIO || ?p2) (initial M2)"
"path M1 (?pIO || ?p1) (initial M1)"
using product_path[of ?pIO ?p2 ?p1 M2 M1]
using ‹p = ?pIO || ?p2 || ?p1› repFreePath(1) by auto
have "(?q2b, ?q1b) = (target (?pIO || ?p2 || ?p1) (initial M2, initial M1))"
using ‹p = ?pIO || ?p2 || ?p1› repFreePath(1) by auto
then have "?q2b = target (?pIO || ?p2) (initial M2)"
"?q1b = target (?pIO || ?p1) (initial M1)"
by auto
have "io_targets M2 (initial M2) ?pIO = {?q2b}"
by (metis ‹path M2 (map fst p || map (fst ∘ snd) p) (initial M2)›
‹target (?bls || tr2b) (initial M2) = target (map fst p || map (fst ∘ snd) p) (initial M2)›
assms(4) length_map obs_target_is_io_targets)
have "io_targets M1 (initial M1) ?pIO = {?q1b}"
by (metis ‹path M1 (map fst p || map (snd ∘ snd) p) (initial M1)›
‹target (?bls || tr1b) (initial M1) = target (map fst p || map (snd ∘ snd) p) (initial M1)›
assms(3) length_map obs_target_is_io_targets)
have "seq ∈ L M1" "seq ∉ L M2"
using ‹sequence_to_failure M1 M2 seq› by auto
have "io_targets M1 (initial M1) ?bls = {?q1b}"
by (metis ‹length tr1b = length (butlast seq)› ‹path M1 (butlast seq || tr1b) (initial M1)›
assms(3) obs_target_is_io_targets)
obtain q1s where "io_targets M1 (initial M1) seq = {q1s}"
by (meson ‹seq ∈ L M1› assms(3) io_targets_observable_singleton_ob)
moreover have "seq = (butlast seq)@[last seq]"
using ‹seq ≠ []› by auto
ultimately have "io_targets M1 (initial M1) ((butlast seq)@[last seq]) = {q1s}"
by auto
have "io_targets M1 ?q1b [last seq] = {q1s}"
using observable_io_targets_suffix[OF assms(3) ‹io_targets M1 (initial M1) ?bls = {?q1b}›
‹io_targets M1 (initial M1) ((butlast seq)@[last seq]) = {q1s}›] by assumption
then obtain tr1s where "q1s = target ([last seq] || tr1s) ?q1b"
"path M1 ([last seq] || tr1s) ?q1b"
"length [last seq] = length tr1s"
by auto
have "path M1 ([last seq] || [q1s]) ?q1b"
by (metis (no_types) ‹length [last seq] = length tr1s›
‹path M1 ([last seq] || tr1s) (target (butlast seq || tr1b) (initial M1))›
‹q1s = target ([last seq] || tr1s) (target (butlast seq || tr1b) (initial M1))›
append_Nil append_butlast_last_id butlast.simps(2) length_butlast length_greater_0_conv
not_Cons_self2 target_alt_def(2))
then have "q1s ∈ succ M1 (last seq) ?q1b"
by auto
have "succ M2 (last seq) ?q2b = {}"
proof (rule ccontr)
assume "succ M2 (last seq) (target (butlast seq || tr2b) (initial M2)) ≠ {}"
then obtain q2f where "q2f ∈ succ M2 (last seq) ?q2b"
by blast
then have "target ([last seq] || [q2f]) ?q2b = q2f"
"path M2 ([last seq] || [q2f]) ?q2b"
"length [q2f] = length [last seq]"
by auto
then have "q2f ∈ io_targets M2 ?q2b [last seq]"
by (metis io_target_from_path)
then have "io_targets M2 ?q2b [last seq] = {q2f}"
using assms(4) by (meson observable_io_target_is_singleton)
have "io_targets M2 (initial M2) (butlast seq @ [last seq]) = {q2f}"
using observable_io_targets_append[OF assms(4) ‹io_targets M2 (initial M2) ?bls = {?q2b}›
‹io_targets M2 ?q2b [last seq] = {q2f}›] by assumption
then have "seq ∈ L M2"
using ‹seq = butlast seq @ [last seq]› by auto
then show "False"
using ‹seq ∉ L M2› by blast
qed
have "?pIO ∈ L M1" "?pIO ∈ L M2"
using ‹path M1 (?pIO || ?p1) (initial M1)› ‹path M2 (?pIO || ?p2) (initial M2)› by auto
then have "butlast (?pIO@[last seq]) ∈ L M1 ∩ L M2"
by auto
have "?pIO@[last seq] ∈ L M1"
using observable_io_targets_append[OF assms(3) ‹io_targets M1 (initial M1) ?pIO = {?q1b}›
‹io_targets M1 ?q1b [last seq] = {q1s}›]
by (metis all_not_in_conv insert_not_empty io_targets_elim language_state)
moreover have "?pIO@[last seq] ∉ L M2"
proof
assume "?pIO@[last seq] ∈ L M2"
then obtain q2f where "io_targets M2 (initial M2) (?pIO@[last seq]) = {q2f}"
by (meson assms(4) io_targets_observable_singleton_ob)
have "io_targets M2 ?q2b [last seq] = {q2f}"
using observable_io_targets_split[OF assms(4)
‹io_targets M2 (initial M2) (?pIO@[last seq]) = {q2f}›
‹io_targets M2 (initial M2) (map fst p) = {?q2b}›] by assumption
then have "q2f ∈ succ M2 (last seq) ?q2b"
by (simp add: io_targets_succ)
then show "False"
using ‹succ M2 (last seq) ?q2b = {}› by auto
qed
ultimately have "?pIO@[last seq] ∈ L M1 - L M2"
by auto
have "sequence_to_failure M1 M2 (?pIO@[last seq])"
using ‹butlast (?pIO@[last seq]) ∈ L M1 ∩ L M2› ‹?pIO@[last seq] ∈ L M1 - L M2› by auto
have "length (?pIO@[last seq]) = Suc (length ?pIO)"
by auto
then have "length (?pIO@[last seq]) ≤ |?PM|"
using ‹length p < |?PM|› by auto
have "card (nodes M2 × nodes M1) ≤ |M2| * |M1|"
by (simp add: card_cartesian_product)
have "finite (nodes M2 × nodes M1)"
proof
show "finite (nodes M2)"
using assms by auto
show "finite (nodes M1)"
using assms by auto
qed
have "|?PM| ≤ |M2| * |M1|"
by (meson ‹card (nodes M2 × nodes M1) ≤ |M2| * |M1|› ‹finite (nodes M2 × nodes M1)›
card_mono dual_order.trans product_nodes)
then have "length (?pIO@[last seq]) ≤ |M2| * |M1|"
using ‹length (?pIO@[last seq]) ≤ |?PM|› by auto
then have "sequence_to_failure M1 M2 (?pIO@[last seq]) ∧ length (?pIO@[last seq]) ≤ |M2| * |M1|"
using ‹sequence_to_failure M1 M2 (?pIO@[last seq])› by auto
then show ?thesis
by blast
qed
subsection ‹ Minimal sequence to failure extending ›
text ‹
A minimal sequence to a failure extending some some set of IO-sequences is a sequence to a failure
of minimal length such that a prefix of that sequence is contained in the set.
›
fun minimal_sequence_to_failure_extending ::
"'in list set ⇒ ('in,'out,'state) FSM ⇒ ('in,'out,'state) FSM ⇒ ('in × 'out) list
⇒ ('in × 'out) list ⇒ bool" where
"minimal_sequence_to_failure_extending V M1 M2 v' io = (
v' ∈ L⇩i⇩n M1 V ∧ sequence_to_failure M1 M2 (v' @ io)
∧ ¬ (∃ io' . ∃ w' ∈ L⇩i⇩n M1 V . sequence_to_failure M1 M2 (w' @ io')
∧ length io' < length io))"
lemma minimal_sequence_to_failure_extending_det_state_cover_ob :
assumes "well_formed M1"
and "well_formed M2"
and "observable M2"
and "is_det_state_cover M2 V"
and "¬ M1 ≼ M2"
obtains vs xs
where "minimal_sequence_to_failure_extending V M1 M2 vs xs"
proof -
let ?exts = "{xs. ∃vs' ∈ L⇩i⇩n M1 V. sequence_to_failure M1 M2 (vs'@xs)}"
obtain stf where "sequence_to_failure M1 M2 stf"
using assms sequence_to_failure_ob by blast
then have "sequence_to_failure M1 M2 ([] @ stf)"
by simp
moreover have "[] ∈ L⇩i⇩n M1 V"
by (meson assms(4) det_state_cover_initial language_state_for_inputs_empty)
ultimately have "stf ∈ ?exts"
by blast
let ?xsMin = "arg_min length (λxs. xs ∈ ?exts)"
have xsMin_def : "?xsMin ∈ ?exts
∧ (∀xs ∈ ?exts. length ?xsMin ≤ length xs)"
by (metis (no_types, lifting) ‹stf ∈ ?exts› arg_min_nat_lemma)
then obtain vs where "vs ∈ L⇩i⇩n M1 V
∧ sequence_to_failure M1 M2 (vs @ ?xsMin)"
by blast
moreover have "¬(∃xs . ∃ws ∈ L⇩i⇩n M1 V. sequence_to_failure M1 M2 (ws@xs)
∧ length xs < length ?xsMin)"
using leD xsMin_def by blast
ultimately have "minimal_sequence_to_failure_extending V M1 M2 vs ?xsMin"
by auto
then show ?thesis
using that by auto
qed
lemma mstfe_prefix_input_in_V :
assumes "minimal_sequence_to_failure_extending V M1 M2 vs xs"
shows "(map fst vs) ∈ V"
proof -
have "vs ∈ L⇩i⇩n M1 V"
using assms by auto
then show ?thesis
using language_state_for_inputs_map_fst_contained by auto
qed
subsection ‹ Complete test suite derived from the product machine ›
text ‹
The classical result of testing FSMs for language inclusion :
Any failure can be observed by a sequence of length at
most n*m where n is the number of states of the reference
model (here FSM @{verbatim M2}) and m is an upper bound on the number
of states of the SUT (here FSM @{verbatim M1}).
›
lemma product_suite_soundness :
assumes "well_formed M1"
and "well_formed M2"
and "observable M1"
and "observable M2"
and "inputs M2 = inputs M1"
and "|M1| ≤ m "
shows "¬ M1 ≼ M2 ⟶ ¬ M1 ≼⟦{xs . set xs ⊆ inputs M2 ∧ length xs ≤ |M2| * m}⟧ M2"
(is "¬ M1 ≼ M2 ⟶ ¬ M1 ≼⟦?TS⟧ M2")
proof
assume "¬ M1 ≼ M2"
obtain stf where "sequence_to_failure M1 M2 stf ∧ length stf ≤ |M2| * |M1|"
using sequence_to_failure_length[OF assms(1-4) ‹¬ M1 ≼ M2›] by blast
then have "sequence_to_failure M1 M2 stf" "length stf ≤ |M2| * |M1|"
by auto
then have "stf ∈ L M1"
by auto
let ?xs = "map fst stf"
have "set ?xs ⊆ inputs M1"
by (meson ‹stf ∈ L M1› assms(1) language_state_inputs)
then have "set ?xs ⊆ inputs M2"
using assms(5) by auto
have "length ?xs ≤ |M2| * |M1|"
using ‹length stf ≤ |M2| * |M1|› by auto
have "length ?xs ≤ |M2| * m"
proof -
show ?thesis
by (metis (no_types) ‹length (map fst stf) ≤ |M2| * |M1|› ‹|M1| ≤ m›
dual_order.trans mult.commute mult_le_mono1)
qed
have "stf ∈ L⇩i⇩n M1 {?xs}"
by (meson ‹stf ∈ L M1› insertI1 language_state_for_inputs_map_fst)
have "?xs ∈ ?TS"
using ‹set ?xs ⊆ inputs M2› ‹length ?xs ≤ |M2| * m› by blast
have "stf ∈ L⇩i⇩n M1 ?TS"
by (metis (no_types, lifting) ‹map fst stf ∈ {xs. set xs ⊆ inputs M2 ∧ length xs ≤ |M2| * m}›
‹stf ∈ L M1› language_state_for_inputs_map_fst)
have "stf ∉ L M2"
using ‹sequence_to_failure M1 M2 stf› by auto
then have "stf ∉ L⇩i⇩n M2 ?TS"
by auto
show "¬ M1 ≼⟦?TS⟧ M2"
using ‹stf ∈ L⇩i⇩n M1 ?TS› ‹stf ∉ L⇩i⇩n M2 ?TS› by blast
qed
lemma product_suite_completeness :
assumes "well_formed M1"
and "well_formed M2"
and "observable M1"
and "observable M2"
and "inputs M2 = inputs M1"
and "|M1| ≤ m "
shows "M1 ≼ M2 ⟷ M1 ≼⟦{xs . set xs ⊆ inputs M2 ∧ length xs ≤ |M2| * m}⟧ M2"
(is "M1 ≼ M2 ⟷ M1 ≼⟦?TS⟧ M2")
proof
show "M1 ≼ M2 ⟹ M1 ≼⟦?TS⟧ M2"
unfolding language_state_for_inputs.simps io_reduction.simps by blast
show "M1 ≼⟦?TS⟧ M2 ⟹ M1 ≼ M2"
using product_suite_soundness[OF assms] by auto
qed
end