Pr-1st-1.1-m09-Slajd16: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Szopen (dyskusja | edycje)
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

Zakończenie statyczne: definicja formalna

Przetwarzanie rozproszone Π jest w danej chwili w stanie zakończenia statycznego, gdy spełniony jest predykat:

Sterm(𝒫)Pi::Pi𝒫::(passivei(𝒯i=)¬activatei(𝒜𝒱i))

Oznaczenia w powyższym wzorze wprost odpowiadają wcześniej podanej definicji: wszystkie procesy są pasywne (passivei=True ), wszystkie wiadomości znajdujące się w kanałach są dostępne (𝒯i=) i dla żadnego procesu nie jest spełniony warunek uaktywnienia (activatei(𝒜𝒱i)=False ). Definicja ta uwzględnia zatem zarówno stany procesów jak istany kanałów.

Porównując z Dterm(𝒫), predykat Sterm(𝒫) odpowiada detekcji nieco późniejszej, gdyż dodatkowo wymaga się, by wiadomości nie były już transmitowane (𝒯i=).


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