# Theory Partial_Order_Reduction.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
```