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

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 $P_{i}$ skojarzony jest zbiór warunkujący $𝒟_{i} = 𝒟_{i}^{1} \cup 𝒟_{i}^{1} \cup \dots 𝒟_{i}^{q_{i}}$ , liczby naturalne $k_{i}^{1}, k_{i}^{2}, \dots, k_{i}^{q_{i}}$ , i liczby naturalne $r_{i}^{1}, r_{i}^{2}, \dots, r_{i}^{q_{i}}$ , gdzie $𝒟_{i} \subseteq 𝒫$ oraz dla każdego naturalnego $u$ , $1 \leq u \leq q_{i}$ , $1 \leq k_{i}^{u} \leq r_{i}^{u} = | 𝒟_{i}^{u} |$ . Proces staje się aktywny po otrzymaniu: wiadomości od co najmniej $k_{i}^{1}$ różnych procesów ze zbioru $𝒟_{i}^{1}$ , lub wiadomości od co najmniej $k_{i}^{2}$ różnych procesów ze zbioru $𝒟_{i}^{2}$ , lub... lub wiadomości od co najmniej $k_{i}^{q_{i}}$ różnych procesów ze zbioru $𝒟_{i}^{q_{i}}$ ,. Wówczas:

$d e a d l o c k (ℬ) \equiv$

$(ℬ \subseteq 𝒫) \land (ℬ \neq \emptyset) \land$

$\forall P_{i} : : P_{i} \in ℬ (p a s s i v e_{i} \land (\forall u, 1 \leq u \leq q_{i} : :$

$(\exists ℬ_{i}^{u} \subseteq 𝒟_{i}^{u} \cap ℬ : :$

$(| 𝒟_{i}^{u} ∖ ℬ_{i}^{u} | < k_{i}^{u} \land$

$(\forall P_{j} : : P_{j} \in ℬ_{i}^{u} : : (\neg i n - t r a n s i t_{i} [j] \land \neg a v a i l a b l e_{i} [j]))))))$

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

@@ Linia 14: / Linia 14: @@
 <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>
@@ Linia 22: / Linia 22: @@
 <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>

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

Aktualna wersja na dzień 10:47, 5 wrz 2023

Zakleszczenie w modelu dysjunkcyjnym k spośród r

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia