%% 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);