User Manual for Rodin v.2.3: Initial Model

2.10.1 Initial Model

Let us look at the initial model which consists of doors_ctx1 and 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 reflects where 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.

2.10.1.1 Deadlock Freeness

Looking through the initial model, you will see that everything already has been proved. This is true, but Rodin does not do any deadlock freeness proof yet, so we will have to add them by ourself. A model is considered as deadlocked if the system reaches a state with 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:

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. Clearly, we want to avoid this happening. 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 the not theorem button 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 is must be proven that the theorem always holds if the other invariants declared before hold. We do not need to prove that an event preserves the invariant marked as theorem because this is a logical consequence when it preserves the other invariants.

INVARIANTS

$\tt DLF :$: $\it \exists p, l\mathord {\mkern 1mu\cdot \mkern 1mu}(p \mapsto l \in aut \land sit(p) \neq l)$

$\includegraphics{img/prob.png}$ You can also use ProB to search for deadlocks. 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 2.9). There are two ways to search for deadlocks:

Just press on the Check button and mark Find Deadlocks before starting the check 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 right to the Check button. ProB then prompts you for an optional predicate. Just leave that empty for the start. The difference to the first alternative is that ProB searches now for variable values where all invariants are true but none of the guards.

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

Save the machine. We will see in the Event-B Explorer View that the auto-prover (3.1.6) 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 on the theorem button. Another reason that you don’t see the proof obligation DLF/THM could be that you forgot 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 turn off the post-tactics because we want to see the proof develop in its different stages. Then select the root node in the Prove Tree, right-click on it and select Purge. This removes any proof that might be already started by the auto-provers. By doing this we want to assure that we 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:

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 words: every person is allowed to go both to the outside and to a location $l$ ). The basic idea of our proof is that a person is either outside and can to the location $l$ . When it is not outside, it can walk outside.

What we implicitly assumed was that there is actually a person, so we need to prove now is that $P$ is non-empty. This holds since carrier sets are always non-empty, but is a bit hard to prove. Now add the hypothesis $\exists x . x \in P$ using the $\includegraphics[height=2ex]{img/icons/rodin/ah_prover.png}$ button after entering the predicate into the Proof Control text area. In the Proof Tree view you can now see three new nodes that have to be proven:

$\mathord {\top }$ is the trivial well-definedness condition, just click on $\includegraphics[height=2ex]{img/icons/rodin/auto_prover.png}$ to prove it.
$\exists x\mathord {\mkern 1mu\cdot \mkern 1mu}x\in P$ is the hypothesis that we introduced, just click on $\includegraphics[height=2ex]{img/icons/rodin/auto_prover.png}$ to prove 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 use the introduced hypothesis in the proof. We 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. You see that it is automatically instantiated. That means that we can use $x$ from now on in our proof as an example for a person and we have the new hypothesis $x \in P$ .

An existential quantification can be proven by giving an example for the variables. First, we instantiate $p$ in the goal with $x$ : 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)$ which results from the old goal by replacing $p$ by $x$ . You can see the the current proof tree in Figure 2.25. In the node ah we added the hypothesis, in $\exists$ hyp we instantiated $x$ from a hypothesis and in $\exists$ goal 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 do 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$ in its domain. This is easy to prove since $sit$ is a total function (3.3.5). Just press $\includegraphics[height=2ex]{img/icons/rodin/auto_prover.png}$ .
Then 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.

Let’s continue with the case $sit(x)=outside$ : When $x$ is outside, it can always go to the $l$ of 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}$ . Now click on the $\exists$ symbol in the 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 still is $\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 has not (yet) anything to do with our 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 use our $l$ as an example for the $l$ in the existential quantification. Again, we have first the trivial goal $\mathord {\top }$ as well-definedness condition, just press $\includegraphics[height=2ex]{img/icons/rodin/auto_prover.png}$ . The remaining goal should be $\exists l\mathord {\mkern 1mu\cdot \mkern 1mu}x\mapsto l\in aut \land sit(x)\neq l$ . This can be proven by the already selected hypothesis $sit(x)=outside$ , $l\in L\setminus \{ outside\}$ and $P\mathbin \times \{ l\} \subseteq aut$ . Just press $\includegraphics[height=2ex]{img/icons/rodin/auto_prover.png}$ .

Now our second case of the case distinction remains where $x$ is not outside ( $sit(x)\neq outside$ ). Then $x$ can just 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 $\includegraphics[height=2ex]{img/icons/rodin/auto_prover.png}$ 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 the information 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. There should be still the result from the last search for $outside$ . (If not, repeat the search by entering $outside$ into the Proof Control and press $\includegraphics[height=2ex]{img/icons/rodin/sh_prover.png}$ ). Select $P \mathbin \times \{ outside\} \subseteq aut$ (in Figure 2.26, it’s the second entry) and press $\includegraphics[height=2ex]{img/icons/rodin/add.png}$ to add it to your selected hypothesis. Then the auto-prover has enough information, just click $\includegraphics[height=2ex]{img/icons/rodin/auto_prover.png}$ and the last goal of our theorem should be proven.