2 (*<*)

     2 (*<*)

     3 theory PrioGDef

     3 theory PrioGDef

     4 imports Precedence_ord Moment

     4 imports Precedence_ord Moment

     5 begin

     5 begin

     6 (*>*)

     6 (*>*)

   385   The following @{text "cp"} is a shorthand for @{text "cprec_fun"}. 

   385   The following @{text "cp"} is a shorthand for @{text "cprec_fun"}. 

   386   *}

   386   *}

   387 definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"

   387 definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"

   388   where "cp s \<equiv> cprec_fun (schs s)"

   388   where "cp s \<equiv> cprec_fun (schs s)"

   389 

   389 

   390 text {* \noindent

   392 text {* \noindent

   391   Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"} and 

   393   Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"} and 

   392   @{text "dependants"} still have the 

   394   @{text "dependants"} still have the 

   393   same meaning, but redefined so that they no longer RAG on the 

   395   same meaning, but redefined so that they no longer RAG on the 

   394   fictitious {\em waiting queue function}

   396   fictitious {\em waiting queue function}

   583   lemmas @{text "step_v_hold_inv"}, @{text " step_v_wait_inv"}, 

   585   lemmas @{text "step_v_hold_inv"}, @{text " step_v_wait_inv"}, 

   584   @{text "step_v_get_hold"} and @{text "step_v_not_wait"}.

   586   @{text "step_v_get_hold"} and @{text "step_v_not_wait"}.

   585   *}

   587   *}

   586 definition next_th:: "state \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> thread \<Rightarrow> bool"

   588 definition next_th:: "state \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> thread \<Rightarrow> bool"

   587   where "next_th s th cs t = (\<exists> rest. wq s cs = th#rest \<and> rest \<noteq> [] \<and> 

   589   where "next_th s th cs t = (\<exists> rest. wq s cs = th#rest \<and> rest \<noteq> [] \<and> 

   588 

   591 

   589 text {* \noindent

   592 text {* \noindent

   590   The aux function @{text "count Q l"} is used to count the occurrence of situation @{text "Q"}

   593   The aux function @{text "count Q l"} is used to count the occurrence of situation @{text "Q"}

   591   in list @{text "l"}:

   594   in list @{text "l"}:

   592   *}

   595   *}