625 before reaching state @{text "s"}. |
625 before reaching state @{text "s"}. |
626 *} |
626 *} |
627 definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat" |
627 definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat" |
628 where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s" |
628 where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s" |
629 |
629 |
|
630 definition "pvD s th = (if (th \<in> readys s \<or> th \<notin> threads s) then 0 else (1::nat))" |
|
631 |
630 text {* @{text "the_preced"} is also the same as @{text "preced"}, the only |
632 text {* @{text "the_preced"} is also the same as @{text "preced"}, the only |
631 difference is the order of arguemts. *} |
633 difference is the order of arguemts. *} |
632 definition "the_preced s th = preced th s" |
634 definition "the_preced s th = preced th s" |
633 |
635 |
|
636 |
634 text {* @{term "the_thread"} extracts thread out of RAG node. *} |
637 text {* @{term "the_thread"} extracts thread out of RAG node. *} |
635 fun the_thread :: "node \<Rightarrow> thread" where |
638 fun the_thread :: "node \<Rightarrow> thread" where |
636 "the_thread (Th th) = th" |
639 "the_thread (Th th) = th" |
|
640 |
637 |
641 |
638 text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *} |
642 text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *} |
639 definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}" |
643 definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}" |
640 |
644 |
641 text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *} |
645 text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *} |