User Manual for Rodin v.2.3: Machines

3.2.3 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.3.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 variable. 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.3.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(\mathbf{c})$ can be used as hypotheses in the proofs.

3.2.3.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 hold at each state of the machine. Each invariant $i$ consists of a label and a predicate $I_ i(\mathbf{c},\mathbf{v},\mathbf{w})$ . An invariant can refer to the constants as well as the variables of the concrete and all abstract machines.

We write $I(\mathbf{c},\mathbf{v})$ to denote the conjunction of all invariants of the abstract machines and $J(\mathbf{c},\mathbf{v},\mathbf{w})$ for the conjunction of the 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 3.2.5.2.

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

3.2.3.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 (see below in section 3.2.3.4). Once a variable disappears in a refinement, i.e. is not declared in machine $M_{i+2}$ , it cannot be re-introduced in a later refinement.

3.2.3.4 Events

A possible state change of 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) leading 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.3.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 – e.g. event $E_1$ is refined by $E_2$ and $E_2$ 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 $E_1$ and $E_2$ .

3.2.3.4.1 Parameters

An event may 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 inferable by 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(\mathbf{c},{\mathbf{v},\mathbf{w}},\mathbf{w}’,\mathbf{u},t)$ for the abstract parameter must be specified (see below – 3.2.3.4.4).

3.2.3.4.2 Guards

Each guard consist of a label and a predicate $H(\mathbf{c},\mathbf{w},\mathbf{u})$ . Variables or parameters of abstract machines are not accessible in a guard.

We write $G(\mathbf{c},\mathbf{v},\mathbf{t})$ for the conjunction of all guards of all abstract events.

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

3.2.3.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. And $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}({\mathbf{t},\mathbf{u}},\mathbf{w},\mathbf{u},\mathbf{w}’)= 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(\mathbf{c},\mathbf{w},\mathbf{u})$ when $E(\mathbf{c},\mathbf{w},\mathbf{u})$ is assigned to $x$ deterministically.

3.2.3.4.4 Witnesses

Witnesses are composed of a label and a predicate that are is to establish 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(\mathbf{c},{\mathbf{v},\mathbf{w}},\mathbf{w}’,\mathbf{u},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'}(\mathbf{c},{\mathbf{v},\mathbf{w}},\mathbf{w}’,{\mathbf{t},\mathbf{u}},x’)$ .

We denote the conjunction of all witnesses of an event with $W(\mathbf{c},{\mathbf{v},\mathbf{w}},\mathbf{v}’,\mathbf{w}’,{\mathbf{t},\mathbf{u}})$ .

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

	Witness feasibility for a parameter $p$
Name	eventlabel/ $p$ /WFIS
Goal	$\begin{array}{r@{\ }l}& A(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land \mathcal{T}({\mathbf{t},\mathbf{u}},\mathbf{w},\mathbf{u},\mathbf{w}’)\\ \mathbin \Rightarrow & W(\mathbf{c},{\mathbf{v},\mathbf{w}},\mathbf{w}’,\mathbf{u},p) \end{array}$

	Witness feasibility for an abstract variable $x$
Name	eventlabel/ $x’$ /WFIS
Goal	$\begin{array}{r@{\ }l}& A(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land \mathcal{T}({\mathbf{t},\mathbf{u}},\mathbf{w},\mathbf{u},\mathbf{w}’)\\ \mathbin \Rightarrow & W(\mathbf{c},{\mathbf{v},\mathbf{w}},\mathbf{w}’,{\mathbf{t},\mathbf{u}},x’) \end{array}$

A witness may contain well-definedness conditions, see 3.2.4.4 for the corresponding proof obligation.

3.2.3.4.5 Initialization

The initialization of a machine is given by a special event called INITIALISATION. Unlike other events, the initialization must not contain guards and parameters. The actions must not make use of variable values before the initialization 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.3.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.4.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 defined in the reference section regarding non-deterministic assignments.

	Action feasibility
Name	eventlabel/actionlabel/FIS
Goal	$\begin{array}{r@{\ }l}& A(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land G(\mathbf{c},\mathbf{v},\mathbf{t})\land H(\mathbf{c},\mathbf{w},\mathbf{u})\\ \mathbin \Rightarrow & \mathcal{F}(a) \end{array}$

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

	Invariant preservation
Name	eventlabel/invlabel/INV
Goal	$\begin{array}{r@{\ }l}& A(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land G(\mathbf{c},\mathbf{v},\mathbf{t})\land H(\mathbf{c},\mathbf{w},\mathbf{u})\\ \mathbin \Rightarrow & I_ i(\mathbf{c},{\mathbf{v},\mathbf{w}}’) \end{array}$

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

There are special cases regarding initialisation:

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

	Invariant establishment
Name	INITIALISATION/invlabel/INV
Goal	$A(\mathbf{c})\mathbin \Rightarrow I_ i(\mathbf{c},{\mathbf{v},\mathbf{w}}’)$

3.2.3.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 see below in Section 3.2.3.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.3.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 strenghtening
Name	eventname/guardlabel/GRD
Goal	$\begin{array}{r@{\ }l}& A(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land H(\mathbf{c},\mathbf{w},\mathbf{u})\land \\ & W(\mathbf{c},{\mathbf{v},\mathbf{w}},\mathbf{v}’,\mathbf{w}’,{\mathbf{t},\mathbf{u}})\land \mathcal{T}({\mathbf{t},\mathbf{u}},\mathbf{w},\mathbf{u},\mathbf{w}’)\\ \mathbin \Rightarrow & G_ i(\mathbf{c},\mathbf{v},\mathbf{t}) \end{array}$

3.2.3.5.2 Action simulation

If an abstract event’s action $i$ (with before-after predicate $Q_ i(\mathbf{c},\mathbf{v},\mathbf{t},\mathbf{v}’)$ ) 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}({\mathbf{t},\mathbf{u}},\mathbf{w},\mathbf{u},\mathbf{w}’)$ , the relevant abstract behaviour by the before-after-predicate $Q_ i(\mathbf{c},\mathbf{v},\mathbf{t},\mathbf{v}’)$ . The relation between abstract and concrete event is specified by the witnesses.

	Action simulation
Name	eventname/actionlabel/SIM
Goal	$\begin{array}{r@{\ }l}& A(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land H(\mathbf{c},\mathbf{w},\mathbf{u})\land \\ & W(\mathbf{c},{\mathbf{v},\mathbf{w}},\mathbf{v}’,\mathbf{w}’,{\mathbf{t},\mathbf{u}})\land \mathcal{T}({\mathbf{t},\mathbf{u}},\mathbf{w},\mathbf{u},\mathbf{w}’)\\ \mathbin \Rightarrow & Q_ i(\mathbf{c},\mathbf{v},\mathbf{t},\mathbf{v}’) \end{array}$

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

3.2.3.5.3 Preserved variables

If $x$ is a variable of both the abstract and concrete machine and the concrete event assigns a value $x$ but the abstract event does not, it must be proven that the variable’s value does not change. Let $Q_ i(\mathbf{c},\mathbf{w},\mathbf{u},\mathbf{w}’)$ 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(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land H(\mathbf{c},\mathbf{w},\mathbf{u})\land Q_ i(\mathbf{c},\mathbf{w},\mathbf{u},\mathbf{w}’) \\ \mathbin \Rightarrow & x’=x \end{array}$

3.2.3.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$ being the abstract guards of the merged events and $\mathbf{t}_1,\ldots ,\mathbf{t}_ n$ their parameters.

	Guard strengthening (merge)
Name	eventlabel/MRG
Goal	$\begin{array}{l@{\ }l}& A(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land H(\mathbf{c},\mathbf{w},\mathbf{u})\land \\ & W(\mathbf{c},{\mathbf{v},\mathbf{w}},\mathbf{v}’,\mathbf{w}’,{\mathbf{t},\mathbf{u}})\land \mathcal{T}({\mathbf{t},\mathbf{u}},\mathbf{w},\mathbf{u},\mathbf{w}’)\\ \mathbin \Rightarrow & G_1(\mathbf{c},\mathbf{v},\mathbf{t}_1)\lor \ldots \lor G_ n(\mathbf{c},\mathbf{v},\mathbf{t}_ n) \end{array}$

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

3.2.3.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 ability to extend an event is just syntactic sugar – the same effect can be achieved by manually copying the parameters, guards and actions.

This is especially usefull when additional features are gradually introduced into a model by refinement, which is also called “superposition refinement”.

3.2.3.8 Termination

Event-B makes it possible to prove the termination of events in a model. 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(\mathbf{c},\mathbf{w})$ can be specified in a model. A variant is an expression that is either numeric ( $V(\mathbf{c},\mathbf{w})\in \mathord {\mathbb Z}$ ) or a finite set ( $V(\mathbf{c},\mathbf{w})\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 underly 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 assume a default constant variant such 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 its refinements is also guaranteed due to the guard strengthening.

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

3.2.3.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(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land G(\mathbf{c},\mathbf{v},\mathbf{t})\land H(\mathbf{c},\mathbf{w},\mathbf{u})\\ \mathbin \Rightarrow & V(\mathbf{c},\mathbf{w})\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(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land \\ & G(\mathbf{c},\mathbf{v},\mathbf{t})\land H(\mathbf{c},\mathbf{w},\mathbf{u})\land \mathcal{T}({\mathbf{t},\mathbf{u}},\mathbf{w},\mathbf{u},\mathbf{w}’)\\ \mathbin \Rightarrow & V(\mathbf{c},\mathbf{w}’)<V(\mathbf{c},\mathbf{w}) \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(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land \\ & G(\mathbf{c},\mathbf{v},\mathbf{t})\land H(\mathbf{c},\mathbf{w},\mathbf{u})\land \mathcal{T}({\mathbf{t},\mathbf{u}},\mathbf{w},\mathbf{u},\mathbf{w}’)\\ \mathbin \Rightarrow & V(\mathbf{c},\mathbf{w}’)\leq V(\mathbf{c},\mathbf{w}) \end{array}$

3.2.3.8.2 Set variant

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

	Decreasing of a variant (anticipated event)
Name	FIN
Goal	$A(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\mathbin \Rightarrow \mathrm{finite}(V(\mathbf{c},\mathbf{w}))$

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(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land \\ & G(\mathbf{c},\mathbf{v},\mathbf{t})\land H(\mathbf{c},\mathbf{w},\mathbf{u})\land \mathcal{T}({\mathbf{t},\mathbf{u}},\mathbf{w},\mathbf{u},\mathbf{w}’)\\ \mathbin \Rightarrow & V(\mathbf{c},\mathbf{w}’)\subset V(\mathbf{c},\mathbf{w}) \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(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land \\ & G(\mathbf{c},\mathbf{v},\mathbf{t})\land H(\mathbf{c},\mathbf{w},\mathbf{u})\land \mathcal{T}({\mathbf{t},\mathbf{u}},\mathbf{w},\mathbf{u},\mathbf{w}’)\\ \mathbin \Rightarrow & V(\mathbf{c},\mathbf{w}’)\subseteq V(\mathbf{c},\mathbf{w}) \end{array}$

Rodin Handbook