Pr-1st-1.1-m09-Slajd11

Definicja formalna: Oznaczenia (1)

W sformułowaniu formalnym tego problemu, podobnie jak w sformułowaniu problemu zakleszczenia, wykorzystamy następujące oznaczenia:

$p a s s i v e_{i}$ – zmienna logiczna (predykat) przyjmująca wartość True wtedy i tylko wtedy, gdy proces $P_{i}$ jest pasywny
$a v a i l a b l e_{i}$ – tablica [1..n ] zmiennych logicznych procesu $P_{i}$ skojarzona z wiadomościami dostępnymi
$a v a i l a b l e_{i} [j]$ – j-ty element tablicy $a v a i l a b l e_{i}$ przyjmujący wartość True, gdy dla $P_{i}$ jest dostępna wiadomość wysłana przez $P_{j}$