equal
deleted
inserted
replaced
359 text {* \noindent |
359 text {* \noindent |
360 The following function @{text "holdents s th"} returns the set of resources held by thread |
360 The following function @{text "holdents s th"} returns the set of resources held by thread |
361 @{text "th"} in state @{text "s"}. |
361 @{text "th"} in state @{text "s"}. |
362 *} |
362 *} |
363 definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set" |
363 definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set" |
364 where "holdents s th \<equiv> {cs . (Cs cs, Th th) \<in> depend s}" |
364 where "holdents s th \<equiv> {cs . holding s th cs}" |
|
365 |
|
366 lemma holdents_test: |
|
367 "holdents s th = {cs . (Cs cs, Th th) \<in> depend s}" |
|
368 unfolding holdents_def |
|
369 unfolding s_depend_def |
|
370 unfolding s_holding_abv |
|
371 unfolding wq_def |
|
372 by (simp) |
365 |
373 |
366 text {* \noindent |
374 text {* \noindent |
367 @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in |
375 @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in |
368 state @{text "s"}: |
376 state @{text "s"}: |
369 *} |
377 *} |