Theory Simple_Network_Language_Certificate_Checking
section ‹A Verified Certificate Checker for the Simple Networks Lanuage›
theory Simple_Network_Language_Certificate_Checking
imports
Extract_Certificate
Normalized_Zone_Semantics_Certification_Impl
Munta_Model_Checker.Simple_Network_Language_Export_Code
Munta_Base.Trace_Timing
begin
unbundle no_library_syntax
notation fun_rel_syn (infixr "→" 60)
no_notation Omega_Words_Fun.build (infixr ‹##› 65)
no_notation Assertions.models (infix "⊨" 50)
paragraph ‹Misc›
lemma list_set_rel_singleton_iff:
"([a], {b}) ∈ ⟨R⟩list_set_rel ⟷ (a, b) ∈ R"
unfolding list_set_rel_def relcomp.simps by (auto simp: list_all2_Cons1 list_rel_def)
definition (in Graph_Defs)
"alw_ev φ x ≡ ∀xs. run (x ## xs) ⟶ alw (ev (holds φ)) (x ## xs)"
lemma (in Graph_Defs) alw_ev_to_ctl_star:
"alw_ev φ x ⟷ models_state (All (G (F (State (PropS φ))))) x"
unfolding alw_ev_def by (simp add: models_state.simps[abs_def])
context Simple_Network_Rename_Formula
begin
lemma buechi_models_state_compatible:
assumes "Φ = formula.EX φ"
shows
"Graph_Defs.models_state
(λ (L, s, u) (L', s', u'). rename.renum.sem ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩)
(map_state_formula (λφ (L, s, _).
check_sexp (map_sexp (λp. renum_states p) renum_vars id φ) L (the o s))
(All (G (F (State (PropS φ))))))
a⇩0'
⟷ Graph_Defs.models_state
(λ (L, s, u) (L', s', u'). sem ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩)
(map_state_formula (λφ (L, s, _). check_sexp φ L (the o s)) (All (G (F (State (PropS φ))))))
a⇩0" (is "Graph_Defs.models_state _ ?φ _ ⟷ _")
proof -
have "?φ = map_state_formula
(λP (L, s, _).
check_sexp
(map_sexp (λp. extend_bij (renum_states p) loc_set) (extend_bij renum_vars var_set) id P)
L (the ∘ s))
(All (G (F (State (PropS φ)))))"
using assms formula_dom by (auto simp: sexp_eq)
show ?thesis
unfolding a⇩0_def a⇩0'_def ‹?φ = _› using assms formula_dom
by - (rule sym, rule models_state_compatible, auto)
qed
lemma buechi_compatible:
assumes "Φ = formula.EX φ"
shows
"Graph_Defs.alw_ev
(λ (L, s, u) (L', s', u'). rename.renum.sem ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩)
(λ (L, s, _). check_sexp (map_sexp (λp. renum_states p) renum_vars id φ) L (the o s)) a⇩0'
⟷ Graph_Defs.alw_ev
(λ (L, s, u) (L', s', u'). sem ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩)
(λ (L, s, _). check_sexp φ L (the o s)) a⇩0"
using buechi_models_state_compatible[OF assms] unfolding Graph_Defs.alw_ev_to_ctl_star by simp
lemmas buechi_compatible' =
buechi_compatible[unfolded rename_N_eq_sem, folded N_eq_sem, unfolded a⇩0_def a⇩0'_def Φ'_def]
end
lemma stream_all2_flip:
assumes "stream_all2 R xs ys"
shows "stream_all2 (λy x. R x y) ys xs"
using assms by (coinduction arbitrary: xs ys) auto
lemma (in Bisimulation_Invariant) alw_ev_iff:
fixes φ :: "'a ⇒ bool" and ψ :: "'b ⇒ bool"
assumes compatible: "⋀a b. A_B.equiv' a b ⟹ φ a ⟷ ψ b"
and that: "A_B.equiv' a b"
shows "A.alw_ev φ a ⟷ B.alw_ev ψ b"
unfolding Graph_Defs.alw_ev_def
apply safe
subgoal
using that
by - (
drule B_A.simulation_run,
auto simp: compatible intro: equiv'_rotate_1 dest!: equiv'_rotate_2
elim!: alw_ev_lockstep stream_all2_flip)
subgoal for xs
using that
by - (
drule A_B.simulation_run,
auto simp: compatible intro: equiv'_rotate_2 elim!: alw_ev_lockstep stream_all2_flip)
done
paragraph ‹Splitters›
context
fixes f :: "'a ⇒ nat" and width :: nat
begin
fun split_size :: "nat ⇒ 'a list ⇒ 'a list ⇒ 'a list list" where
"split_size _ acc [] = [acc]"
| "split_size n acc (x # xs) =
(let k = f x in if n < width then split_size (n + k) (x # acc) xs else acc # split_size k [x] xs)"
lemma split_size_full_split:
"(⋃x ∈ set (split_size n acc xs). set x) = set xs ∪ set acc"
by (induction n acc xs rule: split_size.induct) auto
end
definition split_eq_width :: "nat ⇒ 'a list ⇒ 'a list list" where
"split_eq_width n ≡ split_size (λ_. 1 :: nat) n 0 []"
lemma list_all2_split_size_1:
assumes "list_all2 R xs ys" "list_all2 R acc acc'"
shows "list_all2 (list_all2 R)
(split_size (λ_. 1 :: nat) k n acc xs) (split_size (λ_. 1 :: nat) k n acc' ys)"
using assms by (induction arbitrary: acc acc' n rule: list_all2_induct) auto
fun zip2 where
"zip2 [] [] = []"
| "zip2 [] xs = []"
| "zip2 ys [] = []"
| "zip2 (x # xs) (y # ys) = (x, y) # zip2 xs ys"
lemma length_hd_split_size_mono:
"length (hd (split_size f k n acc xs)) ≥ length acc"
apply (induction xs arbitrary: acc n)
apply (solves auto)
apply clarsimp
apply (rule order.trans[rotated])
apply rprems
apply simp
done
lemma split_size_non_empty[simp]:
"split_size f k n acc xs = [] ⟷ False"
by (induction xs arbitrary: acc n) auto
lemma list_all2_split_size_2:
assumes "length acc = length acc'"
shows
"list_all2 (list_all2 R)
(split_size (λ_. 1 :: nat) k n acc xs) (split_size (λ_. 1 :: nat) k n acc' ys)
⟷ list_all2 R xs ys ∧ list_all2 R acc acc'"
using assms
proof (induction xs ys arbitrary: acc acc' n rule: zip2.induct)
case (2 y ys)
{ assume A: "list_all2 (list_all2 R) [acc] (split_size (λ_. Suc 0) k (Suc n) (y # acc') ys)"
then obtain x where "split_size (λ_. Suc 0) k (Suc n) (y # acc') ys = [x]"
by (cases "split_size (λ_. Suc 0) k (Suc n) (y # acc') ys") auto
with length_hd_split_size_mono[of "y # acc'" "(λ_. Suc 0)" k "Suc n" ys] have
"length x ≥ length (y # acc')"
by auto
with A ‹_ = [x]› ‹length acc = length acc'› have False
by (auto dest: list_all2_lengthD)
}
with 2 show ?case
by clarsimp
next
case (3 y ys)
{ assume A: "list_all2 (list_all2 R) (split_size (λ_. Suc 0) k (Suc n) (y # acc) ys) [acc']"
then obtain x where "split_size (λ_. Suc 0) k (Suc n) (y # acc) ys = [x]"
by (cases "split_size (λ_. Suc 0) k (Suc n) (y # acc) ys") auto
with length_hd_split_size_mono[of "y # acc" "(λ_. Suc 0)" k "Suc n" ys] have
"length x ≥ length (y # acc)"
by auto
with A ‹_ = [x]› ‹length acc = length acc'› have False
by (auto dest: list_all2_lengthD)
}
with 3 show ?case
by clarsimp
qed auto
lemma list_all2_split_eq_width:
shows "list_all2 R xs ys ⟷ list_all2 (list_all2 R) (split_eq_width k xs) (split_eq_width k ys)"
unfolding split_eq_width_def by (subst list_all2_split_size_2; simp)
lemma length_split_size_1:
"sum_list (map length (split_size (λ_. 1 :: nat) k n acc xs)) = length xs + length acc"
by (induction xs arbitrary: acc n) auto
lemma length_sum_list:
"sum_list (map length (split_eq_width k xs)) = length xs"
unfolding split_eq_width_def by (subst length_split_size_1; simp)
definition split_k :: "nat ⇒ 'a list ⇒ 'a list list" where
"split_k k xs ≡ let
width = length xs div k;
width = (if length xs mod k = 0 then width else width + 1)
in split_eq_width width xs"
lemma length_hd_split_size:
"length (hd (split_size (λ_. 1 :: nat) k n acc xs))
= (if n + length xs < k then n + length xs else max k n)" if "length acc = n"
using that by (induction xs arbitrary: n acc) auto
lemma length_hd_split_eq_width:
"length (hd (split_eq_width width xs)) = (if length xs < width then length xs else width)"
unfolding split_eq_width_def by (subst length_hd_split_size; simp)
lemma list_all2_split_k:
"list_all2 R xs ys ⟷ list_all2 (list_all2 R) (split_k k xs) (split_k k ys)"
proof (cases "length xs = length ys")
case True
show ?thesis
unfolding split_k_def Let_def True by (rule list_all2_split_eq_width)
next
case False
{ assume "list_all2 (list_all2 R) (split_k k xs) (split_k k ys)"
then have "list_all2 R (concat (split_k k xs)) (concat (split_k k ys))"
by (meson concat_transfer rel_funD)
then have "length (concat (split_k k xs)) = length (concat (split_k k ys))"
by (rule list_all2_lengthD)
then have "length xs = length ys"
unfolding split_k_def by (simp add: length_concat length_sum_list)
}
with False show ?thesis
by (auto dest: list_all2_lengthD)
qed
definition split_k' :: "nat ⇒ ('a × 'b list) list ⇒ 'a list list" where
"split_k' k xs ≡ let
width = sum_list (map (length o snd) xs) div k;
width = (if length xs mod k = 0 then width else width + 1)
in map (map fst) (split_size (length o snd) width 0 [] xs)"
lemma split_eq_width_full_split:
"set xs = (⋃x ∈ set (split_eq_width n xs). set x)"
unfolding split_eq_width_def by (auto simp add: split_size_full_split)
lemma split_k_full_split:
"set xs = (⋃x ∈ set (split_k n xs). set x)"
unfolding split_k_def by (simp add: split_eq_width_full_split)
lemma split_k'_full_split:
"fst ` set xs = (⋃x ∈ set (split_k' n xs). set x)"
unfolding split_k'_def by (simp add: split_size_full_split image_UN[symmetric])
lemma (in Graph_Defs) Ex_ev_reaches:
"∃ y. x →* y ∧ φ y" if "Ex_ev φ x"
using that unfolding Ex_ev_def
proof safe
fix xs assume prems: "run (x ## xs)" "ev (holds φ) (x ## xs)"
show "∃y. x →* y ∧ φ y"
proof (cases "φ x")
case True
then show ?thesis
by auto
next
case False
with prems obtain y ys zs where
"φ y" "xs = ys @- y ## zs" "y ∉ set ys"
unfolding ev_holds_sset by (auto elim!:split_stream_first')
with prems have "steps (x # ys @ [y])"
by (auto intro: run_decomp[THEN conjunct1])
with ‹φ y› show ?thesis
including graph_automation by (auto 4 3)
qed
qed
text ‹More debugging auxiliaries›
concrete_definition (in -) M_table
uses Reachability_Problem_Impl_Precise.M_table_def
definition
"check_nonneg n M ≡ imp_for 0 (n + 1) Heap_Monad.return
(λxc σ. mtx_get (Suc n) M (0, xc) ⤜ (λx'e. Heap_Monad.return (x'e ≤ Le 0))) True"
definition
"check_diag_nonpos n M ≡ imp_for 0 (n + 1) Heap_Monad.return
(λxc σ. mtx_get (Suc n) M (xc, xc) ⤜ (λx'd. Heap_Monad.return (x'd ≤ Le 0))) True"
text ‹Complete DBM printing›
context
fixes n :: nat
fixes show_clock :: "nat ⇒ string"
and show_num :: "'a :: {linordered_ab_group_add,heap} ⇒ string"
notes [id_rules] = itypeI[of n "TYPE (nat)"]
and [sepref_import_param] = IdI[of n]
begin
definition
"make_string' e i j ≡
let
i = (if i > 0 then show_clock i else ''0'');
j = (if j > 0 then show_clock j else ''0'')
in
case e of
DBMEntry.Le a ⇒ i @ '' - '' @ j @ '' <= '' @ show_num a
| DBMEntry.Lt a ⇒ i @ '' - '' @ j @ '' < '' @ show_num a
| _ ⇒ i @ '' - '' @ j @ '' < inf''"
definition
"dbm_list_to_string' xs ≡
(concat o intersperse '', '' o rev o snd o snd) $ fold (λe (i, j, acc).
let
s = make_string' e i j;
j = (j + 1) mod (n + 1);
i = (if j = 0 then i + 1 else i)
in (i, j, s # acc)
) xs (0, 0, [])"
lemma [sepref_import_param]:
"(dbm_list_to_string', PR_CONST dbm_list_to_string') ∈ ⟨Id⟩list_rel → ⟨Id⟩list_rel"
by simp
definition show_dbm' where
"show_dbm' M ≡ PR_CONST dbm_list_to_string' (dbm_to_list n M)"
sepref_register "PR_CONST dbm_list_to_string'"
lemmas [sepref_fr_rules] = dbm_to_list_impl.refine
sepref_definition show_dbm_impl_all is
"Refine_Basic.RETURN o show_dbm'" :: "(mtx_assn n)⇧k →⇩a list_assn id_assn"
unfolding show_dbm'_def by sepref
end
definition
"abstr_repair_impl m ≡
λai. imp_nfoldli ai (λσ. Heap_Monad.return True)
(λai bi. abstra_upd_impl m ai bi ⤜ (λx'. repair_pair_impl m x' 0 (constraint_clk ai)))"
definition E_op_impl ::
"nat ⇒ (nat, int) acconstraint list ⇒ nat list ⇒ _"
where
"E_op_impl m l_inv r g l'_inv M ≡
do {
M1 ← up_canonical_upd_impl m M m;
M2 ← abstr_repair_impl m l_inv M1;
is_empty1 ← check_diag_impl m M2;
M3 ← (if is_empty1 then mtx_set (Suc m) M2 (0, 0) (Lt 0) else abstr_repair_impl m g M2);
is_empty3 ← check_diag_impl m M3;
if is_empty3 then
mtx_set (Suc m) M3 (0, 0) (Lt 0)
else do {
M4 ←
imp_nfoldli r (λσ. Heap_Monad.return True) (λxc σ. reset_canonical_upd_impl m σ m xc 0) M3;
abstr_repair_impl m l'_inv M4
}
}"
paragraph ‹Full Monomorphization of @{term E_op_impl}›
definition min_int :: "int ⇒ int ⇒ int" where
"min_int x y ≡ if x ≤ y then x else y"
named_theorems int_folds
lemma min_int_fold[int_folds]:
"min = min_int"
unfolding min_int_def min_def ..
fun min_int_entry :: "int DBMEntry ⇒ int DBMEntry ⇒ int DBMEntry" where
"min_int_entry (Lt x) (Lt y) = (if x ≤ y then Lt x else Lt y)"
| "min_int_entry (Lt x) (Le y) = (if x ≤ y then Lt x else Le y)"
| "min_int_entry (Le x) (Lt y) = (if x < y then Le x else Lt y)"
| "min_int_entry (Le x) (Le y) = (if x ≤ y then Le x else Le y)"
| "min_int_entry ∞ x = x"
| "min_int_entry x ∞ = x"
export_code min_int_entry in SML
lemma min_int_entry[int_folds]:
"min = min_int_entry"
apply (intro ext)
subgoal for a b
by (cases a; cases b; simp add: dbm_entry_simps)
done
fun dbm_le_int :: "int DBMEntry ⇒ int DBMEntry ⇒ bool" where
"dbm_le_int (Lt a) (Lt b) ⟷ a ≤ b"
| "dbm_le_int (Lt a) (Le b) ⟷ a ≤ b"
| "dbm_le_int (Le a) (Lt b) ⟷ a < b"
| "dbm_le_int (Le a) (Le b) ⟷ a ≤ b"
| "dbm_le_int _ ∞ ⟷ True"
| "dbm_le_int _ _ ⟷ False"
lemma dbm_le_dbm_le_int[int_folds]:
"dbm_le = dbm_le_int"
apply (intro ext)
subgoal for a b
by (cases a; cases b; auto simp: dbm_le_def)
done
fun dbm_lt_int :: "int DBMEntry ⇒ int DBMEntry ⇒ bool"
where
"dbm_lt_int (Le a) (Le b) ⟷ a < b" |
"dbm_lt_int (Le a) (Lt b) ⟷ a < b" |
"dbm_lt_int (Lt a) (Le b) ⟷ a ≤ b" |
"dbm_lt_int (Lt a) (Lt b) ⟷ a < b" |
"dbm_lt_int ∞ _ = False" |
"dbm_lt_int _ ∞ = True"
lemma dbm_lt_dbm_lt_int[int_folds]:
"dbm_lt = dbm_lt_int"
apply (intro ext)
subgoal for a b
by (cases a; cases b; auto)
done
definition [symmetric, int_folds]:
"dbm_lt_0 x ≡ x < (Le (0 :: int))"
lemmas [int_folds] = dbm_lt_0_def[unfolded DBM.less]
lemma dbm_lt_0_code_simps [code]:
"dbm_lt_0 (Le x) ⟷ x < 0"
"dbm_lt_0 (Lt x) ⟷ x ≤ 0"
"dbm_lt_0 ∞ = False"
unfolding dbm_lt_0_def[symmetric] DBM.less dbm_lt_dbm_lt_int by simp+
definition abstra_upd_impl_int
:: "nat ⇒ (nat, int) acconstraint ⇒ int DBMEntry Heap.array ⇒ int DBMEntry Heap.array Heap"
where [symmetric, int_folds]:
"abstra_upd_impl_int = abstra_upd_impl"
schematic_goal abstra_upd_impl_int_code[code]:
"abstra_upd_impl_int ≡ ?i"
unfolding abstra_upd_impl_int_def[symmetric] abstra_upd_impl_def
unfolding int_folds
.
definition fw_upd_impl_int
:: "nat ⇒ int DBMEntry Heap.array ⇒ nat ⇒ nat ⇒ nat ⇒ int DBMEntry Heap.array Heap"
where [symmetric, int_folds]:
"fw_upd_impl_int = fw_upd_impl"
lemmas [int_folds] = DBM.add dbm_add_int
schematic_goal fw_upd_impl_int_code [code]:
"fw_upd_impl_int ≡ ?i"
unfolding fw_upd_impl_int_def[symmetric] fw_upd_impl_def
unfolding int_folds
.
definition fwi_impl_int
:: "nat ⇒ int DBMEntry Heap.array ⇒ nat ⇒ int DBMEntry Heap.array Heap"
where [symmetric, int_folds]:
"fwi_impl_int = fwi_impl"
schematic_goal fwi_impl_int_code [code]:
"fwi_impl_int ≡ ?i"
unfolding fwi_impl_int_def[symmetric] fwi_impl_def unfolding int_folds .
definition fw_impl_int
:: "nat ⇒ int DBMEntry Heap.array ⇒ int DBMEntry Heap.array Heap"
where [symmetric, int_folds]:
"fw_impl_int = fw_impl"
schematic_goal fw_impl_int_code [code]:
"fw_impl_int ≡ ?i"
unfolding fw_impl_int_def[symmetric] fw_impl_def unfolding int_folds .
definition repair_pair_impl_int
:: "nat ⇒ int DBMEntry Heap.array ⇒ nat ⇒ nat ⇒ int DBMEntry Heap.array Heap"
where [symmetric, int_folds]:
"repair_pair_impl_int ≡ repair_pair_impl"
schematic_goal repair_pair_impl_int_code[code]:
"repair_pair_impl_int ≡ ?i"
unfolding repair_pair_impl_int_def[symmetric] repair_pair_impl_def
unfolding int_folds
.
definition abstr_repair_impl_int
:: "nat ⇒ (nat, int) acconstraint list ⇒ int DBMEntry Heap.array ⇒ int DBMEntry Heap.array Heap"
where [symmetric, int_folds]:
"abstr_repair_impl_int = abstr_repair_impl"
schematic_goal abstr_repair_impl_int_code[code]:
"abstr_repair_impl_int ≡ ?i"
unfolding abstr_repair_impl_int_def[symmetric] abstr_repair_impl_def
unfolding int_folds
.
definition check_diag_impl_int
:: "nat ⇒ int DBMEntry Heap.array ⇒ bool Heap"
where [symmetric, int_folds]:
"check_diag_impl_int = check_diag_impl"
schematic_goal check_diag_impl_int_code[code]:
"check_diag_impl_int ≡ ?i"
unfolding check_diag_impl_int_def[symmetric] check_diag_impl_def
unfolding int_folds
.
definition check_diag_impl'_int
:: "nat ⇒ nat ⇒ int DBMEntry Heap.array ⇒ bool Heap"
where [symmetric, int_folds]:
"check_diag_impl'_int = check_diag_impl'"
schematic_goal check_diag_impl'_int_code[code]:
"check_diag_impl'_int ≡ ?i"
unfolding check_diag_impl'_int_def[symmetric] check_diag_impl'_def
unfolding int_folds
.
definition reset_canonical_upd_impl_int
:: "nat ⇒ int DBMEntry Heap.array ⇒ _"
where [symmetric, int_folds]:
"reset_canonical_upd_impl_int = reset_canonical_upd_impl"
schematic_goal reset_canonical_upd_impl_int_code[code]:
"reset_canonical_upd_impl_int ≡ ?i"
unfolding reset_canonical_upd_impl_int_def[symmetric] reset_canonical_upd_impl_def
unfolding int_folds
.
definition up_canonical_upd_impl_int
:: "nat ⇒ int DBMEntry Heap.array ⇒ _"
where [symmetric, int_folds]:
"up_canonical_upd_impl_int = up_canonical_upd_impl"
schematic_goal up_canonical_upd_impl_int_code[code]:
"up_canonical_upd_impl_int ≡ ?i"
unfolding up_canonical_upd_impl_int_def[symmetric] up_canonical_upd_impl_def
.
schematic_goal E_op_impl_code[code]:
"E_op_impl ≡ ?i"
unfolding E_op_impl_def
unfolding int_folds
.
definition free_impl_int :: "nat ⇒ int DBMEntry Heap.array ⇒ _"
where [symmetric, int_folds]:
"free_impl_int = free_impl"
schematic_goal free_impl_int_code[code]:
"free_impl_int ≡ ?i"
unfolding free_impl_int_def[symmetric] free_impl_def
unfolding int_folds
.
definition down_impl_int :: "nat ⇒ int DBMEntry Heap.array ⇒ _"
where [symmetric, int_folds]:
"down_impl_int = down_impl"
schematic_goal down_impl_int_code[code]:
"down_impl_int ≡ ?i"
unfolding down_impl_int_def[symmetric] down_impl_def
unfolding int_folds
.
fun neg_dbm_entry_int where
"neg_dbm_entry_int (Le (a :: int)) = Lt (-a)" |
"neg_dbm_entry_int (Lt a) = Le (-a)" |
"neg_dbm_entry_int DBMEntry.INF = DBMEntry.INF"
lemma neg_dbm_entry_int_fold [int_folds]:
"neg_dbm_entry = neg_dbm_entry_int"
apply (intro ext)
subgoal for x
by (cases x; auto)
done
schematic_goal and_entry_impl_code [code]:
"and_entry_impl ≡ ?impl"
unfolding and_entry_impl_def unfolding int_folds .
schematic_goal and_entry_repair_impl_code [code]:
"and_entry_repair_impl ≡ ?impl"
unfolding and_entry_repair_impl_def unfolding int_folds .
definition upd_entry_impl_int :: "_ ⇒ _ ⇒ _ ⇒ int DBMEntry Heap.array ⇒ _"
where [symmetric, int_folds]:
"upd_entry_impl_int = upd_entry_impl"
schematic_goal upd_entry_impl_int_code [code]:
"upd_entry_impl_int ≡ ?i"
unfolding upd_entry_impl_int_def[symmetric] upd_entry_impl_def unfolding int_folds .
schematic_goal upd_entries_impl_code [code]:
"upd_entries_impl ≡ ?impl"
unfolding upd_entries_impl_def int_folds .
definition get_entries_impl_int :: "nat ⇒ int DBMEntry Heap.array ⇒ _"
where [symmetric, int_folds]:
"get_entries_impl_int = get_entries_impl"
schematic_goal get_entries_impl_int_code[code]:
"get_entries_impl_int ≡ ?i"
unfolding get_entries_impl_int_def[symmetric] get_entries_impl_def unfolding int_folds .
schematic_goal dbm_minus_canonical_impl_code [code]:
"dbm_minus_canonical_impl ≡ ?i"
unfolding dbm_minus_canonical_impl_def unfolding int_folds .
definition abstr_upd_impl_int
:: "nat ⇒ (nat, int) acconstraint list ⇒ int DBMEntry Heap.array ⇒ int DBMEntry Heap.array Heap"
where [symmetric, int_folds]:
"abstr_upd_impl_int = abstr_upd_impl"
schematic_goal abstr_upd_impl_int_code[code]:
"abstr_upd_impl_int ≡ ?i"
unfolding abstr_upd_impl_int_def[symmetric] abstr_upd_impl_def unfolding int_folds .
definition abstr_FW_impl_int :: "_ ⇒ _ ⇒ int DBMEntry Heap.array ⇒ _"
where [symmetric, int_folds]:
"abstr_FW_impl_int = abstr_FW_impl"
schematic_goal abstr_FW_impl_int_code [code]:
"abstr_FW_impl_int ≡ ?i"
unfolding abstr_FW_impl_int_def[symmetric] abstr_FW_impl_def unfolding int_folds .
paragraph ‹Extracting executable implementations›
lemma hfkeep_hfdropI:
assumes "(fi, f) ∈ A⇧k →⇩a B"
shows "(fi, f) ∈ A⇧d →⇩a B"
supply [sep_heap_rules] =
assms[to_hnr, unfolded hn_refine_def, simplified hn_ctxt_def, simplified, rule_format]
by sepref_to_hoare sep_auto
context Simple_Network_Impl_nat_ceiling_start_state
begin
sublocale impl: Reachability_Problem_Impl_Precise
where trans_fun = trans_from
and inv_fun = inv_fun
and ceiling = k_impl
and A = prod_ta
and l⇩0 = l⇩0
and l⇩0i = l⇩0i
and n = m
and k = k_fun
and trans_impl = trans_impl
and states' = states'
and loc_rel = loc_rel
and f = reach.E_precise_op'
and op_impl = "PR_CONST impl.E_precise_op'_impl"
and states_mem_impl = states'_memi
and F = "λ(l, _). F l"
and F1 = "F o fst"
and F' = "F o fst"
and F_impl = impl.F_impl
apply standard
apply (unfold PR_CONST_def, rule impl.E_precise_op'_impl.refine, rule states'_memi_correct)
subgoal
by auto
subgoal
apply simp
done
subgoal
apply simp
done
subgoal
using impl.F_impl.refine by (intro hfkeep_hfdropI) simp
done
lemma state_impl_abstract':
assumes "states'_memi li"
shows "∃l. (li, l) ∈ loc_rel"
proof -
obtain Li si where "li = (Li, si)"
by force
with state_impl_abstract[of Li si] show ?thesis
using assms unfolding states'_memi_def states_def by auto
qed
interpretation Bisimulation_Invariant
"(λ(l, u) (l', u'). conv_A prod_ta ⊢' ⟨l, u⟩ → ⟨l', u'⟩)"
"(λ(L, s, u) (L', s', u'). Simple_Network_Language.conv A ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩)"
"(λ((L, s), u) (L', s', u'). L = L' ∧ u = u' ∧ s = s')"
"(λ((L, s), u). conv.all_prop L s)"
"(λ(L, s, u). conv.all_prop L s)"
by (rule prod_bisim)
lemma unreachability_prod:
assumes
"formula = formula.EX φ"
"(∄u l' u'. (∀c≤m. u c = 0) ∧ conv_A prod_ta ⊢' ⟨l⇩0, u⟩ →* ⟨l', u'⟩ ∧ PR_CONST F l')"
shows "¬ Simple_Network_Language.conv A,(L⇩0, map_of s⇩0, λ_. 0) ⊨ formula"
proof -
let ?check = "¬ B.Ex_ev (λ(L, s, _). check_sexp φ L (the ∘ s)) (L⇩0, map_of s⇩0, λ_. 0)"
have *: "PR_CONST F l ⟷ (λ((L, s), _). check_sexp φ L (the o s)) (l, u)"
for l and u :: "nat ⇒ real"
unfolding assms(1) by auto
have "conv.all_prop L⇩0 (map_of s⇩0)"
using all_prop_start unfolding conv_all_prop .
then have
"?check ⟷ ¬ reach.Ex_ev (λ ((L, s), _). check_sexp φ L (the o s)) (l⇩0, u⇩0)"
by (auto intro!: Ex_ev_iff[symmetric, unfolded A_B.equiv'_def])
also from assms(2) have "…"
apply -
apply standard
apply (drule reach.Ex_ev_reaches)
unfolding impl.reaches_steps'[symmetric]
apply (subst (asm) *)
apply force
done
finally show ?thesis
using assms unfolding models_def by simp
qed
lemma no_buechi_run_prod:
assumes
"formula = formula.EX φ"
"¬ has_deadlock (Simple_Network_Language.conv A) (L⇩0, map_of s⇩0, λ_. 0)"
"∄u xs. (∀c≤m. u c = 0) ∧ reach.run ((l⇩0, u) ## xs) ∧ alw (ev (holds (F ∘ fst))) ((l⇩0, u) ## xs)"
shows "¬ Graph_Defs.alw_ev
(λ (L, s, u) (L', s', u'). Simple_Network_Language.conv A ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩)
(λ (L, s, _). check_sexp φ L (the o s)) (L⇩0, map_of s⇩0, λ_. 0)"
proof -
let ?F = "λ((L, s), _). check_sexp φ L (the o s)"
have *: "?F = (F ∘ fst)"
using assms(1) by auto
have "conv.all_prop L⇩0 (map_of s⇩0)"
using all_prop_start unfolding conv_all_prop .
then have
"¬ B.alw_ev (λ(L, s, _). check_sexp φ L (the ∘ s)) (L⇩0, map_of s⇩0, λ_. 0)
⟷ ¬ reach.alw_ev ?F (l⇩0, u⇩0)"
by (auto intro!: alw_ev_iff[symmetric, unfolded A_B.equiv'_def])
also have "…"
proof -
from assms(2) have "¬ reach.deadlock (l⇩0, λ_. 0)"
unfolding has_deadlock_def deadlock_start_iff .
then obtain xs where "reach.run ((l⇩0, λ_. 0) ## xs)"
using reach.no_deadlock_run_extend[of "(l⇩0, λ_. 0)" "[]"] by auto
with assms(3) show ?thesis
unfolding reach.alw_ev_def ‹?F = _› by force
qed
finally show ?thesis
using assms by simp
qed
lemma deadlock_prod:
"¬ reach.deadlock (l⇩0, λ_. 0)
⟷ ¬ has_deadlock (Simple_Network_Language.conv A) (L⇩0, map_of s⇩0, λ_. 0)"
unfolding has_deadlock_def deadlock_start_iff ..
lemma list_assn_split:
"list_assn (list_assn impl.location_assn) (split_k num_split L) (split_k num_split Li) =
list_assn impl.location_assn L Li"
proof -
have 1: "impl.location_assn = pure (the_pure impl.location_assn)"
using impl.pure_K by auto
have "(split_k num_split Li, split_k num_split L) ∈ ⟨⟨the_pure impl.location_assn⟩list_rel⟩list_rel
⟷ (Li, L) ∈ ⟨the_pure impl.location_assn⟩list_rel"
unfolding list_rel_def by (auto simp: list_all2_split_k[symmetric])
then show ?thesis
apply (subst (2) 1, subst 1)
unfolding list_assn_pure_conv unfolding pure_def by auto
qed
theorem unreachability_checker_hnr:
assumes "⋀li. P_loc li ⟹ states'_memi li"
and "list_all (λx. P_loc x ∧ states'_memi x) L_list"
and "list_all (λ(l, y). list_all (λM. length M = Suc m * Suc m) y) M_list"
and "fst ` set M_list = set L_list"
and "formula = formula.EX φ"
shows "(
uncurry0 (impl.unreachability_checker L_list M_list (split_k num_split)),
uncurry0 (SPEC (λr. r ⟶
¬ Simple_Network_Language.conv A,(L⇩0, map_of s⇩0, λ_. 0) ⊨ formula)))
∈ unit_assn⇧k →⇩a bool_assn"
proof -
define checker where "checker ≡ impl.unreachability_checker L_list M_list"
from assms(4) have "fst ` set M_list ⊆ set L_list"
by blast
note [sep_heap_rules] =
impl.unreachability_checker_hnr[
OF state_impl_abstract',
OF assms(1,2) this assms(3) split_k_full_split list_assn_split
impl.L_dom_M_eqI[OF state_impl_abstract', OF assms(1,2) this assms(3,4)],
to_hnr, unfolded hn_refine_def, rule_format, folded checker_def
]
show ?thesis
unfolding checker_def[symmetric] using unreachability_prod[OF assms(5)]
by sepref_to_hoare (sep_auto simp: pure_def)
qed
theorem unreachability_checker2_refine:
assumes "⋀li. P_loc li ⟹ states'_memi li"
and "list_all (λx. P_loc x ∧ states'_memi x) L_list"
and "list_all (λ(l, y). list_all (λM. length M = Suc m * Suc m) y) M_list"
and "fst ` set M_list = set L_list"
and "formula = formula.EX φ"
shows "
impl.unreachability_checker2 L_list M_list (split_k num_split) ⟶
¬ Simple_Network_Language.conv A,(L⇩0, map_of s⇩0, λ_. 0) ⊨ formula"
using impl.unreachability_checker2_refine[OF state_impl_abstract',
OF assms(1,2) assms(4)[THEN equalityD1] assms(3) split_k_full_split list_assn_split assms(4)
]
unreachability_prod[OF assms(5)]
by auto
theorem unreachability_checker3_refine:
assumes "⋀li. P_loc li ⟹ states'_memi li"
and "list_all (λx. P_loc x ∧ states'_memi x) L_list"
and "list_all (λ(l, y). list_all (λM. length M = Suc m * Suc m) y) M_list"
and "fst ` set M_list = set L_list"
and "formula = formula.EX φ"
shows "
impl.certify_unreachable_pure L_list M_list (split_k' num_split M_list) ⟶
¬ Simple_Network_Language.conv A,(L⇩0, map_of s⇩0, λ_. 0) ⊨ formula"
using impl.certify_unreachable_pure_refine[
OF state_impl_abstract', OF assms(1,2) assms(4)[THEN equalityD1] assms(3)
split_k'_full_split[of M_list, unfolded assms(4)] assms(4)
]
unreachability_prod[OF assms(5)]
by auto
lemma init_conds: "{l⇩0} ⊆ states'" "([l⇩0i], {l⇩0}) ∈ ⟨loc_rel⟩list_set_rel"
unfolding list_set_rel_singleton_iff using impl.init_impl by blast+
theorem no_buechi_run_checker_refine:
assumes "⋀li. P_loc li ⟹ states'_memi li"
and "list_all (λx. P_loc x ∧ states'_memi x) L_list"
and "list_all (λ(l, y). list_all (λ(M, _). length M = Suc m * Suc m) y) M_list"
and "fst ` set M_list = set L_list"
and "formula = formula.EX φ"
and "¬ has_deadlock (Simple_Network_Language.conv A) (L⇩0, map_of s⇩0, λ_. 0)"
shows "
impl.certify_no_buechi_run_pure L_list M_list (split_k' num_split M_list) [l⇩0i] ⟶
¬ Graph_Defs.alw_ev
(λ (L, s, u) (L', s', u'). Simple_Network_Language.conv A ⊢ ⟨L, s, u⟩ → ⟨L', s', u'⟩)
(λ (L, s, _). check_sexp φ L (the o s)) (L⇩0, map_of s⇩0, λ_. 0)"
proof -
have
"(case (l, D) of (l, _) ⇒ F l) = (F ∘ fst) (l, Z)"
if "l⇩0' ∈ {l⇩0}" "reach1.E_precise_op'.E_from_op_empty⇧*⇧* (l⇩0', init_dbm) (l, D)"
"dbm.zone_of (curry (conv_M D)) = Z" for l⇩0' l D Z
unfolding comp_def by simp
with init_conds show ?thesis
using impl.certify_no_buechi_run_pure_refine[
OF state_impl_abstract', OF assms(1,2) assms(4)[THEN equalityD1] assms(3)
split_k'_full_split[of M_list, unfolded assms(4)] _ _ assms(4),
of "{(L⇩0, map_of s⇩0)}" "[l⇩0i]"
]
using no_buechi_run_prod[OF assms(5, 6)] by auto
qed
lemma abstr_repair_impl_refine:
"impl.abstr_repair_impl = abstr_repair_impl m"
unfolding abstr_repair_impl_def impl.abstr_repair_impl_def impl.abstra_repair_impl_def ..
lemma E_op_impl_refine:
"impl.E_precise_op'_impl l r g l' M = E_op_impl m (inv_fun l) r g (inv_fun l') M"
unfolding impl.E_precise_op'_impl_def E_op_impl_def abstr_repair_impl_refine ..
definition
"succs1 n_ps invs ≡
let
inv_fun = λ(L, a). concat (map (λi. invs !! i !! (L ! i)) [0..<n_ps]);
E_op_impl = (λl r g l' M. E_op_impl m (inv_fun l) r g (inv_fun l') M)
in (λL_s M.
if M = [] then Heap_Monad.return []
else imp_nfoldli (trans_impl L_s) (λσ. Heap_Monad.return True)
(λc σ. case c of (g, a1a, r, L_s') ⇒ do {
M ← heap_map amtx_copy M;
Ms ← imp_nfoldli M (λσ. Heap_Monad.return True)
(λxb σ. do {
x'c ← E_op_impl L_s r g L_s' xb;
x'e ← check_diag_impl m x'c;
Heap_Monad.return (if x'e then σ else op_list_prepend x'c σ)
}) [];
Heap_Monad.return (op_list_prepend (L_s', Ms) σ)
})
[])" for n_ps :: "nat" and invs :: "(nat, int) acconstraint list iarray iarray"
lemma succs1_refine:
"impl.succs_precise'_impl = succs1 n_ps invs2"
unfolding impl.succs_precise'_impl_def impl.succs_precise_inner_impl_def
unfolding succs1_def Let_def PR_CONST_def E_op_impl_refine
unfolding inv_fun_alt_def ..
schematic_goal trans_impl_alt_def:
"trans_impl ≡ ?impl"
unfolding trans_impl_def
apply (abstract_let int_trans_impl int_trans_impl)
apply (abstract_let bin_trans_from_impl bin_trans_impl)
apply (abstract_let broad_trans_from_impl broad_trans_impl)
unfolding int_trans_impl_def bin_trans_from_impl_def broad_trans_from_impl_def
apply (abstract_let trans_in_broad_grouped trans_in_broad_grouped)
apply (abstract_let trans_out_broad_grouped trans_out_broad_grouped)
apply (abstract_let trans_in_map trans_in_map)
apply (abstract_let trans_out_map trans_out_map)
apply (abstract_let int_trans_from_all_impl int_trans_from_all_impl)
unfolding int_trans_from_all_impl_def
apply (abstract_let int_trans_from_vec_impl int_trans_from_vec_impl)
unfolding int_trans_from_vec_impl_def
apply (abstract_let int_trans_from_loc_impl int_trans_from_loc_impl)
unfolding int_trans_from_loc_impl_def
apply (abstract_let trans_i_map trans_i_map)
unfolding trans_out_broad_grouped_def trans_out_broad_map_def
unfolding trans_in_broad_grouped_def trans_in_broad_map_def
unfolding trans_in_map_def trans_out_map_def
unfolding trans_i_map_def
apply (abstract_let trans_map trans_map)
.
schematic_goal succs1_alt_def:
"succs1 ≡ ?impl"
unfolding succs1_def
apply (abstract_let trans_impl trans_impl)
unfolding trans_impl_alt_def
.
schematic_goal succs_impl_alt_def:
"impl.succs_precise'_impl ≡ ?impl"
unfolding impl.succs_precise'_impl_def impl.succs_precise_inner_impl_def
apply (abstract_let impl.E_precise_op'_impl E_op_impl)
unfolding impl.E_precise_op'_impl_def fw_impl'_int
apply (abstract_let trans_impl trans_impl)
unfolding trans_impl_def
apply (abstract_let int_trans_impl int_trans_impl)
apply (abstract_let bin_trans_from_impl bin_trans_impl)
apply (abstract_let broad_trans_from_impl broad_trans_impl)
unfolding int_trans_impl_def bin_trans_from_impl_def broad_trans_from_impl_def
apply (abstract_let trans_in_broad_grouped trans_in_broad_grouped)
apply (abstract_let trans_out_broad_grouped trans_out_broad_grouped)
apply (abstract_let trans_in_map trans_in_map)
apply (abstract_let trans_out_map trans_out_map)
apply (abstract_let int_trans_from_all_impl int_trans_from_all_impl)
unfolding int_trans_from_all_impl_def
apply (abstract_let int_trans_from_vec_impl int_trans_from_vec_impl)
unfolding int_trans_from_vec_impl_def
apply (abstract_let int_trans_from_loc_impl int_trans_from_loc_impl)
unfolding int_trans_from_loc_impl_def
apply (abstract_let trans_i_map trans_i_map)
unfolding trans_out_broad_grouped_def trans_out_broad_map_def
unfolding trans_in_broad_grouped_def trans_in_broad_map_def
unfolding trans_in_map_def trans_out_map_def
unfolding trans_i_map_def
apply (abstract_let trans_map trans_map)
apply (abstract_let "inv_fun :: nat list × int list ⇒ _" inv_fun)
unfolding inv_fun_alt_def
apply (abstract_let invs2 invs)
unfolding invs2_def
apply (abstract_let n_ps n_ps)
by (rule Pure.reflexive)
end
concrete_definition (in -) succs_impl
uses Simple_Network_Impl_nat_ceiling_start_state.succs1_alt_def
context Simple_Network_Impl_nat_ceiling_start_state
begin
schematic_goal check_deadlock_impl_alt_def:
"impl.check_deadlock_impl ≡ ?impl"
unfolding impl.check_deadlock_impl_def
apply (abstract_let trans_impl trans_impl)
unfolding trans_impl_alt_def
apply (abstract_let "inv_fun :: nat list × int list ⇒ _" inv_fun)
unfolding inv_fun_alt_def
apply (abstract_let invs2 invs)
unfolding invs2_def
apply (abstract_let n_ps n_ps)
.
context
fixes L_list
assumes L_list: "list_all states'_memi L_list"
begin
private lemma A:
"list_all (λx. states'_memi x ∧ states'_memi x) L_list"
using L_list by simp
context
fixes M_list :: "((nat list × int list) × int DBMEntry list list) list"
assumes assms: "fst ` set M_list ⊆ set L_list"
"list_all (λ(l, y). list_all (λM. length M = Suc m * Suc m) y) M_list"
begin
lemmas assms = L_list assms
lemma unreachability_checker_def:
"impl.unreachability_checker L_list M_list (split_k num_split) ≡
let Fi = impl.F_impl; Pi = impl.P_impl; copyi = amtx_copy; Lei = dbm_subset_impl m;
l⇩0i = Heap_Monad.return l⇩0i; s⇩0i = impl.init_dbm_impl; succsi = impl.succs_precise'_impl
in do {
let _ = start_timer ();
M_table ← impl.M_table M_list;
let _ = save_time STR ''Time for loading certificate'';
r ← certify_unreachable_impl_inner
Fi Pi copyi Lei succsi l⇩0i s⇩0i (split_k num_split) L_list M_table;
Heap_Monad.return r
}"
by (subst impl.unreachability_checker_alt_def[OF
state_impl_abstract', OF _ A assms(2,3) split_k_full_split list_assn_split];
simp)
schematic_goal unreachability_checker_alt_def:
"impl.unreachability_checker L_list M_list (split_k num_split) ≡ ?x"
apply (subst unreachability_checker_def)
apply (subst impl.M_table_def[OF state_impl_abstract', of states'_memi, OF _ A assms(2,3)])
apply assumption
unfolding impl.F_impl_def impl.P_impl_def
apply (abstract_let states'_memi check_states)
unfolding states'_memi_def states_mem_compute'
apply (abstract_let "map states_i [0..<n_ps]" states_i)
unfolding succs_impl_alt_def
unfolding k_impl_alt_def k_i_def
unfolding impl.E_op''_impl_def impl.abstr_repair_impl_def impl.abstra_repair_impl_def
unfolding impl.start_inv_check_impl_def unbounded_dbm_impl_def unbounded_dbm'_def
unfolding impl.init_dbm_impl_def impl.a⇩0_impl_def
unfolding impl.subsumes_impl_def
unfolding impl.emptiness_check_impl_def
unfolding impl.state_copy_impl_def
by (rule Pure.reflexive)
definition no_deadlock_certifier where
"no_deadlock_certifier ≡
Reachability_Problem_Impl_Precise.unreachability_checker
m trans_impl l⇩0i (PR_CONST impl.E_precise_op'_impl)
states'_memi (λ(l, M). impl.check_deadlock_impl l M ⤜ (λr. Heap_Monad.return (¬ r)))"
lemma no_deadlock_certifier_alt_def1:
"no_deadlock_certifier L_list M_list (split_k num_split) ≡
let
Fi = (λ(l, M). impl.check_deadlock_impl l M ⤜ (λr. Heap_Monad.return (¬ r)));
Pi = impl.P_impl; copyi = amtx_copy; Lei = dbm_subset_impl m;
l⇩0i = Heap_Monad.return l⇩0i; s⇩0i = impl.init_dbm_impl;
succsi = impl.succs_precise'_impl
in do {
let _ = start_timer ();
M_table ← impl.M_table M_list;
let _ = save_time STR ''Time for loading certificate'';
r ← certify_unreachable_impl_inner
Fi Pi copyi Lei succsi l⇩0i s⇩0i (split_k num_split) L_list M_table;
Heap_Monad.return r
}"
unfolding no_deadlock_certifier_def
by (subst impl.deadlock_unreachability_checker_alt_def[
OF state_impl_abstract', OF _ A assms(2,3) split_k_full_split list_assn_split
];
simp)
schematic_goal no_deadlock_certifier_alt_def:
"no_deadlock_certifier L_list M_list (split_k num_split) ≡ ?x"
apply (subst no_deadlock_certifier_alt_def1)
apply (subst impl.M_table_def[OF state_impl_abstract', of states'_memi, OF _ A assms(2,3)])
apply assumption
unfolding check_deadlock_impl_alt_def impl.P_impl_def
apply (abstract_let states'_memi check_states)
unfolding states'_memi_def states_mem_compute'
apply (abstract_let "map states_i [0..<n_ps]" states_i)
unfolding succs_impl_alt_def
unfolding k_impl_alt_def k_i_def
unfolding impl.E_op''_impl_def impl.abstr_repair_impl_def impl.abstra_repair_impl_def
unfolding impl.start_inv_check_impl_def unbounded_dbm_impl_def unbounded_dbm'_def
unfolding impl.init_dbm_impl_def impl.a⇩0_impl_def
unfolding impl.subsumes_impl_def
unfolding impl.emptiness_check_impl_def
unfolding impl.state_copy_impl_def
.
lemmas no_deadlock_certifier_hnr' =
impl.deadlock_unreachability_checker_hnr[folded no_deadlock_certifier_def,
OF state_impl_abstract',
OF _ A assms(2,3) impl.L_dom_M_eqI[OF state_impl_abstract' A assms(2,3)]
split_k_full_split list_assn_split,
unfolded deadlock_prod
]
schematic_goal unreachability_checker2_alt_def:
"impl.unreachability_checker2 L_list M_list (split_k num_split) ≡ ?x"
apply (subst impl.unreachability_checker2_def[
OF state_impl_abstract', OF _ A assms(2,3) split_k_full_split list_assn_split
], (simp; fail))
apply (subst impl.M_table_def[OF state_impl_abstract', of states'_memi, OF _ A assms(2,3)])
apply assumption
unfolding check_deadlock_impl_alt_def impl.P_impl_def impl.F_impl_def
apply (abstract_let states'_memi check_states)
unfolding states'_memi_def states_mem_compute'
apply (abstract_let "map states_i [0..<n_ps]" states_i)
unfolding succs_impl_alt_def
unfolding k_impl_alt_def k_i_def
unfolding impl.E_op''_impl_def impl.abstr_repair_impl_def impl.abstra_repair_impl_def
unfolding impl.start_inv_check_impl_def unbounded_dbm_impl_def unbounded_dbm'_def
unfolding impl.init_dbm_impl_def impl.a⇩0_impl_def
unfolding impl.subsumes_impl_def
unfolding impl.emptiness_check_impl_def
unfolding impl.state_copy_impl_def
by (rule Pure.reflexive)
definition no_deadlock_certifier2 where
"no_deadlock_certifier2 ≡
Reachability_Problem_Impl_Precise.unreachability_checker2
m trans_impl l⇩0i (PR_CONST impl.E_precise_op'_impl)
states'_memi (λ(l, M). impl.check_deadlock_impl l M ⤜ (λr. Heap_Monad.return (¬ r)))"
schematic_goal no_deadlock_certifier2_alt_def:
"no_deadlock_certifier2 L_list M_list (split_k num_split) ≡ ?x"
unfolding no_deadlock_certifier2_def
apply (subst impl.deadlock_unreachability_checker2_def[
OF state_impl_abstract', OF _ A assms(2,3) split_k_full_split list_assn_split
], (simp; fail))
apply (subst impl.M_table_def[OF state_impl_abstract', of states'_memi, OF _ A assms(2,3)])
apply assumption
unfolding check_deadlock_impl_alt_def impl.P_impl_def
apply (abstract_let states'_memi check_states)
unfolding states'_memi_def states_mem_compute'
apply (abstract_let "map states_i [0..<n_ps]" states_i)
unfolding succs_impl_alt_def
unfolding k_impl_alt_def k_i_def
unfolding impl.E_op''_impl_def impl.abstr_repair_impl_def impl.abstra_repair_impl_def
unfolding impl.start_inv_check_impl_def unbounded_dbm_impl_def unbounded_dbm'_def
unfolding impl.init_dbm_impl_def impl.a⇩0_impl_def
unfolding impl.subsumes_impl_def
unfolding impl.emptiness_check_impl_def
unfolding impl.state_copy_impl_def
by (rule Pure.reflexive)
lemmas no_deadlock_certifier2_refine' =
impl.deadlock_unreachability_checker2_hnr[
folded no_deadlock_certifier2_def,
OF state_impl_abstract' A assms(3) _ split_k_full_split list_assn_split
]
schematic_goal unreachability_checker3_alt_def:
"impl.certify_unreachable_pure L_list M_list (split_k' num_split M_list) ≡ ?x"
if "fst ` set M_list = set L_list"
apply (subst impl.certify_unreachable_pure_def[
OF state_impl_abstract', OF _ A assms(2,3) split_k'_full_split[of M_list, unfolded that]
], (simp; fail))
apply (abstract_let "impl.init_dbm_impl :: int DBMEntry Heap.array Heap" init_dbm)
unfolding impl.init_dbm_impl_def
apply (abstract_let "impl.Mi M_list" Mi)
apply (subst impl.Mi_def[OF state_impl_abstract', of states'_memi, OF _ A assms(2,3)])
apply assumption
unfolding check_deadlock_impl_alt_def impl.P_impl_def impl.F_impl_def
apply (abstract_let states'_memi check_state)
unfolding states'_memi_def states_mem_compute'
apply (abstract_let "map states_i [0..<n_ps]" states_i)
apply (abstract_let "impl.succs_precise'_impl" succsi)
unfolding succs_impl.refine[OF Simple_Network_Impl_nat_ceiling_start_state_axioms] succs1_refine
apply (abstract_let invs2 invs)
unfolding invs2_def
apply (abstract_let n_ps n_ps)
apply (abstract_let n_vs n_vs)
.
schematic_goal check_deadlock_impl_alt_def2:
"impl.check_deadlock_impl ≡ ?impl"
unfolding impl.check_deadlock_impl_def
apply (abstract_let trans_impl trans_impl)
unfolding trans_impl_alt_def
apply (abstract_let "inv_fun :: nat list × int list ⇒ _" inv_fun)
unfolding inv_fun_alt_def
apply (abstract_let invs2 invs)
unfolding invs2_def
apply (abstract_let n_ps n_ps)
.
definition no_deadlock_certifier3 where
"no_deadlock_certifier3 ≡
Reachability_Problem_Impl_Precise.certify_unreachable_pure
m trans_impl l⇩0i (PR_CONST impl.E_precise_op'_impl)
states'_memi (λ(l, M). impl.check_deadlock_impl l M ⤜ (λr. Heap_Monad.return (¬ r)))"
definition
"check_deadlock_fold = (λa. run_heap ((case a of (l, s) ⇒ array_unfreeze s
⤜ (λs. Heap_Monad.return (id l, s)))
⤜ (λa. case a of (l, M) ⇒ impl.check_deadlock_impl l M
⤜ (λr. Heap_Monad.return (¬ r)))))"
schematic_goal no_deadlock_certifier3_alt_def:
"no_deadlock_certifier3 L_list M_list (split_k' num_split M_list) ≡ ?x"
if "fst ` set M_list = set L_list"
unfolding no_deadlock_certifier3_def
apply (subst impl.deadlock_unreachability_checker3_def[
OF state_impl_abstract', OF _ A assms(2,3) split_k'_full_split[of M_list, unfolded that]
], (simp; fail))
unfolding check_deadlock_fold_def[symmetric]
apply (abstract_let check_deadlock_fold check_deadlock1)
unfolding check_deadlock_fold_def
apply (abstract_let impl.check_deadlock_impl check_deadlock)
apply (abstract_let "impl.init_dbm_impl :: int DBMEntry Heap.array Heap" init_dbm)
unfolding impl.init_dbm_impl_def
apply (abstract_let "impl.Mi M_list" Mi)
apply (subst impl.Mi_def[OF state_impl_abstract', of states'_memi, OF _ A assms(2,3)])
apply assumption
apply (abstract_let "(λa :: (nat list × int list) × int DBMEntry iarray. run_heap
((case a of (l, s) ⇒ array_unfreeze s ⤜ (λs. Heap_Monad.return (id l, s))) ⤜ impl.P_impl))"
P)
apply (abstract_let "impl.P_impl :: _ × int DBMEntry Heap.array ⇒ _" P_impl)
apply (abstract_let "(λ(as :: int DBMEntry iarray) bs.
(∃i≤m. as !! (i + i * m + i) < Le 0) ∨ array_all2 (Suc m * Suc m) (≤) as bs)"
subsumption)
unfolding check_deadlock_impl_alt_def2
unfolding impl.P_impl_def impl.F_impl_def
apply (abstract_let states'_memi check_states)
unfolding states'_memi_def states_mem_compute'
apply (abstract_let "map states_i [0..<n_ps]" states_i)
apply (abstract_let "impl.succs_precise'_impl" succsi)
unfolding succs_impl.refine[OF Simple_Network_Impl_nat_ceiling_start_state_axioms] succs1_refine
apply (abstract_let invs2 invs)
unfolding invs2_def
apply (abstract_let n_ps n_ps)
apply (abstract_let n_vs n_vs)
.
lemma no_deadlock_certifier3_refine':
"no_deadlock_certifier3 L_list M_list (split_k' num_split M_list)
⟶ (∀u. (∀c≤m. u c = 0) ⟶ ¬ reach.deadlock (l⇩0, u))" if "fst ` set M_list = set L_list"
by (rule impl.deadlock_unreachability_checker3_hnr[
folded no_deadlock_certifier3_def, OF state_impl_abstract' A assms(3)
]) (simp add: that split_k'_full_split[symmetric])+
end
context
fixes M_list :: "((nat list × int list) × (int DBMEntry list × nat) list) list"
assumes assms:
"fst ` set M_list ⊆ set L_list"
"list_all (λ(l, y). list_all (λ(M, _). length M = Suc m * Suc m) y) M_list"
begin
schematic_goal no_buechi_run_checker_alt_def:
"impl.certify_no_buechi_run_pure L_list M_list (split_k' num_split M_list) [l⇩0i] ≡ ?x"
if "fst ` set M_list = set L_list"
apply (subst impl.certify_no_buechi_run_pure_def[
OF state_impl_abstract', OF _ A assms split_k'_full_split[of M_list, unfolded that] init_conds
], assumption)
apply (subst impl.initsi_def[
OF state_impl_abstract', OF _ A assms split_k'_full_split[of M_list, unfolded that] init_conds
], assumption)
apply (abstract_let "impl.init_dbm_impl :: int DBMEntry Heap.array Heap" init_dbm)
unfolding impl.init_dbm_impl_def
apply (abstract_let "impl.M2i M_list" Mi)
apply (subst impl.M2i_def[OF state_impl_abstract', of states'_memi, OF _ A assms(1,2)])
apply assumption
unfolding check_deadlock_impl_alt_def impl.P_impl_def impl.F_impl_def
apply (abstract_let states'_memi check_state)
unfolding states'_memi_def states_mem_compute'
apply (abstract_let "map states_i [0..<n_ps]" states_i)
apply (abstract_let "impl.succs_precise'_impl" succsi)
unfolding succs_impl.refine[OF Simple_Network_Impl_nat_ceiling_start_state_axioms] succs1_refine
apply (abstract_let invs2 invs)
unfolding invs2_def
apply (abstract_let n_ps n_ps)
apply (abstract_let n_vs n_vs)
.
end
end
theorem no_deadlock_certifier_hnr:
assumes "list_all states'_memi L_list"
and "list_all (λ(l, y). list_all (λM. length M = Suc m * Suc m) y) M_list"
and "fst ` set M_list = set L_list"
shows "(
uncurry0 (no_deadlock_certifier L_list M_list (split_k num_split)),
uncurry0 (SPEC (λr. r ⟶
¬ has_deadlock (Simple_Network_Language.conv A) (L⇩0, map_of s⇩0, λ_. 0))))
∈ unit_assn⇧k →⇩a bool_assn"
proof -
define checker where "checker ≡ no_deadlock_certifier L_list M_list"
define P where "P ≡ reach.deadlock"
note *[sep_heap_rules] =
no_deadlock_certifier_hnr'[
OF assms(1) _ assms(2),
to_hnr, unfolded hn_refine_def, rule_format, folded checker_def P_def
]
from assms(3) show ?thesis
unfolding checker_def[symmetric] deadlock_prod[symmetric] P_def[symmetric]
by sepref_to_hoare (sep_auto simp: pure_def)
qed
theorem no_deadlock_certifier2_refine:
assumes "list_all states'_memi L_list"
and "list_all (λ(l, y). list_all (λM. length M = Suc m * Suc m) y) M_list"
and "fst ` set M_list = set L_list"
shows "no_deadlock_certifier2 L_list M_list (split_k num_split) ⟶
¬ has_deadlock (Simple_Network_Language.conv A) (L⇩0, map_of s⇩0, λ_. 0)"
using no_deadlock_certifier2_refine'[OF assms(1) _ assms(2), of num_split] assms(3)
unfolding deadlock_prod[symmetric] by auto
theorem no_deadlock_certifier3_refine:
assumes "list_all states'_memi L_list"
and "list_all (λ(l, y). list_all (λM. length M = Suc m * Suc m) y) M_list"
and "fst ` set M_list = set L_list"
shows "no_deadlock_certifier3 L_list M_list (split_k' num_split M_list) ⟶
¬ has_deadlock (Simple_Network_Language.conv A) (L⇩0, map_of s⇩0, λ_. 0)"
using no_deadlock_certifier3_refine' assms unfolding deadlock_prod[symmetric] by auto
definition
"show_dbm_impl' M ≡ do {
s ← show_dbm_impl m show_clock show M;
Heap_Monad.return (String.implode s)
}"
definition
"show_state_impl l ≡ do {
let s = show_state l;
let s = String.implode s;
Heap_Monad.return s
}"
definition
"trace_table M_table ≡ do {
M_list' ← list_of_map_impl M_table;
let _ = println STR ''Inverted table'';
Heap_Monad.fold_map (λ (l, xs). do {
s1 ← show_state_impl l;
let _ = println (s1 + STR '':'');
Heap_Monad.fold_map (λM. do {
s2 ← show_dbm_impl_all m show_clock show M;
let _ = println (STR '' '' + String.implode s2);
Heap_Monad.return ()
}) xs;
Heap_Monad.return ()
}) M_list';
Heap_Monad.return ()
}" for M_table
definition
"check_prop_fail L_list M_list ≡ let
P_impl = impl.P_impl;
copy = amtx_copy;
show_dbm = show_dbm_impl';
show_state = show_state_impl
in do {
M_table ← M_table M_list;
r ← check_prop_fail_impl P_impl copy show_dbm show_state L_list M_table;
case r of None ⇒ Heap_Monad.return () | Some (l, M) ⇒ do {
let b = states'_memi l;
let _ = println (if b then STR ''State passed'' else STR ''State failed'');
b ← check_diag_impl m M;
let _ = println (if b then STR ''DBM passed diag'' else STR ''DBM failed diag'');
b ← check_diag_nonpos m M;
let _ = println (if b then STR ''DBM passed diag nonpos'' else STR ''DBM failed diag nonpos'');
b ← check_nonneg m M;
let _ = println (if b then STR ''DBM passed nonneg'' else STR ''DBM failed nonneg'');
s ← show_dbm_impl_all m show_clock show M;
let _ = println (STR ''DBM: '' + String.implode s);
Heap_Monad.return ()
}
}"
definition
"check_deadlock_fail L_list M_list ≡ let
P_impl = (λ(l, M). impl.check_deadlock_impl l M);
copy = amtx_copy;
show_dbm = show_dbm_impl';
show_state = show_state_impl
in do {
M_table ← M_table M_list;
r ← check_prop_fail_impl P_impl copy show_dbm show_state L_list M_table;
case r of None ⇒ Heap_Monad.return () | Some (l, M) ⇒ do {
let _ = println (STR ''⏎The following state is deadlocked'');
s ← show_state l;
let _ = println s;
s ← show_dbm_impl_all m show_clock show M;
let _ = println (String.implode s);
Heap_Monad.return ()
}
}"
definition
"check_invariant_fail ≡ λL_list M_list. let
copy = amtx_copy;
succs = impl.succs_precise'_impl;
Lei = dbm_subset_impl m;
show_state = show_state_impl;
show_dbm = show_dbm_impl_all m show_clock show
in do {
M_table ← M_table M_list;
r ← check_invariant_fail_impl copy Lei succs L_list M_table;
case r of None ⇒ Heap_Monad.return ()
| Some (Inl (Inl (l, l', xs))) ⇒ do {
let _ = println (STR ''The successor is not contained in L:'');
s ← show_state l;
let _ = println (STR '' '' + s);
s ← show_state l';
let _ = println (STR '' '' + s);
Heap_Monad.fold_map (λM. do {
s ← show_dbm M;
let _ = println (STR '' '' + String.implode s);
Heap_Monad.return ()
}) xs;
Heap_Monad.return ()
}
| Some (Inl (Inr (l, l', xs))) ⇒ do {
let _ = println (STR ''The successor is not empty:'');
s ← show_state l;
let _ = println (STR '' '' + s);
s ← show_state l';
let _ = println (STR '' '' + s);
Heap_Monad.fold_map (λM. do {
s ← show_dbm M;
let _ = println (STR '' '' + String.implode s);
Heap_Monad.return ()
}) xs;
Heap_Monad.return ()
}
| Some (Inr (l, as, l', M, xs)) ⇒ do {
s1 ← show_state l;
s2 ← show_state l';
s3 ← show_dbm M;
let _ = println (STR ''⏎A successor of the zones for:⏎ '' + s1);
Heap_Monad.fold_map (λM. do {
s ← show_dbm M;
let _ = println (STR ''⏎'' + String.implode s);
Heap_Monad.return ()
}) as;
let _ = println (STR ''⏎is not subsumed:⏎ '' + s2 + STR ''⏎'');
let _ = println (String.implode s3 + STR ''⏎'');
let _ = println (STR ''These are the candidate dbms:'');
Heap_Monad.fold_map (λM. do {
s ← show_dbm M;
let _ = println (STR ''⏎'' + String.implode s);
Heap_Monad.return ()
}) xs;
let _ = println (STR '''');
Heap_Monad.return ()
}
}
"
schematic_goal check_prop_fail_alt_def:
"check_prop_fail ≡ ?t"
unfolding check_prop_fail_def
unfolding M_table_def trace_table_def
unfolding impl.P_impl_def
unfolding show_dbm_impl'_def
unfolding show_state_impl_def
apply (abstract_let states'_memi check_states)
unfolding states'_memi_def states_mem_compute'
apply (abstract_let "map states_i [0..<n_ps]" states_i)
by (rule Pure.reflexive)
schematic_goal check_deadlock_fail_alt_def:
"check_deadlock_fail ≡ ?t"
unfolding check_deadlock_fail_def
unfolding M_table_def trace_table_def
unfolding check_deadlock_impl_alt_def
unfolding succs_impl_alt_def
unfolding k_impl_alt_def k_i_def
unfolding impl.E_op''_impl_def impl.abstr_repair_impl_def impl.abstra_repair_impl_def
unfolding unbounded_dbm_impl_def unbounded_dbm'_def
unfolding impl.emptiness_check_impl_def
unfolding impl.state_copy_impl_def
unfolding show_dbm_impl'_def
unfolding show_state_impl_def
.
schematic_goal check_invariant_fail_alt_def:
"check_invariant_fail ≡ ?t"
unfolding check_invariant_fail_def
unfolding M_table_def
unfolding succs_impl_alt_def
unfolding impl.E_op''_impl_def impl.abstr_repair_impl_def impl.abstra_repair_impl_def
unfolding impl.subsumes_impl_def
unfolding impl.emptiness_check_impl_def
unfolding impl.state_copy_impl_def
unfolding show_dbm_impl'_def show_state_impl_def
by (rule Pure.reflexive)
end
concrete_definition unreachability_checker uses
Simple_Network_Impl_nat_ceiling_start_state.unreachability_checker_alt_def
concrete_definition no_deadlock_certifier uses
Simple_Network_Impl_nat_ceiling_start_state.no_deadlock_certifier_alt_def
concrete_definition unreachability_checker2 uses
Simple_Network_Impl_nat_ceiling_start_state.unreachability_checker2_alt_def
concrete_definition no_deadlock_certifier2 uses
Simple_Network_Impl_nat_ceiling_start_state.no_deadlock_certifier2_alt_def
concrete_definition unreachability_checker3 uses
Simple_Network_Impl_nat_ceiling_start_state.unreachability_checker3_alt_def
concrete_definition no_deadlock_certifier3 uses
Simple_Network_Impl_nat_ceiling_start_state.no_deadlock_certifier3_alt_def
concrete_definition no_buechi_run_checker uses
Simple_Network_Impl_nat_ceiling_start_state.no_buechi_run_checker_alt_def
concrete_definition check_prop_fail uses
Simple_Network_Impl_nat_ceiling_start_state.check_prop_fail_alt_def
concrete_definition check_deadlock_fail uses
Simple_Network_Impl_nat_ceiling_start_state.check_deadlock_fail_alt_def
concrete_definition check_invariant_fail uses
Simple_Network_Impl_nat_ceiling_start_state.check_invariant_fail_alt_def
lemma states'_memi_alt_def:
"Simple_Network_Impl_nat_defs.states'_memi broadcast bounds' automata = (
λ(L, s).
let
n_ps = length automata;
n_vs = Simple_Network_Impl_Defs.n_vs bounds';
states_i = map (Simple_Network_Impl_nat_defs.states_i automata) [0..<n_ps]
in
length L = n_ps ∧ (∀i<n_ps. L ! i ∈ states_i ! i) ∧
length s = n_vs ∧ Simple_Network_Impl_nat_defs.check_boundedi bounds' s
)
"
unfolding Simple_Network_Impl_nat_defs.states'_memi_def
unfolding Simple_Network_Impl_nat_defs.states_mem_compute'
unfolding Prod_TA_Defs.n_ps_def list_all_iff
by (intro ext) simp
definition
"certificate_checker_pre
L_list M_list broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula
≡
let
_ = start_timer ();
check1 = Simple_Network_Impl_nat_ceiling_start_state
broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula;
_ = save_time STR ''Time to check ceiling'';
n_ps = length automata;
n_vs = Simple_Network_Impl_Defs.n_vs bounds';
states_i = map (Simple_Network_Impl_nat_defs.states_i automata) [0..<n_ps];
_ = start_timer ();
check2 = list_all (λ(L, s). length L = n_ps ∧ (∀i<n_ps. L ! i ∈ states_i ! i) ∧
length s = n_vs ∧ Simple_Network_Impl_nat_defs.check_boundedi bounds' s
) L_list;
_ = save_time STR ''Time to check states'';
_ = start_timer ();
n_sq = Suc m * Suc m;
check3 = list_all (λ(l, xs). list_all (λM. length M = n_sq) xs) M_list;
_ = save_time STR ''Time to check DBMs'';
check4 = (case formula of formula.EX _ ⇒ True | _ ⇒ False)
in check1 ∧ check2 ∧ check3 ∧ check4"
definition
"certificate_checker num_split dc
M_list broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula
≡
let
L_list = map fst M_list;
check = certificate_checker_pre
L_list M_list broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula
in if check then
do {
r ←
if dc then
no_deadlock_certifier
broadcast bounds' automata m num_states num_actions L⇩0 s⇩0 L_list M_list num_split
else
unreachability_checker
broadcast bounds' automata m num_states num_actions L⇩0 s⇩0 formula L_list M_list num_split;
Heap_Monad.return (Some r)
} else Heap_Monad.return None"
definition
"certificate_checker2 num_split dc
M_list broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula
≡
let
L_list = map fst M_list;
check = certificate_checker_pre
L_list M_list broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula
in if check then
if dc then
no_deadlock_certifier2
broadcast bounds' automata m num_states num_actions L⇩0 s⇩0 L_list M_list num_split
else
unreachability_checker2
broadcast bounds' automata m num_states num_actions L⇩0 s⇩0 formula L_list M_list num_split
else False"
definition
"certificate_checker3 num_split dc
M_list broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula
≡
let
L_list = map fst M_list;
check = certificate_checker_pre
L_list M_list broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula
in if check then
if dc then
no_deadlock_certifier3
broadcast bounds' automata m num_states num_actions L⇩0 s⇩0 L_list M_list num_split
else
unreachability_checker3
broadcast bounds' automata m num_states num_actions L⇩0 s⇩0 formula L_list M_list num_split
else False"
definition
"certificate_checker_dbg num_split dc
(show_clock :: (nat ⇒ string)) (show_state :: (nat list × int list ⇒ char list))
M_list broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula
≡
let
_ = start_timer ();
check1 = Simple_Network_Impl_nat_ceiling_start_state
broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula;
_ = save_time STR ''Time to check ceiling'';
L_list = map fst M_list;
n_ps = length automata;
n_vs = Simple_Network_Impl_Defs.n_vs bounds';
states_i = map (Simple_Network_Impl_nat_defs.states_i automata) [0..<n_ps];
_ = start_timer ();
check2 = list_all (λ(L, s). length L = n_ps ∧ (∀i<n_ps. L ! i ∈ states_i ! i) ∧
length s = n_vs ∧ Simple_Network_Impl_nat_defs.check_boundedi bounds' s
) L_list;
_ = save_time STR ''Time to check states'';
check3 = (case formula of formula.EX _ ⇒ True | _ ⇒ False)
in if check1 ∧ check2 ∧ check3 then
do {
check_prop_fail broadcast bounds' automata m show_clock show_state L_list M_list;
check_invariant_fail broadcast bounds' automata m
num_states num_actions show_clock show_state L_list M_list;
(if dc then
check_deadlock_fail broadcast bounds' automata m
num_states num_actions show_clock show_state L_list M_list
else Heap_Monad.return ());
r ← unreachability_checker
broadcast bounds' automata m num_states num_actions L⇩0 s⇩0 formula L_list M_list num_split;
Heap_Monad.return (Some r)
} else Heap_Monad.return None" for show_clock show_state
definition
"print_fail s b ≡ if b then () else println (s + STR '' precondition check failed!'')"
definition
"certificate_checker_pre1
L_list M_list broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula
≡
let
_ = start_timer ();
check1 = Simple_Network_Impl_nat_ceiling_start_state
broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula;
_ = save_time STR ''Time to check ceiling'';
n_ps = length automata;
n_vs = Simple_Network_Impl_Defs.n_vs bounds';
states_i = map (Simple_Network_Impl_nat_defs.states_i automata) [0..<n_ps];
_ = start_timer ();
check2 = list_all (λ(L, s). length L = n_ps ∧ (∀i<n_ps. L ! i ∈ states_i ! i) ∧
length s = n_vs ∧ Simple_Network_Impl_nat_defs.check_boundedi bounds' s
) L_list;
_ = save_time STR ''Time to check states'';
_ = start_timer ();
n_sq = Suc m * Suc m;
check3 = list_all (λ(l, xs). list_all (λ(M, _). length M = n_sq) xs) M_list;
_ = save_time STR ''Time to check DBMs'';
check4 = (case formula of formula.EX _ ⇒ True | _ ⇒ False);
_ = map (λ(a, b). print_fail a b) [
(STR ''Ceiling'', check1),
(STR ''States'', check2),
(STR ''DBM'', check3),
(STR ''Formula'', check4)
]
in check1 ∧ check2 ∧ check3 ∧ check4"
definition
"buechi_certificate_checker num_split
M_list broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula
≡
let
L_list = map fst M_list;
check = certificate_checker_pre1
L_list M_list broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula
in if check then
no_buechi_run_checker
broadcast bounds' automata m num_states num_actions L⇩0 s⇩0 formula L_list M_list num_split
else let _ = println STR ''Checking Buechi preconditions failed'' in False"
theorem certificate_check:
"<emp> certificate_checker num_split False
M_list broadcast bounds automata m num_states num_actions k L⇩0 s⇩0 formula
<λ Some r ⇒ ↑(r ⟶ ¬ N broadcast automata bounds,(L⇩0, map_of s⇩0, λ_ . 0) ⊨ formula)
| None ⇒ true>⇩t"
proof -
define A where "A ≡ N broadcast automata bounds"
define check where "check ≡ A,(L⇩0, map_of s⇩0, λ_ . 0) ⊨ formula"
{ fix φ assume A: "formula = formula.EX φ"
note
Simple_Network_Impl_nat_ceiling_start_state.unreachability_checker_hnr[
of broadcast bounds automata m num_states num_actions k L⇩0 s⇩0 formula
"Simple_Network_Impl_nat_defs.states'_memi broadcast bounds automata"
"map fst M_list" M_list,
folded A_def check_def,
to_hnr, unfolded hn_refine_def, rule_format,
OF _ _ _ _ _ A, unfolded A]
} note *[sep_heap_rules] = this[simplified, unfolded hd_of_formulai.simps[abs_def]]
show ?thesis
unfolding A_def[symmetric] check_def[symmetric]
unfolding certificate_checker_def certificate_checker_pre_def
unfolding Let_def
unfolding states'_memi_alt_def[unfolded Let_def, symmetric, of automata bounds broadcast]
by (sep_auto simp: unreachability_checker.refine[symmetric] pure_def split: formula.split_asm)
qed
theorem certificate_deadlock_check:
"<emp> certificate_checker num_split True
M_list broadcast bounds automata m num_states num_actions k L⇩0 s⇩0 formula
<λ Some r ⇒ ↑(r ⟶ ¬ has_deadlock (N broadcast automata bounds) (L⇩0, map_of s⇩0, λ_ . 0))
| None ⇒ true>⇩t"
proof -
define A where "A ≡ N broadcast automata bounds"
define check where "check ≡ ¬ has_deadlock A (L⇩0, map_of s⇩0, λ_ . 0)"
note *[sep_heap_rules] = Simple_Network_Impl_nat_ceiling_start_state.no_deadlock_certifier_hnr[
of broadcast bounds automata m num_states num_actions k L⇩0 s⇩0 formula
"map fst M_list" M_list,
folded A_def check_def,
to_hnr, unfolded hn_refine_def, rule_format, unfolded hd_of_formulai.simps[abs_def]
]
show ?thesis
unfolding A_def[symmetric] check_def[symmetric]
unfolding certificate_checker_def certificate_checker_pre_def
unfolding Let_def
unfolding states'_memi_alt_def[unfolded Let_def, symmetric, of automata bounds broadcast]
by (sep_auto simp: no_deadlock_certifier.refine[symmetric] pure_def split: formula.split_asm)
qed
theorem certificate_check2:
"certificate_checker2 num_split False
M_list broadcast bounds automata m num_states num_actions k L⇩0 s⇩0 formula
⟶ ¬ N broadcast automata bounds,(L⇩0, map_of s⇩0, λ_ . 0) ⊨ formula"
using Simple_Network_Impl_nat_ceiling_start_state.unreachability_checker2_refine[
of broadcast bounds automata m num_states num_actions k L⇩0 s⇩0 formula
"Simple_Network_Impl_nat_defs.states'_memi broadcast bounds automata"
"map fst M_list" M_list
]
unfolding certificate_checker2_def certificate_checker_pre_def
unfolding Let_def
unfolding states'_memi_alt_def[unfolded Let_def, symmetric, of automata bounds broadcast]
by (clarsimp split: formula.split_asm simp: unreachability_checker2.refine[symmetric])
theorem certificate_deadlock_check2:
"certificate_checker2 num_split True
M_list broadcast bounds automata m num_states num_actions k L⇩0 s⇩0 formula
⟶ ¬ has_deadlock (N broadcast automata bounds) (L⇩0, map_of s⇩0, λ_ . 0)"
using Simple_Network_Impl_nat_ceiling_start_state.no_deadlock_certifier2_refine[
of broadcast bounds automata m num_states num_actions k L⇩0 s⇩0 formula
"map fst M_list" M_list num_split
]
unfolding certificate_checker2_def certificate_checker_pre_def Let_def
unfolding states'_memi_alt_def[unfolded Let_def, symmetric, of automata bounds broadcast]
by (clarsimp simp: no_deadlock_certifier2.refine[symmetric])
theorem certificate_check3:
"certificate_checker3 num_split False
M_list broadcast bounds automata m num_states num_actions k L⇩0 s⇩0 formula
⟶ ¬ N broadcast automata bounds,(L⇩0, map_of s⇩0, λ_ . 0) ⊨ formula"
using Simple_Network_Impl_nat_ceiling_start_state.unreachability_checker3_refine[
of broadcast bounds automata m num_states num_actions k L⇩0 s⇩0 formula
"Simple_Network_Impl_nat_defs.states'_memi broadcast bounds automata"
"map fst M_list" M_list
]
unfolding certificate_checker3_def certificate_checker_pre_def
unfolding Let_def
unfolding states'_memi_alt_def[unfolded Let_def, symmetric, of automata bounds broadcast]
by (clarsimp split: formula.split_asm simp: unreachability_checker3.refine[symmetric])
theorem certificate_deadlock_check3:
"certificate_checker3 num_split True
M_list broadcast bounds automata m num_states num_actions k L⇩0 s⇩0 formula
⟶ ¬ has_deadlock (N broadcast automata bounds) (L⇩0, map_of s⇩0, λ_ . 0)"
using Simple_Network_Impl_nat_ceiling_start_state.no_deadlock_certifier3_refine[
of broadcast bounds automata m num_states num_actions k L⇩0 s⇩0 formula
"map fst M_list" M_list
]
unfolding certificate_checker3_def certificate_checker_pre_def Let_def
unfolding states'_memi_alt_def[unfolded Let_def, symmetric, of automata bounds broadcast]
by (clarsimp simp: no_deadlock_certifier3.refine[symmetric])
fun sexp_of_Ex where
"sexp_of_Ex (formula.EX s) = s"
theorem buechi_certificate_check:
"buechi_certificate_checker num_split
M_list broadcast bounds automata m num_states num_actions k L⇩0 s⇩0 formula
⟶ ¬ has_deadlock (N broadcast automata bounds) (L⇩0, map_of s⇩0, λ_. 0)
⟶ (∃φ. formula = formula.EX φ) ∧ ¬ Graph_Defs.alw_ev
(λ(L, s, u) (L', x, y).
(N broadcast automata bounds) ⊢ ⟨L, s, u⟩ → ⟨L', x, y⟩)
(λ(L, s, _). check_sexp (sexp_of_Ex formula) L (the ∘ s))
(L⇩0, map_of s⇩0, λ_. 0)"
using Simple_Network_Impl_nat_ceiling_start_state.no_buechi_run_checker_refine[
of broadcast bounds automata m num_states num_actions k L⇩0 s⇩0 formula
"Simple_Network_Impl_nat_defs.states'_memi broadcast bounds automata"
"map fst M_list" M_list
]
unfolding buechi_certificate_checker_def certificate_checker_pre1_def
unfolding Let_def
unfolding states'_memi_alt_def[unfolded Let_def, symmetric, of automata bounds broadcast]
by (clarsimp split: formula.split_asm simp: no_buechi_run_checker.refine[symmetric])
definition rename_check where
"rename_check num_split dc broadcast bounds' automata k L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
state_space
≡
do {
let r = do_rename_mc (
λ(show_clock :: (nat ⇒ string)) (show_state :: (nat list × int list ⇒ char list)).
certificate_checker num_split dc state_space)
dc broadcast bounds' automata k STR ''_urge'' L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
(λ_ _. '' '') (λ_. '' '') (λ_. '' '');
case r of Some r ⇒ do {
r ← r;
case r of
None ⇒ Heap_Monad.return Preconds_Unsat
| Some False ⇒ Heap_Monad.return Unsat
| Some True ⇒ Heap_Monad.return Sat
}
| None ⇒ Heap_Monad.return Renaming_Failed
}
"
definition rename_check2 where
"rename_check2 num_split dc broadcast bounds' automata k L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
state_space
≡
let r = do_rename_mc (
λ(show_clock :: (nat ⇒ string)) (show_state :: (nat list × int list ⇒ char list)).
certificate_checker2 num_split dc state_space)
dc broadcast bounds' automata k STR ''_urge'' L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
(λ_ _. '' '') (λ_. '' '') (λ_. '' '')
in case r of
Some False ⇒ Unsat
| Some True ⇒ Sat
| None ⇒ Renaming_Failed
"
definition rename_check3 where
"rename_check3 num_split dc broadcast bounds' automata k L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
state_space
≡
let r = do_rename_mc (
λ(show_clock :: (nat ⇒ string)) (show_state :: (nat list × int list ⇒ string)).
certificate_checker3 num_split dc state_space)
dc broadcast bounds' automata k STR ''_urge'' L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
(λ_ _. '' '') (λ_. '' '') (λ_. '' '')
in case r of
Some False ⇒ Unsat
| Some True ⇒ Sat
| None ⇒ Renaming_Failed
"
definition rename_check_dbg where
"rename_check_dbg num_split dc broadcast bounds' automata k L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
inv_renum_states inv_renum_vars inv_renum_clocks
state_space
≡
do {
let r = do_rename_mc (
λ(show_clock :: (nat ⇒ string)) (show_state :: (nat list × int list ⇒ string)).
certificate_checker_dbg num_split dc show_clock show_state state_space)
dc broadcast bounds' automata k STR ''_urge'' L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
inv_renum_states inv_renum_vars inv_renum_clocks;
case r of Some r ⇒ do {
r ← r;
case r of
None ⇒ Heap_Monad.return Preconds_Unsat
| Some False ⇒ Heap_Monad.return Unsat
| Some True ⇒ Heap_Monad.return Sat
}
| None ⇒ Heap_Monad.return Renaming_Failed
}
"
definition rename_check_buechi where
"rename_check_buechi num_split broadcast bounds' automata k L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
state_space
≡
let r = do_rename_mc (
λ(show_clock :: (nat ⇒ string)) (show_state :: (nat list × int list ⇒ string)).
buechi_certificate_checker num_split state_space)
False broadcast bounds' automata k STR ''_urge'' L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
(λ_ _. '' '') (λ_. '' '') (λ_. '' '')
in case r of
Some False ⇒ Unsat
| Some True ⇒ Sat
| None ⇒ Renaming_Failed
"
theorem certificate_check_rename:
"<emp> rename_check num_split False broadcast bounds automata k L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
state_space
<λ Sat ⇒ ↑(
(¬ N broadcast automata bounds,(L⇩0, map_of s⇩0, λ_ . 0) ⊨ formula))
| Renaming_Failed ⇒ ↑(¬ Simple_Network_Rename_Formula
broadcast bounds
renum_acts renum_vars renum_clocks renum_states STR ''_urge''
s⇩0 L⇩0 automata formula)
| Unsat ⇒ true
| Preconds_Unsat ⇒ true
>⇩t" (is ?A)
and certificate_check_rename2:
"case rename_check2 num_split False broadcast bounds automata k L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
state_space
of
Sat ⇒ ¬ N broadcast automata bounds,(L⇩0, map_of s⇩0, λ_ . 0) ⊨ formula
| Renaming_Failed ⇒ ¬ Simple_Network_Rename_Formula
broadcast bounds
renum_acts renum_vars renum_clocks renum_states STR ''_urge''
s⇩0 L⇩0 automata formula
| Unsat ⇒ True
| Preconds_Unsat ⇒ True" (is ?B)
and certificate_check_rename3:
"case rename_check3 num_split False broadcast bounds automata k L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
state_space
of
Sat ⇒ ¬ N broadcast automata bounds,(L⇩0, map_of s⇩0, λ_ . 0) ⊨ formula
| Renaming_Failed ⇒ ¬ Simple_Network_Rename_Formula
broadcast bounds
renum_acts renum_vars renum_clocks renum_states STR ''_urge''
s⇩0 L⇩0 automata formula
| Unsat ⇒ True
| Preconds_Unsat ⇒ True" (is ?C)
and buechi_check_rename:
"case rename_check_buechi num_split broadcast bounds automata k L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
certificate
of
Sat ⇒
¬ has_deadlock (N broadcast automata bounds) (L⇩0, map_of s⇩0, λ_. 0) ⟶
¬ Graph_Defs.alw_ev
(λ(L, s, u) (L', x, y). (N broadcast automata bounds) ⊢ ⟨L, s, u⟩ → ⟨L', x, y⟩)
(λ(L, s, _). check_sexp (sexp_of_Ex formula) L (the ∘ s))
(L⇩0, map_of s⇩0, λ_. 0)
| Renaming_Failed ⇒ ¬ Simple_Network_Rename_Formula
broadcast bounds
renum_acts renum_vars renum_clocks renum_states STR ''_urge''
s⇩0 L⇩0 automata formula
| Unsat ⇒ True
| Preconds_Unsat ⇒ True" (is ?D)
proof -
let ?urge = "STR ''_urge''"
let ?automata = "map (conv_urge ?urge) automata"
have *: "
Simple_Network_Rename_Formula_String
broadcast bounds
renum_acts renum_vars renum_clocks renum_states
automata ?urge formula s⇩0 L⇩0
= Simple_Network_Rename_Formula
broadcast bounds
renum_acts renum_vars renum_clocks renum_states
?urge s⇩0 L⇩0 automata formula
"
unfolding
Simple_Network_Rename_Formula_String_def Simple_Network_Rename_Formula_def
Simple_Network_Rename_def Simple_Network_Rename_Formula_axioms_def
Simple_Network_Rename_Start_def Simple_Network_Rename_Start_axioms_def
using infinite_literal by auto
define A where "A ≡ N broadcast automata bounds"
define check where "check ≡ A,(L⇩0, map_of s⇩0, λ_ . 0) ⊨ formula"
define A' where "A' ≡ N
(map renum_acts broadcast)
(map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states) ?automata)
(map (λ(a,p). (renum_vars a, p)) bounds)"
define check' where "check' ≡
A',(map_index renum_states L⇩0, map_of (map (λ(x, v). (renum_vars x, v)) s⇩0), λ_ . 0) ⊨
map_formula renum_states renum_vars id formula"
define deadlock_check where "deadlock_check ≡ has_deadlock A (L⇩0, map_of s⇩0, λ_ . 0)"
define deadlock_check' where "deadlock_check' ≡
has_deadlock A' (map_index renum_states L⇩0, map_of (map (λ(x, v). (renum_vars x, v)) s⇩0), λ_ . 0)"
define buechi_check where "buechi_check ≡
¬ Graph_Defs.alw_ev
(λ(L, s, u) (L', x, y). A ⊢ ⟨L, s, u⟩ → ⟨L', x, y⟩)
(λ(L, s, _). check_sexp (sexp_of_Ex formula) L (the ∘ s))
(L⇩0, map_of s⇩0, λ_. 0)"
define buechi_check' where "buechi_check' ≡
¬ Graph_Defs.alw_ev
(λ(L, s, u) (L', x, y). A' ⊢ ⟨L, s, u⟩ → ⟨L', x, y⟩)
(λ(L, s, _). check_sexp (sexp_of_Ex (map_formula renum_states renum_vars id formula)) L (the ∘ s))
(map_index renum_states L⇩0, map_of (map (λ(x, v). (renum_vars x, v)) s⇩0), λ_ . 0)"
define renaming_valid where "renaming_valid ≡
Simple_Network_Rename_Formula
broadcast bounds
renum_acts renum_vars renum_clocks renum_states STR ''_urge'' s⇩0 L⇩0 automata formula"
define formula_is_ex where
"formula_is_ex ≡ ∃φ. map_formula renum_states renum_vars id formula = formula.EX φ"
have [simp]: "check ⟷ check'" if renaming_valid
using that unfolding check_def check'_def A_def A'_def renaming_valid_def
by (rule Simple_Network_Rename_Formula.models_iff'[symmetric])
have [simp]: "buechi_check ⟷ buechi_check'" if renaming_valid formula_is_ex
proof -
from that(2) obtain φ where "formula = formula.EX φ"
unfolding formula_is_ex_def by (cases formula) auto
with that(1) show ?thesis
unfolding
buechi_check_def buechi_check'_def check_def check'_def A_def A'_def renaming_valid_def
by (simp add: Simple_Network_Rename_Formula.buechi_compatible'[symmetric])
qed
have **[simp]: "deadlock_check ⟷ deadlock_check'" if renaming_valid
using that unfolding deadlock_check_def deadlock_check'_def A_def A'_def renaming_valid_def
unfolding Simple_Network_Rename_Formula_def
by - (elim conjE,
rule Simple_Network_Language_Renaming.Simple_Network_Rename_Start.has_deadlock_iff'[symmetric])
note [sep_heap_rules] =
certificate_check[
of num_split state_space
"map renum_acts broadcast" "map (λ(a,p). (renum_vars a, p)) bounds"
"map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states) ?automata"
m num_states num_actions k "map_index renum_states L⇩0" "map (λ(x, v). (renum_vars x, v)) s⇩0"
"map_formula renum_states renum_vars id formula",
folded A'_def renaming_valid_def, folded check'_def, simplified
]
show ?A ?B ?C ?D
using certificate_check2[
of num_split state_space
"map renum_acts broadcast" "map (λ(a,p). (renum_vars a, p)) bounds"
"map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states) ?automata"
m num_states num_actions k "map_index renum_states L⇩0" "map (λ(x, v). (renum_vars x, v)) s⇩0"
"map_formula renum_states renum_vars id formula",
folded A'_def renaming_valid_def, folded check'_def
]
using certificate_check3[
of num_split state_space
"map renum_acts broadcast" "map (λ(a,p). (renum_vars a, p)) bounds"
"map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states) ?automata"
m num_states num_actions k "map_index renum_states L⇩0" "map (λ(x, v). (renum_vars x, v)) s⇩0"
"map_formula renum_states renum_vars id formula",
folded A'_def renaming_valid_def, folded check'_def
]
using buechi_certificate_check[
of num_split certificate
"map renum_acts broadcast" "map (λ(a,p). (renum_vars a, p)) bounds"
"map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states) ?automata"
m num_states num_actions k "map_index renum_states L⇩0" "map (λ(x, v). (renum_vars x, v)) s⇩0"
"map_formula renum_states renum_vars id formula",
folded A'_def renaming_valid_def,
folded buechi_check'_def deadlock_check'_def formula_is_ex_def
]
unfolding
rename_check_def rename_check2_def rename_check3_def rename_check_buechi_def
do_rename_mc_def rename_network_def
unfolding if_False
unfolding Simple_Network_Rename_Formula_String_Defs.check_renaming[symmetric] * Let_def
unfolding
A_def[symmetric] renaming_valid_def[symmetric]
check_def[symmetric] buechi_check_def[symmetric] deadlock_check_def[symmetric]
by (sep_auto split: bool.splits)+
qed
theorem certificate_deadlock_check_rename:
"<emp> rename_check num_split True broadcast bounds automata k L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
state_space
<λ Sat ⇒ ↑(¬ has_deadlock (N broadcast automata bounds) (L⇩0, map_of s⇩0, λ_ . 0))
| Renaming_Failed ⇒ ↑(¬ Simple_Network_Rename_Formula
broadcast bounds renum_acts renum_vars renum_clocks renum_states STR ''_urge'' s⇩0 L⇩0
automata (formula.EX (sexp.not sexp.true)))
| Unsat ⇒ true
| Preconds_Unsat ⇒ true
>⇩t" (is ?A)
and certificate_deadlock_check_rename2:
"case rename_check2 num_split True broadcast bounds automata k L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
state_space
of
Sat ⇒ ¬ has_deadlock (N broadcast automata bounds) (L⇩0, map_of s⇩0, λ_ . 0)
| Renaming_Failed ⇒ ¬ Simple_Network_Rename_Formula
broadcast bounds renum_acts renum_vars renum_clocks renum_states STR ''_urge'' s⇩0 L⇩0
automata (formula.EX (sexp.not sexp.true))
| Unsat ⇒ True
| Preconds_Unsat ⇒ True" (is ?B)
and certificate_deadlock_check_rename3:
"case rename_check3 num_split True broadcast bounds automata k L⇩0 s⇩0 formula
m num_states num_actions renum_acts renum_vars renum_clocks renum_states
state_space
of
Sat ⇒ ¬ has_deadlock (N broadcast automata bounds) (L⇩0, map_of s⇩0, λ_ . 0)
| Renaming_Failed ⇒ ¬ Simple_Network_Rename_Formula
broadcast bounds renum_acts renum_vars renum_clocks renum_states STR ''_urge'' s⇩0 L⇩0
automata (formula.EX (sexp.not sexp.true))
| Unsat ⇒ True
| Preconds_Unsat ⇒ True" (is ?C)
proof -
let ?formula = "formula.EX (sexp.not sexp.true)"
let ?urge = "STR ''_urge''"
let ?automata = "map (conv_urge ?urge) automata"
have *: "
Simple_Network_Rename_Formula_String
broadcast bounds
renum_acts renum_vars renum_clocks renum_states
automata ?urge ?formula s⇩0 L⇩0
= Simple_Network_Rename_Formula
broadcast bounds
renum_acts renum_vars renum_clocks renum_states
?urge s⇩0 L⇩0 automata ?formula
"
unfolding
Simple_Network_Rename_Formula_String_def Simple_Network_Rename_Formula_def
Simple_Network_Rename_def Simple_Network_Rename_Formula_axioms_def
Simple_Network_Rename_Start_def Simple_Network_Rename_Start_axioms_def
using infinite_literal by auto
define A where "A ≡ N broadcast automata bounds"
define check where "check ≡ has_deadlock A (L⇩0, map_of s⇩0, λ_ . 0)"
define A' where "A' ≡ N
(map renum_acts broadcast)
(map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states) ?automata)
(map (λ(a,p). (renum_vars a, p)) bounds)"
define check' where "check' ≡
has_deadlock A' (map_index renum_states L⇩0, map_of (map (λ(x, v). (renum_vars x, v)) s⇩0), λ_ . 0)"
define renaming_valid where "renaming_valid ≡
Simple_Network_Rename_Formula
broadcast bounds renum_acts renum_vars renum_clocks renum_states ?urge s⇩0 L⇩0 automata ?formula
"
have **[simp]: "check ⟷ check'" if renaming_valid
using that unfolding check_def check'_def A_def A'_def renaming_valid_def
unfolding Simple_Network_Rename_Formula_def
by - (elim conjE,
rule Simple_Network_Language_Renaming.Simple_Network_Rename_Start.has_deadlock_iff'[symmetric])
note [sep_heap_rules] =
certificate_deadlock_check[
of num_split state_space
"map renum_acts broadcast" "map (λ(a,p). (renum_vars a, p)) bounds"
"map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states) ?automata"
m num_states num_actions k "map_index renum_states L⇩0" "map (λ(x, v). (renum_vars x, v)) s⇩0"
"map_formula renum_states renum_vars id ?formula",
folded A'_def renaming_valid_def, folded check'_def, simplified
]
show ?A ?B ?C
using certificate_deadlock_check2[
of num_split state_space
"map renum_acts broadcast" "map (λ(a, p). (renum_vars a, p)) bounds"
"map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states) ?automata"
m num_states num_actions k "map_index renum_states L⇩0" "map (λ(x, v). (renum_vars x, v)) s⇩0"
"map_formula renum_states renum_vars id ?formula",
folded A'_def renaming_valid_def, folded check'_def, simplified
]
using certificate_deadlock_check3[
of num_split state_space
"map renum_acts broadcast" "map (λ(a, p). (renum_vars a, p)) bounds"
"map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states) ?automata"
m num_states num_actions k "map_index renum_states L⇩0" "map (λ(x, v). (renum_vars x, v)) s⇩0"
"map_formula renum_states renum_vars id ?formula",
folded A'_def renaming_valid_def, folded check'_def, simplified
]
unfolding
rename_check_def rename_check2_def rename_check3_def do_rename_mc_def rename_network_def
unfolding if_True
unfolding Simple_Network_Rename_Formula_String_Defs.check_renaming[symmetric] * Let_def
unfolding
A_def[symmetric] check_def[symmetric] renaming_valid_def[symmetric]
by (sep_auto split: bool.splits)+
qed
lemmas [code] = Simple_Network_Impl_nat_defs.states_i_def
export_code rename_check rename_check2 rename_check3 rename_check_buechi in SML module_name Test
export_code rename_check_dbg in SML module_name Test
end