Event Model Decomposition - Revision history

imported>Ladenberger: /* Generation of the proof obligations */

2011-10-27T09:48:36Z

Generation of the proof obligations

← Older revision		Revision as of 09:48, 27 October 2011
Line 65:		Line 65:

	=== <font id="po">Generation of the proof obligations</font> ===		=== <font id="po">Generation of the proof obligations</font> ===
	A model to be decomposed is assumed to be proved, ''i.e.'' all the [[http://handbook.event-b.org/current/html/generated_proof_obligations.html\|proof obligations]] (PO) have been handled successfully.		A model to be decomposed is assumed to be proved, ''i.e.'' all the [http://handbook.event-b.org/current/html/generated_proof_obligations.html proof obligations] (PO) have been handled successfully.

	Moreover, the following conditions on PO shall be fulfilled during the decomposition:		Moreover, the following conditions on PO shall be fulfilled during the decomposition:

imported>Ladenberger: /* Generation of the proof obligations */

2011-10-27T09:47:06Z

Generation of the proof obligations

← Older revision		Revision as of 09:47, 27 October 2011
Line 65:		Line 65:

	=== <font id="po">Generation of the proof obligations</font> ===		=== <font id="po">Generation of the proof obligations</font> ===
	A model to be decomposed is assumed to be proved, ''i.e.'' all the [[~~Proof_Obligation~~\|proof obligations]] (PO) have been handled successfully.		A model to be decomposed is assumed to be proved, ''i.e.'' all the [[http://handbook.event-b.org/current/html/generated_proof_obligations.html\|proof obligations]] (PO) have been handled successfully.

	Moreover, the following conditions on PO shall be fulfilled during the decomposition:		Moreover, the following conditions on PO shall be fulfilled during the decomposition:

imported>Ladenberger: /* Partitioning the events in the sub-machines of the decomposition */

2011-10-27T09:18:40Z

Partitioning the events in the sub-machines of the decomposition

← Older revision		Revision as of 09:18, 27 October 2011
Line 158:		Line 158:
	===== <font id="evt_partition">Partitioning the events in the sub-machines of the decomposition</font> =====		===== <font id="evt_partition">Partitioning the events in the sub-machines of the decomposition</font> =====
	The sub-machines <math>M_1,...,M_n</math> shall be built and the events of <math>M</math> shall be partitioned in these newly created machines, according to the end-user [[#config\|configuration]]. The initialization event of <math>M</math> shall be left out. All other events shall be distributed.		The sub-machines <math>M_1,...,M_n</math> shall be built and the events of <math>M</math> shall be partitioned in these newly created machines, according to the end-user [[#config\|configuration]]. The initialization event of <math>M</math> shall be left out. All other events shall be distributed.
	<br>At this step, the sub-machines shall only contain these ''internal'' events. In particular, the <math>SEES</math> and <math>REFINES</math> clauses of <math>M_1,...,M_n</math> shall be empty. In the same manner, the <math>REFINES</math> and <math>WITH</math> ([[~~Witnesses_(Modelling_Language)~~\|witnesses]]) clauses of the events shall be left out.		<br>At this step, the sub-machines shall only contain these ''internal'' events. In particular, the <math>SEES</math> and <math>REFINES</math> clauses of <math>M_1,...,M_n</math> shall be empty. In the same manner, the <math>REFINES</math> and <math>WITH</math> ([[Event-B Modelling Language\|witnesses]]) clauses of the events shall be left out.
	<br>If an event has the extended status (''i.e.'' it inherits the actions of the refined event), then it shall first be merged with the refined event before being copied in the sub-machine. Note that such a merge is performed by the pretty printer of the Rodin platform (compare the information displayed, on the one hand in the "Pretty Print" view, and on the other hand in the "Edit" view, for an extended event).		<br>If an event has the extended status (''i.e.'' it inherits the actions of the refined event), then it shall first be merged with the refined event before being copied in the sub-machine. Note that such a merge is performed by the pretty printer of the Rodin platform (compare the information displayed, on the one hand in the "Pretty Print" view, and on the other hand in the "Edit" view, for an extended event).

imported>Ladenberger: /* Propagating the event status */

2011-10-27T09:16:33Z

Propagating the event status

← Older revision		Revision as of 09:16, 27 October 2011
Line 167:		Line 167:
	* An event tagged as anticipated in the non-decomposed machine shall remain anticipated in the sub-machine.		* An event tagged as anticipated in the non-decomposed machine shall remain anticipated in the sub-machine.
	* An ''external'' event shall always be declared as ordinary.		* An ''external'' event shall always be declared as ordinary.
	See [[~~Events_(Modelling_Language)~~\|the modelling language]] for precisions on the convergence status.		See [[Event-B Modelling Language\|the modelling language]] for precisions on the convergence status.

	In the same manner, an event (''internal'' or ''external'') of a sub-machine shall always be declared as non-extended.		In the same manner, an event (''internal'' or ''external'') of a sub-machine shall always be declared as non-extended.

imported>Ladenberger: /* Terminology */

2011-10-27T09:15:42Z

Terminology

← Older revision		Revision as of 09:15, 27 October 2011
Line 16:		Line 16:

	* Event model decomposition: The decomposition of a model in sub-models, called shared variables (or A-style decomposition, after [[#ancre_1\|Abrial]]). The shared events (or B-style decomposition, after [[#ancre_2\|Butler]]) is not considered here.		* Event model decomposition: The decomposition of a model in sub-models, called shared variables (or A-style decomposition, after [[#ancre_1\|Abrial]]). The shared events (or B-style decomposition, after [[#ancre_2\|Butler]]) is not considered here.
	A model can contain contexts, machines, or both (see [[~~Machines_and_Contexts_(Modelling_Language)~~\|the modelling language]]). The notion of model decomposition covers on the one hand the machine decomposition, and on the other hand the context decomposition, both being interdependent.		A model can contain contexts, machines, or both (see [[Event-B Modelling Language\|the modelling language]]). The notion of model decomposition covers on the one hand the machine decomposition, and on the other hand the context decomposition, both being interdependent.
	* Sub-machine: A machine built from a non-decomposed machine during the event model decomposition.		* Sub-machine: A machine built from a non-decomposed machine during the event model decomposition.
	* Sub-context: A context built from a non-decomposed context during the event model decomposition.		* Sub-context: A context built from a non-decomposed context during the event model decomposition.

imported>Pascal: /* Constructing an external event */

2010-06-02T14:05:35Z

Constructing an external event

← Older revision		Revision as of 14:05, 2 June 2010
Line 244:		Line 244:
	<math>x_1,...,x_n,s_1,...,s_m \bcmsuch P(x1,...,x_n,s_1,...,s_m, x_1',...,x_n',s_1',...,s_m')</math>		<math>x_1,...,x_n,s_1,...,s_m \bcmsuch P(x1,...,x_n,s_1,...,s_m, x_1',...,x_n',s_1',...,s_m')</math>

	<li>The second step consists in adding guards to define the types of the parameters, if necessary~~. More precisely, a theorem shall be added for each parameter for which typing is required~~. The <tt>.bcm</tt> file associated to the non-decomposed machine shall be parsed in order to retrieve the typing information.		<li>The second step consists in adding guards to define the types of the parameters, if necessary. The <tt>.bcm</tt> file associated to the non-decomposed machine shall be parsed in order to retrieve the typing information.

	<li>The third and last step of the construction consists in introducing an existential quantifier to resolve the invalid assignment. <math>external\_e</math> is the newly built external event.</li>		<li>The third and last step of the construction consists in introducing an existential quantifier to resolve the invalid assignment. <math>external\_e</math> is the newly built external event.</li>

imported>Pascal: /* Generation of the proof obligations */

2010-03-17T14:15:32Z

Generation of the proof obligations

← Older revision		Revision as of 14:15, 17 March 2010
Line 65:		Line 65:

	=== <font id="po">Generation of the proof obligations</font> ===		=== <font id="po">Generation of the proof obligations</font> ===
	A model to be decomposed is assumed to be proved, ''i.e.'' all the [[Proof_Obligation\|proof obligations]] (PO) have been handled successfully~~. The decomposition of a model shall otherwise be forbidden~~.		A model to be decomposed is assumed to be proved, ''i.e.'' all the [[Proof_Obligation\|proof obligations]] (PO) have been handled successfully.

	Moreover, the following conditions on PO shall be fulfilled during the decomposition:		Moreover, the following conditions on PO shall be fulfilled during the decomposition:

imported>Mathieu: /* Bibliography */

2010-02-26T18:03:12Z

Bibliography

← Older revision		Revision as of 18:03, 26 February 2010
Line 488:		Line 488:

	[[Category:Design]]		[[Category:Design]]
			[[Category:Composition]]

imported>Pascal: /* Implementation */

2009-11-19T14:18:45Z

Implementation

← Older revision		Revision as of 14:18, 19 November 2009
Line 478:		Line 478:
	== Implementation ==		== Implementation ==
	A first plugin prototype is accessible under <tt>_exploratory/tshoang/ch.ethz.eventb.decomposition</tt>.		A first plugin prototype is accessible under <tt>_exploratory/tshoang/ch.ethz.eventb.decomposition</tt>.

	~~=== Known issues ===~~
	~~Bugs found in the prototype (SVN version 7604):~~

	* If a decomposed machine is refined the events in the refined machine which were marked as "external" do not inherit the "external" attribute
	* If type of the "INITIALIZATION" event of a decomposed machine is changed from "extended" to "not extended" in its refinement an error message is generated that some of the actions are missing although they are there correctly copied from the abstract "INITIALIZATION" event

	== Bibliography ==		== Bibliography ==

imported>Pascal: /* Ensuring that a shared variable is not refined by an initialization event */

2009-11-18T08:47:28Z

Ensuring that a shared variable is not refined by an initialization event

← Older revision		Revision as of 08:47, 18 November 2009
Line 301:		Line 301:
	If <math>M_{i}'</math> refines a sub-machine <math>M_i</math> issued from the decomposition of a machine <math>M</math>, the initialization event of <math>M_{i}'</math> shall not constrain a ''shared'' variable more or less than it was in the initialization event of <math>M_i</math>.		If <math>M_{i}'</math> refines a sub-machine <math>M_i</math> issued from the decomposition of a machine <math>M</math>, the initialization event of <math>M_{i}'</math> shall not constrain a ''shared'' variable more or less than it was in the initialization event of <math>M_i</math>.

	An initialization event shall not contain an action modifying at the same time a ''shared'' variable and a ''private'' variable (''eg.'' <math>a,b \bcmsuch P(a',b')</math>, where <math>a</math> is ''private'' and <math>b</math> is ''shared''). If such a behavior was authorized, a two-way simulation proof obligation would indeed be necessary to ensure that the ''shared'' variable is not constrained differently in further refinements. As a consequence, the decomposition of <math>M</math> shall be forbidden if ~~its~~ initialization event ~~contain~~ such an action. Moreover, the static checker shall ensure that the initialization event of <math>M_{i}'</math> does not contain such an action.		An initialization event shall not contain an action modifying at the same time a ''shared'' variable and a ''private'' variable (''eg.'' <math>a,b \bcmsuch P(a',b')</math>, where <math>a</math> is ''private'' and <math>b</math> is ''shared''). If such a behavior was authorized, a two-way simulation proof obligation would indeed be necessary to ensure that the ''shared'' variable is not constrained differently in further refinements. As a consequence, the decomposition of <math>M</math> shall be forbidden if the initialization event of <math>M_i</math> contains such an action. Moreover, the static checker shall ensure that the initialization event of <math>M_{i}'</math> does not contain such an action.

	Finally, the static checker shall ensure that the actions of the initialization event of <math>M_i</math> related to the shared variables are not modified in <math>M_{i}'</math>. More precisely, the actions shall be syntactically equal.		Finally, the static checker shall ensure that the actions of the initialization event of <math>M_i</math> related to the shared variables are not modified in <math>M_{i}'</math>. More precisely, the actions shall be syntactically equal.