%% file phonebook2b.mcrl2 %% Telephone directory, modified to asynchronously report the phone number %% corresponding to the queried name. sort Name; PhoneNumber; PhoneBook = Name -> PhoneNumber; %% Phone number representing the non-existant or undefined phone number, %% must be different from any "real" phone number. map p0: PhoneNumber; %% Operations supported by the phone book. act addPhone: Name # PhoneNumber; delPhone: Name; findPhone: Name; reportPhone: Name # PhoneNumber; % Added action %% Process representing the phone book. proc PhoneDir(b: PhoneBook) = sum n: Name, p: PhoneNumber . (p != p0) -> addPhone(n, p) . PhoneDir(b[n->p]) + sum n: Name . findPhone(n) . reportPhone(n, b(n)) . PhoneDir() + sum n: Name . delPhone(n) . PhoneDir(b[n->p0]) ; %% Initially the phone book is empty. init PhoneDir(lambda n: Name . p0);