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.
Contents
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 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
("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
("becomes equal to") assignment is the deterministic assignment where an expression is given for each assigned identifier.
- The
("becomes member of") assignment is the set-based (non-deterministic) assignment, where a set expression is given for the assigned identifier.
Let and
be variables, and
and
be expressions. In the following table, the left-hand assignments are equivalent (
) to the right-hand ones (see the B-book):
![]() |
![]() |
Rule 1 |
![]() |
![]() |
Rule 2 |
![]() |
![]() |
Rule 3 |
Rewriting rules on Event-B actions
Let and
be variables,
and
be expressions, and
and
be predicates. The left-hand actions are equivalent (
) to the right-hand ones:
![]() |
![]() |
Rule 4 |
![]() |
![]() |
Rule 5 |
- Rule 4 could be more general since P can refer to other before variables than v, e.g. w or x /= v, w. Similarly for Q.
![]() |
![]() |
Rule 4 |
Simplification rules on Event-B predicates
Let ,
and
be variables, and
and
be predicates.
- Rule 6: If
is equal to
, then the
predicate is true, and it may be deleted in conjunctive predicates (
) where it appears.
- Rule 7: The
predicate, where
, may be rewritten as
.
- Rule 8: The
predicate may be deleted in conjunctive predicates where it appears if the
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 ,
and
be variables, and
and
be predicates.
![]() |
![]() |
![]() |
![]() |
![]() |