Difference between revisions of "Event Model Decomposition"

From Event-B
Jump to navigationJump to search
imported>Pascal
imported>Pascal
(151 intermediate revisions by 2 users not shown)
Line 2: Line 2:
  
 
== Introduction ==
 
== Introduction ==
One of the most important feature of the Event-B approach is the ability to introduce new events during refinement steps, but a consequence is an increasing complexity of the refinement process when having to deal with many events and many state variables.
+
One of the most important feature of the Event-B approach is the possibility to introduce new events during refinement steps, but a consequence is an increasing complexity of the refinement process when having to deal with many events and many state variables.
  
The main idea of the decomposition is to cut a model <math>A</math> into sub-models <math>A_1, ..., A_n</math>, which can be refined separately and more comfortably than the whole.  
+
The main idea of the decomposition is to cut a model <math>M</math> into sub-models <math>M_1, ..., M_n</math>, which can be refined separately and more comfortably than the whole.  
  
The constraint that shall be satisfied by the decomposition is that these refined models might - the recomposition will never be performed in practice - be recomposed into a whole model <math>C</math> in a way that guarantees that <math>C</math> refines <math>A</math>. An event-based decomposition of a model is detailed in [[#ancre_1|Event Model Decomposition]]: the events of a model are partitioned to form the events of the sub-models. In parallel, the variables on which these events act are distributed among the sub-models.  
+
The constraint that shall be satisfied by the decomposition is that these refined models might be recomposed into a whole model <math>MR</math> in a way that guarantees that <math>MR</math> refines <math>M</math>. Note that this recomposition will never be performed in practice.
 +
 
 +
An event-based decomposition of a model is detailed in the [[#ancre_1|Event Model Decomposition]] article: the events of a model are partitioned to form the events of the sub-models. In parallel, the variables on which these events act are distributed among the sub-models.  
  
 
The purpose is here to precisely describe what is required at the Rodin platform level to integrate this event model decomposition, and to explain why. The details of how it could be implemented are out of scope.
 
The purpose is here to precisely describe what is required at the Rodin platform level to integrate this event model decomposition, and to explain why. The details of how it could be implemented are out of scope.
  
 
== Terminology ==
 
== Terminology ==
* Event model decomposition: The decomposition of a model, as defined in [[Machines_and_Contexts_(Modelling_Language)|the modelling language]], in sub-models. Other [[#ancre_2|decomposition structures for Event-B]] are not considered here.
+
This section introduces the definitions of the main technical terms, which are widely used in the sequel.
A model can contain contexts, machines, or both. The notion of model decomposition covers on the one hand the machine decomposition, and on the other hand the context decomposition, both being interdependent.
+
 
 +
* Event model decomposition: The decomposition of a model in sub-models, called A-style decomposition (after [[#ancre_1|Abrial]]). The 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.
 
* 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.  
* ''Shared'' variable: A variable of a given machine which is accessed by events distributed in distinct sub-machines (by opposition to ''private'' variable).  
+
* ''Shared'' variable: A variable accessed by events of distinct sub-machines (by opposition to ''private'' variable). A variable is said to be shared between a sub-machine <math>M_i</math> and a sub-machine <math>M_j</math> if and only if it is accessed by events of <math>M_i</math> and by events of <math>M_j</math>.  
* ''Private'' variable: A variable of a given machine which is only accessed by events of the same sub-machine (by opposition to ''shared'' variable).
+
* ''Private'' variable: A variable accessed by events of a single sub-machine (by opposition to ''shared'' variable).
 
* ''External'' event: An event of a sub-machine which is built from an event of the non-decomposed machine, and which simulates the way the ''shared'' variables (between this sub-machine and another sub-machine) are handled in the non-decomposed machine (by opposition to ''internal'' event).  
 
* ''External'' event: An event of a sub-machine which is built from an event of the non-decomposed machine, and which simulates the way the ''shared'' variables (between this sub-machine and another sub-machine) are handled in the non-decomposed machine (by opposition to ''internal'' event).  
 
* ''Internal'' event: An event copied from the non-decomposed machine to a sub-machine, according to the end-user specified distribution (by opposition to ''external'' event).
 
* ''Internal'' event: An event copied from the non-decomposed machine to a sub-machine, according to the end-user specified distribution (by opposition to ''external'' event).
Line 22: Line 26:
 
Note that a variable is said to be ''accessed'' when it is read or written. More precisely, such an access may be performed by a predicate (invariant, guard, witness) or in an assignment (action).
 
Note that a variable is said to be ''accessed'' when it is read or written. More precisely, such an access may be performed by a predicate (invariant, guard, witness) or in an assignment (action).
  
[[Image:Models.png]]
+
== High-level Specification ==
 +
The high-level specification details how the event model decomposition shall be integrated into the Rodin platform as a new feature, by linking to the existing architecture.
 +
 
 +
=== Definition of the decomposition ===
 +
It is necessary to first give a definition of the event model decomposition in the Rodin platform. Is it an Event-B project decomposition? Or, is it a decomposition performed from some well-identified machines and contexts of a given Event-B project?
 +
 
 +
As illustrated in the diagram below, when considering a given Event-B project, the entry point for the decomposition is a machine <math>M</math> of the project, and its whole hierarchy of seen contexts. The machine <math>M</math> to be taken as input for the decomposition shall be pointed by the end-user.
 +
 
 +
<center>
 +
[[Image:Decomposition.png]]
 +
</center>
 +
 
 +
=== <font id="config">Configuration of the decomposition</font> ===
 +
The end-user shall be asked to parametrize the decomposition, and more precisely to:
 +
* identify the machine to be taken as input for the decomposition.
 +
* identify the sub-machines to be created.
 +
* partition the events.
 +
 
 +
It is more suitable for the end-user to visualize the configuration, and as a consequence it shall preferably be performed through the Graphical User Interface of the Rodin platform.
 +
 
 +
The following dialog box, which fills these requirements, is given as an example. The left-hand side displays the non-decomposed model and the right-hand side the decomposed model. The second one is built by the user, by first adding machines and then copying events from left to right.
 +
 
 +
<center>
 +
[[Image:GUI.png]]
 +
</center>
 +
 
 +
The end-user shall have a way to backup its configuration. More precisely, it shall be possible on the one hand to export a configuration to a file, and on the other hand to import a configuration from a file.
 +
 
 +
=== Execution of the decomposition ===
 +
A <tt>Decompose</tt> action shall be added. It shall be enabled if and only if a machine is selected. It shall be available from the <tt>Project</tt> menu, from the toolbar, and in the contextual menu displayed when right-clicking on the selected project.
 +
 
 +
[[Image:Action.png]]
 +
 
 +
A new Event-B project shall be created for each sub-machine built during the configuration. The [[#machine_decomposition|decomposition of the sub-machine]] shall first be completed, and then the non-decomposed [[#context_decomposition|context shall be partitioned]].
 +
<br>The created projects and components (machines and contexts) shall be tagged as "automatically generated". It shall be possible to identify the non-decomposed machine from which they are issued.
 +
 
 +
As far as possible, the developments shall not be performed in the Event-B core; the dedicated extension points shall be used instead (''eg.'' those provided for the static checker. See the <tt>plugin.xml</tt> file of the <tt>org.eventb.core</tt> package).
 +
 
 +
=== <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.
 +
 
 +
Moreover, the following conditions on PO shall be fulfilled during the decomposition:
 +
* The decomposition shall not generate any new proof obligation.
 +
* The proof obligations related to the non-decomposed model shall not be "propagated" to the decomposed models to be proved again. As a consequence, the Proof Obligation Generator (POG) shall be temporary disconnected until the decomposition is performed.
  
 
== Low-level Specification ==
 
== Low-level Specification ==
 
The low-level specification details through several steps how the event model decomposition shall be performed, and in which order. It establishes a distinction between the steps performed on the end-user's initiative, and the computed ones. It links when possible to the already implemented features of the Rodin platform which can be used at some steps.
 
The low-level specification details through several steps how the event model decomposition shall be performed, and in which order. It establishes a distinction between the steps performed on the end-user's initiative, and the computed ones. It links when possible to the already implemented features of the Rodin platform which can be used at some steps.
 +
 +
The following sequence shall be observed to decompose a machine <math>M</math> in sub-machines <math>M_1,...,M_n</math>:
 +
# The events of <math>M</math> shall be partitioned in <math>M_1,...,M_n</math>, as indicated by the end-user (see [[#evt_partition|Event partition]]).
 +
# The Rodin platform shall update the status of the events (see [[#evt_status|Event status]]).
 +
# The Rodin platform shall distribute the variables of <math>M</math> in <math>M_1,...,M_n</math>, according to the event partition (see [[#var_distribution|Variable distribution]]).
 +
# The Rodin platform shall distribute the invariants of <math>M</math> in <math>M_1,...,M_n</math>, according to the variable distribution (see [[#inv_distribution|Invariant distribution]]).
 +
# The Rodin platform shall build ''external'' events in <math>M_1,...,M_n</math>, from the events of <math>M</math>, and according to the variable distribution (see [[#build_external|External event construction]]).
 +
# The Rodin platform shall build the initialization events of <math>M_1,...,M_n</math>, according to the variable distribution (see [[#build_init|Initialization event construction]]).
 +
# The Rodin platform shall build the contexts seen by <math>M_1,...,M_n</math>, from the hierarchy of contexts associated to <math>M</math> (see [[#context_decomposition|Context decomposition]]).
 +
 +
This order will be justified by itself subsequently, when going into the details of the decomposition.
  
 
=== <font id="machine_decomposition">Decomposition of a machine in sub-machines</font> ===
 
=== <font id="machine_decomposition">Decomposition of a machine in sub-machines</font> ===
The purpose of this paragraph is to specify how to decompose a machine in sub-machines.  
+
The purpose of this paragraph is to precisely describe how to decompose <math>M</math>.  
  
The hierarchy of machines (see the <math>REFINES</math> clauses) shall be first flatten (virtually or not), as illustrated below. The resulting machine is considered as being the non-decomposed machine from which the sub-machines shall be built.
+
The refinement hierarchy for <math>M</math> (see the <math>REFINES</math> clauses) shall not be considered for the decomposition. A sub-machine <math>M_i</math> may indeed be seen as a new abstract machine, which may be later refined if necessary. It is necessary to keep this assumption in mind when decomposing <math>M</math>.
<br>Note that it may be necessary to rename some variables or invariants.
 
 
 
<center>
 
[[Image:Flattening_machines.png]]
 
</center>
 
  
 
==== About the variables ====
 
==== About the variables ====
Line 82: Line 135:
 
The second option, which has the main advantage to be more scalable, is retained here.
 
The second option, which has the main advantage to be more scalable, is retained here.
  
===== Ensuring that a shared variable is not data-refined =====
+
===== Ensuring that a shared variable is not refined =====
A shared variable shall always be present in the state space of any refinement of the component.  
+
A ''shared'' variable shall always be present in the state space of any refinement of the component.  
 
The verification shall be added to those already performed by the static checker. The static checker shall have a way to determine if a given variable is ''shared'' or not.
 
The verification shall be added to those already performed by the static checker. The static checker shall have a way to determine if a given variable is ''shared'' or not.
  
===== <font id="var_partition">Partitioning the variables in the sub-machines of the decomposition</font> =====
+
===== <font id="var_distribution">Distributing the variables in the sub-machines of the decomposition</font> =====
The first question raised by the partition of the variables is whether it shall be the first stage of the decomposition, or not. Let's first suppose that the answer is "yes". The case where <math>e</math> is an event that accesses a variable <math>v1</math> associated to a sub-machine <math>M1</math> and a variable <math>v2</math> associated to a sub-machine <math>M2</math> cannot be successfully handled: should <math>e</math> be associated to <math>M1</math> or to <math>M2</math>? Moreover, contrary to the events, the variables are not essentially bearers of meanings, and they cannot by themselves guide the decomposition.
+
The first question raised by the distribution of the variables is whether it shall be the first stage of the decomposition, or not. Let's first suppose that the answer is "yes". The case where <math>e</math> is an event that accesses a variable <math>v1</math> associated to a sub-machine <math>M_1</math> and a variable <math>v2</math> associated to a sub-machine <math>M_2</math> cannot be successfully handled: should <math>e</math> be associated to <math>M_1</math> or to <math>M_2</math>? Moreover, contrary to the events, the variables are not essentially bearers of meanings, and they cannot by themselves guide the decomposition.
  
 
As a consequence, it is pertinent to assume that the events have been first partitioned. The following cases have then to be taken into consideration when dealing with the variable distribution:
 
As a consequence, it is pertinent to assume that the events have been first partitioned. The following cases have then to be taken into consideration when dealing with the variable distribution:
* If <math>v</math> is a variable that is only accessed by events of a given sub-machine <math>m</math>, then <math>v</math> is a ''private'' variable of <math>m</math>, and it shall be moved to <math>m</math>.
+
* If <math>v</math> is a variable that is only accessed by events of a given sub-machine <math>M_i</math>, then <math>v</math> is a ''private'' variable of <math>M_i</math>. It shall be moved to <math>M_i</math>.
* If <math>v</math> is a variable that is accessed by events of distinct sub-machines <math>m_1, ..., m_n</math>, then <math>v</math> is a ''shared'' variable, and it shall be duplicated in all sub-machines.
+
* If <math>v</math> is a variable that is accessed by events of distinct sub-machines <math>M_i, ..., M_j</math>, then <math>v</math> is a ''shared'' variable. It shall be tagged as such and duplicated in all sub-machines.
 +
 
 +
If all the variables are ''shared'' at the conclusion of the distribution, the end user shall be notified (it certainly means that the decomposition was not judicious!).
  
If all the variables are ''shared'' at the conclusion of the partition, the end user shall be notified (it certainly means that the decomposition was not judicious!).
+
===== Propagating the sharing status =====
 +
A variable tagged as ''shared'' in the non-decomposed machine (when resulting from a previous decomposition) shall remain ''shared'' in the sub-machines.
  
 
==== About the events ====
 
==== About the events ====
Line 99: Line 155:
  
 
We will examine in this section how to define such events in the Rodin platform, how to construct them, and how to enforce the rules that apply (in particular, these events cannot be refined).
 
We will examine in this section how to define such events in the Rodin platform, how to construct them, and how to enforce the rules that apply (in particular, these events cannot be refined).
 +
 +
===== <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.
 +
<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>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).
 +
 +
===== <font id="evt_status">Propagating the event status</font> =====
 +
The convergence status of a given event shall be propagated in the sub-machines as described below:
 +
* An event tagged as ordinary in the non-decomposed machine shall remain ordinary in the sub-machine.
 +
* An event tagged as convergent in the non-decomposed machine shall become ordinary 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.
 +
See [[Events_(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.
 +
 +
An event tagged as ''external'' in the non-decomposed machine (when resulting from a previous decomposition) shall remain ''external'' in the sub-machine.
  
 
===== Identifying an event as external =====
 
===== Identifying an event as external =====
Line 128: Line 201:
  
 
This solution is preferred because the notion of ''external'' event is totally orthogonal to the notion of convergence.
 
This solution is preferred because the notion of ''external'' event is totally orthogonal to the notion of convergence.
 +
 +
===== Ensuring that an external event is not refined =====
 +
If a machine <math>M_{i}'</math> refines a sub-machine <math>M_i</math>, several verifications shall be performed by the static checker to ensure that the external events defined in <math>M_i</math> are not refined in <math>M_{i}'</math>. In other terms, they shall be strictly identical in <math>M_i</math> and <math>M_{i}'</math>:
 +
* For each external event of <math>M_i</math>, <math>M_{i}'</math> shall define an event with the same name.
 +
* This event shall have a ''REFINES'' clause pointing to the event itself.
 +
* This event shall have the ''extended'' status.
 +
* This event shall not declare any additional element (parameter, guard, witness or action).
 +
The verifications shall be performed by the static checker. The static checker shall have a way to determine if a given event is ''external'' or not.
 +
 +
<font color=blue>With the introduction of theorem in guard, "extended" status will cause problem since ones required to prove again the theorem in guard at every refinement level. As far as I can see, there are two different possibilities:
 +
 +
* Changing all the theorems in guard into actual guards.
 +
 +
* Change the POG to disable the PO generation for proving theorem in guard for external events.
 +
 +
I (Son) think the first option is better and easier to implement.</font>
  
 
===== <font id="build_external">Constructing an external event</font> =====
 
===== <font id="build_external">Constructing an external event</font> =====
The construction of an ''external'' event highly relies on some [[Rewriting_rules_for_event_model_decomposition|rewriting / simplification rules]]. It is recommended to peruse them before reading further.
+
If <math>e</math> is an event that modifies a ''shared'' variable <math>s</math> (''i.e.'' <math>s</math> is listed among the free identifiers on the left-hand side of an assignment), then an ''external'' event that modifies <math>s</math> shall be built from <math>e</math> in each sub-machine where <math>s</math> is accessed.
 +
 
 +
The construction of an ''external'' event depends on the ''source'' machine (''i.e.'' the sub-machine containing the event <math>e</math> from which the ''external'' event is to be built) and on the ''destination'' machine (''i.e.'' the sub-machine where the ''external'' event is to be built).
 +
<br>
 +
Building an ''external'' event from a given event <math>e</math> modifying a ''shared'' variable <math>s</math> and duplicating it in each sub-machine where <math>s</math> is accessed is indeed incorrect, as illustrated below: the sub-machine <math>M_3</math> does not know the ''shared'' variable <math>s2</math> and the sub-machine <math>M_1</math> does not know the ''shared'' variable <math>s4</math>.
 +
 
 +
<center>
 +
[[Image:External_events.png]]
 +
</center>
  
<math>e</math> is an event of <math>M</math>, <math>v_i</math> are ''private'' variables of <math>M</math>, <math>s_i</math> are ''shared'' variables between <math>M</math> and the destination sub-machine (''i.e.'' the sub-machine where the ''external'' event will be dispatched), <math>P, P_i, Q_i</math> are before-after predicates of <math>M</math>, and <math>G</math> is a predicate of <math>M</math>.
+
The construction of an ''external'' event highly relies on some [[Rewriting_rules_for_event_model_decomposition|rewriting rules]]. It is recommended to peruse them before reading further.
 +
 
 +
<math>e</math> is an ''internal'' event of the ''source'' machine <math>M_s</math>, <math>s_i</math> are variables shared between <math>M_s</math> and the ''destination'' machine <math>M_d</math>, <math>v_i</math> are other variables (''private'' to <math>M_s</math> or ''shared'' between <math>M_s</math> and another sub-machine, distinct from <math>M_d</math>), <math>P, P_i</math> are before-after predicates, and <math>G</math> is a predicate.
  
 
<u>Generic construction</u>
 
<u>Generic construction</u>
<br>We first focus on the generic construction of an ''external'' event from an event of a sub-machine <math>M</math> whose action is expressed as follows:  
+
<br>We first focus on the generic construction of an ''external'' event from an ''internal'' event whose action is expressed as follows:  
  
 
   e
 
   e
Line 144: Line 243:
  
 
<ol>
 
<ol>
<li>The first step of the construction consists in replacing the ''private'' variables by parameters. Note that this step is purely fictive, because assigning an event parameter is not allowed!</li>
+
<li>The first step of the construction consists in replacing the <math>v_i</math> variables by parameters. Note that this step is purely fictive, because assigning an event parameter is not allowed!</li>
  
 
   e
 
   e
Line 166: Line 265:
  
 
<u>Derived constructions</u>
 
<u>Derived constructions</u>
<br>Then, it is possible to derivate the construction for other actions:
+
<br>Then, it is possible to derive the construction for other actions:
# [[Rewriting_rules_for_event_model_decomposition|Rewriting rules 1 to 5]] shall be first applied as many times as possible, from left to right, to get the action into the generic form introduced before.
+
# Each assignment of the action shall be handled separately (see [[Rewriting_rules_for_event_model_decomposition#separately|transformation rules]] on Event-B actions).
# Then, the steps detailed for the generic construction shall be followed.
+
# The [[Rewriting_rules_for_event_model_decomposition#transf_rules|transformation rules]] shall be applied on each Event-B assignment.
# Then, the [[Rewriting_rules_for_event_model_decomposition|simplification rules 6 to 8]] shall be enforced.
 
# Finally, the [[Rewriting_rules_for_event_model_decomposition|Rewriting rules 1 to 4]] shall be applied, from right to left.
 
 
 
Thus, if <math>P_i(x_1,...,x_n,s_1,...,s_m,s_i')~</math> is equal to <math>s_i' = Q_i(x_1,...,x_n,s_1,...,s_m)~</math>, and if there is no ''private'' variable (''i.e.'' there is no existential quantifier on the right-hand side of the assignments), then <math>s_i \bcmsuch P_{n+i}(x_1,...,x_n,s_1,...s_m,s_i')</math> shall be rewritten as <math>s_i \bcmeq Q_i(x_1,...,x_n,s_1,...,s_m)</math>.
 
<br>
 
The proof obligations generated for deterministic actions are indeed more suitable than those generated for non-deterministic actions.
 
 
 
In the same manner, <math>P_i(x_1,...,x_n,s_1,...,s_m,s_i')~</math> is equal to <math>s_i' \in Q_i(x_1,...,x_n,s_1,...,s_m)</math>, and if there is no private variable (''i.e.'' there is no existential quantifier on the right-hand side of the assignments), then <math>s_i \bcmsuch P_{n+i}(x_1,...,x_n,s_1,...s_m,s_i')</math> shall be rewritten as <math>s_i \bcmin Q_i(x_1,...,x_n,s_1,...,s_m)</math>.
 
<br>
 
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>).
 
  
 
<u>Example</u>
 
<u>Example</u>
Line 202: Line 291:
 
     s_m\!\!\! &\bcmsuch P_{n+m}(x_1,...,x_n,s_1,...s_m,s_m') \end{array}</math>
 
     s_m\!\!\! &\bcmsuch P_{n+m}(x_1,...,x_n,s_1,...s_m,s_m') \end{array}</math>
  
In this example, the rules [[Rewriting_rules_for_event_model_decomposition#rule_4|4]], [[Rewriting_rules_for_event_model_decomposition#rule_7|7]] and [[Rewriting_rules_for_event_model_decomposition#rule_8|8]] shall be applied.
+
===== <font id="build_init">Decomposing the initialization event</font> =====
 
+
An initialization event shall be built in each sub-machine from the initialization event of the non-decomposed machine, and according to the distribution of the variables among these sub-machines. The construction is detailed below. <math>initialization</math> is the initial event and <math>e</math> the built event, <math>x_i</math> are variables (''private'' or ''shared'') of the sub-machine containing <math>e</math>, <math>y_i</math> are variables of other sub-machines, and <math>P</math> is a predicate.
===== Partitioning the events in the sub-machines of the decomposition =====
 
The following sequence shall be followed:
 
* The events shall be first partitioned, as indicated by the end-user. More precisely, machines shall be created, according to this partition. At this step, the machines shall only contain the specified events. In particular, the <math>SEES</math> and <math>REFINES</math> clauses shall be empty. Moreover, note that it may be necessary to rename some events when performing the partition.
 
* The Rodin platform shall then be able to distribute the variables, according to the event partition (see [[#var_partition|Variable partition]]).
 
* The Rodin platform shall be able to distribute the invariants, according to the variable partition (see [[#inv_partition|Invariant partition]]).
 
* If <math>e</math> is an event that modifies a ''shared'' variable <math>s</math> (''i.e.'' <math>s</math> is listed among the free identifiers on the left-hand side of an assignment), then an ''external'' event that modifies <math>s</math> shall be built from <math>e</math> in each sub-machine where <math>s</math> is accessed.
 
 
 
''N.B.'' : Note that the construction of an ''external'' event depends on the ''source'' sub-machine (''i.e.'' the sub-machine containing the ''internal'' event <math>e</math> from which the ''external'' event is to be built) and on the ''destination'' sub-machine (''i.e.'' the sub-machine where the ''external'' event is to be built).
 
<br>
 
Building an ''external'' event from a given event <math>e</math> modifying a ''shared'' variable <math>s</math> and duplicating it in each sub-machine where <math>s</math> is accessed does not indeed entirely fit the requirements, as illustrated below: the sub-machine <math>M3</math> does not know the ''shared'' variable <math>s2</math> and the sub-machine <math>M1</math> does not know the ''shared'' variable <math>s4</math>.
 
 
 
<center>
 
[[Image:External_events.png]]
 
</center>
 
 
 
===== <font id="convergence">Propagating the convergence status</font> =====
 
A sub-machine can be seen as a new abstract machine. As a consequence, the convergence status of a given event shall be propagated in the sub-machines as described below:
 
* An event tagged as ordinary in the non-decomposed machine shall remain ordinary in the sub-machine.
 
* An event tagged as convergent in the non-decomposed machine shall become ordinary 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.
 
 
 
See [[Events_(Modelling_Language)|the modelling language]] for precisions on the convergence status.
 
 
 
===== Propagating the extended status =====
 
An event (''external'' or not) of a sub-machine shall always be declared as non-extended.
 
 
 
===== Ensuring that an external event cannot be refined =====
 
The verification shall be performed by the static checker. The static checker shall have a way to determine if a given event is ''external'' or not.
 
 
 
===== Decomposing the initialization event =====
 
An initialization event shall be built in each sub-machine from the initialization event of the non-decomposed machine, and according to the distribution of the variables among these sub-machines. The construction is detailed below. <math>initialization</math> is the initial event and <math>e</math> the built event, <math>x_i</math> are variables (''private'' or ''shared'') of the sub-machine containing <math>e</math>, <math>y_i</math> are variables of other sub-machines, <math>P</math> is a before-after predicate and <math>G</math> is a predicate.
 
  
 
   initialization     
 
   initialization     
 
   '''THEN'''                   
 
   '''THEN'''                   
     <math>x_1,...,x_n,y_1,...,y_m \bcmsuch P(x1,...,x_n,y_1,...,y_m,x_1',...,x_n',y_1',...,y_m')</math>
+
     <math>x_1,...,x_n,y_1,...,y_m \bcmsuch P(x_1',...,x_n',y_1',...,y_m')</math>
  
 
Only the variables of the considered sub-machine shall appear in the built initialization event; other variables shall become bound:  
 
Only the variables of the considered sub-machine shall appear in the built initialization event; other variables shall become bound:  
Line 245: Line 302:
 
   e   
 
   e   
 
   '''THEN'''                   
 
   '''THEN'''                   
     <math>x_1,...,x_n \bcmsuch \exists z_1,...,z_m \qdot P(x1,...,x_n,y_1,...,y_m,x_1',...,x_n',y_1,...,y_m')</math>
+
     <math>x_1,...,x_n \bcmsuch \exists z_1,...,z_m \qdot P(x_1',...,x_n',z_1,...,z_m)</math>
  
 
The derived cases and simplification rules introduced during [[#build_external|the construction of the external events]] apply here as well.
 
The derived cases and simplification rules introduced during [[#build_external|the construction of the external events]] apply here as well.
  
==== <font id="inv_partition">About the invariants</font> ====
+
===== Ensuring that a shared variable is not refined by an initialization event =====
We will see in this section how to distribute the invariants among the sub-machines, once the variables have been partitioned.
+
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>.
  
* Case 1: If <math>i</math> is an invariant only involving ''private'' variables of a given sub-machine, then it shall be copied in this sub-machine.
+
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.
* Case 2: If <math>i</math> is an invariant involving ''private'' variables of distinct sub-machines, then it shall not be copied.
 
* Case 3: If <math>i</math> is an invariant only involving ''shared'' variables, then it shall only be copied in the sub-machines containing all these variables.
 
* Case 4: If <math>i</math> is an invariant involving ''private'' variables and ''shared'' variables, then it shall only be copied in the sub-machines containing all these variables.
 
  
These different cases are illustrated in the figure below, where <math>P1</math>, <math>P2</math>, <math>P3</math> and <math>P4</math> are predicates. <math>A</math> is an abstract machine, <math>C</math> is a concrete machine extending <math>A</math>, <math>M</math> is the flattened machine for <math>C</math> and <math>A</math> (see [[#machine_decomposition|how flattening a hierarchy of machines]]), and <math>M1</math>, <math>M2</math>, and <math>M3</math> are the sub-machines resulting from the decomposition of <math>M</math>. <math>v1</math> is a ''private'' variable of <math>M1</math>, <math>v2</math> is a variable ''shared'' between <math>M1</math> and <math>M2</math>, <math>v3</math> is a variable ''shared'' between <math>M2</math> and <math>M3></math>, and <math>v4</math> is a ''private'' variable of <math>M3</math>.
+
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.
 +
 
 +
==== <font id="inv_distribution">About the invariants</font> ====
 +
We will see in this section how to distribute the invariants among the sub-machines, once the variables have been distributed.
 +
 
 +
An invariant based on a <math>P(v_m,...,v_n)~</math> predicate shall be copied in a sub-machine <math>M_i</math> if and only if <math>M_i</math> contains the <math>\{v_m,...,v_n\}~</math> variables.
 +
 
 +
This distribution is illustrated in the figure below, where <math>M_0</math> is an abstract machine, <math>M</math> is a concrete machine extending <math>M_0</math>, <math>M_1</math> and <math>M_2</math> are the sub-machines resulting from the decomposition of <math>M</math>. <math>v4</math> is a ''private'' variable of <math>M_2</math>, <math>v3</math> is a variable ''shared'' between <math>M_1</math> and <math>M_2</math>, and <math>P_i</math> are predicates.
  
 
<center>
 
<center>
Line 263: Line 324:
 
</center>
 
</center>
  
'''To summarize, an invariant based on a <math>P(v_m,...,v_n)~</math> predicate is copied in a sub-machine <math>M_x</math> if and only if <math>M_x</math> contains the <math>\{v_m,...,v_n\}~</math> variables.'''
+
If an invariant is used for typing but it has not been copied, a theorem shall be added in the sub-machines for each variable for which typing is required (otherwise a problem will be detected by the static checker). Note that there is no contradiction with the requirements on [[#po|proof obligations]]; no proof obligation (PO) is indeed generated for predicates <math>v \in T</math>, where <math>v</math> is a variable and <math>T</math> is a type.
  
If an invariant is used for typing but it has not been copied, a theorem shall be added in the sub-machines for each variable for which typing is required (otherwise a problem will be detected by the static checker). Note that there is no contradiction with the requirements on [[#po|proof obligations]]; no proof obligation (PO) is indeed generated for predicates <math>v \in T</math>, where <math>v</math> is a variable and <math>T</math> is a type.
+
In the same manner, if an invariant is used for well-definedness but is has not been copied, a theorem shall be added in the sub-machines. The associated proof obligation is the well-definedness (WD) obligation, and it is [[#po|assumed to be proved]]; as a consequence, it does not have to be generated in the sub-machines.
 +
<br>For example, let <math>c</math> be a constant. <math>P0</math>, <math>P1</math> and <math>P2</math> are defined as follows:<br>
 +
<math>\begin{array}{ll}P0\!\!\! &\defi v1 \in \nat \land v2 \in \nat\\
 +
                      P1\!\!\! &\defi v3 = c \div v4\\
 +
                      P2\!\!\! &\defi v4 = v1 + 1 \end{array}</math>
 +
<br>A theorem shall be added to indicate that <math>v4</math> is not null.
 +
<br>The <tt>org.event.core.ast.Formula.getWDPredicate</tt> method shall be used to compute the WD predicate associated to a given predicate. If no WD predicate is required, this method returns <tt>true</tt>. The built WD predicate shall be inserted before the associated predicate in the list of invariants of the considered sub-machine.
  
Beyond that, a workaround exists if an invariant <math>inv</math>, based on a <math>P(v_m,...,v_n)~</math> predicate, seems useful (for example an invariant between a concrete variable and some abstract variable) but it has disappeared in a sub-machine <math>M_x</math> containing variables <math>\{v_p,...,v_q\}~</math> (''eg.'' <math>inv2</math> and <math>inv3</math> have both been excluded from <math>M3</math> machine by application of the stated rules). It is indeed possible to add in the non-decomposed machine a theorem based on <math>P~</math>, but where the variables <math>\{v_m,...,v_n\} \setminus \{v_p,...,v_q\}</math> become bound, and then to perform again the decomposition. It will lead to a new proof obligation in the non-decomposed machine, which does not pose any difficulty.
+
Beyond that, a workaround exists if an invariant <math>inv</math>, based on a <math>P(v_m,...,v_n)~</math> predicate, seems useful (for example an invariant between a concrete variable and some abstract variable) but it has disappeared in a sub-machine <math>M_i</math> containing variables <math>\{v_p,...,v_q\}~</math> (''eg.'' <math>inv2</math> and <math>inv3</math> have both been excluded from the sub-machines by application of the stated rules). It is indeed possible to add in the non-decomposed machine a theorem based on <math>P~</math>, but where the variables <math>\{v_m,...,v_n\} \setminus \{v_p,...,v_q\}</math> become bound, and then to perform again the decomposition. It will lead to a new proof obligation in the non-decomposed machine, which does not pose any difficulty.
<br>For example, if a theorem <math>inv5: P5(v4)~</math>, with <math>P5 \defi \exists v1 \qdot P2(v1,v4)</math>, is added to the <math>C</math> concrete machine, then it will be copied in the sub-machine <math>M3</math> during the decomposition (see case 1). In order to prove the <math>P5~</math> statement, the bound variable <math>v1</math> shall obviously be instantiated with <math>v1</math>.
+
<br>For example, if a theorem <math>inv4: P4(v4)~</math>, with <math>P4 \defi \exists v1 \qdot P2(v1,v4)</math>, is added to the <math>M</math> concrete machine, then it will be copied in the sub-machine <math>M_2</math> during the decomposition. In order to prove the <math>P4~</math> statement, the bound variable <math>v1</math> shall obviously be instantiated with <math>v1</math>.
  
 
==== About the variants ====
 
==== About the variants ====
As mentioned [[#convergence|before]], there is no convergent event in sub-machines. As a consequence, there is no need to take the variants into consideration when performing the decomposition.
+
As mentioned [[#evt_status|before]], there is no convergent event in sub-machines. As a consequence, there is no need to take the variants into consideration when performing the decomposition.
  
 
=== <font id="context_decomposition">Decomposition of a context in sub-contexts</font> ===
 
=== <font id="context_decomposition">Decomposition of a context in sub-contexts</font> ===
The purpose of this paragraph is to specify how to decompose the contexts, according to the decomposition of the machines, and to establish how to link the sub-contexts to the sub-machines.
+
The purpose of this paragraph is to specify how to decompose a context, according to the decomposition of a given machine <math>M</math>, and to establish how to link the sub-contexts to the sub-machines.
  
The hierarchy of contexts (see the <math>EXTENDS</math> clauses) shall be first accumulated in a single context. More precisely, a new context shall be built (virtually or not), which contains all the carrier sets, constants and axioms of the hierarchy. This context is assumed to be the non-decomposed context from which the sub-contexts shall be built.
+
The hierarchy of contexts (see the <math>EXTENDS</math> clauses of contexts and the <math>SEES</math> clause of <math>M</math>) shall be first accumulated in a single context. More precisely, a new context <math>F</math> shall be built (virtually or not), which contains all the carrier sets, constants and axioms of the hierarchy. This context is assumed to be the non-decomposed context from which the sub-contexts <math>C_1,...,C_n</math> shall be built.
 
<br>Note that it may be necessary to rename some axioms when flattening the hierarchy.
 
<br>Note that it may be necessary to rename some axioms when flattening the hierarchy.
  
Line 283: Line 350:
 
</center>
 
</center>
  
Then, an empty context shall be built for each sub-machine <math>m</math>, which shall be linked to <math>m</math> through its <math>SEES</math> clause. Note that, at the conclusion of the context decomposition, the sub-contexts that may be empty shall not be kept, and a <math>SEES</math> clause shall not be added to the associated sub-machines.
+
Then, an empty context <math>C_i</math> shall be built for each sub-machine <math>M_i</math>, by respecting the following sequence: the constants shall be first included, then the carrier sets shall be added, and finally the axioms shall be considered.
 +
<br><math>C_i</math> shall be linked to <math>M_i</math> through its <math>SEES</math> clause. Note that, at the conclusion of the context decomposition, the sub-contexts <math>C_i</math> that may be empty shall not be kept, and a <math>SEES</math> clause shall not be added to the associated sub-machines <math>M_i</math>.
 +
 
 +
==== About the constants ====
 +
A constant of a non-decomposed context <math>F</math> shall be copied in a sub-context <math>C_i</math> if and only if it appears in a predicate (invariant or guard) or in an assignment (action) of the associated sub-machine <math>M_i</math>.
 +
<br>Thus, if a constant is not accessed by a sub-machine (''e.g.'' if such a constant was only accessed by an abstract machine extended by the non-decomposed machine), then it shall be left out during the decomposition. In parallel, if a constant is accessed by distinct sub-machines, then it shall be duplicated in the associated sub-contexts.
  
 
==== About the carrier sets ====
 
==== About the carrier sets ====
A carrier set shall be visible from any sub-machine that references it, through a predicate (invariant or guard) or an assignment (action). In other terms, a carrier set of a non-decomposed context shall be copied in a sub-context if and only if this set appears in a predicate or assignment of the associated sub-machine.
+
A carrier set shall be visible from any sub-machine <math>M_i</math> which accesses it, explicitly or implicitly, through a predicate or an assignment. In other terms, a carrier set of a non-decomposed context <math>F</math> shall be copied in a sub-context <math>C_i</math> if and only if this set appears in a predicate or assignment of the associated sub-machine <math>M_i</math>, or types a constant previously copied to <math>C_i</math>.
 
+
<br>As for the constants, a carrier set may be left out or duplicated.
==== About the constants ====
 
Similarly, a constant of a non-decomposed context shall be copied in a sub-context if and only if it appears in a predicate or an assignment of the associated sub-machine.
 
  
 
==== About the axioms ====
 
==== About the axioms ====
We will see in this section how to distribute the axioms among the sub-contexts, once the carrier sets and constants have been copied.  
+
We will see in this section how to distribute the axioms among the sub-contexts, once the constants and carrier sets have been copied.  
 
 
<font color="red">TODO.
 
An axiom is copied in a sub-machine <math>M_x</math> if and only if <math>M_x</math> contains the referenced constants and sets?
 
<br>Let consider a sub-machine <math>M1</math>. The associated sub-context <math>C1</math> contains a constant <math>cst1</math>; <math>axm1</math> is an axiom referencing <math>cst1</math> and another constant <math>cst2</math>. How to distribute this axiom? Is it copied to <math>M1</math>? In this case, it is necessary to copy <math>cst2</math> too.
 
</font>
 
 
 
== High-level Specification ==
 
The high-level specification details how the event model decomposition shall be integrated into the Rodin platform as a new feature, by linking to the existing architecture.
 
 
 
=== Definition of the decomposition ===
 
It is necessary to first give a definition of the event model decomposition in the Rodin platform. Is it an Event-B project decomposition? Or, is it a decomposition performed from some well-identified machines and contexts of a given Event-B project?
 
  
The entry point for the decomposition is a machine <math>M1</math>, its visible contexts, and its whole parent hierarchy of machines.
+
As for the [[#inv_distribution|invariants]], an axiom is copied in a sub-machine <math>M_i</math> if and only if <math>M_i</math> contains the referenced constants and sets. If an axiom is used for typing but it has not been copied, a theorem shall be added in the sub-contexts for each constant for which typing is required (otherwise a problem will be detected by the static checker).
 
 
<center>
 
[[Image:Machine.png]]
 
</center>
 
 
 
The machine <math>M1</math> to be taken as input for the decomposition shall be pointed by the end-user. The <math>EXTENDS</math> clauses of contexts and the <math>SEES</math> clauses of machines are used to build the associated hierarchy of contexts. In the same manner, the <math>REFINES</math> clauses allow to build the associated hierarchy of machines.
 
 
 
=== Configuration of the decomposition ===
 
The end-user shall be asked to parametrize the decomposition, and more precisely to:
 
* identify the machine to be taken as input for the decomposition.
 
* identify the sub-machines to be created.
 
* partition the events.
 
* indicate which invariants, axioms or theorems shall be ignored (because they are not required any longer).
 
 
 
It is more suitable for the end-user to visualize the configuration, and as a consequence it shall preferably be performed through the Graphical User Interface of the Rodin platform.
 
 
 
The following dialog box, which fills these requirements, is given as an example. The left-hand side displays the non-decomposed model and the right-hand side the decomposed model. The second one is built by the user, by first adding machines and then copying events from left to right. The unchecked invariants are those to be ignored, the checked events are those to be copied (the initialization events are not copied).
 
 
 
<center>
 
[[Image:GUI.png]]
 
</center>
 
 
 
=== Execution of the decomposition ===
 
A <tt>Decompose</tt> action shall be added. It shall be enabled if and only if a machine is selected. It shall be available from the <tt>Project</tt> menu, from the toolbar, and in the contextual menu displayed when right-clicking on the selected project.
 
 
 
[[Image:Action.png]]
 
 
 
A new Event-B project shall be created for each sub-machine built during the configuration. The [[#machine_decomposition|decomposition of the sub-machine]] shall first be completed, and then the non-decomposed [[#context_decomposition|context shall be partitioned]], as specified before.
 
 
 
As far as possible, the developments shall not be performed in the Event-B core; the dedicated extension points shall be used instead (''eg.'' those provided for the static checker. See the <tt>plugin.xml</tt> file of the <tt>org.eventb.core</tt> package).
 
 
 
=== <font id="po">Generation of the proof obligations</font> ===
 
A model to be decomposed is assumed to be proved, ''i.e.'' the proof obligations (PO) have all been handled successfully. The following conditions on PO shall be fulfilled during the decomposition:
 
* The decomposition shall not generate any new proof obligation.
 
* The proof obligations related to the non-decomposed model shall not be "propagated" to the decomposed models to be proved again. As a consequence, the Proof Obligation Generator (POG) shall be temporary disconnected until the decomposition is performed.
 
  
 
== Mathematical Approach ==
 
== Mathematical Approach ==
Line 347: Line 371:
 
Let's define <math>\mathit{MACHINE}</math> as the set of all machine handles, <math>\mathit{EVENT}</math> the set of all events, and <math>\mathit{VAR}</math> the set of all variables.
 
Let's define <math>\mathit{MACHINE}</math> as the set of all machine handles, <math>\mathit{EVENT}</math> the set of all events, and <math>\mathit{VAR}</math> the set of all variables.
  
* The distribution of the events of the non-decomposed machine among the different sub-machines (according to the end-user configuration) can be represented as with a partial function:
+
* The partition of the events of the non-decomposed machine among the different sub-machines (according to the end-user configuration) can be represented with a partial function:
 
<math>\mathit{partition}\in\mathit{EVENT}\pfun\mathit{MACHINE}</math>
 
<math>\mathit{partition}\in\mathit{EVENT}\pfun\mathit{MACHINE}</math>
 
<br>For a given sub-machine <math>m</math>, <math>partition^{-1}[\{m\}]~</math> is then the set of ''internal'' events of <math>m</math>.
 
<br>For a given sub-machine <math>m</math>, <math>partition^{-1}[\{m\}]~</math> is then the set of ''internal'' events of <math>m</math>.
Line 366: Line 390:
  
 
<center>
 
<center>
[[Image:Decomposition.png]]
+
[[Image:Example.png]]
 
</center>
 
</center>
  
A non-decomposed machine has been decomposed in two sub-machines <math>M1</math> and <math>M2</math>, as illustrated by the figure.
+
A non-decomposed machine has been decomposed in two sub-machines <math>M_1</math> and <math>M_2</math>, as illustrated by the figure.
<br>According to the terminology, <math>in\_a</math> and <math>a\_2\_b</math> are ''internal'' events of <math>M1</math>, and <math>b\_2\_c</math> and <math>out\_c</math> are ''internal'' events of <math>M2</math>. Concerning the variables, <math>a</math> and <math>m</math> are ''private'' variables of <math>M1</math>, <math>c</math> and <math>p</math> are ''private'' variables of <math>M2</math>, and <math>b</math>, <math>r</math> and <math>s</math> are ''shared'' variables.
+
<br>According to the terminology, <math>in\_a</math> and <math>a\_2\_b</math> are ''internal'' events of <math>M_1</math>, and <math>b\_2\_c</math> and <math>out\_c</math> are ''internal'' events of <math>M_2</math>. Concerning the variables, <math>a</math> and <math>m</math> are ''private'' variables of <math>M_1</math>, <math>c</math> and <math>p</math> are ''private'' variables of <math>M_2</math>, and <math>b</math>, <math>r</math> and <math>s</math> are ''shared'' variables.
<br>The variables accessed by the ''internal'' events of <math>M1</math> are <math>a</math>, <math>m</math>, <math>b</math>, <math>r</math> and <math>s</math>. The events modifying these variables are <math>in\_a</math>, <math>a\_2\_b</math>, which both are ''internal'' events of <math>M1</math>, and <math>b\_2\_c</math>, which is an ''internal'' event of <math>M2</math>. Thus, according to the definition given above, <math>b\_2\_c</math> is an ''external'' event for <math>M1</math>. In the same manner, <math>a\_2\_b</math> is an ''external'' event for <math>M2</math>.
+
<br>The variables accessed by the ''internal'' events of <math>M_1</math> are <math>a</math>, <math>m</math>, <math>b</math>, <math>r</math> and <math>s</math>. The events modifying these variables are <math>in\_a</math>, <math>a\_2\_b</math>, which both are ''internal'' events of <math>M_1</math>, and <math>b\_2\_c</math>, which is an ''internal'' event of <math>M_2</math>. Thus, according to the definition given above, <math>b\_2\_c</math> is an ''external'' event for <math>M_1</math>. In the same manner, <math>a\_2\_b</math> is an ''external'' event for <math>M_2</math>.
  
 
''N.B.'': Note that the expression "is an ''external'' event for" is an extrapolation, and shall be literally interpreted as "should lead to the construction of an ''external'' event in".
 
''N.B.'': Note that the expression "is an ''external'' event for" is an extrapolation, and shall be literally interpreted as "should lead to the construction of an ''external'' event in".
 +
 +
== Example ==
 +
It seems to be interesting to illustrate the decomposition step by step through an example. The considered example is described in the [[#ancre_1|Event Model Decomposition]]. <br>The [http://deploy-eprints.ecs.soton.ac.uk/139 QuestionResponse.zip] archive file contains the corresponding <tt>QuestionResponse</tt> Rodin project, and in particular the <math>M</math> machine taken as input for the decomposition. The <tt>QuestionResponse_i</tt> projects are issued from the decomposition and respectively contain the <math>M_1</math>, <math>M_2</math> and <math>M_3</math> sub-machines.
 +
 +
=== The events ===
 +
The events of <math>M</math> are partitioned among <math>M_1</math>, <math>M_2</math> and <math>M_3</math>, as illustrated below:
 +
* The <math>prepare\_question</math> event is an ''internal'' event of <math>M_1</math>.
 +
* The <math>read\_question</math> and <math>write\_question</math> events are ''internal'' events of <math>M_2</math>.
 +
* The <math>produce\_response</math> event is an ''internal'' event of <math>M_3</math>.
 +
<center>
 +
[[Image:Example2.png]]
 +
</center>
 +
 +
=== The variables ===
 +
The status (''private'' or ''shared'') of the variables is given below:
 +
[[Image:Example_variables.png|left]]
 +
* is a ''private'' variable of <math>M_1</math>.
 +
* is a ''private'' variable of <math>M_3</math>.
 +
* is a ''private'' variable of <math>M_2</math>.
 +
* is shared between <math>M_1</math> and <math>M_2</math>.
 +
* is shared between <math>M_2</math> and <math>M_3</math>.
 +
* is shared between <math>M_1</math> and <math>M_2</math>.
 +
* is shared between <math>M_1</math> and <math>M_2</math>.
 +
* is shared between <math>M_2</math> and <math>M_3</math>.
 +
* is shared between <math>M_2</math> and <math>M_3</math>.
 +
<br>
 +
The distribution of the variables follows:
 +
* The <math>question</math>, <math>buffer\_1</math>, <math>bit\_11</math> and <math>bit\_12</math> variables are copied in <math>M_1</math>.
 +
* The <math>channel</math>, <math>buffer\_1</math>, <math>buffer\_2</math>, <math>bit\_11</math>, <math>bit\_12</math>, <math>bit\_21</math> and <math>bit\_22</math> variables are copied in <math>M_2</math>.
 +
* The <math>response</math>, <math>buffer\_2</math>, <math>bit\_21</math> and <math>bit\_22</math> variables are copied in <math>M_3</math>.
 +
 +
=== The invariants ===
 +
The defined invariants are copied:
 +
[[Image:Example_invariants.png|left]]
 +
* is copied in <math>M_1</math> and <math>M_2</math>.
 +
* is copied in <math>M_1</math> and <math>M_2</math>.
 +
* is discarded, because it refers to an ''unknown'' variable (<math>bool\_1</math>).
 +
* is copied in <math>M_2</math> and <math>M_3</math>.
 +
* is copied in <math>M_2</math> and <math>M_3</math>.
 +
* is discarded, because it refers to an ''unknown'' variable (<math>bool\_2</math>).
 +
<br>
 +
The missing typing theorems are added. The typing information is extracted from the <tt>QuestionResponse.bcm</tt> file:
 +
* The <math>question \in \pow (QUESTION)</math> theorem is added to <math>M_1</math> to type the <math>question</math> variable.
 +
* The <math>buffer\_1 \in QUESTION</math> theorem is added to <math>M_1</math> to type the <math>buffer\_1</math> variable.
 +
* The <math>channel \in \pow (QUESTION)</math> theorem is added to <math>M_2</math> to type the <math>channel</math> variable.
 +
* The <math>response \in \pow (RESPONSE)</math> theorem is added to <math>M_3</math> to type the <math>response</math> variable.
 +
* The <math>buffer\_2 \in QUESTION</math> theorem is added to <math>M_3</math> to type the <math>buffer\_2</math> variable.
 +
 +
=== The external events ===
 +
[[Image:external_prepare_question.png|left]]
 +
<math>prepare\_question</math> is an event of <math>M_1</math> modifying the <math>bit\_11</math> and <math>buffer\_1</math> shared variables. 
 +
<br>These variables are accessed by the <math>write\_question</math> event of <math>M_2</math>.
 +
<br>An ''external'' event is therefore built from <math>prepare\_question</math> in <math>M_2</math>.
 +
<br>Since <math>M_2</math> does not contain the <math>question</math> variable, a <math>question</math> parameter is created.
 +
<br>Moreover, a guard is added to type it. The <tt>QuestionResponse.bcm</tt> is parsed to retrieve this typing information.
 +
<br>The <math>act1</math> action related to the <math>question</math> variable is discarded.
 +
<br>The <math>act2</math> and <math>act3</math> actions are kept.
 +
<br>
 +
<br>
 +
In parallel, <math>produce\_response</math> is an event of <math>M_3</math> modifying the <math>bit\_22</math> shared variable. This variable is accessed by the <math>read\_question</math> event of <math>M_2</math>. As a consequence, an external event is built from <math>produce\_response</math> in <math>M_2</math>.
 +
 +
In the same manner, <math>read\_question</math> is an event of <math>M_2</math> modifying the <math>bit\_21</math> and <math>buffer\_2</math> shared variables. These variables are accessed by the <math>produce\_response</math> event of <math>M_3</math>. As a consequence, an external event is built from <math>read\_question</math> in <math>M_3</math>.
 +
 +
Finally, <math>write\_question</math> is an event of <math>M_2</math> modifying the <math>bit\_12</math> shared variable. This variable is accessed by the <math>prepare\_question</math> event of <math>M_1</math>. As a consequence, an external event is built from <math>write\_question</math> in <math>M_1</math>.
 +
 +
=== The initialization events ===
 +
The initialization events of the sub-machines are built from the initialization event of <math>M</math>, which is detailed below:
 +
<br>
 +
[[image:Example_initialization.png]]
 +
<br>The initialization event of <math>M_1</math> initializes the variables contained in this sub-machine: the assignments related to the <math>question</math>, <math>buffer\_1</math>, <math>bit\_11</math> and <math>bit\_12</math> variables are kept; the other assignments are discarded.
 +
<br>In the same manner, the initialization event of <math>M_3</math> initializes the variables contained in this sub-machine: the assignments related to the <math>response</math>, <math>buffer\_2</math>, <math>bit\_21</math> and <math>bit\_22</math> are kept; the other assignments are discarded.
 +
<br>Finally, when building the initialization event of <math>M_2</math>, the assignments are all kept, except those corresponding to <math>question</math> and <math>response</math>.
 +
 +
=== The contexts ===
 +
The contexts of the sub-machines are built from the context <math>C0</math> associated to <math>M</math>:
 +
<br>
 +
[[image:Example_contexts.png]]
 +
<br>
 +
For each sub-machine <math>M_i</math>, an empty context is created and a ''SEES'' clause identifying this context is added in <math>M_i</math>. Then, these contexts are filled:
 +
* <math>M_1</math>, <math>M_2</math> and <math>M_3</math> reference the <math>QUESTION</math> set. It is therefore copied in each context.
 +
* The <math>RESPONSE</math> set is only referenced by <math>M_3</math>. It is copied in the associated context.
 +
* The <math>answer</math> constant is only referenced by <math>M_3</math>. It is copied in the associated context.
 +
* The sets and constants referenced by the <math>axm1</math> axiom have been previously copied in the context associated to <math>M_3</math>. As a consequence, it is copied in this context too.
 +
 +
To summarize, the context seen by <math>M_1</math> and <math>M_2</math> only contains the <math>QUESTION</math> set. The context seen by <math>M_3</math> is equal to <math>C0</math>.
 +
 +
== Implementation ==
 +
A first plugin prototype is accessible under <tt>_exploratory/tshoang/ch.ethz.eventb.decomposition</tt>.
  
 
== Bibliography ==
 
== Bibliography ==
 
* J.R. Abrial, <font id="ancre_3">''The B-book: assigning programs to meanings''</font>, Cambridge University Press, 1996 (ISBN 0-521-49619-5).
 
* J.R. Abrial, <font id="ancre_3">''The B-book: assigning programs to meanings''</font>, Cambridge University Press, 1996 (ISBN 0-521-49619-5).
* J.R. Abrial, Mathematical Models for Refinement and Decomposition, in ''The Event-B Book'', to be published in 2009 ([http://www.event-b.org/abook.html lien externe]).
+
* J.R. Abrial, Mathematical Models for Refinement and Decomposition, in [http://www.event-b.org/abook.html ''Modeling in Event-B: System and Software Engineering''], to be published in 2009.
* J.R. Abrial, <font id="ancre_1">''Event Model Decomposition''</font>, Version 1.3, April 2009.
+
* J.R. Abrial, <font id="ancre_1">[http://wiki.event-b.org/images/Event_Model_Decomposition-1.3.pdf ''Event Model Decomposition'']</font>, Version 1.3, April 2009.
* M. Butler, <font id="ancre_2">Decomposition Structures for Event-B</font>, in ''Integrated Formal Methods iFM2009'', Springer, LNCS 5423, 2009 ([http://eprints.ecs.soton.ac.uk/16965/1/butler.pdf lien externe]).
+
* M. Butler, <font id="ancre_2">[http://eprints.ecs.soton.ac.uk/16965/1/butler.pdf ''Decomposition Structures for Event-B'']</font>, in Integrated Formal Methods iFM2009, Springer, LNCS 5423, 2009.
 +
* M. Butler, <font id="ancre_4">[http://eprints.ecs.soton.ac.uk/16910/2/marktoberdorf2.pdf ''Incremental Design of Distributed Systems with Event-B'']</font>, in Marktoberdorf Summer School 2008 Lecture Notes, 2008.
 +
* M. Poppleton,[http://eprints.ecs.soton.ac.uk/16487/1/poppletonABZ2008.pdf ''The composition of Event-B models''], in ABZ2008: Int. Conference on ASM, B and Z, 2008.
  
 
[[Category:Design]]
 
[[Category:Design]]
[[Category:Work in progress]]
 

Revision as of 16:49, 7 October 2009

Introduction

One of the most important feature of the Event-B approach is the possibility to introduce new events during refinement steps, but a consequence is an increasing complexity of the refinement process when having to deal with many events and many state variables.

The main idea of the decomposition is to cut a model M into sub-models M_1, ..., M_n, which can be refined separately and more comfortably than the whole.

The constraint that shall be satisfied by the decomposition is that these refined models might be recomposed into a whole model MR in a way that guarantees that MR refines M. Note that this recomposition will never be performed in practice.

An event-based decomposition of a model is detailed in the Event Model Decomposition article: the events of a model are partitioned to form the events of the sub-models. In parallel, the variables on which these events act are distributed among the sub-models.

The purpose is here to precisely describe what is required at the Rodin platform level to integrate this event model decomposition, and to explain why. The details of how it could be implemented are out of scope.

Terminology

This section introduces the definitions of the main technical terms, which are widely used in the sequel.

  • Event model decomposition: The decomposition of a model in sub-models, called A-style decomposition (after Abrial). The B-style decomposition (after Butler) is not considered here.

A model can contain contexts, machines, or both (see 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-context: A context built from a non-decomposed context during the event model decomposition.
  • Shared variable: A variable accessed by events of distinct sub-machines (by opposition to private variable). A variable is said to be shared between a sub-machine M_i and a sub-machine M_j if and only if it is accessed by events of M_i and by events of M_j.
  • Private variable: A variable accessed by events of a single sub-machine (by opposition to shared variable).
  • External event: An event of a sub-machine which is built from an event of the non-decomposed machine, and which simulates the way the shared variables (between this sub-machine and another sub-machine) are handled in the non-decomposed machine (by opposition to internal event).
  • Internal event: An event copied from the non-decomposed machine to a sub-machine, according to the end-user specified distribution (by opposition to external event).

Note that a variable is said to be accessed when it is read or written. More precisely, such an access may be performed by a predicate (invariant, guard, witness) or in an assignment (action).

High-level Specification

The high-level specification details how the event model decomposition shall be integrated into the Rodin platform as a new feature, by linking to the existing architecture.

Definition of the decomposition

It is necessary to first give a definition of the event model decomposition in the Rodin platform. Is it an Event-B project decomposition? Or, is it a decomposition performed from some well-identified machines and contexts of a given Event-B project?

As illustrated in the diagram below, when considering a given Event-B project, the entry point for the decomposition is a machine M of the project, and its whole hierarchy of seen contexts. The machine M to be taken as input for the decomposition shall be pointed by the end-user.

Decomposition.png

Configuration of the decomposition

The end-user shall be asked to parametrize the decomposition, and more precisely to:

  • identify the machine to be taken as input for the decomposition.
  • identify the sub-machines to be created.
  • partition the events.

It is more suitable for the end-user to visualize the configuration, and as a consequence it shall preferably be performed through the Graphical User Interface of the Rodin platform.

The following dialog box, which fills these requirements, is given as an example. The left-hand side displays the non-decomposed model and the right-hand side the decomposed model. The second one is built by the user, by first adding machines and then copying events from left to right.

GUI.png

The end-user shall have a way to backup its configuration. More precisely, it shall be possible on the one hand to export a configuration to a file, and on the other hand to import a configuration from a file.

Execution of the decomposition

A Decompose action shall be added. It shall be enabled if and only if a machine is selected. It shall be available from the Project menu, from the toolbar, and in the contextual menu displayed when right-clicking on the selected project.

Action.png

A new Event-B project shall be created for each sub-machine built during the configuration. The decomposition of the sub-machine shall first be completed, and then the non-decomposed context shall be partitioned.
The created projects and components (machines and contexts) shall be tagged as "automatically generated". It shall be possible to identify the non-decomposed machine from which they are issued.

As far as possible, the developments shall not be performed in the Event-B core; the dedicated extension points shall be used instead (eg. those provided for the static checker. See the plugin.xml file of the org.eventb.core package).

Generation of the proof obligations

A model to be decomposed is assumed to be proved, i.e. all the proof obligations (PO) have been handled successfully. The decomposition of a model shall otherwise be forbidden.

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

  • The decomposition shall not generate any new proof obligation.
  • The proof obligations related to the non-decomposed model shall not be "propagated" to the decomposed models to be proved again. As a consequence, the Proof Obligation Generator (POG) shall be temporary disconnected until the decomposition is performed.

Low-level Specification

The low-level specification details through several steps how the event model decomposition shall be performed, and in which order. It establishes a distinction between the steps performed on the end-user's initiative, and the computed ones. It links when possible to the already implemented features of the Rodin platform which can be used at some steps.

The following sequence shall be observed to decompose a machine M in sub-machines M_1,...,M_n:

  1. The events of M shall be partitioned in M_1,...,M_n, as indicated by the end-user (see Event partition).
  2. The Rodin platform shall update the status of the events (see Event status).
  3. The Rodin platform shall distribute the variables of M in M_1,...,M_n, according to the event partition (see Variable distribution).
  4. The Rodin platform shall distribute the invariants of M in M_1,...,M_n, according to the variable distribution (see Invariant distribution).
  5. The Rodin platform shall build external events in M_1,...,M_n, from the events of M, and according to the variable distribution (see External event construction).
  6. The Rodin platform shall build the initialization events of M_1,...,M_n, according to the variable distribution (see Initialization event construction).
  7. The Rodin platform shall build the contexts seen by M_1,...,M_n, from the hierarchy of contexts associated to M (see Context decomposition).

This order will be justified by itself subsequently, when going into the details of the decomposition.

Decomposition of a machine in sub-machines

The purpose of this paragraph is to precisely describe how to decompose M.

The refinement hierarchy for M (see the REFINES clauses) shall not be considered for the decomposition. A sub-machine M_i may indeed be seen as a new abstract machine, which may be later refined if necessary. It is necessary to keep this assumption in mind when decomposing M.

About the variables

Some variables are needed by several sub-machines of the decomposition. As a consequence, these variables shall be replicated in the sub-machines. Beyond that, since it is not possible to ensure that such a variable will be refined in the same way in each sub-machine, they shall be given a special status (shared variable), with the limitation that they cannot be refined.

We will specify in this section how to introduce the notion of shared variable in the Rodin platform, and how to check the associated rules.

Defining a variable as shared

The following DTD excerpt describes the structure of a variable in the Rodin database:

<!ENTITY % NameAttDecl "name CDATA #REQUIRED">
<!ENTITY % CommentAttDecl "org.eventb.core.comment CDATA #IMPLIED">
<!ENTITY % IdentAttDecl "org.eventb.core.identifier CDATA #REQUIRED">

<!ELEMENT %variable; EMPTY>
<!ATTLIST %variable;
  %NameAttDecl;
  %CommentAttDecl;
  %IdentAttDecl;
  >

A first possibility to tag a variable as shared would be to add a shared specific attribute, which would be set to true if and only if the variable is shared:

<ENTITY % shared "org.eventb.core.shared CDATA #REQUIRED">

<!ELEMENT %variable; EMPTY>
<!ATTLIST %variable;
  ...
  %shared; (false|true) #REQUIRED
  >

Another possibility would be to define a more generic attribute, which could take different values, according to the nature of the variable:

<ENTITY % nature "org.eventb.core.nature CDATA #REQUIRED">

<!ATTLIST %variable;
  ...
  %nature; (0|1) #REQUIRED
  >

The second option, which has the main advantage to be more scalable, is retained here.

Ensuring that a shared variable is not refined

A shared variable shall always be present in the state space of any refinement of the component. The verification shall be added to those already performed by the static checker. The static checker shall have a way to determine if a given variable is shared or not.

Distributing the variables in the sub-machines of the decomposition

The first question raised by the distribution of the variables is whether it shall be the first stage of the decomposition, or not. Let's first suppose that the answer is "yes". The case where e is an event that accesses a variable v1 associated to a sub-machine M_1 and a variable v2 associated to a sub-machine M_2 cannot be successfully handled: should e be associated to M_1 or to M_2? Moreover, contrary to the events, the variables are not essentially bearers of meanings, and they cannot by themselves guide the decomposition.

As a consequence, it is pertinent to assume that the events have been first partitioned. The following cases have then to be taken into consideration when dealing with the variable distribution:

  • If v is a variable that is only accessed by events of a given sub-machine M_i, then v is a private variable of M_i. It shall be moved to M_i.
  • If v is a variable that is accessed by events of distinct sub-machines M_i, ..., M_j, then v is a shared variable. It shall be tagged as such and duplicated in all sub-machines.

If all the variables are shared at the conclusion of the distribution, the end user shall be notified (it certainly means that the decomposition was not judicious!).

Propagating the sharing status

A variable tagged as shared in the non-decomposed machine (when resulting from a previous decomposition) shall remain shared in the sub-machines.

About the events

It shall be possible to simulate the way the shared variables are handled in the non-decomposed machine. This is precisely the purpose of the so-called external events.

We will examine in this section how to define such events in the Rodin platform, how to construct them, and how to enforce the rules that apply (in particular, these events cannot be refined).

Partitioning the events in the sub-machines of the decomposition

The sub-machines M_1,...,M_n shall be built and the events of M shall be partitioned in these newly created machines, according to the end-user configuration. The initialization event of M shall be left out. All other events shall be distributed.
At this step, the sub-machines shall only contain these internal events. In particular, the SEES and REFINES clauses of M_1,...,M_n shall be empty. In the same manner, the REFINES and WITH (witnesses) clauses of the events shall be left out.
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).

Propagating the event status

The convergence status of a given event shall be propagated in the sub-machines as described below:

  • An event tagged as ordinary in the non-decomposed machine shall remain ordinary in the sub-machine.
  • An event tagged as convergent in the non-decomposed machine shall become ordinary 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.

See 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.

An event tagged as external in the non-decomposed machine (when resulting from a previous decomposition) shall remain external in the sub-machine.

Identifying an event as external

An attribute is already defined, which is introduced below, to precise the nature of an event. A first solution would be to add another masked value (eg. 4) to encode the external status.

<!ENTITY % convergence "org.eventb.core.convergence">

<!ATTLIST %event;
 ...
 %convergence; (0|1|2) #REQUIRED
 ...
 >

Another solution would be to add a distinct external attribute, which would be set to true if and only if the event is external:

<ENTITY % external "org.eventb.core.external CDATA #REQUIRED">

<!ATTLIST %event;
 ...
 %external; (false|true) #REQUIRED
 >

This solution is preferred because the notion of external event is totally orthogonal to the notion of convergence.

Ensuring that an external event is not refined

If a machine M_{i}' refines a sub-machine M_i, several verifications shall be performed by the static checker to ensure that the external events defined in M_i are not refined in M_{i}'. In other terms, they shall be strictly identical in M_i and M_{i}':

  • For each external event of M_i, M_{i}' shall define an event with the same name.
  • This event shall have a REFINES clause pointing to the event itself.
  • This event shall have the extended status.
  • This event shall not declare any additional element (parameter, guard, witness or action).

The verifications shall be performed by the static checker. The static checker shall have a way to determine if a given event is external or not.

With the introduction of theorem in guard, "extended" status will cause problem since ones required to prove again the theorem in guard at every refinement level. As far as I can see, there are two different possibilities:

  • Changing all the theorems in guard into actual guards.
  • Change the POG to disable the PO generation for proving theorem in guard for external events.

I (Son) think the first option is better and easier to implement.

Constructing an external event

If e is an event that modifies a shared variable s (i.e. s is listed among the free identifiers on the left-hand side of an assignment), then an external event that modifies s shall be built from e in each sub-machine where s is accessed.

The construction of an external event depends on the source machine (i.e. the sub-machine containing the event e from which the external event is to be built) and on the destination machine (i.e. the sub-machine where the external event is to be built).
Building an external event from a given event e modifying a shared variable s and duplicating it in each sub-machine where s is accessed is indeed incorrect, as illustrated below: the sub-machine M_3 does not know the shared variable s2 and the sub-machine M_1 does not know the shared variable s4.

External events.png

The construction of an external event highly relies on some rewriting rules. It is recommended to peruse them before reading further.

e is an internal event of the source machine M_s, s_i are variables shared between M_s and the destination machine M_d, v_i are other variables (private to M_s or shared between M_s and another sub-machine, distinct from M_d), P, P_i are before-after predicates, and G is a predicate.

Generic construction
We first focus on the generic construction of an external event from an internal event whose action is expressed as follows:

 e
 WHERE 
   G(v_1,...,v_n,s_1,...,s_m)~      
 THEN                  
   v_1,...,v_n,s_1,...,s_m \bcmsuch P(v1,...,v_n,s_1,...,s_m, v_1',...,v_n',s_1',...,s_m')
  1. The first step of the construction consists in replacing the v_i variables by parameters. Note that this step is purely fictive, because assigning an event parameter is not allowed!
  2. e ANY x_1,...,x_n~ WHERE G(x_1,...,x_n,s_1,...,s_m)~ THEN 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')
  3. 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 .bcm file associated to the non-decomposed machine shall be parsed in order to retrieve the typing information.
  4. The third and last step of the construction consists in introducing an existential quantifier to resolve the invalid assignment. external\_e is the newly built external event.
  5. external_e ANY x_1,...,x_n~ WHERE G(x_1,...,x_n,s_1,...,s_m)~ THEN s_1,...,s_m \bcmsuch \exists y_1,...y_n \qdot P(x1,...,x_n,s_1,...,s_m, y_1,...,y_n,s_1',...,s_m')

Derived constructions
Then, it is possible to derive the construction for other actions:

  1. Each assignment of the action shall be handled separately (see transformation rules on Event-B actions).
  2. The transformation rules shall be applied on each Event-B assignment.

Example

 e
 WHERE 
   G(v_1,...,v_n,s_1,...,s_m)~      
 THEN                  
   \begin{array}{ll}v_1\!\!\! &\bcmsuch P_1(v_1,...,v_n,s_1,...,s_m,v_1')\\
    ...\\
    v_n\!\!\! &\bcmsuch P_n(v_1,...,v_n,s_1,...,s_m,v_n')\\
    s_1\!\!\! &\bcmsuch P_{n+1}(v_1,...,v_n,s_1,...,s_m,s_1')\\
    ...\\
    s_m\!\!\! &\bcmsuch P_{n+m}(v_1,...,v_n,s_1,...,s_m,s_m') \end{array}
 external_e
 ANY x_1,...,x_n~
 WHERE 
   G(x_1,...,x_n,s_1,...,s_m)~      
 THEN                  
   \begin{array}{ll}s_1\!\!\! &\bcmsuch P_{n+1}(x_1,...,x_n,s_1,...,s_m,s_1')\\
    ...\\
    s_m\!\!\! &\bcmsuch P_{n+m}(x_1,...,x_n,s_1,...s_m,s_m') \end{array}
Decomposing the initialization event

An initialization event shall be built in each sub-machine from the initialization event of the non-decomposed machine, and according to the distribution of the variables among these sub-machines. The construction is detailed below. initialization is the initial event and e the built event, x_i are variables (private or shared) of the sub-machine containing e, y_i are variables of other sub-machines, and P is a predicate.

 initialization    
 THEN                  
   x_1,...,x_n,y_1,...,y_m \bcmsuch P(x_1',...,x_n',y_1',...,y_m')

Only the variables of the considered sub-machine shall appear in the built initialization event; other variables shall become bound:

 e   
 THEN                  
   x_1,...,x_n \bcmsuch \exists z_1,...,z_m \qdot P(x_1',...,x_n',z_1,...,z_m)

The derived cases and simplification rules introduced during the construction of the external events apply here as well.

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

If M_{i}' refines a sub-machine M_i issued from the decomposition of a machine M, the initialization event of M_{i}' shall not constrain a shared variable more or less than it was in the initialization event of M_i.

An initialization event shall not contain an action modifying at the same time a shared variable and a private variable (eg. a,b \bcmsuch P(a',b'), where a is private and b 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 M shall be forbidden if its initialization event contain such an action. Moreover, the static checker shall ensure that the initialization event of M_{i}' does not contain such an action.

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

About the invariants

We will see in this section how to distribute the invariants among the sub-machines, once the variables have been distributed.

An invariant based on a P(v_m,...,v_n)~ predicate shall be copied in a sub-machine M_i if and only if M_i contains the \{v_m,...,v_n\}~ variables.

This distribution is illustrated in the figure below, where M_0 is an abstract machine, M is a concrete machine extending M_0, M_1 and M_2 are the sub-machines resulting from the decomposition of M. v4 is a private variable of M_2, v3 is a variable shared between M_1 and M_2, and P_i are predicates.

Invariants.png

If an invariant is used for typing but it has not been copied, a theorem shall be added in the sub-machines for each variable for which typing is required (otherwise a problem will be detected by the static checker). Note that there is no contradiction with the requirements on proof obligations; no proof obligation (PO) is indeed generated for predicates v \in T, where v is a variable and T is a type.

In the same manner, if an invariant is used for well-definedness but is has not been copied, a theorem shall be added in the sub-machines. The associated proof obligation is the well-definedness (WD) obligation, and it is assumed to be proved; as a consequence, it does not have to be generated in the sub-machines.
For example, let c be a constant. P0, P1 and P2 are defined as follows:
\begin{array}{ll}P0\!\!\! &\defi v1 \in \nat \land v2 \in \nat\\
                       P1\!\!\! &\defi v3 = c \div v4\\
                       P2\!\!\! &\defi v4 = v1 + 1 \end{array}
A theorem shall be added to indicate that v4 is not null.
The org.event.core.ast.Formula.getWDPredicate method shall be used to compute the WD predicate associated to a given predicate. If no WD predicate is required, this method returns true. The built WD predicate shall be inserted before the associated predicate in the list of invariants of the considered sub-machine.

Beyond that, a workaround exists if an invariant inv, based on a P(v_m,...,v_n)~ predicate, seems useful (for example an invariant between a concrete variable and some abstract variable) but it has disappeared in a sub-machine M_i containing variables \{v_p,...,v_q\}~ (eg. inv2 and inv3 have both been excluded from the sub-machines by application of the stated rules). It is indeed possible to add in the non-decomposed machine a theorem based on P~, but where the variables \{v_m,...,v_n\} \setminus \{v_p,...,v_q\} become bound, and then to perform again the decomposition. It will lead to a new proof obligation in the non-decomposed machine, which does not pose any difficulty.
For example, if a theorem inv4: P4(v4)~, with P4 \defi \exists v1 \qdot P2(v1,v4), is added to the M concrete machine, then it will be copied in the sub-machine M_2 during the decomposition. In order to prove the P4~ statement, the bound variable v1 shall obviously be instantiated with v1.

About the variants

As mentioned before, there is no convergent event in sub-machines. As a consequence, there is no need to take the variants into consideration when performing the decomposition.

Decomposition of a context in sub-contexts

The purpose of this paragraph is to specify how to decompose a context, according to the decomposition of a given machine M, and to establish how to link the sub-contexts to the sub-machines.

The hierarchy of contexts (see the EXTENDS clauses of contexts and the SEES clause of M) shall be first accumulated in a single context. More precisely, a new context F shall be built (virtually or not), which contains all the carrier sets, constants and axioms of the hierarchy. This context is assumed to be the non-decomposed context from which the sub-contexts C_1,...,C_n shall be built.
Note that it may be necessary to rename some axioms when flattening the hierarchy.

Flattening contexts.png

Then, an empty context C_i shall be built for each sub-machine M_i, by respecting the following sequence: the constants shall be first included, then the carrier sets shall be added, and finally the axioms shall be considered.
C_i shall be linked to M_i through its SEES clause. Note that, at the conclusion of the context decomposition, the sub-contexts C_i that may be empty shall not be kept, and a SEES clause shall not be added to the associated sub-machines M_i.

About the constants

A constant of a non-decomposed context F shall be copied in a sub-context C_i if and only if it appears in a predicate (invariant or guard) or in an assignment (action) of the associated sub-machine M_i.
Thus, if a constant is not accessed by a sub-machine (e.g. if such a constant was only accessed by an abstract machine extended by the non-decomposed machine), then it shall be left out during the decomposition. In parallel, if a constant is accessed by distinct sub-machines, then it shall be duplicated in the associated sub-contexts.

About the carrier sets

A carrier set shall be visible from any sub-machine M_i which accesses it, explicitly or implicitly, through a predicate or an assignment. In other terms, a carrier set of a non-decomposed context F shall be copied in a sub-context C_i if and only if this set appears in a predicate or assignment of the associated sub-machine M_i, or types a constant previously copied to C_i.
As for the constants, a carrier set may be left out or duplicated.

About the axioms

We will see in this section how to distribute the axioms among the sub-contexts, once the constants and carrier sets have been copied.

As for the invariants, an axiom is copied in a sub-machine M_i if and only if M_i contains the referenced constants and sets. If an axiom is used for typing but it has not been copied, a theorem shall be added in the sub-contexts for each constant for which typing is required (otherwise a problem will be detected by the static checker).

Mathematical Approach

The purpose of this section is to mathematically formalize the Event-B decomposition previously specified, and by the way to remove the possible remaining ambiguity.

Let's define \mathit{MACHINE} as the set of all machine handles, \mathit{EVENT} the set of all events, and \mathit{VAR} the set of all variables.

  • The partition of the events of the non-decomposed machine among the different sub-machines (according to the end-user configuration) can be represented with a partial function:

\mathit{partition}\in\mathit{EVENT}\pfun\mathit{MACHINE}
For a given sub-machine m, partition^{-1}[\{m\}]~ is then the set of internal events of m.

  • The access of a variable by a given event (according to the static-checker) can be expressed as:

\mathit{access}\in\mathit{EVENT}\rel\mathit{VAR}
For a given variable v, (partition;access^{-1})[\{v\}]~ is then the set of the sub-machines accessing v, and v is a private variable of a sub-machine m if and only if this set contains a single component (i.e. card((partition;access^{-1})[\{v\}]) = 1~); otherwise, and if and only if this set is not empty, v is shared.
In parallel, for a given sub-machine m, (access;partition^{-1})[\{m\}]~ is the set of variables accessed by the events contained in m.

  • The association of a variable with the events modifying this variable (according to the static-checker) can be specified as:

\mathit{modify}\in\mathit{VAR}\rel\mathit{EVENT}
For a given sub-machine m and a variable v \in (access;partition^{-1})[\{m\}], modify[\{v\}]~ is then the set of the events modifying v.

  • The construction of the external events for a sub-machine can be represented with a relation:

\mathit{extern}\in\mathit{MACHINE}\rel\mathit{EVENT}
It is computed as follows: extern = (modify;access;partition^{-1}) \setminus partition^{-1}
Thus, the external events of a given sub-machine m are events modifying the variables accessed by the internal events of m, but they are not internal events of m.

Example

The following example is taken from the Event Model Decomposition.

Example.png

A non-decomposed machine has been decomposed in two sub-machines M_1 and M_2, as illustrated by the figure.
According to the terminology, in\_a and a\_2\_b are internal events of M_1, and b\_2\_c and out\_c are internal events of M_2. Concerning the variables, a and m are private variables of M_1, c and p are private variables of M_2, and b, r and s are shared variables.
The variables accessed by the internal events of M_1 are a, m, b, r and s. The events modifying these variables are in\_a, a\_2\_b, which both are internal events of M_1, and b\_2\_c, which is an internal event of M_2. Thus, according to the definition given above, b\_2\_c is an external event for M_1. In the same manner, a\_2\_b is an external event for M_2.

N.B.: Note that the expression "is an external event for" is an extrapolation, and shall be literally interpreted as "should lead to the construction of an external event in".

Example

It seems to be interesting to illustrate the decomposition step by step through an example. The considered example is described in the Event Model Decomposition.
The QuestionResponse.zip archive file contains the corresponding QuestionResponse Rodin project, and in particular the M machine taken as input for the decomposition. The QuestionResponse_i projects are issued from the decomposition and respectively contain the M_1, M_2 and M_3 sub-machines.

The events

The events of M are partitioned among M_1, M_2 and M_3, as illustrated below:

  • The prepare\_question event is an internal event of M_1.
  • The read\_question and write\_question events are internal events of M_2.
  • The produce\_response event is an internal event of M_3.

Example2.png

The variables

The status (private or shared) of the variables is given below:

Example variables.png
  • is a private variable of M_1.
  • is a private variable of M_3.
  • is a private variable of M_2.
  • is shared between M_1 and M_2.
  • is shared between M_2 and M_3.
  • is shared between M_1 and M_2.
  • is shared between M_1 and M_2.
  • is shared between M_2 and M_3.
  • is shared between M_2 and M_3.


The distribution of the variables follows:

  • The question, buffer\_1, bit\_11 and bit\_12 variables are copied in M_1.
  • The channel, buffer\_1, buffer\_2, bit\_11, bit\_12, bit\_21 and bit\_22 variables are copied in M_2.
  • The response, buffer\_2, bit\_21 and bit\_22 variables are copied in M_3.

The invariants

The defined invariants are copied:

Example invariants.png
  • is copied in M_1 and M_2.
  • is copied in M_1 and M_2.
  • is discarded, because it refers to an unknown variable (bool\_1).
  • is copied in M_2 and M_3.
  • is copied in M_2 and M_3.
  • is discarded, because it refers to an unknown variable (bool\_2).


The missing typing theorems are added. The typing information is extracted from the QuestionResponse.bcm file:

  • The question \in \pow (QUESTION) theorem is added to M_1 to type the question variable.
  • The buffer\_1 \in QUESTION theorem is added to M_1 to type the buffer\_1 variable.
  • The channel \in \pow (QUESTION) theorem is added to M_2 to type the channel variable.
  • The response \in \pow (RESPONSE) theorem is added to M_3 to type the response variable.
  • The buffer\_2 \in QUESTION theorem is added to M_3 to type the buffer\_2 variable.

The external events

External prepare question.png

prepare\_question is an event of M_1 modifying the bit\_11 and buffer\_1 shared variables.
These variables are accessed by the write\_question event of M_2.
An external event is therefore built from prepare\_question in M_2.
Since M_2 does not contain the question variable, a question parameter is created.
Moreover, a guard is added to type it. The QuestionResponse.bcm is parsed to retrieve this typing information.
The act1 action related to the question variable is discarded.
The act2 and act3 actions are kept.

In parallel, produce\_response is an event of M_3 modifying the bit\_22 shared variable. This variable is accessed by the read\_question event of M_2. As a consequence, an external event is built from produce\_response in M_2.

In the same manner, read\_question is an event of M_2 modifying the bit\_21 and buffer\_2 shared variables. These variables are accessed by the produce\_response event of M_3. As a consequence, an external event is built from read\_question in M_3.

Finally, write\_question is an event of M_2 modifying the bit\_12 shared variable. This variable is accessed by the prepare\_question event of M_1. As a consequence, an external event is built from write\_question in M_1.

The initialization events

The initialization events of the sub-machines are built from the initialization event of M, which is detailed below:
Example initialization.png
The initialization event of M_1 initializes the variables contained in this sub-machine: the assignments related to the question, buffer\_1, bit\_11 and bit\_12 variables are kept; the other assignments are discarded.
In the same manner, the initialization event of M_3 initializes the variables contained in this sub-machine: the assignments related to the response, buffer\_2, bit\_21 and bit\_22 are kept; the other assignments are discarded.
Finally, when building the initialization event of M_2, the assignments are all kept, except those corresponding to question and response.

The contexts

The contexts of the sub-machines are built from the context C0 associated to M:
Example contexts.png
For each sub-machine M_i, an empty context is created and a SEES clause identifying this context is added in M_i. Then, these contexts are filled:

  • M_1, M_2 and M_3 reference the QUESTION set. It is therefore copied in each context.
  • The RESPONSE set is only referenced by M_3. It is copied in the associated context.
  • The answer constant is only referenced by M_3. It is copied in the associated context.
  • The sets and constants referenced by the axm1 axiom have been previously copied in the context associated to M_3. As a consequence, it is copied in this context too.

To summarize, the context seen by M_1 and M_2 only contains the QUESTION set. The context seen by M_3 is equal to C0.

Implementation

A first plugin prototype is accessible under _exploratory/tshoang/ch.ethz.eventb.decomposition.

Bibliography