User Manual for Rodin v.2.3: The Celebrity algorithm

2.9.3 The Celebrity algorithm

We take a brief tour through the model to see how the problem and algorithm is specified. The celebrity problem itself is described in the context Celebrity_c0. There are three constants. $P$ is the set of persons, each represented by a number, $c$ is the celebrity we are looking for and $k$ is the “knows” relation between the persons. The axioms encode the properties about the “knows” relation that we stated above.

In the most abstract machine Celebrity_0 we specify what the algorithm should do. The variable $r$ can be any person initially and the event celebrity finds the celebrity in one step. After the event celebrity occurred, $r$ contains the result of the algorithm. You might ask yourself, what is the problem if we can just pick the celebrity and assign it to the result? The answer is that we wrote down our problem in a way that we know that there is a celebrity $c$ and we specify the algorithm by stating it should return it. Later in the refinement we model how to find the celebrity without using $c$ anymore. By the refinement relation we know then that the algorithm works correctly.

So let’s have a look at the first refinement Celebrity_1. A variable $Q$ is introduced which contains a subset of the persons, the potential celebrities. We start with $Q$ being all persons. Two new events remove_1 and remove_2 are added that remove persons from $Q$ who cannot be the celebrity. remove_1 removes a person that knows somebody while remove_2 removes a person that is not known by any other person. As an invariant we state that the celebrity is always in $Q$ . When there is just one person left in the set, we know that this is the celebrity.

The second refinement Celebrity_2 then splits the potential celebrities $Q$ into one arbitrary person – the candidate $b$ – and the “rest” $R$ . remove_1 then removes a person $x$ from $R$ if $b$ knows $x$ . remove_2 checks if there is a person $x$ in $R$ that does not know the candidate. If found, $x$ is the new candidate $b$ and is removed from the rest $R$ . If $R$ is empty, we know that the candidate is the celebrity.

The third refinement then makes some more assumptions about the given problem. The context Celebrity_c1 extends Celebrity_c0 and states that there are $n+1$ persons with the numbers $0\mathbin {.\mkern 1mu.}n$ . Instead of having an abstract data structure like a set, the third refinement just introduces an index variable $a$ that points to the first person of the rest. Instead of taking an arbitrary element from $R$ as in the second refinement, the remove events just takes the first element $a$ . $a$ is then removed from $R$ just by increasing it by one. When $a$ is larger then $n$ , $R$ is empty and $b$ contains the result.

This last refinement works only on the following three integer variables: The index $a$ , the candidate $b$ and the result $r$ . Each event is deterministic and in every step only one event is enabled. The events together can be interpreted as an implementation of the algorithm:

$r \mathrel {:\mkern 1mu=}0$	// initialisation `act1`
$a \mathrel {:\mkern 1mu=}1$	// initialisation `act2`
$b \mathrel {:\mkern 1mu=}0$	// initialisation `act3`
while $a\leq n$ do	// guard in `remove_1` and `remove_2`
if $a\mapsto b\in k$ then	// guard in `remove_1` and negated in `remove_2`
$a \mathrel {:\mkern 1mu=}a+1$	// action in `remove_1`
else	// $a\mapsto b\not\in k$
$b \mathrel {:\mkern 1mu=}a$	// action `act1` in `remove_2`
$a \mathrel {:\mkern 1mu=}a+1$	// action `act2` in `remove_2`
end if
end while
$r \mathrel {:\mkern 1mu=}b$	// action in `celebrity`

Rodin Handbook

2.9.3 The Celebrity algorithm