Rodin User’s Handbook v.2.8: Machines

3.2.4 Machines

A machine describes the dynamic behavior of a model by means of variables whose values are changed by events.

There are two basic things that must be proven for a machine:

The machine must be consistent, i.e. it should never reach a state which violates the invariant.
The machine is a correct refinement, i.e. its behavior must correspond to any machines that it refines.

3.2.4.1 Refinement and Abstract machines

A machine can refine at most one other machine. We refer to the refined machine as the abstract machine and refer to the refinement as the concrete machine. More generally, a machine $M_0$ can be refined by machine $M_1$ , $M_1$ refined by $M_2$ and so on. The most concrete refinement would be $M_ n$ .

Basically, a refinement consists of two aspects:

The concrete machine’s state is connected to the state of the abstract machine. To do this, an invariant is used to relate abstract and concrete variables. This invariant is called a gluing invariant.
Each abstract event can be refined by one or more concrete events.

The full invariant of the machine consists of both abstract and concrete invariants. The invariants are accumulated during refinements.

$\includegraphics[width=7mm]{img/info_64.png}$
How to use Refinement: Refinement can be used to subsequently add complexity to the model - this is called superposition refinement (or horizontal refinement). It can also be used to add detail to data structures – this is called data refinement (or vertical refinement). We’ve seen both types of refinement in the tutorial (Chapter 2).

3.2.4.2 Seeing a context

If the machine sees a context, the sets and constants declared in the context can be used in all predicates and expressions. The conjunction of axioms $A$ can be used as hypotheses in the proofs.

3.2.4.3 Variables and invariants

Variables can be declared by adding their unique name (an identifier) to the Variables section. The type of the variables must be inferable by the invariants of the machine. We denote the variables of the abstract machines $M_1,\ldots ,M_{n-1}$ with a $\mathbf{v}$ and the variables of the concrete machine with a $\mathbf{w}$ .

An invariant is a statement that must be valid at each state of the machine. Each invariant $i$ consists of a label and a predicate $I_ i$ . An invariant can refer to the constants as well as the variables of the concrete and all abstract machines.

We write $I$ to denote the conjunction of all invariants of the abstract machines and $J$ for the conjunction of the concrete machine’s invariant.

Invariants that are marked as theorems derive their correctness from the preservation of other invariants, so their preservation does not need to be proven. The proof obligation can be found in Section 3.2.6.2.

If an invariant contains a well-definedness condition, a corresponding proof obligation is generated (3.2.5.2).

3.2.4.3.1 Common variables between machines

With some restrictions, the abstract variables $\mathbf{v}$ and concrete variables $\mathbf{w}$ can have variables in common. If a variable $v$ is declared in a machine $M_ i$ , it can be re-used in the direct refinement $M_{i+1}$ . In that case, it is assumed that the values of the abstract and concrete variable are always equal. To ensure this, special proof obligations are generated (3.2.4.4). Once a variable disappears in a refinement, i.e. it is not declared in machine $M_{i+2}$ , it cannot be re-introduced in a later refinement.

3.2.4.4 Events

A possible state change for a machine is defined by an event. The condition under which an event can be executed is given by a guard. The event’s action describes how the new and old state relate to each other.

Events occur atomically (i.e. one event happens at a time) and to a new state. Two events never happen at the same time. Time is also not factored into the execution of the event.

An event has the following elements:

Name
Parameters
Guards
Witnesses
Actions
Status (ordinary, convergent or anticipated): The status is used for termination proofs (see Section 3.2.4.8 for details).

An event can refine one or more events of an abstract machine. To keep things simple, we will first consider events with only one refined event. If there are several refinement steps, we describe events from the refined machines as abstract events and the event from the concrete machine as the concrete event. For example, if an event $E_1$ is refined by $E_2$ and $E_2$ is refined by $E3$ , we call $E_1$ and $E_2$ the abstract events and $E_3$ the concrete event. Likewise, if we refer to the parameters of the abstract events, we mean all the parameters of all the abstract events (e.g., the parameters of $E_1$ and $E_2$ ).

3.2.4.4.1 Parameters

An event can have an arbitrary number of parameters. Their names must be unique, i.e. there must be no constant or variable with the same name. The types of the parameters must be declared in the guards of the event. We denote the parameters of all abstract events with $\mathbf{t}$ and the parameters of the concrete event with $\mathbf{u}$ .

Similarly to variables, an event can have parameters in common with the event it refines. If the refined event has a parameter $t$ which is not a parameter of the refinement, a witness $W_ t$ for the abstract parameter must be specified (3.2.4.4.4). All free identifiers in $W_ t$ must be either constants, concrete or abstract variables, concrete parameters or the abstract parameter $t$ .

3.2.4.4.2 Guards

Each guard consist of a label and a predicate $H$ . All free identifiers in $H$ must be constants, concrete variables or concrete parameters. Variables or parameters of abstract machines are not accessible in a guard.

We write $G$ for the conjunction of all guards of all abstract events.

Like axioms and invariants, guards can also be marked as theorems. The proof obligation can be found in Section 3.2.6.3. If the guard contains WD-conditions, a proof obligation is generated. See Section 3.2.5.3 for the proof obligation.

3.2.4.4.3 Actions

An action is composed of a label and an assignment. Section 3.3.8 gives an overview of how they are assigned. They can be put into two groups: deterministic and non-deterministic assignments. Each assignment affects one or more concrete variables.

If an event has more than one action, they are executed in parallel. An error will occur if a new value is assigned to a variable in more than one action. All variables to which no new value is assigned keep the same value in new and old state.

We now define the before-after-predicate $\mathcal{T}$ of the actions together. Let $Q_1,\ldots ,Q_ n$ be the before-after-predicate of the event’s assignments. Let $x_1,\ldots ,$ $x_ k$ be the variables that are assigned by any action of the event. Let $y_1,\ldots ,y_ l$ be the variables of the concrete machine that are not modified by any of the event’s actions (i.e. $\mathbf{w}= x_1,\ldots ,x_ k,y_1,\ldots ,y_ l$ ). Then the before-after-predicate of the concrete event is $\mathcal{T}= Q_1 \land \ldots \land Q_ n \land y_1 = y_1’ \land \ldots \land y_ l=y_ l’$ .

Please note that Rodin optimizes proof obligations when a before-after-predicate is a hypothesis. $x’$ is replaced directly by $x$ when $x$ is not changed by the event and replaced by $E$ when $E$ is assigned to $x$ deterministically.

3.2.4.4.4 Witnesses

Witnesses are composed of a label and a predicate that establishes a link between the values of the variables and parameters of the concrete and abstract events. Most of the time, this predicate is a simple equality.

$\includegraphics[width=7mm]{img/warning_64.png}$
Unlike other elements in Event-B that have a label, the label of a witness has a meaning and cannot be chosen arbitrarily.

If the user does not specify a witness, Rodin uses the default witness $\mathord {\top }$ .

Witnesses are necessary in the following circumstances:

The abstract event has a parameter $p$ that is not a parameter of the concrete event. In this case, the label of the witness must be $p$ , and the witness has the form $W_ p$ . All identifiers of $W_ p$ must be either constants, concrete or abstract variables, primed concrete variables (i.e. $v’$ for each concrete variable $v$ ), concrete parameters or the abstract parameter $p$ .
The abstract event assigns non-deterministically (using $\mathrel {:\mkern 1mu\in }$ or $\mathrel {:\mkern 1mu\mid }$ ) a value to a variable $x$ that is not a variable of the concrete machine. In this case, the label of the witness must be $x’$ , the witness has the form $W_{x'}$ . All identifiers of $W_ p$ must be either constants, concrete or abstract variables, primed concrete variables (i.e. $v’$ for each concrete variable $v$ ), concrete parameters or the primed abstract variable $x’$ . $x’$ denotes the new value of $x$ .

We denote the conjunction of all witnesses of an event with $W$ .

The feasibility of the witness must be proven, i.e. that there is actually a value for which the predicate holds.

	Witness feasibility for a parameter $p$
Name	eventlabel/ $p$ /WFIS
Goal	$\begin{array}{r@{\ }l}& A \land I \land J \land H \\ \mathbin \Rightarrow & \exists p \mathord {\mkern 1mu\cdot \mkern 1mu}W_ p \end{array}$

	Witness feasibility for an abstract variable $x$
Name	eventlabel/ $x’$ /WFIS
Goal	$\begin{array}{r@{\ }l}& A \land I \land J \land H \land \mathcal{T}\\ \mathbin \Rightarrow & \exists x’ \mathord {\mkern 1mu\cdot \mkern 1mu}W_{x'} \end{array}$

A witness may contain well-definedness conditions. See 3.2.5.4 for the corresponding proof obligation.

3.2.4.4.5 Initialisation

The initialisation of a machine is given by a special event called INITIALISATION. Unlike other events, the initialisation must not contain guards and parameters. The actions must not make use of variable values before the initialisation event occurs. All variables must have a value assigned to them. If there is no assignment for the variable $x$ , Rodin assumes a default assignment of the form $x\mathrel {:\mkern 1mu\mid }\mathord {\top }$ .

3.2.4.4.6 Ensuring machine consistency

The following proof obligations are generated for events:

The assignment of each action must be well-defined when the event is enabled. See 3.2.5.5 for the corresponding proof obligation.

If the event’s guard is enabled, every action must be feasible. This is trivially true in the case of the deterministic assignments. For a non-deterministic assignment $a$ , the feasibility $\mathcal{F}(a)$ must be proven. The feasibility operator $\mathcal{F}$ is described in Section 3.3.8.

	Action feasibility
Name	eventlabel/actionlabel/FIS
Goal	$\begin{array}{r@{\ }l}& A \land I \land J \land H \land W_ p \land \mathcal{S}\\ \mathbin \Rightarrow & \mathcal{F}(a) \end{array}$

For each invariant $J_ i$ with the label invlabel that contains a variable affected by the assignment, it must be proven that the invariant still is still valid for the new values.

	Invariant preservation
Name	eventlabel/invlabel/INV
Goal	$\begin{array}{r@{\ }l}& A \land I \land J \land H \land W_{v} \land \mathcal{T}\\ \mathbin \Rightarrow & J_ i[\mathbf{v}’/\mathbf{v},\mathbf{w}’/\mathbf{w}] \end{array}$

Rodin simplifies this proof obligations by replacing $x’$ with $x$ for variables that are not changed and $x’$ by $E$ for variables that are assigned by a deterministic ( $x \mathrel {:\mkern 1mu=}E$ ) assignment.

There are special proof obligations generated for the initialisation event:

	Action feasibility (in the initialisation)
Name	INITIALISATION/actionlabel/FIS
Goal	$A \land W \land \mathcal{T}\mathbin \Rightarrow \mathcal{F}(a)$

	Invariant establishment
Name	INITIALISATION/invlabel/INV
Goal	$A \land W \land \mathcal{T}\mathbin \Rightarrow I_ i[\mathbf{v}’/\mathbf{v},\mathbf{w}’/\mathbf{w}]$

3.2.4.5 Ensuring a correct refinement

An event can refine one or more events of the abstract machine. We first consider the refinement of only one event. For refining more than one event (i.e. merging events), please refer below to Section 3.2.4.6.

If an event does not refine an abstract event, it is implicitly assumed that it refines skip, the event that is always enabled (i.e. its guard is $\mathord {\top }$ ) and does nothing (i.e. all variables keep their values).

3.2.4.5.1 Guard strengthening

A concrete event must only be enabled if the abstract event is enabled. This condition is called guard strengthening. For each abstract guard $G_ i$ with label guardlabel, the following proof obligation is generated:

	Guard strengthening
Name	eventname/guardlabel/GRD
Goal	$\begin{array}{r@{\ }l}& A \land I \land J \land H \land W_ p \\ \mathbin \Rightarrow & G_ i \end{array}$

3.2.4.5.2 Action simulation

If an abstract event’s action $i$ (with before-after predicate $Q_ i$ ) assigns a value to a variable that is also declared in the concrete machine, it must be proven that the abstract event’s behaviour corresponds to the concrete behaviour. The behaviour of the concrete event is given by the concrete before-after-predicate $\mathcal{T}$ , and the relevant abstract behaviour is given by the before-after-predicate $Q_ i$ . The relation between abstract and concrete event is specified by witnesses.

	Action simulation
Name	eventname/actionlabel/SIM
Goal	$\begin{array}{r@{\ }l}& A \land I \land J \land H \land W \land \mathcal{T}\\ \mathbin \Rightarrow & Q_ i \end{array}$

When the assignments are deterministic or the witnesses are equations, the proof obligation can usually be simplified by Rodin.

3.2.4.5.3 Preserved variables

If $x$ is a variable of both the abstract and concrete machine and the concrete event assigns a value to $x$ but the abstract event does not, it must be proven that the variable’s value does not change. Let $Q_ i$ be the before-after-predicate of the action that changes $x$ .

	Equality of a preserved variable $x$
Name	eventname/ $x$ /EQL
Goal	$\begin{array}{r@{\ }l}& A \land I \land J \land H \land Q_ i \\ \mathbin \Rightarrow & x’=x \end{array}$

3.2.4.6 Merging events

Refining more than one abstract event by a single event is called merging of events. To merge events, two conditions must be taken into account.

If two abstract events declare the same parameter, they must be of the same type.
All abstract events must have identical actions.

Instead of the guard strengthening proof obligation, the following proof obligation is created with $G_1,\ldots ,G_ n$ as the abstract guards of the merged events and $\mathbf{t}_1,\ldots ,\mathbf{t}_ n$ as their parameters.

	Guard strengthening (merge)
Name	eventlabel/MRG
Goal	$\begin{array}{l@{\ }l}& A \land I \land J \land H \land W \land \mathcal{T}\\ \mathbin \Rightarrow & G_1\lor \ldots \lor G_ n \end{array}$

The other proof obligations are the same as for refining a single event. Also, the same rules for defining witnesses apply.

3.2.4.7 Extending events

Instead of refining another event, an event can extend it. In this case the refined event will implicitly have all the parameters, guards and actions of the refined event. It can have additional parameters, guards and actions. The same effect can be achieved by manually copying the parameters, guards and actions.

This is especially useful when additional features are gradually introduced into a model by refinement (also called “superposition refinement”).

3.2.4.8 Termination

Event-B makes it possible to prove how an event will terminate. Termination means that a chosen set of events are enabled only a finite number of times before an event that is not marked as terminating occurs. To support proofs for termination, a variant $V$ can be specified in a model. All free identifiers in $V$ must be constants or concrete variables. A variant is an expression that is either numeric ( $V\in \mathord {\mathbb Z}$ ) or a finite set ( $V\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ , where $\alpha$ is an arbitrary type).

Events can be marked as:

ordinary: when the event may occur arbitrarily often and does not underlie any restrictions regarding the variant.
convergent: when the event must decrease the variant.
anticipated: when the event must not increase the variant.

Informally, termination is proven by stating that the convergent events strictly decrease the variant which has a lower bound. If a model contains a convergent event, a variant must be specified. If only anticipated events are declared, it is sufficient to create a default constant variant so that all anticipated events do not increase the variant. When an event is marked as anticipated, one must just prove that the event does not increase the variant. The proof of termination is then delayed to the refinements of the anticipated event. A refinement of an anticipated event must be either anticipated or convergent.

If the convergence of an event is proven, the convergence of its refinements is also guaranteed due to guard strengthening.

A variant must be well-defined. The corresponding well-definedness proof obligations can be found in Section 3.2.5.6. The following other proof obligations are generated:

3.2.4.8.1 Numeric variant

If the variant is numeric, an anticipated or convergent event must only be enabled when the variant is non-negative.

	Numeric variant is a natural number
Name	eventlabel/NAT
Goal	$\begin{array}{r@{\ }l}& A \land I \land J \land G \land H \\ \mathbin \Rightarrow & V\in \mathord {\mathbb N}\end{array}$

A convergent event must decrease the variant

	Decreasing of a numeric variant (convergent event)
Name	eventlabel/VAR
Goal	$\begin{array}{r@{\ }l}& A \land I \land J \land G \land H \land \mathcal{T}\\ \mathbin \Rightarrow & V[\mathbf{w}’/\mathbf{w}]<V \end{array}$

and an anticipated event must not increase the variant.

	Decreasing of a numeric variant (anticipated event)
Name	eventlabel/VAR
Goal	$\begin{array}{r@{\ }l}& A \land I \land J \land G \land H \land \mathcal{T}\\ \mathbin \Rightarrow & V[\mathbf{w}’/\mathbf{w}]\leq V \end{array}$

3.2.4.8.2 Set variant

If the variant is a set t, it must be proven that the set is always finite:

	Decreasing of a variant (anticipated event)
Name	FIN
Goal	$\begin{array}{r@{\ }l}& A \land I \land J \\ \mathbin \Rightarrow & \mathrm{finite}(V) \end{array}$

A convergent event must remove elements from the set

	Decreasing of a set variant (convergent event)
Name	eventlabel/VAR
Goal	$\begin{array}{r@{\ }l}& A \land I \land J \land G \land H \land \mathcal{T}\\ \mathbin \Rightarrow & V[\mathbf{w}’/\mathbf{w}]\subset V \end{array}$

and an anticipated event must not add elements.

	Decreasing of a set variant (anticipated event)
Name	eventlabel/VAR
Goal	$\begin{array}{r@{\ }l}& A \land I \land J \land G \land H \land \mathcal{T}\\ \mathbin \Rightarrow & V[\mathbf{w}’/\mathbf{w}]\subseteq V \end{array}$

Rodin Handbook