Difference between revisions of "Rewriting rules for event model decomposition"
imported>Pascal |
imported>Pascal |
||
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 rewriting / simplification rules applied in the event model decomposition when building the ''external'' events, and more especially their actions. | ||
+ | |||
+ | == Equivalence relation == | ||
+ | It is possible to define an equivalence relation on the Event-B actions, and by restrictions on the Event-B assignments (an action is a set of 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>\equiv</math> symbol. | ||
+ | |||
+ | |||
== Rewriting rules on Event-B assignments == | == Rewriting rules on Event-B assignments == | ||
Line 11: | Line 18: | ||
* 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>\equiv</math>) to the right-hand ones: |
{{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> | + | |<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> | + | |<math>v \bcmin E</math>||<math>v \bcmsuch v' \in E</math>||<font id="rule_3">Rule 3</font> |
|} | |} | ||
Line 24: | Line 31: | ||
== Rewriting rules on Event-B actions == | == Rewriting 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 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>\equiv</math>) to the right-hand ones: |
{{SimpleHeader}} | {{SimpleHeader}} | ||
|- | |- | ||
− | |<math>v~ \bcmsuch P(v,v')</math><br><math>w \bcmsuch Q(w,w')</math>||<math>v,w \bcmsuch P(v,v') \land Q(w,w')</math> | + | |<math>v~ \bcmsuch P(v,v')</math><br><math>w \bcmsuch Q(w,w')</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>v~ \bcmeq E</math><br><math>w \bcmeq F</math> | + | |<math>v,w \bcmeq E,F</math>||<math>v~ \bcmeq E</math><br><math>w \bcmeq F</math>||<font id="rule_5">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. | ||
− | * 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.P(x_1,...,x_n,z) \land Q(y_1,...,y_m))</math> predicate, where <math>z \notin \{y_1,...,y_n\}</math>, may be rewritten as <math>(\exists z.P(x_1,...,x_n,z)) \land Q(y_1,...,y_m)</math>. | + | * <font id="rule_7">Rule 7</font>: The <math>(\exists z.P(x_1,...,x_n,z) \land Q(y_1,...,y_m))</math> predicate, where <math>z \notin \{y_1,...,y_n\}</math>, may be rewritten as <math>(\exists z.P(x_1,...,x_n,z)) \land Q(y_1,...,y_m)</math>. |
== Simplification rules based on Event-B proof obligations == | == Simplification rules based on Event-B proof obligations == | ||
+ | |||
+ | == 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.P(a,a',x) \land Q(b,b')</math> | ||
+ | |- | ||
+ | |<center><math>\equiv</math> [[#rule_7|(Rule 7)]]</center> | ||
+ | |- | ||
+ | |<math>a,b \bcmsuch (\exists x.P(a,a',x)) \land Q(b,b')</math> | ||
+ | |- | ||
+ | |<center><math>\equiv</math> [[#rule_4|(Rule 4)]]</center> | ||
+ | |- | ||
+ | |<math>a \bcmsuch \exists x.P(a,a',x)</math><br><math>b \bcmsuch Q(b,b')</math> | ||
+ | |} |
Revision as of 12:51, 3 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 external events, and more especially their actions.
Contents
Equivalence relation
It is possible to define an equivalence relation on the Event-B actions, and by restrictions on the Event-B assignments (an action is a set of 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:
![]() |
![]() |
Rule 1 |
![]() |
![]() |
Rule 2 |
![]() |
![]() |
Rule 3 |
Thus, each Event-B assignment can be expressed in a "becomes such that" form, and more precisely as , where
is a before-after predicate.
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 |
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
.
Simplification rules based on Event-B proof obligations
Example
Let ,
and
be variables, and
and
be predicates.
![]() |
![]() |
![]() |
![]() |
![]() ![]() |