Theory Wp_Method_Implementations

section ‹Implementations of the Wp-Method›

theory Wp_Method_Implementations
imports Intermediate_Frameworks Pair_Framework "../Distinguishability" Test_Suite_Representations "../OFSM_Tables_Refined" "HOL-Library.List_Lexorder"
begin

subsection ‹Distinguishing Sets›

fun add_distinguishing_set_or_state_identifier :: "nat ⇒ ('a :: linorder, 'b :: linorder, 'c :: linorder) fsm ⇒ (('b × 'c) list × 'a) × ('b × 'c) list × 'a ⇒ ('b × 'c) prefix_tree ⇒ ('b×'c) prefix_tree" where
  "add_distinguishing_set_or_state_identifier k M ((io1,q1),(io2,q2)) t = (if length io1 = k ∨ length io2 = k
    then insert empty (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
    else distinguishing_set M)"

lemma add_distinguishing_set_or_state_identifier_distinguishes :
  assumes "observable M"
  and     "minimal M"
  and     "α ∈ L M"
  and     "β ∈ L M" 
  and     "after_initial M α ≠ after_initial M β"   
shows "∃ io ∈ set (add_distinguishing_set_or_state_identifier k M ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β)) . distinguishes M (after_initial M α) (after_initial M β) io"
proof (cases "length α = k ∨ length β = k")
  case False
  then show ?thesis 
    using distinguishing_set_distinguishes[OF assms(1,2) after_is_state[OF assms(1,3)] after_is_state[OF assms(1,4)] assms(5)]
    by auto
next
  case True
  then have "set ((add_distinguishing_set_or_state_identifier k) M ((α,after_initial M α),(β,after_initial M β)) t) = set (insert empty (get_distinguishing_sequence_from_ofsm_tables M (after_initial M α) (after_initial M β)))"
    by auto
  then have "get_distinguishing_sequence_from_ofsm_tables M (after_initial M α) (after_initial M β) ∈ set ((add_distinguishing_set_or_state_identifier k) M ((α,after_initial M α),(β,after_initial M β)) t) ∪ (set (after t α) ∩ set (after t β))"
    unfolding insert_set by auto
  then show ?thesis
    by (meson after_is_state assms(1) assms(2) assms(3) assms(4) assms(5) get_distinguishing_sequence_from_ofsm_tables_distinguishes) 
qed


lemma add_distinguishing_set_or_state_identifier_finite : 
  "finite_tree ((add_distinguishing_set_or_state_identifier k) M ((α,after_initial M α),(β,after_initial M β)) t)"
proof (cases "length α = k ∨ length β = k")
  case False
  then show ?thesis 
    unfolding add_distinguishing_set.simps distinguishing_set.simps Let_def
    using from_list_finite_tree
    by simp
next
  case True
  then have "((add_distinguishing_set_or_state_identifier k) M ((α,after_initial M α),(β,after_initial M β)) t) = (insert empty (get_distinguishing_sequence_from_ofsm_tables M (after_initial M α) (after_initial M β)))"
    by auto
  then show ?thesis
    using insert_finite_tree[OF empty_finite_tree] by metis
qed  



fun distinguishing_set_or_state_identifier :: "nat ⇒ ('a :: linorder, 'b :: linorder, 'c :: linorder) fsm ⇒ nat ⇒ 'a ⇒ ('b×'c) prefix_tree" where
  "distinguishing_set_or_state_identifier l M k q = (if k = l 
    then get_HSI M q
    else distinguishing_set M)"

lemma get_HSI_subset :
  assumes "observable M"
  and     "minimal M"
  and     "q ∈ states M"
shows "set (get_HSI M q) ⊆ set (distinguishing_set M)"
proof 
  fix io assume "io ∈ set (get_HSI M q)"

  show "io ∈ set (distinguishing_set M)"
  proof (cases "io = []")
    case True
    then show ?thesis by auto
  next
    case False

    then obtain io' where *:"io@io' ∈ list.set (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((≠) q) (states_as_list M)))"
      using ‹io ∈ set (get_HSI M q)›
      unfolding get_HSI.simps from_list_set
      by blast
    obtain q' where "q ≠ q'" and "q' ∈ states M" and "io@io' = get_distinguishing_sequence_from_ofsm_tables M q q'"
      using states_as_list_set[of M] filter_map_elem[OF *]
      by blast

    have "(q,q') ∈ list.set (filter (λ (x,y) . x ≠ y) (list_ordered_pairs (states_as_list M)))
            ∨ (q',q) ∈ list.set (filter (λ (x,y) . x ≠ y) (list_ordered_pairs (states_as_list M)))"
      using list_ordered_pairs_set_containment[of q "states_as_list M" q'] ‹q ∈ states M› ‹q' ∈ states M› ‹q ≠ q'›
      unfolding states_as_list_set
      by force
    moreover define pairs where pairs: "pairs = filter (λ (x,y) . x ≠ y) (list_ordered_pairs (states_as_list M))"
    ultimately have "(q,q') ∈ list.set pairs ∨ (q',q) ∈ list.set pairs"
      by auto      
    then have "get_distinguishing_sequence_from_ofsm_tables M q q' ∈ list.set (map (case_prod (get_distinguishing_sequence_from_ofsm_tables M)) pairs)"
      using get_distinguishing_sequence_from_ofsm_tables_sym[OF assms ‹q' ∈ states M› ‹q ≠ q'›, symmetric]
      by (metis case_prod_conv map_set)
    then have "io@io' ∈ set (distinguishing_set M)"
      unfolding ‹io@io' = get_distinguishing_sequence_from_ofsm_tables M q q'› distinguishing_set.simps Let_def pairs
      using from_list_set_elem
      by blast
    then show ?thesis 
      using set_prefix by metis
  qed
qed

lemma distinguishing_set_or_state_identifier_distinguishes :
  assumes "observable M"
  and     "minimal M"
  and     "q1 ∈ states M" and "q2 ∈ states M" and "q1 ≠ q2"
shows "∃ io . ∀ k1 k2 . io ∈ set (distinguishing_set_or_state_identifier l M k1 q1) ∩ set (distinguishing_set_or_state_identifier l M k2 q2) ∧ distinguishes M q1 q2 io"
  using get_HSI_distinguishes[OF assms]
  using distinguishing_set_distinguishes[OF assms]
  using get_HSI_subset[OF assms(1,2,3)]
  using get_HSI_subset[OF assms(1,2,4)]
  unfolding distinguishing_set_or_state_identifier.simps
  by auto

lemma distinguishing_set_or_state_identifier_finite :
  "finite_tree (distinguishing_set_or_state_identifier l M k q)"
  using get_HSI_finite[of M q]
  using distinguishing_set_finite[of M]
  unfolding distinguishing_set_or_state_identifier.simps 
  by (cases "k = l"; force)



subsection ‹Using the H-Framework›

definition wp_method_via_h_framework :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ ('b×'c) prefix_tree" where
  "wp_method_via_h_framework M m = h_framework_static_with_empty_graph M (distinguishing_set_or_state_identifier (Suc (m - size_r M)) M) m"

definition wp_method_via_h_framework_lists :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ (('b×'c) × bool) list list" where
  "wp_method_via_h_framework_lists M m = sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M (initial M) (wp_method_via_h_framework M m))"

lemma wp_method_via_h_framework_completeness_and_finiteness :
  fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
  fixes M2 :: "('e,'b,'c) fsm"
  assumes "observable M1"
  and     "observable M2"
  and     "minimal M1"
  and     "minimal M2"
  and     "size_r M1 ≤ m"
  and     "size M2 ≤ m"
  and     "inputs M2 = inputs M1"
  and     "outputs M2 = outputs M1"
shows "(L M1 = L M2) ⟷ ((L M1 ∩ set (wp_method_via_h_framework M1 m)) = (L M2 ∩ set (wp_method_via_h_framework M1 m)))"
and "finite_tree (wp_method_via_h_framework M1 m)"
  using h_framework_static_with_empty_graph_completeness_and_finiteness[OF assms, where dist_fun="distinguishing_set_or_state_identifier (Suc (m - size_r M1)) M1"]
  using distinguishing_set_or_state_identifier_distinguishes[OF assms(1,3)]
  using distinguishing_set_or_state_identifier_finite 
  unfolding wp_method_via_h_framework_def 
  by blast+

lemma wp_method_via_h_framework_lists_completeness :
  fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
  fixes M2 :: "('d,'b,'c) fsm"
  assumes "observable M1"
  and     "observable M2"
  and     "minimal M1"
  and     "minimal M2"
  and     "size_r M1 ≤ m"
  and     "size M2 ≤ m"
  and     "inputs M2 = inputs M1"
  and     "outputs M2 = outputs M1"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (initial M2)) (wp_method_via_h_framework_lists M1 m)"
  using h_framework_static_with_empty_graph_lists_completeness[OF assms, where dist_fun="distinguishing_set_or_state_identifier (Suc (m - size_r M1)) M1", OF _ distinguishing_set_or_state_identifier_finite]
  using distinguishing_set_or_state_identifier_distinguishes[OF assms(1,3)] 
  unfolding wp_method_via_h_framework_lists_def h_framework_static_with_empty_graph_lists_def wp_method_via_h_framework_def 
  by blast


subsection ‹Using the SPY-Framework›

definition wp_method_via_spy_framework :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ ('b×'c) prefix_tree" where
  "wp_method_via_spy_framework M m = spy_framework_static_with_empty_graph M (distinguishing_set_or_state_identifier (Suc (m - size_r M)) M) m"

lemma wp_method_via_spy_framework_completeness_and_finiteness :
  fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
  fixes M2 :: "('d,'b,'c) fsm"
  assumes "observable M1"
  and     "observable M2"
  and     "minimal M1"
  and     "minimal M2"
  and     "size_r M1 ≤ m"
  and     "size M2 ≤ m"
  and     "inputs M2 = inputs M1"
  and     "outputs M2 = outputs M1"
shows "(L M1 = L M2) ⟷ ((L M1 ∩ set (wp_method_via_spy_framework M1 m)) = (L M2 ∩ set (wp_method_via_spy_framework M1 m)))"
and "finite_tree (wp_method_via_spy_framework M1 m)"  
  unfolding wp_method_via_spy_framework_def
  using spy_framework_static_with_empty_graph_completeness_and_finiteness[OF assms, of "distinguishing_set_or_state_identifier (Suc (m - size_r M1)) M1"]
  using distinguishing_set_or_state_identifier_distinguishes[OF assms(1,3)]
  using distinguishing_set_or_state_identifier_finite
  by metis+

definition wp_method_via_spy_framework_lists :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ nat ⇒ (('b×'c) × bool) list list" where
  "wp_method_via_spy_framework_lists M m = sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M (initial M) (wp_method_via_spy_framework M m))"

lemma wp_method_via_spy_framework_lists_completeness :
  fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
  fixes M2 :: "('d,'b,'c) fsm"
  assumes "observable M1"
  and     "observable M2"
  and     "minimal M1"
  and     "minimal M2"
  and     "size_r M1 ≤ m"
  and     "size M2 ≤ m"
  and     "inputs M2 = inputs M1"
  and     "outputs M2 = outputs M1"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (initial M2)) (wp_method_via_spy_framework_lists M1 m)"
  unfolding wp_method_via_spy_framework_lists_def
            wp_method_via_spy_framework_completeness_and_finiteness(1)[OF assms]
            passes_test_cases_from_io_tree[OF assms(1,2) fsm_initial fsm_initial wp_method_via_spy_framework_completeness_and_finiteness(2)[OF assms]]
  by blast


subsection ‹Code Generation›

lemma wp_method_via_spy_framework_code[code] :
  "wp_method_via_spy_framework M m = (let 
      tables = (compute_ofsm_tables M (size M - 1));
      distMap = mapping_of (map (λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2))
                        (filter (λ qq . fst qq ≠ snd qq) (List.product (states_as_list M) (states_as_list M))));
      distHelper = (λ q1 q2 . if q1 ∈ states M ∧ q2 ∈ states M ∧ q1 ≠ q2 then the (Mapping.lookup distMap (q1,q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2);
      pairs = filter (λ (x,y) . x ≠ y) (list_ordered_pairs (states_as_list M));
      distSet = from_list (map (case_prod distHelper) pairs);
      hsiMap = mapping_of (map (λ q . (q,from_list (map (λq' . distHelper q q') (filter ((≠) q) (states_as_list M))))) (states_as_list M));
      l = (Suc (m - size_r M));
      distFun = (λ k q . if k = l 
                      then (if q ∈ states M then the (Mapping.lookup hsiMap q) else get_HSI M q)
                      else distSet)
    in spy_framework_static_with_empty_graph M distFun m)"   
(is "?f1 = ?f2") 
proof -
  define hsiMap' where "hsiMap' = mapping_of (map (λ q . (q,from_list (map (λq' . get_distinguishing_sequence_from_ofsm_tables M q q') (filter ((≠) q) (states_as_list M))))) (states_as_list M))"
  define distFun' where "distFun' = (λ k q . if k = (Suc (m - size_r M))
                      then (if q ∈ states M then the (Mapping.lookup hsiMap' q) else get_HSI M q)
                      else distinguishing_set M)"
  have *: "?f2 = spy_framework_static_with_empty_graph M distFun' m"
    unfolding distFun'_def hsiMap'_def distinguishing_set.simps Let_def
    apply (subst (3 4 ) get_distinguishing_sequence_from_ofsm_tables_precomputed[of M])
    unfolding Let_def  
    by presburger

  define hsiMap where "hsiMap = map_of (map (λ q . (q,from_list (map (λq' . get_distinguishing_sequence_from_ofsm_tables M q q') (filter ((≠) q) (states_as_list M))))) (states_as_list M))"
  define distFun where "distFun = (λ k q . if k = (Suc (m - size_r M))
                      then (if q ∈ states M then the (hsiMap q) else get_HSI M q)
                      else distinguishing_set M)"

  have "distinct (map fst (map (λ q . (q,from_list (map (λq' . get_distinguishing_sequence_from_ofsm_tables M q q') (filter ((≠) q) (states_as_list M))))) (states_as_list M)))"
    using states_as_list_distinct
    by (metis map_pair_fst) 
  then have "Mapping.lookup hsiMap' = hsiMap"
    unfolding hsiMap_def hsiMap'_def  
    using mapping_of_map_of
    by blast
  then have "distFun' = distFun"
    unfolding distFun_def distFun'_def by meson

  have **:"distFun' = (distinguishing_set_or_state_identifier (Suc (m - size_r M)) M)" 
  proof     
    fix k show "distFun' k = (distinguishing_set_or_state_identifier (Suc (m - size_r M)) M) k"
    proof (cases "k = (Suc (m - size_r M))")
      case False
      then show ?thesis 
        unfolding distFun_def distinguishing_set_or_state_identifier.simps ‹distFun' = distFun› by auto
    next
      case True
      then have "distFun k = (λ q . (if q ∈ states M then the (hsiMap q) else get_HSI M q))"
            and "(distinguishing_set_or_state_identifier (Suc (m - size_r M)) M) k = (λ q . get_HSI M q)"
        unfolding distFun_def distinguishing_set_or_state_identifier.simps by auto
      moreover have "(λ q . (if q ∈ states M then the (hsiMap q) else get_HSI M q)) = (λ q . get_HSI M q)"
      proof 
        fix q show "(if q ∈ states M then the (hsiMap q) else get_HSI M q) = get_HSI M q"
        proof (cases "q ∈ states M")
          case True
          then have "q ∈ list.set (states_as_list M)"
            using states_as_list_set by blast
          then show ?thesis
            unfolding distFun_def hsiMap_def map_of_map_pair_entry get_HSI.simps
            using True
            by fastforce
        next
          case False
          then show ?thesis using distFun_def by auto
        qed
      qed
      ultimately show ?thesis unfolding ‹distFun' = distFun› by simp
    qed
  qed
  
  show ?thesis
    unfolding * ** wp_method_via_spy_framework_def by simp
qed

lemma wp_method_via_h_framework_code[code] :
  "wp_method_via_h_framework M m = (let 
      tables = (compute_ofsm_tables M (size M - 1));
      distMap = mapping_of (map (λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2))
                        (filter (λ qq . fst qq ≠ snd qq) (List.product (states_as_list M) (states_as_list M))));
      distHelper = (λ q1 q2 . if q1 ∈ states M ∧ q2 ∈ states M ∧ q1 ≠ q2 then the (Mapping.lookup distMap (q1,q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2);
      pairs = filter (λ (x,y) . x ≠ y) (list_ordered_pairs (states_as_list M));
      distSet = from_list (map (case_prod distHelper) pairs);
      hsiMap = mapping_of (map (λ q . (q,from_list (map (λq' . distHelper q q') (filter ((≠) q) (states_as_list M))))) (states_as_list M));
      l = (Suc (m - size_r M));
      distFun = (λ k q . if k = l 
                      then (if q ∈ states M then the (Mapping.lookup hsiMap q) else get_HSI M q)
                      else distSet)
    in h_framework_static_with_empty_graph M distFun m)"  
(is "?f1 = ?f2") 
proof -
  define hsiMap' where "hsiMap' = mapping_of (map (λ q . (q,from_list (map (λq' . get_distinguishing_sequence_from_ofsm_tables M q q') (filter ((≠) q) (states_as_list M))))) (states_as_list M))"
  define distFun' where "distFun' = (λ k q . if k = (Suc (m - size_r M))
                      then (if q ∈ states M then the (Mapping.lookup hsiMap' q) else get_HSI M q)
                      else distinguishing_set M)"
  have *: "?f2 = h_framework_static_with_empty_graph M distFun' m"
    unfolding distFun'_def hsiMap'_def distinguishing_set.simps Let_def
    apply (subst (3 4 ) get_distinguishing_sequence_from_ofsm_tables_precomputed[of M])
    unfolding Let_def  
    by presburger

  define hsiMap where "hsiMap = map_of (map (λ q . (q,from_list (map (λq' . get_distinguishing_sequence_from_ofsm_tables M q q') (filter ((≠) q) (states_as_list M))))) (states_as_list M))"
  define distFun where "distFun = (λ k q . if k = (Suc (m - size_r M))
                      then (if q ∈ states M then the (hsiMap q) else get_HSI M q)
                      else distinguishing_set M)"

  have "distinct (map fst (map (λ q . (q,from_list (map (λq' . get_distinguishing_sequence_from_ofsm_tables M q q') (filter ((≠) q) (states_as_list M))))) (states_as_list M)))"
    using states_as_list_distinct
    by (metis map_pair_fst) 
  then have "Mapping.lookup hsiMap' = hsiMap"
    unfolding hsiMap_def hsiMap'_def  
    using mapping_of_map_of
    by blast
  then have "distFun' = distFun"
    unfolding distFun_def distFun'_def by meson

  have **:"distFun' = (distinguishing_set_or_state_identifier (Suc (m - size_r M)) M)" 
  proof     
    fix k show "distFun' k = (distinguishing_set_or_state_identifier (Suc (m - size_r M)) M) k"
    proof (cases "k = (Suc (m - size_r M))")
      case False
      then show ?thesis 
        unfolding distFun_def distinguishing_set_or_state_identifier.simps ‹distFun' = distFun› by auto
    next
      case True
      then have "distFun k = (λ q . (if q ∈ states M then the (hsiMap q) else get_HSI M q))"
            and "(distinguishing_set_or_state_identifier (Suc (m - size_r M)) M) k = (λ q . get_HSI M q)"
        unfolding distFun_def distinguishing_set_or_state_identifier.simps by auto
      moreover have "(λ q . (if q ∈ states M then the (hsiMap q) else get_HSI M q)) = (λ q . get_HSI M q)"
      proof 
        fix q show "(if q ∈ states M then the (hsiMap q) else get_HSI M q) = get_HSI M q"
        proof (cases "q ∈ states M")
          case True
          then have "q ∈ list.set (states_as_list M)"
            using states_as_list_set by blast
          then show ?thesis
            unfolding distFun_def hsiMap_def map_of_map_pair_entry get_HSI.simps
            using True
            by fastforce
        next
          case False
          then show ?thesis using distFun_def by auto
        qed
      qed
      ultimately show ?thesis unfolding ‹distFun' = distFun› by simp
    qed
  qed
  
  show ?thesis
    unfolding * ** wp_method_via_h_framework_def by simp
qed


end