Theory ASC_Example

theory ASC_Example
  imports ASC_Hoare
begin


section ‹ Example product machines and properties ›

text ‹
This section provides example FSMs and shows that the assumptions on the inputs of the adaptive
state counting algorithm are not vacuous.
›


subsection ‹ Constructing FSMs from transition relations ›

text ‹
This subsection provides a function to more easily create FSMs, only requiring a set of
transition-tuples and an initial state.
›


fun from_rel :: "('state × ('in × 'out) × 'state) set ⇒ 'state ⇒ ('in, 'out, 'state) FSM" where
"from_rel rel q0 = ⦇ succ = λ io p . { q . (p,io,q) ∈ rel },
                    inputs = image (fst ∘ fst ∘ snd) rel,
                    outputs = image (snd ∘ fst ∘ snd) rel,
                    initial = q0 ⦈"



lemma nodes_from_rel : "nodes (from_rel rel q0) ⊆ insert q0 (image (snd ∘ snd) rel)"
  (is "nodes ?M ⊆ insert q0 (image (snd ∘ snd) rel)")
proof -
  have "⋀ q io p . q ∈ succ ?M io p ⟹ q ∈ image (snd ∘ snd) rel"
    by force
  have "⋀ q . q ∈ nodes ?M ⟹ q = q0 ∨ q ∈ image (snd ∘ snd) rel"
  proof -
    fix q assume "q ∈ nodes ?M"
    then show "q = q0 ∨ q ∈ image (snd ∘ snd) rel"
    proof (cases rule: FSM.nodes.cases)
      case initial
      then show ?thesis by auto
    next
      case (execute p a)
      then show ?thesis
        using ‹⋀ q io p . q ∈ succ ?M io p ⟹ q ∈ image (snd ∘ snd) rel› by blast
    qed
  qed
  then show "nodes ?M ⊆ insert q0 (image (snd ∘ snd) rel)"
    by blast
qed



fun well_formed_rel :: "('state × ('in × 'out) × 'state) set ⇒ bool" where
  "well_formed_rel rel = (finite rel
                          ∧ (∀ s1 x y . (x ∉ image (fst ∘ fst ∘ snd) rel
                                            ∨ y ∉ image (snd ∘ fst ∘ snd) rel)
                                        ⟶ ¬(∃ s2 . (s1,(x,y),s2) ∈ rel))
                          ∧ rel ≠ {})"

lemma well_formed_from_rel :
  assumes "well_formed_rel rel"
  shows "well_formed (from_rel rel q0)"  (is "well_formed ?M")
proof -
  have "nodes ?M ⊆ insert q0 (image (snd ∘ snd) rel)"
    using nodes_from_rel[of rel q0] by auto
  moreover have "finite (insert q0 (image (snd ∘ snd) rel))"
    using assms by auto
  ultimately have "finite (nodes ?M)"
    by (simp add: Finite_Set.finite_subset)
  moreover have "finite (inputs ?M)" "finite (outputs ?M)"
    using assms by auto
  ultimately have "finite_FSM ?M"
    by auto

  moreover have "inputs ?M ≠ {}"
    using assms by auto
  moreover have "outputs ?M ≠ {}"
    using assms by auto
  moreover have "⋀ s1 x y . (x ∉ inputs ?M ∨ y ∉ outputs ?M) ⟶ succ ?M (x,y) s1 = {}"
    using assms by auto

  ultimately show ?thesis
    by auto
qed




fun completely_specified_rel_over :: "('state × ('in × 'out) × 'state) set ⇒ 'state set ⇒ bool"
  where
  "completely_specified_rel_over rel nods = (∀ s1 ∈ nods .
                                                ∀ x ∈ image (fst ∘ fst ∘ snd) rel .
                                                  ∃ y ∈ image (snd ∘ fst ∘ snd) rel .
                                                    ∃ s2 . (s1,(x,y),s2) ∈ rel)"

lemma completely_specified_from_rel :
  assumes "completely_specified_rel_over rel (nodes ((from_rel rel q0)))"
  shows "completely_specified (from_rel rel q0)"  (is "completely_specified ?M")
  unfolding completely_specified.simps
proof
  fix s1 assume "s1 ∈ nodes (from_rel rel q0)"
  show  "∀x∈inputs ?M. ∃y∈outputs ?M. ∃s2. s2 ∈ succ ?M (x, y) s1"
  proof
    fix x assume "x ∈ inputs (from_rel rel q0)"
    then have "x ∈  image (fst ∘ fst ∘ snd) rel"
      using assms by auto

    obtain y s2 where "y ∈ image (snd ∘ fst ∘ snd) rel" "(s1,(x,y),s2) ∈ rel"
      using assms ‹s1 ∈ nodes (from_rel rel q0)› ‹x ∈  image (fst ∘ fst ∘ snd) rel›
      by (meson completely_specified_rel_over.elims(2))

    then have "y ∈ outputs (from_rel rel q0)" "s2 ∈ succ (from_rel rel q0) (x, y) s1"
      by auto

    then show "∃y∈outputs (from_rel rel q0). ∃s2. s2 ∈ succ (from_rel rel q0) (x, y) s1"
      by blast
  qed
qed





fun observable_rel :: "('state × ('in × 'out) × 'state) set ⇒ bool" where
  "observable_rel rel = (∀ io s1 . { s2 . (s1,io,s2) ∈ rel } = {}
                                    ∨ (∃ s2 . { s2' . (s1,io,s2') ∈ rel } = {s2}))"

lemma observable_from_rel :
  assumes "observable_rel rel"
  shows "observable (from_rel rel q0)"  (is "observable ?M")
proof -
  have "⋀ io s1 . { s2 . (s1,io,s2) ∈ rel } = succ ?M io s1"
    by auto
  then show ?thesis using assms by auto
qed





abbreviation "OFSM_rel rel q0 ≡ well_formed_rel rel
                                ∧ completely_specified_rel_over rel (nodes (from_rel rel q0))
                                ∧ observable_rel rel"

lemma OFMS_from_rel :
  assumes "OFSM_rel rel q0"
  shows "OFSM (from_rel rel q0)"
  by (metis assms completely_specified_from_rel observable_from_rel well_formed_from_rel)




subsection ‹ Example FSMs and properties ›



abbreviation "M⇩S_rel :: (nat×(nat×nat)×nat) set ≡ {(0,(0,0),1), (0,(0,1),1), (1,(0,2),1)}"
abbreviation "M⇩S :: (nat,nat,nat) FSM ≡ from_rel M⇩S_rel 0"

abbreviation "M⇩I_rel :: (nat×(nat×nat)×nat) set ≡ {(0,(0,0),1), (0,(0,1),1), (1,(0,2),0)}"
abbreviation "M⇩I :: (nat,nat,nat) FSM ≡ from_rel M⇩I_rel 0"

lemma example_nodes :
  "nodes M⇩S = {0,1}" "nodes M⇩I = {0,1}"
proof -
  have "0 ∈ nodes M⇩S" by auto
  have "1 ∈ succ M⇩S (0,0) 0" by auto
  have "1 ∈ nodes M⇩S"
    by (meson ‹0 ∈ nodes M⇩S› ‹1 ∈ succ M⇩S (0, 0) 0› succ_nodes)

  have "{0,1} ⊆ nodes M⇩S"
    using ‹0 ∈ nodes M⇩S› ‹1 ∈ nodes M⇩S› by auto
  moreover have "nodes M⇩S ⊆ {0,1}"
    using nodes_from_rel[of M⇩S_rel 0] by auto
  ultimately show "nodes M⇩S = {0,1}"
    by blast
next
  have "0 ∈ nodes M⇩I" by auto
  have "1 ∈ succ M⇩I (0,0) 0" by auto
  have "1 ∈ nodes M⇩I"
    by (meson ‹0 ∈ nodes M⇩I› ‹1 ∈ succ M⇩I (0, 0) 0› succ_nodes)

  have "{0,1} ⊆ nodes M⇩I"
    using ‹0 ∈ nodes M⇩I› ‹1 ∈ nodes M⇩I› by auto
  moreover have "nodes M⇩I ⊆ {0,1}"
    using nodes_from_rel[of M⇩I_rel 0] by auto
  ultimately show "nodes M⇩I = {0,1}"
    by blast
qed



lemma example_OFSM :
  "OFSM M⇩S" "OFSM M⇩I"
proof -
  have "well_formed_rel M⇩S_rel"
    unfolding well_formed_rel.simps by auto

  moreover have "completely_specified_rel_over M⇩S_rel (nodes (from_rel M⇩S_rel 0))"
    unfolding completely_specified_rel_over.simps
  proof
    fix s1 assume "(s1::nat) ∈ nodes (from_rel M⇩S_rel 0)"
    then have "s1 ∈ (insert 0 (image (snd ∘ snd) M⇩S_rel))"
      using nodes_from_rel[of M⇩S_rel 0] by blast
    moreover have "completely_specified_rel_over M⇩S_rel (insert 0 (image (snd ∘ snd) M⇩S_rel))"
      unfolding completely_specified_rel_over.simps by auto
    ultimately show "∀x∈(fst ∘ fst ∘ snd) ` M⇩S_rel.
                      ∃y∈(snd ∘ fst ∘ snd) ` M⇩S_rel. ∃s2. (s1, (x, y), s2) ∈ M⇩S_rel"
      by simp
  qed

  moreover have "observable_rel M⇩S_rel"
    by auto

  ultimately have "OFSM_rel M⇩S_rel 0"
    by auto

  then show "OFSM M⇩S"
    using OFMS_from_rel[of M⇩S_rel 0] by linarith
next
  have "well_formed_rel M⇩I_rel"
    unfolding well_formed_rel.simps by auto

  moreover have "completely_specified_rel_over M⇩I_rel (nodes (from_rel M⇩I_rel 0))"
    unfolding completely_specified_rel_over.simps
  proof
    fix s1 assume "(s1::nat) ∈ nodes (from_rel M⇩I_rel 0)"
    then have "s1 ∈ (insert 0 (image (snd ∘ snd) M⇩I_rel))"
      using nodes_from_rel[of M⇩I_rel 0] by blast
    have "completely_specified_rel_over M⇩I_rel (insert 0 (image (snd ∘ snd) M⇩I_rel))"
      unfolding completely_specified_rel_over.simps by auto
    show "∀x∈(fst ∘ fst ∘ snd) ` M⇩I_rel.
            ∃y∈(snd ∘ fst ∘ snd) ` M⇩I_rel. ∃s2. (s1, (x, y), s2) ∈ M⇩I_rel"
      by (meson ‹completely_specified_rel_over M⇩I_rel (insert 0 ((snd ∘ snd) ` M⇩I_rel))›
          ‹s1 ∈ insert 0 ((snd ∘ snd) ` M⇩I_rel)› completely_specified_rel_over.elims(2))
  qed

  moreover have "observable_rel M⇩I_rel"
    by auto

  ultimately have "OFSM_rel M⇩I_rel 0"
    by auto

  then show "OFSM M⇩I"
    using OFMS_from_rel[of M⇩I_rel 0] by linarith
qed



lemma example_fault_domain : "asc_fault_domain M⇩S M⇩I 2"
proof -
  have "inputs M⇩S = inputs M⇩I"
    by auto
  moreover have "card (nodes M⇩I) ≤ 2"
    using example_nodes(2) by auto
  ultimately show "asc_fault_domain M⇩S M⇩I 2"
    by auto
qed

abbreviation "FAIL⇩I :: (nat×nat) ≡ (3,3)"
abbreviation "PM⇩I :: (nat, nat, nat×nat) FSM ≡ ⦇
            succ = (λ a (p1,p2) . (if (p1 ∈ nodes M⇩S ∧ p2 ∈ nodes M⇩I ∧ (fst a ∈ inputs M⇩S)
                                        ∧ (snd a ∈ outputs M⇩S ∪ outputs M⇩I))
                                    then (if (succ M⇩S a p1 = {} ∧ succ M⇩I a p2 ≠ {})
                                      then {FAIL⇩I}
                                      else (succ M⇩S a p1 × succ M⇩I a p2))
                                    else {})),
            inputs = inputs M⇩S,
            outputs = outputs M⇩S ∪ outputs M⇩I,
            initial = (initial M⇩S, initial M⇩I)
          ⦈"

lemma example_productF : "productF M⇩S M⇩I FAIL⇩I PM⇩I"
proof -
  have "inputs M⇩S = inputs M⇩I"
    by auto
  moreover have "fst FAIL⇩I ∉ nodes M⇩S"
    using example_nodes(1) by auto
  moreover have "snd FAIL⇩I ∉ nodes M⇩I"
    using example_nodes(2) by auto
  ultimately show ?thesis
    unfolding productF.simps by blast
qed



abbreviation "V⇩I :: nat list set ≡ {[],[0]}"

lemma example_det_state_cover : "is_det_state_cover M⇩S V⇩I"
proof -
  have "d_reaches M⇩S (initial M⇩S) [] (initial M⇩S)"
    by auto
  then have "initial M⇩S ∈ d_reachable M⇩S (initial M⇩S)"
    unfolding d_reachable.simps by blast

  have "d_reached_by M⇩S (initial M⇩S) [0] 1 [1] [0]"
  proof
    show "length [0] = length [0] ∧
    length [0] = length [1] ∧ path M⇩S (([0] || [0]) || [1]) (initial M⇩S)
                            ∧ target (([0] || [0]) || [1]) (initial M⇩S) = 1"
      by auto

    have "⋀ys2 tr2.
       length [0] = length ys2
          ∧ length [0] = length tr2
          ∧ path M⇩S (([0] || ys2) || tr2) (initial M⇩S)
            ⟶ target (([0] || ys2) || tr2) (initial M⇩S) = 1"
    proof
      fix ys2 tr2 assume "length [0] = length ys2 ∧ length [0] = length tr2
                            ∧ path M⇩S (([0] || ys2) || tr2) (initial M⇩S)"
      then have "length ys2 = 1" "length tr2 = 1" "path M⇩S (([0] || ys2) || tr2) (initial M⇩S)"
        by auto
      moreover obtain y2 where "ys2 = [y2]"
        using ‹length ys2 = 1›
        by (metis One_nat_def ‹length [0] = length ys2 ∧ length [0] = length tr2
            ∧ path M⇩S (([0] || ys2) || tr2) (initial M⇩S)› append.simps(1) append_butlast_last_id
            butlast_snoc length_butlast length_greater_0_conv list.size(3) nat.simps(3))
      moreover obtain t2 where "tr2 = [t2]"
        using ‹length tr2 = 1›
        by (metis One_nat_def ‹length [0] = length ys2 ∧ length [0] = length tr2
            ∧ path M⇩S (([0] || ys2) || tr2) (initial M⇩S)› append.simps(1) append_butlast_last_id
            butlast_snoc length_butlast length_greater_0_conv list.size(3) nat.simps(3))
      ultimately have "path M⇩S [((0,y2),t2)] (initial M⇩S)"
        by auto
      then have "t2 ∈ succ M⇩S (0,y2) (initial M⇩S)"
        by auto
      moreover have "⋀ y . succ M⇩S (0,y) (initial M⇩S) ⊆ {1}"
        by auto
      ultimately have "t2 = 1"
        by blast

      show "target (([0] || ys2) || tr2) (initial M⇩S) = 1"
        using ‹ys2 = [y2]› ‹tr2 = [t2]› ‹t2 = 1› by auto
    qed
    then show "∀ys2 tr2.
       length [0] = length ys2 ∧ length [0] = length tr2
          ∧ path M⇩S (([0] || ys2) || tr2) (initial M⇩S)
            ⟶ target (([0] || ys2) || tr2) (initial M⇩S) = 1"
      by auto
  qed

  then have "d_reaches M⇩S (initial M⇩S) [0] 1"
    unfolding d_reaches.simps by blast
  then have "1 ∈ d_reachable M⇩S (initial M⇩S)"
    unfolding d_reachable.simps by blast

  then have "{0,1} ⊆ d_reachable M⇩S (initial M⇩S)"
    using ‹initial M⇩S ∈ d_reachable M⇩S (initial M⇩S)› by auto
  moreover have "d_reachable M⇩S (initial M⇩S) ⊆ nodes M⇩S"
  proof
    fix s assume "s∈d_reachable M⇩S (initial M⇩S)"
    then have "s ∈ reachable M⇩S (initial M⇩S)"
      using d_reachable_reachable by auto
    then show "s ∈ nodes M⇩S"
      by blast
  qed
  ultimately have "d_reachable M⇩S (initial M⇩S) = {0,1}"
    using example_nodes(1) by blast



  fix f' :: "nat ⇒ nat list"
  let ?f = "f'( 0 := [], 1 := [0])"

  have "is_det_state_cover_ass M⇩S ?f"
    unfolding is_det_state_cover_ass.simps
  proof
    show "?f (initial M⇩S) = []" by auto
    show "∀s∈d_reachable M⇩S (initial M⇩S). d_reaches M⇩S (initial M⇩S) (?f s) s"
    proof
      fix s assume "s∈d_reachable M⇩S (initial M⇩S)"
      then have "s ∈ reachable M⇩S (initial M⇩S)"
        using d_reachable_reachable by auto
      then have "s ∈ nodes M⇩S"
        by blast
      then have "s = 0 ∨ s = 1"
        using example_nodes(1) by blast
      then show "d_reaches M⇩S (initial M⇩S) (?f s) s"
      proof
        assume "s = 0"
        then show "d_reaches M⇩S (initial M⇩S) (?f s) s"
          using ‹d_reaches M⇩S (initial M⇩S) [] (initial M⇩S)› by auto
      next
        assume "s = 1"
        then show "d_reaches M⇩S (initial M⇩S) (?f s) s"
          using ‹d_reaches M⇩S (initial M⇩S) [0] 1› by auto
      qed
    qed
  qed

  moreover have "V⇩I = image ?f (d_reachable M⇩S (initial M⇩S))"
    using ‹d_reachable M⇩S (initial M⇩S) = {0,1}› by auto

  ultimately show ?thesis
    unfolding is_det_state_cover.simps by blast
qed



abbreviation "Ω⇩I::(nat,nat) ATC set ≡ { Node 0 (λ y . Leaf) }"

lemma "applicable_set M⇩S Ω⇩I"
  by auto


lemma example_test_tools : "test_tools M⇩S M⇩I FAIL⇩I PM⇩I V⇩I Ω⇩I"
  using example_productF example_det_state_cover by auto




lemma OFSM_not_vacuous :
  "∃ M :: (nat,nat,nat) FSM . OFSM M"
  using example_OFSM(1) by blast


lemma fault_domain_not_vacuous :
  "∃ (M2::(nat,nat,nat) FSM) (M1::(nat,nat,nat) FSM) m . asc_fault_domain M2 M1 m"
  using example_fault_domain by blast


lemma test_tools_not_vacuous :
  "∃ (M2::(nat,nat,nat) FSM)
     (M1::(nat,nat,nat) FSM)
     (FAIL::(nat×nat))
     (PM::(nat,nat,nat×nat) FSM)
     (V::(nat list set))
     (Ω::(nat,nat) ATC set) . test_tools M2 M1 FAIL PM V Ω"
proof (rule exI, rule exI)
  show "∃ FAIL PM V Ω. test_tools M⇩S M⇩I FAIL PM V Ω"
    using example_test_tools by blast
qed

lemma precondition_not_vacuous :
  shows "∃ (M2::(nat,nat,nat) FSM)
           (M1::(nat,nat,nat) FSM)
           (FAIL::(nat×nat))
           (PM::(nat,nat,nat×nat) FSM)
           (V::(nat list set))
           (Ω::(nat,nat) ATC set)
           (m :: nat) .
              OFSM M1 ∧ OFSM M2 ∧ asc_fault_domain M2 M1 m ∧ test_tools M2 M1 FAIL PM V Ω"
proof (intro exI)
  show "OFSM M⇩I ∧ OFSM M⇩S ∧ asc_fault_domain M⇩S M⇩I 2 ∧ test_tools M⇩S M⇩I FAIL⇩I PM⇩I V⇩I Ω⇩I"
    using example_OFSM(2,1) example_fault_domain example_test_tools by linarith
qed

end