Pr-1st-1.1-m05-Slajd08: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
Nie podano opisu zmian |
||
Linia 1: | Linia 1: | ||
==Zakleszczenie w modelu jednostkowym== | ==Zakleszczenie w modelu jednostkowym== | ||
[[Image: | [[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 >>]] |
Wersja z 15:53, 7 wrz 2006
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ówczas: