Rewriting rules for event model decomposition

The purpose of this page is to list and justify the transformation 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 and simplification rules

It is first necessary to introduce some equivalence and simplification rules on Event-B assignments and predicates. These rules will then help to understand the transformation rules to be applied to build the actions of the external events.

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.

Equivalence 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

Equivalence 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).

Example

Let $a$, $b$ and $x$ be variables, and $P$ and $Q$ be predicates.

$a,b \bcmsuch \exists x \qdot P(a,a',x) \land Q(b,b')$

$\defi$ (Rule 7)

$a,b \bcmsuch (\exists x \qdot P(a,a',x)) \land Q(b,b')$

$\defi$ (Rule 4)

$\begin{array}{ll}a\!\!\! &\bcmsuch \exists x \qdot P(a,a',x)\\ b\!\!\! &\bcmsuch Q(b,b')\end{array}$

Transformation rules

The transformation from a given Event-B action of a sub-machine $M_i$ to another action of a sub-machine $M_j$ is subsequently be represented with the $\rightsquigarrow$ symbol. $s$ and $t$ are assumed to be variables shared between $M_i$ and $M_j$, $v$ and $w$ other variables, $E$ and $F$ expressions, and $P$ and $Q$ before-after predicates.
Let's first establish a transformation rule for generic Event-B assignments. It is then possible to deduce transformation rules for other assignments of the Event-B language.

Generic transformation rule on Event-B assignments

The generic transformation rule on Event-B assignments is defined below:

$v,s \bcmeq P(s,s',v,v')$

$s \bcmsuch \exists v' \qdot P(s,s',v,v')$

Rule 9

Derived transformation rules on Event-B assignments

The transformation rules for other Event-B assignments are obtained by applying the generic rule and the equivalence / simplification rules previously introduced. More precisely:

1. The equivalence rules 1 to 5 shall be first applied as many times as possible, from left to right, to get the assignment into the generic form.
2. Then, generic transformation rule 9 shall be enforced.
3. Then, the simplification rules 6 to 8 shall be enforced.
4. Finally, the equivalence rules 1 to 3 shall be applied, from right to left. The proof obligations generated for deterministic actions are indeed more suitable than those generated for non-deterministic actions. In the same manner, for a given set $S$, proving that $\exists x \qdot x \in S$ (FIS proof obligation generated from $x \bcmsuch x' \in S$) is indeed not as "simple" as proving that $S \neq \emptyset$ (proof obligation generated from $x \bcmin S$).

Example

$s,v \bcmsuch E,F$

$\defi$ (Rule 5)

$s,v \bcmsuch s' = E \land v' = F$

$\rightsquigarrow$ (Rule 9)

$s \bcmsuch (\exists v' \qdot s' = E \land v' = F)$

$\defi$ (Rule 7)

$s \bcmsuch s' = E \land (\exists v' \qdot v' = F)$

$\defi$ (Rule 6)

$s \bcmsuch s' = E$

$\defi$ (Rule 1)

$s \bcmeq E$

Formalization

The derived transformation rules on Event-B assignments are listed below:

$s \bcmeq E$	$s \bcmeq E$	Rule 10
$v \bcmeq E$	(empty)	Rule 11
$s \bcmin E$	$s \bcmin E$	Rule 12
$v \bcmin E$	(empty)	Rule 13
$s(E) \bcmeq F$	$s(E) \bcmeq F$	Rule 14
$v(E) \bcmeq F$	(empty)	Rule 15
$s,v \bcmsuch E,F$	$s \bcmeq E$	Rule 16

Derived transformation rules on Event-B actions

The transformation can be done separately for each assignment of an Event-B action, as demonstrated below:

$\begin{array}{ll}s,v\!\!\! &\bcmsuch P(s,s',v,v')\\ t,w \!\!\! &\bcmsuch Q(t,t',w,w')\end{array}$

$\defi$ (Rule 4)

$s,v,t,w \bcmsuch P(s,s',v,v') \land Q(t,t',w,w')$

$\rightsquigarrow$ (Rule 9)

$s,t \bcmsuch \exists v',w' \qdot P(s,s',v,v') \land Q(t,t',w,w')$

$\defi$ (Rule 7)

$s,t \bcmsuch (\exists v' \qdot P(s,s',v,v')) \land (\exists w' \qdot Q(t,t',w,w'))$

$\defi$ (Rule 4)

$\begin{array}{ll}s\!\!\! &\bcmsuch \exists v' \qdot P(s,s',v,v')\\ t\!\!\! &\bcmsuch \exists w' \qdot Q(t,t',w,w')\end{array}$