Theory ASC_Sufficiency
theory ASC_Sufficiency
imports ASC_Suite
begin
section ‹ Sufficiency of the test suite to test for reduction ›
text ‹
This section provides a proof that the test suite generated by the adaptive state counting algorithm
is sufficient to test for reduction.
›
subsection ‹ Properties of minimal sequences to failures extending the deterministic state cover ›
text ‹
The following two lemmata show that minimal sequences to failures extending the deterministic state
cover do not with their extending suffix visit any state twice or visit a state also reached by a
sequence in the chosen permutation of reactions to the deterministic state cover.
›
lemma minimal_sequence_to_failure_extending_implies_Rep_Pre :
assumes "minimal_sequence_to_failure_extending V M1 M2 vs xs"
and "OFSM M1"
and "OFSM M2"
and "test_tools M2 M1 FAIL PM V Ω"
and "V'' ∈ N (vs@xs') M1 V"
and "prefix xs' xs"
shows "¬ Rep_Pre M2 M1 vs xs'"
proof
assume "Rep_Pre M2 M1 vs xs'"
then obtain xs1 xs2 s1 s2 where "prefix xs1 xs2"
"prefix xs2 xs'"
"xs1 ≠ xs2"
"io_targets M2 (initial M2) (vs @ xs1) = {s2}"
"io_targets M2 (initial M2) (vs @ xs2) = {s2}"
"io_targets M1 (initial M1) (vs @ xs1) = {s1}"
"io_targets M1 (initial M1) (vs @ xs2) = {s1}"
by auto
then have "s2 ∈ io_targets M2 (initial M2) (vs @ xs1)"
"s2 ∈ io_targets M2 (initial M2) (vs @ xs2)"
"s1 ∈ io_targets M1 (initial M1) (vs @ xs1)"
"s1 ∈ io_targets M1 (initial M1) (vs @ xs2)"
by auto
have "vs@xs1 ∈ L M1"
using io_target_implies_L[OF ‹s1 ∈ io_targets M1 (initial M1) (vs @ xs1)›] by assumption
have "vs@xs2 ∈ L M1"
using io_target_implies_L[OF ‹s1 ∈ io_targets M1 (initial M1) (vs @ xs2)›] by assumption
have "vs@xs1 ∈ L M2"
using io_target_implies_L[OF ‹s2 ∈ io_targets M2 (initial M2) (vs @ xs1)›] by assumption
have "vs@xs2 ∈ L M2"
using io_target_implies_L[OF ‹s2 ∈ io_targets M2 (initial M2) (vs @ xs2)›] by assumption
obtain tr1_1 where "path M1 (vs@xs1 || tr1_1) (initial M1)"
"length tr1_1 = length (vs@xs1)"
"target (vs@xs1 || tr1_1) (initial M1) = s1"
using ‹s1 ∈ io_targets M1 (initial M1) (vs @ xs1)› by auto
obtain tr1_2 where "path M1 (vs@xs2 || tr1_2) (initial M1)"
"length tr1_2 = length (vs@xs2)"
"target (vs@xs2 || tr1_2) (initial M1) = s1"
using ‹s1 ∈ io_targets M1 (initial M1) (vs @ xs2)› by auto
obtain tr2_1 where "path M2 (vs@xs1 || tr2_1) (initial M2)"
"length tr2_1 = length (vs@xs1)"
"target (vs@xs1 || tr2_1) (initial M2) = s2"
using ‹s2 ∈ io_targets M2 (initial M2) (vs @ xs1)› by auto
obtain tr2_2 where "path M2 (vs@xs2 || tr2_2) (initial M2)"
"length tr2_2 = length (vs@xs2)"
"target (vs@xs2 || tr2_2) (initial M2) = s2"
using ‹s2 ∈ io_targets M2 (initial M2) (vs @ xs2)› by auto
have "productF M2 M1 FAIL PM"
using assms(4) by auto
have "well_formed M1"
using assms(2) by auto
have "well_formed M2"
using assms(3) by auto
have "observable PM"
by (meson assms(2) assms(3) assms(4) observable_productF)
have "length (vs@xs1) = length tr2_1"
using ‹length tr2_1 = length (vs @ xs1)› by presburger
then have "length tr2_1 = length tr1_1"
using ‹length tr1_1 = length (vs@xs1)› by presburger
have "vs@xs1 ∈ L PM"
using productF_path_inclusion[OF ‹length (vs@xs1) = length tr2_1› ‹length tr2_1 = length tr1_1›
‹productF M2 M1 FAIL PM› ‹well_formed M2› ‹well_formed M1›]
by (meson Int_iff ‹productF M2 M1 FAIL PM› ‹vs @ xs1 ∈ L M1› ‹vs @ xs1 ∈ L M2› ‹well_formed M1›
‹well_formed M2› productF_language)
have "length (vs@xs2) = length tr2_2"
using ‹length tr2_2 = length (vs @ xs2)› by presburger
then have "length tr2_2 = length tr1_2"
using ‹length tr1_2 = length (vs@xs2)› by presburger
have "vs@xs2 ∈ L PM"
using productF_path_inclusion[OF ‹length (vs@xs2) = length tr2_2› ‹length tr2_2 = length tr1_2›
‹productF M2 M1 FAIL PM› ‹well_formed M2› ‹well_formed M1›]
by (meson Int_iff ‹productF M2 M1 FAIL PM› ‹vs @ xs2 ∈ L M1› ‹vs @ xs2 ∈ L M2› ‹well_formed M1›
‹well_formed M2› productF_language)
have "io_targets PM (initial M2, initial M1) (vs @ xs1) = {(s2, s1)}"
using productF_path_io_targets_reverse
[OF ‹productF M2 M1 FAIL PM› ‹s2 ∈ io_targets M2 (initial M2) (vs @ xs1)›
‹s1 ∈ io_targets M1 (initial M1) (vs @ xs1)› ‹vs @ xs1 ∈ L M2› ‹vs @ xs1 ∈ L M1› ]
proof -
have "∀c f. c ≠ initial (f::('a, 'b, 'c) FSM) ∨ c ∈ nodes f"
by blast
then show ?thesis
by (metis (no_types) ‹⟦observable M2; observable M1; well_formed M2; well_formed M1;
initial M2 ∈ nodes M2; initial M1 ∈ nodes M1⟧
⟹ io_targets PM (initial M2, initial M1) (vs @ xs1) = {(s2, s1)}›
assms(2) assms(3))
qed
have "io_targets PM (initial M2, initial M1) (vs @ xs2) = {(s2, s1)}"
using productF_path_io_targets_reverse
[OF ‹productF M2 M1 FAIL PM› ‹s2 ∈ io_targets M2 (initial M2) (vs @ xs2)›
‹s1 ∈ io_targets M1 (initial M1) (vs @ xs2)› ‹vs @ xs2 ∈ L M2› ‹vs @ xs2 ∈ L M1› ]
proof -
have "∀c f. c ≠ initial (f::('a, 'b, 'c) FSM) ∨ c ∈ nodes f"
by blast
then show ?thesis
by (metis (no_types) ‹⟦observable M2; observable M1; well_formed M2; well_formed M1;
initial M2 ∈ nodes M2; initial M1 ∈ nodes M1⟧
⟹ io_targets PM (initial M2, initial M1) (vs @ xs2) = {(s2, s1)}›
assms(2) assms(3))
qed
have "prefix (vs @ xs1) (vs @ xs2)"
using ‹prefix xs1 xs2› by auto
have "sequence_to_failure M1 M2 (vs@xs)"
using assms(1) by auto
have "prefix (vs@xs1) (vs@xs')"
using ‹prefix xs1 xs2› ‹prefix xs2 xs'› prefix_order.dual_order.trans same_prefix_prefix
by blast
have "prefix (vs@xs2) (vs@xs')"
using ‹prefix xs2 xs'› prefix_order.dual_order.trans same_prefix_prefix by blast
have "io_targets PM (initial PM) (vs @ xs1) = {(s2,s1)}"
using ‹io_targets PM (initial M2, initial M1) (vs @ xs1) = {(s2, s1)}› assms(4) by auto
have "io_targets PM (initial PM) (vs @ xs2) = {(s2,s1)}"
using ‹io_targets PM (initial M2, initial M1) (vs @ xs2) = {(s2, s1)}› assms(4) by auto
have "(vs @ xs2) @ (drop (length xs2) xs) = vs@xs"
by (metis ‹prefix xs2 xs'› append_eq_appendI append_eq_conv_conj assms(6) prefixE)
moreover have "io_targets PM (initial PM) (vs@xs) = {FAIL}"
using sequence_to_failure_reaches_FAIL_ob[OF ‹sequence_to_failure M1 M2 (vs@xs)› assms(2,3)
‹productF M2 M1 FAIL PM›]
by assumption
ultimately have "io_targets PM (initial PM) ((vs @ xs2) @ (drop (length xs2) xs)) = {FAIL}"
by auto
have "io_targets PM (s2,s1) (drop (length xs2) xs) = {FAIL}"
using observable_io_targets_split
[OF ‹observable PM›
‹io_targets PM (initial PM) ((vs @ xs2) @ (drop (length xs2) xs)) = {FAIL}›
‹io_targets PM (initial PM) (vs @ xs2) = {(s2, s1)}›]
by assumption
have "io_targets PM (initial PM) (vs@xs1@(drop (length xs2) xs)) = {FAIL}"
using observable_io_targets_append
[OF ‹observable PM› ‹io_targets PM (initial PM) (vs @ xs1) = {(s2,s1)}›
‹io_targets PM (s2,s1) (drop (length xs2) xs) = {FAIL}›]
by simp
have "sequence_to_failure M1 M2 (vs@xs1@(drop (length xs2) xs))"
using sequence_to_failure_alt_def
[OF ‹io_targets PM (initial PM) (vs@xs1@(drop (length xs2) xs)) = {FAIL}› assms(2,3)]
assms(4)
by blast
have "length xs1 < length xs2"
using ‹prefix xs1 xs2› ‹xs1 ≠ xs2› prefix_length_prefix by fastforce
have prefix_drop: "ys = ys1 @ (drop (length ys1)) ys" if "prefix ys1 ys"
for ys ys1 :: "('a × 'b) list"
using that by (induction ys1) (auto elim: prefixE)
then have "xs = (xs1 @ (drop (length xs1) xs))"
using ‹prefix xs1 xs2› ‹prefix xs2 xs'› ‹prefix xs' xs› by simp
then have "length xs1 < length xs"
using prefix_drop[OF ‹prefix xs2 xs'›] ‹prefix xs2 xs'› ‹prefix xs' xs›
using ‹length xs1 < length xs2›
by (auto dest!: prefix_length_le)
have "length (xs1@(drop (length xs2) xs)) < length xs"
using ‹length xs1 < length xs2› ‹length xs1 < length xs› by auto
have "vs ∈ L⇩i⇩n M1 V
∧ sequence_to_failure M1 M2 (vs @ xs1@(drop (length xs2) xs))
∧ length (xs1@(drop (length xs2) xs)) < length xs"
using ‹length (xs1 @ drop (length xs2) xs) < length xs›
‹sequence_to_failure M1 M2 (vs @ xs1 @ drop (length xs2) xs)›
assms(1) minimal_sequence_to_failure_extending.simps
by blast
then have "¬ minimal_sequence_to_failure_extending V M1 M2 vs xs"
by (meson minimal_sequence_to_failure_extending.elims(2))
then show "False"
using assms(1) by linarith
qed
lemma minimal_sequence_to_failure_extending_implies_Rep_Cov :
assumes "minimal_sequence_to_failure_extending V M1 M2 vs xs"
and "OFSM M1"
and "OFSM M2"
and "test_tools M2 M1 FAIL PM V Ω"
and "V'' ∈ N (vs@xsR) M1 V"
and "prefix xsR xs"
shows "¬ Rep_Cov M2 M1 V'' vs xsR"
proof
assume "Rep_Cov M2 M1 V'' vs xsR"
then obtain xs' vs' s2 s1 where "xs' ≠ []"
"prefix xs' xsR"
"vs' ∈ V''"
"io_targets M2 (initial M2) (vs @ xs') = {s2}"
"io_targets M2 (initial M2) (vs') = {s2}"
"io_targets M1 (initial M1) (vs @ xs') = {s1}"
"io_targets M1 (initial M1) (vs') = {s1}"
by auto
then have "s2 ∈ io_targets M2 (initial M2) (vs @ xs')"
"s2 ∈ io_targets M2 (initial M2) (vs')"
"s1 ∈ io_targets M1 (initial M1) (vs @ xs')"
"s1 ∈ io_targets M1 (initial M1) (vs')"
by auto
have "vs@xs' ∈ L M1"
using io_target_implies_L[OF ‹s1 ∈ io_targets M1 (initial M1) (vs @ xs')›] by assumption
have "vs' ∈ L M1"
using io_target_implies_L[OF ‹s1 ∈ io_targets M1 (initial M1) (vs')›] by assumption
have "vs@xs' ∈ L M2"
using io_target_implies_L[OF ‹s2 ∈ io_targets M2 (initial M2) (vs @ xs')›] by assumption
have "vs' ∈ L M2"
using io_target_implies_L[OF ‹s2 ∈ io_targets M2 (initial M2) (vs')›] by assumption
obtain tr1_1 where "path M1 (vs@xs' || tr1_1) (initial M1)"
"length tr1_1 = length (vs@xs')"
"target (vs@xs' || tr1_1) (initial M1) = s1"
using ‹s1 ∈ io_targets M1 (initial M1) (vs @ xs')› by auto
obtain tr1_2 where "path M1 (vs' || tr1_2) (initial M1)"
"length tr1_2 = length (vs')"
"target (vs' || tr1_2) (initial M1) = s1"
using ‹s1 ∈ io_targets M1 (initial M1) (vs')› by auto
obtain tr2_1 where "path M2 (vs@xs' || tr2_1) (initial M2)"
"length tr2_1 = length (vs@xs')"
"target (vs@xs' || tr2_1) (initial M2) = s2"
using ‹s2 ∈ io_targets M2 (initial M2) (vs @ xs')› by auto
obtain tr2_2 where "path M2 (vs' || tr2_2) (initial M2)"
"length tr2_2 = length (vs')"
"target (vs' || tr2_2) (initial M2) = s2"
using ‹s2 ∈ io_targets M2 (initial M2) (vs')› by auto
have "productF M2 M1 FAIL PM"
using assms(4) by auto
have "well_formed M1"
using assms(2) by auto
have "well_formed M2"
using assms(3) by auto
have "observable PM"
by (meson assms(2) assms(3) assms(4) observable_productF)
have "length (vs@xs') = length tr2_1"
using ‹length tr2_1 = length (vs @ xs')› by presburger
then have "length tr2_1 = length tr1_1"
using ‹length tr1_1 = length (vs@xs')› by presburger
have "vs@xs' ∈ L PM"
using productF_path_inclusion[OF ‹length (vs@xs') = length tr2_1› ‹length tr2_1 = length tr1_1›
‹productF M2 M1 FAIL PM› ‹well_formed M2› ‹well_formed M1›]
by (meson Int_iff ‹productF M2 M1 FAIL PM› ‹vs @ xs' ∈ L M1› ‹vs @ xs' ∈ L M2› ‹well_formed M1›
‹well_formed M2› productF_language)
have "length (vs') = length tr2_2"
using ‹length tr2_2 = length (vs')› by presburger
then have "length tr2_2 = length tr1_2"
using ‹length tr1_2 = length (vs')› by presburger
have "vs' ∈ L PM"
using productF_path_inclusion[OF ‹length (vs') = length tr2_2› ‹length tr2_2 = length tr1_2›
‹productF M2 M1 FAIL PM› ‹well_formed M2› ‹well_formed M1›]
by (meson Int_iff ‹productF M2 M1 FAIL PM› ‹vs' ∈ L M1› ‹vs' ∈ L M2› ‹well_formed M1›
‹well_formed M2› productF_language)
have "io_targets PM (initial M2, initial M1) (vs @ xs') = {(s2, s1)}"
using productF_path_io_targets_reverse
[OF ‹productF M2 M1 FAIL PM› ‹s2 ∈ io_targets M2 (initial M2) (vs @ xs')›
‹s1 ∈ io_targets M1 (initial M1) (vs @ xs')› ‹vs @ xs' ∈ L M2› ‹vs @ xs' ∈ L M1› ]
proof -
have "∀c f. c ≠ initial (f::('a, 'b, 'c) FSM) ∨ c ∈ nodes f"
by blast
then show ?thesis
by (metis (no_types) ‹⟦observable M2; observable M1; well_formed M2; well_formed M1;
initial M2 ∈ nodes M2; initial M1 ∈ nodes M1⟧
⟹ io_targets PM (initial M2, initial M1) (vs @ xs') = {(s2, s1)}›
assms(2) assms(3))
qed
have "io_targets PM (initial M2, initial M1) (vs') = {(s2, s1)}"
using productF_path_io_targets_reverse
[OF ‹productF M2 M1 FAIL PM› ‹s2 ∈ io_targets M2 (initial M2) (vs')›
‹s1 ∈ io_targets M1 (initial M1) (vs')› ‹vs' ∈ L M2› ‹vs' ∈ L M1› ]
proof -
have "∀c f. c ≠ initial (f::('a, 'b, 'c) FSM) ∨ c ∈ nodes f"
by blast
then show ?thesis
by (metis (no_types) ‹⟦observable M2; observable M1; well_formed M2; well_formed M1;
initial M2 ∈ nodes M2; initial M1 ∈ nodes M1⟧
⟹ io_targets PM (initial M2, initial M1) (vs') = {(s2, s1)}›
assms(2) assms(3))
qed
have "io_targets PM (initial PM) (vs') = {(s2, s1)}"
by (metis (no_types) ‹io_targets PM (initial M2, initial M1) vs' = {(s2, s1)}›
‹productF M2 M1 FAIL PM› productF_simps(4))
have "sequence_to_failure M1 M2 (vs@xs)"
using assms(1) by auto
have "xs = xs' @ (drop (length xs') xs)"
by (metis ‹prefix xs' xsR› append_assoc append_eq_conv_conj assms(6) prefixE)
then have "io_targets PM (initial M2, initial M1) (vs @ xs' @ (drop (length xs') xs)) = {FAIL}"
by (metis ‹productF M2 M1 FAIL PM› ‹sequence_to_failure M1 M2 (vs @ xs)› assms(2) assms(3)
productF_simps(4) sequence_to_failure_reaches_FAIL_ob)
then have "io_targets PM (initial M2, initial M1) ((vs @ xs') @ (drop (length xs') xs)) = {FAIL}"
by auto
have "io_targets PM (s2, s1) (drop (length xs') xs) = {FAIL}"
using observable_io_targets_split
[OF ‹observable PM›
‹io_targets PM (initial M2,initial M1) ((vs @ xs') @ (drop (length xs') xs)) = {FAIL}›
‹io_targets PM (initial M2, initial M1) (vs @ xs') = {(s2, s1)}›]
by assumption
have "io_targets PM (initial PM) (vs' @ (drop (length xs') xs)) = {FAIL}"
using observable_io_targets_append
[OF ‹observable PM› ‹io_targets PM (initial PM) (vs') = {(s2, s1)}›
‹io_targets PM (s2, s1) (drop (length xs') xs) = {FAIL}›]
by assumption
have "sequence_to_failure M1 M2 (vs' @ (drop (length xs') xs))"
using sequence_to_failure_alt_def
[OF ‹io_targets PM (initial PM) (vs' @ (drop (length xs') xs)) = {FAIL}› assms(2,3)]
assms(4)
by blast
have "length (drop (length xs') xs) < length xs"
by (metis (no_types) ‹xs = xs' @ drop (length xs') xs› ‹xs' ≠ []› length_append
length_greater_0_conv less_add_same_cancel2)
have "vs' ∈ L⇩i⇩n M1 V"
proof -
have "V'' ∈ Perm V M1"
using assms(5) unfolding N.simps by blast
then obtain f where f_def : "V'' = image f V
∧ (∀ v ∈ V . f v ∈ language_state_for_input M1 (initial M1) v)"
unfolding Perm.simps by blast
then obtain v where "v ∈ V" "vs' = f v"
using ‹vs' ∈ V''› by auto
then have "vs' ∈ language_state_for_input M1 (initial M1) v"
using f_def by auto
have "language_state_for_input M1 (initial M1) v = L⇩i⇩n M1 {v}"
by auto
moreover have "{v} ⊆ V"
using ‹v ∈ V› by blast
ultimately have "language_state_for_input M1 (initial M1) v ⊆ L⇩i⇩n M1 V"
unfolding language_state_for_inputs.simps language_state_for_input.simps by blast
then show ?thesis
using‹vs' ∈ language_state_for_input M1 (initial M1) v› by blast
qed
have "¬ minimal_sequence_to_failure_extending V M1 M2 vs xs"
using ‹vs' ∈ L⇩i⇩n M1 V›
‹sequence_to_failure M1 M2 (vs' @ (drop (length xs') xs))›
‹length (drop (length xs') xs) < length xs›
using minimal_sequence_to_failure_extending.elims(2) by blast
then show "False"
using assms(1) by linarith
qed
lemma mstfe_no_repetition :
assumes "minimal_sequence_to_failure_extending V M1 M2 vs xs"
and "OFSM M1"
and "OFSM M2"
and "test_tools M2 M1 FAIL PM V Ω"
and "V'' ∈ N (vs@xs') M1 V"
and "prefix xs' xs"
shows "¬ Rep_Pre M2 M1 vs xs'"
and "¬ Rep_Cov M2 M1 V'' vs xs'"
using minimal_sequence_to_failure_extending_implies_Rep_Pre[OF assms]
minimal_sequence_to_failure_extending_implies_Rep_Cov[OF assms]
by linarith+
subsection ‹ Sufficiency of the test suite to test for reduction ›
text ‹
The following lemma proves that set of input sequences generated in the final iteration of the
@{verbatim TS} function constitutes a test suite sufficient to test for reduction the FSMs it has
been generated for.
This proof is performed by contradiction: If the test suite is not sufficient, then some minimal
sequence to a failure extending the deterministic state cover must exist. Due to the test suite
being assumed insufficient, this sequence cannot be contained in it and hence a prefix of it must
have been contained in one of the sets calculated by the @{verbatim R} function. This is only
possible if the prefix is not a minimal sequence to a failure extending the deterministic state
cover or if the test suite observes a failure, both of which violates the assumptions.
›
lemma asc_sufficiency :
assumes "OFSM M1"
and "OFSM M2"
and "asc_fault_domain M2 M1 m"
and "test_tools M2 M1 FAIL PM V Ω"
and "final_iteration M2 M1 Ω V m i"
shows "M1 ≼⟦(TS M2 M1 Ω V m i) . Ω⟧ M2 ⟶ M1 ≼ M2"
proof
assume "atc_io_reduction_on_sets M1 (TS M2 M1 Ω V m i) Ω M2"
show "M1 ≼ M2"
proof (rule ccontr)
let ?TS = "λ n . TS M2 M1 Ω V m n"
let ?C = "λ n . C M2 M1 Ω V m n"
let ?RM = "λ n . RM M2 M1 Ω V m n"
assume "¬ M1 ≼ M2"
obtain vs xs where "minimal_sequence_to_failure_extending V M1 M2 vs xs"
using assms(1) assms(2) assms(4)
minimal_sequence_to_failure_extending_det_state_cover_ob[OF _ _ _ _ ‹¬ M1 ≼ M2›, of V]
by blast
then have "vs ∈ L⇩i⇩n M1 V"
"sequence_to_failure M1 M2 (vs @ xs)"
"¬ (∃ io' . ∃ w' ∈ L⇩i⇩n M1 V . sequence_to_failure M1 M2 (w' @ io')
∧ length io' < length xs)"
by auto
then have "vs@xs ∈ L M1 - L M2"
by auto
have "vs@xs ∈ L⇩i⇩n M1 {map fst (vs@xs)}"
by (metis (full_types) Diff_iff ‹vs @ xs ∈ L M1 - L M2› insertI1
language_state_for_inputs_map_fst)
have "vs@xs ∉ L⇩i⇩n M2 {map fst (vs@xs)}"
by (meson Diff_iff ‹vs @ xs ∈ L M1 - L M2› language_state_for_inputs_in_language_state
subsetCE)
have "finite V"
using det_state_cover_finite assms(4,2) by auto
then have "finite (?TS i)"
using TS_finite[of V M2] assms(2) by auto
then have "io_reduction_on M1 (?TS i) M2"
using io_reduction_from_atc_io_reduction
[OF ‹atc_io_reduction_on_sets M1 (TS M2 M1 Ω V m i) Ω M2›]
by auto
have "map fst (vs@xs) ∉ ?TS i"
proof -
have f1: "∀ps P Pa. (ps::('a × 'b) list) ∉ P - Pa ∨ ps ∈ P ∧ ps ∉ Pa"
by blast
have "∀P Pa ps. ¬ P ⊆ Pa ∨ (ps::('a × 'b) list) ∈ Pa ∨ ps ∉ P"
by blast
then show ?thesis
using f1 by (metis (no_types) ‹vs @ xs ∈ L M1 - L M2› ‹io_reduction_on M1 (?TS i) M2›
language_state_for_inputs_in_language_state language_state_for_inputs_map_fst)
qed
have "map fst vs ∈ V"
using ‹vs ∈ L⇩i⇩n M1 V› by auto
let ?stf = "map fst (vs@xs)"
let ?stfV = "map fst vs"
let ?stfX = "map fst xs"
have "?stf = ?stfV @ ?stfX"
by simp
then have "?stfV @ ?stfX ∉ ?TS i"
using ‹?stf ∉ ?TS i› by auto
have "mcp (?stfV @ ?stfX) V ?stfV"
by (metis ‹map fst (vs @ xs) = map fst vs @ map fst xs›
‹minimal_sequence_to_failure_extending V M1 M2 vs xs› assms(1) assms(2) assms(4)
minimal_sequence_to_failure_extending_mcp)
have "set ?stf ⊆ inputs M1"
by (meson DiffD1 ‹vs @ xs ∈ L M1 - L M2› assms(1) language_state_inputs)
then have "set ?stf ⊆ inputs M2"
using assms(3) by blast
moreover have "set ?stf = set ?stfV ∪ set ?stfX"
by simp
ultimately have "set ?stfX ⊆ inputs M2"
by blast
obtain xr j where "xr ≠ ?stfX"
"prefix xr ?stfX"
"Suc j ≤ i"
"?stfV@xr ∈ RM M2 M1 Ω V m (Suc j)"
using TS_non_containment_causes_final_suc[OF ‹?stfV @ ?stfX ∉ ?TS i›
‹mcp (?stfV @ ?stfX) V ?stfV› ‹set ?stfX ⊆ inputs M2› assms(5,2)]
by blast
let ?yr = "take (length xr) (map snd xs)"
have "length ?yr = length xr"
using ‹prefix xr (map fst xs)› prefix_length_le by fastforce
have "(xr || ?yr) = take (length xr) xs"
by (metis (no_types, opaque_lifting) ‹prefix xr (map fst xs)› append_eq_conv_conj prefixE take_zip
zip_map_fst_snd)
have "prefix (vs@(xr || ?yr)) (vs@xs)"
by (simp add: ‹xr || take (length xr) (map snd xs) = take (length xr) xs› take_is_prefix)
have "xr = take (length xr) (map fst xs)"
by (metis ‹length (take (length xr) (map snd xs)) = length xr›
‹xr || take (length xr) (map snd xs) = take (length xr) xs› map_fst_zip take_map)
have "vs@(xr || ?yr) ∈ L M1"
by (metis DiffD1 ‹prefix (vs @ (xr || take (length xr) (map snd xs))) (vs @ xs)›
‹vs @ xs ∈ L M1 - L M2› language_state_prefix prefixE)
then have "vs@(xr || ?yr) ∈ L⇩i⇩n M1 {?stfV @ xr}"
by (metis ‹length (take (length xr) (map snd xs)) = length xr› insertI1
language_state_for_inputs_map_fst map_append map_fst_zip)
have "length xr < length xs"
by (metis ‹xr = take (length xr) (map fst xs)› ‹xr ≠ map fst xs› not_le_imp_less take_all
take_map)
from ‹?stfV@xr ∈ RM M2 M1 Ω V m (Suc j)› have "?stfV@xr ∈ {xs' ∈ C M2 M1 Ω V m (Suc j) .
(¬ (L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'}))
∨ (∀ io ∈ L⇩i⇩n M1 {xs'} .
(∃ V'' ∈ N io M1 V .
(∃ S1 .
(∃ vs xs .
io = (vs@xs)
∧ mcp (vs@xs) V'' vs
∧ S1 ⊆ nodes M2
∧ (∀ s1 ∈ S1 . ∀ s2 ∈ S1 .
s1 ≠ s2 ⟶
(∀ io1 ∈ RP M2 s1 vs xs V'' .
∀ io2 ∈ RP M2 s2 vs xs V'' .
B M1 io1 Ω ≠ B M1 io2 Ω ))
∧ m < LB M2 M1 vs xs (TS M2 M1 Ω V m j ∪ V) S1 Ω V'' ))))}"
unfolding RM.simps by blast
moreover have "∀ xs' ∈ ?C (Suc j) . L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'}"
proof
fix xs' assume "xs' ∈ ?C (Suc j)"
from ‹Suc j ≤ i› have "?C (Suc j) ⊆ ?TS i"
using C_subset TS_subset by blast
then have "{xs'} ⊆ ?TS i"
using ‹xs' ∈ ?C (Suc j)› by blast
show "L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'}"
using io_reduction_on_subset[OF ‹io_reduction_on M1 (?TS i) M2› ‹{xs'} ⊆ ?TS i›]
by assumption
qed
ultimately have "(∀ io ∈ L⇩i⇩n M1 {?stfV@xr} .
(∃ V'' ∈ N io M1 V .
(∃ S1 .
(∃ vs xs .
io = (vs@xs)
∧ mcp (vs@xs) V'' vs
∧ S1 ⊆ nodes M2
∧ (∀ s1 ∈ S1 . ∀ s2 ∈ S1 .
s1 ≠ s2 ⟶
(∀ io1 ∈ RP M2 s1 vs xs V'' .
∀ io2 ∈ RP M2 s2 vs xs V'' .
B M1 io1 Ω ≠ B M1 io2 Ω ))
∧ m < LB M2 M1 vs xs (TS M2 M1 Ω V m j ∪ V) S1 Ω V'' ))))"
by blast
then have "
(∃ V'' ∈ N (vs@(xr || ?yr)) M1 V .
(∃ S1 .
(∃ vs' xs' .
vs@(xr || ?yr) = (vs'@xs')
∧ mcp (vs'@xs') V'' vs'
∧ S1 ⊆ nodes M2
∧ (∀ s1 ∈ S1 . ∀ s2 ∈ S1 .
s1 ≠ s2 ⟶
(∀ io1 ∈ RP M2 s1 vs' xs' V'' .
∀ io2 ∈ RP M2 s2 vs' xs' V'' .
B M1 io1 Ω ≠ B M1 io2 Ω ))
∧ m < LB M2 M1 vs' xs' (TS M2 M1 Ω V m j ∪ V) S1 Ω V'' )))"
using ‹vs@(xr || ?yr) ∈ L⇩i⇩n M1 {?stfV @ xr}›
by blast
then obtain V'' S1 vs' xs' where RM_impl :
"V'' ∈ N (vs@(xr || ?yr)) M1 V"
"vs@(xr || ?yr) = (vs'@xs')"
"mcp (vs'@xs') V'' vs'"
"S1 ⊆ nodes M2"
"(∀ s1 ∈ S1 . ∀ s2 ∈ S1 .
s1 ≠ s2 ⟶
(∀ io1 ∈ RP M2 s1 vs' xs' V'' .
∀ io2 ∈ RP M2 s2 vs' xs' V'' .
B M1 io1 Ω ≠ B M1 io2 Ω ))"
" m < LB M2 M1 vs' xs' (TS M2 M1 Ω V m j ∪ V) S1 Ω V''"
by blast
have "?stfV = mcp' (map fst (vs @ (xr || take (length xr) (map snd xs)))) V"
by (metis (full_types) ‹length (take (length xr) (map snd xs)) = length xr›
‹mcp (map fst vs @ map fst xs) V (map fst vs)› ‹prefix xr (map fst xs)› map_append
map_fst_zip mcp'_intro mcp_prefix_of_suffix)
have "is_det_state_cover M2 V"
using assms(4) by blast
moreover have "well_formed M2"
using assms(2) by auto
moreover have "finite V"
using det_state_cover_finite assms(4,2) by auto
ultimately have "vs ∈ V''"
"vs = mcp' (vs @ (xr || take (length xr) (map snd xs))) V''"
using N_mcp_prefix[OF ‹?stfV = mcp' (map fst (vs @ (xr || take (length xr) (map snd xs)))) V›
‹V'' ∈ N (vs@(xr || ?yr)) M1 V›, of M2]
by simp+
have "vs' = vs"
by (metis (no_types) ‹mcp (vs' @ xs') V'' vs'›
‹vs = mcp' (vs @ (xr || take (length xr) (map snd xs))) V''›
‹vs @ (xr || take (length xr) (map snd xs)) = vs' @ xs'› mcp'_intro)
then have "xs' = (xr || ?yr)"
using ‹vs @ (xr || take (length xr) (map snd xs)) = vs' @ xs'› by blast
have "V ⊆ ?TS i"
proof -
have "1 ≤ i"
using ‹Suc j ≤ i› by linarith
then have "?TS 1 ⊆ ?TS i"
using TS_subset by blast
then show ?thesis
by auto
qed
have "?stfV@xr ∈ ?C (Suc j)"
using ‹?stfV@xr ∈ RM M2 M1 Ω V m (Suc j)› unfolding RM.simps by blast
have "(∀vs'a∈V''. prefix vs'a (vs' @ xs') ⟶ length vs'a ≤ length vs')"
using ‹mcp (vs' @ xs') V'' vs'› by auto
moreover have "atc_io_reduction_on_sets M1 (?TS j ∪ V) Ω M2"
proof -
have "j < i"
using ‹Suc j ≤ i› by auto
then have "?TS j ⊆ ?TS i"
by (simp add: TS_subset)
then show ?thesis
using atc_io_reduction_on_subset
[OF ‹atc_io_reduction_on_sets M1 (TS M2 M1 Ω V m i) Ω M2›, of "?TS j"]
by (meson Un_subset_iff ‹V ⊆ ?TS i› ‹atc_io_reduction_on_sets M1 (TS M2 M1 Ω V m i) Ω M2›
atc_io_reduction_on_subset)
qed
moreover have "finite (?TS j ∪ V)"
proof -
have "finite (?TS j)"
using TS_finite[OF ‹finite V›, of M2 M1 Ω m j] assms(2) by auto
then show ?thesis
using ‹finite V› by blast
qed
moreover have "V ⊆ ?TS j ∪ V"
by blast
moreover have "(∀ p . (prefix p xs' ∧ p ≠ xs') ⟶ map fst (vs' @ p) ∈ ?TS j ∪ V)"
proof
fix p
show "prefix p xs' ∧ p ≠ xs' ⟶ map fst (vs' @ p) ∈ TS M2 M1 Ω V m j ∪ V"
proof
assume "prefix p xs' ∧ p ≠ xs'"
have "prefix (map fst (vs' @ p)) (map fst (vs' @ xs'))"
by (simp add: ‹prefix p xs' ∧ p ≠ xs'› map_mono_prefix)
have "prefix (map fst (vs' @ p)) (?stfV @ xr)"
using ‹length (take (length xr) (map snd xs)) = length xr›
‹prefix (map fst (vs' @ p)) (map fst (vs' @ xs'))›
‹vs' = vs› ‹xs' = xr || take (length xr) (map snd xs)›
by auto
then have "prefix (map fst vs' @ map fst p) (?stfV @ xr)"
by simp
then have "prefix (map fst p) xr"
by (simp add: ‹vs' = vs›)
have "?stfV @ xr ∈ ?TS (Suc j)"
proof (cases j)
case 0
then show ?thesis
using ‹map fst vs @ xr ∈ C M2 M1 Ω V m (Suc j)› by auto
next
case (Suc nat)
then show ?thesis
using TS.simps(3) ‹map fst vs @ xr ∈ C M2 M1 Ω V m (Suc j)› by blast
qed
have "mcp (map fst vs @ xr) V (map fst vs)"
using ‹mcp (map fst vs @ map fst xs) V (map fst vs)› ‹prefix xr (map fst xs)›
mcp_prefix_of_suffix
by blast
have "map fst vs @ map fst p ∈ TS M2 M1 Ω V m (Suc j)"
using TS_prefix_containment[OF ‹?stfV @ xr ∈ ?TS (Suc j)›
‹mcp (map fst vs @ xr) V (map fst vs)›
‹prefix (map fst p) xr›]
by assumption
have "Suc (length xr) = (Suc j)"
using C_index[OF ‹?stfV@xr ∈ ?C (Suc j)› ‹mcp (map fst vs @ xr) V (map fst vs)›]
by assumption
have"Suc (length p) < (Suc j)"
proof -
have "map fst xs' = xr"
by (metis ‹xr = take (length xr) (map fst xs)›
‹xr || take (length xr) (map snd xs) = take (length xr) xs›
‹xs' = xr || take (length xr) (map snd xs)› take_map)
then show ?thesis
by (metis (no_types) Suc_less_eq ‹Suc (length xr) = Suc j› ‹prefix p xs' ∧ p ≠ xs'›
append_eq_conv_conj length_map nat_less_le prefixE prefix_length_le take_all)
qed
have "mcp (map fst vs @ map fst p) V (map fst vs)"
using ‹mcp (map fst vs @ xr) V (map fst vs)› ‹prefix (map fst p) xr› mcp_prefix_of_suffix
by blast
then have "map fst vs @ map fst p ∈ ?C (Suc (length (map fst p)))"
using TS_index(2)[OF ‹map fst vs @ map fst p ∈ TS M2 M1 Ω V m (Suc j)›] by auto
have "map fst vs @ map fst p ∈ ?TS j"
using TS_union[of M2 M1 Ω V m j]
proof -
have "Suc (length p) ∈ {0..<Suc j}"
using ‹Suc (length p) < Suc j› by force
then show ?thesis
by (metis UN_I ‹TS M2 M1 Ω V m j = (⋃j∈set [0..<Suc j]. C M2 M1 Ω V m j)›
‹map fst vs @ map fst p ∈ C M2 M1 Ω V m (Suc (length (map fst p)))›
length_map set_upt)
qed
then show "map fst (vs' @ p) ∈ TS M2 M1 Ω V m j ∪ V"
by (simp add: ‹vs' = vs›)
qed
qed
moreover have "vs' @ xs' ∈ L M2 ∩ L M1"
by (metis (no_types, lifting) IntI RM_impl(2)
‹∀xs'∈C M2 M1 Ω V m (Suc j). L⇩i⇩n M1 {xs'} ⊆ L⇩i⇩n M2 {xs'}›
‹map fst vs @ xr ∈ C M2 M1 Ω V m (Suc j)›
‹vs @ (xr || take (length xr) (map snd xs)) ∈ L⇩i⇩n M1 {map fst vs @ xr}›
language_state_for_inputs_in_language_state subsetCE)
ultimately have "Prereq M2 M1 vs' xs' (?TS j ∪ V) S1 Ω V''"
using RM_impl(4,5) unfolding Prereq.simps by blast
have "V'' ∈ Perm V M1"
using ‹V'' ∈ N (vs@(xr || ?yr)) M1 V› unfolding N.simps by blast
have ‹prefix (xr || ?yr) xs›
by (simp add: ‹xr || take (length xr) (map snd xs) = take (length xr) xs› take_is_prefix)
have "¬ Rep_Pre M2 M1 vs (xr || ?yr)"
using minimal_sequence_to_failure_extending_implies_Rep_Pre
[OF ‹minimal_sequence_to_failure_extending V M1 M2 vs xs› assms(1,2)
‹test_tools M2 M1 FAIL PM V Ω› RM_impl(1)
‹prefix (xr || take (length xr) (map snd xs)) xs›]
by assumption
then have "¬ Rep_Pre M2 M1 vs' xs'"
using ‹vs' = vs› ‹xs' = xr || ?yr› by blast
have "¬ Rep_Cov M2 M1 V'' vs (xr || ?yr)"
using minimal_sequence_to_failure_extending_implies_Rep_Cov
[OF ‹minimal_sequence_to_failure_extending V M1 M2 vs xs› assms(1,2)
‹test_tools M2 M1 FAIL PM V Ω› RM_impl(1)
‹prefix (xr || take (length xr) (map snd xs)) xs›]
by assumption
then have "¬ Rep_Cov M2 M1 V'' vs' xs'"
using ‹vs' = vs› ‹xs' = xr || ?yr› by blast
have "vs'@xs' ∈ L M1"
using ‹vs @ (xr || take (length xr) (map snd xs)) ∈ L M1›
‹vs' = vs› ‹xs' = xr || take (length xr) (map snd xs)›
by blast
have "LB M2 M1 vs' xs' (?TS j ∪ V) S1 Ω V'' ≤ card (nodes M1)"
using LB_count[OF ‹vs'@xs' ∈ L M1› assms(1,2,3) ‹test_tools M2 M1 FAIL PM V Ω›
‹V'' ∈ Perm V M1› ‹Prereq M2 M1 vs' xs' (?TS j ∪ V) S1 Ω V''›
‹¬ Rep_Pre M2 M1 vs' xs'› ‹ ¬ Rep_Cov M2 M1 V'' vs' xs'›]
by assumption
then have "LB M2 M1 vs' xs' (?TS j ∪ V) S1 Ω V'' ≤ m"
using assms(3) by linarith
then show "False"
using ‹m < LB M2 M1 vs' xs' (?TS j ∪ V) S1 Ω V''› by linarith
qed
qed
subsection ‹ Main result ›
text ‹
The following lemmata add to the previous result to show that some FSM @{verbatim M1} is a reduction
of FSM @{verbatim M2} if and only if it is a reduction on the test suite generated by the adaptive
state counting algorithm for these FSMs.
›
lemma asc_soundness :
assumes "OFSM M1"
and "OFSM M2"
shows "M1 ≼ M2 ⟶ atc_io_reduction_on_sets M1 T Ω M2"
using atc_io_reduction_on_sets_reduction assms by blast
lemma asc_main_theorem :
assumes "OFSM M1"
and "OFSM M2"
and "asc_fault_domain M2 M1 m"
and "test_tools M2 M1 FAIL PM V Ω"
and "final_iteration M2 M1 Ω V m i"
shows "M1 ≼ M2 ⟷ atc_io_reduction_on_sets M1 (TS M2 M1 Ω V m i) Ω M2"
by (metis asc_sufficiency assms(1-5) atc_io_reduction_on_sets_reduction)
end