Pr-1st-1.1-m09-Slajd16: 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 9: | Linia 9: | ||
</math> | </math> | ||
Oznaczenia w powyższym wzorze wprost odpowiadają wcześniej podanej definicji: wszystkie procesy są pasywne (<math>passive_i = True</math> ), wszystkie wiadomości znajdujące się w kanałach są dostępne (<math>\mathcal{IT}_i = \emptyset</math>) i dla żadnego procesu nie jest spełniony warunek uaktywnienia (<math>activate_i (\mathcal{AV}_i) = False </math> ). Definicja ta uwzględnia zatem zarówno stany procesów jak istany kanałów. | Oznaczenia w powyższym wzorze wprost odpowiadają wcześniej podanej definicji: wszystkie procesy są pasywne (<math>passive_i = True</math> ), wszystkie wiadomości znajdujące się w kanałach są dostępne (<math>\mathcal{IT}_i = \emptyset</math>) i dla żadnego procesu nie jest spełniony warunek uaktywnienia (<math>activate_i (\mathcal{AV}_i) = False</math> ). Definicja ta uwzględnia zatem zarówno stany procesów jak istany kanałów. | ||
Porównując z <math>Dterm(\mathcal{P})</math>, predykat <math>Sterm(\mathcal{P})</math> odpowiada detekcji nieco późniejszej, gdyż dodatkowo wymaga się, by wiadomości nie były już transmitowane (<math>\mathcal{IT}_i = \emptyset </math>). | Porównując z <math>Dterm(\mathcal{P})</math>, predykat <math>Sterm(\mathcal{P})</math> odpowiada detekcji nieco późniejszej, gdyż dodatkowo wymaga się, by wiadomości nie były już transmitowane (<math>\mathcal{IT}_i = \emptyset</math>). | ||
[[pr-1st-1.1-m09-Slajd15 | << Poprzedni slajd]] | [[pr-1st-1.1-m09-toc|Spis treści ]] | [[pr-1st-1.1-m09-Slajd17 | Następny slajd >>]] | [[pr-1st-1.1-m09-Slajd15 | << Poprzedni slajd]] | [[pr-1st-1.1-m09-toc|Spis treści ]] | [[pr-1st-1.1-m09-Slajd17 | Następny slajd >>]] |
Aktualna wersja na dzień 10:50, 5 wrz 2023
Zakończenie statyczne: definicja formalna
Przetwarzanie rozproszone jest w danej chwili w stanie zakończenia statycznego, gdy spełniony jest predykat:
Oznaczenia w powyższym wzorze wprost odpowiadają wcześniej podanej definicji: wszystkie procesy są pasywne ( ), wszystkie wiadomości znajdujące się w kanałach są dostępne () i dla żadnego procesu nie jest spełniony warunek uaktywnienia ( ). Definicja ta uwzględnia zatem zarówno stany procesów jak istany kanałów.
Porównując z , predykat odpowiada detekcji nieco późniejszej, gdyż dodatkowo wymaga się, by wiadomości nie były już transmitowane ().