Event-B建模实际操作：控制桥上的汽车（二）

紧接上节。现在我们要继续工作，做出初始模型的第一个精化。一个精化就是一个比初始模型更精确的模型。虽然它更精确，但也不应该与初始模型矛盾。这样，我们就必须证明这个精化与初始模型的一致性。

First Refinement: Introducing the One-Way Bridge

We are now going to proceed with a refinement of our initial model. A refinement is a more precise model than the initial one. It is more precise but it should not contradict the initial model. Therefore, we shall certainly have to prove that the refinement is consistent with the initial model.

In this first refinement, we introduce the bridge. This means that we are able to observe more accurately our system. Together with this more accurate observation, we can also see more events, namely cars entering and leaving the island. These events are called IL_in and IL_out. Note that events ML_out and ML_in, which were present in the initial model, still exist in this refinement: they now correspond to cars leaving the mainland and entering the bridge or leaving the bridge and entering the mainland. All this is illustrated in Fig. 24.

Fig. 24. Adding inv3 to prove the deadlock freedom

In Rodin, the easiest way to create a refinement is by right-clicking on the machine in the project browser and selecting Refine, as shown in Fig. 25. This will create a “stub” consisting of all variables and events. Here I create a machine with the name m1.

Fig. 25. Create a refinement

The state, which was defined by the constant d and variable n in the initial model, now becomes more accurate. The constant d remains, but the variable n is now replaced by three variables. This is because now we can see cars on the bridge and in the island, something which we could not distinguish in the previous abstraction. Moreover, we can see where cars on the bridge are going: either towards the island or towards the mainland. For these reasons, the state is now represented by means of three variables a, b, and c. Variable a denotes the number of cars on the bridge and going to the island, variable b denotes the number of cars in the island, and variable c denotes the number of cars on the bridge and going to the mainland.

Fig. 26. Add new variables

Variables a, b, and c are all natural numbers. This is stated in invariants inv1, inv2, and inv3 below. Then we express that the sum of these variables is equal to the previous abstract variable n which has disappeared. This is expressed in invariant inv4. This invariant relates the concrete state represented by the three variables a, b, and c, to the abstract state represented by the variable n. And finally, we state that the bridge is one-way: this is our basic requirement FUN-3. This is expressed by saying that a or c is equal to zero. Clearly, they cannot be both positive since the bridge is one-way, but they can be both equal to zero if the bridge is empty. This one-way property is expressed in invariant inv5.

Fig. 27. Add new invariants

After adding new variables and new invariants, we can see some error messages. Because we add new variables but didn’t initialize them, and variable n has not been identified. To fix this error, we need to click the text “extended ordinary”, which are highlighted in Fig. 28.

Fig. 28. Click “extended ordinary” first

Then we can initialize the variable a, b, c. The code after initialization should look like the code shown in Fig. 29.

Fig. 29. Refining the Initialization Event Init

The two abstract events ML_out and ML_in now have to be refined as they are not dealing with the

abstract variable n anymore but with the concrete variables a, b, and c. Here is the proposed concrete

versions (sometimes also called refined versions) of events ML_in and ML_out:

Fig. 30. A refined version of events ML_in and ML_out

It is easy to understand what these events are doing. For example, in event ML_in, the action decrements variable c as there will be one car less on the bridge, and this can be done if there are some cars on the bridge going to the mainland, that is when 0 < c holds (notice that we are sure that there are no cars on the bridge going to the island as a must be equal to 0 since c is positive).

And we can see that all proof obligations can be automatically discharged.

Fig. 31. Current proof obligations in m1

Fig. 31. Current proof obligations in m1

We now have to introduce some new events corresponding to cars entering and leaving the island. Next

are the proposed new events in Fig. 32.

Fig. 32. new events: IL_in and IL_out

It is also easy to understand what these events are doing. Event IL_in corresponds to a car leaving the bridge and entering the island. The action thus decrements the number of cars on the bridge and simultaneously increments the number b of cars on the island. But this can only be done when there are cars on the bridge, that is when the condition 0 < a hold.

Event IL_out corresponds to a car leaving the island and entering the bridge. The action clearly decreases b and simultaneously increases c. But this can be done only if there are cars on the island, that is if the condition 0 < b holds. A second condition for event IL_out to be enabled is that there are no cars on the bridge going to the island (remember, the bridge is one-way), that is if the condition a = 0 holds.

However, after we adding IL_in and IL_out, we got 2 warnings: No variant specified for convergent evert IL_in and IL_out, as shown in Fig. 33.

Fig. 33. No variant specified for convergent evert IL_in and IL_out

In the case where we introduce some new events, we have to prove something else, namely that they do not diverge. In other words, new events must not be indefinitely enabled. Should it be the case, then the concrete versions of the existing events, here ML_out and ML_in, could be postponed indefinitely, which is certainly something we want to avoid since such events could possibly occur in the abstraction. For proving this, we have to exhibit a natural number expression called a variant and prove that it is decreased by all new events. This leads to two proof obligation rules: one states that the proposed variant is a natural number and the other states that the variant is decreased by the new events.

In our case, the proposed variant is the following:

Finally, we have to prove that all concrete events (old and new together) do not deadlock more often than the abstract events. We have thus to prove that the disjunction of the abstract guards implies the disjunction of the concrete guards.

Once there are no error messages, expand the m1 machine in the Event-B Explorer. Then expand the Proof Obligations section. We can see that the auto prover did quite a good job. Only three proofs have not been completed (a completed proof is indicated by a green mark). we can observe the proof obligations all be discharged automatically except for thm1/THM, as shown in Fig. 34.

Fig. 34. Current Proof Obligations in m1

Make sure that you understand the different buttons in the Proof Control View (The Proof Control view contains the buttons with which you can perform an interactive proof. An overview of this proof can be seen in Fig. 35).

Fig. 35. The Proof Control View

Here I will introduce how to use the proof control view to solve proof obligation thm1/THM (Make sure that you understand how to prove thm1/THM manually). The goal is to prove c>0 ∨ a>0 ∨ (a+b<d ∧ c=0) ∨ (0<b ∧ a=0). We only know a∈ℕ, b∈ℕ, c∈ℕ,d>0,… We can decompose c∈ℕ into c>0 and c=0; a∈ℕ into a>0 and a=0; b∈ℕ into b>0 and b=0. Make sure you finished the following task: (1) Type c=0 into the Proof Control View and press the

button. The proof is split into two branches. One is c=0, another is c>0. (2) Type a=0 into the Proof Control View and press the

button. (3) Type b=0 into the Proof Control View and press the

button. Then press the ‘pp’ button for each goal, and press the ‘save’ button. We can see that each goal is indicated by a green mark

now, as shown in Fig. 36.

Fig. 36. The Proof Tree View of thm1/THM

So, we have finished machine m1. As a whole, the first refined model (context + machine) design by Rodin is shown as follows.

Context cd (final version):

CONTEXT

cd ›

CONSTANTS

⚬ d ›

AXIOMS

⚬ axm1: d∈ℕ not theorem ›

⚬ axm2: d>0 not theorem ›

END

Machine m1 (final version):

MACHINE

m1 ›

REFINES

⚬ m0

SEES

⚬ cd

VARIABLES

⚬ a ›number of cars on bridge going to island

⚬ b ›number of cars on island

⚬ c ›number of cars on bridge going to mainland

INVARIANTS

⚬ inv1: a ∈ ℕ not theorem ›

⚬ inv2: b ∈ ℕ not theorem ›

⚬ inv3: c ∈ ℕ not theorem ›

⚬ inv4: n=a+b+c not theorem ›

⚬ inv5: a=0 ∨ c=0 not theorem ›The bridge is one−way

⚬ thm1: c>0 ∨

a>0 ∨

(a+b<d ∧ c=0) ∨

(0<b ∧ a=0) theorem ›

VARIANT

⚬ 2∗a+b ›

EVENTS

⚬ INITIALISATION: not extended ordinary ›

THEN

⚬ act2: a≔0 ›

⚬ act3: b≔0 ›

⚬ act4: c≔0 ›

END

⚬ ML_out: not extended ordinary ›

REFINES

⚬ ML_out

WHERE

⚬ grd1: a+b<d not theorem ›

⚬ grd2: c=0 not theorem ›

THEN

⚬ act1: a≔a+1 ›

END

⚬ ML_in: not extended ordinary ›

REFINES

⚬ ML_in

WHERE

⚬ grd1: c>0 not theorem ›

THEN

⚬ act1: c≔c−1 ›

END

⚬ IL_in: not extended convergent ›entering island

WHERE

⚬ grd1: a>0 not theorem ›

THEN

⚬ act1: a≔a−1 ›

⚬ act2: b≔b+1 ›

END

⚬ IL_out: not extended convergent ›leaving island

WHERE

⚬ grd1: 0<b not theorem ›

⚬ grd2: a=0 not theorem ›

THEN

⚬ act1: b≔b−1 ›

⚬ act2: c≔c+1 ›

END

END