Rodin User’s Handbook v.2.8: The Celebrity algorithm

2.9.5 The Celebrity algorithm

We will now take a brief tour through the model to see how the problem and algorithm are 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.

$\includegraphics[width=7mm]{img/pencil_64.png}$

CONTEXT

Celebrity_c0

CONSTANTS

$\tt k$

$\tt c$

$\tt P$

AXIOMS

$\tt axm1 :$

$\it P \subseteq \mathord {\mathbb N}$

$\tt axm2 :$

$\it c \in P$

$\tt axm3 :$

$\it k \in (P \setminus \{ c\} ) \mathbin \leftrightarrow P$

$\tt axm4 :$

$\it k^{-1} [\{ c\} ] = P \setminus \{ c\}$

$\tt axm5 :$

$\it k \mathbin {\mkern 1mu\cap \mkern 1mu}id = \emptyset$

END

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 has occurred, $r$ contains the result of the algorithm. You might then wonder why there is a problem if you can just pick the celebrity and assign it to the result. This is because we defined our problem in such a way so that we are certain a celebrity $c$ exists and the algorithm simply returns it. Later in the refinement, we will model how to find the celebrity without using $c$ . Because of the refinement relation, we know that the algorithm works correctly.

$\includegraphics[width=7mm]{img/pencil_64.png}$

MACHINE

Celebrity_0

SEES

Celebrity_c0

VARIABLES

$\tt r$

INVARIANTS

$\tt inv1 :$

$\it r \in P$

EVENTS

Initialisation

begin

$\tt act1 :$

$\it r :\in P$

end

Event

celebrity $\mathrel {\widehat=}$

begin

$\tt act1 :$

$\it r := c$

end

END

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 to remove people 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. An invariants states 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. (We do not show the machine here because it simply takes up too much space — please consult the project that you imported earlier to inspect the model.)

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$ .

$\includegraphics[width=7mm]{img/pencil_64.png}$

CONTEXT

Celebrity_c1

EXTENDS

Celebrity_c0

CONSTANTS

$\tt n$

AXIOMS

$\tt axm1 :$

$\it n \in \mathord {\mathbb N}$

$\tt axm2 :$

$\it n > 0$

$\tt axm3 :$

$\it P = 0\mathbin {.\mkern 1mu.}n$

END

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 $R$ , which is the group of people who have not yet been checked. 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$ 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.5 The Celebrity algorithm