160   @{text "waiting wq th cs"} as follows: \end{minipage} *}

   160   @{text "waiting wq th cs"} as follows: \end{minipage} *}

   161 

   161 

   162 definition

   162 definition

   163   "waiting_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"

   163   "waiting_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"

   164 

   164 

   165 text {* 

   166 text {* 

   166 

   167 

   167   Resource Allocation Graphs (RAG for short) are used extensively in our

   168   Resource Allocation Graphs (RAG for short) are used extensively in our

   168   formal analysis. The following type @{text "node"} is used to represent

   169   formal analysis. The following type @{text "node"} is used to represent

   169   the two types of nodes in RAGs. *}

   170   the two types of nodes in RAGs. *}