Pr-1st-1.1-m09-Slajd16

Zakończenie statyczne: definicja formalna

Przetwarzanie rozproszone $\mathrm{\Pi }$ jest w danej chwili w stanie zakończenia statycznego, gdy spełniony jest predykat:

$Sterm({𝒫})\equiv \mathrm{\forall }{P}_i::P_i\in \in {𝒫}::(passiv{e}_i\wedge ({{ℐ}{𝒯}}_i=\mathrm{\varnothing })\mathrm{\neg }activat{e}_i({{𝒜}{𝒱}}_i))$

Oznaczenia w powyższym wzorze wprost odpowiadają wcześniej podanej definicji: wszystkie procesy są pasywne ($passiv{e}_i=True$ ), wszystkie wiadomości znajdujące się w kanałach są dostępne (${{ℐ}{𝒯}}_i=\mathrm{\varnothing }$) i dla żadnego procesu nie jest spełniony warunek uaktywnienia ($activat{e}_i({{𝒜}{𝒱}}_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=\mathrm{\varnothing }$).

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