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