Pr-1st-1.1-m09-Slajd19: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
m Zastępowanie tekstu – „ </math>” na „</math>” |
||
| Linia 17: | Linia 17: | ||
W konsekwencji: | W konsekwencji: | ||
:<math>Sterm(\mathcal{P}) \equiv \forall P_i :: P_i \in \mathcal{P} :: (passive_i \land (\mathcal{IT}_i = \emptyset) \land </math> | :<math>Sterm(\mathcal{P}) \equiv \forall P_i :: P_i \in \mathcal{P} :: (passive_i \land (\mathcal{IT}_i = \emptyset) \land</math> | ||
::<math>\neg activate_i(\mathcal{AV}_i)) | ::<math>\neg activate_i(\mathcal{AV}_i)) | ||
\equiv \forall P_i :: P_i \in \mathcal{P} :: (passive_i \land (\mathcal{IT}_i = \emptyset) \land (\mathcal{AV}_i = \emptyset) \equiv Cterm(\mathcal{P}) </math> | \equiv \forall P_i :: P_i \in \mathcal{P} :: (passive_i \land (\mathcal{IT}_i = \emptyset) \land (\mathcal{AV}_i = \emptyset) \equiv Cterm(\mathcal{P})</math> | ||
Warto zauważyć silne związki między pojęciami zakończenia i zakleszczenia. W istocie, zakończenie jest szczególnym wypadkiem zakleszczenia, w którym zakleszczone są wszystkie procesy przetwarzania rozproszonego. | Warto zauważyć silne związki między pojęciami zakończenia i zakleszczenia. W istocie, zakończenie jest szczególnym wypadkiem zakleszczenia, w którym zakleszczone są wszystkie procesy przetwarzania rozproszonego. | ||
Aktualna wersja na dzień 10:47, 5 wrz 2023
Klasyczna definicja zakończenia a zakończenie statyczne
Rozważmy teraz relację między a .
Twierdzenie 9.2
Jeżeli procesy są uaktywnione przez każdą dostępną wiadomość, to przetwarzanie rozproszone obejmujące zbiór procesów jest statycznie zakończone wtedy i tylko wtedy, gdy zachodzi predykat .
Dowód W wypadku procesów uaktywnianych każdą wiadomością:
W konsekwencji:
Warto zauważyć silne związki między pojęciami zakończenia i zakleszczenia. W istocie, zakończenie jest szczególnym wypadkiem zakleszczenia, w którym zakleszczone są wszystkie procesy przetwarzania rozproszonego.
