Difference between revisions of "Rewriting rules for event model decomposition"

From Event-B
Jump to navigationJump to search
imported>Pascal
imported>Ladenberger
 
(23 intermediate revisions by 3 users not shown)
Line 1: Line 1:
The purpose of this page is to list and justify the rewriting / simplification rules applied in the event model decomposition when building the ''external'' events, and more especially their actions.
+
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.
  
== Rewriting rules for the Event-B assignments ==
+
== <font id="equiv_rules">Equivalence and simplification rules</font> ==
As detailed in [[Actions_(Modelling_Language)|the modelling language]], the Event-B assignments are formed of two parts:  
+
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.
* a left-hand side, which is a list of free identifiers.
+
 
* a right-hand side.
+
=== 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 <math>\defi</math> symbol.
 +
 
 +
=== Equivalence rules on Event-B assignments ===
 +
As detailed in [[Event-B Modelling Language|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:
 
There are various kinds of assignments:
Line 11: Line 19:
 
* The <math>\bcmin</math> ("becomes member of") assignment is the set-based (non-deterministic) assignment, where a set expression is given for the assigned identifier.
 
* The <math>\bcmin</math> ("becomes member of") assignment is the set-based (non-deterministic) assignment, where a set expression is given for the assigned identifier.
  
Let <math>v</math> and <math>w</math> be variables, and <math>E</math> and <math>F</math> be expressions. In the following table, the left-hand assignments are equivalent (\defi) to the right-hand ones:
+
Let <math>v</math> and <math>w</math> be variables, and <math>E</math> and <math>F</math> be expressions. In the following table, the left-hand assignments are equivalent (<math>\defi</math>) to the right-hand ones (see [[Event_Model_Decomposition#ancre_3|the B-book]]):
 
{{SimpleHeader}}
 
{{SimpleHeader}}
 
|-
 
|-
|<math>v \bcmeq E</math>||<math>v \bcmsuch v' = E</math>
+
|<math>v \bcmeq E</math>||<math>v \bcmsuch v' = E</math>||<font id="rule_1">Rule 1</font>
 +
|-
 +
|<math>v(E) \bcmeq F</math>||<math>v \bcmeq v \ovl \{E \mapsto F\}</math>||<font id="rule_2">Rule 2</font>
 +
|-
 +
|<math>v \bcmin E</math>||<math>v \bcmsuch v' \in E</math>||<font id="rule_3">Rule 3</font>
 +
|}
 +
 
 +
=== Equivalence rules on Event-B actions ===
 +
Let <math>v</math> and <math>w</math> be variables, <math>E</math> and <math>F</math> be expressions, and  <math>P</math> and <math>Q</math> be predicates. The left-hand actions are equivalent (<math>\defi</math>) to the right-hand ones:
 +
{{SimpleHeader}}
 +
|-
 +
|<math>\begin{array}{ll}v\!\!\! &\bcmsuch P(v,v')\\ w\!\!\! &\bcmsuch Q(w,w') \end{array}</math>||<math>v,w \bcmsuch P(v,v') \land Q(w,w')</math>||<font id="rule_4">Rule 4</font>
 +
|-
 +
|<math>v,w \bcmeq E,F</math>||<math>\begin{array}{ll}v\!\!\! &\bcmeq E\\ w\!\!\! &\bcmeq F \end{array}</math>||<font id="rule_5">Rule 5</font>
 +
|}
 +
 
 +
''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>.
 +
 
 +
''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}}
 +
|-
 +
|<math>v,w \bcmeq E,F</math>||<math>\begin{array}{ll}v,w \bcmsuch v'\!\!\! = E \land w'\!\!\! = F \end{array}</math>||Rule 5
 +
|-
 +
|}
 +
 
 +
=== Simplification rules on Event-B predicates ===
 +
Let <math>x_i</math>, <math>y</math> and <math>z</math> be variables, and <math>P</math> and <math>Q</math> be predicates.
 +
* <font id="rule_6">Rule 6</font>: If <math>P(x_1,...,x_n,y)~</math> is equal to <math>y = Q(x_1,...,x_n)~</math>, then the <math>\exists y.P(x1,...,x_n,y)</math> predicate is true, and it may be deleted in conjunctive predicates (<math>\land</math>) where it appears.
 +
* <font id="rule_7">Rule 7</font>: The <math>(\exists z \qdot P(x_1,...,x_n,z) \land Q(y_1,...,y_m))</math> predicate, where <math>z \notin \{x_1,...,x_n,y_1,...,y_m\}</math>, may be rewritten as <math>(\exists z \qdot P(x_1,...,x_n,z)) \land Q(y_1,...,y_m)</math>.
 +
* <font id="rule_8">Rule 8</font>: The <math>\exists z \qdot P(x_1,...,x_n,z)</math> predicate may be deleted in conjunctive predicates where it appears if the <math>y \bcmsuch P(x_1,...,x_n,y')</math> 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 [[Event_Model_Decomposition#po|proof obligations]] in the event model decomposition).
 +
 
 +
=== Example ===
 +
Let <math>a</math>, <math>b</math> and <math>x</math> be variables, and <math>P</math> and <math>Q</math> be predicates.
 +
{|
 +
|-
 +
|<math>a,b \bcmsuch \exists x \qdot P(a,a',x) \land Q(b,b')</math>
 +
|-
 +
|<center><math>\defi</math> [[#rule_7|(Rule 7)]]</center>
 +
|-
 +
|<math>a,b \bcmsuch (\exists x \qdot P(a,a',x)) \land Q(b,b')</math>
 +
|-
 +
|<center><math>\defi</math> [[#rule_4|(Rule 4)]]</center>
 +
|-
 +
|<math>\begin{array}{ll}a\!\!\! &\bcmsuch \exists x \qdot P(a,a',x)\\ b\!\!\! &\bcmsuch Q(b,b')\end{array}</math>
 +
|}
 +
 
 +
== Transformation rules ==
 +
The transformation from a given Event-B action of a sub-machine <math>M_i</math> to another action of a sub-machine <math>M_j</math> is subsequently be represented with the <math>\rightsquigarrow</math> symbol. <math>s</math> and <math>t</math> are assumed to be variables shared between <math>M_i</math> and <math>M_j</math>, <math>v</math> and <math>w</math> other variables, <math>E</math> and <math>F</math> expressions, and <math>P</math> and <math>Q</math> before-after predicates.
 +
<br>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:
 +
{{SimpleHeader}}
 +
|-
 +
|<math>v,s \bcmeq P(s,s',v,v')</math>||<math>s \bcmsuch \exists v' \qdot P(s,s',v,v')</math>||<font id="rule_9">Rule 9</font>
 +
|}
 +
 
 +
=== Derived transformation rules on Event-B assignments ===
 +
The transformation rules for other Event-B assignments are obtained by applying the [[#rule_9|generic rule]] and the [[#equiv_rules|equivalence / simplification rules]] previously introduced.
 +
More precisely:
 +
# The equivalence rules [[#rule_1|1]] to [[#rule_5|5]] shall be first applied as many times as possible, from left to right, to get the assignment into the generic form.
 +
# Then, generic transformation rule [[#rule_9|9]] shall be enforced.
 +
# Then, the simplification rules [[#rule_6|6]] to [[#rule_8|8]] shall be enforced.
 +
# Finally, the equivalence rules [[#rule_1|1]] to [[#rule_3|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 <math>S</math>, proving that <math>\exists x \qdot x \in S</math> (FIS proof obligation generated from <math>x \bcmsuch x' \in S</math>) is indeed not as "simple" as proving that <math>S \neq \emptyset</math> (proof obligation generated from <math>x \bcmin S</math>).
 +
 
 +
==== Example ====
 +
{|
 +
|-
 +
|<math>s,v \bcmsuch E,F</math>
 +
|-
 +
|<center><math>\defi</math> [[#rule_5|(Rule 5)]]</center>
 +
|-
 +
|<math>s,v \bcmsuch s' = E \land v' = F</math>
 +
|-
 +
|<center><math>\rightsquigarrow</math> [[#rule_9|(Rule 9)]]</center>
 +
|-
 +
|<math>s \bcmsuch (\exists v' \qdot s' = E \land v' = F)</math>
 
|-
 
|-
|<math>v,w \bcmeq E,F</math>||<math>v \bcmeq E \pprod w \bcmeq F</math>
+
|<center><math>\defi</math> [[#rule_7|(Rule 7)]]</center>
 
|-
 
|-
|<math>v(E) \bcmeq F</math>||<math>v \bcmeq v \ovl \{E \mapsto F\}</math>
+
|<math>s \bcmsuch s' = E \land (\exists v' \qdot v' = F)</math>
 
|-
 
|-
|<math>v \bcmin E</math>||<math>v \bcmsuch v' \in E</math>
+
|<center><math>\defi</math> [[#rule_6|(Rule 6)]]</center>
 +
|-
 +
|<math>s \bcmsuch s' = E</math>
 +
|-
 +
|<center><math>\defi</math> [[#rule_1|(Rule 1)]]</center>
 +
|-
 +
|<math>s \bcmeq E</math>
 
|}
 
|}
  
Thus, each Event-B assignment can be expressed in a "becomes such that" form.
+
==== <font id="transf_rules">Formalization</font> ====
 +
The derived transformation rules on Event-B assignments are listed below:
 +
{{SimpleHeader}}
 +
|-
 +
|<math>s \bcmeq E</math>||<math>s \bcmeq E</math>||<font id="rule_10">Rule 10</font>
 +
|-
 +
|<math>v \bcmeq E</math>||(empty)||<font id="rule_11">Rule 11</font>
 +
|-
 +
|<math>s \bcmin E</math>||<math>s \bcmin E</math>||<font id="rule_12">Rule 12</font>
 +
|-
 +
|<math>v \bcmin E</math>||(empty)||<font id="rule_13">Rule 13</font>
 +
|-
 +
|<math>s(E) \bcmeq F</math>||<math>s(E) \bcmeq F</math>||<font id="rule_14">Rule 14</font>
 +
|-
 +
|<math>v(E) \bcmeq F</math>||(empty)||<font id="rule_15">Rule 15</font>
 +
|-
 +
|<math>s,v \bcmsuch E,F</math>||<math>s \bcmeq E</math>||<font id="rule_16">Rule 16</font>
 +
|}
  
== Simplification rules on Event-B predicates ==
+
=== <font id="separately">Derived transformation rules on Event-B actions</font> ===
 +
The transformation can be done separately for each assignment of an Event-B action, as demonstrated below:
 +
{|
 +
|-
 +
|<math>\begin{array}{ll}s,v\!\!\! &\bcmsuch P(s,s',v,v')\\ t,w \!\!\! &\bcmsuch Q(t,t',w,w')\end{array}</math>
 +
|-
 +
|<center><math>\defi</math> [[#rule_4|(Rule 4)]]</center>
 +
|-
 +
|<math>s,v,t,w \bcmsuch P(s,s',v,v') \land Q(t,t',w,w')</math>
 +
|-
 +
|<center><math>\rightsquigarrow</math> [[#rule_9|(Rule 9)]]</center>
 +
|-
 +
|<math>s,t \bcmsuch \exists v',w' \qdot P(s,s',v,v') \land Q(t,t',w,w')</math>
 +
|-
 +
|<center><math>\defi</math> [[#rule_7|(Rule 7)]]</center>
 +
|-
 +
|<math>s,t \bcmsuch (\exists v' \qdot P(s,s',v,v')) \land (\exists w' \qdot Q(t,t',w,w'))</math>
 +
|-
 +
|<center><math>\defi</math> [[#rule_4|(Rule 4)]]</center>
 +
|-
 +
|<math>\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}</math>
 +
|}
  
== Rewriting rules for the Event-B actions ==
 
  
== Simplification rules based on Event-B proof obligations ==
+
[[Category:Design]]

Latest revision as of 09:19, 27 October 2011

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}