(* Title: HOL/HOLCF/IOA/Deadlock.thy Author: Olaf Müller
*)
section \<open>Deadlock freedom of I/O Automata\<close>
theory Deadlock imports RefCorrectness CompoScheds begin
text\<open>Input actions may always be added to a schedule.\<close>
lemma scheds_input_enabled: "Filter (\x. x \ act A) \ sch \ schedules A \ a \ inp A \ input_enabled A \ Finite sch \<Longrightarrow> Filter (\<lambda>x. x \<in> act A) \<cdot> sch @@ a \<leadsto> nil \<in> schedules A" apply (simp add: schedules_def has_schedule_def) apply auto apply (frule inp_is_act) apply (simp add: executions_def) apply (pair ex) apply (rename_tac s ex) apply (subgoal_tac "Finite ex") prefer 2 apply (simp add: filter_act_def) defer apply (rule_tac [2] Map2Finite [THEN iffD1]) apply (rule_tac [2] t = "Map fst \ ex" in subst) prefer 2 apply assumption apply (erule_tac [2] FiniteFilter) text\<open>subgoal 1\<close> apply (frule exists_laststate) apply (erule allE) apply (erule exE) text\<open>using input-enabledness\<close> apply (simp add: input_enabled_def) apply (erule conjE)+ apply (erule_tac x = "a"in allE) apply simp apply (erule_tac x = "u"in allE) apply (erule exE) text\<open>instantiate execution\<close> apply (rule_tac x = " (s, ex @@ (a, s2) \ nil) " in exI) apply (simp add: filter_act_def MapConc) apply (erule_tac t = "u"in lemma_2_1) apply simp apply (rule sym) apply assumption done
text\<open>
Deadlock freedom: component B cannot block an out or int action of component
A in every schedule.
Needs compositionality on schedule level, input-enabledness, compatibility and distributivity of \<open>is_exec_frag\<close> over \<open>@@\<close>. \<close>
lemma IOA_deadlock_free: assumes"a \ local A" and"Finite sch" and"sch \ schedules (A \ B)" and"Filter (\x. x \ act A) \ (sch @@ a \ nil) \ schedules A" and"compatible A B" and"input_enabled B" shows"(sch @@ a \ nil) \ schedules (A \ B)"
supply if_split [split del] apply (insert assms) apply (simp add: compositionality_sch locals_def) apply (rule conjI) text\<open>\<open>a \<in> act (A \<parallel> B)\<close>\<close> prefer 2 apply (simp add: actions_of_par) apply (blast dest: int_is_act out_is_act)
text\<open>\<open>Filter B (sch @@ [a]) \<in> schedules B\<close>\<close> apply (case_tac "a \ int A") apply (drule intA_is_not_actB) apply (assumption) (* \<longrightarrow> a \<notin> act B *) apply simp
text\<open>case \<open>a \<notin> int A\<close>, i.e. \<open>a \<in> out A\<close>\<close> apply (case_tac "a \ act B") apply simp text\<open>case \<open>a \<in> act B\<close>\<close> apply simp apply (subgoal_tac "a \ out A") prefer 2 apply blast apply (drule outAactB_is_inpB) apply assumption apply assumption apply (rule scheds_input_enabled) apply simp apply assumption+ done
end
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
