Difference between pages "Event Model Decomposition" and "Rodin 3.0 Plug-in Migration Guide"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
imported>Nicolas
 
Line 1: Line 1:
−
{{TOCright}}
+
Release 3.0 of the Rodin platform introduces important changes to the Rodin
 +
Platform API.  These changes make the core platform stronger and fix some
 +
erroneous design decisions that were taken in previous Rodin releases.
  
−
== Introduction ==
+
This guide details the actions that plug-in developers must take in order to
−
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.
+
port their plug-ins from the 2.8 API to the 3.0 API.
  
−
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.
+
== AST Library ==
  
−
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.
+
=== Type Environments ===
  
−
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.  
+
Type environments have changed in Rodin 3.0 in order to reinforce their good use and their robustness.
 +
One of these changes concerns their mutability state and has an important impact on type environments use.  
  
−
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 general principle is the following, if you want to create and build a type environment then you have to use an {{class|ITypeEnvironmentBuilder}} which is the only type providing methods that could modify the type environment. Then in some case you could need to guarantee that your type environment will not mutate anymore and make a snapshot of type {{class|ISealedTypeEnvironment}}.  
  
−
== Terminology ==
+
Let's consider that you dispose of a new type environment of type {{class|ITypeEnvironmentBuilder}}, in some cases you will need to provide it as a parameter and you will face 3 options depending on the parameter Java type:
−
This section introduces the definitions of the main technical terms, which are widely used in the sequel.
+
* It is an {{class|ISealedTypeEnvironment}}: you must provide an immutable snapshot of your type environment using method ''makeSnapshot()''.
 +
* It is an {{class|ITypeEnvironmentBuilder}}: here two choices are possible, you could give your object reference as parameter and it will be modified if a further treatment is made on it or you could give a copy of your object using method ''makeBuilder()'' to prevent side effect on your object.
 +
* It is an {{class|ITypeEnvrionment}}: it is a convenient way to have genericity since it is the super type of both preceding ones. You can opt for any options above. There is a convention that a parameter of type ITypeEnvironment is not modified by the callee, but this is not enforced. If you want a strong guarantee that the type environment that you pass cannot be modified, pass it as a sealed environment.
  
−
* 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.
+
Reciprocally, if you ask for a type environment as parameter, these 3 options are available:
−
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.
+
* Use an {{class|ISealedTypeEnvironment}}: if you want to provide a strong guarantee that you will not modify the parameter.
−
* Sub-machine: A machine built from a non-decomposed machine during the event model decomposition.
+
* Use an {{class|ITypeEnvrionmentBuilder}}: if you need to modify the received type environment by side effect
−
* Sub-context: A context built from a non-decomposed context during the event model decomposition.  
+
* Use an {{class|ITypeEnvrionment}}: in case you will not modify the type environment and allow the user to provide the most convenient type for him. You must not later cast the parameter to type {{class|ITypeEnvironmentBuilder}}.
−
* ''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 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).
+
Finally regarding return type of methods, you should use only one of the two following choices ({{class|ITypeEnvironment}} is discouraged since it provides no information about what is actually returned):
 +
* Return an {{class|ISealedTypeEnvironment}}: it guarantees that the type environment will not mutate and allow to share its reference as long as no modification is needed.
 +
* Return an {{class|ITypeEnvrionmentBuilder}}: it allows modifications and must be used in case no reference is kept on the object or if you want to share the modifications on it.
  
−
== High-level Specification ==
+
And the last case but not the least, if you create a type environment field you have also 2 options:
−
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.
+
* You should use an {{class|ISealedTypeEnvironment}} in one of these cases:
 +
** It is never modified or has an expected immutable behavior.
 +
** The type environment is built all at once and is never modified later.
 +
** You need to return a copy of it often (allows to share the reference) and modify it only rarely.
 +
* You should use an {{class|ITypeEnvironmentBuilder}} in one of these cases:
 +
** The field is only internal to the class (and has builder type at least one time).
 +
** The type environment is built to be returned externally and the reference can be shared.
  
−
=== Definition of the decomposition ===
+
Those precendent cases are only the most general examples that you will face and are made to give an idea of the new API good usage, but finally the developper is the only person that can decide of the better option to choose.
−
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.
+
=== Free Identifier Cache ===
  
−
<center>
+
Every instance of {{class|Formula}} contains a cache of the free identifiers
−
[[Image:Decomposition.png]]
+
occurring within the tree rooted at that node.  Since Rodin 3.0, the free
−
</center>
+
identifiers that correspond to the names of given types that occur in the
 +
formula tree are also added to the free identifier cache.  Consequently, the
 +
<tt>getFreeIdentifiers()</tt> method of class {{class|Formula}} now returns a
 +
larger list of free identifiers. You still can use method
 +
<tt>getSyntacticallyFreeIdentifiers()</tt> if you are not interested in the
 +
name of given types, at the price of a small performance penalty, because the
 +
latter method will traverse the whole formula tree.
  
−
=== <font id="config">Configuration of the decomposition</font> ===
+
=== Formula Factories ===
−
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 AST library now demands that all nodes and types of a formula have been
 +
built by the same formula factory.  It is no longer possible to mix nodes
 +
coming from different factories. Moreover, this modification made the notion
 +
of language versions obsolete: references to the <tt>LanguageVersion</tt>
 +
enumeration have been removed.<br> In most cases, e.g., in the sequent prover,
 +
this restriction is not important as all formulas are always in the same
 +
language and therefore built by the same factory.  If you are in a special
 +
case where you need to mix several formula factories, we have added the
 +
<tt>translate(FormulaFactory)</tt> to class {{class|Formula}} which allows to
 +
rebuild a full copy of a formula with a different formula factory.
  
−
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.
+
=== Datatype ===
  
−
<center>
+
==== Datatype Definition ====
−
[[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.
+
The definition of datatypes has completely changed to be simplest and more compact.
 +
A datatype must now be defined in a declarative way with a datatype builder. Here are the few steps necessary to declare a new datatype:
 +
* Retrieve a datatype builder {{class|IDatatypeBuilder}} provided by a {{class|FormulaFactory}} using <tt>makeDatatypeBuilder(String, GivenType[])</tt>. This step sets the datatype name and its type parameters (as given types).
 +
* Add a datatype constructor {{class|IConstructorBuilder}} on the builder using method <tt>addConstructor(String)</tt> which sets the constructor name.
 +
* Add the arguments of a constructor using <tt>addArgument(Type)</tt> (simple argument) or <tt>addArgument(String, Type)</tt> (destructor with a name). The argument type will be provided in the right format by using the <tt>parseType(String)</tt> method of the {{class|IDatatypeBuilder}}.
 +
* Once all constructors, and their arguments, were added:
 +
** Check that at least one basic constructor exists by using the <tt>hasBasicConstructor()</tt> method of the datatype builder
 +
** Finalize the datatype by using the <tt>finalizeDatatype()</tt> builder method which returns the finalized datatype {{class||IDatatype}}
  
−
=== Execution of the decomposition ===
+
As you can have noticed a constructor argument type is now represented with a standard event-B {{class|Type}} object.
−
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.
+
The type representation principle is the following:
 +
* A type parameter is always represented by the given type defined by the type parameter name (as provided to retrieve the dataype builder)
 +
* The datatype is represented by the given type defined by the datatype name
 +
But since the string representation of a datatype must contain its type parameters, the datatype builder provides the <tt>parseType(String)</tt> parser. It allows to transform the string representation into the type representation as soon as the datatype is represented with its type parameters correctly named and ordered. E.g.: For the datatype "DT" with the type parameters "X", "Y" and "Z", the string representation is "DT(X,Y,Z)" and the type representation is the given type "DT".
  
−
[[Image:Action.png]]
+
==== Datatype Use ====
  
−
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]].
+
The datatype interface {{class|IDatatype}} has also been simplified and some services have been moved in the new specialized extensions:
−
<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.
+
* {{class|ITypeConstructorExtension}} for the type constructor, it provides:
 +
** the type parameters names
 +
* {{class|IConstructorExtension}} for a constructor, it provides:
 +
** the constructor name
 +
** the constructor arguments as: destructor extensions, types, expressions
 +
* {{class|IDestructorExtension}} for a destructor, it provides:
 +
** the destructor name
 +
** the destructor type
 +
** the parent constructor
  
−
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).
+
Those new interfaces provide the way to identify easily the extensions of a datatype and their relationships, it avoids in many cases the use of the {{class|IDatatype}} object like it was the case before.
 +
Moreover the datatype interface now provides access to the datatype constructors and destructors giving their name instead of their identifier.
  
−
=== <font id="po">Generation of the proof obligations</font> ===
+
== Sequent Prover ==
−
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:
+
All constants, methods and classes that were marked as deprecated in the API have been removed. If you were using one of these, please read its Javadoc in Rodin 2.7 which describes an alternative implementation.
−
* 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 ==
+
=== New Action Rewrite Hypothesis ===
−
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.
+
Reasoners now can use a new type of action: IRewriteHypAction. It is equivalent to a Forward Inference Action followed by a Hide Action.
  
−
The following sequence shall be observed to decompose a machine <math>M</math> in sub-machines <math>M_1,...,M_n</math>:
+
The interface IForwardHypAction is still present, as well as the "HIDE" type of ISelectionHypAction. However, if your reasoner performs a forward hypothesis action directly followed by a "hide" action which hides the hypothesis used during the inference, then your reasoner indeed performs a rewrite action. We strongly encourage you to use IRewriteHypAction interface for such use.
−
# 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]]).
+
Indeed, it allows to define a strong relationship between the inference action and the hide action: during reuse, the hide action is performed only if the forward inference occurs.
−
# 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.
+
=== FormulaFactory ===
  
−
=== <font id="machine_decomposition">Decomposition of a machine in sub-machines</font> ===
+
Formula factories have been growing in importance since the mathematical extensions and the theory plug-in have been developed.
−
The purpose of this paragraph is to precisely describe how to decompose <math>M</math>.  
+
They are now found in many places, and in Rodin 3.0 they are even more present.
  
−
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>.  
+
A FormulaFactory instance is used to parse and make formulas in a given mathematical language.
 +
Proofs now bear their own formula factory, potentially different from the formula factories of the other proofs in the same file, hence the addition of ''IProofTree.getFormulaFactory()'' and ''IPRProof.getFormulaFactory()'' methods. You must be aware of that fact if you pass formula factory arguments in method calls, in order to use the right one.
  
−
==== About the variables ====
+
=== Context Dependent Reasoners ===
−
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.
+
The older notion of Signature Reasoner has been replaced by that of Context Dependent Reasoner.
 +
In org.eventb.core.seqprover.reasoners extension point, reasoners now have an optional ''contextDependent'' boolean. The proofs that use a context dependent reasoner will not be trusted merely based on their dependencies, but instead they will be replayed in order to update their status.
  
−
===== Defining a variable as shared =====
+
This applies in particular to '''Theory Plug-in reasoners''', that depend on the mathematical language and proof rules defined in theories, which change over time. Thus, these reasoners shall be declared as ''context dependent'' in Rodin 3.0.
−
The following DTD excerpt describes the structure of a variable in the Rodin database:
 
  
−
<!ENTITY % NameAttDecl "name CDATA #REQUIRED">
+
== Rodin Core Plug-ins ==
−
<!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 <tt>shared</tt> specific attribute, which would be set to <tt>true</tt> if and only if the variable is ''shared'':
+
=== Rodin Database structure enforcement ===
 +
==== A bit of background ====
 +
The contents of any file managed by the Rodin database are based on a hierarchical model, defined by item types (i.e. elements or attribute types) which the database handles and the relationships between them.<br />
 +
Historically, the sole definition of items was provided from the Rodin Core extension points <tt>org.rodinp.core.internalElementTypes</tt> and <tt>org.rodinp.core.attributeTypes</tt> to plug-in developers. The relationship definitions were then implicit and externally managed by the Event-B UI plug-in which defined <tt>org.eventb.ui.editorItems</tt> extension point to contribute to the Event-B Editor. Thus, the structure could be considered weak, as only editors were in charge of maintaining the file structure. In other terms, it was possible to get elements or attributes at wrong locations in the Rodin database provided that edition happened outside the Event-B Editor.<br />
  
−
<ENTITY % shared "org.eventb.core.shared CDATA #REQUIRED">
+
In Rodin 3.0, type relationships are enforced at database level, to ensure the structural coherence of any managed Rodin file in the Rodin database. In other terms, all elements which are present at some locations in the textual representation of the Rodin file (used for persistence), which however do not have sense in regard of the structural definitions on such a file, will be ignored by the Rodin database (but kept in the text file anyway).
−
+
Consequently, the way to define item type relationships is now provided to plug-in developers from the same level as the element type definition: the Rodin Core plug-in.
−
<!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:
+
==== Migration instructions ====
 +
If you do (or intend to) contribute model elements and attribute types to the Rodin database, you now have to define the relationships they can have between them, or with the core elements. The relationships are defined in a simple manner using parent-child(ren) relationship definitions.
 +
To define such permissions, you have to contribute to the new dedicated extension point <tt>org.rodinp.core.itemRelations</tt>. Please refer to the documentation of the extension point for further details on how to implement things.
  
−
<ENTITY % nature "org.eventb.core.nature CDATA #REQUIRED">
+
If your plug-in already contributes model element and attribute types, using contributions to <tt>org.eventb.ui.editorItems</tt>, a compatibility mechanism has been activated in order to integrate legacy relationships. However, it is not advised to rely on such compatibility mechanism.  
−
 
−
<!ATTLIST %variable;
 
−
  ...
 
−
  %nature; (0|1) #REQUIRED
 
−
  >
 
−
 
−
<!-- The nature attribute encodes the kind of variable:
 
−
      0: private variable
 
−
      1: shared variable
 
−
-->
 
  
−
The second option, which has the main advantage to be more scalable, is retained here.
+
''IMPORTANT:'' Moreover, the compatibility mechanism does not offer backward compatibility for elements which are contributed to the database but are not supposed to be edited from the Event-B editor.
  
−
===== Ensuring that a shared variable is not refined =====
+
=== Rodin keyboard core and UI separation ===
−
A ''shared'' variable shall always be present in the state space of any refinement of the component.
+
==== A bit of background ====
−
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_distribution">Distributing the variables in the sub-machines of the decomposition</font> =====
+
The Rodin keyboard translation capability lets keyboard key combinations entered by the end user be transformed into dedicated Unicode representations (e.g. the following string <tt>/<<:</tt> is translated to ⊄).
−
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.
+
Two kinds of translation mechanisms are provided :
 +
- a simple string translation mechanism: from a given string, it returns a string where all symbols are translated,
 +
- an Event-B UI text widgets adaptation mechanism: textual widgets can be adapted for "on-the-fly" symbol translation.
  
−
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:
+
Historically, only one plug-in has been defined to provide these two functionnalities : <tt>org.rodinp.keyboard</tt>.<br />
−
* 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>.
+
This was cumbersome for plug-ins developers wanting to use only the simple translation mechanism and had to manage unwanted plug-in dependencies.
−
* 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.
+
Indeed, a dependency on <tt>org.eventb.ui</tt> (and on which the second mechanism relies) was imposed to them.
  
−
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!).
+
==== Migration instructions ====
 +
In Rodin 3.0, the UI part and core parts of the translation capability have been separated into two different plug-ins: <tt>org.rodinp.keyboard.core</tt> and <tt>org.rodinp.keyboard.ui</tt>.<br />
 +
The migration actions you have to perform depends on what you need from the translation mechanism:
 +
* if your plug-in use the simple translation mechanism: you simply have to update your plug-in dependencies from <tt>org.rodinp.keyboard</tt> to <tt>org.rodinp.keyboard.core</tt>, and fix corresponding imports in your code.
 +
* if your plug-in defines UI widgets that need to be adapted: you simply have to update your plug-in dependencies from <tt>org.rodinp.keyboard</tt> to <tt>org.rodinp.keyboard.ui</tt>, and fix corresponding imports in your code.
  
−
===== Propagating the sharing status =====
+
== Event-B Core Plug-in ==
−
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 ====
+
All constants, methods and classes that were marked as deprecated in the API have been removed. If you were using one of these, please read its Javadoc in Rodin 2.7 which describes an alternative implementation.
−
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).
+
== Event-B PP and PP Trans Plug-ins ==
  
−
===== <font id="evt_partition">Partitioning the events in the sub-machines of the decomposition</font> =====
+
Methods that were marked as deprecated in the API have been removed.
−
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> =====
+
== Event-B UI Plug-in ==
−
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.
+
There isn't any change from Event-B UI Plug-in which impacts its downstream plug-ins.
  
−
An event tagged as ''external'' in the non-decomposed machine (when resulting from a previous decomposition) shall remain ''external'' in the sub-machine.
+
== Rodin Keyboard Plug-ins ==
 +
The translation of mathematical symbols has been refactored to avoid a dependency on the Event-B UI plug-in: there is now a separation between symbol translation and translation which occurs in graphical components.<br>
 +
The plug-in <tt>org.rodinp.keyboard</tt> is now split into two plug-ins :
 +
* org.rodinp.keyboard.core : this plug-in contains the core translation utilities that one can access through the  following method <tt>org.rodinp.keyboard.core.RodinKeyboardCore.translate(String)</tt>,
 +
* org.rodinp.keyboard.ui : this plug-in contains the UI translation capabilties that where previously available from <tt>org.rodinp.keyboard</tt>.
  
−
===== Identifying an event as external =====
+
[[Category:Developer documentation]]
−
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.
+
[[Category:Rodin Platform]]
−
 
 
−
<!ENTITY % convergence "org.eventb.core.convergence">
 
−
 
−
<!ATTLIST %event;
 
−
  ...
 
−
  %convergence; (0|1|2) #REQUIRED
 
−
  ...
 
−
  >
 
−
  <!--
 
−
    The convergence attribute specifies which PO should be generated
 
−
    for the combination event / variant:
 
−
      0: ordinary event, no PO
 
−
      1: convergent event, PO to show event decreases variant
 
−
      2: anticipated event, PO to show event doesn't increase variant
 
−
  -->
 
−
 
 
−
Another solution would be to add a distinct <tt>external</tt> attribute, which would be set to <tt>true</tt> 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 <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> =====
 
−
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>
 
−
 
 
−
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>
 
−
<br>We first focus on the generic construction of an ''external'' event from an ''internal'' event whose action is expressed as follows:
 
−
 
 
−
  e
 
−
  '''WHERE'''
 
−
    <math>G(v_1,...,v_n,s_1,...,s_m)~</math>     
 
−
  '''THEN'''                 
 
−
    <math>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')</math>
 
−
 
 
−
<ol>
 
−
<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
 
−
  '''ANY''' <math>x_1,...,x_n~</math>
 
−
  '''WHERE'''
 
−
    <math>G(x_1,...,x_n,s_1,...,s_m)~</math>     
 
−
  '''THEN'''                 
 
−
    <math>x_1,...,x_n,s_1,...,s_m \bcmsuch P(x1,...,x_n,s_1,...,s_m, x_1',...,x_n',s_1',...,s_m')</math>
 
−
 
 
−
<li>The second step consists in adding guards to define the types of the parameters, if necessary. More precisely, a theorem shall be added for each parameter for which typing is required. The <tt>.bcm</tt> file associated to the non-decomposed machine shall be parsed in order to retrieve the typing information.
 
−
 
 
−
<li>The third and last step of the construction consists in introducing an existential quantifier to resolve the invalid assignment. <math>external\_e</math> is the newly built external event.</li>
 
−
 
 
−
  external_e
 
−
  '''ANY''' <math>x_1,...,x_n~</math>
 
−
  '''WHERE'''
 
−
    <math>G(x_1,...,x_n,s_1,...,s_m)~</math>     
 
−
  '''THEN'''                 
 
−
    <math>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')</math>
 
−
</ol>
 
−
 
 
−
<u>Derived constructions</u>
 
−
<br>Then, it is possible to derive the construction for other actions:
 
−
# Each assignment of the action shall be handled separately (see [[Rewriting_rules_for_event_model_decomposition#separately|transformation rules]] on Event-B actions).
 
−
# The [[Rewriting_rules_for_event_model_decomposition#transf_rules|transformation rules]] shall be applied on each Event-B assignment.
 
−
 
 
−
<u>Example</u>
 
−
 
 
−
  e
 
−
  '''WHERE'''
 
−
    <math>G(v_1,...,v_n,s_1,...,s_m)~</math>     
 
−
  '''THEN'''                 
 
−
    <math>\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}</math>
 
−
 
 
−
  external_e
 
−
  '''ANY''' <math>x_1,...,x_n~</math>
 
−
  '''WHERE'''
 
−
    <math>G(x_1,...,x_n,s_1,...,s_m)~</math>     
 
−
  '''THEN'''                 
 
−
    <math>\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}</math>
 
−
 
 
−
===== <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.
 
−
 
 
−
  initialization   
 
−
  '''THEN'''                 
 
−
    <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:
 
−
 
 
−
  e 
 
−
  '''THEN'''                 
 
−
    <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.
 
−
 
 
−
===== Ensuring that a shared variable is not refined by an initialization event =====
 
−
If <math>M_{i}'</math> refines a sub-machine <math>M_i</math> issued from the decomposition of a machine <math>M</math>, the initialization event of <math>M_{i}'</math> shall not constrain a ''shared'' variable more or less than it was in the initialization event of <math>M_i</math>.
 
−
 
 
−
An initialization event shall not contain an action modifying at the same time a ''shared'' variable and a ''private'' variable (''eg.'' <math>a,b \bcmsuch P(a',b')</math>, where <math>a</math> is ''private'' and <math>b</math> is ''shared''). If such a behavior was authorized, a two-way simulation proof obligation would indeed be necessary to ensure that the ''shared'' variable is not constrained differently in further refinements. As a consequence, the decomposition of <math>M</math> shall be forbidden if its initialization event contain such an action. Moreover, the static checker shall ensure that the initialization event of <math>M_{i}'</math> does not contain such an action.
 
−
 
 
−
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>
 
−
[[Image:Invariants.png]]
 
−
</center>
 
−
 
 
−
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_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>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 ====
 
−
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> ===
 
−
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 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.
 
−
 
 
−
<center>
 
−
[[Image:Flattening_contexts.png]]
 
−
</center>
 
−
 
 
−
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 ====
 
−
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 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 [[#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).
 
−
 
 
−
== 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 <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 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>
 
−
<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>.
 
−
* The access of a variable by a given event (according to the static-checker) can be expressed as:
 
−
<math>\mathit{access}\in\mathit{EVENT}\rel\mathit{VAR}</math>
 
−
<br>For a given variable <math>v</math>, <math>(partition;access^{-1})[\{v\}]~</math> is then the set of the sub-machines accessing <math>v</math>, and <math>v</math> is a ''private'' variable of a sub-machine <math>m</math> if and only if this set contains a single component (''i.e.'' <math>card((partition;access^{-1})[\{v\}]) = 1~</math>); otherwise, and if and only if this set is not empty, <math>v</math> is ''shared''.
 
−
<br>In parallel, for a given sub-machine <math>m</math>, <math>(access;partition^{-1})[\{m\}]~</math> is the set of variables accessed by the events contained in <math>m</math>.
 
−
* The association of a variable with the events modifying this variable (according to the static-checker) can be specified as:
 
−
<math>\mathit{modify}\in\mathit{VAR}\rel\mathit{EVENT}</math>
 
−
<br>For a given sub-machine <math>m</math> and a variable <math>v \in (access;partition^{-1})[\{m\}]</math>, <math>modify[\{v\}]~</math> is then the set of the events modifying <math>v</math>.
 
−
* The construction of the ''external'' events for a sub-machine can be represented with a relation:
 
−
<math>\mathit{extern}\in\mathit{MACHINE}\rel\mathit{EVENT}</math>
 
−
<br>It is computed as follows: <math>extern = (modify;access;partition^{-1}) \setminus partition^{-1}</math>
 
−
<br>Thus, the ''external'' events of a given sub-machine <math>m</math> are events modifying the variables accessed by the ''internal'' events of <math>m</math>, but they are not ''internal'' events of <math>m</math>.
 
−
 
 
−
=== Example ===
 
−
The following example is taken from the [[#ancre_1|Event Model Decomposition]].
 
−
 
 
−
<center>
 
−
[[Image:Example.png]]
 
−
</center>
 
−
 
 
−
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>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>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".
 
−
 
 
−
== 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 ==
 
−
* 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 [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">[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">[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]]
 

Revision as of 18:23, 14 January 2014

Release 3.0 of the Rodin platform introduces important changes to the Rodin Platform API. These changes make the core platform stronger and fix some erroneous design decisions that were taken in previous Rodin releases.

This guide details the actions that plug-in developers must take in order to port their plug-ins from the 2.8 API to the 3.0 API.

AST Library

Type Environments

Type environments have changed in Rodin 3.0 in order to reinforce their good use and their robustness. One of these changes concerns their mutability state and has an important impact on type environments use.

The general principle is the following, if you want to create and build a type environment then you have to use an ITypeEnvironmentBuilder which is the only type providing methods that could modify the type environment. Then in some case you could need to guarantee that your type environment will not mutate anymore and make a snapshot of type ISealedTypeEnvironment.

Let's consider that you dispose of a new type environment of type ITypeEnvironmentBuilder, in some cases you will need to provide it as a parameter and you will face 3 options depending on the parameter Java type:

  • It is an ISealedTypeEnvironment: you must provide an immutable snapshot of your type environment using method makeSnapshot().
  • It is an ITypeEnvironmentBuilder: here two choices are possible, you could give your object reference as parameter and it will be modified if a further treatment is made on it or you could give a copy of your object using method makeBuilder() to prevent side effect on your object.
  • It is an ITypeEnvrionment: it is a convenient way to have genericity since it is the super type of both preceding ones. You can opt for any options above. There is a convention that a parameter of type ITypeEnvironment is not modified by the callee, but this is not enforced. If you want a strong guarantee that the type environment that you pass cannot be modified, pass it as a sealed environment.

Reciprocally, if you ask for a type environment as parameter, these 3 options are available:

  • Use an ISealedTypeEnvironment: if you want to provide a strong guarantee that you will not modify the parameter.
  • Use an ITypeEnvrionmentBuilder: if you need to modify the received type environment by side effect
  • Use an ITypeEnvrionment: in case you will not modify the type environment and allow the user to provide the most convenient type for him. You must not later cast the parameter to type ITypeEnvironmentBuilder.

Finally regarding return type of methods, you should use only one of the two following choices (ITypeEnvironment is discouraged since it provides no information about what is actually returned):

  • Return an ISealedTypeEnvironment: it guarantees that the type environment will not mutate and allow to share its reference as long as no modification is needed.
  • Return an ITypeEnvrionmentBuilder: it allows modifications and must be used in case no reference is kept on the object or if you want to share the modifications on it.

And the last case but not the least, if you create a type environment field you have also 2 options:

  • You should use an ISealedTypeEnvironment in one of these cases:
    • It is never modified or has an expected immutable behavior.
    • The type environment is built all at once and is never modified later.
    • You need to return a copy of it often (allows to share the reference) and modify it only rarely.
  • You should use an ITypeEnvironmentBuilder in one of these cases:
    • The field is only internal to the class (and has builder type at least one time).
    • The type environment is built to be returned externally and the reference can be shared.

Those precendent cases are only the most general examples that you will face and are made to give an idea of the new API good usage, but finally the developper is the only person that can decide of the better option to choose.

Free Identifier Cache

Every instance of Formula contains a cache of the free identifiers occurring within the tree rooted at that node. Since Rodin 3.0, the free identifiers that correspond to the names of given types that occur in the formula tree are also added to the free identifier cache. Consequently, the getFreeIdentifiers() method of class Formula now returns a larger list of free identifiers. You still can use method getSyntacticallyFreeIdentifiers() if you are not interested in the name of given types, at the price of a small performance penalty, because the latter method will traverse the whole formula tree.

Formula Factories

The AST library now demands that all nodes and types of a formula have been built by the same formula factory. It is no longer possible to mix nodes coming from different factories. Moreover, this modification made the notion of language versions obsolete: references to the LanguageVersion enumeration have been removed.
In most cases, e.g., in the sequent prover, this restriction is not important as all formulas are always in the same language and therefore built by the same factory. If you are in a special case where you need to mix several formula factories, we have added the translate(FormulaFactory) to class Formula which allows to rebuild a full copy of a formula with a different formula factory.

Datatype

Datatype Definition

The definition of datatypes has completely changed to be simplest and more compact. A datatype must now be defined in a declarative way with a datatype builder. Here are the few steps necessary to declare a new datatype:

  • Retrieve a datatype builder IDatatypeBuilder provided by a FormulaFactory using makeDatatypeBuilder(String, GivenType[]). This step sets the datatype name and its type parameters (as given types).
  • Add a datatype constructor IConstructorBuilder on the builder using method addConstructor(String) which sets the constructor name.
  • Add the arguments of a constructor using addArgument(Type) (simple argument) or addArgument(String, Type) (destructor with a name). The argument type will be provided in the right format by using the parseType(String) method of the IDatatypeBuilder.
  • Once all constructors, and their arguments, were added:
    • Check that at least one basic constructor exists by using the hasBasicConstructor() method of the datatype builder
    • Finalize the datatype by using the finalizeDatatype() builder method which returns the finalized datatype

As you can have noticed a constructor argument type is now represented with a standard event-B Type object. The type representation principle is the following:

  • A type parameter is always represented by the given type defined by the type parameter name (as provided to retrieve the dataype builder)
  • The datatype is represented by the given type defined by the datatype name

But since the string representation of a datatype must contain its type parameters, the datatype builder provides the parseType(String) parser. It allows to transform the string representation into the type representation as soon as the datatype is represented with its type parameters correctly named and ordered. E.g.: For the datatype "DT" with the type parameters "X", "Y" and "Z", the string representation is "DT(X,Y,Z)" and the type representation is the given type "DT".

Datatype Use

The datatype interface IDatatype has also been simplified and some services have been moved in the new specialized extensions:

  • ITypeConstructorExtension for the type constructor, it provides:
    • the type parameters names
  • IConstructorExtension for a constructor, it provides:
    • the constructor name
    • the constructor arguments as: destructor extensions, types, expressions
  • IDestructorExtension for a destructor, it provides:
    • the destructor name
    • the destructor type
    • the parent constructor

Those new interfaces provide the way to identify easily the extensions of a datatype and their relationships, it avoids in many cases the use of the IDatatype object like it was the case before. Moreover the datatype interface now provides access to the datatype constructors and destructors giving their name instead of their identifier.

Sequent Prover

All constants, methods and classes that were marked as deprecated in the API have been removed. If you were using one of these, please read its Javadoc in Rodin 2.7 which describes an alternative implementation.

New Action Rewrite Hypothesis

Reasoners now can use a new type of action: IRewriteHypAction. It is equivalent to a Forward Inference Action followed by a Hide Action.

The interface IForwardHypAction is still present, as well as the "HIDE" type of ISelectionHypAction. However, if your reasoner performs a forward hypothesis action directly followed by a "hide" action which hides the hypothesis used during the inference, then your reasoner indeed performs a rewrite action. We strongly encourage you to use IRewriteHypAction interface for such use. Indeed, it allows to define a strong relationship between the inference action and the hide action: during reuse, the hide action is performed only if the forward inference occurs.

FormulaFactory

Formula factories have been growing in importance since the mathematical extensions and the theory plug-in have been developed. They are now found in many places, and in Rodin 3.0 they are even more present.

A FormulaFactory instance is used to parse and make formulas in a given mathematical language. Proofs now bear their own formula factory, potentially different from the formula factories of the other proofs in the same file, hence the addition of IProofTree.getFormulaFactory() and IPRProof.getFormulaFactory() methods. You must be aware of that fact if you pass formula factory arguments in method calls, in order to use the right one.

Context Dependent Reasoners

The older notion of Signature Reasoner has been replaced by that of Context Dependent Reasoner. In org.eventb.core.seqprover.reasoners extension point, reasoners now have an optional contextDependent boolean. The proofs that use a context dependent reasoner will not be trusted merely based on their dependencies, but instead they will be replayed in order to update their status.

This applies in particular to Theory Plug-in reasoners, that depend on the mathematical language and proof rules defined in theories, which change over time. Thus, these reasoners shall be declared as context dependent in Rodin 3.0.

Rodin Core Plug-ins

Rodin Database structure enforcement

A bit of background

The contents of any file managed by the Rodin database are based on a hierarchical model, defined by item types (i.e. elements or attribute types) which the database handles and the relationships between them.
Historically, the sole definition of items was provided from the Rodin Core extension points org.rodinp.core.internalElementTypes and org.rodinp.core.attributeTypes to plug-in developers. The relationship definitions were then implicit and externally managed by the Event-B UI plug-in which defined org.eventb.ui.editorItems extension point to contribute to the Event-B Editor. Thus, the structure could be considered weak, as only editors were in charge of maintaining the file structure. In other terms, it was possible to get elements or attributes at wrong locations in the Rodin database provided that edition happened outside the Event-B Editor.

In Rodin 3.0, type relationships are enforced at database level, to ensure the structural coherence of any managed Rodin file in the Rodin database. In other terms, all elements which are present at some locations in the textual representation of the Rodin file (used for persistence), which however do not have sense in regard of the structural definitions on such a file, will be ignored by the Rodin database (but kept in the text file anyway). Consequently, the way to define item type relationships is now provided to plug-in developers from the same level as the element type definition: the Rodin Core plug-in.

Migration instructions

If you do (or intend to) contribute model elements and attribute types to the Rodin database, you now have to define the relationships they can have between them, or with the core elements. The relationships are defined in a simple manner using parent-child(ren) relationship definitions. To define such permissions, you have to contribute to the new dedicated extension point org.rodinp.core.itemRelations. Please refer to the documentation of the extension point for further details on how to implement things.

If your plug-in already contributes model element and attribute types, using contributions to org.eventb.ui.editorItems, a compatibility mechanism has been activated in order to integrate legacy relationships. However, it is not advised to rely on such compatibility mechanism.

IMPORTANT: Moreover, the compatibility mechanism does not offer backward compatibility for elements which are contributed to the database but are not supposed to be edited from the Event-B editor.

Rodin keyboard core and UI separation

A bit of background

The Rodin keyboard translation capability lets keyboard key combinations entered by the end user be transformed into dedicated Unicode representations (e.g. the following string /<<: is translated to ⊄). Two kinds of translation mechanisms are provided : - a simple string translation mechanism: from a given string, it returns a string where all symbols are translated, - an Event-B UI text widgets adaptation mechanism: textual widgets can be adapted for "on-the-fly" symbol translation.

Historically, only one plug-in has been defined to provide these two functionnalities : org.rodinp.keyboard.
This was cumbersome for plug-ins developers wanting to use only the simple translation mechanism and had to manage unwanted plug-in dependencies. Indeed, a dependency on org.eventb.ui (and on which the second mechanism relies) was imposed to them.

Migration instructions

In Rodin 3.0, the UI part and core parts of the translation capability have been separated into two different plug-ins: org.rodinp.keyboard.core and org.rodinp.keyboard.ui.
The migration actions you have to perform depends on what you need from the translation mechanism:

  • if your plug-in use the simple translation mechanism: you simply have to update your plug-in dependencies from org.rodinp.keyboard to org.rodinp.keyboard.core, and fix corresponding imports in your code.
  • if your plug-in defines UI widgets that need to be adapted: you simply have to update your plug-in dependencies from org.rodinp.keyboard to org.rodinp.keyboard.ui, and fix corresponding imports in your code.

Event-B Core Plug-in

All constants, methods and classes that were marked as deprecated in the API have been removed. If you were using one of these, please read its Javadoc in Rodin 2.7 which describes an alternative implementation.

Event-B PP and PP Trans Plug-ins

Methods that were marked as deprecated in the API have been removed.

Event-B UI Plug-in

There isn't any change from Event-B UI Plug-in which impacts its downstream plug-ins.

Rodin Keyboard Plug-ins

The translation of mathematical symbols has been refactored to avoid a dependency on the Event-B UI plug-in: there is now a separation between symbol translation and translation which occurs in graphical components.
The plug-in org.rodinp.keyboard is now split into two plug-ins :

  • org.rodinp.keyboard.core : this plug-in contains the core translation utilities that one can access through the following method org.rodinp.keyboard.core.RodinKeyboardCore.translate(String),
  • org.rodinp.keyboard.ui : this plug-in contains the UI translation capabilties that where previously available from org.rodinp.keyboard.
Retrieved from ‘https://wiki.event-b.org/index.php?title=Event_Model_Decomposition&oldid=6992’