Rewriting rules for event model decomposition: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Son
imported>Ladenberger
 
(5 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 actions of an ''external'' event of a sub-machine from those of an initial event in the non-decomposed machine.
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 relation ==
== <font id="equiv_rules">Equivalence and simplification rules</font> ==
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.
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.
This relation is represented with the <math>\defi</math> symbol.


== Rewriting rules on Event-B assignments ==
=== Equivalence rules on Event-B assignments ===
As detailed in [[Actions_(Modelling_Language)|the modelling language]], the Event-B assignments are formed of two parts:  
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 left-hand side, which is a list of free identifiers.
* A right-hand side.
* A right-hand side.
Line 26: Line 29:
|}
|}


== Rewriting rules on Event-B actions ==
=== 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:
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}}
{{SimpleHeader}}
Line 35: Line 38:
|}
|}


<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.
 
''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>\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>
|<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 ===
Let <math>x_i</math>, <math>y</math> and <math>z</math> be variables, and <math>P</math> and <math>Q</math> be 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_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.
Line 50: Line 53:
* <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).
* <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 ==
=== Example ===
Let <math>a</math>, <math>b</math> and <math>x</math> be variables, and <math>P</math> and <math>Q</math> be predicates.
Let <math>a</math>, <math>b</math> and <math>x</math> be variables, and <math>P</math> and <math>Q</math> be predicates.
{|
{|
Line 64: Line 67:
|<math>\begin{array}{ll}a\!\!\! &\bcmsuch \exists x \qdot P(a,a',x)\\ b\!\!\! &\bcmsuch Q(b,b')\end{array}</math>
|<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>
|-
|<center><math>\defi</math> [[#rule_7|(Rule 7)]]</center>
|-
|<math>s \bcmsuch s' = E \land (\exists v' \qdot v' = F)</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>
|}
==== <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>
|}
=== <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>
|}
[[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}