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" ― ‹Transition relation of a promela program› 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" ― ‹Predicate defining runs of promela programs› 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) (* from PromelaDatastructures *) hide_const (open) abort abortv err errv usc warn the_warn with_warn hide_const (open) idx idx' end