--- a/PIPDefs.thy	Sun Jan 17 22:18:35 2016 +0800
+++ b/PIPDefs.thy	Wed Jan 27 19:26:56 2016 +0800
@@ -626,14 +626,18 @@
 definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat"
   where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s"
 
+definition "pvD s th = (if (th \<in> readys s \<or> th \<notin> threads s) then 0 else (1::nat))"
+
 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}"