diff -r 2af87bb52fca -r 25fd656667a7 PIPDefs.thy~ --- a/PIPDefs.thy~ Thu Jan 07 22:10:06 2016 +0800 +++ b/PIPDefs.thy~ Sat Jan 09 22:19:27 2016 +0800 @@ -1,7 +1,7 @@ chapter {* Definitions *} (*<*) theory PIPDefs -imports Precedence_ord Moment +imports Precedence_ord Moment RTree Max begin (*>*) @@ -607,6 +607,37 @@ *} definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat" where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s" + +text {* @{text "the_preced"} is also the same as @{text "preced"}, the only + difference is the order of arguemts. *} +definition "the_preced s th = preced th s" + +text {* @{term "the_thread"} extracts thread out of RAG node. *} +fun the_thread :: "node \<Rightarrow> thread" where + "the_thread (Th th) = th" + +text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *} +definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}" + +text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *} +definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}" + +text {* + The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}. + It characterizes the dependency between threads when calculating current + precedences. It is defined as the composition of the above two sub-graphs, + names @{term "wRAG"} and @{term "hRAG"}. + *} +definition "tRAG s = wRAG s O hRAG s" + +text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *} +lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)" + by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv + s_holding_abv cs_RAG_def, auto) + +definition "cp_gen s x = + Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)" + (*<*) end