Pr-1st-1.1-m10-Slajd67: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
m Zastępowanie tekstu – „<math> ” na „<math>” |
m Zastępowanie tekstu – „,...,” na „,\ldots,” |
||
| Linia 9: | Linia 9: | ||
:<math>\tau _b^k < \tau _e^k \le \tau ^x \le \tau _b^{k+1} < \tau _e^{k+1}</math> | :<math>\tau _b^k < \tau _e^k \le \tau ^x \le \tau _b^{k+1} < \tau _e^{k+1}</math> | ||
W dalszej części dowodu pokażemy, że jeżeli algorytm zakończy się w chwili <math>\tau _e^{k+1}</math> z <math>dTerminationDetected_{\alpha}[\tau _e^{k+1}] = True</math>, to <math>Dterm(\mathcal{P})[\tau ^t] = True</math>. Oznacza to dalej, że są spełnione następujące dwa warunki dla każdego <math>Q_i, i \in \{1, 2, | W dalszej części dowodu pokażemy, że jeżeli algorytm zakończy się w chwili <math>\tau _e^{k+1}</math> z <math>dTerminationDetected_{\alpha}[\tau _e^{k+1}] = True</math>, to <math>Dterm(\mathcal{P})[\tau ^t] = True</math>. Oznacza to dalej, że są spełnione następujące dwa warunki dla każdego <math>Q_i, i \in \{1, 2,\ldots, n \}</math>, | ||
:C4. <math>passive_i</math> [<math>\tau ^x</math>] = ''True'' (Wszystkie procesy są pasywne w chwili <math>\tau ^x</math>) | :C4. <math>passive_i</math> [<math>\tau ^x</math>] = ''True'' (Wszystkie procesy są pasywne w chwili <math>\tau ^x</math>) | ||
:C5. <math>activate_i(\mathcal{AV}_i \cup \mathcal{IT}_i)[\tau ^x] = False</math> (Ani wiadomości już dostępne, ani znajdujące się w kanałach komunikacyjnych nie wystarczą do uaktywnienia procesu <math>P_i</math>) | :C5. <math>activate_i(\mathcal{AV}_i \cup \mathcal{IT}_i)[\tau ^x] = False</math> (Ani wiadomości już dostępne, ani znajdujące się w kanałach komunikacyjnych nie wystarczą do uaktywnienia procesu <math>P_i</math>) | ||
Aktualna wersja na dzień 21:57, 15 wrz 2023
Szkic dowodu twierdzenia 10.5
Dowód
Oznaczymy dwa ostatnie cykle detekcyjne odpowiednio przez k ik+1 , a przez taki moment, że:
W dalszej części dowodu pokażemy, że jeżeli algorytm zakończy się w chwili z , to . Oznacza to dalej, że są spełnione następujące dwa warunki dla każdego ,
- C4. [] = True (Wszystkie procesy są pasywne w chwili )
- C5. (Ani wiadomości już dostępne, ani znajdujące się w kanałach komunikacyjnych nie wystarczą do uaktywnienia procesu )
Dowód warunku C4 pomijamy, jako identyczny jak w przypadku warunku C1 dla twierdzenia o poprawności algorytmu zakończenia detekcji zakończenia statycznego.
