Theory Promela.PromelaLTL
section "LTL integration"
theory PromelaLTL
imports
Promela
LTL.LTL
begin
text ‹We have a semantic engine for Promela. But we need to have
an integration with LTL -- more specificly, we must know when a proposition
is true in a global state. This is achieved in this theory.›
subsection ‹LTL optimization›
text ‹For efficiency reasons, we do not store the whole @{typ expr} on the labels
of a system automaton, but @{typ nat} instead. This index then is used to look up the
corresponding @{typ expr}.›
type_synonym APs = "expr iarray"
primrec ltlc_aps_list' :: "'a ltlc ⇒ 'a list ⇒ 'a list"
where
"ltlc_aps_list' True_ltlc l = l"
| "ltlc_aps_list' False_ltlc l = l"
| "ltlc_aps_list' (Prop_ltlc p) l = (if List.member l p then l else p#l)"
| "ltlc_aps_list' (Not_ltlc x) l = ltlc_aps_list' x l"
| "ltlc_aps_list' (Next_ltlc x) l = ltlc_aps_list' x l"
| "ltlc_aps_list' (Final_ltlc x) l = ltlc_aps_list' x l"
| "ltlc_aps_list' (Global_ltlc x) l = ltlc_aps_list' x l"
| "ltlc_aps_list' (And_ltlc x y) l = ltlc_aps_list' y (ltlc_aps_list' x l)"
| "ltlc_aps_list' (Or_ltlc x y) l = ltlc_aps_list' y (ltlc_aps_list' x l)"
| "ltlc_aps_list' (Implies_ltlc x y) l = ltlc_aps_list' y (ltlc_aps_list' x l)"
| "ltlc_aps_list' (Until_ltlc x y) l = ltlc_aps_list' y (ltlc_aps_list' x l)"
| "ltlc_aps_list' (Release_ltlc x y) l = ltlc_aps_list' y (ltlc_aps_list' x l)"
| "ltlc_aps_list' (WeakUntil_ltlc x y) l = ltlc_aps_list' y (ltlc_aps_list' x l)"
| "ltlc_aps_list' (StrongRelease_ltlc x y) l = ltlc_aps_list' y (ltlc_aps_list' x l)"
lemma ltlc_aps_list'_correct:
"set (ltlc_aps_list' φ l) = atoms_ltlc φ ∪ set l"
by (induct φ arbitrary: l) (auto simp add: in_set_member)
lemma ltlc_aps_list'_distinct:
"distinct l ⟹ distinct (ltlc_aps_list' φ l)"
by (induct φ arbitrary: l) (auto simp add: in_set_member)
definition ltlc_aps_list :: "'a ltlc ⇒ 'a list"
where
"ltlc_aps_list φ = ltlc_aps_list' φ []"
lemma ltlc_aps_list_correct:
"set (ltlc_aps_list φ) = atoms_ltlc φ"
unfolding ltlc_aps_list_def
by (force simp: ltlc_aps_list'_correct)
lemma ltlc_aps_list_distinct:
"distinct (ltlc_aps_list φ)"
unfolding ltlc_aps_list_def
by (auto intro: ltlc_aps_list'_distinct)
primrec idx' :: "nat ⇒ 'a list ⇒ 'a ⇒ nat option" where
"idx' _ [] _ = None"
| "idx' ctr (x#xs) y = (if x = y then Some ctr else idx' (ctr+1) xs y)"
definition "idx = idx' 0"
lemma idx'_correct:
assumes "distinct xs"
shows "idx' ctr xs y = Some n ⟷ n ≥ ctr ∧ n < length xs + ctr ∧ xs ! (n-ctr) = y"
using assms
proof (induction xs arbitrary: n ctr)
case (Cons x xs)
show ?case
proof (cases "x=y")
case True with Cons.prems have *: "y ∉ set xs" by auto
{
assume A: "(y#xs)!(n-ctr) = y"
and less: "ctr ≤ n"
and length: "n < length (y#xs) + ctr"
have "n = ctr"
proof (rule ccontr)
assume "n ≠ ctr" with less have "n-ctr > 0" by auto
moreover from ‹n≠ctr› length have "n-ctr < length(y#xs)" by auto
ultimately have "(y#xs)!(n-ctr) ∈ set xs" by simp
with A * show False by auto
qed
}
with True Cons show ?thesis by auto
next
case False
from Cons have "distinct xs" by simp
with Cons.IH False have "idx' (Suc ctr) xs y = Some n ⟷ Suc ctr ≤ n ∧ n < length xs + Suc ctr ∧ xs ! (n - Suc ctr) = y"
by simp
with False show ?thesis
apply -
apply (rule iffI)
apply clarsimp_all
done
qed
qed simp
lemma idx_correct:
assumes "distinct xs"
shows "idx xs y = Some n ⟷ n < length xs ∧ xs ! n = y"
using idx'_correct[OF assms]
by (simp add: idx_def)
lemma idx_dom:
assumes "distinct xs"
shows "dom (idx xs) = set xs"
by (auto simp add: idx_correct assms in_set_conv_nth)
lemma idx_image_self:
assumes "distinct xs"
shows "(the ∘ idx xs) ` set xs = {..<length xs}"
proof (safe)
fix x
assume "x ∈ set xs" with in_set_conv_nth obtain n where n: "n < length xs" "xs ! n = x" by metis
with idx_correct[OF assms] have "idx xs x = Some n" by simp
hence "the (idx xs x) = n" by simp
with n show "(the ∘ idx xs) x < length xs" by simp
next
fix n
assume "n < length xs"
moreover with nth_mem have "xs ! n ∈ set xs" by simp
then obtain x where "xs ! n = x" "x ∈ set xs" by simp_all
ultimately have "idx xs x = Some n" by (simp add: idx_correct[OF assms])
hence "the (idx xs x) = n" by simp
thus "n ∈ (the ∘ idx xs) ` set xs"
using ‹x ∈ set xs›
by auto
qed
lemma idx_ran:
assumes "distinct xs"
shows "ran (idx xs) = {..<length xs}"
using ran_is_image[where M="idx xs"]
using idx_image_self[OF assms] idx_dom[OF assms]
by simp
lemma idx_inj_on_dom:
assumes "distinct xs"
shows "inj_on (idx xs) (dom (idx xs))"
by (fastforce simp add: idx_dom assms in_set_conv_nth idx_correct
intro!: inj_onI)
definition ltl_convert :: "expr ltlc ⇒ APs × nat ltlc" where
"ltl_convert φ = (
let APs = ltlc_aps_list φ;
φ⇩i = map_ltlc (the ∘ idx APs) φ
in (IArray APs, φ⇩i))"
lemma ltl_convert_correct:
assumes "ltl_convert φ = (APs, φ⇩i)"
shows "atoms_ltlc φ = set (IArray.list_of APs)" (is "?P1")
and "atoms_ltlc φ⇩i = {..<IArray.length APs}" (is "?P2")
and "φ⇩i = map_ltlc (the ∘ idx (IArray.list_of APs)) φ" (is "?P3")
and "distinct (IArray.list_of APs)"
proof -
let ?APs = "IArray.list_of APs"
from assms have APs_def: "?APs = ltlc_aps_list φ"
unfolding ltl_convert_def by auto
with ltlc_aps_list_correct show APs_set: ?P1 by metis
from assms show ?P3
unfolding ltl_convert_def
by auto
from assms have "atoms_ltlc φ⇩i = (the ∘ idx ?APs) ` atoms_ltlc φ"
unfolding ltl_convert_def
by (auto simp add: ltlc.set_map)
moreover from APs_def ltlc_aps_list_distinct show "distinct ?APs" by simp
note idx_image_self[OF this]
moreover note APs_set
ultimately show ?P2 by simp
qed
definition prepare
:: "_ × (program ⇒ unit) ⇒ ast ⇒ expr ltlc ⇒ (program × APs × gState) × nat ltlc"
where
"prepare cfg ast φ ≡
let
(prog,g⇩0) = Promela.setUp ast;
(APs,φ⇩i) = PromelaLTL.ltl_convert φ
in
((prog, APs, g⇩0), φ⇩i)"
lemma prepare_instrument[code]:
"prepare cfg ast φ ≡
let
(_,printF) = cfg;
_ = PromelaStatistics.start ();
(prog,g⇩0) = Promela.setUp ast;
_ = printF prog;
(APs,φ⇩i) = PromelaLTL.ltl_convert φ;
_ = PromelaStatistics.stop_timer ()
in
((prog, APs, g⇩0), φ⇩i)"
by (simp add: prepare_def)
export_code prepare checking SML
subsection ‹Language of a Promela program›
definition propValid :: "APs ⇒ gState ⇒ nat ⇒ bool" where
"propValid APs g i ⟷ i < IArray.length APs ∧ exprArith g emptyProc (APs!!i) ≠ 0"
definition promela_E :: "program ⇒ (gState × gState) set"
where
"promela_E prog ≡ {(g,g'). g' ∈ ls.α (nexts_code prog g)}"
definition promela_E_ltl :: "program × APs ⇒ (gState × gState) set" where
"promela_E_ltl = promela_E ∘ fst"
definition promela_is_run' :: "program × gState ⇒ gState word ⇒ bool"
where
"promela_is_run' progg r ≡
let (prog,g⇩0)=progg in
r 0 = g⇩0
∧ (∀i. r (Suc i) ∈ ls.α (nexts_code prog (r i)))"
abbreviation "promela_is_run ≡ promela_is_run' ∘ setUp"
definition promela_is_run_ltl :: "program × APs × gState ⇒ gState word ⇒ bool"
where
"promela_is_run_ltl promg r ≡ let (prog,APs,g) = promg in promela_is_run' (prog,g) r"
definition promela_props :: "gState ⇒ expr set"
where
"promela_props g = {e. exprArith g emptyProc e ≠ 0}"
definition promela_props_ltl :: "APs ⇒ gState ⇒ nat set"
where
"promela_props_ltl APs g ≡ Collect (propValid APs g)"
definition promela_language :: "ast ⇒ expr set word set" where
"promela_language ast ≡ {promela_props ∘ r | r. promela_is_run ast r}"
definition promela_language_ltl :: "program × APs × gState ⇒ nat set word set" where
"promela_language_ltl promg ≡ let (prog,APs,g) = promg in
{promela_props_ltl APs ∘ r | r. promela_is_run_ltl promg r}"
lemma promela_props_ltl_map_aprops:
assumes "ltl_convert φ = (APs,φ⇩i)"
shows "promela_props_ltl APs =
map_props (idx (IArray.list_of APs)) ∘ promela_props"
proof -
let ?APs = "IArray.list_of APs"
let ?idx = "idx ?APs"
from ltl_convert_correct assms have D: "distinct ?APs" by simp
show ?thesis
proof (intro ext set_eqI iffI)
fix g i
assume "i ∈ promela_props_ltl APs g"
hence "propValid APs g i" by (simp add: promela_props_ltl_def)
hence l: "i < IArray.length APs" "exprArith g emptyProc (APs!!i) ≠ 0"
by (simp_all add: propValid_def)
hence "APs!!i ∈ promela_props g" by (simp add: promela_props_def)
moreover from idx_correct l D have "?idx (APs!!i) = Some i" by fastforce
ultimately show "i ∈ (map_props ?idx ∘ promela_props) g"
unfolding o_def map_props_def
by blast
next
fix g i
assume "i ∈ (map_props ?idx ∘ promela_props) g"
then obtain p where p_def: "p ∈ promela_props g" "?idx p = Some i"
unfolding map_props_def o_def
by auto
hence expr: "exprArith g emptyProc p ≠ 0" by (simp add: promela_props_def)
from D p_def have "i < IArray.length APs" "APs !! i = p"
using idx_correct by fastforce+
with expr have "propValid APs g i" by (simp add: propValid_def)
thus "i ∈ promela_props_ltl APs g"
by (simp add: promela_props_ltl_def)
qed
qed
lemma promela_run_in_language_iff:
assumes conv: "ltl_convert φ = (APs,φ⇩i)"
shows "promela_props ∘ ξ ∈ language_ltlc φ
⟷ promela_props_ltl APs ∘ ξ ∈ language_ltlc φ⇩i" (is "?L ⟷ ?R")
proof -
let ?APs = "IArray.list_of APs"
from conv have D: "distinct ?APs"
by (simp add: ltl_convert_correct)
with conv have APs: "atoms_ltlc φ ⊆ dom (idx ?APs)"
by (simp add: idx_dom ltl_convert_correct)
note map_semantics = map_semantics_ltlc[OF idx_inj_on_dom[OF D] APs]
promela_props_ltl_map_aprops[OF conv]
ltl_convert_correct[OF conv]
have "?L ⟷ (promela_props ∘ ξ) ⊨⇩c φ" by (simp add: language_ltlc_def)
also have "... ⟷ (promela_props_ltl APs ∘ ξ) ⊨⇩c φ⇩i"
using map_semantics
by (simp add: o_assoc)
also have "... ⟷ ?R"
by (simp add: language_ltlc_def)
finally show ?thesis .
qed
lemma promela_language_sub_iff:
assumes conv: "ltl_convert φ = (APs,φ⇩i)"
and setUp: "setUp ast = (prog,g)"
shows "promela_language_ltl (prog,APs,g) ⊆ language_ltlc φ⇩i ⟷ promela_language ast ⊆ language_ltlc φ"
using promela_run_in_language_iff[OF conv] setUp
by (auto simp add: promela_language_ltl_def promela_language_def promela_is_run_ltl_def)
hide_const (open) abort abortv
err errv
usc
warn the_warn with_warn
hide_const (open) idx idx'
end