%% file phonebook5.mcrl2
%% Telephone directory, modified to asynchronously report the phone number
%% corresponding to the queried name. The sorts Name and PhoneNumber are
%% constrained to have a small, constant number of elements.
sort Name = struct n0 | n1 | n2;
%% Phone number p0 is assumed to represent the non-existant or undefined phone number,
%% must be different from any "real" phone number.
%% This is already guaranteed by definition of a structured sort
PhoneNumber = struct p0 | p1 | p2 | p3 ;
PhoneBook = Name -> PhoneNumber;
%% Operations supported by the phone book.
act addPhone: Name # PhoneNumber;
changePhone: Name # PhoneNumber;
delPhone: Name;
findPhone: Name;
reportPhone: Name # PhoneNumber; % Added action
map emptybook: Name -> PhoneNumber;
var n: Name;
eqn emptybook(n) = p0;
%% Process representing the phone book.
proc PhoneDir(b: PhoneBook) =
sum n: Name, p: PhoneNumber . (p != p0 && b(n) == p0) -> addPhone(n, p) . PhoneDir(b[n->p])
+ sum n: Name, p: PhoneNumber . (p != p0 && b(n) != p0) -> changePhone(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(emptybook);