Pr-1st-1.1-m09-Slajd17

Zakończenie dynamiczne \leftrightarrow statyczne

Niech $\vartheta \leftrightsquigarrow {\vartheta }^{\prime }$ oznacza, że zajście predykatu $\vartheta$ prowadzi w skończonym choć nieprzewidzianym czasie do zajścia predykatu ${\vartheta }^{\prime }$.

Twierdzenie 9.1

$Dterm({𝒫})\leftrightsquigarrow Sterm({𝒫})$

Dowód

W chwili $\tau$, gdy $Dterm({𝒫})=True$, wszystkie procesy $P_i$ są pasywne, zachodzi $activat{e}_i({{𝒜}{𝒱}}_i\cup {{ℐ}{𝒯}}_i)[\tau ]$, a część wiadomości może znajdować się w kanałach. Jednakże, wszystkie wiadomości transmitowane są brane pod uwagę, a ich dotarcie do węzłów docelowych iw konsekwencji ich dostępność, jest uwzględniona w wartości predykatu \neg $activat{e}_i({{𝒜}{𝒱}}_i\cup {{ℐ}{𝒯}}_i))$. Wobec niezawodności kanałów, wiadomości transmitowane osiągną węzły docelowe po skończonym choć nieprzewidywalnym czasie, w pewnym momencie ${\tau }^{\prime }>\tau$. Wówczas ${{ℐ}{𝒯}}_i[{\tau }^{\prime }]=\mathrm{\varnothing }$. Wobec stałej pasywności wszystkich procesów od chwili \tau, w każdej chwili ${\tau }^{″}:{\tau }^{\prime }>{\tau }^{″}$, ${{𝒜}{𝒱}}_i[{\tau }^{″}]={{𝒜}{𝒱}{ℐ}}_i[\tau ]\cup {{ℐ}{𝒯}}_i[\tau ]$ oraz ${{ℐ}{𝒯}}_i[{\tau }^{″}]=\mathrm{\varnothing }$.Stąd otrzymujemy:

$\mathrm{\neg }activat{e}_i({{𝒜}{𝒱}}_i[{\tau }^{″}]=True,{{ℐ}{𝒯}}_i[{\tau }^{″}]=\mathrm{\varnothing }$

Predykat $Sterm({𝒫})$ przyjmuje zatem wartość True.

Udowodniliśmy więc, że opóźnienie między momentem zajścia predykatu $Dterm({𝒫})$ a momentem zajścia predykatu $Sterm({𝒫})$ jest skończone lecz nieprzewidywalne. Wybór między jedną a drugą definicją zakończenia zależy oczywiście od użytkownika. Łatwo przewidzieć, że detekcja stanu opisanego predykatem $Dterm({𝒫})$ będzie trudniejsza, a więc w ogolności bardziej kosztowna. Z drugiej jednak strony, zajście $Dterm({𝒫})$ może pozwolić, na przykład, na uznanie wyników przetwarzania za ostateczne (w konsekwencji możliwe do dalszego wykorzystania) nawet, gdy pewne wiadomości są jeszcze transmitowane.

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