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

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

W modelu OR do uaktywnienia procesu $P_{i}$ wystarczy jedna wiadomość od któregokolwiek z procesów jego zbioru warunkującego $𝒟_{i}$ . Dlatego:

$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 | 𝒟_{i} | = 1 \land$

$𝒟 \subseteq ℬ \land$

$(\forall P_{j} : : P_{j} \in 𝒟_{i} : : (\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]))))$

@@ Linia 6: / Linia 6: @@
-<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  |\mathcal{D}_i|=1 \land </math>
+<math>\qquad \forall P_i :: P_i \in \mathcal{B} ( passive_i \land  |\mathcal{D}_i|=1 \land</math>
-<math>\qquad \mathcal{D} \subseteq \mathcal{B} \land </math>
+<math>\qquad \mathcal{D} \subseteq \mathcal{B} \land</math>
 <math>\qquad \qquad (\forall P_j :: P_j \in \mathcal{D}_i :: (\neg in\mbox{-}transit_i[j] \land \neg available_i[j]))))</math>