Pr-1st-1.1-m05-Slajd13: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
m Zastępowanie tekstu – „ </math>” na „</math>” |
||
| (Nie pokazano 1 wersji utworzonej przez jednego użytkownika) | |||
| Linia 1: | Linia 1: | ||
==Zakleszczenie w modelu dysjunkcyjnym k spośród r== | ==Zakleszczenie w modelu dysjunkcyjnym k spośród r== | ||
[[Image: | [[Image:Pr-1st-1.1-m05-Slajd13.png|Zakleszczenie w modelu dysjunkcyjnym k spośród r]] | ||
W modelu ''dysjunkcyjnym k spośród r'' z każdym pasywnym procesem <math>P_i</math> skojarzony jest zbiór warunkujący | W modelu ''dysjunkcyjnym k spośród r'' z każdym pasywnym procesem <math>P_i</math> skojarzony jest zbiór warunkujący | ||
| Linia 10: | Linia 10: | ||
oraz dla każdego naturalnego <math>u</math>, | oraz dla każdego naturalnego <math>u</math>, | ||
<math>1 \le u \le q_i</math>, | <math>1 \le u \le q_i</math>, | ||
<math>1 \le | <math>1 \le k_i^u \le r_i^u = | \mathcal{D}_i^u|</math>. Proces staje się aktywny po otrzymaniu: wiadomości od co najmniej | ||
<math>k_i^1</math> różnych procesów ze zbioru | <math>k_i^1</math> różnych procesów ze zbioru | ||
<math>\mathcal{D}_i^1</math>, lub wiadomości od co najmniej <math>k_i^2</math> różnych procesów ze zbioru <math>\mathcal{D}_i^2</math>, lub ... lub wiadomości od co najmniej <math>k_i^{q_i}</math> różnych procesów ze zbioru <math>\mathcal{D}_i^{q_i}</math>, . Wówczas: | <math>\mathcal{D}_i^1</math>, lub wiadomości od co najmniej <math>k_i^2</math> różnych procesów ze zbioru <math>\mathcal{D}_i^2</math>, lub... lub wiadomości od co najmniej <math>k_i^{q_i}</math> różnych procesów ze zbioru <math>\mathcal{D}_i^{q_i}</math>,. Wówczas: | ||
<math>deadlock(\mathcal{B}) \equiv </math> | <math>deadlock(\mathcal{B}) \equiv</math> | ||
<math>\qquad ( \mathcal{B} \subseteq \mathcal{P} ) \land ( \mathcal{B} \ne \emptyset ) \land </math> | <math>\qquad ( \mathcal{B} \subseteq \mathcal{P} ) \land ( \mathcal{B} \ne \emptyset ) \land</math> | ||
<math>\qquad \forall P_i :: P_i \in \mathcal{B} ( passive_i \land ( \forall u, 1 \le u \le q_i ::</math> | <math>\qquad \forall P_i :: P_i \in \mathcal{B} ( passive_i \land ( \forall u, 1 \le u \le q_i ::</math> | ||
| Linia 22: | Linia 22: | ||
<math>\qquad (\exists \mathcal{B}_i^u \subseteq \mathcal{D}_i^u \cap \mathcal{B}::</math> | <math>\qquad (\exists \mathcal{B}_i^u \subseteq \mathcal{D}_i^u \cap \mathcal{B}::</math> | ||
<math>\qquad (|\mathcal{D}_i^u \setminus \mathcal{B}_i^u| < k_i^u \land </math> | <math>\qquad (|\mathcal{D}_i^u \setminus \mathcal{B}_i^u| < k_i^u \land</math> | ||
<math>\qquad (\forall P_j :: P_j \in \mathcal{B}_i^u :: (\neg in\mbox{-}transit_i[j] \land \neg available_i[j]))))))</math> | <math>\qquad (\forall P_j :: P_j \in \mathcal{B}_i^u :: (\neg in\mbox{-}transit_i[j] \land \neg available_i[j]))))))</math> | ||
| Linia 28: | Linia 28: | ||
[[ | [[Pr-1st-1.1-m05-Slajd12 | << Poprzedni slajd]] | [[Pr-1st-1.1-m05-toc|Spis treści ]] | [[Pr-1st-1.1-m05-Slajd14 | Następny slajd >>]] | ||
Aktualna wersja na dzień 10:47, 5 wrz 2023
Zakleszczenie w modelu dysjunkcyjnym k spośród r
W modelu dysjunkcyjnym k spośród r z każdym pasywnym procesem skojarzony jest zbiór warunkujący , liczby naturalne , i liczby naturalne , gdzie oraz dla każdego naturalnego , , . Proces staje się aktywny po otrzymaniu: wiadomości od co najmniej różnych procesów ze zbioru , lub wiadomości od co najmniej różnych procesów ze zbioru , lub... lub wiadomości od co najmniej różnych procesów ze zbioru ,. Wówczas:
