Rodin Handbook





 

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