- 1 użytkownik = 1 proces
- nie ma rozróżnienia pomiędzy numerem telefonu a samym telefonem
- numer telefonu rozpatrujemy jako całość (nie dzielimy na cyfry)
- proces przyjmuje rolę inicjującego lub odbierającego połączenie (tylko
strona inicjująca może zakończyć połączenie)
WERYFIKACJA
Autorzy skupiają się na dwóch własnościach modelu
- połączenie między dwoma użytkownikami jest zawsze możliwe
<>connect[1].to[2] == 1,
<>connect[2].to[1] == 1, ...
Dla 4 procesów, na 64 MB pamięci nie dało się w pełni udowodnić tej własności - 7 z 12 kombinacji prowadziło do wyczerpania pamięci. Prawdopodobnie kolejność inicjalizacji ma w tym przypadku znaczenie.
Dla 3 procesów udało się pokazać, że warunek ten jest zawsze spełniony.
- jeśli zadzwonisz do siebie to usłyszysz sygnał zajętości
[](partner1 == one -> <> event1== engaged),
[](partner2 == two -> <> event1== engaged)
Dla 3 procesów nie udało się w pełni udowodnić tej własności (nawet z opcją supertrace) , jednak nie została ona podważona nawet na głębokości 290K.
