User Manual for Rodin v.2.3: Populate the Context

2.6.2 Populate the Context

In this section we model the Agatha puzzle step by step.

2.6.2.1 Modelling the Persons

We 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:

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

CONSTANTS

$\tt Agatha$

$\tt butler$

$\tt Charles$

These constants or persons respectively are part of a set:

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

SETS

$\tt persons$

Now, the constants itself are not very useful since they have no type (In addition, the constants will be highlighted in red, indicating a problem). The semantics of the sets (3.3.4) and constants (3.2.2.3) are specified in the axioms (3.2.2.3). As already mentioned above the persons are part of the set persons. We model this by creating a partition (3.3.4.7) in the AXIOMS section:

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

AXIOMS

$\tt person\_ partition :$

$\it partition(persons, \{ Agatha\} , \{ butler\} , \{ Charles\} )$

$\includegraphics[width=7mm]{img/warning_64.png}$
Please note the curly braces {} around the constants. It’s very easy to forget these, which will result in typing errors that are very hard to interpret for a novice.

$\includegraphics[width=7mm]{img/info_64.png}$
The New Enumerated Set Wizard (3.1.4.2) allows you to create the constants, the set and the axiom automatically at the same time. To access this wizard, click on the New Enumerated Set Wizard tool bar item or find it under Event-B $\rangle$ New Enumerated Set Wizard. This will bring up the wizard where we can enter the name of the set and the constants in the corresponding text fields. The wizard will create the enumarted set, the constants and the axiom automatically.

2.6.2.2 Modelling the Relations “Persons who hate each other” and “Who’s how rich”

We create two more constants hates and richer to model the relations “Persons who hate each other” and “Who’s how rich”. The relations are abstract, which means that they say nothing about the concrete persons (Agatha, the butler and Charles). We define the concrete relationships between the persons later in this section.

The first constant hates is an arbitrary relation (3.3.5) between persons:

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

AXIOMS

$\tt hate\_ relation :$

$\it hates \in persons \mathbin \leftrightarrow persons$

The second constant richer is also a relation between persons:

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

AXIOMS

$\tt richer\_ relation1 :$

$\it richer \in persons \mathbin \leftrightarrow persons$

However, we know that the relation is irreflexive (no person is richer than itself):

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

AXIOMS

$\tt richer\_ relation2 :$

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

In addition, we know that the relation is transitive:

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

AXIOMS

$\tt richer\_ relation3 :$

$\it (\forall x,y,z \mathord {\mkern 1mu\cdot \mkern 1mu}( x\mapsto y\in richer \land y\mapsto z\in richer) \mathbin \Rightarrow x\mapsto z\in richer)$

Finally, the relation is trichotomous (one person is always richer than the other or vice versa, never both directions):

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

AXIOMS

$\tt richer\_ relation4 :$

$\it (\forall x,y \mathord {\mkern 1mu\cdot \mkern 1mu}x\in persons \land y\in persons \land x\neq y \mathbin \Rightarrow (x\mapsto y\in richer \mathbin \Leftrightarrow y\mapsto x \notin richer))$

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 killer which is an element of persons:

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

CONSTANTS

$\tt killer$

AXIOMS

$\tt killer\_ type :$

$\it killer \in persons$

In addition, the puzzle have 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:

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

AXIOMS

$\tt killer\_ hates :$

$\it killer \mapsto Agatha \in hates$

$\tt killer\_ not\_ richer :$

$\it killer \mapsto Agatha \notin richer$

Charles hates no one that Agatha hates and Agatha hates everybody except the butler:

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

AXIOMS

$\tt charles\_ hates :$

$\it hates[\{ Agatha\} ] \mathbin {\mkern 1mu\cap \mkern 1mu}hates[\{ Charles\} ] = \emptyset$

$\tt agatha\_ hates :$

$\it hates[\{ Agatha\} ] = persons \setminus \{ butler\}$

The butler hates everyone not richer than aunt Agatha and the butler hates everyone whom Agatha hates. However, no one hates everyone:

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

AXIOMS

$\tt butler\_ hates\_ 1 :$

$\it \forall x\mathord {\mkern 1mu\cdot \mkern 1mu}( x\mapsto Agatha \notin richer \mathbin \Rightarrow butler\mapsto x \in hates)$

$\tt butler\_ hates\_ 2 :$

$\it hates[\{ Agatha\} ] \subseteq hates[\{ butler\} ]$

$\tt noone\_ hates\_ everyone :$

$\it \forall x \mathord {\mkern 1mu\cdot \mkern 1mu}x \in persons \mathbin \Rightarrow hates[\{ x\} ] \neq persons$

Finally, we have to model the solution:

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

AXIOMS

$\tt solution :$

$\it killer = Agatha$

We mark the axiom solution as a theorem (2.7.1) by clicking on the not theorem button¹ as shown in figure 2.12.

$\includegraphics{img/tutorial/tut_05_agatha3.png}$

Figure 2.12: Mark an Axiom as Theorem

$\includegraphics[width=7mm]{img/info_64.png}$
Theorems describe properties that are expected to be able to be derived from the axioms. Therefore, to prove a theorem you only use axioms and theorems that have already been proven.

The introduced theorem still has to be proven. Thus Rodin generates a proof obligation called solution/THM. But at this point of the tutorial we do not want to go into the details of proof yet.

$\includegraphics{img/prob.png}$ 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 “SETUP_CONTEXT” is enabled that assigns values to the constants. In our example, ProB should find a solution where Agatha is the murder. You can actually inspect the axioms and the theorem in the state view to see why they are fulfilled.
This contribution requires the ProB plugin. The content is maintained by the plugin contributors and may be out of date.

This concludes the tutorial. The following section shows the complete Context.

Footnotes

Yes, this sounds wrong. However, the button is a toggle button, so after clicking it, the label changes to “theorem”. The button always displays the current state.

Rodin Handbook

2.6.2 Populate the Context

2.6.2.1 Modelling the Persons

2.6.2.2 Modelling the Relations “Persons who hate each other” and “Who’s how rich”

2.6.2.3 Modelling the “Crime”