Pr-1st-1.1-m05-Slajd08: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Szopen (dyskusja | edycje)
Nie podano opisu zmian
 
Szopen (dyskusja | edycje)
Nie podano opisu zmian
Linia 1: Linia 1:
==Zakleszczenie w modelu jednostkowym==
==Zakleszczenie w modelu jednostkowym==


[[Image:pr-1st-1.1-m05-Slajd08.png|Zakleszczenie w modelu jednostkowym]]
[[Image:Pr-1st-1.1-m05-Slajd08.png|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  
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  
Linia 15: Linia 15:
<math>\qquad \qquad (\exists P_j :: P_j \in \mathcal{D}_i \cap \mathcal{B} :: (\neg in\mbox{-}transit_i[j] \land \neg available_i[j]))))</math>
<math>\qquad \qquad (\exists P_j :: P_j \in \mathcal{D}_i \cap \mathcal{B} :: (\neg in\mbox{-}transit_i[j] \land \neg available_i[j]))))</math>


[[pr-1st-1.1-m05-Slajd07 | << Poprzedni slajd]] | [[pr-1st-1.1-m05-toc|Spis treści ]] | [[pr-1st-1.1-m05-Slajd09 | Następny slajd >>]]
[[Pr-1st-1.1-m05-Slajd07 | << Poprzedni slajd]] | [[Pr-1st-1.1-m05-toc|Spis treści ]] | [[Pr-1st-1.1-m05-Slajd09 | Następny slajd >>]]

Wersja z 15:53, 7 wrz 2006

Zakleszczenie w modelu jednostkowym

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()

(𝒫)()

Pi::Pi(passivei|𝒟i|=1

(Pj::Pj𝒟i::(¬in-transiti[j]¬availablei[j]))))

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