Rewriting rules for event model decomposition - Revision history

imported>Ladenberger: /* Equivalence rules on Event-B assignments */

2011-10-27T09:19:13Z

Equivalence rules on Event-B assignments

← Older revision		Revision as of 09:19, 27 October 2011
Line 10:		Line 10:

	=== Equivalence 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.

imported>Mathieu: /* Derived transformation rules on Event-B actions */ Category:Design

2009-08-12T12:05:14Z

Derived transformation rules on Event-B actions: Category:Design

← Older revision		Revision as of 12:05, 12 August 2009
Line 154:		Line 154:
	\|<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>		\|<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]]

imported>Pascal: /* Transformation rules */

2009-07-22T15:09:11Z

Transformation rules

← Older revision		Revision as of 15:09, 22 July 2009
Line 69:		Line 69:

	== Transformation rules ==		== Transformation rules ==
	The transformation from a given Event-B action to another is subsequently be represented with the <math>\rightsquigarrow</math> symbol. <math>v</math> and <math>w</math> are assumed to be ~~private~~ variables, <math>s</math> and <math>t</math> ~~shared~~ variables, <math>E</math> and <math>F</math> expressions, and <math>P</math> and <math>Q</math> before-after predicates.		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.		<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.

imported>Pascal: /* Rewriting rules for event model decomposition */

2009-07-17T09:17:39Z

Rewriting rules for event model decomposition

Show changes

imported>Pascal: /* Rewriting rules on Event-B actions */

2009-07-16T12:22:28Z

Rewriting rules on Event-B actions

← Older revision		Revision as of 12:22, 16 July 2009
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 ==

imported>Son: /* Rewriting rules on Event-B actions */

2009-07-14T09:37:11Z

Rewriting rules on Event-B actions

← Older revision		Revision as of 09:37, 14 July 2009
Line 42:		Line 42:
	\|-		\|-
	\|}		\|}

			* 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.
			{{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>
			\|-
			\|}

	</font>		</font>

imported>Son: /* Rewriting rules on Event-B actions */

2009-07-14T09:27:48Z

Rewriting rules on Event-B actions

← Older revision		Revision as of 09:27, 14 July 2009
Line 34:		Line 34:
	\|<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>		\|<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>
	\|}		\|}

			<font color=blue>
			* 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>
			\|-
			\|}
			</font>

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

imported>Pascal: /* Rewriting rules on Event-B assignments */

2009-07-07T12:44:37Z

Rewriting rules on Event-B assignments

← Older revision		Revision as of 12:44, 7 July 2009
Line 25:		Line 25:
	\|<math>v \bcmin E</math>\|\|<math>v \bcmsuch v' \in E</math>\|\|<font id="rule_3">Rule 3</font>		\|<math>v \bcmin E</math>\|\|<math>v \bcmsuch v' \in E</math>\|\|<font id="rule_3">Rule 3</font>
	\|}		\|}

	Thus, each Event-B assignment can be expressed in a "becomes such that" form, and more precisely as <math>v_1,...,v_n \bcmsuch P(v_1,...v_n,v_1',...v_n')</math>, where <math>P</math> is a before-after predicate.

	== Rewriting rules on Event-B actions ==		== Rewriting rules on Event-B actions ==

imported>Pascal: /* Rewriting rules on Event-B assignments */

2009-07-06T16:29:23Z

Rewriting rules on Event-B assignments

← Older revision		Revision as of 16:29, 6 July 2009
Line 8:		Line 8:
	== Rewriting rules on Event-B assignments ==		== Rewriting 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 [[Actions_(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.

	There are various kinds of assignments:		There are various kinds of assignments:

imported>Pascal: /* Simplification rules on Event-B predicates */

2009-07-03T16:33:36Z

Simplification rules on Event-B predicates

← Older revision		Revision as of 16:33, 3 July 2009
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 actions of an ''external'' event of a sub-machine from those of an initial event in the non-decomposed machine.

	== Equivalence relation ==		== 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.		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.
Line 40:		Line 40:
	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.
	* <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>.		* <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).
	~~== Simplification rules based on Event-B proof obligations ==~~
	<font ~~color~~="~~red~~">~~TO BE COMPLETED~~</font>

	== Example ==		== Example ==