Theory UPPAAL_State_Networks_Impl_Refine
theory UPPAAL_State_Networks_Impl_Refine
imports
Program_Analysis
Munta_Base.Normalized_Zone_Semantics_Impl_Refine
Munta_Base.TA_Impl_Misc
Munta_Base.TA_Syntax_Bundles
begin
unbundle no_library_syntax
section ‹Imperative Implementation of UPPAAL Style Networks›
subsection ‹Executable Successor Computation›
lemma exec_state_length:
assumes "exec prog n (pc, st, s, f, rs) pcs = Some ((pc', st', s', f', rs'), pcs')"
shows "length s = length s'"
using assms
proof (induction prog n "(pc, st, s, f, rs)" pcs arbitrary: pc st s f rs pcs rule: exec.induct)
case 1
then show ?case by simp
next
case prems: (2 prog n pc st m f rs pcs)
from prems(2) show ?case
apply (clarsimp split: option.split_asm if_split_asm)
apply (drule prems(1), assumption+)
by (erule step.elims; simp split: if_split_asm)
qed
locale UPPAAL_Reachability_Problem_precompiled_defs' =
UPPAAL_Reachability_Problem_precompiled_defs +
fixes na :: nat
begin
text ‹Definition of implementation auxiliaries (later connected to the automaton via proof)›
definition
"trans_i_map =
map (map (List.map_filter
(λ (g, a, m, l'). case a of Sil a ⇒ Some (g, a, m, l') | _ ⇒ None)
)) trans"
definition
"trans_in_map ≡
map (map (map
(λ (g, a, m, l'). case a of In a ⇒ (g, a, m, l')) o filter (λ (g, a, m, l').
case a of In a ⇒ True | _ ⇒ False))
) trans"
definition
"trans_out_map ≡
map (map (map
(λ (g, a, m, l'). case a of Out a ⇒ (g, a, m, l')) o filter (λ (g, a, m, l').
case a of Out a ⇒ True | _ ⇒ False))
) trans"
abbreviation
"nested_list_to_iarray xs ≡ IArray (map IArray xs)"
definition
"actions_by_state i ≡ fold (λ t acc. acc[fst (snd t) := (i, t) # (acc ! fst (snd t))])"
definition
"all_actions_by_state t L ≡
fold (λ i. actions_by_state i (t !! i !! (L ! i))) [0..<p] (repeat [] na)"
definition "PROG' pc ≡ (if pc < length prog then (IArray prog) !! pc else None)"
abbreviation "PF ≡ stripfp PROG'"
abbreviation "PT ≡ striptp PROG'"
definition "runf pc s ≡ exec PF max_steps (pc, [], s, True, []) []"
definition "runt pc s ≡ exec PT max_steps (pc, [], s, True, []) []"
lemma PROG'_PROG [simp]:
"PROG' = PROG"
unfolding PROG'_def PROG_def by (rule ext) simp
definition "bounded' s ≡
(∀i<length s. fst (IArray bounds !! i) < s ! i ∧ s ! i < snd (IArray bounds !! i))"
definition
"check_pred L s ≡
list_all
(λ q.
case runf (pred ! q ! (L ! q)) s of
Some ((_, _, _, f, _), _) ⇒ f ∧ bounded' s
| None ⇒ False
)
[0..<p]
"
definition
"make_cconstr pcs = List.map_filter
(λ pc.
case PROG pc of
Some (CEXP ac) ⇒ Some ac
| _ ⇒ None
)
pcs"
definition
"check_g pc s ≡
case runt pc s of
Some ((_, _, _, True, _), pcs) ⇒ Some (make_cconstr pcs)
| _ ⇒ None
"
definition
"trans_i_from ≡ λ (L, s) i.
List.map_filter (λ (g, a, m, l').
case check_g g s of
Some cc ⇒
(case runf m s of
Some ((_, _, s', _, r), _) ⇒
if check_pred (L[i := l']) s'
then Some (cc, a, r, (L[i := l'], s'))
else None
| _ ⇒ None)
| _ ⇒ None)
((IArray (map IArray trans_i_map)) !! i !! (L ! i))"
definition
"trans_i_fun L ≡ concat (map (trans_i_from L) [0..<p])"
definition
"make_reset m1 s ≡
case runf m1 s of
Some ((_, _, _, _, r1), _) ⇒ r1
| None ⇒ []
"
definition
"pairs_by_action ≡ λ (L, s) OUT. concat o
map (λ (i, g1, a, m1, l1). List.map_filter
(λ (j, g2, a, m2, l2).
if i = j then None else
case (check_g g1 s, check_g g2 s) of
(Some cc1, Some cc2) ⇒ (
case runf m2 s of
Some ((_, _, s1, _, r2), _) ⇒ (
case runf m1 s1 of
Some (( _, _, s', _, _), _) ⇒
if check_pred (L[i := l1, j := l2]) s'
then Some (cc1 @ cc2, a, make_reset m1 s @ r2, (L[i := l1, j := l2], s'))
else None
| _ ⇒ None)
| _ ⇒ None)
| _ ⇒ None
)
OUT)
"
definition
"trans_s_fun ≡ λ (L, s).
let
In = all_actions_by_state (nested_list_to_iarray trans_in_map) L;
Out = all_actions_by_state (nested_list_to_iarray trans_out_map) L
in
concat (map (λ a. pairs_by_action (L, s) (Out ! a) (In ! a)) [0..<na])
"
definition
"trans_fun L ≡ trans_s_fun L @ trans_i_fun L"
lemma trans_i_fun_trans_fun:
assumes "(g, a, r, L') ∈ set (trans_i_fun L)"
shows "(g, a, r, L') ∈ set (trans_fun L)"
using assms unfolding trans_fun_def by auto
lemma trans_s_fun_trans_fun:
assumes "(g, a, r, L') ∈ set (trans_s_fun L)"
shows "(g, a, r, L') ∈ set (trans_fun L)"
using assms unfolding trans_fun_def by auto
end
context Prod_TA_Defs
begin
lemma prod_trans_i_alt_def:
"prod_trans_i =
{((L, s), g, a, r, (L', s')) | L s g c a r m L' s'.
(L, g, (a, Networks.label.Act (c, m)), r, L') ∈ Product_TA_Defs.product_trans_i (N_s s) ∧
(∀ q < p. (P ! q) (L ! q) s) ∧ (∀ q < p. (P ! q) (L' ! q) s')
∧ c s ∧ Some s' = m s}"
unfolding
prod_trans_i_def trans_of_def Product_TA_Defs.product_ta_def
Product_TA_Defs.product_trans_def
Product_TA_Defs.product_trans_i_def Product_TA_Defs.product_trans_s_def
by (safe; simp; metis)
lemma prod_trans_s_alt_def:
"prod_trans_s =
{((L, s), g, a, r, (L', s')) | L s g ci co a r mi mo L' s1 s'.
ci s ∧ co s
∧ (∀ q < p. (P ! q) (L ! q) s) ∧ (∀ q < p. (P ! q) (L' ! q) s')
∧ (L, g, (a, Networks.label.Syn (ci, mi) (co, mo)), r, L')
∈ Product_TA_Defs.product_trans_s (N_s s)
∧ Some s' = mi s1 ∧ Some s1 = mo s
}"
unfolding
prod_trans_s_def trans_of_def Product_TA_Defs.product_ta_def
Product_TA_Defs.product_trans_def
Product_TA_Defs.product_trans_i_def
Product_TA_Defs.product_trans_s_def
by (safe; simp; metis)
end
context UPPAAL_Reachability_Problem_precompiled_defs
begin
lemma T_s_unfold_1:
"fst ` equiv.defs.T_s q s = fst ` fst (equiv.N ! q)" if "q < p"
using ‹q < p›
unfolding equiv.defs.T_s_def
unfolding equiv.state_ta_def
unfolding equiv.state_trans_t_def
by force
lemma T_s_unfold_2:
"(snd o snd o snd o snd) ` equiv.defs.T_s q s = (snd o snd o snd o snd) ` fst (equiv.N ! q)"
if "q < p"
using ‹q < p›
unfolding equiv.defs.T_s_def
unfolding equiv.state_ta_def
unfolding equiv.state_trans_t_def
by force
end
lemma (in Equiv_TA_Defs) p_p:
"defs.p = p"
by simp
context
Prod_TA_Defs
begin
lemma states'_alt_def:
"states' s =
{L. length L = p ∧
(∀ q < p. (L ! q) ∈ fst ` (fst (fst A ! q)) ∪ (snd o snd o snd o snd) ` (fst (fst A ! q)))}"
unfolding trans_of_def Product_TA_Defs.product_ta_def N_s_def
unfolding Product_TA_Defs.product_trans_def
unfolding Product_TA_Defs.product_trans_i_def Product_TA_Defs.product_trans_s_def
apply simp
apply safe
unfolding T_s_def
apply (fastforce simp: Product_TA_Defs.states_def trans_of_def p_def)
apply (force simp: Product_TA_Defs.states_def trans_of_def p_def)
by (fastforce simp: Product_TA_Defs.states_def trans_of_def p_def image_iff)
end
context UPPAAL_Reachability_Problem_precompiled
begin
lemma PF_unfold:
"equiv.PF = stripfp (conv_prog PROG)"
using [[show_abbrevs=false]]
unfolding N_def stripfp_def
apply (rule ext)
subgoal for x
apply (cases "PROG x")
apply (solves simp)
subgoal for a
by (cases a) auto
done
done
lemma PT_unfold:
"equiv.PT = striptp (conv_prog PROG)"
using [[show_abbrevs=false]]
unfolding N_def striptp_def
apply (rule ext)
subgoal for x
apply (cases "PROG x")
apply (solves simp)
subgoal for a
by (cases a) auto
done
done
lemma states'I:
"l ∈ equiv.defs.states' s" if "A ⊢ (l, s) ⟶⇗g,a,r⇖ (l', s')"
using equiv.defs.prod_ta_cases[OF that]
unfolding equiv.defs.prod_trans_i_alt_def equiv.defs.prod_trans_s_alt_def
unfolding Product_TA_Defs.product_trans_def
unfolding Product_TA_Defs.product_trans_i_def Product_TA_Defs.product_trans_s_def
by fastforce
lemma A_lengthD:
"length l = p" if "A ⊢ (l, s) ⟶⇗g,a,r⇖ (l', s')"
using that by (auto dest: states'I)
lemma N_s_state_trans:
assumes "equiv.defs.N_s s ! q ⊢ l ! q ⟶⇗g,(a, c, m'),r⇖ l'" "q < p"
obtains f' g' where
"(l ! q, g', (a, c, m'), f', l') ∈ equiv.state_trans q" "g = g' s" "r = f' s"
using assms
unfolding equiv.defs.N_s_def trans_of_def equiv.defs.T_s_def
unfolding equiv.state_ta_def by auto
lemma make_f_collect_store:
assumes "(l, pc_g, a, pc_u, l') ∈ fst (equiv.N ! q)" "c ∈ set (equiv.make_f pc_u s)" "q < p"
shows "c ∈ fst ` collect_store' pc_u"
proof -
from assms(1) ‹q < p› have "(pc_g, a, pc_u, l') ∈ set (trans ! q ! l)"
unfolding N_def T_def by (auto dest!: nth_mem)
from assms obtain pc x2 x3 x4 pcs r where exec:
"exec equiv.PF max_steps (pc_u, [], s, True, []) [] = Some ((pc, x2, x3, x4, r), pcs)"
unfolding equiv.make_f_def by (auto split: option.split_asm) metis
with assms have "c ∈ set r" unfolding equiv.make_f_def by auto
with exec_reset'[OF exec] obtain pc' d where "Some (STOREC c d) = equiv.PF pc'" "pc' ∈ set pcs"
by force
with exec obtain y2 y3 y4 y5 where steps:
"steps equiv.PF max_steps (pc_u, [], s, True, []) (pc', y2, y3, y4, y5)"
by (auto intro: exec_steps')
from ‹_ = equiv.PF pc'› have "pc' < length prog"
unfolding N_def PROG_def stripfp_def by (simp split: if_split_asm)
from steps have "pc' ∈ steps_approx max_steps prog pc_u"
unfolding PF_unfold
unfolding stripfp_def
by (auto simp: PROG_def intro: steps_steps_approx[of stripf, OF _ _ _ ‹pc' < length prog›])
with ‹_ = equiv.PF pc'› ‹_ ∈ set (trans ! q ! l)› show ?thesis
unfolding collect_store'_def stripfp_def N_def PROG_def
apply (clarsimp split: if_split_asm)
apply (cases "prog ! pc'")
apply (simp; fail)
subgoal for x
by (cases x; force)
done
qed
lemma resets_approx:
"set r ⊆
⋃ {fst ` collect_store' r | i g a r. (g, a, r, (l' ! i)) ∈ set (trans ! i ! (l ! i))}"
if "A ⊢ (l, s) ⟶⇗g,a,r⇖ (l', s')"
proof -
from that have [simp]: "length l = p" by (auto dest: A_lengthD)
show ?thesis using that
apply clarsimp
apply (drule equiv.defs.prod_ta_cases)
apply safe
subgoal for x
unfolding equiv.defs.prod_trans_i_alt_def
apply simp
unfolding Product_TA_Defs.product_trans_def
apply safe
unfolding Product_TA_Defs.product_trans_i_def
apply clarsimp
apply (erule N_s_state_trans, assumption)
unfolding equiv.state_trans_t_def
apply clarsimp
subgoal for q l'' pc_g pc_u
apply (frule make_f_collect_store, assumption+)
unfolding N_def T_def
apply (clarsimp dest!: nth_mem)
subgoal premises prems for b j
proof -
from prems(6,8,11-) have
"(pc_g, Sil a, pc_u, l[q := l''] ! q) ∈ set (trans ! q ! (l ! q))"
by simp
with prems(6,8,11-) show ?thesis by blast
qed
done
done
subgoal for x
unfolding equiv.defs.prod_trans_s_alt_def
apply simp
unfolding Product_TA_Defs.product_trans_def
apply safe
unfolding Product_TA_Defs.product_trans_s_def
apply clarsimp
apply (erule N_s_state_trans, assumption)
apply (erule N_s_state_trans, assumption)
unfolding equiv.state_trans_t_def
apply clarsimp
apply (erule disjE)
subgoal for s1 p' q l'' l'aa pc_g pc_ga pc_u pc_ua
apply (frule make_f_collect_store, assumption+)
unfolding N_def T_def
apply (clarsimp dest!: nth_mem)
subgoal premises prems for b j j'
proof -
from prems(9-) have
"(pc_g, In a, pc_u, l[p' := l'', q := l'aa] ! p') ∈ set (trans ! p' ! (l ! p'))"
by simp
with prems(9-) show ?thesis by blast
qed
done
subgoal for s1 q p' l'aa l'' pc_ga pc_g pc_ua pc_u
apply (frule make_f_collect_store, assumption+)
unfolding N_def T_def
apply (clarsimp dest!: nth_mem)
subgoal premises prems for b j j'
proof -
from prems(9-) have
"(pc_g, Out a, pc_u, l[q := l'aa, p' := l''] ! p') ∈ set (trans ! p' ! (l ! p'))"
by simp
with prems(9-) show ?thesis by blast
qed
done
done
done
qed
lemma make_g_clkp_set'':
fixes x
assumes
"(l, pc_g, a, pc_u, l') ∈ fst (equiv.N ! q)" "x ∈ collect_clock_pairs (equiv.make_g pc_g s)"
"q < p"
shows "x ∈ clkp_set'' q l"
proof -
from assms(1) ‹q < p› have "(pc_g, a, pc_u, l') ∈ set (trans ! q ! l)"
unfolding N_def T_def by (auto dest!: nth_mem)
from assms obtain pc x2 x3 x4 r pcs where exec:
"exec equiv.PT max_steps (pc_g, [], s, True, []) [] = Some ((pc, x2, x3, x4, r), pcs)"
unfolding equiv.make_g_def by (auto split: option.split_asm)
with assms have "x ∈ collect_clock_pairs (List.map_filter (λ pc.
case equiv.P pc of
Some (CEXP ac) ⇒ Some ac
| _ ⇒ None
)
pcs)"
unfolding equiv.make_g_def by auto
then obtain pc' ac where
"equiv.P pc' = Some (CEXP ac)" "x = constraint_pair ac" "pc' ∈ set pcs"
unfolding equiv.make_g_def collect_clock_pairs_def set_map_filter
by (clarsimp split: option.split_asm; auto split: instrc.split_asm)
with exec obtain y2 y3 y4 y5 where steps:
"steps equiv.PT max_steps (pc_g, [], s, True, []) (pc', y2, y3, y4, y5)"
by (auto intro: exec_steps')
from ‹equiv.P pc' = _› have "pc' < length prog"
unfolding N_def PROG_def by (simp split: if_split_asm)
from steps have "pc' ∈ steps_approx max_steps prog pc_g"
unfolding PT_unfold
unfolding striptp_def
by (auto simp: PROG_def intro: steps_steps_approx[of stript, OF _ _ _ ‹pc' < length prog›])
with ‹equiv.P pc' = _› ‹_ ∈ set (trans ! q ! l)› ‹x = _› show ?thesis
unfolding clkp_set''_def collect_cexp'_def N_def PROG_def by (force split: if_split_asm)
qed
lemma guard_approx:
"collect_clock_pairs g ⊆
⋃ {clkp_set'' i (l ! i) | i g a r.
(g, a, r, (l' ! i)) ∈ set (trans ! i ! (l ! i)) ∧ l ∈ equiv.defs.states' s ∧ i < p
}"
if "A ⊢ (l, s) ⟶⇗g,a,r⇖ (l', s')"
proof -
from that have [simp]: "length l = p" by (auto dest: A_lengthD)
show ?thesis using that
apply clarsimp
apply (drule equiv.defs.prod_ta_cases)
apply safe
subgoal for x b
unfolding equiv.defs.prod_trans_i_alt_def
apply simp
unfolding Product_TA_Defs.product_trans_def
apply safe
unfolding Product_TA_Defs.product_trans_i_def
apply clarsimp
apply (erule N_s_state_trans, assumption)
unfolding equiv.state_trans_t_def
apply clarsimp
subgoal for q l'' pc_g pc_u
apply (frule make_g_clkp_set'', assumption+)
unfolding N_def T_def
apply (clarsimp dest!: nth_mem)
subgoal premises prems for j
proof -
from prems(6,8,11-) have
"(pc_g, Sil a, pc_u, l[q := l''] ! q) ∈ set (trans ! q ! (l ! q))"
by simp
with prems(6,8,11-) prems show ?thesis by blast
qed
done
done
subgoal for x b
unfolding equiv.defs.prod_trans_s_alt_def
apply simp
unfolding Product_TA_Defs.product_trans_def
apply safe
unfolding Product_TA_Defs.product_trans_s_def
apply clarsimp
apply (erule N_s_state_trans, assumption)
apply (erule N_s_state_trans, assumption)
unfolding equiv.state_trans_t_def
apply clarsimp
apply (drule collect_clock_pairs_append_cases)
apply (erule disjE)
subgoal for s1 p' q l'' l'aa pc_g pc_ga pc_u pc_ua
unfolding equiv.make_c_def
apply (clarsimp split: option.split_asm)
apply (frule make_g_clkp_set'', assumption+)
unfolding N_def T_def
apply (clarsimp dest!: nth_mem)
subgoal premises prems for j j'
proof -
from prems(9-) have
"(pc_g, In a, pc_u, l[p' := l'', q := l'aa] ! p') ∈ set (trans ! p' ! (l ! p'))"
by simp
with prems(9-) show ?thesis by blast
qed
done
subgoal for s1 q p' l'aa l'' pc_ga pc_g pc_ua pc_u
apply (frule make_g_clkp_set'', assumption+)
unfolding N_def T_def
apply (clarsimp dest!: nth_mem)
subgoal premises prems for j j'
proof -
from prems(9-) have
"(pc_g, Out a, pc_u, l[q := l'aa, p' := l''] ! p') ∈ set (trans ! p' ! (l ! p'))"
by simp
with prems(9-) show ?thesis by blast
qed
done
done
done
qed
end
abbreviation "conv B ≡ (conv_prog (fst B), (map conv_A' (fst (snd B))), snd (snd B))"
context UPPAAL_Reachability_Problem_precompiled
begin
sublocale defs':
Equiv_TA_Defs "conv N" max_steps .
lemma equiv_states'_alt_def:
"equiv.defs.states' s =
{L. length L = p ∧
(∀ q < p. L ! q ∈ fst ` fst (equiv.N ! q)
∨ L ! q ∈ (snd o snd o snd o snd) ` fst (equiv.N ! q))}"
unfolding Product_TA_Defs.states_def
unfolding equiv.defs.N_s_def trans_of_def
using T_s_unfold_1 T_s_unfold_2 by simp
lemma init_states:
"init ∈ equiv.defs.states' s⇩0"
using processes_have_trans start_has_trans
unfolding equiv_states'_alt_def
unfolding init_def N_def T_def by force
lemma p_p[simp]:
"defs'.p = p"
unfolding defs'.p_def by simp
lemma T_s_unfold_1':
"fst ` defs'.defs.T_s q s = fst ` fst (defs'.N ! q)" if "q < p"
using ‹q < p›
unfolding defs'.defs.T_s_def
unfolding defs'.state_ta_def
unfolding defs'.state_trans_t_def p_p
by force
lemma T_s_unfold_2':
"(snd o snd o snd o snd) ` defs'.defs.T_s q s = (snd o snd o snd o snd) ` fst (defs'.N ! q)"
if "q < p"
using ‹q < p›
unfolding defs'.defs.T_s_def
unfolding defs'.state_ta_def
unfolding defs'.state_trans_t_def p_p
by force
lemma product_states'_alt_def:
"defs'.defs.states' s =
{L. length L = p ∧
(∀ q < p. L ! q ∈ fst ` fst (defs'.N ! q)
∨ L ! q ∈ (snd o snd o snd o snd) ` fst (defs'.N ! q))}"
unfolding Product_TA_Defs.states_def
unfolding defs'.defs.N_s_def trans_of_def
using T_s_unfold_1' T_s_unfold_2'
by force
lemma states'_conv[simp]:
"defs'.defs.states' s = equiv.defs.states' s"
unfolding product_states'_alt_def equiv_states'_alt_def
unfolding N_def T_def by simp
lemma init_states_defs'[intro]:
"init ∈ defs'.defs.states' s⇩0"
using init_states by simp
lemma
"defs'.I = equiv.I"
by simp
lemma PF_PF[simp]:
"defs'.PF = equiv.PF"
apply simp
unfolding stripfp_def
apply (rule ext)
apply clarsimp
subgoal for x
apply (cases "equiv.P x")
apply simp
subgoal for a
by (cases a) auto
done
done
lemma PF_PROG[simp]:
"equiv.PF = stripfp PROG"
unfolding N_def by simp
lemma I_simp[simp]:
"(equiv.I ! q) l = pred ! q ! l" if "q < p"
unfolding N_def P_def using ‹q < p› process_length(3) by simp
lemma
"defs'.P = conv_prog PROG"
by (simp add: N_def)
lemma states_len[intro]:
assumes
"q < p" "L ∈ equiv.defs.states' s"
shows
"L ! q < length (trans ! q)"
using assms unfolding Product_TA_Defs.states_def
apply simp
unfolding trans_of_def equiv.defs.N_s_def
apply (simp add: T_s_unfold_1[simplified] T_s_unfold_2[simplified])
unfolding N_def
apply simp
unfolding T_def
using state_set
unfolding process_length(2)[symmetric]
apply safe
apply (erule allE)
apply (erule impE)
apply assumption
apply safe
by (clarsimp dest!: nth_mem; force)+
end
locale UPPAAL_Reachability_Problem_precompiled_ceiling =
UPPAAL_Reachability_Problem_precompiled +
fixes k :: "nat list list list"
assumes k_ceiling:
"∀ i < p. ∀ l < length (trans ! i). ∀ (x, m) ∈ clkp_set'' i l. m ≤ k ! i ! l ! x"
"∀ i < p. ∀ l < length (trans ! i). ∀ (x, m) ∈ collect_clock_pairs (inv ! i ! l).
m ≤ k ! i ! l ! x"
and k_resets:
"∀ i < p. ∀ l < length (trans ! i). ∀ (g, a, r, l') ∈ set (trans ! i ! l).
∀ c ∈ {0..<m+1} - fst ` collect_store'' r. k ! i ! l' ! c ≤ k ! i ! l ! c"
and k_length:
"length k = p" "∀ i < p. length (k ! i) = length (trans ! i)"
"∀ xs ∈ set k. ∀ xxs ∈ set xs. length xxs = m + 1"
and k_0:
"∀ i < p. ∀ l < length (trans ! i). k ! i ! l ! 0 = 0"
and guaranteed_resets:
"∀ i < p. ∀ l < length (trans ! i). ∀ (g, a, r, l') ∈ set (trans ! i ! l).
guaranteed_execution_cond prog r max_steps
"
begin
definition "k_fun l c ≡ if c > 0 ∧ c ≤ m then Max {k ! i ! (fst l ! i) ! c | i . i < p} else 0"
lemma p_p':
"equiv.p = p"
by simp
lemma clkp_set_clk_set_subs:
"fst ` clkp_set A (l, s) ⊆ clk_set A"
unfolding TA_clkp_set_unfold by auto
lemma k_ceiling_1:
"∀ l. ∀(x,m) ∈ clkp_set A l. m ≤ k_fun l x"
apply safe
subgoal premises prems for l s x d
proof -
from ‹(x, d) ∈ _› have "0 < x" "x ≤ m"
using clkp_set_clk_set_subs[of l s] clk_set by force+
from prems show ?thesis
unfolding clkp_set_def
apply safe
subgoal
unfolding collect_clki_def
unfolding inv_of_def
unfolding equiv.defs.prod_ta_def
unfolding equiv.defs.prod_invariant_def
unfolding inv_of_def
Product_TA_Defs.product_ta_def
Product_TA_Defs.product_invariant_def
equiv.defs.N_s_def
unfolding length_N
unfolding equiv.state_ta_def
unfolding p_p'
unfolding equiv.state_inv_def
unfolding N_def
unfolding collect_clock_pairs_def
apply (clarsimp cong: if_cong simp: I_def)
subgoal premises prems for l' i
proof -
have "nat d ≤ k ! i ! (l ! i) ! x"
using prems lengths k_ceiling(2)
unfolding collect_clock_pairs_def
by (auto 4 4)
also from ‹_ < p› have "… ≤ Max {k ! i ! (l ! i) ! x |i. i < p}"
by (auto intro: Max_ge)
finally show ?thesis
unfolding k_fun_def using ‹0 < x› ‹x ≤ m› by auto
qed
done
subgoal
unfolding collect_clkt_def
apply clarsimp
subgoal premises prems for g a r l' s'
proof -
from guard_approx[OF prems(2)] prems(1) obtain i g a r where *:
"(x, d) ∈ clkp_set'' i (l ! i)" "(g, a, r, l' ! i) ∈ set (trans ! i ! (l ! i))"
"l ∈ equiv.defs.states' s" "i < p"
by auto
from ‹i < p› ‹l ∈ _› have "l ! i < length (trans ! i)"
by auto
with k_ceiling(1) * have "nat d ≤ k ! i ! (l ! i) ! x"
by force
also from ‹_ < p› have "… ≤ Max {k ! i ! (l ! i) ! x |i. i < p}"
by (auto intro: Max_ge)
finally show ?thesis
unfolding k_fun_def using ‹0 < x› ‹x ≤ m› by auto
qed
done
done
qed
done
lemma k_ceiling_2:
"∀ l g a r l' c. A ⊢ l ⟶⇗g,a,r⇖ l' ∧ c ∉ set r ⟶ k_fun l' c ≤ k_fun l c"
unfolding trans_of_def equiv.defs.prod_ta_def equiv.defs.prod_trans_def
apply clarsimp
apply safe
subgoal premises prems for l s g a r l' s' c
proof -
from prems obtain p' l'' pc_g pc_u where *:
"p' < p" "l' = l[p' := l'']"
"r = equiv.make_f pc_u s" "Some s' = equiv.make_mf pc_u s"
"(l ! p', pc_g, Sil a, pc_u, l'') ∈ fst (equiv.N ! p')"
"l ∈ equiv.defs.states' s"
apply atomize_elim
unfolding equiv.defs.prod_trans_i_def
unfolding Product_TA_Defs.product_ta_def Product_TA_Defs.product_trans_def trans_of_def
apply clarsimp
apply safe
unfolding Product_TA_Defs.product_trans_i_def
unfolding trans_of_def
apply clarsimp
unfolding equiv.defs.N_s_def
unfolding equiv.defs.T_s_def
unfolding Equiv_TA_Defs.state_ta_def
unfolding equiv.state_trans_t_def
unfolding Product_TA_Defs.product_trans_s_def
by auto
from ‹l ∈ _› have [simp]: "length l = p"
by simp
from ‹r = _› have "fst ` collect_store'' pc_u ⊆ set r"
supply find_resets_start.simps[simp del]
unfolding collect_store''_def equiv.make_f_def
apply (clarsimp split: option.split_asm)
subgoal
using ‹Some s' = _› unfolding equiv.make_mf_def
by (auto split: option.split_asm)
subgoal premises prems for pc' g st f pcs c d pc_t pc''
proof -
from prems have
"steps (map_option stripf o (λpc. if pc < size prog then prog ! pc else None)) max_steps
(pc_u, [], s, True, []) (pc', g, st, f, r)"
"prog ! pc' = Some (INSTR HALT)"
unfolding PF_unfold stripfp_def N_def PROG_def
by (auto dest!: exec_steps split: if_split_asm elim!: stripf.elims)
with prems show ?thesis
by (force intro: sym dest!: resets_start')
qed
done
with ‹c ∉ _› have "c ∉ fst ` collect_store'' pc_u" by blast
show ?thesis
proof (cases "c > m")
case True
then show ?thesis
unfolding k_fun_def by auto
next
case False
with ‹c ∉ fst ` _ _› have "c ∈ {0..<m+1} - fst ` collect_store'' pc_u"
by auto
from * have "(l ! p') < length (trans ! p')"
unfolding N_def T_def by auto
from * have "(pc_g, Sil a, pc_u, l'') ∈ set (trans ! p' ! (l ! p'))"
"(l ! p') < length (trans ! p')"
unfolding N_def T_def by auto
with k_resets ‹c ∈ _› ‹p' < _› have "k ! p' ! l'' ! c ≤ k ! p' ! (l ! p') ! c"
unfolding k_fun_def by force
with ‹l' = _› show ?thesis
unfolding k_fun_def
apply clarsimp
apply (rule Max.boundedI)
apply force
using p_gt_0 apply force
apply clarsimp
subgoal for i
apply (cases "i = p'")
apply simp
apply (rule le_trans)
by (auto intro: Max_ge)
done
qed
qed
subgoal premises prems for l s g a r l' s' c
proof -
from prems obtain p1 l1 pc_g1 pc_u1 p2 l2 pc_g2 pc_u2 s'' where *:
"p1 < p" "p2 < p" "l' = l[p1 := l1, p2 := l2]"
"r = equiv.make_f pc_u1 s @ equiv.make_f pc_u2 s"
"Some s' = equiv.make_mf pc_u1 s''" "Some s'' = equiv.make_mf pc_u2 s"
"(l ! p1, pc_g1, In a, pc_u1, l1) ∈ fst (equiv.N ! p1)"
"(l ! p2, pc_g2, Out a, pc_u2, l2) ∈ fst (equiv.N ! p2)"
"l ∈ equiv.defs.states' s"
apply atomize_elim
unfolding equiv.defs.prod_trans_s_def
unfolding Product_TA_Defs.product_ta_def Product_TA_Defs.product_trans_def trans_of_def
apply clarsimp
apply safe
subgoal
unfolding Product_TA_Defs.product_trans_i_def
by auto
unfolding Product_TA_Defs.product_trans_s_def
unfolding trans_of_def
apply clarsimp
unfolding equiv.defs.N_s_def
unfolding equiv.defs.T_s_def
unfolding Equiv_TA_Defs.state_ta_def
unfolding equiv.state_trans_t_def
apply clarsimp
by blast
from ‹l ∈ _› have [simp]: "length l = p"
by simp
from * have **:
"(pc_g1, In a, pc_u1, l1) ∈ set (trans ! p1 ! (l ! p1))" "(l ! p1) < length (trans ! p1)"
"(pc_g2, Out a, pc_u2, l2) ∈ set (trans ! p2 ! (l ! p2))" "(l ! p2) < length (trans ! p2)"
unfolding N_def T_def by auto
with ‹p1 < p› guaranteed_resets have guaranteed_execution:
"guaranteed_execution_cond prog pc_u1 max_steps"
by blast
from ‹r = _› have "fst ` collect_store'' pc_u1 ⊆ set r"
supply find_resets_start.simps[simp del]
unfolding collect_store''_def
equiv.make_f_def
apply (clarsimp split: option.split_asm)
subgoal
using ‹Some s'' = _› unfolding equiv.make_mf_def
by (auto split: option.split_asm)
subgoal
using ‹Some s'' = _› unfolding equiv.make_mf_def
by (auto split: option.split_asm)
subgoal
using ‹Some s' = _› unfolding equiv.make_mf_def
using guaranteed_execution'[OF guaranteed_execution, of "[]" s True "[]" "[]"]
unfolding stripfp_def PROG_def by auto
subgoal premises prems for _ _ _ _ r2 _ pc' g st f r1 pcs c d pc_t pc''
proof -
from prems have
"steps (map_option stripf o (λpc. if pc < size prog then prog ! pc else None)) max_steps
(pc_u1, [], s, True, []) (pc', g, st, f, r1)"
"prog ! pc' = Some (INSTR HALT)" "r = r1 @ r2"
unfolding PF_unfold stripfp_def N_def PROG_def
by (auto dest!: exec_steps split: if_split_asm elim!: stripf.elims)
with prems show ?thesis
by (force intro: sym dest!: resets_start')
qed
done
moreover from ‹r = _› have "fst ` collect_store'' pc_u2 ⊆ set r"
supply find_resets_start.simps[simp del]
unfolding collect_store''_def
equiv.make_f_def
apply (clarsimp split: option.split_asm)
subgoal
using ‹Some s'' = _› unfolding equiv.make_mf_def
by (auto split: option.split_asm)
subgoal
using ‹Some s'' = _› unfolding equiv.make_mf_def
by (auto split: option.split_asm)
subgoal
using ‹Some s' = _› unfolding equiv.make_mf_def
using guaranteed_execution'[OF guaranteed_execution, of "[]" s True "[]" "[]"]
unfolding stripfp_def PROG_def by auto
subgoal premises prems for pc' g st f r1 pcs _ _ _ _ r2 _ c d pc_t pc''
proof -
from prems have
"steps (map_option stripf o (λpc. if pc < size prog then prog ! pc else None)) max_steps
(pc_u2, [], s, True, []) (pc', g, st, f, r1)"
"prog ! pc' = Some (INSTR HALT)" "r = r2 @ r1"
unfolding PF_unfold stripfp_def N_def PROG_def
by (auto dest!: exec_steps split: if_split_asm elim!: stripf.elims)
with prems show ?thesis
by (force intro: sym dest!: resets_start')
qed
done
ultimately have c_not_elem: "c ∉ fst ` collect_store'' pc_u1" "c ∉ fst ` collect_store'' pc_u2"
using ‹c ∉ _› by auto
show ?thesis
proof (cases "c > m")
case True
then show ?thesis
unfolding k_fun_def by auto
next
case False
with c_not_elem have
"c ∈ {0..<m+1} - fst ` collect_store'' pc_u1"
"c ∈ {0..<m+1} - fst ` collect_store'' pc_u2"
by auto
with ** k_resets ‹p1 < _› ‹p2 < _› have
"k ! p1 ! l1 ! c ≤ k ! p1 ! (l ! p1) ! c" "k ! p2 ! l2 ! c ≤ k ! p2 ! (l ! p2) ! c"
by (auto split: prod.split_asm)
with ‹l' = _› show ?thesis
unfolding k_fun_def
apply clarsimp
apply (rule Max.boundedI)
apply force
using p_gt_0 apply force
apply clarsimp
subgoal for i
apply (cases "i = p2")
subgoal
apply simp
apply (rule le_trans)
by (auto intro: Max_ge)
apply (cases "i = p1")
apply simp
apply (rule le_trans)
by (auto intro: Max_ge)
done
qed
qed
done
lemma
shows k_ceiling':
"∀ l. ∀(x,m) ∈ clkp_set A l. m ≤ k_fun l x"
"∀ l g a r l' c. A ⊢ l ⟶⇗g,a,r⇖ l' ∧ c ∉ set r ⟶ k_fun l' c ≤ k_fun l c"
and k_bound':
"∀ l. ∀ i > m. k_fun l i = 0"
and k_0':
"∀ l. k_fun l 0 = 0"
using k_ceiling_1 k_ceiling_2 unfolding k_fun_def by auto
sublocale Reachability_Problem A "(init, s⇩0)" m k_fun "PR_CONST (λ (l, s). F l s)"
by (standard; rule k_ceiling' k_bound' k_0')
end
locale UPPAAL_Reachability_Problem_precompiled_start_state =
UPPAAL_Reachability_Problem_precompiled _ _ _ _ pred
for pred :: "nat list list" +
fixes s⇩0 :: "int list"
assumes start_pred:
"∀ q < p. ∃ pc st s' rs pcs.
exec (stripfp PROG) max_steps ((pred ! q ! (init ! q)), [], s⇩0, True, []) []
= Some ((pc, st, s', True, rs), pcs)"
and bounded: "bounded bounds s⇩0"
and pred_time_indep: "∀ x ∈ set pred. ∀ pc ∈ set x. time_indep_check prog pc max_steps"
and upd_time_indep:
"∀ T ∈ set trans. ∀ xs ∈ set T. ∀ (_, _, pc_u, _) ∈ set xs.
time_indep_check prog pc_u max_steps"
and clock_conj:
"∀ T ∈ set trans. ∀ xs ∈ set T. ∀ (pc_g, _, _, _) ∈ set xs.
conjunction_check prog pc_g max_steps"
begin
lemma B0[intro]:
"bounded defs'.B s⇩0"
using bounded unfolding bounded_def N_def by simp
lemma equiv_P_simp:
"equiv.P = PROG"
unfolding N_def by simp
lemma time_indep_P[intro]:
"time_indep (conv_prog equiv.P) max_steps (pred ! q ! (L ! q), [], s, True, [])"
if "q < p" "L ∈ equiv.defs.states' s"
proof -
from that lengths process_length have "q < length pred" "L ! q < length (pred ! q)" by auto
then have "pred ! q ∈ set pred" "pred ! q ! (L ! q) ∈ set (pred ! q)" by auto
with pred_time_indep time_indep_overapprox show ?thesis
by (auto simp: PROG_def equiv_P_simp)
qed
lemma time_indep_PROG[intro]:
"time_indep (conv_prog PROG) max_steps (pc_u, [], s, True, [])"
if "q < p" "(l, pc_g, a, pc_u, l') ∈ T q"
proof -
from that lengths process_length have
"q < length trans" "l < length (trans ! q)" "(pc_g, a, pc_u, l') ∈ set (trans ! q ! l)"
unfolding T_def by auto
moreover then have "trans ! q ∈ set trans" "trans ! q ! l ∈ set (trans ! q)" by auto
ultimately show ?thesis using upd_time_indep time_indep_overapprox
unfolding PROG_def by blast
qed
lemma facts[intro]:
"u ⊢⇩a ac" if
"q < defs'.p"
"(l, pc_g, a, pc_u, l') ∈ fst (defs'.N ! q)"
"stepst defs'.P max_steps u (pc_g, [], s, True, []) (pc_t, st_t, s_t, True, rs_t)"
"stepsc defs'.P max_steps u (pc_g, [], s, True, []) (pc', st, s', f', rs)"
"defs'.P pc' = Some (CEXP ac)"
proof -
let ?P = "conv_P prog"
from that(5) obtain ac' where
"ac = conv_ac ac'" "prog ! pc' = Some (CEXP ac')" "pc' < length prog"
apply (clarsimp split: option.split_asm if_split_asm simp add: PROG_def N_def)
subgoal for z
by (cases z) auto
done
with that have "u ⊢⇩a conv_ac ac'"
apply -
apply (rule conjunction_check)
using clock_conj apply simp_all
unfolding N_def apply simp_all
using lengths process_length(2) by (force dest!: nth_mem simp: PROG_def N_def T_def)+
with ‹ac = _› show ?thesis by simp
qed
sublocale product':
Equiv_TA "conv N" max_steps init s⇩0
apply standard
apply standard
apply (simp; blast)
subgoal
apply clarsimp
apply (force simp: N_def)
done
apply blast
apply (simp; fail)
unfolding PF_PF using start_pred apply simp
by (rule B0)
lemma fst_S[simp]:
"fst ` (λ(l, g, a, r, l'). (l, map conv_ac g, a, r, l')) ` S = fst ` S"
by force
lemma snd_S[simp]:
"(snd ∘ snd ∘ snd ∘ snd) ` (λ(l, g, a, r, l'). (l, map conv_ac g, a, r, l')) ` S
= (snd ∘ snd ∘ snd ∘ snd) ` S"
by force
end
locale UPPAAL_Reachability_Problem_precompiled' =
UPPAAL_Reachability_Problem_precompiled_start_state +
UPPAAL_Reachability_Problem_precompiled_defs' +
UPPAAL_Reachability_Problem_precompiled_ceiling +
assumes action_set:
"∀ T ∈ set trans. ∀ xs ∈ set T. ∀ (_, a, _) ∈ set xs. pred_act (λ a. a < na) a"
begin
sublocale Reachability_Problem_Impl_Defs _ _ A "(init, s⇩0)" m k_fun "PR_CONST (λ (l, s). F l s)" .
definition
"states' = {(L, s). L ∈ equiv.defs.states' s ∧ check_pred L s ∧ length s = length bounds}"
lemma in_trans_in_mapI:
assumes
"q < p" "l < length (trans ! q)" "i < length (trans ! q ! l)"
"(g1, In a, r1) = trans ! q ! l ! i"
shows "(g1, a, r1) ∈ set (IArray (map IArray trans_in_map) !! q !! l)"
using assms process_length(2) unfolding trans_in_map_def
by (force dest: nth_mem intro!: image_eqI[where x = "(g1, In a, r1)"])
lemma in_trans_out_mapI:
assumes
"q < p" "l < length (trans ! q)" "i < length (trans ! q ! l)"
"(g1, Out a, r1) = trans ! q ! l ! i"
shows "(g1, a, r1) ∈ set (IArray (map IArray trans_out_map) !! q !! l)"
using assms process_length(2) unfolding trans_out_map_def
by (force dest: nth_mem intro!: image_eqI[where x = "(g1, Out a, r1)"])
lemma in_trans_in_mapD:
assumes
"(g1, a, r1) ∈ set (IArray (map IArray trans_in_map) !! q !! l)"
"q < p" "l < length (trans ! q)"
obtains i where
"i < length (trans ! q ! l) ∧ trans ! q ! l ! i = (g1, In a, r1)"
using assms process_length(2) unfolding trans_in_map_def
by (fastforce dest: mem_nth split: act.split_asm)
lemma in_trans_out_mapD:
assumes
"(g1, a, r1) ∈ set (IArray (map IArray trans_out_map) !! q !! l)"
"q < p" "l < length (trans ! q)"
obtains i where
"i < length (trans ! q ! l) ∧ trans ! q ! l ! i = (g1, Out a, r1)"
using assms process_length(2) unfolding trans_out_map_def
by (fastforce dest: mem_nth split: act.split_asm)
lemma in_actions_by_stateI:
assumes
"(g1, a, r1) ∈ set xs" "a < length acc"
shows
"(q, g1, a, r1) ∈ set (actions_by_state q xs acc ! a)
∧ a < length (actions_by_state q xs acc)"
using assms unfolding actions_by_state_def
apply (induction xs arbitrary: acc)
apply (simp; fail)
apply simp
apply (erule disjE)
apply (rule fold_acc_preserv
[where P = "λ acc. (q, g1, a, r1) ∈ set (acc ! a) ∧ a < length acc"]
)
apply (subst list_update_nth_split; auto)
by auto
lemma in_actions_by_state_preserv:
assumes
"(q, g1, a, r1) ∈ set (acc ! a)" "a < length acc"
shows
"(q, g1, a, r1) ∈ set (actions_by_state y xs acc ! a)
∧ a < length (actions_by_state y xs acc)"
using assms unfolding actions_by_state_def
apply -
apply (rule fold_acc_preserv
[where P = "λ acc. (q, g1, a, r1) ∈ set (acc ! a) ∧ a < length acc"]
)
apply (subst list_update_nth_split; auto)
by auto
lemma length_actions_by_state_preserv[simp]:
shows "length (actions_by_state y xs acc) = length acc"
unfolding actions_by_state_def by (auto intro: fold_acc_preserv simp: list_update_nth_split)
lemma in_all_actions_by_stateI:
assumes
"a < na" "q < p" "(g1, a, r1) ∈ set (M !! q !! (L ! q))"
shows
"(q, g1, a, r1) ∈ set (all_actions_by_state M L ! a)"
unfolding all_actions_by_state_def
apply (rule fold_acc_ev_preserv
[where P = "λ acc. (q, g1, a, r1) ∈ set (acc ! a)" and Q = "λ acc. a < length acc",
THEN conjunct1]
)
apply (rule in_actions_by_state_preserv[THEN conjunct1])
using assms by (auto intro: in_actions_by_stateI[THEN conjunct1])
lemma actions_by_state_inj:
assumes "j < length acc"
shows "∀ (q, a) ∈ set (actions_by_state i xs acc ! j). (q, a) ∉ set (acc ! j) ⟶ i = q"
unfolding actions_by_state_def
apply (rule fold_acc_preserv
[where P =
"λ acc'. (∀ (q, a) ∈ set (acc' ! j). (q, a) ∉ set (acc ! j) ⟶ i = q) ∧ j < length acc'",
THEN conjunct1])
subgoal for x acc
by (cases "fst (snd x) = j"; simp)
using assms by auto
lemma actions_by_state_inj':
assumes "j < length acc" "(q, a) ∉ set (acc ! j)" "(q, a) ∈ set (actions_by_state i xs acc ! j)"
shows "i = q"
using actions_by_state_inj[OF assms(1)] assms(2-) by fast
lemma in_actions_by_stateD:
assumes
"(q, g, a, t) ∈ set (actions_by_state i xs acc ! j)" "(q, g, a, t) ∉ set (acc ! j)"
"j < length acc"
shows
"(g, a, t) ∈ set xs ∧ j = a"
using assms unfolding actions_by_state_def
apply -
apply (drule fold_evD
[where y = "(g, a, t)" and Q = "λ acc'. length acc' = length acc"
and R = "λ (_, a', t). a' = j"]
)
apply assumption
apply (subst (asm) list_update_nth_split[of j]; force)
apply simp+
apply (subst (asm) list_update_nth_split[of j]; force)
by auto
lemma in_all_actions_by_stateD:
assumes
"(q, g1, a, r1) ∈ set (all_actions_by_state M L ! a')" "a' < na"
shows
"(g1, a, r1) ∈ set (M !! q !! (L ! q)) ∧ q < p ∧ a' = a"
using assms
unfolding all_actions_by_state_def
apply -
apply (drule fold_evD''[where y = q and Q = "λ acc. length acc = na"])
apply (simp; fail)
apply (drule actions_by_state_inj'[rotated])
apply (simp; fail)+
apply safe
apply (drule in_actions_by_stateD)
apply assumption
apply (rule fold_acc_preserv)
apply (simp; fail)+
subgoal premises prems
proof -
from prems(2) have "q ∈ set [0..<p]" by auto
then show ?thesis by simp
qed
by (auto intro: fold_acc_preserv dest!: in_actions_by_stateD)
lemma length_all_actions_by_state_preserv:
"length (all_actions_by_state M L) = na"
unfolding all_actions_by_state_def by (auto intro: fold_acc_preserv)
lemma less_naI:
assumes
"q < p"
"(g1, a, r1) = trans ! q ! l ! j"
"l < length (trans ! q)"
"j < length (trans ! q ! l)"
shows "pred_act (λa. a < na) a"
using action_set assms process_length(2) by (force dest!: nth_mem)
lemma in_actions_trans_in_mapI:
assumes
"pa < p"
"(g1, In a, r1) = trans ! pa ! (L ! pa) ! j"
"L ! pa < length (trans ! pa)"
"j < length (trans ! pa ! (L ! pa))"
shows "(pa, g1, a, r1) ∈ set (all_actions_by_state (IArray (map IArray trans_in_map)) L ! a)"
apply (rule in_all_actions_by_stateI)
using assms action_set process_length(2) apply (fastforce dest!: nth_mem)
using assms by (fastforce intro: in_trans_in_mapI)+
lemma in_actions_trans_out_mapI:
assumes
"pa < p"
"(g1, Out a, r1) = trans ! pa ! (L ! pa) ! j"
"L ! pa < length (trans ! pa)"
"j < length (trans ! pa ! (L ! pa))"
shows "(pa, g1, a, r1) ∈ set (all_actions_by_state (IArray (map IArray trans_out_map)) L ! a)"
apply (rule in_all_actions_by_stateI)
using assms action_set process_length(2) apply (fastforce dest!: nth_mem)
using assms by (fastforce intro: in_trans_out_mapI)+
lemma in_pairs_by_actionD2:
assumes
"(g, a, r, L', s') ∈ set (pairs_by_action (L, s) xs ys)"
"∀ (q, g, a'', m, l) ∈ set xs. a'' = a'"
"∀ (q, g, a'', m, l) ∈ set ys. a'' = a'"
shows "check_pred L' s'"
using assms(1) unfolding pairs_by_action_def using assms(2,3)
by (clarsimp split: option.split_asm simp: set_map_filter) (clarsimp split: if_split_asm)
lemma in_pairs_by_actionD1:
assumes
"(g, a, r, L', s') ∈ set (pairs_by_action (L, s) xs ys)"
"∀ (q, g, a'', m, l) ∈ set xs. a'' = a'"
"∀ (q, g, a'', m, l) ∈ set ys. a'' = a'"
obtains
pa q pc_g1 pc_g2 g1 g2 r1 r2 pc_u1 pc_u2 l1' l2' s1
x1 x2 x3 x4 x5 y1 y2 y3 y4
where
"pa ≠ q"
"(pa, pc_g1, a, pc_u1, l1') ∈ set ys"
"(q, pc_g2, a, pc_u2, l2') ∈ set xs"
"L' = L[pa := l1', q := l2']"
"runf pc_u1 s1 = Some ((x1, x2, s', x3, x4), x5)"
"runf pc_u2 s = Some ((y1, y2, s1, y3, r2), y4)"
"check_g pc_g1 s = Some g1" "check_g pc_g2 s = Some g2"
"r1 = make_reset pc_u1 s"
"g = g1 @ g2" "r = r1 @ r2"
proof -
obtain
pa q pc_g1 pc_g2 g1 g2 r1 r2 pc_u1 pc_u2 l1' l2' s1
x1 x2 x3 x4 x5 y1 y2 y3 y4
where
"(q, pc_g1, a, pc_u1, l1') ∈ set ys" "(pa, pc_g2, a, pc_u2, l2') ∈ set xs" "q ≠ pa"
"check_g pc_g1 s = Some g1" "check_g pc_g2 s = Some g2"
"runf pc_u1 s1 = Some ((x1, x2, s', x3, x4), x5)"
"runf pc_u2 s = Some ((y1, y2, s1, y3, r2), y4)"
"r1 = make_reset pc_u1 s"
"Some (g1 @ g2, a, r1 @ r2, L[q := l1', pa := l2'], s') = Some (g, a, r, L', s')"
proof -
from assms(1) show ?thesis
unfolding pairs_by_action_def using assms(2,3)
apply clarsimp
unfolding set_map_filter
apply clarsimp
apply (clarsimp split: option.split_asm if_split_asm)
by (force intro!: that)
qed
then show ?thesis by (fast intro: that)
qed
lemma in_pairs_by_actionD:
assumes
"(g, a, r, L', s') ∈ set (pairs_by_action (L, s) xs ys)"
"∀ (q, g, a'', m, l) ∈ set xs. a'' = a'"
"∀ (q, g, a'', m, l) ∈ set ys. a'' = a'"
obtains
pa q pc_g1 pc_g2 p1 p2 g1 g2 r1 r2 pc_u1 pc_u2 l1' l2' s1
x1 x2 x3 x4 x5 y1 y2 y3 y4
where
"pa ≠ q"
"(pa, pc_g1, a, pc_u1, l1') ∈ set ys"
"(q, pc_g2, a, pc_u2, l2') ∈ set xs"
"L' = L[pa := l1', q := l2']"
"runf pc_u1 s1 = Some ((x1, x2, s', x3, x4), x5)"
"runf pc_u2 s = Some ((y1, y2, s1, y3, r2), y4)"
"check_g pc_g1 s = Some g1" "check_g pc_g2 s = Some g2"
"r1 = make_reset pc_u1 s"
"g = g1 @ g2" "r = r1 @ r2"
"check_pred L' s'"
using in_pairs_by_actionD1[OF assms] in_pairs_by_actionD2[OF assms] by metis
lemma in_trans_funD:
assumes "y ∈ set (trans_fun L)"
shows "y ∈ set (trans_s_fun L) ∨ y ∈ set (trans_i_fun L)"
using assms unfolding trans_fun_def by auto
lemma states'_states'[intro]:
"L ∈ equiv.defs.states' s" if "(L, s) ∈ states'"
using that unfolding states'_def by auto
lemma bounded'_bounded:
"bounded' s ⟷ bounded bounds s" if "length s = length bounds"
using that unfolding bounded'_def bounded_def by simp
lemma bounded_bounded':
"bounded bounds s ⟹ bounded' s"
unfolding bounded'_def bounded_def by simp
lemma P_unfold:
"(∀q<p. (equiv.defs.P ! q) (L ! q) s) ⟷ (check_pred L s)" if "length s = length bounds"
unfolding equiv.state_ta_def equiv.state_pred_def check_pred_def using process_length(3) that
apply simp
unfolding list_all_iff
unfolding N_def
unfolding runf_def P_def
by (fastforce split: option.splits simp: bounded'_bounded)
lemma P_unfold_1:
"(∀q<p. (equiv.defs.P ! q) (L ! q) s) ⟹ (check_pred L s)"
unfolding equiv.state_ta_def equiv.state_pred_def check_pred_def using process_length(3)
apply simp
unfolding list_all_iff
unfolding N_def
unfolding runf_def P_def
by (fastforce split: option.split_asm simp: bounded_bounded')
lemma equiv_PT[simp]:
"equiv.PT = PT"
unfolding striptp_def N_def by simp
lemmas [simp] = equiv_P_simp
lemma transD:
assumes
"(pc_g, a, pc_u, l') = trans ! q ! (L ! q) ! j"
"L ! q < length (trans ! q)" "j < length (trans ! q ! (L ! q))"
"q < p"
shows "(L ! q, pc_g, a, pc_u, l') ∈ fst (equiv.N ! q)"
using assms unfolding N_def T_def by simp solve_ex_triv
lemma trans_ND:
assumes
"(L ! q, pc_g, a, pc_u, l') ∈ fst (equiv.N ! q)"
"q < p"
shows
"equiv.defs.N_s s ! q ⊢ L ! q
⟶⇗equiv.make_g pc_g s,(a, equiv.make_c pc_g, equiv.make_mf pc_u),equiv.make_f pc_u s⇖ l'"
using assms
unfolding equiv.defs.N_s_def trans_of_def equiv.defs.T_s_def
unfolding equiv.state_ta_def equiv.state_trans_t_def
by clarsimp solve_ex_triv+
lemma make_f_unfold:
"equiv.make_f pc s = make_reset pc s"
unfolding make_reset_def equiv.make_f_def runf_def by simp
lemma make_g_simp:
assumes "check_g pc_g s = Some g1"
shows "g1 = equiv.make_g pc_g s"
using assms unfolding check_g_def equiv.make_g_def runt_def
by (clarsimp split: option.splits bool.splits simp: make_cconstr_def)
lemma make_c_simp:
assumes "check_g pc_g s = Some g1"
shows "equiv.make_c pc_g s"
using assms unfolding check_g_def equiv.make_c_def runt_def
by (clarsimp split: option.splits bool.splits simp: make_cconstr_def)
lemma make_reset_simp:
assumes "runf pc_u s = Some ((y1, y2, s1, y3, r2), y4)"
shows "make_reset pc_u s = r2"
using assms unfolding runf_def make_reset_def by (auto split: option.splits)
lemma make_mf_simp:
assumes "runf pc_u s = Some ((y1, y2, s1, y3, r2), y4)"
shows "equiv.make_mf pc_u s = Some s1"
using assms unfolding runf_def equiv.make_mf_def by (auto split: option.splits)
lemma trans_fun_trans_of':
"(trans_fun, trans_of A) ∈ transition_rel states'"
unfolding transition_rel_def T_def
apply simp
unfolding trans_of_def
apply safe
subgoal for L s g a r L' s'
unfolding equiv.defs.prod_ta_def equiv.defs.prod_trans_def
apply simp
apply safe
subgoal
apply (rule trans_i_fun_trans_fun)
unfolding equiv.defs.prod_trans_i_alt_def
apply safe
unfolding trans_fun_def trans_i_from_def trans_i_fun_def
unfolding Product_TA_Defs.product_trans_i_def
apply clarsimp
subgoal premises prems for c m p' l'
proof -
from prems have "L ! p' < length (trans ! p')" by auto
from prems obtain pc_g pc_u where
"(L ! p', pc_g, Sil a, pc_u, l') ∈ T p'"
"g = equiv.make_g pc_g s" "r = equiv.make_f pc_u s"
"c = equiv.make_c pc_g" "m = equiv.make_mf pc_u"
unfolding equiv.defs.N_s_def trans_of_def equiv.defs.T_s_def
unfolding equiv.state_ta_def equiv.state_trans_t_def
apply clarsimp
unfolding N_def T_def by clarsimp
from this(1) have "(pc_g, Sil a, pc_u, l') ∈ set (trans ! p' ! (L ! p'))"
unfolding T_def by auto
moreover have "check_g pc_g s = Some g"
using ‹g = _› ‹c = _› ‹c s›
unfolding check_g_def equiv.make_g_def equiv.make_c_def
by (auto split: option.splits simp: runt_def make_cconstr_def)
moreover obtain x1 x2 x3 pcs where "runf pc_u s = Some ((x1, x2, s', x3, r), pcs)"
using ‹r = _› ‹m = _› prems(5)
unfolding equiv.make_f_def equiv.make_mf_def runf_def trans_of_def
by (auto split: option.splits)
moreover have "check_pred (L[p' := l']) s'"
using prems(3) by (auto intro: P_unfold_1)
ultimately show ?thesis using process_length(2) ‹p' < _› ‹L ! p' < _›
by (force simp: set_map_filter trans_i_map_def)
qed
done
subgoal
apply (rule trans_s_fun_trans_fun)
unfolding equiv.defs.prod_trans_s_alt_def
apply safe
unfolding trans_fun_def trans_s_fun_def
unfolding Product_TA_Defs.product_trans_s_def
apply clarsimp
subgoal premises prems for ci co mi mo s1 q1 q2 g1 g2 r1 r2 l1' l2'
proof -
from prems have "L ! q1 < length (trans ! q1)" "L ! q2 < length (trans ! q2)" by auto
from prems obtain pc_g1 pc_u1 where
"(L ! q1, pc_g1, In a, pc_u1, l1') ∈ T q1"
"g1 = equiv.make_g pc_g1 s" "r1 = equiv.make_f pc_u1 s"
"ci = equiv.make_c pc_g1" "mi = equiv.make_mf pc_u1"
unfolding equiv.defs.N_s_def trans_of_def equiv.defs.T_s_def
unfolding equiv.state_ta_def equiv.state_trans_t_def
apply clarsimp
unfolding N_def T_def by clarsimp
from prems obtain pc_g2 pc_u2 where
"(L ! q2, pc_g2, Out a, pc_u2, l2') ∈ T q2"
"g2 = equiv.make_g pc_g2 s" "r2 = equiv.make_f pc_u2 s"
"co = equiv.make_c pc_g2" "mo = equiv.make_mf pc_u2"
unfolding equiv.defs.N_s_def trans_of_def equiv.defs.T_s_def
unfolding equiv.state_ta_def equiv.state_trans_t_def
apply clarsimp
unfolding N_def T_def by clarsimp
from ‹_ ∈ T q1› have "(pc_g1, In a, pc_u1, l1') ∈ set (trans ! q1 ! (L ! q1))"
unfolding T_def by auto
from ‹_ ∈ T q2› have "(pc_g2, Out a, pc_u2, l2') ∈ set (trans ! q2 ! (L ! q2))"
unfolding T_def by auto
moreover have "check_g pc_g1 s = Some g1" "check_g pc_g2 s = Some g2"
using ‹g1 = _› ‹ci = _› ‹ci s› ‹g2 = _› ‹co = _› ‹co s›
unfolding check_g_def equiv.make_g_def equiv.make_c_def
by (auto split: option.splits simp: runt_def make_cconstr_def)
moreover obtain x1 x2 x3 pcs where "runf pc_u2 s = Some ((x1, x2, s1, x3, r2), pcs)"
using ‹r2 = _› ‹mo = _› ‹Some s1 = _›
unfolding equiv.make_f_def equiv.make_mf_def runf_def trans_of_def
by (auto split: option.splits)
moreover obtain x1 x2 x3 x4 pcs where "runf pc_u1 s1 = Some ((x1, x2, s', x3, x4), pcs)"
using ‹r1 = _› ‹mi = _› ‹Some s' = _›
unfolding equiv.make_f_def equiv.make_mf_def runf_def trans_of_def
by (auto split: option.splits)
moreover have "r1 = make_reset pc_u1 s"
using ‹r1 = _› unfolding make_reset_def equiv.make_f_def runf_def by auto
moreover have "check_pred (L[q1 := l1', q2 := l2']) s'"
using prems(5) by (auto intro: P_unfold_1)
moreover have "a < na"
using action_set ‹_ ∈ set (trans ! q1 ! (L ! q1))› ‹q1 < _› ‹L ! q1 < _›
process_length(2)
by (fastforce dest!: nth_mem)
moreover have
"(q1, pc_g1, a, pc_u1, l1')
∈ set (all_actions_by_state (nested_list_to_iarray trans_in_map) L ! a)"
using ‹L ! q1 < _› ‹_ ∈ set (trans ! q1 ! (L ! q1))› ‹q1 < p›
by (force intro: in_actions_trans_in_mapI dest: mem_nth)
moreover have
"(q2, pc_g2, a, pc_u2, l2')
∈ set (all_actions_by_state (nested_list_to_iarray trans_out_map) L ! a)"
using ‹L ! q2 < _› ‹_ ∈ set (trans ! q2 ! (L ! q2))› ‹q2 < p›
by (force intro: in_actions_trans_out_mapI dest: mem_nth)
ultimately show ?thesis
using process_length(2) ‹q1 < _› ‹L ! q1 < _› ‹q2 < _› ‹L ! q2 < _› ‹_ ≠ _›
unfolding pairs_by_action_def
apply -
apply (rule bexI[where x = a])
by auto (force simp: set_map_filter)
qed
done
done
subgoal for L s g a r L' s'
apply (drule in_trans_funD)
apply (erule disjE)
unfolding equiv.defs.prod_ta_def equiv.defs.prod_trans_def
apply simp
apply (rule disjI2)
subgoal
unfolding equiv.defs.prod_trans_s_alt_def
apply safe
unfolding trans_s_fun_def
apply clarsimp
subgoal for x
apply (erule in_pairs_by_actionD[where a' = x])
apply (solves ‹auto dest: in_all_actions_by_stateD›)
apply (solves ‹auto dest: in_all_actions_by_stateD›)
apply (drule in_all_actions_by_stateD, assumption)
apply (drule in_all_actions_by_stateD, assumption)
apply safe
apply (erule in_trans_in_mapD)
apply (simp; fail)
apply blast
apply (erule in_trans_out_mapD)
apply blast
apply blast
apply (simp only: ex_simps[symmetric])
unfolding states'_def
apply (clarsimp)
apply (subst P_unfold, assumption)
apply (subst P_unfold)
subgoal
unfolding runf_def by (auto dest!: exec_state_length)
apply simp
apply (drule transD[rotated 2], solve_triv+, blast)
apply (drule transD[rotated 2], solve_triv+, blast)
apply (drule_tac s = s in trans_ND, assumption)
apply (drule_tac s = s in trans_ND, assumption)
unfolding Product_TA_Defs.product_trans_s_def
apply clarsimp
unfolding trans_of_def
subgoal
apply (simp only: ex_simps[symmetric])
apply defer_ex
apply defer_ex
apply solve_ex_triv
apply solve_ex_triv
apply solve_ex_triv
unfolding make_f_unfold
by (auto simp add: make_c_simp make_mf_simp make_reset_simp make_g_simp[symmetric])
done
done
subgoal
apply simp
apply (rule disjI1)
using process_length(2)
unfolding equiv.defs.prod_trans_i_alt_def
apply simp
unfolding P_unfold
unfolding trans_i_fun_def trans_i_from_def states'_def
apply simp
apply (erule bexE)
unfolding set_map_filter
apply simp
subgoal premises prems for q
proof -
from prems have len: "q < length trans" "L ! q < length (trans ! q)" by auto
from prems(4) obtain pc_g pc_u l' x1 x2 x3 x4 where
"(pc_g, a, pc_u, l') ∈ set (IArray.list_of (map IArray trans_i_map ! q) ! (L ! q))"
"check_g pc_g s = Some g"
"r = make_reset pc_u s"
"runf pc_u s = Some ((x1, x2, s', x3, r), x4)"
"check_pred (L[q := l']) s'"
"L' = L[q := l']"
apply atomize_elim
unfolding make_reset_def
by (force split: option.splits if_split_asm)
moreover then have
"(L, g, (a, Networks.label.Act (equiv.make_c pc_g, equiv.make_mf pc_u)), r, L')
∈ Product_TA_Defs.product_trans_i (equiv.defs.N_s s)"
unfolding Product_TA_Defs.product_trans_i_def
apply clarsimp
apply solve_ex_triv
apply safe
using prems apply simp
unfolding trans_i_map_def
using len ‹q < p› apply (clarsimp simp: set_map_filter)
apply (clarsimp split: act.split_asm)
apply (frule make_c_simp)
apply (drule mem_nth)
apply safe
apply (drule transD[rotated], solve_triv+)
apply (drule trans_ND)
apply solve_triv
apply (subst make_g_simp)
using ‹q < p› prems(1) by (auto simp add: make_f_unfold)
ultimately show ?thesis
apply (subst P_unfold)
subgoal
using prems(1) by fast
apply (subst P_unfold)
subgoal
using ‹runf _ _ = _› prems(1)
unfolding runf_def by (auto dest!: exec_state_length)
using prems(1) by (force simp: make_mf_simp dest: make_c_simp)
qed
done
done
done
lemma transition_rel_mono:
"(a, b) ∈ transition_rel B" if "(a, b) ∈ transition_rel C" "B ⊆ C"
using that unfolding transition_rel_def b_rel_def fun_rel_def by auto
end
context
Equiv_TA_Defs
begin
lemma state_set_subs:
"state_set (trans_of (defs.product s''))
⊆ {L. length L = defs.p ∧ (∀q<defs.p. L ! q ∈ State_Networks.state_set (fst (defs.N ! q)))}"
unfolding defs.states'_alt_def[symmetric]
unfolding defs.N_s_def
unfolding state_set_def Product_TA_Defs.states_def
unfolding trans_of_def
unfolding Product_TA_Defs.product_ta_def Product_TA_Defs.product_trans_def
unfolding Product_TA_Defs.product_trans_i_def Product_TA_Defs.product_trans_s_def
unfolding defs.T_s_def
unfolding Product_TA_Defs.states_def trans_of_def
apply simp
apply safe
apply (simp; fail)
using [[goals_limit = 1]]
apply force
apply force
apply (force simp: image_iff)
apply force
subgoal for x _ _ _ _ _ _ L p g _ _ _ r l' q
apply (cases "p = q")
apply (force simp: image_iff)
apply (force simp: image_iff)
done
apply force
subgoal for _ _ _ _ _ _ _ _ p q g1 g2 _ _ _ _ _ r1 r2 l1' l2' qa
apply (cases "qa = q")
apply force
apply (cases "qa = p")
by (force simp: image_iff)+
done
end
context UPPAAL_Reachability_Problem_precompiled_defs
begin
lemma N_s_state_indep:
assumes "(L ! q, g, a, r, l') ∈ map trans_of (equiv.defs.N_s s) ! q" "q < p"
obtains g r where "(L ! q, g, a, r, l') ∈ map trans_of (equiv.defs.N_s s') ! q"
using assms unfolding trans_of_def equiv.defs.N_s_def equiv.defs.T_s_def by force
lemma fst_product_state_indep:
"fst ` fst (equiv.defs.product s) = fst ` fst (equiv.defs.product s')"
unfolding Product_TA_Defs.product_ta_def Product_TA_Defs.product_trans_def
unfolding Product_TA_Defs.product_trans_s_def Product_TA_Defs.product_trans_i_def
apply simp
unfolding equiv.defs.states'_alt_def
apply clarsimp
apply (rule equalityI)
subgoal
apply (rule subsetI)
apply clarsimp
apply (erule disjE)
apply (erule conjE exE)+
apply (erule N_s_state_indep)
apply (simp; fail)
apply (rule img_fst)
apply (rule Set.UnI1)
apply (subst mem_Collect_eq)
apply solve_ex_triv+
apply (erule conjE exE)+
apply (erule N_s_state_indep, (simp; fail))
apply (erule N_s_state_indep, (simp; fail))
apply (rule img_fst)
apply (rule Set.UnI2)
apply (subst mem_Collect_eq)
apply (rule exI)+
apply (rule conjI)
defer
by solve_ex_triv+
subgoal
apply (rule subsetI)
apply clarsimp
apply (erule disjE)
apply (erule conjE exE)+
apply (erule N_s_state_indep)
apply (simp; fail)
apply (rule img_fst)
apply (rule Set.UnI1)
apply (subst mem_Collect_eq)
apply solve_ex_triv+
apply (erule conjE exE)+
apply (erule N_s_state_indep, (simp; fail))
apply (erule N_s_state_indep, (simp; fail))
apply (rule img_fst)
apply (rule Set.UnI2)
apply (subst mem_Collect_eq)
apply (rule exI)+
apply (rule conjI)
defer
by solve_ex_triv+
done
lemma last_product_state_indep:
"(snd o snd o snd o snd) ` fst (equiv.defs.product s)
= (snd o snd o snd o snd) ` fst (equiv.defs.product s')"
unfolding Product_TA_Defs.product_ta_def Product_TA_Defs.product_trans_def
unfolding Product_TA_Defs.product_trans_s_def Product_TA_Defs.product_trans_i_def
apply simp
unfolding equiv.defs.states'_alt_def
apply clarsimp
apply (rule equalityI)
subgoal
apply (rule subsetI)
apply clarsimp
apply (erule disjE)
apply (erule conjE exE)+
apply (erule N_s_state_indep)
apply (simp; fail)
apply (rule image_eqI)
prefer 2
apply (rule Set.UnI1)
apply (subst mem_Collect_eq)
apply solve_ex_triv+
apply (erule conjE exE)+
apply (erule N_s_state_indep, (simp; fail))
apply (erule N_s_state_indep, (simp; fail))
apply (rule image_eqI)
defer
apply (rule Set.UnI2)
apply (subst mem_Collect_eq)
apply (rule exI)+
apply (rule conjI)
defer
apply solve_ex_triv+
defer
apply (rule HOL.refl)
by simp
subgoal
apply (rule subsetI)
apply clarsimp
apply (erule disjE)
apply (erule conjE exE)+
apply (erule N_s_state_indep)
apply (simp; fail)
apply (rule image_eqI)
prefer 2
apply (rule Set.UnI1)
apply (subst mem_Collect_eq)
apply solve_ex_triv+
apply (erule conjE exE)+
apply (erule N_s_state_indep, (simp; fail))
apply (erule N_s_state_indep, (simp; fail))
apply (rule image_eqI)
defer
apply (rule Set.UnI2)
apply (subst mem_Collect_eq)
apply (rule exI)+
apply (rule conjI)
defer
apply solve_ex_triv+
defer
apply (rule HOL.refl)
by simp
done
lemma state_set_T':
"state_set (equiv.defs.T' s'') ⊇ fst ` state_set (trans_of A)"
unfolding trans_of_def
unfolding state_set_def
unfolding Prod_TA_Defs.prod_ta_def equiv.defs.prod_trans_def
apply simp
unfolding equiv.defs.prod_trans_i_def equiv.defs.prod_trans_s_def
unfolding trans_of_def
apply safe
apply (subst fst_product_state_indep; force)
apply (subst fst_product_state_indep; force)
apply (subst (asm) last_product_state_indep[simplified]; force)
by (subst (asm) last_product_state_indep[simplified]; force)
lemma state_set_T'2:
"length L = equiv.defs.p"
"∀q<equiv.defs.p. L ! q ∈ State_Networks.state_set (fst (equiv.defs.N ! q))"
if "(L, s) ∈ state_set (trans_of A)"
using subset_trans [OF state_set_T' equiv.state_set_subs] that by blast+
lemma state_set_states':
"L ∈ equiv.defs.states' s" if "(L, s) ∈ state_set (trans_of A)"
using state_set_T'2[OF that] unfolding equiv.defs.states'_alt_def by simp
lemma state_set_pred:
"∀q<p. (equiv.defs.P ! q) (L ! q) s" if "(L, s) ∈ state_set (trans_of A)"
using that
unfolding Normalized_Zone_Semantics_Impl_Refine.state_set_def
unfolding trans_of_def Prod_TA_Defs.prod_ta_def Prod_TA_Defs.prod_trans_def
unfolding Prod_TA_Defs.prod_trans_i_def Prod_TA_Defs.prod_trans_s_def
by force
end
context UPPAAL_Reachability_Problem_precompiled'
begin
lemma bounded_bounded'':
"bounded bounds s ⟹ length s = length bounds"
unfolding bounded'_def bounded_def by simp
lemma P_bounded:
"(∀q<p. (equiv.defs.P ! q) (L ! q) s) ⟹ bounded bounds s"
unfolding equiv.state_ta_def equiv.state_pred_def check_pred_def using process_length(3) p_gt_0
apply simp
unfolding list_all_iff
unfolding N_def
unfolding runf_def P_def
apply (drule spec[of _ 0])
by (simp split: option.split; auto split: option.split_asm)
lemma P_state_length:
"(∀q<p. (equiv.defs.P ! q) (L ! q) s) ⟹ length s = length bounds"
by (intro P_bounded bounded_bounded'')
lemma state_set_state_length:
"length s = length bounds" if "(L, s) ∈ state_set (trans_of A)"
using that unfolding state_set_def
apply (safe dest!: equiv.defs.prod_ta_cases)
unfolding equiv.defs.prod_trans_i_alt_def equiv.defs.prod_trans_s_alt_def
by safe (auto dest: P_state_length)
lemma state_set_states:
"state_set (trans_of A) ⊆ states'"
using state_set_states' state_set_pred unfolding states'_def
by (auto intro: P_unfold_1 state_set_state_length)
lemma p_p_2[simp]:
"defs'.defs.p = p"
unfolding defs'.p_p p_p ..
lemma len_product'_N[simp]:
"length defs'.defs.N = p"
unfolding defs'.defs.p_def[symmetric] by (rule p_p_2)
lemma len_equiv_N:
"length equiv.defs.N = p"
unfolding equiv.defs.p_def[symmetric] by simp
lemma
"defs'.p = p"
unfolding defs'.p_def by simp
lemma equiv_p_p: "equiv.p = p"
by simp
lemma init_states:
"init ∈ equiv.defs.states' s⇩0"
using processes_have_trans start_has_trans
unfolding equiv_states'_alt_def
unfolding init_def N_def T_def by force
lemma start_pred':
"check_pred init s⇩0"
using start_pred bounded unfolding check_pred_def runf_def list_all_iff
by (fastforce split: option.split intro: bounded_bounded')
lemma start_states':
"(init, s⇩0) ∈ states'"
using start_pred' init_states bounded unfolding states'_def bounded_def by auto
lemma trans_fun_trans_of[intro, simp]:
"(trans_fun, trans_of A) ∈ transition_rel states"
using trans_fun_trans_of' state_set_states start_states' unfolding transition_rel_def by blast
definition
"inv_fun ≡ λ (L, _). concat (map (λ i. IArray (map IArray inv) !! i !! (L ! i)) [0..<p])"
lemma states_states':
"states ⊆ states'"
using state_set_states start_states' by auto
lemma states'_length[simp]:
"length L = p" if "(L, s) ∈ states'"
using that unfolding states'_def by auto
lemma inv_simp:
"I q (L ! q) = inv ! q ! (L ! q)" if "q < p" "(L, s) ∈ states'"
unfolding I_def using that states'_states'[OF that(2)] lengths by (auto dest!: states_len)
lemma inv_fun_inv_of':
"(inv_fun, inv_of A) ∈ inv_rel Id states'"
unfolding inv_rel_def
apply (clarsimp simp: equiv.defs.inv_of_simp Product_TA_Defs.inv_of_product)
using process_length(1)
unfolding inv_fun_def Product_TA_Defs.product_invariant_def init_def
unfolding equiv.defs.N_s_def
apply simp
apply (rule arg_cong[where f = concat])
unfolding inv_of_def Equiv_TA_Defs.state_ta_def apply simp
unfolding equiv.state_inv_def N_def Equiv_TA_Defs.state_inv_def
by (auto simp: inv_simp)
lemma inv_rel_mono:
"(a, b) ∈ inv_rel Id B" if "(a, b) ∈ inv_rel Id C" "B ⊆ C"
using that unfolding inv_rel_def b_rel_def fun_rel_def by auto
lemma inv_fun_inv_of[intro, simp]:
"(inv_fun, inv_of A) ∈ inv_rel Id states"
using inv_fun_inv_of' states_states' by (rule inv_rel_mono)
definition "final_fun ≡ λ (L, s). hd_of_formula formula L s"
lemma final_fun_final':
"(final_fun, (λ (l, s). F l s)) ∈ inv_rel Id states'"
unfolding F_def final_fun_def inv_rel_def in_set_member[symmetric] list_ex_iff
by (force dest!: states'_states')
lemma final_fun_final[intro, simp]:
"(final_fun, (λ (l, s). F l s)) ∈ inv_rel Id states"
using final_fun_final' states_states' by (rule inv_rel_mono)
lemma fst_clkp_setD:
assumes "(c, d) ∈ clkp_set A l"
shows "c > 0" "c ≤ m" "d ∈ range int"
using assms clock_set consts_nats clkp_set'_subs
unfolding Nats_def clk_set'_def TA_clkp_set_unfold by force+
lemma init_has_trans:
"(init, s⇩0) ∈ fst ` (trans_of A) ⟷ trans_fun (init, s⇩0) ≠ []"
apply standard
using trans_fun_trans_of unfolding transition_rel_def apply force
using trans_fun_trans_of' start_states' unfolding transition_rel_def by fast
end
context UPPAAL_Reachability_Problem_precompiled'
begin
abbreviation "k_i ≡ IArray (map (IArray o (map (IArray o map int))) k)"
definition
"k_impl ≡ λ (l, _). IArray (map (λ c. Max {k_i !! i !! (l ! i) !! c | i. i < p}) [0..<m+1])"
lemma k_impl_alt_def:
"k_impl =
(λ (l, _). IArray (map (λ c. Max ((λ i. k_i !! i !! (l ! i) !! c) ` {0..<p})) [0..<m+1]))"
proof -
have "{i. i < p} = {0..<p}"
by auto
then show ?thesis unfolding k_impl_def setcompr_eq_image by auto
qed
lemma k_length_alt:
"∀ i < p. ∀ j < length (k ! i). length (k ! i ! j) = m + 1"
using k_length(1,3) by (auto dest: nth_mem)
lemma Max_int_commute:
"int (Max S) = Max (int ` S)" if "finite S" "S ≠ {}"
apply (rule mono_Max_commute)
apply standard
using that by auto
lemma k_impl_k'[intro]:
"k_impl (l, s) = IArray (k' (l, s))" if "(l, s) ∈ states'"
proof -
have l_len[simp]: "l ! i < length (trans ! i)" if "i < p" for i
using ‹i < p› ‹(l, s) ∈ _› by auto
have *: "k_i !! i !! (l ! i) !! c = k ! i ! (l ! i) ! c"
if "c ≤ m" "i < p" for c i
proof -
from k_length_alt that k_length(1,2) have "length (k ! i ! (l ! i)) = m + 1"
by auto
with that k_length process_length(2) processes_have_trans start_has_trans show ?thesis
unfolding init_def by auto
qed
show ?thesis
unfolding k_impl_def k'_def k_fun_def
apply clarsimp
apply safe
subgoal
apply (subst Max_int_commute)
subgoal
by auto
subgoal
using p_gt_0 by auto
apply (rule arg_cong[where f = Max])
apply safe
using * apply (solves auto)
by (solves ‹auto simp add: *[symmetric]›)
subgoal
apply (rule Max_eqI)
apply (solves auto)
using k_length_alt k_length processes_have_trans k_0 p_gt_0 unfolding init_def
apply (solves auto)
using k_length_alt k_length processes_have_trans k_0 p_gt_0 unfolding init_def
apply clarsimp
apply (rule exI[where x = 0])
by simp
subgoal
apply (subst Max_int_commute)
subgoal
by auto
subgoal
using p_gt_0 by auto
apply (rule arg_cong[where f = Max])
apply safe
using * apply (solves auto)
by (solves ‹auto simp add: *[symmetric]›)
done
qed
lemma k_impl_k'2[intro]:
"k_impl (l, s) = IArray (k' (l, s))" if
"(l, s) ∈ Normalized_Zone_Semantics_Impl_Refine.state_set (trans_of A)"
using that states_states' by auto
lemma k_impl_k'_0[intro]:
"k_impl (init, s⇩0) = IArray (k' (init, s⇩0))"
using states_states' by auto
sublocale impl:
Reachability_Problem_Impl
where trans_fun = trans_fun
and trans_impl = trans_fun
and inv_fun = inv_fun
and F_fun = final_fun
and ceiling = k_impl
and A = A
and l⇩0 = "(init, s⇩0)"
and l⇩0i = "(init, s⇩0)"
and F = "PR_CONST ((λ (l, s). F l s))"
and n = m
and k = k_fun
and loc_rel = Id
and show_clock = "show"
and show_state = "show"
and states' = states
unfolding PR_CONST_def
apply standard
apply (fastforce simp: inv_rel_def b_rel_def)
subgoal
by auto (metis IdI list_rel_id_simp relAPP_def)
by (fastforce simp: inv_rel_def b_rel_def)+
lemma F_reachable_correct':
"impl.op.F_reachable
⟷ (∃ L' s' u u'.
conv_A A ⊢' ⟨(init, s⇩0), u⟩ →* ⟨(L', s'), u'⟩
∧ (∀ c ∈ {1..m}. u c = 0) ∧ check_bexp φ L' s'
)" if "formula = formula.EX φ"
using that E_op''.E_from_op_reachability_check[of F_rel "PR_CONST (λ(x, y). F x y)",
unfolded F_rel_def, OF HOL.refl]
reachability_check
unfolding impl.E_op_F_reachable E_op''.F_reachable_def E_op''.reachable_def
unfolding F_rel_def unfolding F_def by force
lemma PT_PT:
"defs'.PT = equiv.PT"
apply simp
unfolding striptp_def
apply (rule ext)
apply clarsimp
subgoal for x
apply (cases "PROG x")
apply (simp; fail)
subgoal for a
by (cases a) auto
done
done
lemma P_P[simp]:
"defs'.defs.P = equiv.defs.P"
unfolding Equiv_TA_Defs.state_ta_def
unfolding Equiv_TA_Defs.p_def
unfolding Equiv_TA_Defs.state_pred_def
using PF_PF by (auto split: option.split)
lemma map_map_filter:
"map f (List.map_filter g xs) = List.map_filter (map_option f o g) xs"
by (induction xs; simp add: List.map_filter_simps split: option.split)
lemma make_g_conv:
"defs'.make_g = conv_cc oo equiv.make_g"
unfolding Equiv_TA_Defs.make_g_def PT_PT PF_PF apply simp
apply (intro ext)
apply (clarsimp split: option.splits simp: map_map_filter)
apply (rule arg_cong2[where f = List.map_filter])
by (auto split: option.split instrc.split)
lemma make_c_conv:
"defs'.make_c = equiv.make_c"
unfolding Equiv_TA_Defs.make_c_def PT_PT by simp
lemma make_f_conv:
"defs'.make_f = equiv.make_f"
unfolding Equiv_TA_Defs.make_f_def PF_PF by simp
lemma make_mf_conv:
"defs'.make_mf = equiv.make_mf"
unfolding Equiv_TA_Defs.make_mf_def PF_PF by simp
lemmas make_convs = make_g_conv make_c_conv make_f_conv make_mf_conv
lemma state_trans_conv:
"Equiv_TA_Defs.state_trans_t (conv N) max_steps q
= (λ (a, b, c). (a, λ x. conv_cc (b x), c)) ` equiv.state_trans q" if ‹q < p›
unfolding Equiv_TA_Defs.state_trans_t_def image_Collect
using ‹q < _› make_convs by (force split: prod.splits)+
lemma map_conv_t:
"map trans_of (defs'.defs.N_s s) ! q = conv_t ` (map trans_of (equiv.defs.N_s s) ! q)"
if ‹q < p›
using ‹q < p›
apply (subst nth_map)
unfolding defs'.defs.N_s_length p_p_2
apply assumption
apply (subst nth_map)
unfolding equiv.defs.N_s_length
apply simp
unfolding trans_of_def Prod_TA_Defs.N_s_def
unfolding len_equiv_N len_product'_N
apply simp
unfolding Prod_TA_Defs.T_s_def
unfolding image_Collect
unfolding Equiv_TA_Defs.state_ta_def Equiv_TA_Defs.p_def
apply simp
using state_trans_conv[of q]
apply simp
apply safe
apply force
apply solve_ex_triv+
unfolding image_iff by force
lemma product_trans_t_conv:
"Product_TA_Defs.product_trans_s (defs'.defs.N_s s)
= conv_t ` Product_TA_Defs.product_trans_s (equiv.defs.N_s s)"
unfolding Product_TA_Defs.product_trans_s_def
apply (simp only: states'_conv)
apply safe
apply (simp only: equiv.states'_len_simp equiv_p_p map_conv_t)
unfolding image_Collect
apply (simp split: prod.split)
apply safe
subgoal
by defer_ex solve_ex_triv+
subgoal
by solve_ex_triv+ (force simp only: equiv.states'_len_simp equiv_p_p map_conv_t)
done
lemma product_trans_t_conv':
"Product_TA_Defs.product_trans_i (defs'.defs.N_s s)
= conv_t ` Product_TA_Defs.product_trans_i (equiv.defs.N_s s)"
unfolding Product_TA_Defs.product_trans_i_def
apply (simp only: states'_conv)
apply safe
apply (simp only: equiv.states'_len_simp equiv_p_p map_conv_t)
unfolding image_Collect
apply (simp split: prod.split)
apply safe
subgoal
by defer_ex solve_ex_triv+
subgoal
by solve_ex_triv+ (force simp only: equiv.states'_len_simp equiv_p_p map_conv_t)
done
lemma prod_trans_s_conv:
"defs'.defs.prod_trans_s = conv_t ` equiv.defs.prod_trans_s"
unfolding defs'.defs.prod_trans_s_alt_def
unfolding equiv.defs.prod_trans_s_alt_def
unfolding product_trans_t_conv
unfolding p_p_2 P_P
apply simp
apply safe
unfolding p_p P_P
apply (simp add: image_Collect)
apply solve_ex_triv
subgoal
apply defer_ex
apply defer_ex
by solve_ex_triv+
subgoal
apply defer_ex
apply defer_ex
by solve_ex_triv+
done
lemma prod_trans_i_conv:
"defs'.defs.prod_trans_i = conv_t ` equiv.defs.prod_trans_i"
unfolding defs'.defs.prod_trans_i_alt_def
unfolding equiv.defs.prod_trans_i_alt_def
unfolding product_trans_t_conv'
unfolding p_p_2 P_P
apply simp
apply safe
unfolding p_p P_P
apply (simp add: image_Collect)
apply solve_ex_triv
subgoal
apply defer_ex
apply defer_ex
by solve_ex_triv+
subgoal
apply defer_ex
apply defer_ex
by solve_ex_triv+
done
lemma prod_trans_conv:
"defs'.defs.prod_trans = conv_t ` equiv.defs.prod_trans"
unfolding defs'.defs.prod_trans_def
unfolding equiv.defs.prod_trans_def
unfolding prod_trans_s_conv
unfolding prod_trans_i_conv image_Un ..
lemma prod_invariant_conv:
"defs'.defs.prod_invariant = (map conv_ac ∘∘ Prod_TA_Defs.prod_invariant) EA"
apply (rule ext)
apply safe
unfolding defs'.defs.prod_invariant_def equiv.defs.prod_invariant_def
unfolding Product_TA_Defs.product_ta_def inv_of_def
apply simp
unfolding Product_TA_Defs.product_invariant_def List.map_concat
apply (simp add: Prod_TA_Defs.N_s_length)
unfolding Equiv_TA_Defs.p_p Equiv_TA_Defs.p_def apply simp
apply (rule cong[where f = concat])
apply (rule HOL.refl)
unfolding Prod_TA_Defs.N_s_def inv_of_def Equiv_TA_Defs.state_ta_def
unfolding Equiv_TA_Defs.p_def unfolding Equiv_TA_Defs.state_inv_def
by (simp split: prod.split)
lemma prod_conv: "defs'.defs.prod_ta = conv_A A"
unfolding defs'.defs.prod_ta_def
unfolding equiv.defs.prod_ta_def
unfolding conv_A_def
by (simp add: prod_invariant_conv[symmetric] prod_trans_conv[symmetric])
lemma F_reachable_correct:
"impl.op.F_reachable
⟷ (∃ L' s' u u'.
conv N ⊢⇩max_steps ⟨init, s⇩0, u⟩ →* ⟨L', s', u'⟩
∧ (∀ c ∈ {1..m}. u c = 0) ∧ check_bexp φ L' s'
)" if "formula = formula.EX φ" "start_inv_check"
unfolding F_reachable_correct'[OF that(1)]
apply (subst product'.prod_correct[symmetric])
using prod_conv p_p p_gt_0 apply simp
using prod_conv p_p p_gt_0 apply simp
using F_reachable_equiv[OF that(2)]
by (simp add: F_def, simp add: that(1))
definition
"reachability_checker_old ≡
worklist_algo2_impl
impl.subsumes_impl impl.a⇩0_impl impl.F_impl impl.succs_impl impl.emptiness_check_impl"
definition
"reachability_checker' ≡
pw_impl
(return o fst) impl.state_copy_impl impl.tracei impl.subsumes_impl impl.a⇩0_impl impl.F_impl
impl.succs_impl impl.emptiness_check_impl"
theorem reachability_check':
"(uncurry0 reachability_checker',
uncurry0 (
Refine_Basic.RETURN (∃ L' s' u u'.
conv_A A ⊢' ⟨(init, s⇩0), u⟩ →* ⟨(L', s'), u'⟩
∧ (∀ c ∈ {1..m}. u c = 0) ∧ check_bexp φ L' s'
)
)
)
∈ unit_assn⇧k →⇩a bool_assn" if "formula = formula.EX φ"
using impl.pw_impl_hnr_F_reachable
unfolding reachability_checker'_def F_reachable_correct'[OF that] .
corollary reachability_checker'_hoare:
"<emp> reachability_checker'
<λ r. ↑(r = (∃ L' s' u u'.
conv_A A ⊢' ⟨(init, s⇩0), u⟩ →* ⟨(L', s'), u'⟩
∧ (∀ c ∈ {1..m}. u c = 0) ∧ check_bexp φ L' s'
))
>⇩t" if "formula = formula.EX φ"
apply (rule cons_post_rule)
using reachability_check'[OF that, to_hnr] apply (simp add: hn_refine_def)
by (sep_auto simp: pure_def)
definition reachability_checker where
"reachability_checker ≡ do
{
init_sat ← impl.start_inv_check_impl;
if init_sat then do
{ x ← reachability_checker';
return (if x then REACHABLE else UNREACHABLE)
}
else
return INIT_INV_ERR
}"
theorem reachability_check:
"(uncurry0 reachability_checker,
uncurry0 (
Refine_Basic.RETURN (
if start_inv_check
then
if
(
∃ L' s' u u'.
conv N ⊢⇩max_steps ⟨init, s⇩0, u⟩ →* ⟨L', s', u'⟩
∧ (∀ c ∈ {1..m}. u c = 0) ∧ check_bexp φ L' s'
)
then REACHABLE
else UNREACHABLE
else INIT_INV_ERR
)
))
∈ unit_assn⇧k →⇩a id_assn" if "formula = formula.EX φ"
apply (simp only: F_reachable_correct[OF that, symmetric] cong: if_cong)
supply
impl.pw_impl_hnr_F_reachable
[unfolded reachability_checker'_def[symmetric], to_hnr, unfolded hn_refine_def,
rule_format, sep_heap_rules]
supply
impl.start_inv_check_impl.refine[to_hnr, unfolded hn_refine_def, rule_format, sep_heap_rules]
unfolding reachability_checker_def
by sepref_to_hoare (sep_auto simp: pure_def)
corollary reachability_checker_hoare:
"<emp> reachability_checker
<λ r. ↑(r =
(
if start_inv_check
then
if
(
∃ L' s' u u'.
conv N ⊢⇩max_steps ⟨init, s⇩0, u⟩ →* ⟨L', s', u'⟩
∧ (∀ c ∈ {1..m}. u c = 0) ∧ check_bexp φ L' s'
)
then REACHABLE
else UNREACHABLE
else INIT_INV_ERR
)
)
>⇩t" if "formula = formula.EX φ"
apply (rule cons_post_rule)
using reachability_check[OF that, to_hnr] apply (simp add: hn_refine_def)
by (sep_auto simp: pure_def)
lemma list_all_concat:
"list_all Q (concat xxs) ⟷ (∀ xs ∈ set xxs. list_all Q xs)"
unfolding list_all_iff by auto
lemma inv_of_init_unfold:
"u ⊢ inv_of (conv_A A) (init, s⇩0) ⟷ (∀ i < p. u ⊢ conv_cc (inv ! i ! 0))"
proof -
have *: "inv_of (conv_A A) (init, s⇩0) = conv_cc (equiv.defs.I' s⇩0 init)"
using equiv.defs.inv_of_simp[of init s⇩0]
unfolding inv_of_def conv_A_def by (auto split: prod.split)
have "u ⊢ inv_of (conv_A A) (init, s⇩0) ⟷ (∀ i < p. u ⊢ conv_cc (I i 0))"
unfolding * Product_TA_Defs.inv_of_product Product_TA_Defs.product_invariant_def
apply (simp only: product'.prod.length_L p_p_2 cong: list.map_cong_simp)
unfolding equiv.defs.N_s_def length_N
apply (simp cong: list.map_cong_simp)
unfolding inv_of_def
apply (simp cong: list.map_cong_simp)
unfolding init_def
apply (simp cong: list.map_cong_simp)
unfolding Equiv_TA_Defs.state_ta_def
apply (simp cong: list.map_cong_simp)
unfolding equiv.state_inv_def
unfolding N_def
by (force simp: map_concat list_all_concat clock_val_def cong: list.map_cong_simp)
also have "(∀ i < p. u ⊢ conv_cc (I i 0)) ⟷ (∀ i < p. u ⊢ conv_cc (inv ! i ! 0))"
unfolding I_def using lengths processes_have_trans by fastforce
finally show ?thesis .
qed
corollary reachability_checker_hoare':
"<emp> reachability_checker
<λ r. ↑(r =
(
if (∀u. (∀c∈{1..m}. u c = 0) ⟶ (∀ i < p. u ⊢ conv_cc (inv ! i ! 0)))
then
if
(
∃ L' s' u u'.
conv N ⊢⇩max_steps ⟨init, s⇩0, u⟩ →* ⟨L', s', u'⟩
∧ (∀ c ∈ {1..m}. u c = 0) ∧ check_bexp φ L' s'
)
then REACHABLE
else UNREACHABLE
else INIT_INV_ERR
)
)
>⇩t" if "formula = formula.EX φ"
using reachability_checker_hoare[OF that] unfolding start_inv_check_correct inv_of_init_unfold .
subsubsection ‹Post-processing›
schematic_goal succs_impl_alt_def:
"impl.succs_impl ≡ ?impl"
unfolding impl.succs_impl_def
unfolding k_impl_alt_def
apply (abstract_let
"λ (l, _ :: int list). IArray (map (λ c. MAX i∈{0..<p}. k_i !! i !! (l ! i) !! c) [0..<m+1])"
k_i
)
apply (abstract_let "inv_fun :: nat list × int list ⇒ (nat, int) acconstraint list" inv_fun)
apply (abstract_let "trans_fun" trans_fun)
unfolding inv_fun_def[abs_def] trans_fun_def[abs_def] trans_s_fun_def trans_i_fun_def trans_i_from_def
apply (abstract_let "IArray (map IArray inv)" inv)
apply (abstract_let "IArray (map IArray trans_out_map)" trans_out_map)
apply (abstract_let "IArray (map IArray trans_in_map)" trans_in_map)
apply (abstract_let "IArray (map IArray trans_in_map)" trans_in_map)
by (rule Pure.reflexive)
lemma reachability_checker'_alt_def':
"reachability_checker' ≡
let
key = return ∘ fst;
sub = impl.subsumes_impl;
copy = impl.state_copy_impl;
start = impl.a⇩0_impl;
final = impl.F_impl;
succs = impl.succs_impl;
empty = impl.emptiness_check_impl;
trace = impl.tracei
in pw_impl key copy trace sub start final succs empty"
unfolding reachability_checker'_def by simp
schematic_goal reachability_checker_alt_def:
"reachability_checker ≡ ?impl"
unfolding reachability_checker_def
unfolding reachability_checker'_alt_def' impl.succs_impl_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 k_impl_alt_def
apply (abstract_let k_i k_i)
apply (abstract_let "inv_fun :: nat list × int list ⇒ (nat, int) acconstraint list" )
apply (abstract_let "trans_fun" trans_fun)
unfolding impl.init_dbm_impl_def impl.a⇩0_impl_def
unfolding impl.F_impl_def
unfolding final_fun_def[abs_def]
unfolding impl.subsumes_impl_def
unfolding impl.emptiness_check_impl_def
unfolding impl.state_copy_impl_def
by (rule Pure.reflexive)
end
lemmas [code] = UPPAAL_Reachability_Problem_precompiled'.k_impl_def
paragraph ‹Some post refinements›
code_thms "fw_upd'"
code_thms fw_impl'
code_thms fw_impl
abbreviation plus_int :: "int ⇒ int ⇒ int" where
"plus_int a b ≡ a + b"
fun dbm_add_int :: "int DBMEntry ⇒ int DBMEntry ⇒ int DBMEntry"
where
"dbm_add_int ∞ _ = ∞" |
"dbm_add_int _ ∞ = ∞" |
"dbm_add_int (Le a) (Le b) = (Le (plus_int a b))" |
"dbm_add_int (Le a) (Lt b) = (Lt (plus_int a b))" |
"dbm_add_int (Lt a) (Le b) = (Lt (plus_int a b))" |
"dbm_add_int (Lt a) (Lt b) = (Lt (plus_int a b))"
lemma dbm_add_int:
"dbm_add = dbm_add_int"
apply (rule ext)+
subgoal for x y
by (cases x; cases y) auto
done
definition
"fw_upd'_int m k i j =
Refine_Basic.RETURN
(op_mtx_set m (i, j)
(min (op_mtx_get m (i, j)) (dbm_add_int (op_mtx_get m (i, k)) (op_mtx_get m (k, j)))))"
definition
"fw_upd_impl_int n ≡ λai bib bia bi. do {
xa ← mtx_get (Suc n) ai (bia, bib);
xb ← mtx_get (Suc n) ai (bib, bi);
x ← mtx_get (Suc n) ai (bia, bi);
let e = (dbm_add_int xa xb);
if e < x then mtx_set (Suc n) ai (bia, bi) e else Heap_Monad.return ai
}"
lemma fw_upd_impl_int_eq:
"fw_upd_impl_int = fw_upd_impl"
unfolding fw_upd_impl_int_def fw_upd_impl_def
unfolding dbm_add_int add
unfolding Let_def ..
definition
"fw_impl_int n ≡
imp_for' 0 (n + 1)
(λxb. imp_for' 0 (n + 1)
(λxd. imp_for' 0 (n + 1) (λxf σ'''''. fw_upd_impl_int n σ''''' xb xd xf)))"
lemma fw_impl'_int:
"fw_impl = fw_impl_int"
unfolding fw_impl_def fw_impl_int_def
unfolding fw_upd_impl_int_eq ..
context UPPAAL_Reachability_Problem_precompiled_defs'
begin
definition "run_impl program pc s ≡ exec program max_steps (pc, [], s, True, []) []"
lemma runf_impl:
"runf = run_impl PF"
unfolding runf_def run_impl_def ..
lemma runt_impl:
"runt = run_impl PT"
unfolding runt_def run_impl_def ..
definition
"make_cconstr_impl program pcs =
List.map_filter
(λpc. case program pc of None ⇒ None | Some (INSTR x) ⇒ Map.empty x
| Some (CEXP ac) ⇒ Some ac)
pcs"
lemma make_cconstr_impl:
"make_cconstr = make_cconstr_impl PROG"
unfolding make_cconstr_def make_cconstr_impl_def ..
definition
"check_g_impl programf program pc s ≡
case run_impl programf pc s of None ⇒ None
| Some ((x, xa, xb, True, xc), pcs) ⇒ Some (make_cconstr_impl program pcs)
| Some ((x, xa, xb, False, xc), pcs) ⇒ None"
lemma check_g_impl:
"check_g = check_g_impl PT PROG'"
unfolding check_g_impl_def check_g_def runt_impl PROG'_PROG make_cconstr_impl ..
definition
"make_reset_impl program m1 s ≡
case run_impl program m1 s of
Some ((_, _, _, _, r1), _) ⇒ r1
| None ⇒ []
"
lemma make_reset_impl:
"make_reset = make_reset_impl PF"
unfolding make_reset_def make_reset_impl_def runf_impl ..
definition
"check_pred_impl program bnds L s ≡
list_all
(λq. case run_impl program (pred ! q ! (L ! q)) s of None ⇒ False
| Some ((x, xa, xb, f, xc), xd) ⇒
f ∧ (∀i<length s. fst (bnds !! i) < s ! i ∧ s ! i < snd (bnds !! i)))
[0..<p]"
lemma check_pred_impl:
"check_pred = check_pred_impl PF (IArray bounds)"
unfolding check_pred_def check_pred_impl_def runf_impl bounded'_def ..
definition
"pairs_by_action_impl pf pt porig bnds ≡ λ (L, s) OUT. concat o
map (λ (i, g1, a, m1, l1). List.map_filter
(λ (j, g2, a, m2, l2).
if i = j then None else
case (check_g_impl pt porig g1 s, check_g_impl pt porig g2 s) of
(Some cc1, Some cc2) ⇒
(case run_impl pf m2 s of
Some ((_, _, s1, _, r2), _) ⇒
(case run_impl pf m1 s1 of
Some (( _, _, s', _, _), _) ⇒
if check_pred_impl pf bnds (L[i := l1, j := l2]) s'
then Some (cc1 @ cc2, a, make_reset_impl pf m1 s @ r2, (L[i := l1, j := l2], s'))
else None
| _ ⇒ None)
| _ ⇒ None)
| _ ⇒ None
)
OUT)"
lemma pairs_by_action_impl:
"pairs_by_action = pairs_by_action_impl PF PT PROG' (IArray bounds)"
unfolding pairs_by_action_def pairs_by_action_impl_def
unfolding check_g_impl make_reset_impl check_pred_impl runf_impl ..
definition
"all_actions_by_state_impl upt_p empty_ran i L ≡
fold (λia. actions_by_state ia (i !! ia !! (L ! ia))) upt_p empty_ran"
lemma all_actions_by_state_impl:
"all_actions_by_state = all_actions_by_state_impl [0..<p] (repeat [] na)"
unfolding all_actions_by_state_def all_actions_by_state_impl_def ..
definition
"trans_i_from_impl programf programt program bnds trans_i_array ≡
λ(L, s) i.
List.map_filter
(λ(g, a, m, l').
case check_g_impl programt program g s of None ⇒ None
| Some cc ⇒
(case run_impl programf m s of None ⇒ None
| Some ((xx, xa, s', xb, r), xc) ⇒
if check_pred_impl programf (IArray bounds) (L[i := l']) s'
then Some (cc, a, r, L[i := l'], s') else None))
(trans_i_array !! i !! (L ! i))"
lemma trans_i_from_impl:
"trans_i_from = trans_i_from_impl PF PT PROG' (IArray bounds) (IArray (map IArray trans_i_map))"
unfolding trans_i_from_def trans_i_from_impl_def
unfolding check_g_impl runf_impl check_pred_impl ..
end
context UPPAAL_Reachability_Problem_precompiled'
begin
lemma PF_alt_def:
"PF = (λ pc. if pc < length prog then (IArray (map (map_option stripf) prog)) !! pc else None)"
unfolding stripfp_def PROG'_def by auto
lemma PT_alt_def:
"PT = (λ pc. if pc < length prog then (IArray (map (map_option stript) prog)) !! pc else None)"
unfolding striptp_def PROG'_def by auto
schematic_goal reachability_checker_alt_def_refined:
"reachability_checker ≡ ?impl"
unfolding reachability_checker_alt_def
unfolding fw_impl'_int
unfolding inv_fun_def trans_fun_def trans_s_fun_def trans_i_fun_def
unfolding trans_i_from_impl
unfolding runf_impl runt_impl check_g_impl pairs_by_action_impl check_pred_impl
apply (abstract_let "IArray (map IArray inv)" inv)
apply (abstract_let "IArray (map IArray trans_out_map)" trans_out_map)
apply (abstract_let "IArray (map IArray trans_in_map)" trans_in_map)
apply (abstract_let "IArray (map IArray trans_i_map)" trans_i_map)
apply (abstract_let "IArray bounds" bounds)
apply (abstract_let PF PF)
apply (abstract_let PT PT)
unfolding PF_alt_def PT_alt_def
apply (abstract_let PROG' PROG')
unfolding PROG'_def
apply (abstract_let "length prog" len_prof)
apply (abstract_let "IArray (map (map_option stripf) prog)" prog_f)
apply (abstract_let "IArray (map (map_option stript) prog)" prog_t)
apply (abstract_let "IArray prog" prog)
unfolding all_actions_by_state_impl
apply (abstract_let "[0..<p]")
apply (abstract_let "[0..<na]")
apply (abstract_let "{0..<p}")
apply (abstract_let "[0..<m+1]")
by (rule Pure.reflexive)
end
subsection ‹Check Preconditions›
context UPPAAL_Reachability_Problem_precompiled_defs
begin
abbreviation
"check_nat_subs ≡ ∀ (_, d) ∈ clkp_set'. d ≥ 0"
lemma check_nat_subs:
"check_nat_subs ⟷ snd ` clkp_set' ⊆ ℕ"
unfolding Nats_def apply safe
subgoal for _ _ b using rangeI[of int "nat b"] by auto
by auto
definition
"check_resets ≡ ∀ x c. Some (INSTR (STOREC c x)) ∈ set prog ⟶ x = 0"
lemma check_resets_alt_def:
"check_resets =
(∀ (c, x) ∈ collect_store. x = 0)"
unfolding check_resets_def collect_store_def by auto
definition
"check_pre ≡
length inv = p ∧ length trans = p ∧ length pred = p
∧ (∀ i < p. length (pred ! i) = length (trans ! i) ∧ length (inv ! i) = length (trans ! i))
∧ (∀ T ∈ set trans. ∀ xs ∈ set T. ∀ (_, _, _, l) ∈ set xs. l < length T)
∧ p > 0 ∧ m > 0
∧ (∀ i < p. trans ! i ≠ []) ∧ (∀ q < p. trans ! q ! 0 ≠ [])
∧ check_nat_subs ∧ clk_set' = {1..m}
∧ check_resets
"
lemma finite_clkp_set'[intro, simp]:
"finite clkp_set'"
unfolding clkp_set'_def
using [[simproc add: finite_Collect]]
by (auto intro!: finite_vimageI simp: inj_on_def)
lemma check_pre:
"UPPAAL_Reachability_Problem_precompiled p m inv pred trans prog ⟷ check_pre"
unfolding
UPPAAL_Reachability_Problem_precompiled_def
check_pre_def check_nat_subs check_resets_def
by auto
end
context UPPAAL_Reachability_Problem_precompiled_defs
begin
context
fixes k :: "nat list list list"
begin
definition
"check_ceiling ≡
UPPAAL_Reachability_Problem_precompiled_ceiling_axioms p m max_steps inv trans prog k"
lemma check_axioms:
"UPPAAL_Reachability_Problem_precompiled_ceiling p m max_steps inv pred trans prog k
⟷ check_pre ∧ check_ceiling"
unfolding UPPAAL_Reachability_Problem_precompiled_ceiling_def check_pre check_ceiling_def
by auto
end
end
lemmas [code] =
UPPAAL_Reachability_Problem_precompiled_defs.collect_cexp_alt_def
UPPAAL_Reachability_Problem_precompiled_defs.collect_store_alt_def
UPPAAL_Reachability_Problem_precompiled_defs.check_resets_alt_def
export_code UPPAAL_Reachability_Problem_precompiled_defs.collect_cexp in SML module_name Test
lemmas [code] =
UPPAAL_Reachability_Problem_precompiled_defs.check_pre
UPPAAL_Reachability_Problem_precompiled_defs.check_axioms
UPPAAL_Reachability_Problem_precompiled_defs.clkp_set'_alt_def
UPPAAL_Reachability_Problem_precompiled_defs.clk_set'_alt_def
UPPAAL_Reachability_Problem_precompiled_defs.check_pre_def
UPPAAL_Reachability_Problem_precompiled_defs.check_ceiling_def
UPPAAL_Reachability_Problem_precompiled_defs.init_def
lemmas [code] =
UPPAAL_Reachability_Problem_precompiled_defs'.trans_out_map_def
UPPAAL_Reachability_Problem_precompiled_defs'.trans_in_map_def
UPPAAL_Reachability_Problem_precompiled_defs'.trans_i_map_def
UPPAAL_Reachability_Problem_precompiled_defs'.all_actions_by_state_def
UPPAAL_Reachability_Problem_precompiled_defs'.actions_by_state_def
UPPAAL_Reachability_Problem_precompiled_defs'.pairs_by_action_def
code_pred clock_val_a .
concrete_definition reachability_checker_impl
uses UPPAAL_Reachability_Problem_precompiled'.reachability_checker_alt_def_refined
lemmas [code] =
UPPAAL_Reachability_Problem_precompiled_defs'.make_cconstr_def
UPPAAL_Reachability_Problem_precompiled_defs'.make_reset_def
UPPAAL_Reachability_Problem_precompiled_defs'.check_pred_def
UPPAAL_Reachability_Problem_precompiled_defs'.check_g_def
UPPAAL_Reachability_Problem_precompiled_defs'.runf_def
UPPAAL_Reachability_Problem_precompiled_defs'.runt_def
UPPAAL_Reachability_Problem_precompiled_defs.PROG_def
lemmas [code] =
UPPAAL_Reachability_Problem_precompiled_defs.P_def
lemma exec_code[code]:
"exec prog n (pc, st, m, f, rs) pcs =
(case n of 0 ⇒ None
| Suc n ⇒
(case prog pc of None ⇒ None
| Some instr ⇒
if instr = HALT
then Some ((pc, st, m, f, rs), pc # pcs)
else
(case UPPAAL_Asm.step instr (pc, st, m, f, rs) of
None ⇒ None | Some s ⇒ exec prog n s (pc # pcs))))"
by (cases n) auto
lemmas [code] =
UPPAAL_Reachability_Problem_precompiled'_axioms_def
UPPAAL_Reachability_Problem_precompiled'_def
pred_act_def
definition
"init_pred_check ≡ λ p prog max_steps pred s⇩0.
(∀ q < p.
case (exec
(stripfp (UPPAAL_Reachability_Problem_precompiled_defs.PROG prog))
max_steps
((pred ! q ! (UPPAAL_Reachability_Problem_precompiled_defs.init p ! q)), [], s⇩0, True, [])
[])
of Some ((pc, st, s', True, rs), pcs) ⇒ True | _ ⇒ False)
"
definition
"time_indep_check1 ≡ λ pred prog max_steps.
(∀x∈set pred. ∀pc∈set x. time_indep_check prog pc max_steps)
"
definition
"time_indep_check2 ≡ λ trans prog max_steps.
(∀T∈set trans. ∀xs∈set T. ∀(_, _, pc_u, _)∈set xs. time_indep_check prog pc_u max_steps)
"
definition
"conjunction_check2 ≡ λ trans prog max_steps.
(∀T∈set trans. ∀xs∈set T. ∀(pc_g, _, _, _)∈set xs. conjunction_check prog pc_g max_steps)
"
lemma start_pred[code]:
"UPPAAL_Reachability_Problem_precompiled_start_state_axioms = (λ p max_steps trans prog bounds pred s⇩0.
init_pred_check p prog max_steps pred s⇩0
∧ bounded bounds s⇩0
∧ time_indep_check1 pred prog max_steps
∧ time_indep_check2 trans prog max_steps
∧ conjunction_check2 trans prog max_steps
)"
unfolding UPPAAL_Reachability_Problem_precompiled_start_state_axioms_def
unfolding init_pred_check_def bounded_def time_indep_check1_def time_indep_check2_def
conjunction_check2_def
apply (rule ext)+
apply safe
apply (fastforce split: option.split_asm bool.split_asm)
subgoal premises prems
using prems(1,7) by (fastforce split: option.split_asm bool.split_asm)
done
export_code UPPAAL_Reachability_Problem_precompiled_start_state_axioms
context UPPAAL_Reachability_Problem_precompiled_defs
begin
lemma collect_store''_alt_def:
"collect_store'' pc ≡
case find_resets_start prog pc of
None ⇒ {} |
Some pc' ⇒
⋃ (
(λ cmd. case cmd of Some (INSTR (STOREC c x)) ⇒ {(c, x)} | _ ⇒ {}) `
((!) prog) ` {pc .. pc'}
)"
unfolding collect_store''_def
apply (rule eq_reflection)
apply safe
subgoal
apply (simp del: find_resets_start.simps split: option.split_asm)
by (auto intro: sym intro!: bexI split: option.split)
subgoal
apply (clarsimp simp del: find_resets_start.simps split: option.split_asm)
by (auto intro: sym split: instrc.split_asm instr.split_asm)
done
lemma collect_cexp'_alt_def:
"collect_cexp' pc ≡
⋃ ((λ cmd. case cmd of Some (CEXP ac) ⇒ {ac} | _ ⇒ {}) `
((!) prog) ` steps_approx max_steps prog pc
)"
unfolding collect_cexp'_def
by (auto 4 3 intro!: eq_reflection bexI intro: sym split: option.splits instrc.split_asm)
end
lemmas [code] =
UPPAAL_Reachability_Problem_precompiled_defs'.PROG'_def
UPPAAL_Reachability_Problem_precompiled_start_state_def
UPPAAL_Reachability_Problem_precompiled_ceiling_axioms_def
UPPAAL_Reachability_Problem_precompiled_defs.N_def
UPPAAL_Reachability_Problem_precompiled_defs.collect_store''_alt_def
UPPAAL_Reachability_Problem_precompiled_defs.clkp_set''_def
UPPAAL_Reachability_Problem_precompiled_defs.collect_cexp'_alt_def
UPPAAL_Reachability_Problem_precompiled_defs'.pairs_by_action_impl_def
UPPAAL_Reachability_Problem_precompiled_defs'.make_reset_impl_def
UPPAAL_Reachability_Problem_precompiled_defs'.check_g_impl_def
UPPAAL_Reachability_Problem_precompiled_defs'.run_impl_def
UPPAAL_Reachability_Problem_precompiled_defs'.make_cconstr_impl_def
UPPAAL_Reachability_Problem_precompiled_defs'.check_pred_impl_def
UPPAAL_Reachability_Problem_precompiled_defs'.all_actions_by_state_impl_def
UPPAAL_Reachability_Problem_precompiled_defs'.trans_i_from_impl_def
lemmas [code] =
Equiv_TA_Defs.state_ta_def Prod_TA_Defs.N_s_def Product_TA_Defs.states_def
export_code UPPAAL_Reachability_Problem_precompiled'_axioms in SML module_name Test
export_code UPPAAL_Reachability_Problem_precompiled' in SML module_name Test
hide_const check_and_verify
definition [code]:
"check_and_verify p m k max_steps I T prog final bounds P s⇩0 na ≡
if UPPAAL_Reachability_Problem_precompiled' p m max_steps I T prog bounds P s⇩0 na k
then
reachability_checker_impl p m max_steps I T prog bounds P s⇩0 na k final
⤜ (λ x. return (Some x))
else return None"
abbreviation "N ≡ UPPAAL_Reachability_Problem_precompiled_defs.N"
theorem reachability_check:
"(uncurry0 (check_and_verify p m k max_steps I T prog (formula.EX formula) bounds P s⇩0 na),
uncurry0 (
Refine_Basic.RETURN (
if UPPAAL_Reachability_Problem_precompiled' p m max_steps I T prog bounds P s⇩0 na k
then Some (
if (∀u. (∀c∈{1..m}. u c = 0) ⟶ (∀ i < p. u ⊢ conv_cc (I ! i ! 0)))
then
if
(
∃ L' s' u u'.
conv (N p I P T prog bounds) ⊢⇩max_steps
⟨repeat 0 p, s⇩0, u⟩ →* ⟨L', s', u'⟩
∧ (∀ c ∈ {1..m}. u c = 0) ∧ check_bexp formula L' s'
)
then REACHABLE
else UNREACHABLE
else INIT_INV_ERR
)
else None
)
)
)
∈ unit_assn⇧k →⇩a id_assn"
proof -
define A where "A ≡ conv (N p I P T prog bounds)"
define start_inv where
"start_inv ≡ (∀u. (∀c∈{1..m}. u c = 0) ⟶ (∀ i < p. u ⊢ conv_cc (I ! i ! 0)))"
define reach where
"reach ≡
∃ L' s' u u'.
A ⊢⇩max_steps
⟨repeat 0 p, s⇩0, u⟩ →* ⟨L', s', u'⟩
∧ (∀ c ∈ {1..m}. u c = 0) ∧ check_bexp formula L' s'"
note [sep_heap_rules] =
UPPAAL_Reachability_Problem_precompiled'.reachability_checker_hoare'
[ OF _ HOL.refl[of "formula.EX formula"],
unfolded UPPAAL_Reachability_Problem_precompiled_defs.init_def,
of p m max_steps I T prog bounds P s⇩0 na k,
unfolded A_def[symmetric] start_inv_def[symmetric] reach_def[symmetric]
]
show ?thesis
unfolding A_def[symmetric] start_inv_def[symmetric] reach_def[symmetric]
unfolding check_and_verify_def
by sepref_to_hoare (sep_auto simp: reachability_checker_impl.refine[symmetric])
qed
export_code open
check_and_verify init_pred_check time_indep_check1 time_indep_check1 conjunction_check2
checking SML_imp
end