%% file phonebook4.mcrl2 %% Telephone directory, modified to asynchronously report the phone number %% corresponding to the queried name. Functions have been added to increase %% readability and flexibility, and instead of functions, sets are used. sort Name; PhoneNumber; Pair = struct pair(name: Name, phone: PhoneNumber); PhoneBook = Set(Pair); %% Phone number representing the non-existant or undefined phone number, %% must be different from any "real" phone number. map p0: PhoneNumber; emptybook: PhoneBook; add_phone: PhoneBook # Name # PhoneNumber -> PhoneBook; del_phone: PhoneBook # Name -> PhoneBook; eqn emptybook = {}; var b: PhoneBook; n: Name; p: PhoneNumber; eqn add_phone(b, n, p) = b + {pair(n, p)}; del_phone(b, n) = { x: Pair | x in b && name(x) != n }; % alternative definition for del_phone: % del_phone(b, n) = b - { x: Pair | name(x) == n }; %% 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(add_phone(b,n,p)) + sum n: Name . findPhone(n) . sum p: PhoneNumber . (pair(n, p) in b) -> reportPhone(n, p) . PhoneDir() + sum n: Name . delPhone(n) . PhoneDir(del_phone(b,n)) ; %% Initially the phone book is empty. init PhoneDir(emptybook);