Difference between revisions of "Rewriting rules for event model decomposition"
imported>Pascal |
imported>Ladenberger |
||
(14 intermediate revisions by 3 users not shown) | |||
Line 1: | Line 1: | ||
− | The purpose of this page is to list and justify the | + | 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. |
− | == | + | == <font id="equiv_rules">Equivalence and simplification rules</font> == |
− | As detailed in [[ | + | 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 <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 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>v( | + | |<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 \ | + | |<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}} | {{SimpleHeader}} | ||
|- | |- | ||
− | |<math> | + | |<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 == | + | === 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. | ||
− | * 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. |
− | * The <math>(\exists z | + | * <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> | ||
+ | |- | ||
+ | |<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 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
("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 |
Equivalence 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 |
Note 1: The predicate can refer to other before variables than
(e.g.
or
, where
). Similarly,
can refer to other variables than
.
Note 2: The following equivalence is obtained by enforcing the rules 1 and 4, and is a good replacement for the rule 5:
![]() |
![]() |
Rule 5 |
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.
![]() |
![]() |
![]() |
![]() |
![]() |
Transformation rules
The transformation from a given Event-B action of a sub-machine to another action of a sub-machine
is subsequently be represented with the
symbol.
and
are assumed to be variables shared between
and
,
and
other variables,
and
expressions, and
and
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:
![]() |
![]() |
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:
- 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.
- Then, generic transformation rule 9 shall be enforced.
- Then, the simplification rules 6 to 8 shall be enforced.
- 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
, proving that
(FIS proof obligation generated from
) is indeed not as "simple" as proving that
(proof obligation generated from
).
Example
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
Formalization
The derived transformation rules on Event-B assignments are listed below:
![]() |
![]() |
Rule 10 |
![]() |
(empty) | Rule 11 |
![]() |
![]() |
Rule 12 |
![]() |
(empty) | Rule 13 |
![]() |
![]() |
Rule 14 |
![]() |
(empty) | Rule 15 |
![]() |
![]() |
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:
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |