products/sources/formale sprachen/Isabelle/HOL/HOLCF/IOA/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Deadlock.thy   Sprache: Isabelle

Original von: Isabelle©
(*  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.15 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff