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