Pr-1st-1.1-m09-Slajd14

Zakończenie dynamiczne: definicja formalna

Przedstawioną definicję można bardziej formalnie zapisać z wykorzystaniem przedstawionych wcześniej oznaczeń w następujący sposób: przetwarzanie rozproszone ${\mathit {\Pi }}$ jest w danej chwili w stanie zakończenia dynamicznego, gdy spełniony jest predykat:

$Dterm({\boldsymbol {\mathcal {P}}})\equiv \forall P_{i}::P_{i}\in {\mathcal {P}}::(passive_{i}\land \neg activate_{i}({\mathcal {AV}}_{i}\cup {\mathcal {IT}}_{i}))$

Predykat ten oznacza, że żaden proces składowy przetwarzania rozproszonego nie będzie już nigdy uaktywniony. Stan ten będzie utrzymywany pomimo, że pewne wiadomości są wciąż transmitowane (${\mathcal {IT}}_{i}$), a pewne wiadomości są już dostępne (${\mathcal {AV}}_{i}$).

Takie sformułowanie definiującego stan zakończenia jest interesujące z praktycznego punktu widzenia, gdyż pozwala stwierdzić zakończenie przetwarzania nawet przed dotarciem wszystkich wiadomości do procesów (węzłów) docelowych. Definicja zakończenia dynamicznego uwzględnia rzeczywistą aktywność procesów wyrażoną przez zmienną $passive_{i}$ oraz potencjalną aktywność wyrażoną przez predykat $activate_{i}({\mathcal {AV}}_{i}\cup {\mathcal {IT}}_{i})$.

Predykat $Dterm({\mathcal {P}})$ jest predykatem stabilnym.

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