Sr-3-wyk-1.0-Slajd4
Model matematyczny
W definicjach specyfikacji wystąpią następujące zbiory:
P – zbiór procesów w systemie;
M – zbiór wiadomości przesyłanych w systemie;
VID – zbiór identyfikatorów obrazów grup.
Wyróżnia się następujące elementarne zdarzenia w systemie:
wyślij(p , m) – proces p wysyła wiadomość m ; zauważmy, że nie określa się odbiorcy, gdyż wiadomość wysyłana jest do całej grupy
odbierz(p , m) – proces p odbiera wiadomość m ; nadawca wiadomości może być określony, ale tutaj dla uproszczenia nie jest;
zmiana_obrazu(p , <id, członkowie>) – w procesie p następuje zmiana obrazu; nowy obraz o identyfikatorze id zawiera procesy określone zmienną członkowie . Sam obraz zaś jest parą (id , członkowie ), obejmującą globalny identyfikator obrazu i należące do niego procesy. Dwa obrazy V i V’ są więc równe wtedy i tylko wtedy, gdy równe są ich identyfikatory oraz zbiory procesów.
awaria(p ) – proces p ulega awarii
powrót(p ) – proces p wznawia działanie po awarii
