**Contribution of this section**

- use of functions with updates,
- modelling considerations,
- 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:

- A phone book shall store phone numbers.
- It shall be possible to add and delete entries from a phone book.
- 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 namenwith phone numberpis added to the phone book, and a lookup of namenis performed, then phone numberpshould be reported, provided that in the meantime no other phone number has been added for namen, and the phone number for namenhas 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?

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 namenwith phone numberpis added to the phone book, and a lookup of namenis performed, then phone numberpshould be reported, provided that in the meantime the phone number for namenhas 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
```