Theory Deadlock_Impl
theory Deadlock_Impl
imports Deadlock Munta_Base.Abstract_Term
begin
paragraph ‹Misc›
lemma constraint_clk_conv_ac:
"constraint_clk (conv_ac ac) = constraint_clk ac"
by (cases ac; auto)
lemma constraint_clk_conv_cc:
"collect_clks (conv_cc cc) = collect_clks cc"
by (auto simp: collect_clks_def constraint_clk_conv_ac image_def)
lemma atLeastLessThan_alt_def:
"{a..<b} = {k. a ≤ k ∧ k < b}"
by auto
lemma atLeastLessThan_Suc_alt_def:
"{a..<Suc b} = {k. a ≤ k ∧ k ≤ b}"
by auto
lemma (in Graph_Defs) deadlock_if_deadlocked:
"deadlock y" if "deadlocked y"
using that unfolding deadlock_def by auto
subsection ‹Functional Refinement›
paragraph ‹Elementary list operations›
lemma map_conv_rev_fold:
"map f xs = rev (fold (λ a xs. f a # xs) xs [])"
proof -
have "fold (λ a xs. f a # xs) xs ys = rev (map f xs) @ ys" for ys
by (induction xs arbitrary: ys) auto
then show ?thesis
by simp
qed
lemma concat_map_conv_rev_fold:
"concat (map f xs) = rev (fold (λ xs ys. rev (f xs) @ ys) xs [])"
proof -
have "rev (fold (λ xs ys. rev (f xs) @ ys) xs ys) = rev ys @ List.maps f xs" for ys
by (induction xs arbitrary: ys) (auto simp: maps_simps)
then show ?thesis
by (simp add: concat_map_maps)
qed
lemma concat_conv_fold_rev:
"concat xss = fold (@) (rev xss) []"
using fold_append_concat_rev[of "rev xss"] by simp
lemma filter_conv_rev_fold:
"filter P xs = rev (fold (λx xs. if P x then x # xs else xs) xs [])"
proof -
have "rev ys @ filter P xs = rev (fold (λx xs. if P x then x # xs else xs) xs ys)" for ys
by (induction xs arbitrary: ys) (auto, metis revg.simps(2) revg_fun)
from this[symmetric] show ?thesis
by simp
qed
paragraph ‹DBM operations›
definition
"free_upd1 n M c =
(let
M1 = fold (λi M. if i ≠ c then (M((i, c) := op_mtx_get M (i, 0))) else M) [0..<Suc n] M;
M2 = fold (λi M. if i ≠ c then M((c,i) := ∞) else M) [0..<Suc n] M1
in
M2
)
"
definition
"pre_reset_upd1 n M x ≡ free_upd1 n (restrict_zero_upd n M x) x"
definition
"pre_reset_list_upd1 n M r ≡ fold (λ x M. pre_reset_upd1 n M x) r M"
definition
"upd_pairs xs = fold (λ(p,q) f. f(p:=q)) xs"
lemma upd_pairs_Nil:
"upd_pairs [] f = f"
unfolding upd_pairs_def by simp
lemma upd_pairs_Cons:
"upd_pairs ((p, q) # xs) f = upd_pairs xs (f(p:=q))"
unfolding upd_pairs_def by simp
lemma upd_pairs_no_upd:
assumes "p ∉ fst ` set xs"
shows "upd_pairs xs f p = f p"
using assms by (induction xs arbitrary: f) (auto simp: upd_pairs_Nil upd_pairs_Cons)
lemma upd_pairs_upd:
assumes "(p, y) ∈ set xs" "distinct (map fst xs)"
shows "upd_pairs xs f p = y"
using assms proof (induction xs arbitrary: f)
case Nil
then show ?case
by (simp add: upd_pairs_Nil)
next
case (Cons x xs)
then show ?case
by (cases x) (auto simp add: upd_pairs_Cons upd_pairs_no_upd)
qed
lemma upd_pairs_append:
"upd_pairs (xs @ ys) = upd_pairs ys o upd_pairs xs"
unfolding upd_pairs_def fold_append ..
lemma upd_pairs_commute_single:
"upd_pairs xs (f(a := b)) = (upd_pairs xs f)(a := b)" if "a ∉ fst ` set xs"
using that by (induction xs arbitrary: f) (auto simp: upd_pairs_Nil upd_pairs_Cons fun_upd_twist)
lemma upd_pairs_append':
"upd_pairs (xs @ ys) = upd_pairs xs o upd_pairs ys" if "fst ` set xs ∩ fst ` set ys = {}"
using that
proof (induction xs)
case Nil
then show ?case
by (simp add: upd_pairs_Nil)
next
case (Cons a xs)
then show ?case
by (cases a) (auto simp add: upd_pairs_Nil upd_pairs_Cons upd_pairs_commute_single)
qed
definition
"upd_pairs' xs = fold (λ(p,q) f. f(p:=f q)) xs"
lemma upd_pairs'_Nil:
"upd_pairs' [] f = f"
unfolding upd_pairs'_def by simp
lemma upd_pairs'_Cons:
"upd_pairs' ((p, q) # xs) f = upd_pairs' xs (f(p:=f q))"
unfolding upd_pairs'_def by simp
lemma upd_pairs'_upd_pairs:
assumes "fst ` set xs ∩ snd ` set xs = {}"
shows "upd_pairs' xs f = upd_pairs (map (λ(p, q). (p, f q)) xs) f"
using assms
proof (induction xs arbitrary: f)
case Nil
then show ?case
by (simp add: upd_pairs_Nil upd_pairs'_Nil)
next
case (Cons x xs)
obtain a b where [simp]: "x = (a, b)"
by (cases x)
from Cons.prems have *:
"map (λ(p, q). (p, if q = a then f b else f q)) xs = map (λ(p, q). (p, f q)) xs"
by auto
from Cons show ?case
by (auto simp add: upd_pairs_Cons upd_pairs'_Cons *)
qed
lemma upd_pairs_map:
"upd_pairs (map f xs) = fold (λpq g. let (p,q) = f pq in g(p:=q)) xs"
unfolding upd_pairs_def fold_map
by (intro arg_cong2[where f = fold] ext) (auto simp: comp_def split: prod.split)
lemma down_upd_alt_def:
"down_upd n M =
upd_pairs ([((0, j), fold min [M (k, j). k ← [1..<Suc n]] (Le 0)). j ← [1..<Suc n]]) M"
proof -
define xs where
"xs = [((0::nat, j), Min ({Le 0} ∪ {M (k, j) | k. 1 ≤ k ∧ k ≤ n})). j ← [1..<Suc n]]"
have "distinct (map fst xs)"
unfolding xs_def by (auto simp add: map_concat comp_def distinct_map)
have *: "fold min [M (k, j). k←[1..<Suc n]] (Le 0) = Min ({Le 0} ∪ {M (k, j) |k. 1 ≤ k ∧ k ≤ n})"
for j
by (subst Min.set_eq_fold[symmetric])
(auto simp: atLeastLessThan_Suc_alt_def simp del: upt_Suc intro: arg_cong[where f = Min])
show ?thesis
unfolding * xs_def[symmetric]
by (intro ext, auto simp add: down_upd_def)
(solves ‹subst upd_pairs_upd[OF _ ‹distinct _›] upd_pairs_no_upd,
auto simp: image_def xs_def›)+
qed
lemma down_upd_alt_def1:
"down_upd n M =
fold (λj M. let (p,q) = ((0, j), fold min [M (k, j). k ← [1..<Suc n]] (Le 0)) in M(p:=q))
[1..<Suc n] M"
proof -
have *: "
fold (λj M. let (p,q) = ((0,j), fold min [M (k, j). k ← [1..<Suc n]] (Le 0)) in M(p:=q)) xs M
= fold (λj M'. let (p,q) = ((0,j), fold min [M (k, j). k ← [1..<Suc n]] (Le 0)) in M'(p:=q)) xs M
" for xs
proof (induction xs arbitrary: M)
case Nil
then show ?case
by simp
next
case (Cons x xs)
then show ?case
by (auto 4 7 intro: arg_cong2[where f = min] fold_cong)
qed
then show ?thesis
unfolding down_upd_alt_def upd_pairs_map ..
qed
lemma
"free_upd n M c =
upd_pairs ([((c,i), ∞). i ← [0..<Suc n], i ≠ c] @ [((i,c), M(i,0)). i ← [0..<Suc n], i ≠ c]) M"
if "c ≤ n"
proof -
let ?xs1 = "λn. [((c,i), ∞). i ← [0..<Suc n], i ≠ c]"
let ?xs2 = "λn. [((i,c), M(i,0)). i ← [0..<Suc n], i ≠ c]"
define xs where "xs = ?xs1 n @ ?xs2 n"
have "distinct (map fst xs)"
unfolding xs_def
apply (clarsimp simp del: upt_Suc simp add: map_concat comp_def if_distrib split: if_split)
apply (auto split: if_split_asm simp: distinct_map inj_on_def intro!: distinct_concat)
done
from ‹c ≤ n› show ?thesis
unfolding xs_def[symmetric]
by (intro ext, auto simp: free_upd_def)
(solves ‹subst upd_pairs_upd[OF _ ‹distinct (map fst xs)›] upd_pairs_no_upd,
auto simp: xs_def›)+
qed
lemma free_upd_alt_def1:
"free_upd n M c = (let
M1 = upd_pairs' ([((i,c), (i,0)). i ← [0..<Suc n], i ≠ c]) M;
M2 = upd_pairs ([((c,i), ∞). i ← [0..<Suc n], i ≠ c]) M1
in
M2
)" (is "_ = ?r")
if "0 < c" "c ≤ n"
proof -
let ?xs1 = "λn. [((c,i), ∞). i ← [0..<Suc n], i ≠ c]"
let ?xs2 = "λn. [((i,c), M(i,0)). i ← [0..<Suc n], i ≠ c]"
define xs where "xs = ?xs1 n @ ?xs2 n"
let ?t = "upd_pairs xs M"
have "distinct (map fst xs)"
unfolding xs_def
apply (clarsimp simp del: upt_Suc simp add: map_concat comp_def if_distrib split: if_split)
apply (auto split: if_split_asm simp: distinct_map inj_on_def intro!: distinct_concat)
done
from ‹c ≤ n› have "free_upd n M c = ?t"
by (intro ext, auto simp: free_upd_def)
(solves ‹subst upd_pairs_upd[OF _ ‹distinct _›] upd_pairs_no_upd, auto simp: xs_def›)+
also have "… = ?r"
unfolding xs_def
apply (subst upd_pairs_append')
subgoal
by auto
apply (subst upd_pairs'_upd_pairs)
subgoal
using ‹c > 0› by auto
apply (simp del: upt_Suc add: map_concat)
apply (intro arg_cong2[where f = upd_pairs] arg_cong[where f = concat])
by (simp del: upt_Suc)+
finally show ?thesis .
qed
lemma free_upd_free_upd1:
"free_upd n M c = free_upd1 n M c" if "c > 0" "c ≤ n"
proof -
let ?x1 = "λxs. upd_pairs' ([((i,c), (i,0)). i ← xs, i ≠ c]) M"
let ?x2 = "λxs. fold (λi M. if i ≠ c then (M((i, c) := M(i, 0))) else M) xs M"
have *: "?x1 xs = ?x2 xs" for xs
by (induction xs arbitrary: M) (auto simp: upd_pairs'_Nil upd_pairs'_Cons)
let ?y1 = "λxs. upd_pairs ([((c,i), ∞). i ← xs, i ≠ c])"
let ?y2 = "fold (λi M. if i ≠ c then M((c,i) := ∞) else M)"
have **: "?y1 xs M = ?y2 xs M" for xs M
by (induction xs arbitrary: M) (auto simp: upd_pairs_Nil upd_pairs_Cons)
show ?thesis
unfolding free_upd_alt_def1[OF that] free_upd1_def op_mtx_get_def * ** ..
qed
lemma free_upd_alt_def:
"free_upd n M c =
fold (λi M. if i ≠ c then (M((c,i) := ∞, (i, c) := M(i, 0))) else M) [0..<Suc n] M"
if "c ≤ n"
oops
lemma pre_reset_upd_pre_reset_upd1:
"pre_reset_upd n M c = pre_reset_upd1 n M c" if "c > 0" "c ≤ n"
unfolding pre_reset_upd_def pre_reset_upd1_def free_upd_free_upd1[OF that] ..
lemma pre_reset_list_upd_pre_reset_list_upd1:
"pre_reset_list_upd n M cs = pre_reset_list_upd1 n M cs" if "∀c ∈ set cs. 0 < c ∧ c ≤ n"
unfolding pre_reset_list_upd_def pre_reset_list_upd1_def
using that by (intro fold_cong; simp add: pre_reset_upd_pre_reset_upd1)
lemma pre_reset_list_transfer'[transfer_rule]:
includes lifting_syntax shows
"(eq_onp (λx. x = n) ===> RI2 n ===> list_all2 (eq_onp (λx. 0 < x ∧ x < Suc n)) ===> RI2 n)
pre_reset_list pre_reset_list_upd1"
unfolding rel_fun_def
apply safe
apply (subst pre_reset_list_upd_pre_reset_list_upd1[symmetric])
subgoal
unfolding list.rel_eq_onp by (auto simp: eq_onp_def list_all_iff)
by (rule pre_reset_list_transfer[unfolded rel_fun_def, rule_format])
(auto simp: eq_onp_def list_all2_iff)
subsection ‹Imperative Refinement›
context
fixes n :: nat
notes [id_rules] = itypeI[of n "TYPE (nat)"]
and [sepref_import_param] = IdI[of n]
begin
interpretation DBM_Impl n .
sepref_definition down_impl is
"RETURN o PR_CONST (down_upd n)" :: "mtx_assn⇧d →⇩a mtx_assn"
unfolding down_upd_alt_def1 upd_pairs_map PR_CONST_def
unfolding Let_def prod.case
unfolding fold_map comp_def
unfolding neutral[symmetric]
by sepref
context
notes [map_type_eqs] = map_type_eqI[of "TYPE(nat * nat ⇒ 'e)" "TYPE('e i_mtx)"]
begin
sepref_register
abstr_upd "FW'' n" "Normalized_Zone_Semantics_Impl_Semantic_Refinement.repair_pair n"
and_entry_upd "free_upd1 n" "restrict_zero_upd n" "pre_reset_upd1 n"
end
lemmas [sepref_fr_rules] = abstr_upd_impl.refine fw_impl_refine_FW''
sepref_definition abstr_FW_impl is
"uncurry (RETURN oo PR_CONST (abstr_FW_upd n))" ::
"(list_assn (acconstraint_assn clock_assn id_assn))⇧k *⇩a mtx_assn⇧d →⇩a mtx_assn"
unfolding abstr_FW_upd_def FW''_def[symmetric] PR_CONST_def by sepref
sepref_definition free_impl is
"uncurry (RETURN oo PR_CONST (free_upd1 n))" ::
"[λ(_, i). i≤n]⇩a mtx_assn⇧d *⇩a nat_assn⇧k → mtx_assn"
unfolding free_upd1_def op_mtx_set_def[symmetric] PR_CONST_def by sepref
sepref_definition and_entry_impl is
"uncurry2 (uncurry (λx. RETURN ooo and_entry_upd x))" ::
"[λ(((i, j),_),_). i≤n ∧ j ≤ n]⇩a nat_assn⇧k *⇩a nat_assn⇧k *⇩a id_assn⇧k *⇩a mtx_assn⇧d → mtx_assn"
unfolding and_entry_upd_def by sepref
lemmas [sepref_fr_rules] = and_entry_impl.refine
sepref_definition restrict_zero_impl is
"uncurry (RETURN oo PR_CONST (restrict_zero_upd n))" ::
"[λ(_, i). i≤n]⇩a mtx_assn⇧d *⇩a nat_assn⇧k → mtx_assn"
unfolding restrict_zero_upd_def PR_CONST_def by sepref
lemmas [sepref_fr_rules] = free_impl.refine restrict_zero_impl.refine
sepref_definition pre_reset_impl is
"uncurry (RETURN oo PR_CONST (pre_reset_upd1 n))" ::
"[λ(_, i). i≤n]⇩a mtx_assn⇧d *⇩a (clock_assn)⇧k → mtx_assn"
unfolding pre_reset_upd1_def PR_CONST_def by sepref
lemmas [sepref_fr_rules] = pre_reset_impl.refine
sepref_definition pre_reset_list_impl is
"uncurry (RETURN oo PR_CONST (pre_reset_list_upd1 n))" ::
"mtx_assn⇧d *⇩a (list_assn (clock_assn))⇧k →⇩a mtx_assn"
unfolding pre_reset_list_upd1_def PR_CONST_def by sepref
sepref_definition and_entry_repair_impl is
"uncurry2 (uncurry (λx. RETURN ooo PR_CONST (and_entry_repair_upd n) x))" ::
"[λ(((i, j),_),_). i≤n ∧ j ≤ n]⇩a nat_assn⇧k *⇩a nat_assn⇧k *⇩a id_assn⇧k *⇩a mtx_assn⇧d → mtx_assn"
unfolding and_entry_repair_upd_def PR_CONST_def by sepref
private definition
"V_dbm'' = V_dbm' n"
text ‹We use @{term V_dbm''} because we cannot register @{term V_dbm'} twice with the refinement
framework: we view it as a function first, and as a DBM later.›
lemma V_dbm'_alt_def:
"V_dbm' n = op_amtx_new (Suc n) (Suc n) (V_dbm'')"
unfolding V_dbm''_def by simp
notation fun_rel_syn (infixr "→" 60)
text ‹We need the custom rule here because @{term V_dbm'} is a higher-order constant›
lemma [sepref_fr_rules]:
"(uncurry0 (return V_dbm''), uncurry0 (RETURN (PR_CONST (V_dbm''))))
∈ unit_assn⇧k →⇩a pure (nat_rel ×⇩r nat_rel → Id)"
by sepref_to_hoare sep_auto
sepref_register "V_dbm'' :: nat × nat ⇒ _ DBMEntry"
text ‹Necessary to solve side conditions of @{term op_amtx_new}›
lemma V_dbm''_bounded:
"mtx_nonzero V_dbm'' ⊆ {0..<Suc n} × {0..<Suc n}"
unfolding mtx_nonzero_def V_dbm''_def V_dbm'_def neutral by auto
text ‹We need to pre-process the lemmas due to a failure of ‹TRADE››
lemma V_dbm''_bounded_1:
"(a, b) ∈ mtx_nonzero V_dbm'' ⟹ a < Suc n"
using V_dbm''_bounded by auto
lemma V_dbm''_bounded_2:
"(a, b) ∈ mtx_nonzero V_dbm'' ⟹ b < Suc n"
using V_dbm''_bounded by auto
lemmas [sepref_opt_simps] = V_dbm''_def
sepref_definition V_dbm_impl is
"uncurry0 (RETURN (PR_CONST (V_dbm' n)))" :: "unit_assn⇧k →⇩a mtx_assn"
supply V_dbm''_bounded_1[simp] V_dbm''_bounded_2[simp]
using V_dbm''_bounded
apply (subst V_dbm'_alt_def)
unfolding PR_CONST_def by sepref
text ‹This form of 'type casting' is used to assert a bound on the natural number.›
private definition make_clock :: "nat ⇒ nat" where [sepref_opt_simps]:
"make_clock x = x"
lemma make_clock[sepref_import_param]:
"(make_clock, make_clock) ∈ [λi. i ≤ n]⇩f nat_rel → nbn_rel (Suc n)"
unfolding make_clock_def by (rule frefI) simp
private definition "get_entries m =
[(make_clock i, make_clock j).
i←[0..<Suc n], j←[0..<Suc n], (i > 0 ∨ j > 0) ∧ i ≤ n ∧ j ≤ n ∧ m (i, j) ≠ ∞]"
private lemma get_entries_alt_def:
"get_entries m = [(make_clock i, make_clock j).
i←[0..<Suc n], j←[0..<Suc n], (i > 0 ∨ j > 0) ∧ m (i, j) ≠ ∞]"
unfolding get_entries_def by (intro arg_cong[where f = concat] map_cong) auto
private definition
"upd_entry i j M m = and_entry_repair_upd n j i (neg_dbm_entry (m (i, j))) (op_mtx_copy M)"
private definition
"upd_entries i j m = map (λ M. upd_entry i j M m)"
context
notes [map_type_eqs] = map_type_eqI[of "TYPE(nat * nat ⇒ 'e)" "TYPE('e i_mtx)"]
begin
sepref_register
"dbm_minus_canonical_check_upd n"
"dbm_subset_fed_upd n" "abstr_FW_upd n" "pre_reset_list_upd1 n" "V_dbm' n" "down_upd n"
upd_entry upd_entries get_entries "and_entry_repair_upd n"
end
lemma [sepref_import_param]: "(neg_dbm_entry,neg_dbm_entry) ∈ Id→Id" by simp
lemmas [sepref_fr_rules] = and_entry_repair_impl.refine
sepref_definition upd_entry_impl is
"uncurry2 (uncurry (λx. RETURN ooo PR_CONST upd_entry x))" ::
"[λ(((i, j),_),_). i≤n ∧ j ≤ n]⇩a
nat_assn⇧k *⇩a nat_assn⇧k *⇩a mtx_assn⇧k *⇩a mtx_assn⇧k → mtx_assn"
unfolding upd_entry_def PR_CONST_def by sepref
text ‹This is to ensure that the refinement initially infers the right 'type' for list arguments.›
lemma [intf_of_assn]:
"intf_of_assn AA TYPE('aa) ⟹ intf_of_assn (list_assn(AA)) TYPE('aa list)"
by (rule intf_of_assnI)
lemmas [sepref_fr_rules] = upd_entry_impl.refine
sepref_definition upd_entries_impl is
"uncurry2 (uncurry (λx. RETURN ooo PR_CONST upd_entries x))" ::
"[λ(((i, j),_),_). i≤n ∧ j ≤ n]⇩a
nat_assn⇧k *⇩a nat_assn⇧k *⇩a mtx_assn⇧k *⇩a (list_assn mtx_assn)⇧k → list_assn mtx_assn"
unfolding upd_entries_def PR_CONST_def
unfolding map_conv_rev_fold rev_conv_fold
supply [sepref_fr_rules] = HOL_list_empty_hnr_aux
by sepref
lemma [sepref_import_param]: "((=), (=)) ∈ Id→Id→Id" by simp
sepref_definition get_entries_impl is
"RETURN o PR_CONST get_entries" ::
"mtx_assn⇧k →⇩a list_assn ((clock_assn) ×⇩a (clock_assn))"
unfolding get_entries_alt_def PR_CONST_def
unfolding map_conv_rev_fold
unfolding concat_conv_fold_rev
supply [sepref_fr_rules] = HOL_list_empty_hnr_aux
by sepref
lemmas [sepref_fr_rules] = upd_entries_impl.refine get_entries_impl.refine
private lemma dbm_minus_canonical_upd_alt_def:
"dbm_minus_canonical_upd n xs m =
concat (map (λij. map (λ M.
and_entry_repair_upd n (snd ij) (fst ij) (neg_dbm_entry (m (fst ij, snd ij))) (op_mtx_copy M))
xs) (get_entries m))"
unfolding dbm_minus_canonical_upd_def op_mtx_copy_def get_entries_def split_beta make_clock_def
by simp
sepref_definition dbm_minus_canonical_impl is
"uncurry (RETURN oo PR_CONST (dbm_minus_canonical_check_upd n))" ::
"(list_assn mtx_assn)⇧k *⇩a mtx_assn⇧k →⇩a list_assn mtx_assn"
unfolding dbm_minus_canonical_check_upd_def dbm_minus_canonical_upd_alt_def PR_CONST_def
unfolding upd_entry_def[symmetric] upd_entries_def[symmetric]
unfolding filter_conv_rev_fold concat_map_conv_rev_fold rev_conv_fold
supply [sepref_fr_rules] = HOL_list_empty_hnr_aux
by sepref
lemmas [sepref_fr_rules] = dbm_minus_canonical_impl.refine
sepref_definition dbm_subset_fed_impl is
"uncurry (RETURN oo PR_CONST (dbm_subset_fed_upd n))" ::
"mtx_assn⇧d *⇩a (list_assn mtx_assn)⇧d →⇩a bool_assn"
unfolding dbm_subset_fed_upd_alt_def PR_CONST_def
unfolding list_ex_foldli filter_conv_rev_fold
unfolding short_circuit_conv
supply [sepref_fr_rules] = HOL_list_empty_hnr_aux
by sepref
end
subsection ‹Implementation for a Concrete Automaton›
context TA_Impl
begin
sublocale TA_Impl_Op
where loc_rel = loc_rel and f = "PR_CONST E_op''" and op_impl = E_op''_impl
unfolding PR_CONST_def by standard (rule E_op''_impl.refine)
end
context TA_Impl
begin
definition
"check_deadlock_dbm l M = dbm_subset_fed_upd n M (
[down_upd n (abstr_FW_upd n (inv_of_A l) (abstr_FW_upd n g
(pre_reset_list_upd1 n (abstr_FW_upd n (inv_of_A l') (V_dbm' n)) r)
)). (g, a, r, l') ← trans_fun l
]
)"
abbreviation zone_of ("⟦_⟧") where "zone_of M ≡ [curry (conv_M M)]⇘v,n⇙"
theorem check_deadlock_dbm_correct:
"TA.check_deadlock l ⟦M⟧ = check_deadlock_dbm l M" if
"⟦M⟧ ⊆ V" "l ∈ states'" "Deadlock.canonical' n (curry (conv_M M))"
proof -
text ‹0. Setup ‹&› auxiliary facts›
include lifting_syntax
note [simp del] = And.simps abstr.simps
have inv_of_simp: "inv_of (conv_A A) l = conv_cc (inv_of A l)" for l
using inv_fun unfolding inv_rel_def b_rel_def fun_rel_def conv_A_def
by (force split: prod.split simp: inv_of_def)
have trans_funD: "l' ∈ states"
"collect_clks (inv_of A l) ⊆ clk_set A" "collect_clks (inv_of A l') ⊆ clk_set A"
"collect_clks g ⊆ clk_set A" "set r ⊆ clk_set A"
if "(g, a, r, l') ∈ set (trans_fun l)" for g a r l'
subgoal
using ‹l ∈ states'› that trans_impl_states by auto
subgoal
by (metis collect_clks_inv_clk_set)
subgoal
by (metis collect_clks_inv_clk_set)
subgoal
using that ‹l ∈ _› by (intro collect_clocks_clk_set trans_impl_trans_of)
subgoal
using that ‹l ∈ _› by (intro reset_clk_set trans_impl_trans_of)
done
text ‹1. Transfer to most abstract DBM operations›
have [transfer_rule]:
"(eq_onp (λ (g, a, r, l'). (g, a, r, l') ∈ set (trans_fun l)) ===> RI2 n)
(λ(g, a, r, l'). down n
(abstr_FW n (conv_cc (inv_of A l))
(abstr_FW n (conv_cc g)
(pre_reset_list n (abstr_FW n (conv_cc (inv_of A l')) V_dbm v) r) v) v))
(λ(g, a, r, l'). down_upd n
(abstr_FW_upd n (inv_of A l)
(abstr_FW_upd n g (pre_reset_list_upd1 n (abstr_FW_upd n (inv_of A l') (V_dbm' n)) r))
))
" (is "(_ ===> RI2 n) (λ (g, a, r, l'). ?f g a r l') (λ (g, a, r, l'). ?g g a r l')")
proof -
{
fix g a r l' assume "(g, a, r, l') ∈ set (trans_fun l)"
have *: "rel_acconstraint (eq_onp (λx. 0 < x ∧ x < Suc n)) ri (conv_ac ac) ac"
if "constraint_clk ac > 0" "constraint_clk ac ≤ n" for ac
using that by (cases ac) (auto simp: eq_onp_def ri_def)
have *: "list_all2 (rel_acconstraint (eq_onp (λx. 0 < x ∧ x < Suc n)) ri) (conv_cc g) g"
if "collect_clks g ⊆ clk_set A" for g
unfolding list_all2_map1 using that clock_range
by (auto simp: collect_clks_def intro!: * list.rel_refl_strong)
have [transfer_rule]:
"list_all2 (rel_acconstraint (eq_onp (λx. 0 < x ∧ x < Suc n)) ri) (conv_cc g) g"
"list_all2 (rel_acconstraint (eq_onp (λx. 0 < x ∧ x < Suc n)) ri)
(conv_cc (inv_of A l)) (inv_of A l)"
"list_all2 (rel_acconstraint (eq_onp (λx. 0 < x ∧ x < Suc n)) ri)
(conv_cc (inv_of A l')) (inv_of A l')"
by (intro * trans_funD[OF ‹(g, a, r, l') ∈ set (trans_fun l)›])+
have [transfer_rule]:
"list_all2 (eq_onp (λx. 0 < x ∧ x < Suc n)) r r"
using trans_funD(5)[OF ‹(g, a, r, l') ∈ set (trans_fun l)›] clock_range
by (auto 4 3 dest: bspec subsetD simp: eq_onp_def list_all2_same)
have "RI2 n (?f g a r l') (?g g a r l')"
by transfer_prover
} then show ?thesis
by (intro rel_funI, clarsimp simp: eq_onp_def)
qed
have [transfer_rule]:
"(eq_onp (λl'. l' = l) ===> list_all2 (eq_onp (λ(g,a,r,l'). (g,a,r,l') ∈ set (trans_fun l))))
trans_fun trans_fun
"
unfolding rel_fun_def eq_onp_def by (auto intro: list.rel_refl_strong)
note [transfer_rule] = dbm_subset_fed_transfer
have [transfer_rule]: "eq_onp (λl'. l' = l) l l" "(eq_onp (λx. x < Suc n)) n n"
by (auto simp: eq_onp_def)
have *: "
(dbm_subset_fed_check n (curry (conv_M M))
(map (λ(g, a, r, l').
down n
(abstr_FW n (conv_cc (inv_of A l))
(abstr_FW n (conv_cc g)
(pre_reset_list n (abstr_FW n (conv_cc (inv_of A l')) V_dbm v) r) v) v))
(trans_fun l))) =
(dbm_subset_fed_upd n M
(map (λ(g, a, r, l').
down_upd n
(abstr_FW_upd n (inv_of A l)
(abstr_FW_upd n g (pre_reset_list_upd1 n (abstr_FW_upd n (inv_of A l') (V_dbm' n)) r))
))
(trans_fun l)))
"
by transfer_prover
text ‹2. Semantic argument establishing equivalences between zones and DBMs›
have **:
"[down n (abstr_FW n (conv_cc (inv_of A l)) (abstr_FW n (conv_cc g)
(pre_reset_list n (abstr_FW n (conv_cc (inv_of A l')) V_dbm v) r) v) v)]⇘v,n⇙
= (zone_set_pre ({u. u ⊢ inv_of (conv_A A) l'} ∩ V) r ∩ {u. ∀ x ∈ set r. u x ≥ 0}
∩ {u. u ⊢ conv_cc g} ∩ {u. u ⊢ inv_of (conv_A A) l})⇧↓ ∩ V"
if "(g, a, r, l') ∈ set(trans_fun l)" for g a r l'
proof -
from trans_funD[OF ‹(g, a, r, l') ∈ set (trans_fun l)›] have clock_conditions:
"∀c∈collect_clks (conv_cc (inv_of A l)). 0 < c ∧ c ≤ n"
"∀c∈collect_clks (conv_cc (inv_of A l')). 0 < c ∧ c ≤ n"
"∀c∈collect_clks (conv_cc g). 0 < c ∧ c ≤ n"
"∀c∈set r. 0 < c ∧ c ≤ n"
using ‹l ∈ states'› clock_range by (auto simp: constraint_clk_conv_cc)
have structural_conditions:
"abstr_FW n (conv_cc (inv_of A l')) V_dbm v 0 0 ≤ 0"
"∀x∈set r. abstr_FW n (map conv_ac (inv_of A l')) V_dbm v 0 x ≤ 0"
subgoal
using abstr_FW_diag_preservation[of n V_dbm "conv_cc (inv_of A l')" v]
by (simp add: V_dbm_def)
subgoal
using ‹∀c∈set r. 0 < c ∧ c ≤ n›
by (auto 4 3 simp: V_dbm_def intro: abstr_FW_mono order.trans)
done
note side_conditions = clock_conditions structural_conditions
abstr_FW_canonical[unfolded canonical'_def] abstr_FW_canonical
show ?thesis
apply (subst dbm.down_correct, rule side_conditions)
apply (subst dbm.abstr_FW_correct, rule side_conditions)
apply (subst dbm.abstr_FW_correct, rule side_conditions)
apply (subst dbm.pre_reset_list_correct, (rule side_conditions)+)
apply (subst dbm.abstr_FW_correct, (rule side_conditions)+)
apply (simp add: inv_of_simp dbm.V_dbm_correct atLeastLessThanSuc_atLeastAtMost Int_commute)
done
qed
have **:
"(⋃x∈set (trans_fun l).
dbm.zone_of
(case x of (g, a, r, l') ⇒
down n
(abstr_FW n (conv_cc (inv_of A l))
(abstr_FW n (conv_cc g)
(pre_reset_list n (abstr_FW n (conv_cc (inv_of A l')) V_dbm v) r) v) v)))
= (⋃(g,a,r,l')∈set (trans_fun l).
((zone_set_pre ({u. u ⊢ inv_of (conv_A A) l'} ∩ V) r ∩ {u. ∀ x ∈ set r. u x ≥ 0}
∩ {u. u ⊢ conv_cc g} ∩ {u. u ⊢ inv_of (conv_A A) l})⇧↓ ∩ V)
)
"
by (auto simp: **)
text ‹3. Putting it all together›
have transD: "∃ g'. (g', a, r, l') ∈ set (trans_fun l) ∧ g = conv_cc g'"
if "conv_A A ⊢ l ⟶⇗g,a,r⇖ l'" for g a r l'
using trans_of_trans_impl[OF _ ‹l ∈ states'›] that
unfolding trans_of_def conv_A_def by (auto 5 0 split: prod.split_asm)
have transD2:
"conv_A A ⊢ l ⟶⇗conv_cc g,a,r⇖ l'" if "(g, a, r, l') ∈ set (trans_fun l)" for g a r l'
using trans_impl_trans_of[OF that ‹l ∈ states'›]
unfolding trans_of_def conv_A_def by (auto 4 3 split: prod.split)
show ?thesis
unfolding TA.check_deadlock_alt_def[OF ‹_ ⊆ V›] check_deadlock_dbm_def inv_of_A_def *[symmetric]
apply (subst dbm.dbm_subset_fed_check_correct[symmetric, OF that(3)])
apply (simp add: **)
apply safe
subgoal for x
by (auto 4 5 elim!: transD[elim_format] dest: subsetD)
subgoal for x
apply (drule subsetD, assumption)
apply clarsimp
subgoal for g a r l'
apply (inst_existentials "
(zone_set_pre ({u. u ⊢ inv_of (conv_A A) l'} ∩ V) r ∩ {u. ∀x∈set r. 0 ≤ u x}
∩ {u. u ⊢ conv_cc g} ∩ {u. u ⊢ inv_of (conv_A A) l})⇧↓ ∩ V" "conv_cc g" a r l')
apply (auto dest: transD2)
done
done
done
qed
lemmas [sepref_fr_rules] =
V_dbm_impl.refine abstr_FW_impl.refine pre_reset_list_impl.refine
down_impl.refine dbm_subset_fed_impl.refine
sepref_definition check_deadlock_impl is
"uncurry (RETURN oo PR_CONST check_deadlock_dbm)" ::
"location_assn⇧k *⇩a (mtx_assn n)⇧d →⇩a bool_assn"
unfolding check_deadlock_dbm_def PR_CONST_def
unfolding case_prod_beta
unfolding map_conv_rev_fold
apply (rewrite "HOL_list.fold_custom_empty")
by sepref
end
subsection ‹Checking a Property on the Reachable Set›
locale Worklist_Map2_Impl_check =
Worklist_Map2_Impl_finite +
fixes Q :: "'a ⇒ bool"
fixes Qi
assumes Q_refine: "(Qi,RETURN o PR_CONST Q) ∈ A⇧d →⇩a bool_assn"
and F_False: "F = (λ _. False)"
and Q_mono: "⋀ a b. a ≼ b ⟹ ¬ empty a ⟹ reachable a ⟹ reachable b ⟹ Q a ⟹ Q b"
begin
definition check_passed :: "bool nres" where
"check_passed = do {
(r, passed) ← pw_algo_map2;
ASSERT (finite (dom passed));
passed ← ran_of_map passed;
r ← nfoldli passed (λb. ¬b)
(λ passed' _.
do {
passed' ← SPEC (λl. set l = passed');
nfoldli passed' (λb. ¬b)
(λv' _.
if Q v' then RETURN True else RETURN False
)
False
}
)
False;
RETURN r
}"
lemma check_passed_correct:
"check_passed ≤ SPEC (λ r. (r ⟷ (∃ a. reachable a ∧ ¬ empty a ∧ Q a)))"
proof -
have [simp]: "F_reachable = False"
unfolding F_reachable_def F_False Search_Space_Defs.F_reachable_def by simp
define outer_inv where "outer_inv passed done todo r ≡
set done ∪ set todo = ran passed ∧
(¬ r ⟶ (∀ S ∈ set done. ∀ x ∈ S. ¬ Q x)) ∧
(r ⟶ (∃ a. reachable a ∧ ¬ empty a ∧ Q a))
" for passed :: "'c ⇒ 'a set option" and "done" todo and r :: bool
define inner_inv where "inner_inv passed done todo r ≡
set done ∪ set todo = passed ∧
(¬ r ⟶ (∀ x ∈ set done. ¬ Q x)) ∧
(r ⟶ (∃ a. reachable a ∧ ¬ empty a ∧ Q a))
" for passed :: "'a set" and "done" todo and r :: bool
show ?thesis
supply [refine_vcg] = pw_algo_map2_correct
unfolding check_passed_def
apply (refine_rcg refine_vcg)
subgoal
by auto
subgoal for _ brk_false passed range_list
apply (rule nfoldli_rule[where I = "outer_inv passed"])
subgoal
unfolding outer_inv_def
by auto
apply (refine_rcg refine_vcg)
subgoal for current "done" todo r xs
apply clarsimp
apply (rule nfoldli_rule[where I = "inner_inv current"])
subgoal
unfolding inner_inv_def
by auto
subgoal for p x l1 l2 r'
by (clarsimp simp: inner_inv_def outer_inv_def map_set_rel_def)
(metis Sup_insert Un_insert_left insert_iff subset_Collect_conv)
subgoal for p l1 l2 r'
unfolding inner_inv_def outer_inv_def
by (metis append.assoc append_Cons append_Nil set_append)
subgoal for p r'
unfolding inner_inv_def outer_inv_def
by clarsimp
done
subgoal for l1 l2 r
unfolding outer_inv_def
by auto
subgoal for r
unfolding outer_inv_def
apply clarsimp
apply (elim allE impE)
apply (intro conjI; assumption)
apply safe
apply (drule Q_mono, assumption+)
unfolding map_set_rel_def
by auto
done
done
qed
schematic_goal pw_algo_map2_refine:
"(?x, uncurry0 (PR_CONST pw_algo_map2)) ∈
unit_assn⇧k →⇩a bool_assn ×⇩a hm.hms_assn' K (lso_assn A)"
unfolding PR_CONST_def hm.hms_assn'_id_hms_assn[symmetric] by (rule pw_algo_map2_impl.refine_raw)
sepref_register pw_algo_map2
sepref_register "PR_CONST Q"
sepref_thm check_passed_impl is
"uncurry0 check_passed" :: "unit_assn⇧k →⇩a bool_assn"
supply [sepref_fr_rules] = pw_algo_map2_refine ran_of_map_impl.refine lso_id_hnr Q_refine
using pure_K left_unique_K right_unique_K
unfolding check_passed_def
apply (rewrite in Q PR_CONST_def[symmetric])
unfolding hm.hms_fold_custom_empty
unfolding list_of_set_def[symmetric]
by sepref
concrete_definition (in -) check_passed_impl
uses Worklist_Map2_Impl_check.check_passed_impl.refine_raw is "(uncurry0 ?f,_)∈_"
lemma check_passed_impl_hnr:
"(uncurry0 (check_passed_impl succsi a⇩0i Fi Lei emptyi keyi copyi tracei Qi),
uncurry0 (RETURN (∃a. reachable a ∧ ¬ empty a ∧ Q a)))
∈ unit_assn⇧k →⇩a bool_assn"
using
check_passed_impl.refine[
OF Worklist_Map2_Impl_check_axioms,
FCOMP check_passed_correct[THEN Id_SPEC_refine, THEN nres_relI]
]
by (simp add: RETURN_def)
end
subsection ‹Complete Deadlock Checker›
paragraph ‹Miscellaneous Properties›
context E_From_Op_Bisim
begin
text ‹More general variant of @{thm E_from_op_reachability_check} *)›
theorem E_from_op_reachability_check:
assumes "⋀a b. P a ⟹ a ∼ b ⟹ wf_state a ⟹ wf_state b ⟹ P b"
shows
"(∃l' D'. E⇧*⇧* a⇩0 (l', D') ∧ P (l', D')) ⟷ (∃l' D'. E_from_op⇧*⇧* a⇩0 (l', D') ∧ P (l', D'))"
by (rule E_E⇩1_steps_equiv[OF E_E_from_op_step E_from_op_E_step E_from_op_wf_state];
(assumption | rule assms))
end
context Regions_TA
begin
lemma check_deadlock_anti_mono:
"check_deadlock l Z" if "check_deadlock l Z'" "Z ⊆ Z'"
using that unfolding check_deadlock_def by auto
lemma global_clock_numbering:
"global_clock_numbering A v n"
using valid_abstraction clock_numbering_le clock_numbering by blast
text ‹Variant of @{thm bisim} without emptiness.›
lemma bisim:
"Bisimulation_Invariant
(λ (l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩)
(λ (l, D) (l', D'). ∃ a. A ⊢' ⟨l, D⟩ ↝⇘𝒩(a)⇙ ⟨l', D'⟩)
(λ (l, Z) (l', D). l = l' ∧ Z = [D]⇘v,n⇙)
(λ _. True) (λ (l, D). valid_dbm D)"
proof (standard, goal_cases)
case (1 a b a')
then show ?case
by (blast elim: norm_beta_complete1[OF global_clock_numbering valid_abstraction])
next
case (2 a a' b')
then show ?case
by (blast intro: norm_beta_sound''[OF global_clock_numbering valid_abstraction])
next
case (3 a b)
then show ?case
by simp
next
case (4 a b)
then show ?case
by (auto intro: valid_dbm_step_z_norm''[OF global_clock_numbering valid_abstraction])
qed
lemma steps_z_beta_reaches:
"reaches (l, Z) (l', Z')" if "A ⊢ ⟨l, Z⟩ ↝⇩β* ⟨l', Z'⟩" "Z' ≠ {}"
using that
proof (induction "(l', Z')" arbitrary: l' Z' rule: rtranclp_induct)
case base
then show ?case
by blast
next
case (step y l'' Z'')
obtain l' Z' where [simp]: "y = (l', Z')"
by force
from step.prems step.hyps(2) have "Z' ≠ {}"
by (clarsimp simp: step_z_beta'_empty)
from step.prems step.hyps(3)[OF ‹y = _› this] step.hyps(2) show ?case
including graph_automation_aggressive by auto
qed
lemma reaches_steps_z_beta_iff:
"reaches (l, Z) (l', Z') ⟷ A ⊢ ⟨l, Z⟩ ↝⇩β* ⟨l', Z'⟩ ∧ Z' ≠ {}" if "Z ≠ {}"
apply safe
subgoal
including graph_automation_aggressive by (induction rule: rtranclp_induct) auto
using that by (auto dest: steps_z_beta_reaches elim: rtranclp.cases)
end
lemma dbm_int_init_dbm:
"dbm_int (curry init_dbm) n"
unfolding init_dbm_def by auto
context TA_Start
begin
lemma wf_dbm_canonical'D:
"Deadlock.canonical' n (curry (conv_M D))" if "wf_dbm D"
using that unfolding wf_dbm_def Deadlock.canonical'_def check_diag_conv_M_iff by simp
lemma subsumes_dbm_subsetD:
"dbm_subset n M M'" if "subsumes n (l, M) (l', M')" "¬ check_diag n M"
using that by (cases "l = l'") (auto simp: subsumes_simp_1 subsumes_simp_2)
lemma subsumes_loc_eqD:
"l = l'" if "subsumes n (l, M) (l', M')" "¬ check_diag n M"
using that by (cases "l = l'") (auto simp: subsumes_simp_1 subsumes_simp_2)
lemma init_dbm_zone:
"[curry (init_dbm :: real DBM')]⇘v,n⇙ = {u. ∀c∈{1..n}. u c = 0}"
using init_dbm_semantics by blast
lemma not_check_deadlock_mono:
"(case a of (l, M) ⇒ ¬ TA.check_deadlock l (dbm.zone_of (curry (conv_M M)))) ⟹
a ∼ b ⟹ wf_state a ⟹ wf_state b ⟹
case b of (l, M) ⇒ ¬ TA.check_deadlock l (dbm.zone_of (curry (conv_M M)))"
unfolding TA.check_deadlock_def state_equiv_def dbm_equiv_def by auto
lemma not_check_deadlock_non_empty:
"Z ≠ {}" if "¬ TA.check_deadlock l Z"
using that unfolding TA.check_deadlock_def by auto
end
context TA_Impl
begin
lemma op_E_from_op_iff:
"op.E_from_op = E_op''.E_from_op"
unfolding PR_CONST_def ..
lemmas reachable_states = reachable_states[unfolded op_E_from_op_iff]
lemma E_op''_states:
"l' ∈ states" if "E_op''.E_from_op (l, M) (l', M')" "l ∈ states"
using that by (force simp: a⇩0_def state_set_def E_op''.E_from_op_def)
subsubsection ‹Instantiating the Checker Algorithm›
corollary check_deadlock_dbm_correct':
assumes "l ∈ states'" "wf_state (l, M)"
shows "TA.check_deadlock l (dbm.zone_of (curry (conv_M M))) = check_deadlock_dbm l M"
apply (rule check_deadlock_dbm_correct)
using assms
unfolding wf_state_def Deadlock.canonical'_def prod.case
apply (blast dest: wf_dbm_altD)
apply (rule assms)
using assms
unfolding wf_state_def Deadlock.canonical'_def prod.case
apply -
apply (drule wf_dbm_altD(1))
unfolding canonical'_conv_M_iff check_diag_conv_M_iff by simp
corollary check_deadlock_dbm_correct'':
assumes "E_op''.E_from_op⇧*⇧* a⇩0 (l, M)"
shows "TA.check_deadlock l (dbm.zone_of (curry (conv_M M))) = check_deadlock_dbm l M"
using assms
apply -
apply (rule check_deadlock_dbm_correct')
apply (drule reachable_states, use states'_states in auto; fail)
unfolding wf_state_def prod.case apply (erule E_op''.reachable_wf_dbm)
done
lemma not_check_deadlock_non_empty:
"Z ≠ {}" if "¬ TA.check_deadlock l Z"
using that unfolding TA.check_deadlock_def by auto
sepref_register check_deadlock_dbm :: "'s ⇒ int DBMEntry i_mtx ⇒ bool"
sepref_definition check_deadlock_neg_impl is
"RETURN o (λ(l, M). ¬ check_deadlock_dbm l M)" :: "(location_assn ×⇩a (mtx_assn n))⇧d →⇩a bool_assn"
supply [sepref_fr_rules] = check_deadlock_impl.refine
by sepref
lemma not_check_deadlock_compatible:
assumes
"(case a of (l, Z) ⇒ λ(l', D'). l' = l ∧ dbm.zone_of (curry (conv_M D')) = Z) b"
"case b of (l, M) ⇒ l ∈ states' ∧ wf_state (l, M)"
shows
"(case a of (l, Z) ⇒ ¬ TA.check_deadlock l Z) = (case b of (l, M) ⇒ ¬ check_deadlock_dbm l M)"
using assms by (auto simp: check_deadlock_dbm_correct'[symmetric])
lemma deadlock_check_diag:
"¬ check_diag n M" if "¬ check_deadlock_dbm l M" "E_op''.E_from_op⇧*⇧* a⇩0 (l, M)"
using that(1)
apply (subst (asm) check_deadlock_dbm_correct'[symmetric])
subgoal
using reachable_states that(2) states'_states by auto
subgoal
unfolding wf_state_def using E_op''.reachable_wf_dbm[OF that(2)] by simp
using canonical_check_diag_empty_iff by (blast dest: not_check_deadlock_non_empty)
lemma norm_final_bisim:
"Bisimulation_Invariant
(λ(l, D) (l', D'). ∃a. step_z_norm'' (conv_A A) l D a l' D')
E_op''.E_from_op
(λ (l, M) (l', D'). l' = l ∧ [curry (conv_M D')]⇘v,n⇙ = [M]⇘v,n⇙)
(λ(l, y). valid_dbm y) wf_state"
by (rule
Bisimulation_Invariant_sim_replace[OF
Bisimulation_Invariant_composition[OF
step_z_norm''_step_impl'_equiv[unfolded step_impl'_E] E_op''.E_from_op_bisim
]
])
(auto simp add: state_equiv_def dbm_equiv_def)
interpretation bisim:
Bisimulation_Invariant
"λ(l, Z) (l', Z'). step_z_beta' (conv_A A) l Z l' Z'"
"λa b. op.E_from_op a b"
"λ(l, Z) (l', D'). l' = l ∧ [curry (conv_M D')]⇘v,n⇙ = Z"
"λ_. True" "λ(l, M). l ∈ states ∧ wf_state (l, M)"
unfolding op_E_from_op_iff
by (rule Bisimulation_Invariant_strengthen_post',
(rule Bisimulation_Invariant_composition[OF TA.bisim norm_final_bisim]
Bisimulation_Invariant_sim_replace
)+) (auto 4 3 dest: E_op''_states wf_dbm_D(3) simp: wf_state_def)
lemmas beta_final_bisim = bisim.Bisimulation_Invariant_axioms
definition
"is_start_in_states = (trans_fun l⇩0 ≠ [])"
lemma is_start_in_states:
"l⇩0 ∈ Simulation_Graphs_TA.state_set A" if "is_start_in_states"
proof -
from that obtain g a r l' where "(g, a, r, l') ∈ set (trans_fun l⇩0)"
by (cases "hd (trans_fun l⇩0)" rule: prod_cases4)
(auto dest: hd_in_set simp: is_start_in_states_def)
from trans_impl_trans_of[OF this] states'_states have "A ⊢ l⇩0 ⟶⇗g,a,r⇖ l'"
by simp
then show ?thesis
unfolding Simulation_Graphs_TA.state_set_def trans_of_def by auto
qed
lemma deadlocked_if_not_is_start_in_states:
"deadlocked (l⇩0, Z⇩0)" if "¬ is_start_in_states"
proof -
have *: False if "A ⊢ l⇩0 ⟶⇗g,a,r⇖ l'" for g a r l'
using trans_of_trans_impl[OF that] ‹¬ _› states'_states unfolding is_start_in_states_def by auto
{ fix l g2 a2 r2 l' assume A: "conv_A A ⊢ l ⟶⇗g2,a2,r2⇖ l'"
obtain g1 a1 r1 where **: "A ⊢ l ⟶⇗g1,a1,r1⇖ l'"
using A unfolding trans_of_def conv_A_def by (cases A) force
then have "∃ g1 a1 r1. A ⊢ l ⟶⇗g1,a1,r1⇖ l'"
by auto
} note ** = this
show ?thesis
unfolding deadlocked_def
apply (rule ccontr)
apply clarsimp
apply (cases rule: step'.cases, assumption)
apply (cases rule: step_a.cases, assumption)
apply (auto 4 3 elim: * dest: ** step_delay_loc)
done
qed
lemma deadlock_if_not_is_start_in_states:
"deadlock (l⇩0, Z⇩0)" if "¬ is_start_in_states"
unfolding deadlock_def using deadlocked_if_not_is_start_in_states[OF that] by blast
sepref_definition is_start_in_states_impl is
"uncurry0 (RETURN is_start_in_states)" :: "unit_assn⇧k →⇩a bool_assn"
unfolding is_start_in_states_def by sepref
text ‹Turning this into a Hoare triple:›
thm is_start_in_states_impl.refine[to_hnr, unfolded hn_refine_def, simplified]
lemma is_start_in_states_impl_hoare:
"<emp> is_start_in_states_impl
<λr. ↑ ((r ⟶ l⇩0 ∈ Simulation_Graphs_TA.state_set A)
∧ (¬r ⟶ deadlocked (l⇩0, λ_ . 0))
)>⇩t"
by (sep_auto
intro: deadlocked_if_not_is_start_in_states
simp: mod_star_conv is_start_in_states[simplified]
heap: is_start_in_states_impl.refine[to_hnr, unfolded hn_refine_def, simplified]
)
lemma deadlock_if_deadlocked:
"deadlock y" if "deadlocked y"
using that unfolding deadlock_def by (inst_existentials y) auto
lemma is_start_in_states_impl_hoare':
"<emp> is_start_in_states_impl
<λr. ↑ ((r ⟶ l⇩0 ∈ Simulation_Graphs_TA.state_set A)
∧ (¬r ⟶ (∃u⇩0. (∀c∈{1..n}. u⇩0 c = 0) ∧ deadlock (l⇩0, u⇩0)))
)>⇩t"
by (rule cons_post_rule[OF is_start_in_states_impl_hoare]) (auto intro: deadlock_if_deadlocked)
end
context Reachability_Problem_Impl
begin
context
assumes l⇩0_in_A: "l⇩0 ∈ Simulation_Graphs_TA.state_set A"
begin
interpretation TA:
Regions_TA_Start_State v n "Suc n" "{1..<Suc n}" k "conv_A A" l⇩0 "{u. ∀c∈{1..n}. u c = 0}"
apply standard
subgoal
by (intro l⇩0_state_set l⇩0_in_A)
subgoal
unfolding V'_def
apply safe
subgoal for x
unfolding V_def by auto
apply (inst_existentials "curry init_dbm :: real DBM")
apply (simp add: init_dbm_zone)
by (rule dbm_int_init_dbm)
subgoal
by auto
done
interpretation bisim:
Bisimulation_Invariant
"λ(l, Z) (l', Z'). step_z_beta' (conv_A A) l Z l' Z'"
"λa b. op.E_from_op a b"
"λ(l, Z) (l', D'). l' = l ∧ [curry (conv_M D')]⇘v,n⇙ = Z"
"λ_. True" "λ(l, M). l ∈ states ∧ wf_state (l, M)"
by (rule beta_final_bisim)
lemma check_deadlock:
"(∃a. E_op''.E_from_op⇧*⇧* a⇩0 a ∧
¬ (case a of (l, M) ⇒ check_diag n M) ∧ (case a of (l, M) ⇒ ¬ check_deadlock_dbm l M))
⟷ (∃u⇩0. (∀c ∈ {1..n}. u⇩0 c = 0) ∧ deadlock (l⇩0, u⇩0))" (is "?l ⟷ ?r")
proof -
text ‹@{term TA.reaches} corresponds to non-empty steps of @{term step_z_beta'}›
text ‹@{term bisim.A.reaches} corresponds to steps of @{term step_z_beta'}›
text ‹@{term ‹E_op''.E_from_op⇧*⇧* a⇩0›} corresponds to steps of @{term op.E_from_op} (@{term E_op''})›
have "?r ⟷ (∃l Z. TA.reaches (l⇩0, {u. ∀c∈{1..n}. u c = 0}) (l, Z) ∧ ¬TA.check_deadlock l Z)"
using TA.deadlock_check unfolding TA.a⇩0_def from_R_def by simp
also have
"… ⟷ (∃l Z. bisim.A.reaches (l⇩0, {u. ∀c∈{1..n}. u c = 0}) (l, Z) ∧ ¬TA.check_deadlock l Z)"
apply safe
subgoal for l Z
by (subst (asm) TA.reaches_steps_z_beta_iff) auto
subgoal for l Z
by (subst TA.reaches_steps_z_beta_iff) (auto dest: not_check_deadlock_non_empty)
done
also have "… ⟷ (∃l M. E_op''.E_from_op⇧*⇧* a⇩0 (l, M) ∧ ¬ check_deadlock_dbm l M)"
using bisim.reaches_ex_iff[where
φ = "λ (l, Z). ¬TA.check_deadlock l Z" and ψ = "λ(l, M). ¬ check_deadlock_dbm l M",
OF not_check_deadlock_compatible, of "(l⇩0, {u. ∀c∈{1..n}. u c = 0})" a⇩0
]
using wf_state_init init_dbm_zone states'_states unfolding a⇩0_def by force
also have "… ⟷ ?l"
by (auto 4 4 dest: deadlock_check_diag)
finally show ?thesis ..
qed
lemma check_deadlock':
"(∄a. E_op''.E_from_op⇧*⇧* a⇩0 a ∧
¬ (case a of (l, M) ⇒ check_diag n M) ∧ (case a of (l, M) ⇒ ¬ check_deadlock_dbm l M))
⟷ (∀u⇩0. (∀c ∈ {1..n}. u⇩0 c = 0) ⟶ ¬ deadlock (l⇩0, u⇩0))" (is "?l ⟷ ?r")
using check_deadlock by auto
context
assumes "F = (λ _. False)"
begin
interpretation Worklist_Map2_Impl_check
op.E_from_op a⇩0 F_rel "subsumes n" succs "λ (l, M). check_diag n M" subsumes'
"λ (l, M). F l" state_assn'
succs_impl a⇩0_impl F_impl subsumes_impl emptiness_check_impl fst "return o fst" state_copy_impl
tracei location_assn "λ(l, M). ¬ check_deadlock_dbm l M" check_deadlock_neg_impl
apply standard
subgoal
using check_deadlock_neg_impl.refine unfolding PR_CONST_def .
subgoal
unfolding F_rel_def unfolding ‹F = _› by auto
subgoal for a b
apply (clarsimp simp: E_op''.reachable_def)
apply (subst (asm) check_deadlock_dbm_correct''[symmetric], assumption)
apply (subst (asm) check_deadlock_dbm_correct''[symmetric], assumption)
apply (frule subsumes_loc_eqD, assumption)
apply (drule subsumes_dbm_subsetD, assumption)
apply (drule dbm_subset_conv)
apply (subst (asm) dbm_subset_correct''[symmetric])
by (auto dest: TA.check_deadlock_anti_mono E_op''.reachable_wf_dbm simp: E_op''.reachable_def)
done
lemmas check_passed_impl_hnr =
check_passed_impl_hnr[unfolded op.reachable_def, unfolded op_E_from_op_iff check_deadlock]
end
end
definition
"check_passed_impl_start ≡ do {
r1 ← is_start_in_states_impl;
if r1 then do {
r2 ← check_passed_impl succs_impl a⇩0_impl F_impl subsumes_impl emptiness_check_impl
(return ∘ fst) state_copy_impl tracei check_deadlock_neg_impl;
return r2
}
else return True
}"
lemma check_passed_impl_start_hnr:
"(uncurry0 check_passed_impl_start,
uncurry0 (RETURN (∃u⇩0. (∀c∈{1..n}. u⇩0 c = 0) ∧ deadlock (l⇩0, u⇩0)))
) ∈ unit_assn⇧k →⇩a bool_assn" if "F = (λ_. False)"
proof -
define has_deadlock where "has_deadlock ≡ ∃u⇩0. (∀c∈{1..n}. u⇩0 c = 0) ∧ deadlock (l⇩0, u⇩0)"
note [sep_heap_rules] =
check_passed_impl_hnr[
OF _ that, to_hnr, unfolded hn_refine_def, folded has_deadlock_def, simplified
]
is_start_in_states_impl_hoare'[folded has_deadlock_def, simplified]
show ?thesis
unfolding has_deadlock_def[symmetric] check_passed_impl_start_def
by sepref_to_hoare (sep_auto simp: mod_star_conv)
qed
end
context Reachability_Problem_precompiled
begin
lemma F_is_False_iff:
"PR_CONST F = (λ_. False) ⟷ final = []"
unfolding F_def by (cases final; simp; metis)
lemma F_impl_False: "F_impl = (λ_. return False)" if "final = []"
using that unfolding F_impl_def unfolding final_fun_def List.member_def by auto
definition deadlock_checker where
"deadlock_checker ≡
let
key = return ∘ fst;
sub = subsumes_impl;
copy = state_copy_impl;
start = a⇩0_impl;
final = (λ_. return False);
succs = succs_impl;
empty = emptiness_check_impl;
P = check_deadlock_neg_impl;
trace = tracei
in do {
r1 ← is_start_in_states_impl;
if r1 then do {
r2 ← check_passed_impl succs start final sub empty key copy trace P;
return r2
}
else return True
}"
theorem deadlock_checker_hnr:
assumes "final = []"
shows
"(uncurry0 deadlock_checker, uncurry0 (RETURN (∃u⇩0. (∀c∈{1..m}. u⇩0 c = 0) ∧ deadlock (0, u⇩0))))
∈ unit_assn⇧k →⇩a bool_assn"
unfolding deadlock_checker_def Let_def
using check_passed_impl_start_hnr[
unfolded F_is_False_iff F_impl_False[OF assms] check_passed_impl_start_def,
OF assms] .
schematic_goal deadlock_checker_alt_def:
"deadlock_checker ≡ ?impl"
unfolding deadlock_checker_def
unfolding succs_impl_def
unfolding E_op''_impl_def abstr_repair_impl_def abstra_repair_impl_def
unfolding start_inv_check_impl_def unbounded_dbm_impl_def unbounded_dbm'_def
unfolding check_deadlock_neg_impl_def check_deadlock_impl_def
unfolding is_start_in_states_impl_def
apply (abstract_let "IArray.sub (IArray (map (IArray o map int) k))" k)
apply (abstract_let "inv_fun" inv_fun)
apply (abstract_let "trans_impl" trans)
unfolding inv_fun_def[abs_def] trans_impl_def[abs_def]
apply (abstract_let "IArray inv" inv_ia)
apply (abstract_let "IArray trans_map" trans_map)
unfolding trans_map_def label_def
unfolding init_dbm_impl_def a⇩0_impl_def
unfolding subsumes_impl_def
unfolding emptiness_check_impl_def
unfolding state_copy_impl_def
by (rule Pure.reflexive)
end
concrete_definition deadlock_checker_impl
uses Reachability_Problem_precompiled.deadlock_checker_alt_def
export_code deadlock_checker_impl in SML_imp module_name TA
definition [code]:
"check_deadlock n m k I T ≡
if Reachability_Problem_precompiled n m k I T
then deadlock_checker_impl m k I T ⤜ (λx. return (Some x))
else return None"
theorem deadlock_check:
"(uncurry0 (check_deadlock n m k I T),
uncurry0 (
RETURN (
if (Reachability_Problem_precompiled n m k I T)
then Some (
if
∃ u⇩0. (∀ c ∈ {1..m}. u⇩0 c = 0) ∧
Graph_Defs.deadlock
(λ(l, u) (l', u').
(conv_A (Reachability_Problem_precompiled_defs.A n I T)) ⊢' ⟨l, u⟩ → ⟨l', u'⟩)
(0, u⇩0)
then True
else False
)
else None
)
)
) ∈ unit_assn⇧k →⇩a id_assn"
proof -
define reach_check where
"reach_check =
(∃ u⇩0. (∀ c ∈ {1..m}. u⇩0 c = 0) ∧
Graph_Defs.deadlock
(λ(l, u) (l', u').
(conv_A (Reachability_Problem_precompiled_defs.A n I T)) ⊢' ⟨l, u⟩ → ⟨l', u'⟩)
(0, u⇩0))"
note [sep_heap_rules] = Reachability_Problem_precompiled.deadlock_checker_hnr[OF _ HOL.refl,
to_hnr, unfolded hn_refine_def, rule_format,
of n m k I T,
unfolded reach_check_def[symmetric]
]
show ?thesis
unfolding reach_check_def[symmetric]
by sepref_to_hoare
(sep_auto simp: deadlock_checker_impl.refine[symmetric] mod_star_conv check_deadlock_def)
qed
end