Rewriting rules for event model decomposition: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Son
imported>Pascal
Line 35: Line 35:
|}
|}


<font color=blue>
''Note 1'': The <math>P</math> predicate can refer to other before variables than <math>v</math> (''e.g.'' <math>w</math> or <math>u</math>, where <math>u \notin \{v,w\}</math>). Similarly, <math>Q</math> can refer to other variables than <math>w</math>.
* 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.
{{SimpleHeader}}
|-
|<math>\begin{array}{ll}v\!\!\! &\bcmsuch P(v,w,x,v')\\ w\!\!\! &\bcmsuch Q(w,v,x,w') \end{array}</math>||<math>v,w \bcmsuch P(v,w,x,v') \land Q(w,v,x,w')</math>||<font id="rule_4">Rule 4</font>
|-
|}


* I (Son) thinks this Rule 5 is better to include the Rule 4 so that there is only one action, and it could be a general form of Rule 1.
''Note 2'': The following equivalence is obtained by enforcing the rules [[#rule_1|1]] and [[#rule_4|4]], and is a good replacement for the rule [[#rule_5|5]]:
{{SimpleHeader}}
{{SimpleHeader}}
|-
|-
|<math>v,w \bcmeq E,F</math>||<math>\begin{array}{ll}v,w \bcmsuch v'\!\!\! = E \land w'\!\!\! = F \end{array}</math>||<font id="rule_5">Rule 5</font>
|<math>v,w \bcmeq E,F</math>||<math>\begin{array}{ll}v,w \bcmsuch v'\!\!\! = E \land w'\!\!\! = F \end{array}</math>||Rule 5
|-
|-
|}
|}
</font>


== Simplification rules on Event-B predicates ==
== Simplification rules on Event-B predicates ==

Revision as of 12:22, 16 July 2009

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

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}