Rewriting rules for event model decomposition

The purpose of this page is to list and justify the rewriting / simplification rules applied in the event model decomposition, when building the actions of an external event of a sub-machine from those of an initial event in the non-decomposed machine.

Equivalence relation

It is possible to define an equivalence relation on the Event-B actions, and by restriction on the Event-B assignments. Two actions are considered as being equivalent if the proof obligations generated for these actions are logically equivalent.

This relation is represented with the $\defi$ symbol.

Rewriting rules on Event-B assignments

As detailed in the modelling language, the Event-B assignments are formed of two parts:

A left-hand side, which is a list of free identifiers.
A right-hand side.

There are various kinds of assignments:

The $\bcmsuch$ ("becomes such that") assignment is the most general (non-deterministic) assignment, where a predicate is given on the before and after values of assigned identifiers. The after values of the assigned identifiers are denoted by a primed identifier whose prefix is the assigned identifier.
The $\bcmeq$ ("becomes equal to") assignment is the deterministic assignment where an expression is given for each assigned identifier.
The $\bcmin$ ("becomes member of") assignment is the set-based (non-deterministic) assignment, where a set expression is given for the assigned identifier.

Let $v$ and $w$ be variables, and $E$ and $F$ be expressions. In the following table, the left-hand assignments are equivalent ( $\defi$ ) to the right-hand ones (see the B-book):

$v \bcmeq E$	$v \bcmsuch v' = E$	Rule 1
$v(E) \bcmeq F$	$v \bcmeq v \ovl \{E \mapsto F\}$	Rule 2
$v \bcmin E$	$v \bcmsuch v' \in E$	Rule 3

Rewriting rules on Event-B actions

Let $v$ and $w$ be variables, $E$ and $F$ be expressions, and $P$ and $Q$ be predicates. The left-hand actions are equivalent ( $\defi$ ) to the right-hand ones:

$\begin{array}{ll}v\!\!\! &\bcmsuch P(v,v')\\ w\!\!\! &\bcmsuch Q(w,w') \end{array}$	$v,w \bcmsuch P(v,v') \land Q(w,w')$	Rule 4
$v,w \bcmeq E,F$	$\begin{array}{ll}v\!\!\! &\bcmeq E\\ w\!\!\! &\bcmeq F \end{array}$	Rule 5

Note 1: The $P$ predicate can refer to other before variables than $v$ (e.g. $w$ or $u$ , where $u \notin \{v,w\}$ ). Similarly, $Q$ can refer to other variables than $w$ .

Note 2: The following equivalence is obtained by enforcing the rules 1 and 4, and is a good replacement for the rule 5:

v,w \bcmeq E,F

\begin{array}{ll}v,w \bcmsuch v'\!\!\! = E \land w'\!\!\! = F \end{array}

Rule 5

Simplification rules on Event-B predicates

Let $x_i$ , $y$ and $z$ be variables, and $P$ and $Q$ be predicates.

Rule 6: If $P(x_1,...,x_n,y)~$ is equal to $y = Q(x_1,...,x_n)~$ , then the $\exists y.P(x1,...,x_n,y)$ predicate is true, and it may be deleted in conjunctive predicates ( $\land$ ) where it appears.
Rule 7: The $(\exists z \qdot P(x_1,...,x_n,z) \land Q(y_1,...,y_m))$ predicate, where $z \notin \{x_1,...,x_n,y_1,...,y_m\}$ , may be rewritten as $(\exists z \qdot P(x_1,...,x_n,z)) \land Q(y_1,...,y_m)$ .
Rule 8: The $\exists z \qdot P(x_1,...,x_n,z)$ predicate may be deleted in conjunctive predicates where it appears if the $y \bcmsuch P(x_1,...,x_n,y')$ assignment is among the actions of the initial event. It indeed is nothing else but the feasibility (FIS) proof obligation for such an assignment, and a model to be decomposed is assumed to be proved (see the section related to the proof obligations in the event model decomposition).