Theory Ample_Analysis

section ‹Static Analysis for Partial Order Reduction›

theory Ample_Analysis
imports
  Ample_Abstract
begin

  locale transition_system_ample =
    transition_system_sticky ex en init int sticky +
    transition_system_interpreted_traces ex en int ind
    for ex :: "'action ⇒ 'state ⇒ 'state"
    and en :: "'action ⇒ 'state ⇒ bool"
    and init :: "'state ⇒ bool"
    and int :: "'state ⇒ 'interpretation"
    and sticky :: "'action set"
    and ind :: "'action ⇒ 'action ⇒ bool"
  begin

    sublocale ample_base "ex" "en" "int" "ind" "scut¯¯" by unfold_locales

    lemma restrict_ample_set:
      assumes "s ∈ nodes"
      assumes "A ∩ {a. en a s} ≠ {}" "A ∩ {a. en a s} ∩ sticky = {}"
      assumes "Ind (A ∩ {a. en a s}) (executable - A)"
      assumes "⋀ w. path w s ⟹ A ∩ {a. en a s} ∩ set w = {} ⟹ A ∩ set w = {}"
      shows "ample_set s (A ∩ {a. en a s})"
    unfolding ample_set_def
    proof (intro conjI allI impI)
      show "A ∩ {a. en a s} ⊆ {a. en a s}" by simp
    next
      show "A ∩ {a. en a s} ≠ {}" using assms(2) by this
    next
      fix a
      assume 1: "a ∈ A ∩ {a. en a s}"
      show "scut¯¯ (ex a s) s"
      proof (rule no_cut_scut)
        show "s ∈ nodes" using assms(1) by this
        show "en a s" using 1 by simp
        show "a ∉ sticky" using assms(3) 1 by auto
      qed
    next
      have 1: "A ∩ {a. en a s} ⊆ executable" using executable assms(1) by blast
      show "A ∩ {a. en a s} ⊆ invisible" using executable_visible_sticky assms(3) 1 by blast
    next
      fix w
      assume 1: "path w s" "A ∩ {a. en a s} ∩ set w = {}"
      have 2: "A ∩ set w = {}" using assms(5) 1 by this
      have 3: "set w ⊆ executable" using assms(1) 1(1) by rule
      show "Ind (A ∩ {a. en a s}) (set w)" using assms(4) 2 3 by blast
    qed

  end

  locale transition_system_concurrent =
    transition_system_initial ex en init
    for ex :: "'action ⇒ 'state ⇒ 'state"
    and en :: "'action ⇒ 'state ⇒ bool"
    and init :: "'state ⇒ bool"
    +
    fixes procs :: "'state ⇒ 'process set"
    fixes pac :: "'process ⇒ 'action set"
    fixes psen :: "'process ⇒ 'state ⇒ 'action set"
    assumes procs_finite: "s ∈ nodes ⟹ finite (procs s)"
    assumes psen_en: "s ∈ nodes ⟹ pac p ∩ {a. en a s} ⊆ psen p s"
    assumes psen_ex: "s ∈ nodes ⟹ a ∈ {a. en a s} - pac p ⟹ psen p (ex a s) = psen p s"
  begin

    lemma psen_fin_word:
      assumes "s ∈ nodes" "path w s" "pac p ∩ set w = {}"
      shows "psen p (target w s) = psen p s"
    using assms(2, 1, 3)
    proof induct
      case (nil s)
      show ?case by simp
    next
      case (cons a s w)
      have 1: "ex a s ∈ nodes" using cons(4, 1) by rule
      have "psen p (target (a # w) s) = psen p (target w (ex a s))" by simp
      also have "… = psen p (ex a s)" using cons 1 by simp
      also have "… = psen p s" using psen_ex cons by simp
      finally show ?case by this
    qed

    lemma en_fin_word:
      assumes "⋀ r a b. r ∈ nodes ⟹ a ∈ psen p s - {a. en a s} ⟹ b ∈ {a. en a r} - pac p ⟹
        en a (ex b r) ⟹ en a r"
      assumes "s ∈ nodes" "path w s" "pac p ∩ set w = {}"
      shows "pac p ∩ {a. en a (target w s)} ⊆ pac p ∩ {a. en a s}"
    using assms
    proof (induct w rule: rev_induct)
      case Nil
      show ?case by simp
    next
      case (snoc b w)
      show ?case
      proof (safe, rule ccontr)
        fix a
        assume 2: "a ∈ pac p" "en a (target (w @ [b]) s)" "¬ en a s"
        have 3: "a ∈ psen p s"
        proof -
          have 3: "psen p (target (w @ [b]) s) = psen p s" using psen_fin_word snoc(3, 4, 5) by this
          have 4: "target (w @ [b]) s ∈ nodes" using snoc(3, 4) by rule
          have 5: "a ∈ psen p (target (w @ [b]) s)" using psen_en 4 2(1, 2) by auto
          show ?thesis using 2(1) 3 5 by auto
        qed
        have 4: "en a (target w s)"
        proof (rule snoc(2))
          show "target w s ∈ nodes" using snoc(3, 4) by auto
          show "a ∈ psen p s - {a. en a s}" using 2(3) 3 by simp
          show "b ∈ {a. en a (target w s)} - pac p" using snoc(4, 5) by auto
          show "en a (ex b (target w s))" using 2(2) by simp
        qed
        have 5: "pac p ∩ {a. en a (target w s)} ⊆ pac p ∩ {a. en a s}"
        proof (rule snoc(1))
          show "⋀ r a b. r ∈ nodes ⟹ a ∈ psen p s - {a. en a s} ⟹ b ∈ {a. en a r} - pac p ⟹
            en a (ex b r) ⟹ en a r" using snoc(2) by this
          show "s ∈ nodes" using snoc(3) by this
          show "path w s" using snoc(4) by auto
          show "pac p ∩ set w = {}" using snoc(5) by auto
        qed
        have 6: "en a s" using 2(1) 4 5 by auto
        show "False" using 2(3) 6 by simp
      qed
    qed

    lemma pac_en_blocked:
      assumes "⋀ r a b. r ∈ nodes ⟹ a ∈ psen p s - {a. en a s} ⟹ b ∈ {a. en a r} - pac p ⟹
        en a (ex b r) ⟹ en a r"
      assumes "s ∈ nodes" "path w s" "pac p ∩ {a. en a s} ∩ set w = {}"
      shows "pac p ∩ set w = {}"
      using words_fin_blocked en_fin_word assms by metis

    abbreviation "proc a ≡ {p. a ∈ pac p}"
    abbreviation "Proc A ≡ ⋃ a ∈ A. proc a"

    lemma psen_simple:
      assumes "Proc (psen p s) = {p}"
      assumes "⋀ r a b. r ∈ nodes ⟹ a ∈ psen p s - {a. en a s} ⟹ en b r ⟹
        proc a ∩ proc b = {} ⟹ en a (ex b r) ⟹ en a r"
      shows "⋀ r a b. r ∈ nodes ⟹ a ∈ psen p s - {a. en a s} ⟹ b ∈ {a. en a r} - pac p ⟹
        en a (ex b r) ⟹ en a r"
      using assms by force

  end

end