A Telephone Book

Contribution of this section

1. use of functions with updates,

2. modelling considerations,

3. realistic verification process and its problems.

New tools: none.

In this section we describe the model of a telephone book in mCRL2. We base our model on the following requirements:

1. A phone book shall store phone numbers.

2. It shall be possible to add and delete entries from a phone book.

3. It shall be possible to retrieve a phone number given a name.

By looking at these requirements, we identify the following entities:

• phone book

• phone number

• name

We start by giving abstract types for phone numbers and names; their concrete form will be given later. For the phone book we decide that it is a mapping of names to numbers. This gives us the following specification of sorts.

sort Name;
     PhoneNumber;
     PhoneBook = Name -> PhoneNumber;

As an mCRL2 user, you need to be aware that the types as given here, are predetermined. This means that they cannot be extended on the fly. As a consequence, all names and phone numbers that can ever be added to the phone book must be known upfront.

If we again look at the requirements, our phone book must support the following operations:

• addPhone adds a phone number for a name,

• delPhone deletes a phone number corresponding to a name, and

• findPhone finds the phone number corresponding to a name.

These operations will be the actions of our process. We need to decide on the parameters that the actions are going to take. We assume that our process will support a single phone book, i.e. the process itself models a phone book. It is then natural to model addPhone with parameters Name and PhoneNumber, delPhone with a Name, and findPhone with a Name. This gives rise to the following action specification.

% Operations supported by the phone book.
act  addPhone: Name # PhoneNumber;
     delPhone: Name;
     findPhone: Name;

We now need to take care that not every number is in every phone book. In order to describe a phone book as a total function, we introduce a special phone number, p0, to indicate that a name has no associated phone number.

% Phone number representing the non-existant or undefined phone number,
% must be different from any "real" phone number.
map  p0: PhoneNumber; 

Given this decision, we can specify the empty phone book as the phone book that maps every name to p0.

lambda n: Name . p0;

In modelling the empty phone book we use lambda abstraction. In this expression lambda n: Name says that we are defining a function that takes arguments of type Name, and for each name produces p0 as a result. As p0 is of type PhoneNumber, lambda n: Name . p0 describes a function of type Name ->PhoneNumber, which is by definition equal to PhoneBook.

Given a function b of type PhoneBook, a name n and a phone number p, we can set the value of n in b to p using the expression b[n -> p]. This has as property that, for all names m != n, b[n -> p](m) = b(m), and b[n -> p](n) = p.

Using the above ingredients, we can model a simple phone book using the following specification, that is also available as phonebook1.mcrl2.

% file phonebook1.mcrl2
% Telephone directory as it is described as PVS example

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;

% Process representing the phone book.
proc PhoneDir(b: PhoneBook) = 
     sum n: Name, p: PhoneNumber . addPhone(n, p) . PhoneDir(b[n->p])
   + sum n: Name . findPhone(n) . PhoneDir()
   + sum n: Name . delPhone(n) . PhoneDir(b[n->p0])
   ;
   
% Initially the phone book is empty.
init PhoneDir(lambda n: Name . p0);

Exercise

There are some obvious flaws in the phone book that we have specified. Can you find and explain them?

Hint

Think about the special meaning of phone number p0, and explain the findPhone function to yourself.

Solution

In this specification, the “special” phone number p0 can be assigned to a name freely. Furthermore, a findPhone action can be performed, but the actual phone number is never reported.

Exercise

Fix these issues in the above specification.

Solution

Preventing the assignment of p0 to a name can easily prevented by guarding the addPhone action with p != p0. Fixing the second issue requires some more thought. There are two possible ways around fixing the problem. We can either assume that reporting of the result is immediate, and add the resulting phone number as a parameter to the findPhone action, or we can assume that querying for a phone number is asynchronous, and my take time, and split the query into the action initiating the query (findPhone) and an action reporting the result, e.g. reportPhone.

The first approach is suitable when, e.g., modelling a phone book that is a library in a synchronous program in, say, C or Java. In that case indeed the program pointer of the calling program will not change before the result has been returned, making a model in which reporting the result a faithful representation of reality. This variation is implemented in the following specification (available as phonebook2a.mcrl2). The result is obtained instantaneously. Watch the extra parameter to addPhone.

%% file phonebook2a.mcrl2
%% Telephone directory, modified to actually report the phone number as an
%% answer to a query instantaneously.

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 # PhoneNumber; % Added phone number as argument

%% 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,b(n)) . PhoneDir()
   + sum n: Name . delPhone(n) . PhoneDir(b[n->p0])
   ;
   
%% Initially the phone book is empty.
init PhoneDir(lambda n: Name . p0);

If we are, e.g., modelling a phone book that is a web service, where a client performs a request, and in the meantime may do other kinds of actions like sending requests to other web services, the previous approach provides too coarse an abstraction. In this case it is more accurate to use the second approach, in which performing the query and obtaining the result are truely decoupled. This variation is given by the following specification (available as phonebook2b.mcrl2).

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

In the rest of this tutorial we will stick to the specification with asynchronous reporting (the second variation in the previous exercise).

In complex specifications, it can be convenient to introduce additional functions, with descriptive names, that take care of the modifications of parameters that is done in the process. As a bonus this usually makes it easier to change the data structures used in a specification.

Exercise

Modify the specification in phonebook2b.mcrl2 by adding functions emptybook, add_phone, del_phone and find_phone with the following signatures.

map  emptybook: PhoneBook;
     add_phone: PhoneBook # Name # PhoneNumber -> PhoneBook;
     del_phone: PhoneBook # Name -> PhoneBook;
     find_phone: PhoneBook # Name -> PhoneNumber;

Define equations implementing the above operations.

Solution

A solution to the above exercise is given by the following specification (also available as phonebook3.mcrl2).

%% file phonebook3.mcrl2
%% Telephone directory, modified to asynchronously report the phone number
%% corresponding to the queried name. Functions have been added to increase
%% readability and flexibility.

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; 
     emptybook: PhoneBook;
     add_phone: PhoneBook # Name # PhoneNumber -> PhoneBook;
     del_phone: PhoneBook # Name -> PhoneBook;
     find_phone: PhoneBook # Name -> PhoneNumber;

eqn  emptybook = lambda n: Name . p0;

var b: PhoneBook;
    n: Name;
    p: PhoneNumber;
eqn  add_phone(b, n, p) = b[n->p];
     del_phone(b, n) = b[n->p0];
     find_phone(b, n) = b(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) . reportPhone(n, find_phone(b,n)) . PhoneDir()
   + sum n: Name . delPhone(n) . PhoneDir(del_phone(b,n))
   ;
   
%% Initially the phone book is empty.
init PhoneDir(emptybook);

It should be noted that, instead of using a function of names to phone numbers, we could also have modelled the phone book using a set of pairs of names and phone numbers. A model using sets is likely to become complicated in this case.

Exercise

Modify the specification in phonebook3.mcrl2 such that it uses a set of pairs of names and phone numbers instead of function from names to phone numbers to store the phone numbers internally.

Solution

A possible solution to this exercise is given in phonebook4.mcrl2. Note that the function find_phone cannot be implemented using sets, because no concrete elements can be taken from the set. Therefore, the functionality of find_phone is modelled using the sum operator on a process level.

In the rest of this chapter we stick to the model in which functions occur directly in the specification (phonebook2b.mcrl2). We are going to check whether our model makes sense using the µ-calculus.

A suitable property for our specification is the following:

“if a name n with phone number p is added to the phone book, and a lookup of name n is performed, then phone number p should be reported, provided that in the meantime no other phone number has been added for name n, and the phone number for name n has not been deleted”.

Exercise

Write the above propery in the µ-calculus.

Solution

A solution (available as phonebook1.mcf) is the following:

forall n: Name, p,r: PhoneNumber .
  [true* . addPhone(n,p) .
     !(delPhone(n) || exists q: PhoneNumber . addPhone(n, q))* .
     findPhone(n) .
     !(delPhone(n) || exists q: PhoneNumber . addPhone(n, q))* .
     reportPhone(n, r)] val(p == r)

Exercise

Try to verify this property using the tools. What do you observe?

Hint

You need to use the tools mcrl22lps, lps2pbes and pbes2bool.

Solution

We try checking this property using the following command:

$ mcrl22lps phonebook2b.mcrl2 | lps2pbes -f phonebook1.mcf | pbes2bool
[20:54:11.222 error]   Cannot find a term of sort Name

Observe that the tools fail to verify this requirement because of an error.

The tool is telling you that it wants to find some representative term of sort Name, but is not able to do so. This indeed makes sense as we have not given a specification of names and phone numbers yet.

Exercise

Fix the specification by making sure there are 3 names, and 3 phone numbers (apart from the special phone number p0). Rerun the verification on the fixed specification.

Solution

The following is a fixed specification (also available as phonebook5.mcrl2).

%% 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;
     
map emptybook: Name -> PhoneNumber;
var n: Name;
eqn emptybook(n) = p0;

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

The specification is now easily checked using the following sequence of commands:

$ mcrl22lps phonebook5.mcrl2 | lps2pbes -f phonebook1.mcf | pbes2bool
true

Exercise

Verify whether the following property holds for phonebook5.mcrl2.

“if a name n with phone number p is added to the phone book, and a lookup of name n is performed, then phone number p should be reported, provided that in the meantime the phone number for name n has not been deleted”.

You first need to formalise this property as a µ-calculus formula, and then verify whether it holds. Explain the outcome of the verification.

Solution

The following formula (available as phonebook2.mcf) formalises this property.

forall n: Name, p,r: PhoneNumber .
  [true* . addPhone(n,p) .
     !delPhone(n)* .
     findPhone(n) .
     !delPhone(n)* .
     reportPhone(n, r)] val(p == r)

It can be verified using the commands:

$ mcrl22lps phonebook5.mcrl2 | lps2pbes -f phonebook2.mcf | pbes2bool
false

Observe that this verification fails because addPhone allows you to add a phone number for a person that already has a phone number. If a new phone number is added for such a person, the original phone number is overwritten.

Exercise

Modify the specification in phonebook5.mcrl2 such that addPhone(n,p) can only be executed if no phone number for name n is known. Furthermore, extend the specification with and action changePhone with the following signature

changePhone: Name # PhoneNumber

such that changePhone(n,p) can only be executed if n already has a phone number, and that afterwards the phone number of n has been updated to p. Save the result as phonebook6.mcrl2

Solution

A sample solution is the following (phonebook6.mcrl2)

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

Exercise

Verify whether your new specification satisfies the property you formulated before. Explain the outcome.

Solution

For our version of the property, the verification delivers the following result:

$ mcrl22lps phonebook6.mcrl2 | lps2pbes -f phonebook2.mcf | pbes2bool
false

Exercise

If the verification in the previous exercise failed, think about the influence of the changePhone action on the validity of the property you are trying to check. Describe the changed property in natural language, give the modal µ-calculus formula, and do the verification.

Solution

Our modified property is the following (phonebook3.mcf).

forall n: Name, p,r: PhoneNumber .
  [true* . addPhone(n,p) .
     !(delPhone(n) || exists q: PhoneNumber . changePhone(n, q))* .
     findPhone(n) .
     !(delPhone(n) || exists q: PhoneNumber . changePhone(n, q))* .
     reportPhone(n, r)] val(p == r)

Now the following verification succeeds:

$ mcrl22lps phonebook6.mcrl2 | lps2pbes -f phonebook3.mcf | pbes2bool
false

As an alternative approach to the verification, you can make the phonebook that is used internally available externally through a getPhoneBook action. A specification in which this modification has been made is the following (phonebook7.mcrl2).

%% file phonebook7.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
     getPhoneBook: PhoneBook;

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])
   + getPhoneBook(b) . PhoneDir()
   ;
   
%% Initially the phone book is empty.
init PhoneDir(emptybook);

Our last property (phonebook3.mcf) can now also be formulated as follows (phonebook4.mcf) using the internally stored phonebook.

forall n: Name, p: PhoneNumber . forall b: PhoneBook .
  [true* . addPhone(n,p) .
     !(delPhone(n) || exists q: PhoneNumber . changePhone(n, q))* .
     findPhone(n) .
     !(delPhone(n) || exists q: PhoneNumber . changePhone(n, q))*]
     [getPhoneBook(b)] val(b(n) == p)

The verification result is still the same:

$ mcrl22lps phonebook7.mcrl2 | lps2pbes -f phonebook4.mcf | pbes2bool
false