Pr-1st-1.1-m10-Slajd68: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
m Zastępowanie tekstu – „ </math>” na „</math>” |
||
| Linia 9: | Linia 9: | ||
<math>\tau _e^{k+1}</math> pod warunkiem, że predykat <math>activate_i(\mathcal{AV}_i \cup \mathcal{AIT}_i)</math> miał wartość ''False'' w chwili | <math>\tau _e^{k+1}</math> pod warunkiem, że predykat <math>activate_i(\mathcal{AV}_i \cup \mathcal{AIT}_i)</math> miał wartość ''False'' w chwili | ||
<math>\tau _e^{k+1}</math> dla każdego <math>i \in \{ 1, 2, ..., n \}</math>.Ponieważ każdy proces był pasywny w przedziale | <math>\tau _e^{k+1}</math> dla każdego <math>i \in \{ 1, 2, ..., n \}</math>.Ponieważ każdy proces był pasywny w przedziale | ||
<math>\left \langle \tau _i^k, \tau _i^{k+1} \right \rangle </math>, dla każdego zachodzi: | <math>\left \langle \tau _i^k, \tau _i^{k+1} \right \rangle</math>, dla każdego zachodzi: | ||
:C6. <math>\mathcal{AV}_i[\tau ^x] \subseteq \mathcal{AV}_i[\tau _i^{k+1}]</math> | :C6. <math>\mathcal{AV}_i[\tau ^x] \subseteq \mathcal{AV}_i[\tau _i^{k+1}]</math> | ||
Aktualna wersja na dzień 10:52, 5 wrz 2023
Dowód warunku C5 (1)
Dowód warunku C5
Z konstrukcji algorytmu wynika, że algorytm ten zakończy się w chwili pod warunkiem, że predykat miał wartość False w chwili dla każdego .Ponieważ każdy proces był pasywny w przedziale , dla każdego zachodzi:
- C6.
oraz
