Pr-1st-1.1-m05-Slajd08

Zakleszczenie w modelu jednostkowym

W modelu jednostkowym warunkiem uaktywnienia pasywnego procesu Pi jest przybycie wiadomości od ściśle określonego, jednego nadawcy. Tak więc dla każdego zbioru warunkującego ${{𝒟}}_i$, $|{{𝒟}}_i|=1$. Wówczas:

$deadlock({ℬ})\equiv$

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

$\mathrm{\forall }{P}_i::P_i\in {ℬ}(passiv{e}_i\wedge |{{𝒟}}_i|=1\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 >>