Theory UPPAAL_Model_Checking
theory UPPAAL_Model_Checking
imports
UPPAAL_State_Networks_Impl_Refine
Munta_Base.TA_More
Munta_Base.Abstract_Term
begin
hide_const models
inductive step_u' ::
"('a, 't :: time, 's) unta ⇒ nat ⇒ 's list ⇒ int list ⇒ (nat, 't) cval
⇒ 's list ⇒ int list ⇒ (nat, 't) cval ⇒ bool"
("_ ⊢⇧_ ⟨_, _, _⟩ → ⟨_, _, _⟩" [61,61,61,61,61,61] 61) where
"A ⊢⇧n ⟨L, s, u⟩ → ⟨L'', s'', u''⟩" if
"A ⊢⇩n ⟨L, s, u⟩ →⇘Del⇙ ⟨L', s', u'⟩" "a ≠ Del" "A ⊢⇩n ⟨L', s', u'⟩ →⇘a⇙ ⟨L'', s'', u''⟩"
inductive steps_un' ::
"('a, 't :: time, 's) unta ⇒ nat ⇒ 's list ⇒ int list ⇒ (nat, 't) cval
⇒ 's list ⇒ int list ⇒ (nat, 't) cval ⇒ bool"
("_ ⊢⇧_ ⟨_, _, _⟩ →* ⟨_, _, _⟩" [61,61,61,61,61,61] 61)
where
refl: "A ⊢⇧n ⟨L, s, u⟩ →* ⟨L, s, u⟩" |
step: "A ⊢⇧n ⟨L, s, u⟩ →* ⟨L', s', u'⟩ ⟹ A ⊢⇧n ⟨L', s', u'⟩ → ⟨L'', s'', u''⟩
⟹ A ⊢⇧n ⟨L, s, u⟩ →* ⟨L'', s'', u''⟩"
declare steps_un'.intros[intro]
lemma stepI2:
"A ⊢⇧n ⟨L, s, u⟩ →* ⟨L'', s'', u''⟩" if
"A ⊢⇧n ⟨L', s', u'⟩ →* ⟨L'', s'', u''⟩" "A ⊢⇧n ⟨L, s, u⟩ → ⟨L', s', u'⟩"
using that by induction auto
context Equiv_TA
begin
lemma prod_correct'_action:
"(∃ a. defs.prod_ta ⊢ ⟨(L, s), u⟩ →⇘a⇙ ⟨(L', s'), u'⟩) =
(∃ a. state_ta ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩ ∧ a ≠ Del)"
apply standard
subgoal
by (blast elim: prod.prod_sound'_action)
apply clarify
subgoal for a
apply (cases a; simp; erule prod.prod_complete_silent prod.prod_complete_sync, fast)
done
done
lemma prod_correct'_delay:
"(∃ d. defs.prod_ta ⊢ ⟨(L, s), u⟩ →⇗d⇖ ⟨(L', s'), u'⟩) =
state_ta ⊢ ⟨L, s, u⟩ →⇘Del⇙ ⟨L', s', u'⟩"
by (blast dest: prod.prod_sound'_delay elim: prod.prod_complete_delay)
lemma equiv_correct:
"state_ta ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩ = A ⊢⇩n ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩"
by (blast intro!: equiv_sound equiv_complete)
lemma prod_correct_action:
"(∃ a. defs.prod_ta ⊢ ⟨(L, s), u⟩ →⇘a⇙ ⟨(L', s'), u'⟩) =
(∃ a. A ⊢⇩n ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩ ∧ a ≠ State_Networks.label.Del)"
unfolding prod_correct'_action equiv_correct ..
lemma prod_correct_delay:
"(∃ d. defs.prod_ta ⊢ ⟨(L, s), u⟩ →⇗d⇖ ⟨(L', s'), u'⟩) =
A ⊢⇩n ⟨L, s, u⟩ →⇘Del⇙ ⟨L', s', u'⟩"
unfolding prod_correct'_delay equiv_correct ..
lemma prod_correct:
"defs.prod_ta ⊢ ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩ =
(∃ a. A ⊢⇩n ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩)"
apply standard
subgoal
using prod_correct_action[of u L' s' u'] prod_correct_delay[of u L' s' u']
Timed_Automata.step.cases by metis
subgoal
apply clarify
subgoal for a
apply (cases a)
using prod_correct_action[of u L' s' u'] prod_correct_delay[of u L' s' u']
Timed_Automata.step.intros apply metis+
done
done
done
context
assumes "0 < p"
begin
lemmas equiv_complete'' = equiv_complete''[OF _ ‹0 < p›]
definition
"all_prop L' s' ≡
(∀q<p. ∃pc st s'' rs pcs.
exec PF n ((I ! q) (L' ! q), [], s', True, []) [] =
Some ((pc, st, s'', True, rs), pcs)
) ∧ bounded B s' ∧ L' ∈ defs.states' s'
"
lemma step_u_inv:
"all_prop L' s'" if "A ⊢⇩n ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩"
using equiv_complete''[OF that] equiv_complete'[OF that] unfolding all_prop_def by auto
lemma step_inv:
"all_prop L' s'" if "state_ta ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩"
using step_u_inv[OF equiv_sound[OF that]] .
lemma Equiv_TA_I:
"Equiv_TA A n L' s'" if *[unfolded all_prop_def]: "all_prop L' s'"
using * by - (standard, auto intro!: pred_time_indep upd_time_indep clock_conj Len)
lemma step_u'_inv:
"all_prop L'' s'' ∧ defs.prod_ta ⊢' ⟨(L, s), u⟩ → ⟨(L'', s''), u''⟩"
if "A ⊢⇧n ⟨L, s, u⟩ → ⟨L'', s'', u''⟩"
using that proof cases
case prems: (1 L' s' u')
from step_u_inv[OF prems(1)] have *[unfolded all_prop_def]: "all_prop L' s'" .
interpret equiv: Equiv_TA A n L' s'
using Equiv_TA_I[OF step_u_inv[OF prems(1)]] .
from equiv.step_u_inv[OF ‹0 < p› prems(3)] show ?thesis
using prems prod_correct_delay[of u L' s' u'] equiv.prod_correct_action[of u' L'' s'' u'']
Timed_Automata.step'.intros
by metis
qed
lemma step'_inv:
"all_prop L'' s'' ∧ A ⊢⇧n ⟨L, s, u⟩ → ⟨L'', s'', u''⟩"
if "defs.prod_ta ⊢' ⟨(L, s), u⟩ → ⟨(L'', s''), u''⟩"
using that proof cases
case prems: (step' d l' u' a)
obtain L' s' where "l' = (L', s')"
by force
from step_inv prod_correct'_delay prems(1) have *:
"all_prop L' s'"
unfolding ‹l' = _› by fast
interpret equiv: Equiv_TA A n L' s'
by (rule Equiv_TA_I[OF *])
from equiv.step_inv[OF ‹0 < p›] equiv.prod_correct'_action prems(2)[unfolded ‹l' = _›] have
"all_prop L'' s''"
by metis
then show ?thesis
using prems prod_correct_delay[of u L' s' u'] equiv.prod_correct_action[of u' L'' s'' u'']
step_u'.intros
unfolding ‹l' = _› by metis
qed
lemma prod_correct_step':
"defs.prod_ta ⊢' ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩ =
A ⊢⇧n ⟨L, s, u⟩ → ⟨L', s', u'⟩"
using step'_inv step_u'_inv by blast
lemma all_prop_start:
"all_prop L s"
using Equiv_TA_axioms unfolding Equiv_TA_def all_prop_def by auto
lemma steps_u'_inv:
"all_prop L'' s'' ∧ defs.prod_ta ⊢' ⟨(L, s), u⟩ →* ⟨(L'', s''), u''⟩"
if "A ⊢⇧n ⟨L, s, u⟩ →* ⟨L'', s'', u''⟩"
using that
proof (induction A ≡ A n ≡ n L ≡ L s ≡ s u L'' s'' u'')
case (refl u)
show ?case using all_prop_start by auto
next
case (step u L' s' u' L'' s'' u'')
then interpret equiv: Equiv_TA A n L' s'
by (blast intro: Equiv_TA_I)
from equiv.step_u'_inv[OF ‹0 < p› step.hyps(3)] step.hyps(1-2) show ?case
by (blast intro: steps'_altI)
qed
lemma steps'_inv:
"all_prop L'' s'' ∧ A ⊢⇧n ⟨L, s, u⟩ →* ⟨L'', s'', u''⟩"
if "defs.prod_ta ⊢' ⟨(L, s), u⟩ →* ⟨(L'', s''), u''⟩"
using that all_prop_start
proof (induction defs.prod_ta "(L, s)" u "(L'', s'')" u'' arbitrary: L s)
case (refl' u)
then show ?case using all_prop_start by auto
next
case (step' u l' u' u'' L s)
obtain L' s' where "l' = (L', s')" by force
from step' interpret equiv: Equiv_TA A n L s
by (blast intro: Equiv_TA_I)
from equiv.step'_inv[OF ‹0 < p› step'(1)[unfolded ‹l' = _›]] step'(3)[OF ‹l' = _›] show ?case
by (auto intro: stepI2)
qed
lemma steps_un'_complete:
"defs.prod_ta ⊢' ⟨(L, s), u⟩ →* ⟨(L'', s''), u''⟩"
if "A ⊢⇧n ⟨L, s, u⟩ →* ⟨L'', s'', u''⟩"
using steps_u'_inv[OF that] ..
lemma steps'_sound:
"A ⊢⇧n ⟨L, s, u⟩ →* ⟨L'', s'', u''⟩"
if "defs.prod_ta ⊢' ⟨(L, s), u⟩ →* ⟨(L'', s''), u''⟩"
using steps'_inv[OF that] ..
lemma prod_reachable_correct:
"defs.prod_ta ⊢' ⟨(L, s), u⟩ →* ⟨(L', s'), u'⟩ ⟷ A ⊢⇧n ⟨L, s, u⟩ →* ⟨L', s', u'⟩"
using steps'_sound steps_un'_complete by fast
lemma Bisimulation_Invariant_I:
"Bisimulation_Invariant
(λ (L, s, u) (L', s', u'). defs.prod_ta ⊢' ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩)
(λ (L, s, u) (L', s', u'). A ⊢⇧n ⟨L, s, u⟩ → ⟨L', s', u'⟩)
(=)
(λ (L, s, u). all_prop L s)
(λ (L, s, u). all_prop L s)"
apply (standard; clarsimp)
apply (simp add: Equiv_TA.prod_correct_step' Equiv_TA_I ‹0 < p›)+
using Equiv_TA.step_u'_inv Equiv_TA_I ‹0 < p› apply blast+
done
interpretation Bisimulation_Invariant
"λ (L, s, u) (L', s', u'). defs.prod_ta ⊢' ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩"
"λ (L, s, u) (L', s', u'). A ⊢⇧n ⟨L, s, u⟩ → ⟨L', s', u'⟩"
"(=)"
"λ (L, s, u). all_prop L s"
"λ (L, s, u). all_prop L s"
by (rule Bisimulation_Invariant_I)
end
end
definition models ("_,_ ⊨⇩_ _" [61,61] 61) where
"A,a⇩0 ⊨⇩n Φ ≡ (case Φ of
formula.EX φ ⇒
Graph_Defs.Ex_ev
(λ (L, s, u) (L', s', u'). A ⊢⇧n ⟨L, s, u⟩ → ⟨L', s', u'⟩)
(λ (L, s, _). check_bexp φ L s)
| formula.EG φ ⇒
Graph_Defs.Ex_alw
(λ (L, s, u) (L', s', u'). A ⊢⇧n ⟨L, s, u⟩ → ⟨L', s', u'⟩)
(λ (L, s, _). check_bexp φ L s)
| formula.AX φ ⇒
Graph_Defs.Alw_ev
(λ (L, s, u) (L', s', u'). A ⊢⇧n ⟨L, s, u⟩ → ⟨L', s', u'⟩)
(λ (L, s, _). check_bexp φ L s)
| formula.AG φ ⇒
Graph_Defs.Alw_alw
(λ (L, s, u) (L', s', u'). A ⊢⇧n ⟨L, s, u⟩ → ⟨L', s', u'⟩)
(λ (L, s, _). check_bexp φ L s)
| formula.Leadsto φ ψ ⇒
Graph_Defs.leadsto
(λ (L, s, u) (L', s', u'). A ⊢⇧n ⟨L, s, u⟩ → ⟨L', s', u'⟩)
(λ (L, s, _). check_bexp φ L s)
(λ (L, s, _). check_bexp ψ L s)
) a⇩0
"
definition
"has_deadlock A n a⇩0 ≡
Graph_Defs.deadlock (λ (L, s, u) (L', s', u'). A ⊢⇧n ⟨L, s, u⟩ → ⟨L', s', u'⟩) a⇩0"
lemmas models_iff = models_def[unfolded Graph_Defs.Ex_alw_iff Graph_Defs.Alw_alw_iff]
context Reachability_Problem
begin
lemma reaches_steps':
"reaches (l, u) (l', u') ⟷ conv_A A ⊢' ⟨l, u⟩ →* ⟨l', u'⟩"
apply standard
subgoal premises prems
using prems by (induction "(l, u)" "(l', u')" arbitrary: l' u') (auto intro: steps'_altI)
subgoal premises prems
using prems by induction (auto intro: converse_rtranclp_into_rtranclp)
done
lemma clocks_I:
"(∀ c. c ∈ clk_set (conv_A A) ⟶ u c = u' c)" if "∀ c ∈ {1..n}. u c = u' c"
unfolding clk_set_conv_A using clocks_n using that by auto
lemma init_dbm_reaches_iff:
"(∃ u ∈ [curry init_dbm]⇘v,n⇙. ∃ u'. conv_A A ⊢' ⟨l⇩0, u⟩ →* ⟨l', u'⟩)
⟷ ([curry (init_dbm :: real DBM')]⇘v,n⇙ ≠ {} ∧
(∀ u ∈ [curry init_dbm]⇘v,n⇙. ∃ u'. conv_A A ⊢' ⟨l⇩0, u⟩ →* ⟨l', u'⟩))
"
proof -
interpret ta_bisim: Bisimulation_Invariant
"(λ(l, u) (l', u'). conv_A A ⊢' ⟨l, u⟩ → ⟨l', u'⟩)"
"(λ(l, u) (l', u'). conv_A A ⊢' ⟨l, u⟩ → ⟨l', u'⟩)"
"(λ(l, u) (l', u'). l' = l ∧ (∀ c. c ∈ clk_set (conv_A A) ⟶ u c = u' c))"
"(λ_. True)" "(λ_. True)"
by (rule ta_bisimulation[of "conv_A A"])
show ?thesis
apply safe
apply force
subgoal for u1 u' u2
unfolding init_dbm_semantics reaches_steps'[symmetric]
apply (drule ta_bisim.A_B.simulation_reaches[of _ _ "(l⇩0, u2)"])
subgoal
using clocks_I[of u1 u2] by fastforce
by auto
subgoal for u
by blast
done
qed
theorem reachable_decides_emptiness_new:
"(∃ D'. E⇧*⇧* a⇩0 (l', D') ∧ [curry (conv_M D')]⇘v,n⇙ ≠ {})
⟷ [curry (init_dbm :: real DBM')]⇘v,n⇙ ≠ {} ∧
(∀ u ∈ [curry init_dbm]⇘v,n⇙. ∃ u'. conv_A A ⊢' ⟨l⇩0, u⟩ →* ⟨l', u'⟩)"
unfolding reachable_decides_emptiness init_dbm_reaches_iff ..
lemma reachable_decides_emptiness'_new:
"(∃ D'. E⇧*⇧* a⇩0 (l', D') ∧ [curry (conv_M D')]⇘v,n⇙ ≠ {})
⟷ (∀ u. (∀ c ∈ {1..n}. u c = 0) ⟶ (∃ u'. conv_A A ⊢' ⟨l⇩0, u⟩ →* ⟨l', u'⟩))"
unfolding reachable_decides_emptiness_new
using init_dbm_semantics' init_dbm_semantics'' init_dbm_non_empty by blast
lemma reachability_check_new_aux:
"(∃ D'. E⇧*⇧* a⇩0 (l', D') ∧ [curry (conv_M D')]⇘v,n⇙ ≠ {} ∧ F l')
⟷ (∀ u. (∀ c ∈ {1..n}. u c = 0) ⟶ (∃ u'. conv_A A ⊢' ⟨l⇩0, u⟩ →* ⟨l', u'⟩ ∧ F l'))"
using reachable_decides_emptiness'_new[of l'] by fast
theorem reachability_check_new:
"(∃ D'. E⇧*⇧* a⇩0 (l', D') ∧ F_rel (l', D'))
⟷ (∀ u. (∀ c ∈ {1..n}. u c = 0) ⟶ (∃ u'. conv_A A ⊢' ⟨l⇩0, u⟩ →* ⟨l', u'⟩ ∧ F l'))"
using reachability_check_new_aux[of l'] check_diag_empty_spec reachable_empty_check_diag
unfolding F_rel_def by auto
lemma init_state_in_state_set:
"l⇩0 ∈ state_set (trans_of A)" if "¬ deadlock (l⇩0, u⇩0)"
proof -
obtain l u where "conv_A A ⊢' ⟨l⇩0, u⇩0⟩ → ⟨l, u⟩"
using ‹¬ deadlock _› unfolding deadlock_def deadlocked_def by force
then have "l⇩0 ∈ state_set (trans_of (conv_A A))"
unfolding state_set_def
by cases (auto elim!: step_a.cases step_t.cases)
then show ?thesis
unfolding state_set_def unfolding trans_of_def conv_A_def by (cases A) force
qed
lemma init_state_in_state_set':
"l⇩0 ∈ state_set (trans_of A)" if "(∀u⇩0. (∀c∈{1..n}. u⇩0 c = 0) ⟶ ¬ deadlock (l⇩0, u⇩0))"
using init_state_in_state_set that by auto
end
context Reachability_Problem_Impl
begin
context
fixes Q :: "'s ⇒ bool" and Q_fun
assumes Q_fun: "(Q_fun, Q) ∈ inv_rel loc_rel states'"
begin
lemma leadsto_spec_refine:
"leadsto_spec_alt Q
≤ SPEC (λ r. ¬ r ⟷
(∄x. (λa b. E_op''.E_from_op a b ∧ ¬ check_diag n (snd b))⇧*⇧* (l⇩0, init_dbm) x ∧
F (fst x) ∧ Q (fst x) ∧
(∃a. (λa b. E_op''.E_from_op a b ∧ ¬ check_diag n (snd b) ∧ Q (fst b))⇧*⇧* x a ∧
(λa b. E_op''.E_from_op a b ∧ ¬ check_diag n (snd b) ∧ Q (fst b))⇧+⇧+ a a)
))"
proof -
have *:"
(λx y. (case y of (l', M') ⇒ E_op''.E_from_op x (l', M') ∧ ¬ check_diag n M') ∧
¬ (case y of (l, M) ⇒ check_diag n M))
= (λa b. E_op''.E_from_op a b ∧ ¬ check_diag n (snd b))"
by (intro ext) auto
have **:
"(λx y. (case y of (l', M') ⇒ E_op''.E_from_op x (l', M') ∧ ¬ check_diag n M') ∧
(case y of (l, M) ⇒ Q l) ∧ ¬ (case y of (l, M) ⇒ check_diag n M))
= (λa b. E_op''.E_from_op a b ∧ ¬ check_diag n (snd b) ∧ Q (fst b))"
by (intro ext) auto
have ***: "¬ check_diag n b"
if "(λa b. E_op''.E_from_op a b ∧ ¬ check_diag n (snd b))⇧*⇧* a⇩0 (a, b)" for a b
using that by cases (auto simp: a⇩0_def)
show ?thesis
unfolding leadsto_spec_alt_def[OF Q_fun]
unfolding PR_CONST_def a⇩0_def[symmetric] by (auto dest: *** simp: * **)
qed
lemma leadsto_impl_hnr':
"(uncurry0
(leadsto_impl state_copy_impl
(succs_P_impl' Q_fun) a⇩0_impl subsumes_impl (return ∘ fst)
succs_impl' emptiness_check_impl F_impl (Q_impl Q_fun) tracei),
uncurry0
(SPEC
(λr. (∀u⇩0. (∀c∈{1..n}. u⇩0 c = 0) ⟶ ¬ deadlock (l⇩0, u⇩0)) ⟶
(¬ r) =
(∀u⇩0. (∀c∈{1..n}. u⇩0 c = 0) ⟶
leadsto (λ(l, u). F l) (λ(l, u). ¬ Q l) (l⇩0, u⇩0)))))
∈ unit_assn⇧k →⇩a bool_assn"
proof -
define p1 where "p1 ≡
(∄x. (λa b. E_op''.E_from_op a b ∧ ¬ check_diag n (snd b))⇧*⇧* (l⇩0, init_dbm) x ∧
F (fst x) ∧ Q (fst x) ∧
(∃a. (λa b. E_op''.E_from_op a b ∧ ¬ check_diag n (snd b) ∧ Q (fst b))⇧*⇧* x a ∧
(λa b. E_op''.E_from_op a b ∧ ¬ check_diag n (snd b) ∧ Q (fst b))⇧+⇧+ a a))"
define p2 where "p2 ≡ (∀u⇩0. (∀c∈{1..n}. u⇩0 c = 0) ⟶ ¬ deadlock (l⇩0, u⇩0))"
define p3 where
"p3 ≡ (∀u⇩0. (∀c∈{1..n}. u⇩0 c = 0) ⟶ leadsto (λ(l, u). F l) (λ(l, u). ¬ Q l) (l⇩0, u⇩0))"
show ?thesis
unfolding state_set_eq[symmetric]
using Reachability_Problem_Impl_Op.leadsto_impl_hnr[OF Reachability_Problem_Impl_Op_axioms,
OF Q_fun precond_a⇩0,
FCOMP leadsto_spec_refine[THEN Id_SPEC_refine, THEN nres_relI], to_hnr, unfolded hn_refine_def,
of show_state show_clock
]
using init_state_in_state_set'
using leadsto_mc[of F Q]
unfolding p1_def[symmetric] p2_def[symmetric] p3_def[symmetric]
apply (simp del: state_set_eq)
apply sepref_to_hoare
apply sep_auto
apply (erule cons_post_rule)
apply sep_auto
done
qed
end
end
context UPPAAL_Reachability_Problem_precompiled'
begin
lemma F_reachable_correct'_new:
"impl.op.F_reachable
⟷ (∃ L' s'. ∀ u. (∀ c ∈ {1..m}. u c = 0) ⟶ (∃ u'.
conv_A A ⊢' ⟨(init, s⇩0), u⟩ →* ⟨(L', s'), u'⟩
∧ 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)"]
reachability_check_new
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 F_reachable_correct'_new':
"impl.op.F_reachable
⟷ (∃ L' s'. ∀ u. (∀ c ∈ {1..m}. u c = 0) ⟶ (∃ u'.
conv_A A ⊢' ⟨(init, s⇩0), u⟩ →* ⟨(L', s'), u'⟩
∧ ¬ check_bexp φ L' s')
)" if "formula = formula.AG φ"
using
that E_op''.E_from_op_reachability_check[of F_rel "PR_CONST (λ(x, y). F x y)"]
reachability_check_new
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 F_reachable_correct_new:
"impl.op.F_reachable
⟷ (∃ L' s'. ∀ u. (∀ c ∈ {1..m}. u c = 0) ⟶ (∃ u'.
conv N ⊢⇧max_steps ⟨init, s⇩0, u⟩ →* ⟨L', s', u'⟩
∧ check_bexp φ L' s')
)" if "formula = formula.EX φ"
unfolding F_reachable_correct'_new[OF that]
apply (subst product'.prod_reachable_correct[symmetric])
using prod_conv p_p p_gt_0 by simp+
lemma F_reachable_correct_new':
"impl.op.F_reachable
⟷ (∃ L' s'. ∀ u. (∀ c ∈ {1..m}. u c = 0) ⟶ (∃ u'.
conv N ⊢⇧max_steps ⟨init, s⇩0, u⟩ →* ⟨L', s', u'⟩
∧ ¬ check_bexp φ L' s')
)" if "formula = formula.AG φ"
unfolding F_reachable_correct'_new'[OF that]
apply (subst product'.prod_reachable_correct[symmetric])
using prod_conv p_p p_gt_0 by simp+
definition
"Alw_ev_checker = dfs_map_impl'
(impl.succs_P_impl' final_fun) impl.a⇩0_impl impl.subsumes_impl (return ∘ fst)
impl.state_copy_impl"
definition
"leadsto_checker ψ = do {
r ← leadsto_impl
impl.state_copy_impl (impl.succs_P_impl' (λ (L, s). ¬ check_bexp ψ L s))
impl.a⇩0_impl impl.subsumes_impl (return ∘ fst)
impl.succs_impl' impl.emptiness_check_impl impl.F_impl
(impl.Q_impl (λ (L, s). ¬ check_bexp ψ L s))
impl.tracei;
return (¬ r)
}"
definition
"model_checker = (
case formula of
formula.EX _ ⇒ reachability_checker' |
formula.AG _ ⇒ do {
r ← reachability_checker';
return (¬ r)
} |
formula.AX _ ⇒ do {
r ← if PR_CONST (λ(x, y). F x y) (init, s⇩0)
then Alw_ev_checker
else return False;
return (¬ r)
} |
formula.EG _ ⇒
if PR_CONST (λ(x, y). F x y) (init, s⇩0)
then Alw_ev_checker
else return False |
formula.Leadsto _ ψ ⇒ leadsto_checker ψ
)
"
lemma p'_gt_0:
"0 < defs'.p"
unfolding p_p by (rule p_gt_0)
interpretation Bisim_A: Bisimulation_Invariant
"(λ(L, s, u) (L', s', u').
defs'.defs.prod_ta ⊢' ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩)"
"(λ(L, s, u) (L', s', u').
conv N ⊢⇧max_steps ⟨L, s, u⟩ → ⟨L', s', u'⟩)"
"(=)" "(λ(L, s, u). product'.all_prop L s)"
"(λ(L, s, u). product'.all_prop L s)"
by (rule product'.Bisimulation_Invariant_I) (rule p'_gt_0)
interpretation Bisim_B: Bisimulation_Invariant
"(λ (l, u) (l', u'). conv_A A ⊢' ⟨l, u⟩ → ⟨l', u'⟩)"
"(λ(L, s, u) (L', s', u').
defs'.defs.prod_ta ⊢' ⟨(L, s), u⟩ → ⟨(L', s'), u'⟩)"
"(λ (l, u') (L, s, u). (l, u') = ((L, s), u))" "λ _. True"
"(λ(L, s, u). product'.all_prop L s)"
unfolding prod_conv[symmetric]
apply standard
apply (solves auto)+
by (rule Bisim_A.A_invariant)
interpretation Bisimulation_Invariant
"(λ (l, u) (l', u'). conv_A A ⊢' ⟨l, u⟩ → ⟨l', u'⟩)"
"(λ(L, s, u) (L', s', u').
conv N ⊢⇧max_steps ⟨L, s, u⟩ → ⟨L', s', u'⟩)"
"(λ (l, u') (L, s, u). (l, u') = ((L, s), u))" "λ _. True"
"(λ(L, s, u). product'.all_prop L s)"
proof -
interpret bisim: Bisimulation_Invariant
"(λ (l, u) (l', u'). conv_A A ⊢' ⟨l, u⟩ → ⟨l', u'⟩)"
"(λ(L, s, u) (L', s', u').
conv N ⊢⇧max_steps ⟨L, s, u⟩ → ⟨L', s', u'⟩)"
"(λa c. ∃b. (case b of (L, s, u) ⇒ product'.all_prop L s) ∧
(case a of (l, u') ⇒ λ(L, s, u). (l, u') = ((L, s), u)) b ∧ b = c)"
"λ _. True"
"(λ(L, s, u). product'.all_prop L s)"
using Bisimulation_Invariant_composition[OF
Bisim_B.Bisimulation_Invariant_axioms Bisim_A.Bisimulation_Invariant_axioms
]
.
show "Bisimulation_Invariant
(λ (l, u) (l', u'). conv_A A ⊢' ⟨l, u⟩ → ⟨l', u'⟩)
(λ(L, s, u) (L', s', u').
conv N ⊢⇧max_steps ⟨L, s, u⟩ → ⟨L', s', u'⟩)
(λ(l, u') (L, s, u). (l, u') = ((L, s), u)) (λ_. True) (λ(L, s, u). product'.all_prop L s)"
apply standard
subgoal for a b a'
apply (drule bisim.A_B_step[of a b a'])
apply auto
done
subgoal for a b a'
apply (drule bisim.B_A_step[of b a' a])
apply auto
done
apply simp
apply (drule bisim.B_invariant)
apply auto
done
qed
lemma models_correct:
"conv N,(init, s⇩0, u⇩0) ⊨⇩max_steps Φ = (case Φ of
formula.EX φ ⇒
(λ ((L, s), u). ∃ L' s' u'. conv_A A ⊢' ⟨(L, s), u⟩ →* ⟨(L', s'), u'⟩ ∧ check_bexp φ L' s')
| formula.EG φ ⇒
Not o Graph_Defs.Alw_ev
(λ (l, u) (l', u'). conv_A A ⊢' ⟨l, u⟩ → ⟨l', u'⟩)
(λ ((L, s), _). ¬ check_bexp φ L s)
| formula.AX φ ⇒
Graph_Defs.Alw_ev
(λ (l, u) (l', u'). conv_A A ⊢' ⟨l, u⟩ → ⟨l', u'⟩)
(λ ((L, s), _). check_bexp φ L s)
| formula.AG φ ⇒
Not o (λ ((L, s), u).
∃ L' s' u'. conv_A A ⊢' ⟨(L, s), u⟩ →* ⟨(L', s'), u'⟩ ∧ ¬ check_bexp φ L' s'
)
| formula.Leadsto φ ψ ⇒
Graph_Defs.leadsto
(λ (l, u) (l', u'). conv_A A ⊢' ⟨l, u⟩ → ⟨l', u'⟩)
(λ ((L, s), _). check_bexp φ L s)
(λ ((L, s), _). check_bexp ψ L s)
) ((init, s⇩0), u⇩0)" if "¬ deadlock ((init, s⇩0), u⇩0)"
proof -
have *: "((Not ∘∘ case_prod) (λ(L, s) _. check_bexp φ L s)) =
(λ((L, s), _). ¬ check_bexp φ L s)" for φ by auto
show ?thesis
apply (subst models_def)
apply (cases Φ)
subgoal for φ
apply simp
apply (subst Ex_ev_iff[
of "(λ((L, s), _). check_bexp φ L s)" _ "((init, s⇩0), u⇩0)", symmetric, simplified
])
apply (drule equiv'_D[simplified], force)
using product'.all_prop_start[OF p'_gt_0] apply (simp add: A_B.equiv'_def[simplified]; fail)
apply (subst Ex_ev[OF that])
unfolding reaches_steps'[symmetric]
apply auto
done
subgoal for φ
apply simp
apply (subst Ex_alw_iff[
of "(λ((L, s), _). check_bexp φ L s)" _ "((init, s⇩0), u⇩0)", symmetric, simplified
])
apply (drule equiv'_D[simplified]; force)
using product'.all_prop_start[OF p'_gt_0] apply (simp add: A_B.equiv'_def[simplified]; fail)
unfolding Graph_Defs.Ex_alw_iff * ..
subgoal for φ
apply simp
apply (subst Alw_ev_iff[
of "(λ((L, s), _). check_bexp φ L s)" _ "((init, s⇩0), u⇩0)", symmetric, simplified
])
apply (drule equiv'_D[simplified]; force)
using product'.all_prop_start[OF p'_gt_0] apply (simp add: A_B.equiv'_def[simplified]; fail)
unfolding Graph_Defs.Ex_alw_iff * ..
subgoal for φ
apply simp
unfolding Graph_Defs.Alw_alw_iff
apply (subst Ex_ev_iff[
of "(λ((L, s), _). ¬check_bexp φ L s)" _ "((init, s⇩0), u⇩0)", symmetric, simplified
])
apply (drule equiv'_D[simplified], subst *[symmetric], force)
using product'.all_prop_start[OF p'_gt_0] apply (simp add: A_B.equiv'_def[simplified]; fail)
apply (subst Ex_ev[OF that])
unfolding reaches_steps'[symmetric]
apply auto
done
subgoal for φ ψ
apply simp
apply (subst Leadsto_iff[
of "(λ((L, s), _). check_bexp φ L s)" _
"(λ((L, s), _). check_bexp ψ L s)" _ "((init, s⇩0), u⇩0)", symmetric, simplified
])
apply (drule equiv'_D[simplified]; force)
apply (drule equiv'_D[simplified]; force)
using product'.all_prop_start[OF p'_gt_0] apply (simp add: A_B.equiv'_def[simplified]; fail)
..
done
qed
lemma final_fun_final':
"((λ (L, s). P L s), (λ (L, s). P L s)) ∈ inv_rel Id states'" for P
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]:
"((λ (L, s). P L s), (λ (L, s). P L s)) ∈ inv_rel Id states" for P
using final_fun_final' states_states' by (rule inv_rel_mono)
abbreviation "u⇩0 ≡ (λ _. 0 :: real)"
lemma deadlock_start_iff:
"Bisim_A.B.deadlock (init, s⇩0, λ_. 0) ⟷ deadlock ((init, s⇩0), u⇩0)"
using product'.all_prop_start[OF p'_gt_0]
by - (rule deadlock_iff[of _ "(init, s⇩0, u⇩0)", symmetric]; simp)
theorem model_check':
"(uncurry0 model_checker,
uncurry0 (
SPEC (λ r.
¬ Graph_Defs.deadlock
(λ (L, s, u) (L', s', u'). conv N ⊢⇧max_steps ⟨L, s, u⟩ → ⟨L', s', u'⟩) (init, s⇩0, u⇩0) ⟶
r = (conv N,(init, s⇩0, u⇩0) ⊨⇩max_steps formula)
)
)
)
∈ unit_assn⇧k →⇩a bool_assn"
proof -
have *: "(λ(l, u). ¬ (case l of (L, s) ⇒ (Not ∘∘∘ check_bexp) φ L s))
= (λ((L, s), _). check_bexp φ L s)" for φ
by auto
have **:
"(λ(l, u). ¬ (case l of (L, s) ⇒ check_bexp φ L s)) = (λ((L, s), _). ¬ check_bexp φ L s)"
for φ by auto
have ***:
"(λ(l, u). case l of (L, s) ⇒ φ L s) = (λ((L, s), _). φ L s)" for φ
by auto
have ****: "(λ(L, y). (Not ∘∘∘ check_bexp) ψ L y) = (λ(L, y). ¬check_bexp ψ L y)" for ψ
by auto
have *****:
"return True = (return False ⤜ return o Not)"
by auto
interpret ta_bisim: Bisimulation_Invariant
"(λ(l, u) (l', u').
conv_A A ⊢' ⟨l, u⟩ → ⟨l', u'⟩)"
"(λ(l, u) (l', u').
conv_A A ⊢' ⟨l, u⟩ → ⟨l', u'⟩)"
"(λ(l, u) (l', u').
l' = l ∧
(∀ c. c ∈ clk_set (conv_A A) ⟶
u c = u' c))"
"(λ_. True)" "(λ_. True)"
by (rule ta_bisimulation[of "conv_A A"])
have bisim2:
"(∃u⇩0. (∀c∈{Suc 0..m}. u⇩0 c = 0) ∧
¬ Alw_ev (λ(l, u). φ l) ((init, s⇩0), u⇩0))
⟷ (¬ Alw_ev (λ(l, u). φ l) ((init, s⇩0), u⇩0))
" for φ
apply safe
subgoal for u
apply (subst (asm) ta_bisim.Alw_ev_iff[of _ "(λ(l, u). φ l)" _ "((init, s⇩0), λ_. 0)"])
using clocks_I[of u "λ_. 0"] unfolding ta_bisim.A_B.equiv'_def
apply auto
done
by force
have bisim1:
"(∃u⇩0. (∀c∈{Suc 0..m}. u⇩0 c = 0) ∧ ¬ Alw_ev (λ((L, s), _). ¬ check_bexp φ L s) ((init, s⇩0), u⇩0)) =
(¬ Alw_ev (λ((L, s), _). ¬ check_bexp φ L s) ((init, s⇩0), u⇩0))" for φ
using bisim2[of "λ (L, s). ¬ check_bexp φ L s"] unfolding *** .
have bisim3:
"(∀u⇩0. (∀c∈{Suc 0..m}. u⇩0 c = 0) ⟶
leadsto (λ((L, s), _). check_bexp φ L s) (λ((L, s), _). check_bexp ψ L s) ((init, s⇩0), u⇩0)) =
leadsto (λ((L, s), _). check_bexp φ L s) (λ((L, s), _). check_bexp ψ L s) ((init, s⇩0), u⇩0)
" for φ ψ
apply safe
apply force
subgoal for u
apply (subst (asm) ta_bisim.Leadsto_iff[of
_ "(λ((L, s), _). check_bexp φ L s)" _ "(λ((L, s), _). check_bexp ψ L s)"
_ "((init, s⇩0), u)"
])
using clocks_I[of u "λ_. 0"] unfolding ta_bisim.A_B.equiv'_def by auto
done
have bisim4:
"(∀u⇩0. (∀c∈{Suc 0..m}. u⇩0 c = 0) ⟶ ¬ deadlock ((init, s⇩0), u⇩0))
⟷ ¬ deadlock ((init, s⇩0), u⇩0)
"
apply safe
apply fast
subgoal for u
apply (subst (asm) ta_bisim.deadlock_iff[of _ "((init, s⇩0), u)"])
using clocks_I[of u "λ_. 0"] unfolding ta_bisim.A_B.equiv'_def by auto
done
have bisim5:
"(∀u. (∀c∈{1..m}. u c = 0) ⟶ (∃u'. conv_A A ⊢' ⟨(init, s⇩0), u⟩ →* ⟨(L', s'), u'⟩ ∧ φ L' s'))
⟷ (∃u'. conv_A A ⊢' ⟨(init, s⇩0), u⇩0⟩ →* ⟨(L', s'), u'⟩ ∧ φ L' s')
" for φ L' s'
unfolding reaches_steps'[symmetric]
apply safe
apply fast
subgoal for u' u
apply (drule ta_bisim.bisim.A_B_reaches[of _ _ "((init, s⇩0), u)"])
subgoal
using clocks_I[of u "λ_. 0"] unfolding ta_bisim.equiv'_def by auto
unfolding ta_bisim.equiv'_def by auto
done
define protect where
"protect = ((λ(l, u) (l', u').
conv_A A ⊢' ⟨l, u⟩ → ⟨l', u'⟩))"
show ?thesis
unfolding deadlock_start_iff
using models_correct
apply simp
unfolding protect_def[symmetric]
apply sepref_to_hoare
apply sep_auto
unfolding model_checker_def reachability_checker'_def Alw_ev_checker_def leadsto_checker_def
apply (cases formula; simp)
subgoal premises prems for φ
using impl.pw_impl_hnr_F_reachable[to_hnr, unfolded hn_refine_def]
apply (subst (asm) (2) F_reachable_correct'_new)
apply (rule prems; fail)
apply (subst (asm) bisim5)
apply sep_auto
unfolding final_fun_def F_def prems
apply (erule cons_post_rule)
apply (sep_auto simp: pure_def)
done
subgoal premises prems for φ
using impl.Alw_ev_impl_hnr[
to_hnr, unfolded hn_refine_def
]
unfolding final_fun_def F_def prems(2)
UPPAAL_Reachability_Problem_precompiled'.final_fun_def[
OF UPPAAL_Reachability_Problem_precompiled'_axioms
]
UPPAAL_Reachability_Problem_precompiled_defs.F_def
apply sep_auto
unfolding **
subgoal
apply (subst (asm) bisim1)
apply (erule cons_post_rule)
using init_state_in_state_set[of u⇩0]
apply (sep_auto simp: pure_def protect_def ***)
done
subgoal
apply (subst (asm) bisim1)
apply simp
apply (erule cons_post_rule)
using init_state_in_state_set[of u⇩0]
apply (sep_auto simp: pure_def protect_def ***)
done
done
subgoal premises prems for φ
using impl.Alw_ev_impl_hnr[to_hnr, unfolded hn_refine_def]
unfolding final_fun_def F_def
unfolding UPPAAL_Reachability_Problem_precompiled_defs.F_def
apply (subst
UPPAAL_Reachability_Problem_precompiled'.final_fun_def[
OF UPPAAL_Reachability_Problem_precompiled'_axioms
])
apply (safe; clarsimp simp: prems(2))
unfolding bisim2
unfolding * ***
subgoal
using init_state_in_state_set[of u⇩0]
by (sep_auto simp: pure_def protect_def)
subgoal
unfolding protect_def *****
apply (erule bind_rule)
using init_state_in_state_set[of u⇩0]
apply (sep_auto simp: pure_def)
done
done
subgoal premises prems for φ
using impl.pw_impl_hnr_F_reachable[to_hnr, unfolded hn_refine_def]
apply (subst (asm) (2) F_reachable_correct'_new')
apply (rule prems; fail)
apply (subst (asm) bisim5)
unfolding final_fun_def F_def prems
apply (sep_auto simp: pure_def)
done
subgoal premises prems for φ ψ
using impl.leadsto_impl_hnr'[
OF final_fun_final, of "Not oo check_bexp ψ",
to_hnr, unfolded hn_refine_def
]
unfolding * F_def
apply (simp add: prems(2))
unfolding *** **** bisim3 bisim4
apply (erule bind_rule)
apply (sep_auto simp: pure_def protect_def)
done
done
qed
theorem model_check'_hoare:
"<emp>
model_checker
<λr. ↑ ((¬ Bisim_A.B.deadlock (init, s⇩0, λ_. 0)) ⟶ r = (
conv N,(init, s⇩0, u⇩0) ⊨⇩max_steps formula
))>⇩t"
using model_check'[to_hnr, unfolded hn_refine_def]
by (sep_auto simp: pure_def elim!: cons_post_rule)
lemma Alw_ev_checker_alt_def':
"Alw_ev_checker ≡
do {
x ← let
key = return ∘ fst;
sub = impl.subsumes_impl;
copy = impl.state_copy_impl;
start = impl.a⇩0_impl;
succs = impl.succs_P_impl' final_fun
in dfs_map_impl' succs start sub key copy;
_ ← return ();
return x
}"
unfolding Alw_ev_checker_def by simp
lemma leadsto_checker_alt_def':
"leadsto_checker ψ ≡
do {
r ← let
key = return ∘ fst;
sub = impl.subsumes_impl;
copy = impl.state_copy_impl;
start = impl.a⇩0_impl;
final = impl.F_impl;
final' = (impl.Q_impl (λ(L, s). ¬ check_bexp ψ L s));
succs = impl.succs_P_impl' (λ(L, s). ¬ check_bexp ψ L s);
succs' = impl.succs_impl';
empty = impl.emptiness_check_impl;
trace = impl.tracei
in
leadsto_impl copy succs start sub key succs' empty final final' trace;
return (¬ r)
}"
unfolding leadsto_checker_def by simp
schematic_goal succs_P_impl_alt_def:
"impl.succs_P_impl (λ(L, s). P L s) ≡ ?impl" for P
unfolding impl.succs_P_impl_def[OF final_fun_final]
unfolding k_impl_alt_def
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_a)
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)
by (rule Pure.reflexive)
lemmas succs_P'_impl_alt_def =
impl.succs_P_impl'_def[OF final_fun_final, unfolded succs_P_impl_alt_def]
lemmas succs_impl'_alt_def =
impl.succs_impl'_def[unfolded succs_impl_alt_def]
lemma reachability_checker'_alt_def':
"reachability_checker' ≡
do {
x ← do {
let key = return ∘ fst;
let sub = impl.subsumes_impl;
let copy = impl.state_copy_impl;
let start = impl.a⇩0_impl;
let final = impl.F_impl;
let succs = impl.succs_impl;
let empty = impl.emptiness_check_impl;
let tracei = impl.tracei;
pw_impl key copy tracei sub start final succs empty
};
_ ← return ();
return x
}"
unfolding reachability_checker'_def by simp
schematic_goal reachability_checker'_alt_def:
"reachability_checker' ≡ ?impl"
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 "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)
schematic_goal Alw_ev_checker_alt_def:
"Alw_ev_checker ≡ ?impl"
unfolding Alw_ev_checker_alt_def' final_fun_def
impl.succs_P_impl_def[OF final_fun_final] impl.succs_P_impl'_def[OF final_fun_final]
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 "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)
schematic_goal leadsto_checker_alt_def:
"leadsto_checker ≡ ?impl"
unfolding leadsto_checker_alt_def'
unfolding impl.F_impl_def impl.Q_impl_def[OF final_fun_final]
unfolding impl.succs_P_impl'_def[OF final_fun_final]
unfolding impl.succs_impl'_def impl.succs_impl_def impl.succs_P_impl_def[OF final_fun_final]
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 "trans_fun" trans_fun)
unfolding impl.init_dbm_impl_def impl.a⇩0_impl_def
unfolding final_fun_def
unfolding impl.subsumes_impl_def
unfolding impl.emptiness_check_impl_def
unfolding impl.state_copy_impl_def
by (rule Pure.reflexive)
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_ia)
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_ia)
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_prog)
apply (abstract_let "IArray (map (map_option stripf) prog)" progf_ia)
apply (abstract_let "IArray (map (map_option stript) prog)" progt_ia)
apply (abstract_let "IArray prog" prog_ia)
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)
schematic_goal Alw_ev_checker_alt_def_refined:
"Alw_ev_checker ≡ ?impl"
unfolding Alw_ev_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_ia)
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_prog)
apply (abstract_let "IArray (map (map_option stripf) prog)" progf_ia)
apply (abstract_let "IArray (map (map_option stript) prog)" progt_ia)
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)
schematic_goal leadsto_checker_alt_def_refined:
"leadsto_checker ≡ ?impl"
unfolding leadsto_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_ia)
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_ia)
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_prog)
apply (abstract_let "IArray (map (map_option stripf) prog)" progf_ia)
apply (abstract_let "IArray (map (map_option stript) prog)" progt_ia)
apply (abstract_let "IArray prog" prog_ia)
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
concrete_definition reachability_checker'
uses UPPAAL_Reachability_Problem_precompiled'.reachability_checker'_alt_def_refined
concrete_definition Alw_ev_checker
uses UPPAAL_Reachability_Problem_precompiled'.Alw_ev_checker_alt_def_refined
concrete_definition leadsto_checker
uses UPPAAL_Reachability_Problem_precompiled'.leadsto_checker_alt_def_refined
context UPPAAL_Reachability_Problem_precompiled'
begin
lemmas model_checker_def_refined = model_checker_def[unfolded
reachability_checker'.refine[OF UPPAAL_Reachability_Problem_precompiled'_axioms]
Alw_ev_checker.refine[OF UPPAAL_Reachability_Problem_precompiled'_axioms]
leadsto_checker.refine[OF UPPAAL_Reachability_Problem_precompiled'_axioms]
]
end
concrete_definition model_checker uses
UPPAAL_Reachability_Problem_precompiled'.model_checker_def_refined
definition [code]:
"precond_mc 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
model_checker p m max_steps I T prog bounds P s⇩0 na k final
⤜ (λ x. return (Some x))
else return None"
theorem model_check:
"<emp> precond_mc p m k max_steps I T prog formula bounds P s⇩0 na
<λ Some r ⇒ ↑(
UPPAAL_Reachability_Problem_precompiled' p m max_steps I T prog bounds P s⇩0 na k ∧
(¬ has_deadlock (conv (N p I P T prog bounds)) max_steps (repeat 0 p, s⇩0, λ_ . 0) ⟶
r = conv (N p I P T prog bounds),(repeat 0 p, s⇩0, λ_ . 0) ⊨⇩max_steps formula
))
| None ⇒ ↑(¬ UPPAAL_Reachability_Problem_precompiled' p m max_steps I T prog bounds P s⇩0 na k)
>⇩t"
proof -
define A where "A ≡ conv (N p I P T prog bounds)"
define check where "check ≡ A,(repeat 0 p, s⇩0, λ_ . 0) ⊨⇩max_steps formula"
note [sep_heap_rules] =
UPPAAL_Reachability_Problem_precompiled'.model_check'_hoare[
of p m max_steps I T prog bounds P s⇩0 na k formula,
unfolded UPPAAL_Reachability_Problem_precompiled_defs.init_def,
folded A_def check_def has_deadlock_def
]
show ?thesis
unfolding UPPAAL_Reachability_Problem_precompiled_defs.init_def
unfolding A_def[symmetric] check_def[symmetric]
unfolding precond_mc_def by (sep_auto simp: model_checker.refine[symmetric])
qed
theorem model_check_alt:
"<emp> precond_mc p m k max_steps I T prog formula bounds P s⇩0 na
<λ r. ↑ (
if UPPAAL_Reachability_Problem_precompiled' p m max_steps I T prog bounds P s⇩0 na k
then r ≠ None ∧
(¬ has_deadlock (conv (N p I P T prog bounds)) max_steps (repeat 0 p, s⇩0, λ_ . 0) ⟶
r = Some (
conv (N p I P T prog bounds),(repeat 0 p, s⇩0, λ_ . 0) ⊨⇩max_steps formula
))
else r = None
)>⇩t"
proof -
define A where "A ≡ conv (N p I P T prog bounds)"
define check where "check ≡ A,(repeat 0 p, s⇩0, λ_ . 0) ⊨⇩max_steps formula"
note [sep_heap_rules] =
UPPAAL_Reachability_Problem_precompiled'.model_check'_hoare[
of p m max_steps I T prog bounds P s⇩0 na k formula,
unfolded UPPAAL_Reachability_Problem_precompiled_defs.init_def,
folded A_def check_def has_deadlock_def
]
show ?thesis
unfolding UPPAAL_Reachability_Problem_precompiled_defs.init_def
unfolding A_def[symmetric] check_def[symmetric]
unfolding precond_mc_def by (sep_auto simp: model_checker.refine[symmetric])
qed
prepare_code_thms dfs_map_impl'_def leadsto_impl_def
lemmas [code] =
reachability_checker'_def
Alw_ev_checker_def
leadsto_checker_def
model_checker_def[unfolded UPPAAL_Reachability_Problem_precompiled_defs.F_def PR_CONST_def]
export_code
precond_mc Pure.type init_pred_check time_indep_check1 time_indep_check1 conjunction_check2
checking SML
end