Pr-1st-1.1-m10-Slajd51: 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 7: | Linia 7: | ||
Z konstrukcji algorytmu wynika, że w każdym cyklu detekcyjnym odpowiedź jest opóźniana do momentu uzyskania przez predykat <math>\neg activate(\mathcal{AV}_i)</math> wartości ''True'' . Skoro algorytm kończy się w chwili | Z konstrukcji algorytmu wynika, że w każdym cyklu detekcyjnym odpowiedź jest opóźniana do momentu uzyskania przez predykat <math>\neg activate(\mathcal{AV}_i)</math> wartości ''True'' . Skoro algorytm kończy się w chwili | ||
<math>\tau _i^{k+1}</math>, to predykat <math>activate(\mathcal{AV}_i)[\tau _'i^{k+1} ]</math> miał wartość ''False'' . Ponieważ w przedziale | <math>\tau _i^{k+1}</math>, to predykat <math>activate(\mathcal{AV}_i)[\tau _'i^{k+1} ]</math> miał wartość ''False'' . Ponieważ w przedziale | ||
<math> \left \langle \tau _i^k, \tau _i^{k+1} \right \rangle</math> | <math>\left \langle \tau _i^k, \tau _i^{k+1} \right \rangle</math> | ||
proces <math>P_i</math> był przez cały czas pasywny, żadna wiadomość nie została w tym czasie odebrana. | proces <math>P_i</math> był przez cały czas pasywny, żadna wiadomość nie została w tym czasie odebrana. | ||
[[Pr-1st-1.1-m10-Slajd50 | << Poprzedni slajd]] | [[Pr-1st-1.1-m10-toc|Spis treści ]] | [[Pr-1st-1.1-m10-Slajd52 | Następny slajd >>]] | [[Pr-1st-1.1-m10-Slajd50 | << Poprzedni slajd]] | [[Pr-1st-1.1-m10-toc|Spis treści ]] | [[Pr-1st-1.1-m10-Slajd52 | Następny slajd >>]] | ||
Aktualna wersja na dzień 22:13, 11 wrz 2023
Dowód warunku C3 (1)
Dowód warunku C3
Z konstrukcji algorytmu wynika, że w każdym cyklu detekcyjnym odpowiedź jest opóźniana do momentu uzyskania przez predykat wartości True . Skoro algorytm kończy się w chwili , to predykat miał wartość False . Ponieważ w przedziale proces był przez cały czas pasywny, żadna wiadomość nie została w tym czasie odebrana.
