## 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.6.2 Populate the ContextIn this section we model the Agatha puzzle step by step. ## 2.6.2.1 Modelling the PersonsWe have three persons in the Agatha puzzle: Agatha herself, the butler and Charles. We model the three persons as constants (one constant for each person) in the corresponding CONSTANTS section:
These constants or persons respectively are part of a set:
Now the constants themselves are not very useful since they have no type (after creating the constants, they will be highlighted in red, which indicates a problem). The semantics of the sets (3.3.4) and constants (3.2.3.3) are specified in the axioms (3.2.3.3). As already mentioned above the persons are part of the set
## 2.6.2.2 Modelling the Relations “Persons who hate each other” and “Who’s how rich”We create two more constants The first constant
The second constant
However, we know that the relation is irreflexive (no person is richer than itself):
In addition, we know that the relation is transitive:
Finally, the relation is trichotomous (one person is always richer than the other or vice versa, never both directions):
## 2.6.2.3 Modelling the “Crime”Since the objective of the puzzle is to find the killer, we have to create a new constant
In addition, the puzzle has some more relationships between the different persons which are all modelled as axioms. We know that the killer hates his victim and is no richer than his victim:
Charles hates no one that Agatha hates and Agatha hates everybody except the butler:
The butler hates everyone not richer than aunt Agatha and the butler hates everyone whom Agatha hates. However, no one hates everyone:
Finally, we have to model the solution:
All axioms are set to “not theorem” when they are created. But we need the solution to be a theorem so that we can prove that it is valid. In order to do this, click on not theorem shown to the right of the axiom solution. This box will automatically change to theorem, and you will have set the axiom as a theorem as shown in Figure 2.12.
The introduced theorem still has to be proven. Thus Rodin generates a proof obligation called solution/THM. However, at this point of the tutorial we do not want to go into more detail about proving yet. You can use ProB to animate contexts, too. Just right-click on the context in the explorer and select Start Animation / Model Checking. If ProB finds solutions for the specified constants that fulfil the axioms, an event “ This concludes the tutorial about contexts. The following section shows the complete Context. |