Pr-1st-1.1-m05-Slajd09: 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 pośredniej wersji utworzonej przez tego samego użytkownika) | |||
| 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 | <math>\qquad \forall P_i :: P_i \in \mathcal{B} ( passive_i \land</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> | <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> | ||
Aktualna wersja na dzień 11:00, 5 wrz 2023
Zakleszczenie w modelu AND
W modelu AND proces pasywny staje się aktywny, jeżeli dotarły do niego wiadomości od każdego z procesów tworzących jego zbiór warunkujący . Wówczas:
