User Manual for Rodin v.2.3: First Refinement

2.10.2 First Refinement

Now we are going to explain the main complexity of our model: the deadlock freeness proof for the first refinement.

The difference between the first refinement and the initial model is that a new constant com been added in order to describe which rooms are connected. Additionally, we have a constant exit, which will be explained later.

The event INITIALISATION does not change, but the event PASS is refined as a consequence. We assume that a person can move to another location l if they have the authorization to be in l (already defined in the abstraction) and also if the location l is connected to the location p where the person is at this precise moment (represented by sit(p)).

We need to add a new guard that is more exact that that of the machine it refines:

$( sit(p) \mapsto l \in com ) \Rightarrow ( sit(p)\neq l )$

We are faced with a difficulty here; it is not possible to prove that the refined event PASS does not happen less often than the abstract event PASS of its predecessor. To prove this we would have to prove that the guard of the abstract event implies that of the concrete event.

The issue is that this condition cannot be verified in general. Moreover, the failure to prove the above condition indicates that there are possibilities that certain people could stay permanently blocked in locations. People are also more limited in the ways that they may move because they can only move between rooms that are connected.

Now we know that this model contains a problem ignored in the document requirements. We must now find a sufficient solution.

$\includegraphics[width=7mm]{img/info_64.png}$
Please note that post-tactics should still be disabled before starting this part of the tutorial.

At the beginning of this section we need to come back to the Event-B Perspective. As described in Section 2.10.1, open door_1 machine and add a derived invariant (theorem) called DLF as follows:

INVARIANTS

$\tt DLF :$: $\it \exists q, m \cdot (q \mapsto m \in aut \wedge sit(q) \mapsto m \in com)$

Save the file. Once again, the prover fails to prove the deadlock freeness automatically. Actually all we want to prove is that “any person authorized to be in a location must also be authorized to go in another location which communicates with the first one”.

This can be illustrated as demonstrated in Figure 2.28.

$\includegraphics[]{img/tutorial/tut_10_graph.png}$

Figure 2.28: The floor plan of the location to be controlled.

To begin with, switch over to the proving perspective and double click on DLF/THM to begin proving. At the beginning of the proof, there aren’t any selected hypothesis, so we need to select a few. The old deadlock freeness invariant will be useful, and axm7 of doors_ctx2 as well.

AXIOMS

$\tt axm7 :$: $\it \exists l\mathord {\mkern 1mu\cdot \mkern 1mu}l\in L\setminus \{ outside\} \land outside\mapsto l\in com \land P\mathbin \times \{ l\} \subseteq aut$

We will try to avoid using exit since we want to keep things as simple as possible. Because sit and aut are inside the invariant, we also are likely to need

$sit \subseteq aut \land sit \in P \mathbin \rightarrow L.$

Once again, the prover automatically rewrites the existential quantifiers in the hypotheses. We now look at the proof. There is an easy case if $sit(p) = outside$ . Add this case as previously using the Case Distinction button (dc). To do this, you first need to instantiate the value for p. To do this, use the hypothesis $\exists p, l \cdot p \mapsto l \in aut \land sit(p) \neq l$ and then click on the existential quantifier to create the expression $p \in P$ (see Figure 2.24). Initialize the value of q with the value of p (type p into the yellow box next to q). For m, you will use the existential quantifier of axm7 of doors_ctx2 to instantiate m (add the axiom as a hypothesis and then click on the existential quantifier next to the l. Once the variable has been initialized, type it into the yellow box next to m).

For the other case, we will need the notion of exit. This function exit connects locations to locations and defines at every location except outside.

We can look at the axioms about exit:

AXIOMS

$\tt axm3 :$: $\it exit \in L\setminus \{ outside\} \mathbin \rightarrow L$
$\tt axm4 :$: $\it exit \subseteq com$
$\tt axm5 :$: $\it \forall s\mathord {\mkern 1mu\cdot \mkern 1mu}s\subseteq exit^{-1} [s] \mathbin \Rightarrow s=\emptyset$
$\tt axm6 :$: $\it aut \mathbin {\rhd \mkern -14mu-}\{ outside\} \subseteq (aut ; exit^{-1} )$

The axioms state that:

(axm3) Every room except the outside has exactly one exit.
(axm4) An exit must be a room that communicates with the current one
(axm5) A chain of exits leads to the outside without any cycles or infinite paths
(axm6) Everyone allowed in a room is allowed to go through its exit.

In our proof, we still need to show that anyone who is not outside can walk through a door. For this, axm5 is useless, so we add all hypotheses containing exit except for axm5. Now we have to instantiate q and m correctly and to conclude that the proof should not be too hard. Once again, for q, the choice p is obvious. But it is not quite as easy for m. Expressed in language, m must be the room behind the exit door of the room that p is currently in.

$\includegraphics[width=7mm]{img/info_64.png}$
Try translating this into set theory. But do not worry if you get it wrong. You can still go back in the proof by right-clicking at the desired point in the proof tree and choose Prune in order to retry.

This concludes the tutorial. Please note that this tutorial gave you only an introduction to proving.

Rodin Handbook

2.10.2 First Refinement