Rodin HandbookThis work is sponsored by the Deploy Project This work is sponsored by the ADVANCE Project This work is licensed under a Creative Commons Attribution 3.0 Unported License |
2.9.5 The Celebrity algorithmWe 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. is the set of persons, each represented by a number, is the celebrity we are looking for and 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 can be any person initially and the event celebrity finds the celebrity in one step. After the event celebrity has occurred, 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 exists and the algorithm simply returns it. Later in the refinement, we will model how to find the celebrity without using . Because of the refinement relation, we know that the algorithm works correctly.
So let’s have a look at the first refinement Celebrity_1. A variable is introduced which contains a subset of the persons, the potential celebrities. We start with being all persons. Two new events, remove_1 and remove_2, are added to remove people from 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 . 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 into one arbitrary person – the candidate – and the “rest” . remove_1 then removes a person from if knows . remove_2 checks if there is a person in that does not know the candidate. If found, is the new candidate and is removed from the rest . If 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 persons with the numbers .
Instead of having an abstract data structure like a set, the third refinement just introduces an index variable that points to the first person of , which is the group of people who have not yet been checked. Instead of taking an arbitrary element from as in the second refinement, the remove events just takes the first element . is then removed from by increasing it by one. When is larger then , is empty and contains the result. This last refinement works only on the following three integer variables: The index , the candidate and the result . 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:
|