Pr-1st-1.1-m05-Slajd12

Zakleszczenie w modelu OR – AND

W modelu OR-AND zbiór warunkujący pasywnego procesu jest zdefiniowany jako ${{𝒟}}_i^1\cup {{𝒟}}_i^1\cup \dots {{𝒟}}_i^{q_i}$, gdzie dla każdego naturalnego $u$, $1\le u\le q_i$, ${{𝒟}}_i^u\subseteq {𝒫}$. Proces staje się aktywny po otrzymaniu wiadomości: od każdego z procesów tworzących zbiór ${{𝒟}}_i^1$, lub od każdego z procesów tworzących zbiór ${{𝒟}}_i^2$, lub... lub od każdego z procesów tworzących zbiór ${{𝒟}}_i^{qi}$.

$deadlock({ℬ})\equiv$

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

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

$\mathrm{\forall }u,1\le u\le q_i$,

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

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