section ‹Test Suites for Language Equivalence› text ‹This file introduces a type for test suites represented as a prefix tree in which each IO-pair is additionally labeled by a boolean value representing whether the IO-pair should be exhibited by the SUT in order to pass the test suite.› theory Test_Suite_Representations imports "../Minimisation" "../Prefix_Tree" begin type_synonym ('b,'c) test_suite = "(('b × 'c) × bool) prefix_tree" (* also reduces the test suite by dropping suffixes after the first element not in LS M q *) function (domintros) test_suite_from_io_tree :: "('a,'b,'c) fsm ⇒ 'a ⇒ ('b × 'c) prefix_tree ⇒ ('b,'c) test_suite" where "test_suite_from_io_tree M q (PT m) = PT (λ ((x,y),b) . case m (x,y) of None ⇒ None | Some t ⇒ (case h_obs M q x y of None ⇒ (if b then None else Some empty) | Some q' ⇒ (if b then Some (test_suite_from_io_tree M q' t) else None)))" by pat_completeness auto termination proof - { fix M :: "('a,'b,'c) fsm" fix q t have "test_suite_from_io_tree_dom (M,q,t)" proof (induction t arbitrary: M q) case (PT m) then have "⋀x y t q'. m (x, y) = Some t ⟹ test_suite_from_io_tree_dom (M, q', t)" by blast then show ?case using test_suite_from_io_tree.domintros[of m q M] by auto qed } then show ?thesis by auto qed subsection ‹Transforming an IO-prefix-tree to a test suite› lemma test_suite_from_io_tree_set : assumes "observable M" and "q ∈ states M" shows "(set (test_suite_from_io_tree M q t)) = ((λ xs . map (λ x . (x,True)) xs) ` (set t ∩ LS M q)) ∪ ((λ xs . (map (λ x . (x,True)) (butlast xs))@[(last xs,False)]) ` {xs@[x] | xs x . xs ∈ set t ∩ LS M q ∧ xs@[x] ∈ set t - LS M q})" (is "?S1 q t = ?S2 q t") proof show "?S1 q t ⊆ ?S2 q t" proof fix xs assume "xs ∈ ?S1 q t" then have "isin (test_suite_from_io_tree M q t) xs" by auto then show "xs ∈ ?S2 q t" using ‹q ∈ states M› proof (induction xs arbitrary: q t) case Nil have "[] ∈ set t" using Nil.prems(1) set_Nil by auto moreover have "[] ∈ LS M q" using Nil.prems(2) by auto ultimately show ?case by auto next case (Cons x' xs) moreover obtain x y b where "x' = ((x,y),b)" by (metis surj_pair) moreover obtain m where "t = PT m" by (meson prefix_tree.exhaust) ultimately have "isin (test_suite_from_io_tree M q (PT m)) (((x,y),b) # xs)" by auto let ?fi = "λ t . (case h_obs M q x y of None ⇒ (if b then None else Some empty) | Some q' ⇒ (if b then Some (test_suite_from_io_tree M q' t) else None))" let ?fo = "case m (x,y) of None ⇒ None | Some t ⇒ ?fi t" obtain tst where "?fo = Some tst" using ‹isin (test_suite_from_io_tree M q (PT m)) (((x,y),b) # xs)› unfolding test_suite_from_io_tree.simps isin.simps by force then have "isin tst xs" using ‹isin (test_suite_from_io_tree M q (PT m)) (((x,y),b) # xs)› by auto obtain t' where "m (x,y) = Some t'" and "?fi t' = Some tst" using ‹?fo = Some tst› by (metis (no_types, lifting) option.case_eq_if option.collapse option.distinct(1)) then consider "h_obs M q x y = None ∧ ¬b ∧ tst = empty" | "∃ q' . h_obs M q x y = Some q' ∧ b ∧ tst = test_suite_from_io_tree M q' t'" unfolding option.case_eq_if using option.collapse[of "h_obs M q x y"] using option.distinct(1) option.inject by metis then show ?case proof cases case 1 then have "h_obs M q x y = None" and "b = False" and "tst = empty" by auto have "isin empty xs" using ‹isin tst xs› ‹tst = empty› by auto then have "xs = []" using set_empty by auto then have *: "x'#xs = [((x,y),b)]" using ‹x' = ((x,y),b)› by auto have "[] ∈ LS M q" using ‹q ∈ states M› by auto moreover have "[] ∈ set t" using set_Nil by auto moreover have "[(x,y)] ∉ LS M q" using ‹h_obs M q x y = None› unfolding h_obs_None[OF ‹observable M›] by auto moreover have "isin t [(x,y)]" unfolding ‹t = PT m› isin.simps using ‹m (x,y) = Some t'› using isin.elims(3) by auto ultimately have "[(x,y)] ∈ {xs @ [x] |xs x. xs ∈ Prefix_Tree.set t ∩ LS M q ∧ xs @ [x] ∈ Prefix_Tree.set t - LS M q}" by auto moreover have "(x'#xs) = ((λ xs . (map (λ x . (x,True)) (butlast xs))@[(last xs,False)]) [(x,y)])" unfolding * ‹b = False› by auto ultimately show ?thesis by blast next case 2 then obtain q' where "h_obs M q x y = Some q'" "b = True" "tst = test_suite_from_io_tree M q' t'" by blast have p1: "isin (test_suite_from_io_tree M q' t') xs" using ‹isin tst xs› ‹tst = test_suite_from_io_tree M q' t'› by auto have p2: "q' ∈ states M" using ‹h_obs M q x y = Some q'› fsm_transition_target unfolding h_obs_Some[OF ‹observable M›] by fastforce have "xs ∈ ?S2 q' t'" using Cons.IH[OF p1 p2] . then consider (a) "xs ∈ map (λx. (x, True)) ` (Prefix_Tree.set t' ∩ LS M q')" | (b) "xs ∈ (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) ` {xs @ [x] |xs x. xs ∈ Prefix_Tree.set t' ∩ LS M q' ∧ xs @ [x] ∈ Prefix_Tree.set t' - LS M q'}" by blast then show ?thesis proof cases case a then obtain xs' where "xs' ∈ set t'" and "xs' ∈ LS M q'" and "xs = map (λx. (x, True)) xs'" by auto have "(x,y)#xs' ∈ set t" using ‹xs' ∈ set t'› ‹m (x,y) = Some t'› unfolding ‹t = PT m› by auto moreover have "(x,y)#xs' ∈ LS M q" using ‹h_obs M q x y = Some q'› ‹xs' ∈ LS M q'› unfolding h_obs_Some[OF ‹observable M›] using LS_prepend_transition[of "(q,x,y,q')" M xs'] by auto moreover have "x'#xs = map (λx. (x, True)) ((x,y)#xs')" unfolding ‹x' = ((x,y),b)› ‹b = True› ‹xs = map (λx. (x, True)) xs'› by auto ultimately show ?thesis by (metis (no_types, lifting) Int_iff UnI1 image_eqI) next case b then obtain xs' where "xs' ∈ {xs @ [x] |xs x. xs ∈ Prefix_Tree.set t' ∩ LS M q' ∧ xs @ [x] ∈ Prefix_Tree.set t' - LS M q'}" and "xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) xs'" by blast moreover obtain bl l where "xs' = bl @ [l]" using calculation by blast ultimately have "bl ∈ set t'" and "bl ∈ LS M q'" and "bl @ [l] ∈ set t'" and "bl@[l] ∉ LS M q'" and "xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl@[l])" by auto have "(x,y)#bl ∈ set t" using ‹bl ∈ set t'› ‹m (x,y) = Some t'› unfolding ‹t = PT m› by auto moreover have "(x,y)#bl ∈ LS M q" using ‹h_obs M q x y = Some q'› ‹bl ∈ LS M q'› unfolding h_obs_Some[OF ‹observable M›] using LS_prepend_transition[of "(q,x,y,q')" M bl] by auto moreover have "(x,y)#(bl @ [l]) ∈ set t" using ‹bl @ [l] ∈ set t'› ‹m (x,y) = Some t'› unfolding ‹t = PT m› by auto moreover have "(x,y)#(bl@[l]) ∉ LS M q" using ‹h_obs M q x y = Some q'› ‹bl@[l] ∉ LS M q'› unfolding h_obs_Some[OF ‹observable M›] using observable_language_transition_target[OF ‹observable M›, of "(q,x,y,q')" "bl@[l]"] unfolding fst_conv snd_conv by blast ultimately have "(x,y)#bl@[l] ∈ {xs @ [x] |xs x. xs ∈ Prefix_Tree.set t ∩ LS M q ∧ xs @ [x] ∈ Prefix_Tree.set t - LS M q}" by fastforce moreover have "x'#xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) ((x,y)#(bl@[l]))" unfolding ‹x' = ((x,y),b)› ‹b = True› ‹xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl@[l])› by auto ultimately show ?thesis by fast qed qed qed qed show "?S2 q t ⊆ ?S1 q t" proof fix xs assume "xs ∈ ?S2 q t" then consider "xs ∈ map (λx. (x, True)) ` (set t ∩ LS M q)" | "xs ∈ (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) ` {xs @ [x] |xs x. xs ∈ Prefix_Tree.set t ∩ LS M q ∧ xs @ [x] ∈ Prefix_Tree.set t - LS M q}" by blast then show "xs ∈ ?S1 q t" proof cases case 1 then show ?thesis using ‹q ∈ states M› proof (induction xs arbitrary: q t) case Nil then show ?case using set_Nil by auto next case (Cons x' xs) obtain xs'' where "xs'' ∈ set t" and "xs'' ∈ LS M q" and "x'#xs = map (λx. (x, True)) xs''" using Cons.prems(1) by (meson IntD1 IntD2 imageE) then obtain x y xs' where "(x,y)#xs' ∈ set t" and "(x,y)#xs' ∈ LS M q" and "x'#xs = map (λx. (x, True)) ((x,y)#xs')" by force then have "x' = ((x,y),True)" and "xs = map (λx. (x, True)) xs'" by auto obtain m where "t = PT m" by (meson prefix_tree.exhaust) have "isin (PT m) ((x,y)#xs')" using ‹(x,y)#xs' ∈ set t› unfolding ‹t = PT m› by auto then obtain t' where "m (x,y) = Some t'" and "isin t' xs'" by (metis case_optionE isin.simps(2)) have "[(x,y)] ∈ LS M q" using ‹(x,y)#xs' ∈ LS M q› language_prefix[of "[(x,y)]" xs' M q] by simp then obtain q' where "h_obs M q x y = Some q'" using h_obs_None[OF ‹observable M›, of q x y] unfolding LS_single_transition by auto have "isin (test_suite_from_io_tree M q (PT m)) (((x,y),True)#xs) = isin (test_suite_from_io_tree M q' t') (xs)" using ‹m (x,y) = Some t'› ‹h_obs M q x y = Some q'› by auto then have *: "x' # xs ∈ set (test_suite_from_io_tree M q t) = (xs ∈ set (test_suite_from_io_tree M q' t'))" unfolding ‹t = PT m› ‹x' = ((x,y),True)› by auto have "xs' ∈ LS M q'" using ‹h_obs M q x y = Some q'› unfolding h_obs_Some[OF ‹observable M›, of q x y] using ‹(x,y)#xs' ∈ LS M q› observable_language_transition_target[OF ‹observable M›] by force moreover have "xs' ∈ set t'" using ‹isin t' xs'› by auto ultimately have p1: "xs ∈ map (λx. (x, True)) ` (set t' ∩ LS M q')" unfolding ‹xs = map (λx. (x, True)) xs'› by auto have p2: "q' ∈ states M" using ‹h_obs M q x y = Some q'› fsm_transition_target unfolding h_obs_Some[OF ‹observable M›] by fastforce show ?case using Cons.IH[OF p1 p2] unfolding * . qed next case 2 then show ?thesis using ‹q ∈ states M› proof (induction xs arbitrary: q t) case Nil then show ?case using set_Nil by auto next case (Cons x' xs) then obtain xsT where "x'#xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) xsT" and "xsT ∈ {xs @ [x] |xs x. xs ∈ Prefix_Tree.set t ∩ LS M q ∧ xs @ [x] ∈ Prefix_Tree.set t - LS M q}" by blast moreover obtain bl l where "xsT = bl @ [l]" using calculation by auto ultimately have "bl ∈ set t" and "bl ∈ LS M q" and "bl @ [l] ∈ set t" and "bl@[l] ∉ LS M q" and "x'#xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl@[l])" by auto obtain m where "t = PT m" by (meson prefix_tree.exhaust) show ?case proof (cases xs) case Nil then have "x' = (l,False)" and "bl = []" using ‹x'#xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl@[l])› by auto moreover obtain x y where "l = (x,y)" using prod.exhaust by metis ultimately have "[(x,y)] ∈ set t" and "[(x,y)] ∉ LS M q" using ‹bl @ [l] ∈ set t› ‹bl@[l] ∉ LS M q› by auto obtain t' where "m (x,y) = Some t'" using ‹[(x,y)] ∈ set t› unfolding ‹t = PT m› by force moreover have "h_obs M q x y = None" using ‹[(x,y)] ∉ LS M q› unfolding h_obs_None[OF ‹observable M›] LS_single_transition by auto ultimately have "isin (test_suite_from_io_tree M q (PT m)) (x'#xs) = isin empty []" unfolding Nil ‹x' = (l,False)› test_suite_from_io_tree.simps isin.simps ‹l = (x,y)› by (simp add: Prefix_Tree.empty_def) then show ?thesis using set_Nil unfolding ‹t = PT m› by auto next case (Cons x'' xs'') then obtain x y bl' where "bl = (x,y)#bl'" using ‹x'#xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl@[l])› by (metis append.left_neutral butlast_snoc list.inject list.simps(8) neq_Nil_conv surj_pair) then have "x' = ((x,y),True)" and "xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl'@[l])" using ‹x'#xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl@[l])› by auto have "isin (PT m) ((x,y)#(bl'@[l]))" using ‹bl@[l] ∈ set t› unfolding ‹bl = (x,y)#bl'› ‹t = PT m› by auto then obtain t' where "m (x,y) = Some t'" and "isin t' (bl'@[l])" unfolding isin.simps using case_optionE by blast have "[(x,y)] ∈ LS M q" using ‹bl ∈ LS M q› language_prefix[of "[(x,y)]" bl' M q] unfolding ‹bl = (x,y)#bl'› by auto then obtain q' where "h_obs M q x y = Some q'" using h_obs_None[OF ‹observable M›] unfolding LS_single_transition by force then have p2: "q' ∈ states M" using fsm_transition_target unfolding h_obs_Some[OF ‹observable M›] by fastforce have "bl' ∈ set t'" using ‹isin t' (bl'@[l])› isin_prefix by auto moreover have "bl' ∈ LS M q'" using ‹h_obs M q x y = Some q'› unfolding h_obs_Some[OF ‹observable M›] using ‹bl ∈ LS M q› observable_language_transition_target[OF ‹observable M›] unfolding ‹bl = (x,y)#bl'› by force moreover have "bl'@[l] ∈ set t'" using ‹isin t' (bl'@[l])› by auto moreover have "bl'@[l] ∉ LS M q'" proof - have "(x, y) # (bl' @ [l]) ∉ LS M q" using ‹bl@[l] ∉ LS M q› unfolding ‹bl = (x,y)#bl'› by auto then show ?thesis using ‹h_obs M q x y = Some q'› unfolding h_obs_Some[OF ‹observable M›] using LS_prepend_transition[of "(q,x,y,q')" M "bl'@[l]"] unfolding ‹bl = (x,y)#bl'› fst_conv snd_conv by blast qed ultimately have "(bl'@[l]) ∈ {xs @ [x] |xs x. xs ∈ Prefix_Tree.set t' ∩ LS M q' ∧ xs @ [x] ∈ Prefix_Tree.set t' - LS M q'}" by blast moreover have "xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl'@[l])" using ‹x'#xs = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (bl@[l])› unfolding Nil ‹bl = (x,y)#bl'› by auto ultimately have "xs ∈ Prefix_Tree.set (test_suite_from_io_tree M q' t')" using Cons.IH[of t', OF _ p2] by blast then have "isin (test_suite_from_io_tree M q t) (x'#xs)" unfolding ‹x' = ((x,y),True)› ‹t = PT m› unfolding test_suite_from_io_tree.simps isin.simps using ‹m (x,y) = Some t'› ‹h_obs M q x y = Some q'› by auto then show ?thesis by auto qed qed qed qed qed (* function written using xyb instead of immediately unfolding to e.g. ((x,y),b) as the resulting domintros fact was too weak see also: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-September/msg00001.html *) function (domintros) passes_test_suite :: "('a,'b,'c) fsm ⇒ 'a ⇒ ('b,'c) test_suite ⇒ bool" where "passes_test_suite M q (PT m) = (∀ xyb ∈ dom m . case h_obs M q (fst (fst xyb)) (snd (fst xyb)) of None ⇒ ¬(snd xyb) | Some q' ⇒ snd xyb ∧ passes_test_suite M q' (case m xyb of Some t ⇒ t))" by pat_completeness auto termination proof - { fix M :: "('a,'b,'c) fsm" fix q t have "passes_test_suite_dom (M,q,t)" proof (induction t arbitrary: M q) case (PT m) then have "⋀ ab ba bb y x2 . m ((ab, ba), bb) = Some y ⟹ passes_test_suite_dom (M, x2, y)" by blast then show ?case using passes_test_suite.domintros[of q M m] by auto qed } then show ?thesis by auto qed lemma passes_test_suite_iff : assumes "observable M" and "q ∈ states M" shows "passes_test_suite M q t = (∀ iob ∈ set t . (map fst iob) ∈ LS M q ⟷ list_all snd iob)" proof show "passes_test_suite M q t ⟹ ∀iob∈Prefix_Tree.set t. (map fst iob ∈ LS M q) = list_all snd iob" proof fix iob assume "passes_test_suite M q t" and "iob ∈ Prefix_Tree.set t" then show "(map fst iob ∈ LS M q) = list_all snd iob" using ‹q ∈ states M› proof (induction iob arbitrary: q t) case Nil then show ?case by auto next case (Cons a iob) obtain m where "t = PT m" by (meson prefix_tree.exhaust) then have "isin (PT m) (a#iob)" using ‹a # iob ∈ Prefix_Tree.set t› by simp moreover obtain x y b where "a = ((x,y),b)" by (metis old.prod.exhaust) ultimately obtain t' where "m ((x,y),b) = Some t'" and "isin t' iob" unfolding isin.simps using case_optionE by blast then have "((x,y),b) ∈ dom m" by auto then have *: "(case h_obs M q x y of None ⇒ ¬b | Some q' ⇒ b ∧ passes_test_suite M q' (case m ((x,y),b) of Some t ⇒ t))" using ‹passes_test_suite M q t› ‹((x,y),b) ∈ dom m› unfolding ‹t = PT m› passes_test_suite.simps by (metis fst_conv snd_conv) show ?case proof (cases b) case False then have "h_obs M q x y = None" using * using case_optionE by blast then have "[(x,y)] ∉ LS M q" unfolding h_obs_None[OF ‹observable M›] by auto then have "(map fst (a#iob)) ∉ LS M q" unfolding ‹a = ((x,y),b)› using language_prefix[of "[(x,y)]" "map fst iob" M q] by fastforce then show ?thesis unfolding ‹a = ((x,y),b)› using False by auto next case True then obtain q' where "h_obs M q x y = Some q'" using * case_optionE by blast then have **: "((map fst (a#iob)) ∈ LS M q) = ((map fst iob) ∈ LS M q')" using observable_language_transition_target[OF ‹observable M›, of "(q,x,y,q')" "map fst iob"] unfolding ‹a = ((x,y),b)› h_obs_Some[OF ‹observable M›] fst_conv snd_conv by (metis (no_types, lifting) LS_prepend_transition fst_conv list.simps(9) mem_Collect_eq singletonI snd_conv) have ***: "list_all snd (a#iob) = list_all snd iob" unfolding ‹a = ((x,y),b)› using True by auto have "passes_test_suite M q' t'" using ‹passes_test_suite M q t› ‹((x,y),b) ∈ dom m› ‹h_obs M q x y = Some q'› True unfolding ‹t = PT m› passes_test_suite.simps using * ‹m ((x, y), b) = Some t'› by auto moreover have "iob ∈ set t'" using ‹isin t' iob› by auto moreover have "q' ∈ states M" using ‹h_obs M q x y = Some q'› fsm_transition_target unfolding h_obs_Some[OF ‹observable M›] by fastforce ultimately show ?thesis using Cons.IH unfolding ** *** by blast qed qed qed show "∀iob∈Prefix_Tree.set t. (map fst iob ∈ LS M q) = list_all snd iob ⟹ passes_test_suite M q t" proof (induction t arbitrary: q) case (PT m) have "⋀ xyb . xyb ∈ dom m ⟹ case h_obs M q (fst (fst xyb)) (snd (fst xyb)) of None ⇒ ¬ snd xyb | Some q' ⇒ snd xyb ∧ passes_test_suite M q' (case m xyb of Some t ⇒ t)" proof - fix xyb assume "xyb ∈ dom m" moreover obtain x y b where "xyb = ((x,y),b)" by (metis old.prod.exhaust) ultimately obtain t' where "m ((x,y),b) = Some t'" by auto then have "isin (PT m) [((x,y),b)]" by auto then have "[((x,y),b)] ∈ set (PT m)" by auto then have "(map fst [((x,y),b)] ∈ LS M q) = list_all snd [((x,y),b)]" using ‹∀iob∈Prefix_Tree.set (PT m). (map fst iob ∈ LS M q) = list_all snd iob› by blast then have "([(x,y)] ∈ LS M q) = b" by auto show "case h_obs M q (fst (fst xyb)) (snd (fst xyb)) of None ⇒ ¬ snd xyb | Some q' ⇒ snd xyb ∧ passes_test_suite M q' (case m xyb of Some t ⇒ t)" proof (cases "h_obs M q x y") case None then have "[(x,y)] ∉ LS M q" unfolding h_obs_None[OF ‹observable M›] by auto then have "b = False" using ‹([(x,y)] ∈ LS M q) = b› by blast then show ?thesis using None unfolding ‹xyb = ((x,y),b)› by auto next case (Some q') then have "[(x,y)] ∈ LS M q" unfolding h_obs_Some[OF ‹observable M›] LS_single_transition by force then have "b" using ‹([(x,y)] ∈ LS M q) = b› by blast moreover have "passes_test_suite M q' t'" proof - have "Some t' ∈ range m" using ‹m ((x,y),b) = Some t'› by (metis range_eqI) moreover have "t' ∈ set_option (Some t')" by auto moreover have "∀iob∈Prefix_Tree.set t'. (map fst iob ∈ LS M q') = list_all snd iob" proof fix iob assume "iob ∈ Prefix_Tree.set t'" then have "isin t' iob" by auto then have "isin (PT m) (((x,y),b)#iob)" using ‹m ((x,y),b) = Some t'› by auto then have "((x,y),b)#iob ∈ set (PT m)" by auto then have "(map fst (((x,y),b)#iob) ∈ LS M q) = list_all snd (((x,y),b)#iob)" using PT.prems by blast moreover have "(map fst (((x,y),b)#iob) ∈ LS M q) = (map fst iob ∈ LS M q')" using observable_language_transition_target[OF ‹observable M›, of "(q,x,y,q')" "map fst iob"] by (metis (no_types, lifting) LS_prepend_transition Some h_obs_Some[OF ‹observable M›] fst_conv list.simps(9) mem_Collect_eq singletonI snd_conv) moreover have "list_all snd (((x,y),b)#iob) = list_all snd iob" using ‹b› by auto ultimately show "(map fst iob ∈ LS M q') = list_all snd iob" by simp qed ultimately show ?thesis using PT.IH by blast qed ultimately show ?thesis using ‹m ((x,y),b) = Some t'› ‹xyb = ((x,y),b)› Some by simp qed qed then show ?case by auto qed qed (* Main result of the test_suite transformation: an IO prefix_tree representing a set of IO sequences can be transformed into a test suite such that passing the test suite equals passing the original set of sequences *) lemma passes_test_suite_from_io_tree : assumes "observable M" and "observable I" and "qM ∈ states M" and "qI ∈ states I" shows "passes_test_suite I qI (test_suite_from_io_tree M qM t) = ((set t ∩ LS M qM) = (set t ∩ LS I qI))" proof - define ts where "ts = test_suite_from_io_tree M qM t" then have "passes_test_suite I qI (test_suite_from_io_tree M qM t) = (∀iob∈set ts. (map fst iob ∈ LS I qI) = list_all snd iob)" using passes_test_suite_iff[OF assms(2,4), of ts] by auto also have "… = ((set t ∩ LS M qM) = (set t ∩ LS I qI))" proof have ts_set: "set ts = map (λx. (x, True)) ` (set t ∩ LS M qM) ∪ (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) ` {xs @ [x] |xs x. xs ∈ set t ∩ LS M qM ∧ xs @ [x] ∈ set t - LS M qM}" using test_suite_from_io_tree_set[OF assms(1,3), of t] ‹ts = test_suite_from_io_tree M qM t› by auto show "∀iob∈Prefix_Tree.set ts. (map fst iob ∈ LS I qI) = list_all snd iob ⟹ set t ∩ LS M qM = set t ∩ LS I qI" proof - assume "∀iob∈Prefix_Tree.set ts. (map fst iob ∈ LS I qI) = list_all snd iob" then have ts_assm: "⋀ iob . iob ∈ set ts ⟹ (map fst iob ∈ LS I qI) = list_all snd iob" by blast show "set t ∩ LS M qM = set t ∩ LS I qI" proof show "set t ∩ LS M qM ⊆ set t ∩ LS I qI" proof fix io assume "io ∈ set t ∩ LS M qM" then have "map (λx. (x, True)) io ∈ set ts" unfolding ts_set by auto moreover have "list_all snd (map (λx. (x, True)) io)" by (induction io; auto) moreover have "map fst (map (λx. (x, True)) io) = io" by (induction io; auto) ultimately have "io ∈ LS I qI" using ts_assm by force then show "io ∈ set t ∩ LS I qI" using ‹io ∈ set t ∩ LS M qM› by blast qed show "set t ∩ LS I qI ⊆ set t ∩ LS M qM" proof fix io assume "io ∈ set t ∩ LS I qI" show "io ∈ set t ∩ LS M qM" proof (rule ccontr) assume "io ∉ set t ∩ LS M qM" then have "io ∈ LS I qI - LS M qM" using ‹io ∈ set t ∩ LS I qI› by blast then obtain io' xy io'' where "io = io' @ [xy] @ io''" and "io' ∈ LS I qI ∩ LS M qM" and "io' @ [xy] ∈ LS I qI - LS M qM" using minimal_failure_prefix_ob[OF assms] by blast have "io' ∈ set t ∩ LS M qM" using ‹io' ∈ LS I qI ∩ LS M qM› ‹io ∈ set t ∩ LS I qI› isin_prefix[of t io' "[xy] @ io''"] language_prefix[of io' "[xy] @ io''"] unfolding ‹io = io' @ [xy] @ io''› by auto moreover have "io' @ [xy] ∈ set t - LS M qM" using ‹io' @ [xy] ∈ LS I qI - LS M qM› ‹io ∈ set t ∩ LS I qI› isin_prefix[of t "io'@[xy]" io''] unfolding ‹io = io' @ [xy] @ io''› by auto ultimately have "io'@[xy] ∈ {xs @ [x] |xs x. xs ∈ set t ∩ LS M qM ∧ xs @ [x] ∈ set t - LS M qM}" by blast then have "(λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (io'@[xy]) ∈ set ts" unfolding ts_set by blast then have "(map (λx. (x, True)) io' @ [(xy, False)]) ∈ set ts" by auto moreover have "(map fst (map (λx. (x, True)) io' @ [(xy, False)]) ∈ LS I qI) ≠ list_all snd ((map (λx. (x, True)) io' @ [(xy, False)]))" proof - have "(map fst (map (λx. (x, True)) io' @ [(xy, False)])) = io'@[xy]" by (induction io'; auto) then show ?thesis using ‹io' @ [xy] ∈ set t - LS M qM› ‹io ∈ set t ∩ LS I qI› language_prefix[of "io'@[xy]" io'' I qI] unfolding ‹io = io' @ [xy] @ io''› by auto qed ultimately show "False" using ts_assm by blast qed qed qed qed show "set t ∩ LS M qM = Prefix_Tree.set t ∩ LS I qI ⟹ ∀iob∈set ts. (map fst iob ∈ LS I qI) = list_all snd iob" proof fix iob assume "set t ∩ LS M qM = set t ∩ LS I qI" and "iob ∈ set ts" then consider (a) "iob ∈ map (λx. (x, True)) ` (set t ∩ LS M qM)" | (b) "iob ∈ (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) ` {xs @ [x] |xs x. xs ∈ set t ∩ LS M qM ∧ xs @ [x] ∈ set t - LS M qM}" using ts_set by blast then show "(map fst iob ∈ LS I qI) = list_all snd iob" proof cases case a then obtain io where "iob = map (λx. (x, True)) io" and "io ∈ set t ∩ LS M qM" by blast then have "map fst iob = io" by auto then have "map fst iob ∈ LS I qI" using ‹io ∈ set t ∩ LS M qM› ‹set t ∩ LS M qM = set t ∩ LS I qI› by auto moreover have "list_all snd iob" unfolding ‹iob = map (λx. (x, True)) io› by (induction io; auto) ultimately show ?thesis by simp next case b then obtain ioxy where "iob = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (ioxy)" and "ioxy ∈ {xs @ [x] |xs x. xs ∈ set t ∩ LS M qM ∧ xs @ [x] ∈ set t - LS M qM}" by blast then obtain io xy where "ioxy = io@[xy]" and "io@[xy] ∈ set t - LS M qM" by blast then have *: "iob = map (λx. (x, True)) io @ [(xy, False)]" using ‹iob = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (ioxy)› by auto then have **: "map fst iob = io@[xy]" by (induction io arbitrary: iob; auto) have "¬map fst iob ∈ LS I qI" unfolding ** using ‹io@[xy] ∈ set t - LS M qM› ‹set t ∩ LS M qM = set t ∩ LS I qI› by blast moreover have "¬ list_all snd iob" unfolding * by auto ultimately show ?thesis by simp qed qed qed finally show ?thesis . qed subsection ‹Code Refinement› context includes lifting_syntax begin lemma map_entries_parametric: "((A ===> B) ===> (A ===> C ===> rel_option D) ===> (B ===> rel_option C) ===> A ===> rel_option D) (λf g m x. case (m ∘ f) x of None ⇒ None | Some y ⇒ g x y) (λf g m x. case (m ∘ f) x of None ⇒ None | Some y ⇒ g x y)" by transfer_prover end lift_definition map_entries :: "('c ⇒ 'a) ⇒ ('c ⇒ 'b ⇒ 'd option) ⇒ ('a, 'b) mapping ⇒ ('c, 'd) mapping" is "λf g m x. case (m ∘ f) x of None ⇒ None | Some y ⇒ g x y" parametric map_entries_parametric . lemma test_suite_from_io_tree_MPT[code] : "test_suite_from_io_tree M q (MPT m) = MPT (map_entries fst (λ ((x,y),b) t . (case h_obs M q x y of None ⇒ (if b then None else Some empty) | Some q' ⇒ (if b then Some (test_suite_from_io_tree M q' t) else None))) m)" (is "?t M q (MPT m) = MPT (?f M q m)") proof - have "⋀xyb . Mapping.lookup (?f M q m) xyb= (λ ((x,y),b) . case Mapping.lookup m (x,y) of None ⇒ None | Some t ⇒ (case h_obs M q x y of None ⇒ (if b then None else Some empty) | Some q' ⇒ (if b then Some (test_suite_from_io_tree M q' t) else None))) xyb" (is "⋀ xyb. ?f1 xyb = ?f2 xyb") proof - fix xyb show "?f1 xyb = ?f2 xyb" proof - obtain x y b where *:"xyb = ((x,y),b)" by (metis prod.collapse) show ?thesis proof (cases "Mapping.lookup m (fst xyb)") case None have "?f1 xyb = None" by (metis (no_types, lifting) None lookup.rep_eq map_entries.rep_eq option.simps(4)) moreover have "?f2 xyb = None" using None by (simp add: "*") ultimately show ?thesis by simp next case (Some t) then have **:"?f1 xyb = (λ ((x,y),b) t . (case h_obs M q x y of None ⇒ (if b then None else Some empty) | Some q' ⇒ (if b then Some (test_suite_from_io_tree M q' t) else None))) xyb t" by (simp add: lookup.rep_eq map_entries.rep_eq) show ?thesis unfolding ** using Some by (simp add: "*") qed qed qed then show ?thesis unfolding MPT_def by auto qed lemma passes_test_suite_MPT[code]: "passes_test_suite M q (MPT m) = (∀ xyb ∈ Mapping.keys m . case h_obs M q (fst (fst xyb)) (snd (fst xyb)) of None ⇒ ¬(snd xyb) | Some q' ⇒ snd xyb ∧ passes_test_suite M q' (case Mapping.lookup m xyb of Some t ⇒ t))" by (simp add: MPT_def keys_dom_lookup) subsection ‹Pass relations on list of lists representations of test suites› fun passes_test_case :: "('a,'b,'c) fsm ⇒ 'a ⇒ (('b × 'c) × bool) list ⇒ bool" where "passes_test_case M q [] = True" | "passes_test_case M q (((x,y),b)#io) = (if b then case h_obs M q x y of Some q' ⇒ passes_test_case M q' io | None ⇒ False else h_obs M q x y = None)" lemma passes_test_case_iff : assumes "observable M" and "q ∈ states M" shows "passes_test_case M q iob = ((map fst (takeWhile snd iob) ∈ LS M q) ∧ (¬ (list_all snd iob) ⟶ map fst (take (Suc (length (takeWhile snd iob))) iob) ∉ LS M q))" using assms(2) proof (induction iob arbitrary: q) case Nil then show ?case by auto next case (Cons a iob) obtain x y b where "a = ((x,y),b)" by (metis prod.collapse) show ?case proof (cases b) case True show ?thesis proof (cases "h_obs M q x y") case None then have "[(x,y)] ∉ LS M q" unfolding h_obs_None[OF assms(1)] LS_single_transition by force then have "(map fst (takeWhile snd (a#iob)) ∉ LS M q)" unfolding ‹a = ((x,y),b)› using True by (metis (mono_tags, opaque_lifting) append.simps(1) append.simps(2) fst_conv language_prefix list.simps(9) prod.sel(2) takeWhile.simps(2)) moreover have "passes_test_case M q (a#iob) = False" using None unfolding ‹a = ((x,y),b)› using True by auto ultimately show ?thesis by blast next case (Some q') then have "passes_test_case M q (a#iob) = passes_test_case M q' iob" unfolding ‹a = ((x,y),b)› using True by auto moreover have "(map fst (takeWhile snd (a#iob)) ∈ LS M q) = (map fst (takeWhile snd iob) ∈ LS M q')" proof - have *: "map fst (takeWhile snd (a#iob)) = (x,y)#(map fst (takeWhile snd iob))" using True unfolding ‹a = ((x,y),b)› by auto show ?thesis using Some unfolding * h_obs_Some[OF assms(1)] by (metis LS_prepend_transition assms(1) fst_conv mem_Collect_eq observable_language_transition_target singletonI snd_conv) qed moreover have "(¬ list_all snd (a#iob) ⟶ map fst (take (Suc (length (takeWhile snd (a#iob)))) (a#iob)) ∉ LS M q) = (¬ list_all snd iob ⟶ map fst (take (Suc (length (takeWhile snd iob))) iob) ∉ LS M q')" proof - have *: "map fst (take (Suc (length (takeWhile snd (a#iob)))) (a#iob)) = (x,y)#(map fst (take (Suc (length (takeWhile snd iob))) iob))" using True unfolding ‹a = ((x,y),b)› by auto have **: "list_all snd (a#iob) = list_all snd iob" using True unfolding ‹a = ((x,y),b)› by auto show ?thesis using Some unfolding * ** h_obs_Some[OF assms(1)] by (metis LS_prepend_transition assms(1) fst_conv mem_Collect_eq observable_language_transition_target prod.sel(2) singletonI) qed ultimately show ?thesis unfolding Cons.IH[OF h_obs_state[OF Some]] by simp qed next case False show ?thesis proof (cases "h_obs M q x y") case None then have "[(x,y)] ∉ LS M q" unfolding h_obs_None[OF assms(1)] LS_single_transition by force then have "(¬ list_all snd (a#iob) ⟶ map fst (take (Suc (length (takeWhile snd (a#iob)))) (a#iob)) ∉ LS M q)" unfolding ‹a = ((x,y),b)› using False by auto moreover have "(map fst (takeWhile snd (a#iob)) ∈ LS M q)" unfolding ‹a = ((x,y),b)› using False Cons.prems by auto moreover have "passes_test_case M q (a#iob) = True" unfolding ‹a = ((x,y),b)› using False None by auto ultimately show ?thesis by simp next case (Some q') then have "[(x,y)] ∈ LS M q" unfolding h_obs_Some[OF assms(1)] LS_single_transition by force then have "¬ (¬ list_all snd (a#iob) ⟶ map fst (take (Suc (length (takeWhile snd (a#iob)))) (a#iob)) ∉ LS M q)" unfolding ‹a = ((x,y),b)› using False by auto moreover have "passes_test_case M q (a#iob) = False" unfolding ‹a = ((x,y),b)› using False Some by auto ultimately show ?thesis by simp qed qed qed lemma test_suite_from_io_tree_finite_tree : assumes "observable M" and "qM ∈ states M" and "finite_tree t" shows "finite_tree (test_suite_from_io_tree M qM t)" proof - have "finite (Prefix_Tree.set t ∩ LS M qM)" using assms(3) unfolding finite_tree_iff by blast then have "finite (map (λx. (x, True)) ` (set t ∩ LS M qM))" by blast have "((λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) ` {xs @ [x] |xs x. xs ∈ set t ∩ LS M qM ∧ xs @ [x] ∈ set t - LS M qM}) ⊆ ((λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) ` (set t))" by blast moreover have "finite ((λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) ` (set t))" using assms(3) unfolding finite_tree_iff by blast ultimately have "finite ((λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) ` {xs @ [x] |xs x. xs ∈ set t ∩ LS M qM ∧ xs @ [x] ∈ set t - LS M qM})" using finite_subset by blast then show ?thesis using ‹finite (map (λx. (x, True)) ` (set t ∩ LS M qM))› unfolding finite_tree_iff test_suite_from_io_tree_set[OF assms(1,2)] by blast qed lemma passes_test_case_prefix : assumes "observable M" and "passes_test_case M q (iob@iob')" shows "passes_test_case M q iob" using assms(2) proof (induction iob arbitrary: q) case Nil then show ?case by auto next case (Cons a iob) obtain x y b where "a = ((x,y),b)" by (metis prod.collapse) show ?case proof (cases b) case False then show ?thesis using Cons.prems unfolding ‹a = ((x,y),b)› by auto next case True show ?thesis proof (cases "h_obs M q x y") case None then show ?thesis using Cons.prems unfolding ‹a = ((x,y),b)› by auto next case (Some q') then have "passes_test_case M q' (iob @ iob')" using True Cons.prems unfolding ‹a = ((x,y),b)› by auto then have "passes_test_case M q' iob" using Cons.IH by auto then show ?thesis using True Some unfolding ‹a = ((x,y),b)› by auto qed qed qed lemma passes_test_cases_of_test_suite : assumes "observable M" and "observable I" and "qM ∈ states M" and "qI ∈ states I" and "finite_tree t" shows "list_all (passes_test_case I qI) (sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M qM t)) = passes_test_suite I qI (test_suite_from_io_tree M qM t)" (is "?P1 = ?P2") proof have "list.set (sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M qM t)) = {y ∈ Prefix_Tree.set (test_suite_from_io_tree M qM t). ∄y'. y' ≠ [] ∧ y @ y' ∈ Prefix_Tree.set (test_suite_from_io_tree M qM t)}" using sorted_list_of_maximal_sequences_in_tree_set[OF test_suite_from_io_tree_finite_tree[OF assms(1,3,5)]] . show "?P1 ⟹ ?P2" proof - assume ?P1 show ?P2 unfolding passes_test_suite_iff[OF assms(2,4)] proof fix iob assume "iob ∈ Prefix_Tree.set (test_suite_from_io_tree M qM t)" then obtain iob' where "iob@iob' ∈ list.set (sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M qM t))" unfolding sorted_list_of_maximal_sequences_in_tree_set[OF test_suite_from_io_tree_finite_tree[OF assms(1,3,5)]] using test_suite_from_io_tree_finite_tree[OF assms(1,3,5)] unfolding finite_tree_iff using prefix_free_set_maximal_list_ob[of "set (test_suite_from_io_tree M qM t)"] by blast then have "passes_test_case I qI (iob@iob')" using ‹?P1› by (metis in_set_conv_decomp_last list_all_append list_all_simps(1)) then have "passes_test_case I qI iob" using passes_test_case_prefix[OF assms(2)] by auto then have "map fst (takeWhile snd iob) ∈ LS I qI" and "(¬ list_all snd iob ⟶ map fst (take (Suc (length (takeWhile snd iob))) iob) ∉ LS I qI)" unfolding passes_test_case_iff[OF assms(2,4)] by auto have "list_all snd iob ⟹ (map fst iob ∈ LS I qI)" using ‹map fst (takeWhile snd iob) ∈ LS I qI› by (metis in_set_conv_decomp_last list_all_append list_all_simps(1) takeWhile_eq_all_conv) moreover have "(map fst iob ∈ LS I qI) ⟹ list_all snd iob" using ‹(¬ list_all snd iob ⟶ map fst (take (Suc (length (takeWhile snd iob))) iob) ∉ LS I qI)› by (metis append_take_drop_id language_prefix map_append) ultimately show "(map fst iob ∈ LS I qI) = list_all snd iob" by blast qed qed show "?P2 ⟹ ?P1" proof - assume ?P2 have "⋀ iob . iob ∈ list.set (sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M qM t)) ⟹ passes_test_case I qI iob" proof - fix iob assume "iob ∈ list.set (sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M qM t))" then have "iob ∈ set (test_suite_from_io_tree M qM t)" unfolding sorted_list_of_maximal_sequences_in_tree_set[OF test_suite_from_io_tree_finite_tree[OF assms(1,3,5)]] by blast then have *: "(map fst iob ∈ LS I qI) = list_all snd iob" using ‹?P2› unfolding passes_test_suite_iff[OF assms(2,4)] by blast consider "iob ∈ map (λx. (x, True)) ` (Prefix_Tree.set t ∩ LS M qM)" | "iob ∈ (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) ` {xs @ [x] |xs x. xs ∈ Prefix_Tree.set t ∩ LS M qM ∧ xs @ [x] ∈ Prefix_Tree.set t - LS M qM}" using ‹iob ∈ set (test_suite_from_io_tree M qM t)› unfolding test_suite_from_io_tree_set[OF assms(1,3)] by blast then show "passes_test_case I qI iob" proof cases case 1 then obtain io where "iob = map (λx. (x, True)) io" by blast have "list_all snd iob" unfolding ‹iob = map (λx. (x, True)) io› by (induction io; auto) then have "(takeWhile snd iob) = iob" by (induction iob; auto) have "map fst (takeWhile snd iob) ∈ LS I qI" using * ‹list_all snd iob› by (simp add: ‹takeWhile snd iob = iob›) then show ?thesis unfolding passes_test_case_iff[OF assms(2,4)] using ‹list_all snd iob› by auto next case 2 then obtain xs x where "iob = (λxs. map (λx. (x, True)) (butlast xs) @ [(last xs, False)]) (xs@[x])" and "xs ∈ set t ∩ LS M qM" and "xs @ [x] ∈ Prefix_Tree.set t - LS M qM" by blast then have **: "iob = (map (λx. (x, True)) xs) @ [(x,False)]" by auto have "isin (test_suite_from_io_tree M qM t) ((takeWhile snd iob)@(dropWhile snd iob))" using ‹iob ∈ set (test_suite_from_io_tree M qM t)› by auto then have "(takeWhile snd iob) ∈ set (test_suite_from_io_tree M qM t)" using isin_prefix[of "test_suite_from_io_tree M qM t" "takeWhile snd iob" "dropWhile snd iob"] by simp then have "(map fst (takeWhile snd iob) ∈ LS I qI) = list_all snd (takeWhile snd iob)" using ‹?P2› unfolding passes_test_suite_iff[OF assms(2,4)] by blast moreover have "list_all snd (takeWhile snd iob)" by (induction iob; auto) ultimately have "map fst (takeWhile snd iob) ∈ LS I qI" by simp have "¬ list_all snd iob" using ** by auto moreover have "(take (Suc (length (takeWhile snd iob))) iob) = iob" unfolding ‹iob = (map (λx. (x, True)) xs) @ [(x,False)]› by (induction xs; auto) ultimately have "map fst (take (Suc (length (takeWhile snd iob))) iob) ∉ LS I qI" using * by simp then show ?thesis using ‹map fst (takeWhile snd iob) ∈ LS I qI› unfolding passes_test_case_iff[OF assms(2,4)] by simp qed qed then show ?P1 using Ball_set_list_all by blast qed qed lemma passes_test_cases_from_io_tree : assumes "observable M" and "observable I" and "qM ∈ states M" and "qI ∈ states I" and "finite_tree t" shows "list_all (passes_test_case I qI) (sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M qM t)) = ((set t ∩ LS M qM) = (set t ∩ LS I qI))" unfolding passes_test_cases_of_test_suite[OF assms] passes_test_suite_from_io_tree[OF assms(1-4)] by blast subsection ‹Alternative Representations› subsubsection ‹Pass and Fail Traces› type_synonym ('b,'c) pass_traces = "('b × 'c) list list" type_synonym ('b,'c) fail_traces = "('b × 'c) list list" type_synonym ('b,'c) trace_test_suite = "('b,'c) pass_traces × ('b,'c) fail_traces" fun trace_test_suite_from_tree :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ ('b × 'c) prefix_tree ⇒ ('b,'c) trace_test_suite" where "trace_test_suite_from_tree M T = (let (passes',fails) = separate_by (is_in_language M (initial M)) (sorted_list_of_sequences_in_tree T); passes = sorted_list_of_maximal_sequences_in_tree (from_list passes') in (passes, fails))" lemma trace_test_suite_from_tree_language_equivalence : assumes "observable M" and "finite_tree T" shows "(L M ∩ set T = L M' ∩ set T) = (list.set (fst (trace_test_suite_from_tree M T)) ⊆ L M' ∧ L M' ∩ list.set (snd (trace_test_suite_from_tree M T)) = {})" proof - obtain passes' fails where *: "(passes',fails) = separate_by (is_in_language M (initial M)) (sorted_list_of_sequences_in_tree T)" by auto define passes where "passes = sorted_list_of_maximal_sequences_in_tree (from_list passes')" have "fst (trace_test_suite_from_tree M T) = passes" using "*" passes_def by auto have "snd (trace_test_suite_from_tree M T) = fails" using "*" passes_def by auto have "list.set passes' = L M ∩ set T" using * sorted_list_of_sequences_in_tree_set[OF assms(2)] unfolding separate_by.simps unfolding is_in_language_iff[OF assms(1) fsm_initial] by (metis inter_set_filter old.prod.inject) moreover have "list.set passes' ⊆ L M' = (list.set passes ⊆ L M')" proof - have "⋀ io . io ∈ list.set passes - {[]} ⟹ ∃ io' . io@io' ∈ list.set passes'" unfolding passes_def unfolding sorted_list_of_maximal_sequences_in_tree_set[OF from_list_finite_tree] unfolding from_list_set by force moreover have "[] ∈ list.set passes'" unfolding ‹list.set passes' = L M ∩ set T› by auto ultimately have "⋀ io . io ∈ list.set passes ⟹ ∃ io' . io@io' ∈ list.set passes'" by force moreover have "⋀ io . io ∈ list.set passes' ⟹ ∃ io' . io@io' ∈ list.set passes" proof - have "⋀ io . io ∈ list.set passes' ⟹ io ∈ set (from_list passes')" unfolding from_list_set by auto moreover have "⋀ io. io ∈ set (from_list passes') ⟹ ∃ io' . io@io' ∈ list.set passes" unfolding passes_def unfolding sorted_list_of_maximal_sequences_in_tree_set[OF from_list_finite_tree] using from_list_finite_tree sorted_list_of_maximal_sequences_in_tree_ob sorted_list_of_maximal_sequences_in_tree_set by fastforce ultimately show "⋀ io . io ∈ list.set passes' ⟹ ∃ io' . io@io' ∈ list.set passes" by blast qed ultimately show ?thesis using language_prefix[of _ _ M' "initial M'"] by (meson subset_iff) qed moreover have "list.set fails = set T - L M" using * sorted_list_of_sequences_in_tree_set[OF assms(2)] unfolding separate_by.simps unfolding is_in_language_iff[OF assms(1) fsm_initial] by (simp add: set_diff_eq) ultimately show ?thesis unfolding ‹fst (trace_test_suite_from_tree M T) = passes› unfolding ‹snd (trace_test_suite_from_tree M T) = fails› by blast qed subsubsection ‹Input Sequences› fun test_suite_to_input_sequences :: "('b::linorder×'c::linorder) prefix_tree ⇒ 'b list list" where "test_suite_to_input_sequences T = sorted_list_of_maximal_sequences_in_tree (from_list (map input_portion (sorted_list_of_maximal_sequences_in_tree T)))" lemma test_suite_to_input_sequences_pass : fixes T :: "('b::linorder × 'c::linorder) prefix_tree" assumes "finite_tree T" and "(L M = L M') ⟷ (L M ∩ set T = L M' ∩ set T)" shows "(L M = L M') ⟷ ({io ∈ L M . (∃ xs ∈ list.set (test_suite_to_input_sequences T) . ∃ xs' ∈ list.set (prefixes xs) . input_portion io = xs')} = {io ∈ L M' . (∃ xs ∈ list.set (test_suite_to_input_sequences T) . ∃ xs' ∈ list.set (prefixes xs) . input_portion io = xs')})" proof - have *: "⋀ io :: ('b::linorder × 'c::linorder) list . (∃ xs ∈ list.set (test_suite_to_input_sequences T) . ∃ xs' ∈ list.set (prefixes xs) . input_portion io = xs') = (∃io'∈set T. map fst io = map fst io')" proof - fix io :: "('b::linorder × 'c::linorder) list" have "(∃io'∈set T. map fst io = map fst io') = (∃ α ∈ list.set (sorted_list_of_maximal_sequences_in_tree T) . ∃ α' ∈ list.set (prefixes α) . map fst io = map fst α')" proof have *: "⋀ io' . io'∈set T ⟷ (∃ io''. io'@io'' ∈ list.set (sorted_list_of_maximal_sequences_in_tree T))" using sorted_list_of_maximal_sequences_in_tree_set[OF assms(1)] using assms(1) set_prefix sorted_list_of_maximal_sequences_in_tree_ob by fastforce show "(∃io'∈set T. map fst io = map fst io') ⟹ (∃ α ∈ list.set (sorted_list_of_maximal_sequences_in_tree T) . ∃ α' ∈ list.set (prefixes α) . map fst io = map fst α')" by (metis append_Nil2 assms(1) prefixes_prepend prefixes_set_Nil sorted_list_of_maximal_sequences_in_tree_ob) show "∃α∈list.set (sorted_list_of_maximal_sequences_in_tree T). ∃α'∈list.set (prefixes α). map fst io = map fst α' ⟹ ∃io'∈Prefix_Tree.set T. map fst io = map fst io'" by (metis "*" prefixes_set_ob) qed also have "… = (∃ xs ∈ list.set (map input_portion (sorted_list_of_maximal_sequences_in_tree T)) . ∃ xs' ∈ list.set (prefixes xs) . map fst io = xs')" proof - have *: "list.set (map input_portion (sorted_list_of_maximal_sequences_in_tree T)) = input_portion ` (list.set (sorted_list_of_maximal_sequences_in_tree T))" by auto have **: "⋀ (α :: ('b::linorder × 'c::linorder) list) . (∃ α' ∈ list.set (prefixes α) . map fst io = map fst α') = (∃ xs' ∈ list.set (prefixes (input_portion α)) . map fst io = xs')" proof fix α :: "('b::linorder × 'c::linorder) list" show "∃α'∈list.set (prefixes α). map fst io = map fst α' ⟹ ∃xs'∈list.set (prefixes (map fst α)). map fst io = xs'" proof - assume "∃α'∈list.set (prefixes α). map fst io = map fst α'" then obtain α' α'' where "α'@α'' = α" and "map fst io = map fst α'" unfolding prefixes_set by blast then show "∃xs'∈list.set (prefixes (map fst α)). map fst io = xs'" unfolding prefixes_set by auto qed show "∃xs'∈list.set (prefixes (map fst α)). map fst io = xs' ⟹ ∃α'∈list.set (prefixes α). map fst io = map fst α'" proof - assume "∃xs'∈list.set (prefixes (map fst α)). map fst io = xs'" then obtain xs' xs'' where "xs'@xs'' = (map fst α)" and "map fst io = xs'" unfolding prefixes_set by blast then have "map fst (take (length xs') α) = map fst io" by (metis ‹∃xs'∈list.set (prefixes (map fst α)). map fst io = xs'› prefixes_take_iff take_map) moreover have "(take (length xs') α) ∈ list.set (prefixes α)" by (metis ‹map fst io = xs'› calculation length_map prefixes_take_iff) ultimately show ?thesis by metis qed qed show ?thesis unfolding ** * by blast qed also have "… = (∃ xs ∈ list.set (test_suite_to_input_sequences T) . ∃ xs' ∈ list.set (prefixes xs) . input_portion io = xs')" proof show "∃xs∈list.set (map (map fst) (sorted_list_of_maximal_sequences_in_tree T)). ∃xs'∈list.set (prefixes xs). map fst io = xs' ⟹ ∃xs∈list.set (test_suite_to_input_sequences T). ∃xs'∈list.set (prefixes xs). map fst io = xs'" proof - assume "∃xs∈list.set (map (map fst) (sorted_list_of_maximal_sequences_in_tree T)). ∃xs'∈list.set (prefixes xs). map fst io = xs'" then obtain xs' xs'' where "xs'@xs'' ∈ list.set (map (map fst) (sorted_list_of_maximal_sequences_in_tree T))" and "map fst io = xs'" unfolding prefixes_set by blast then have *:"xs'@xs'' ∈ set (from_list (map (map fst) (sorted_list_of_maximal_sequences_in_tree T)))" unfolding from_list_set by blast show ?thesis using sorted_list_of_maximal_sequences_in_tree_ob[OF from_list_finite_tree *] ‹map fst io = xs'› unfolding test_suite_to_input_sequences.simps by (metis append.assoc append_Nil2 prefixes_prepend prefixes_set_Nil) qed show "∃xs∈list.set (test_suite_to_input_sequences T). ∃xs'∈list.set (prefixes xs). map fst io = xs' ⟹ ∃xs∈list.set (map (map fst) (sorted_list_of_maximal_sequences_in_tree T)). ∃xs'∈list.set (prefixes xs). map fst io = xs'" proof - assume "∃xs∈list.set (test_suite_to_input_sequences T). ∃xs'∈list.set (prefixes xs). map fst io = xs'" then obtain xs' xs'' where "xs'@xs'' ∈ list.set (test_suite_to_input_sequences T)" and "map fst io = xs'" unfolding prefixes_set by blast then have "xs'@xs'' = [] ∨ (∃ xs''' . (xs'@xs'')@xs'''∈list.set (map (map fst) (sorted_list_of_maximal_sequences_in_tree T)))" unfolding test_suite_to_input_sequences.simps unfolding sorted_list_of_maximal_sequences_in_tree_set[OF from_list_finite_tree] unfolding from_list_set by blast then obtain xs''' where "(xs'@xs'')@xs'''∈list.set (map (map fst) (sorted_list_of_maximal_sequences_in_tree T))" by (metis Nil_is_append_conv ‹map fst io = xs'› append.left_neutral calculation list.simps(8) set_Nil) then show ?thesis using ‹map fst io = xs'› by (metis append.assoc append.right_neutral prefixes_prepend prefixes_set_Nil) qed qed finally show "(∃ xs ∈ list.set (test_suite_to_input_sequences T) . ∃ xs' ∈ list.set (prefixes xs) . input_portion io = xs') = (∃io'∈set T. map fst io = map fst io')" by presburger qed show ?thesis unfolding * using equivalence_io_relaxation[OF assms(2)] . qed lemma test_suite_to_input_sequences_pass_alt_def : fixes T :: "('b::linorder × 'c::linorder) prefix_tree" assumes "finite_tree T" and "(L M = L M') ⟷ (L M ∩ set T = L M' ∩ set T)" shows "(L M = L M') ⟷ (∀ xs ∈ list.set (test_suite_to_input_sequences T) . ∀ xs' ∈ list.set (prefixes xs) . {io ∈ L M . input_portion io = xs'} = {io ∈ L M' . input_portion io = xs'})" unfolding test_suite_to_input_sequences_pass[OF assms] by blast end