Pr-1st-1.1-m05-Slajd09

Zakleszczenie w modelu AND

W modelu AND proces pasywny $P_i$ staje się aktywny, jeżeli dotarły do niego wiadomości od każdego z procesów tworzących jego zbiór warunkujący ${{𝒟}}_i$. Wówczas:

$deadlock({ℬ})\equiv$

$({ℬ}\subseteq {𝒫})\wedge ({ℬ}\ne \mathrm{\varnothing })\wedge$

$\mathrm{\forall }{P}_i::P_i\in {ℬ}(passiv{e}_i\wedge$

$(\mathrm{\exists }{P}_j::P_j\in {{𝒟}}_i\cap {ℬ}::(\mathrm{\neg }in\text{-}transi{t}_i[j]\wedge \mathrm{\neg }availabl{e}_i[j]))))$

<< Poprzedni slajd | Spis treści | Następny slajd >>