Rodin User’s Handbook v.2.8: Deadlock Freeness of initial model

2.10.1 Deadlock Freeness of initial model

Let us look at the initial model which consists of the context doors_ctx1 and the machine doors_0. There are two carrier sets in the model context. One is for people ( $P$ ) and the other is for locations ( $L$ ). There is a location called outside ( $outside$ ) and a relation ( $aut$ ) which defines the places that people are allowed to go. Everyone is permitted to go outside. The model machine has one event, pass, which changes the location of a person and one variable, $sit$ , which denotes where a person is located.

Looking through the initial model, you will see that everything already has been proved (for the initial model and initial contexts). This is true, but Rodin has not yet proved that the model is deadlock free yet, so we will have to prove this ourselves. A model is considered to be deadlocked if the system reaches a state where there are no outgoing transitions. The objective of this section is to develop proofs for deadlock freeness for the initial model and for the first refinement.

Consider the event pass from the initial model:

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

EVENTS

Event

pass $\mathrel {\widehat=}$

any

$\it p$

$\it l$

where

$\tt grd11 :$

$\it p \mapsto l \in aut$

$\tt grd12 :$

$\it sit(p) \neq l$

then

$\tt act11 :$

$\it sit(p) := l$

end

END

Since the initial model has only one event (pass), the system might deadlock when both guards of the event (grd11 and grd12) are false. In this case, to prove that no deadlocks can occur requires proving that someone can always change room. We must therefore prove that the two guards are always true. To do this, add a new derived invariant (a theorem) to doors_0 called DLF (click once on the label not theorem to make it switch to theorem) and change the predicate so that it is the conjunction of the two guards. The difference between a “normal” invariant and one that is marked as theorem is that you must prove that a theorem is always valid when the previously listed invariants are valid. Then we don’t need to prove that an event preserves the invariant marked as theorem because we can conclude this logically when it already preserves the other invariants.

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

INVARIANTS

$\tt DLF :$

$\it \fbox{theorem} ~ \exists p, l\mathord {\mkern 1mu\cdot \mkern 1mu}(p \mapsto l \in aut \land sit(p) \neq l)$

$\includegraphics[width=7mm]{img/warning_64.png}$
Make sure that when you add your DLF invariant, you add it after the other two invariants in doors_0. The auto prover uses these invariants to prove that the DLF invariant is well defined, and if they aren’t in the right order, the proof obligation DLF/WD will not be discharged

$\includegraphics{img/prob.png}$ You can also use ProB to search for deadlocks (after ensuring that ProB is installed). Right-click on the machine you want to check and start the animation with the “Start Animation / Model Checking” menu entry. After starting the animation, go to the Event View in the ProB perspective (see Figure 2.9). There are two ways to search for deadlocks:

Press the Check button and mark Find Deadlocks. Then start the model checking by pressing the button Start consistency checking. ProB then systematically “executes” all events and tries to find a state where no event is enabled.
An alternative is to select Deadlock Freedom Checking after clicking on the triangle to the right of the Check button. ProB will then prompt you to input a predicate, but this is optional, so leave it blank. The difference with this alternative alternative is that ProB searches now for variable values where all the invariants are valid but none of the guards are valid.

This contribution requires the ProB plugin. The content is maintained by the plugin contributors and may be out of date.

Save the machine. We see in the Event-B Explorer View that the auto-prover (3.1.7.5) fails to prove the theorem DLF/THM.

$\includegraphics[width=7mm]{img/warning_64.png}$
If you cannot find the proof obligation DLF/THM, maybe you forgot to mark the invariant as a theorem by clicking once on the not theorem label next to the invariant. Another reason that you might not see the proof obligation DLF/THM is that you have forgotten to rename the invariant “DLF”.

Let us analyze whether this is an inconsistency in the model. Switch to the Proving Perspective and double click on the proof obligation DLF/THM. In the Proof Control view, first disable the post-tactics (there is a small downward pointing arrow in the upper right hand corner above the toolbar (see Figure 2.22). Click on this arrow and make sure that the option Enable post-tactic is unchecked in the dropdown menu.) We are turning off the post-tactics because we want to see the proof develop in its different stages. Now select the root node in the Prove Tree, right-click on it and select Prune. This removes any proof that might be already started by the auto-provers. By doing this we want to assure that you have the same proof as in this tutorial.

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

Figure 2.22: Disabling the proof post-tactics in the Proof Controlling View

In order to succeed with the proof, we need a pair $p \mapsto l$ that is in $aut$ but not in $sit$ . Having a look the axioms, we find axm4 of doors_ctx1, which states that there is a location $l$ different from $outside$ where everyone is allowed to go:

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

AXIOMS

$\tt axm4 :$

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

So for every person $p$ in $P$ , $p \mapsto l$ and $p \mapsto outside$ are in $aut$ . (In other words: every person is allowed to go to both the outside and a location $l$ ). The basic idea of our proof is that a person is either already outside or at the location $l$ . If someone is outside, they are allowed to move to $l$ , and if they are not outside, they are allowed to move outside. ¹.

We assume that there is actually a person, so we need a set $P$ that is non-empty. This is automatically the case since carrier sets are always non-empty, but we need a person as an example for our further proof. Now add the hypothesis $\exists x \mathord {\mkern 1mu\cdot \mkern 1mu}x \in P$ by entering this predicate into the Proof Control text area and hitting the $\includegraphics[height=2ex]{img/icons/rodin/ah_prover.png}$ button. In the Proof Tree view you can now see three new nodes have appeared that need to be proven:

$\mathord {\top }$ is the trivial well-definedness condition. Click on $\includegraphics[height=2ex]{img/icons/rodin/auto_prover.png}$ button to verify it.
$\exists x\mathord {\mkern 1mu\cdot \mkern 1mu}x\in P$ is the hypothesis that we introduced. Click on the $\includegraphics[height=2ex]{img/icons/rodin/auto_prover.png}$ button to verify it.
$\exists p, l\mathord {\mkern 1mu\cdot \mkern 1mu}(p \mapsto l \in aut \land sit(p) \neq l)$ is the original goal but we can now use the introduced hypothesis in the proof. We will now continue with the proof of this goal.

Click on the existential quantifier of the new hypothesis $\exists x \cdot x \in P$ (appearing in the Selected Hypothesis view) as demonstrated in Figure 2.23. The hypothesis disappears and is replaced by a new hypothesis $x \in P$ . This is because the value of $x$ is automatically instantiated. This means that we can use $x$ from now on in our proof as an example for a person

$\includegraphics[width=7mm]{img/warning_64.png}$
If you hover over any red symbol for a short while, a menu will pop up, offering one or more transformations. Make sure that you actually click on the symbol before the menu pops up because otherwise clicking will no longer have any effect. If the menu has popped up before you managed to click on the symbol, you will have to click twice: the first click will discard the menu and the next click will actually perform the operation.

We can prove an existential quantification by giving an example for the variables. First, we instantiate $p$ in the goal with the variable $x$ that we created: enter $x$ in the yellow box corresponding to $p$ in the Goal View and click on the existential quantifier as shown in Figure 2.24.

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

Figure 2.23: Click on the existential quantifier in order to ...

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

Figure 2.24: ... instantiate it, in this case by substituting $x$ .

The instantiation produces two new nodes in the Proof Tree view. The first goal is the trivial well-definedness condition $\mathord {\top }$ and can be easily discharged by pressing $\includegraphics[height=2ex]{img/icons/rodin/auto_prover.png}$ . The remaining goal is $\exists l\mathord {\mkern 1mu\cdot \mkern 1mu}(x \mapsto l \in aut \land sit(x) \neq l)$ is the result of replacing $p$ by $x$ in the old goal. You can see the the current proof tree in Figure 2.25. The node with the label ah refers to when we added the hypothesis, the node with the label $\exists$ hyp refers to when we instantiated $x$ from a hypothesis and the node with the label $\exists$ goal refers to when we instantiated $p$ in the goal.

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

Figure 2.25: The proof tree after instantiating $p$ with $x$ .

Now we need an example for the remaining variable $l$ . There are two situations we want to distinguish: The person $x$ could be outside or not. To distinguish this, type $sit(x) = outside$ into the Proof Control view and click on the button $\includegraphics[height=2ex]{img/icons/rodin/dc_prover.png}$ (dc for distinguish case). Again, you get three new goals.

The first is the well-definedness condition of $sit(x) = outside$ . $sit$ must be a function and $x$ is in its domain. This is easy to prove since $sit$ is a total function (3.3.5). Press the $\includegraphics[height=2ex]{img/icons/rodin/p1.png}$ button to verify it.
The second node has the original goal but $sit(x) = outside$ as a hypothesis.
The third node has the original goal but $\lnot sit(x) = outside$ as a hypothesis.

$\includegraphics[width=7mm]{img/warning_64.png}$
Note that the second and third node will appear identical in the proof tree. You will only see the differences in the hypotheses by selecting the nodes.

Let’s continue with the case $sit(x)=outside$ : When $x$ is outside, it can always go to the $l$ that is defined axm4. To search for axm4, type $outside$ into the Proof Control text field and click the button $\includegraphics[height=2ex]{img/icons/rodin/sh_prover.png}$ . Add axm4 ( $\exists l\mathord {\mkern 1mu\cdot \mkern 1mu}l\in L\setminus \{ outside\} \land P\mathbin \times \{ l\} \subseteq aut$ ) to the selected hypotheses. Now click on the red $\exists$ symbol in axm4 (see Figure 2.26) to instantiate $l$ . Now we have $l$ as an example for a location which is not outside and where everybody can go.

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

Figure 2.26: Searching hypothesis for $outside$ : The third one is axm4.

Our goal is still $\exists l\mathord {\mkern 1mu\cdot \mkern 1mu}x\mapsto l\in aut \land sit(x)\neq l$ . Note that the existential quantification introduces a new $l$ which does not (yet) have anything to do with the location $l$ where anybody can go. Now type $l$ into the yellow box of the goal and press the $\exists$ symbol to state that we want to use our $l$ as an example for the $l$ in the existential quantification. Again, we have the trivial goal $\mathord {\top }$ as well-definedness condition, so just press $\includegraphics[height=2ex]{img/icons/rodin/auto_prover.png}$ button to verify it. The remaining goal should be $x\mapsto l\in aut \land sit(x)\neq l$ . This can be proven with the selected hypotheses $sit(x)=outside$ , $l\in L\setminus \{ outside\}$ and $P\mathbin \times \{ l\} \subseteq aut$ . Press the $\includegraphics[height=2ex]{img/icons/rodin/auto_prover.png}$ button to verify this goal.

Now only second case of the case distinction remains. This is where $x$ is not outside ( $sit(x)\neq outside$ ). In this case, $x$ can simply go outside. Again the goal is $\exists l\mathord {\mkern 1mu\cdot \mkern 1mu}x\mapsto l\in aut \land sit(x)\neq l$ . Type $outside$ as an example for a location $l$ into the yellow box and press the $\exists$ symbol. Press the $\includegraphics[height=2ex]{img/icons/rodin/auto_prover.png}$ button to discharge the trivial well-definedness condition $\mathord {\top }$ . The new goal should be $x \mapsto outside\in aut \land sit(x)\neq outside$ .

To prove this we need to prove that $x$ has the right to go $outside$ . This is stated in the axiom $P \mathbin \times \{ outside\} \subseteq aut$ . Have a look at the Search Hypothesis view. This was also one of the results from the last search for $outside$ . (If you no longer see the results, repeat the search by entering $outside$ into the Proof Control and press the $\includegraphics[height=2ex]{img/icons/rodin/sh_prover.png}$ button.) Select $P \mathbin \times \{ outside\} \subseteq aut$ (in Figure 2.26, it’s the second entry) and press the $\includegraphics[height=2ex]{img/icons/rodin/add.png}$ button to add it to your selected hypothesis. The auto-prover now has enough hypotheses, so simply click the $\includegraphics[height=2ex]{img/icons/rodin/auto_prover.png}$ button and the last goal of our theorem should be proven.

Here is the summary of the proof. Compare this with your final proof tree (as shown in Figure 2.27).

added hypotheses: $\exists x\mathord {\mkern 1mu\cdot \mkern 1mu}x\in P$

well-definedness condition $\mathord {\top }$ : automatically proven

the hypotheses: automatically proven

instantiation of $x$ in the hypotheses $\exists x\mathord {\mkern 1mu\cdot \mkern 1mu}x\in P$

using $x$ as an example for the $\exists p \ldots$ in the goal

well-definedness condition $\mathord {\top }$ : automatically proven

case distinction $sit(x)=outside$

well-definedness condition ( $sit$ is a function with $x$ in its

domain): proven using the p1 provers

first case: instantiation of $l$ from axiom axm4

using $l$ as an example for the $\exists l \ldots$ in the goal

well-definedness condition $\mathord {\top }$ : automatically proven

remaining goal: automatically proven

second case: using $outside$ as an example

for the $\exists l \ldots$ in the goal

well-definedness condition $\mathord {\top }$ : automatically proven

hypotheses $P\mathbin \times \{ outside\}$ selected

remaining goal: automatically proven

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

Figure 2.27: Searching hypothesis for $outside$ : The third one is axm4.

Footnotes

One could argue that this is too restrictive in the real world: After all, why do all people need authorisation for the same location l? But arguing about the realism of the example is out of the scope.

Rodin Handbook

2.10.1 Deadlock Freeness of initial model