Pr-1st-1.1-m09-Slajd17: Różnice pomiędzy wersjami
m Zastępowanie tekstu – „ </math>” na „</math>” |
m Zastępowanie tekstu – „<math> ” na „<math>” |
||
| Linia 15: | Linia 15: | ||
W chwili <math>\tau</math>, gdy <math>Dterm(\mathcal{P}) = True</math>, wszystkie procesy <math>P_i</math> są pasywne, zachodzi | W chwili <math>\tau</math>, gdy <math>Dterm(\mathcal{P}) = True</math>, wszystkie procesy <math>P_i</math> są pasywne, zachodzi | ||
<math>activate_i (\mathcal{AV}_i \cup \mathcal{IT}_i)[\tau]</math>, 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 <math>activate_i (\mathcal{AV}_i \cup \mathcal{IT}_i))</math>. | <math>activate_i (\mathcal{AV}_i \cup \mathcal{IT}_i)[\tau]</math>, 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 <math>activate_i (\mathcal{AV}_i \cup \mathcal{IT}_i))</math>. | ||
Wobec niezawodności kanałów, wiadomości transmitowane osiągną węzły docelowe po skończonym choć nieprzewidywalnym czasie, w pewnym momencie <math> \tau ' > \tau</math>. Wówczas <math>\mathcal{IT}_i[\tau '] = \emptyset</math>. Wobec stałej pasywności wszystkich procesów od chwili \tau, w każdej chwili <math> \tau ' ' : \tau ' > \tau ''</math>, <math>\mathcal{AV}_i[\tau ' '] = \mathcal{AVI}_i[\tau] \cup \mathcal{IT}_i[\tau]</math> oraz | Wobec niezawodności kanałów, wiadomości transmitowane osiągną węzły docelowe po skończonym choć nieprzewidywalnym czasie, w pewnym momencie <math>\tau ' > \tau</math>. Wówczas <math>\mathcal{IT}_i[\tau '] = \emptyset</math>. Wobec stałej pasywności wszystkich procesów od chwili \tau, w każdej chwili <math>\tau ' ' : \tau ' > \tau ''</math>, <math>\mathcal{AV}_i[\tau ' '] = \mathcal{AVI}_i[\tau] \cup \mathcal{IT}_i[\tau]</math> oraz | ||
<math>\mathcal{IT}_i[\tau ''] = \emptyset</math>.Stąd otrzymujemy: | <math>\mathcal{IT}_i[\tau ''] = \emptyset</math>.Stąd otrzymujemy: | ||
Aktualna wersja na dzień 22:16, 11 wrz 2023
Zakończenie dynamiczne \leftrightarrow statyczne
Niech oznacza, że zajście predykatu prowadzi w skończonym choć nieprzewidzianym czasie do zajścia predykatu .
Twierdzenie 9.1
Dowód
W chwili , gdy , wszystkie procesy są pasywne, zachodzi , 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 . Wobec niezawodności kanałów, wiadomości transmitowane osiągną węzły docelowe po skończonym choć nieprzewidywalnym czasie, w pewnym momencie . Wówczas . Wobec stałej pasywności wszystkich procesów od chwili \tau, w każdej chwili , oraz .Stąd otrzymujemy:
Predykat przyjmuje zatem wartość True.
Udowodniliśmy więc, że opóźnienie między momentem zajścia predykatu a momentem zajścia predykatu 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 będzie trudniejsza, a więc w ogolności bardziej kosztowna. Z drugiej jednak strony, zajście 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.
