Difference between pages "Event Model Decomposition" and "Index Query"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
imported>Laurent
m
 
Line 1: Line 1:
−
{{TOCright}}
+
==Purpose==
  
−
== Introduction ==
+
The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences allows for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.
−
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.
 
  
−
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.
+
==Performing queries==
  
−
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 indexer contents are not directly accessible to other plug-ins. Queries are sent through a {{class|IIndexQuery}} object provided by the RodinCore plug-in.
  
−
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.
+
===What to query ?===
  
−
Other [[#ancre_2|decomposition structures for Event-B]] are not considered here.
+
Two types of information can be queried:
 +
* declarations ({{class|IDeclaration}})
 +
* occurrences ({{class|IOccurrence}})
  
−
== Terminology ==
+
A declaration is the unique identifier of an entity in the index repository.
 +
It consists in a handle of the declared element itself plus its user-defined name.
 +
Every occurrence refers to one single declaration.
  
−
* Event model decomposition: The decomposition of a model, as defined in [[Machines_and_Contexts_(Modelling_Language)|the modelling language]], in sub-models.
+
Several query types can be performed, depending on the starting point:
−
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.
+
* getting the declaration of a given element (as {{class|IInternalElement}})
−
[[Image:Models.png]]
+
* getting the declarations of elements that match a given user-defined name (as {{class|String}}) in a given file
−
* Sub-machine: A machine built from a non-decomposed machine during the event model decomposition.
+
* getting the declarations of elements that occur, or could occur, in a given file
−
* Sub-context: A context built from a non-decomposed context during the event model decomposition.
+
* getting occurrences of a given declaration (this declaration having been retrieved from a previous query)
−
* ''Shared'' variable: A variable of a given machine which is accessed by events distributed in distinct sub-machines (by opposition to ''private'' variable).
+
* getting occurrences of a given declaration using propagation (see [[#Propagation|Propagation]] hereafter )
−
* ''Private'' variable: A variable of a given machine which is only accessed by events of the same 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).
+
Thus, a declaration is the key to retrieve occurrences.
  
−
== Low-level Specification ==
+
As the result might be too coarse, queries can be filtered out using various criterias (see {{class|IIndexQuery}} interface for more details).
−
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.
 
  
−
=== Decomposition of a machine in sub-machines ===
+
===Occurrences===
−
The purpose of this paragraph is to specify how to decompose a machine in sub-machines.
 
  
−
<font color="red">What about the <math>EXTENDS</math> clause and the hierarchy of machines? Is it necessary to flatten this hierarchy?</font>
+
An occurrence ({{class|IOccurrence}}) describes a location ({{class|IRodinLocation}}) and a kind of occurrence ({{class|IOccurrenceKind}}) of an element (referred to through its {{class|IDeclaration}}).
 +
For example, in Event-B, an occurrence could be:
  
−
==== About the variables ====
+
; location: in {{class|IAxiom}} 'a' (handle), in the PREDICATE_ATTRIBUTE, between characters 7 and 12
−
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.
+
; kind: REFERENCE
 +
; declaration: the {{class|ICarrierSet}} 's' (handle), named "set1"
  
−
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.
+
Occurrence kinds are contributed by indexers, no kinds are defined at the indexing system level.
 +
See more in [[Event-B Indexers]].
  
−
===== Defining a variable as shared =====
+
===Propagation===
−
The following DTD excerpt describes the structure of a variable in the Rodin database:
 
  
−
<pre>
+
Propagation is a way to get occurrences of several declarations, starting from one single declaration. In particular, it addresses cases where various declarations represent the same entity. The problem is that each declaration has separate occurrences. The propagation mechanism allows to get all occurrences of the entity, whatever the underlying declaration.  
−
<!ENTITY % NameAttDecl "name CDATA #REQUIRED">
 
−
<!ENTITY % CommentAttDecl "org.eventb.core.comment CDATA #IMPLIED">
 
−
<!ENTITY % IdentAttDecl "org.eventb.core.identifier CDATA #REQUIRED">
 
  
−
<!ELEMENT %variable; EMPTY>
+
For example, in Event-B, a variable can be redeclared in a refining machine. In the index repository, each variable has a separate declaration and separate occurrences. However, it might be interesting in some cases to consider occurrences of the concrete variable as a subset of occurrences of the abstract one. The concept here is to 'propagate' the query about the abstract variable to occurrences of the concrete one. This is achievable in this case thanks to event-B propagators.
−
<!ATTLIST %variable;
 
−
  %NameAttDecl;
 
−
  %CommentAttDecl;
 
−
  %IdentAttDecl;
 
−
  >
 
−
</pre>
 
  
−
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'':
+
See more in [[Event-B Indexers#Propagation|Event-B Indexers Propagation]].
  
−
<pre>
+
===Getting a valid result===
−
<ENTITY % shared "org.eventb.core.shared CDATA #REQUIRED">
 
  
−
<!ELEMENT %variable; EMPTY>
+
The indexing system data is constantly evolving, as long as files get modified. Furthermore, as indexing is performed as a background operation, one cannot guess whether the indexing has completed or not. The system may also be updating its data, making it temporarily incoherent. Thus, the problem arises to ensure that the data is valid and up-to-date.
−
<!ATTLIST %variable;
 
−
  ...
 
−
  %shared; (false|true) #REQUIRED
 
−
>
 
−
</pre>
 
  
−
Another possibility would be to define a more generic attribute, which could take different values, according to the nature of the variable:
+
To that end, a method is provided by the {{class|IIndexQuery}}, that blocks the current thread until all planned files are indexed. Requests performed after that will thus return a valid result and benefit from the most up-to-date version of the data.
  
−
<pre>
+
==Query Examples==
−
<ENTITY % nature "org.eventb.core.nature CDATA #REQUIRED">
 
  
−
<!ATTLIST %variable;
+
Here are a few examples of index queries. They are all implicitly preceded by the following code
−
  ...
 
−
  %nature; (0|1) #REQUIRED
 
−
>
 
  
−
<!-- The nature attribute encodes the kind of variable:
+
  final IIndexQuery query = RodinCore.makeIndexQuery();
−
      0: private variable
+
  query.waitUpToDate();
−
      1: shared variable
 
−
-->
 
−
</pre>
 
  
−
The second option, which has the main advantage to be more scalable, is retained here.
+
that creates the query object and waits until the index becomes up-to-date.
  
−
===== Ensuring that a shared variable is not data-refined =====
+
===Occurrences of an element===
−
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.
 
  
−
===== <font id="var_partition">Partitioning the variables in the sub-machines of the decomposition</font> =====
+
Input Data:
−
It is assumed in this section that the events have been previously partitioned among sub-machines.
+
* a handle 'var' of an IVariable
  
−
The following cases have to be taken into consideration when dealing with the variable distribution:
+
To get its declaration
−
* 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 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 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).
+
final IDeclaration declVar = query.getDeclaration(var);
  
−
==== About the events ====
+
Remember to check for a null return value.
−
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).
+
From that declaration, the user-defined name of the variable can be retrieved
  
−
===== Identifying an event as external =====
+
final String userDefinedName = declVar.getName();
−
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.
 
  
−
<pre>
+
To get the occurrences of 'var'
−
<!ENTITY % convergence "org.eventb.core.convergence">
 
  
−
<!ATTLIST %event;
+
final Set<IOccurrence> occurrences = query.getOccurrences(declVar);
−
  ...
 
−
  %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
 
−
  -->
 
−
</pre>
 
  
−
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'':
+
===Homonyms in a file===
  
−
<pre>
+
Input Data:
−
<ENTITY % external "org.eventb.core.external CDATA #REQUIRED">
+
* a handle 'file' of an {{class|IRodinFile}}
 +
* a name "foo"
  
−
<!ATTLIST %event;
+
Goal:
−
  ...
+
getting declarations of all elements named "foo" that occur in 'file'
−
  %external; (false|true) #REQUIRED
 
−
>
 
−
</pre>
 
  
−
This solution is preferred because the notion of ''external'' event is totally orthogonal to the notion of convergence.
+
First, all declarations of all indexed elements that occur in 'file' are retrieved.
 +
Then a query filter on the name is used.
  
−
===== <font id="build_external">Constructing an external event</font> =====
+
final Set<IDeclaration> declarations = query.getDeclarations(file);
−
An ''external'' event shall be built for each event of the non-decomposed machine modifying ''shared'' variables.
+
query.filterName(declarations, "foo");
  
−
As explained in [[Actions_(Modelling_Language)|the modelling language]], a non-deterministic action expressed as a variable identifier, followed by <math>\bcmin</math>, followed by a set expression, can always be translated to a non-deterministic action made of a list of distinct variable identifiers, followed by <math>\bcmsuch</math>, followed by a before-after predicate.  
+
At the end, 'declarations' contains the declarations of all elements named "foo" occurring in 'file'.
  
−
In the same manner, a deterministic action can always be translated to a non-deterministic action, as shown in the following example. Let's consider a machine with variables <math>x</math>, and <math>y</math>. Here is an action:
+
===Parameters of an event===
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math>x \bcmeq y</math> is the same as <math>x \bcmsuch\ x' = y</math>
 
−
|}
 
−
</center>
 
  
−
As a consequence, we will first focus on the construction of an ''external'' event from an event of a sub-machine <math>M</math> whose action relies on <math>\bcmsuch</math>, and then derivate the construction from an event of <math>M</math> whose action relies on <math>\bcmeq</math> or <math>\bcmin</math>.
+
Input Data:
−
<br>
+
* a handle 'file' of an {{class|IRodinFile}}
−
<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>.
+
* a handle 'evt1' of an {{class|IEvent}}
  
−
'''Generic construction for <math>\bcmsuch</math>'''
+
Goal:
 +
getting the declarations of all parameters of 'evt1'
  
−
  e
+
<pre>
−
  '''WHERE'''
+
final Set<IDeclaration> declarations = query.getDeclarations(file);
−
    <math>G(v_1,...,v_n,s_1,...,s_m)~</math>     
+
query.filterType(declarations, IParameter.ELEMENT_TYPE);
−
  '''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>
 
  
−
The first step of the construction is to replace the ''private'' variables by parameters. Note that this step is purely fictive, because assigning an event parameter is not allowed!
+
final Set<IOccurrence> occurrences = query.getOccurrences(declarations);
 +
query.filterKind(occurrences, EventBPlugin.DECLARATION);
  
−
  e
+
final IInternalLocation evt1Location = RodinCore.getInternalLocation(evt1);
−
  '''ANY''' <math>x_1,...,x_n~</math>
+
query.filterLocation(occurrences, evt1Location);
−
  '''WHERE'''
 
−
    <math>G(x_1,...,x_n,s_1,...,s_m)~</math>     
 
−
  '''THEN'''                 
 
−
    <math>v_1,...,v_n,s_1,...,s_m \bcmsuch P(x1,...,x_n,s_1,...,s_m, x_1',...,x_n',s_1',...,s_m')</math>
 
  
−
The second step consists of 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.
+
final Set<IDeclaration> paramsOfEvt1 = query.getDeclarations(occurrences);
−
<font color="red">TODO: Some precisions and examples should be added here</font>.
+
</pre>
  
−
The third and last step of the construction is to introduce an existential quantifier to resolve the invalid assignment. <math>external\_e</math> is the newly built external event.
+
We first get all declarations of elements that occur in 'file', and we filter them so as to keep only declarations of parameters.
  
−
  external_e
+
We then get all occurrences of those parameters. We want parameters that have a DECLARATION occurrence in 'evt1'. To that aim, two filters are successively applied to the occurrences.
−
  '''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.P(x1,...,x_n,s_1,...,s_m, y_1,...,y_n,s_1',...,s_m')</math>
 
  
−
'''Derived construction for <math>\bcmsuch</math>'''
+
Finally we get the declarations ({{class|IDeclaration}}) associated with the filtered occurrences.
  
−
  e
+
===Query with propagation===
−
  '''WHERE'''
 
−
    <math>G(v_1,...,v_n,s_1,...,s_m)~</math>     
 
−
  '''THEN'''                 
 
−
    <math>v_1 \bcmsuch P_1(v_1,...,v_n,s_1,...,s_m,v_1')</math>
 
−
    ...
 
−
    <math>v_n \bcmsuch P_n(v_1,...,v_n,s_1,...,s_m,v_n')</math>
 
−
    <math>s_1 \bcmsuch P_{n+1}(v_1,...,v_n,s_1,...,s_m,s_1')</math>
 
−
    ...
 
−
    <math>s_m \bcmsuch P_{n+m}(v_1,...,v_n,s_1,...,s_m,s_m')</math>
 
  
−
It may alternatively be represented with a single predicate, which is an intersection of the P_1,...,P_{n+m} predicates:
+
Input Data:
 +
* a handle 'var' to a {{class|IVariable}}
  
−
  e
+
Goal:
−
  '''WHERE'''
+
getting all occurrences of 'var' including occurrences in machines that redeclare 'var'.
−
    <math>G(v_1,...,v_n,s_1,...,s_m)~</math>     
 
−
  '''THEN'''                 
 
−
    <math>v_1,...,v_n,s_1,...,s_m \bcmsuch P_1(v1,...,v_n,s_1,...,s_m,v_1') \land ... \land P_n(v_1,...,v_n,s_1,...,s_m,v_n') \land P_{n+1}(v_1,...,v_n,s_1,...,s_m,s_1') \land ... \land P_{n+m}(v_1,...,v_n,s_1,...,s_m,s_m') </math>
 
−
 
 
−
It is then possible to build the external event, by following the same steps of construction than for the generic case:
 
  
−
  external_e
+
<pre>
−
  '''ANY''' <math>x_1,...,x_n~</math>
+
final IDeclaration declaration = query.getDeclaration(var);
−
  '''WHERE'''
+
if (declaration != null) {
−
    <math>G(x_1,...,x_n,s_1,...,s_m)~</math>     
+
  final Set<IOccurrence> propagatedOccs = query.getOccurrences(declaration,
−
  '''THEN'''                 
+
        EventBPlugin.getIdentifierPropagator());
−
    <math>s_1,...,s_m \bcmsuch \exists y_1,...y_n.(P_1(x1,...,x_n,s_1,...,s_m,y_1) \land ... \land P_n(x_1,...,x_n,s_1,...,s_m,y_n) \land P_{n+1}(x_1,...,x_n,s_1,...,s_m,s_1') \land ... \land P_{n+m}(x_1,...,x_n,s_1,...s_m,s_m'))</math>
+
  ...
−
 
+
}
−
Or, after applying some simplification rules:
+
</pre>
−
 
 
−
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 \bcmsuch \exists y_1.(P_1(x1,...,x_n,s_1,...,s_m,y_1)) \land ... \land \exists y_n.(P_n(x_1,...,x_n,s_1,...,s_m,y_n)) \land P_{n+1}(x_1,...,x_n,s_1,...,s_m,s_1')</math>
 
−
    ...
 
−
    <math>s_m \bcmsuch \exists y_1.(P_1(x1,...,x_n,s_1,...,s_m,y_1)) \land ... \land \exists y_n.(P_n(x_1,...,x_n,s_1,...,s_m,y_n)) \land P_{n+m}(x_1,...,x_n,s_1,...s_m,s_m')</math>
 
−
 
 
−
'''Construction for <math>\bcmeq</math>'''<br>
 
−
Additional simplification rules apply:
 
−
If <math>P_i(x_1,...,x_n,s_1,...,s_m,y_i)~</math> is equal to  <math>y_i = Q_i(x_1,...,x_n,s_1,...,s_m)~</math>, then <math>\exists y_i.P_i(x1,...,x_n,s_1,...,s_m,y_i)</math> is always true and shall be deleted.
 
−
 
 
−
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>
 
−
Proof obligations generated for deterministic actions are indeed more suitable than those generated for non-deterministic actions.
 
−
 
 
−
'''Construction for <math>\bcmin</math>'''<br>
 
−
Additional simplification rules apply:
 
−
If <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.x \in S</math> (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>).
 
−
 
 
−
===== Partitioning the events in the sub-machines of the decomposition =====
 
−
Let's first assume that the variables have been previously partitioned among sub-machines. The case where <math>e</math> is an event that accesses a ''private'' variable <math>v1</math> associated to a sub-machine <math>M1</math> and a ''private'' variable <math>v2</math> associated to a sub-machine <math>M2</math> cannot be successfully handled. As a consequence, 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>EXTENDS</math> clauses shall be empty.
 
−
* 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 inheritance 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.
 
−
 
 
−
===== 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
 
−
  '''WHERE'''
 
−
    <math>G(x_1,...,x_n,y_1,...,y_m)~</math>     
 
−
  '''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>
 
−
 
 
−
Only the variables of the considered sub-machine shall appear in the built initialization event; other variables shall become bound:
 
−
 
 
−
  e
 
−
  '''WHERE'''
 
−
    <math>G(x_1,...,x_n)~</math>     
 
−
  '''THEN'''                 
 
−
    <math>x_1,...,x_n \bcmsuch \exists z_1,...,z_m.P(x1,...,x_n,y_1,...,y_m,x_1',...,x_n',y_1,...,y_m')</math>
 
−
 
 
−
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> ====
 
−
We will see in this section how to distribute the invariants among the sub-machines, once the variables have been partitioned.
 
−
 
 
−
* Case 1: If <math>i</math> is an invariant only involving ''private'' variables, then it shall be copied in the sub-machines containing these variables.  
 
−
* Case 2: If <math>i</math> is an invariant only involving ''shared'' variables, then it shall be copied in the sub-machines containing these variables.
 
−
* Case 3: If <math>i</math> is an invariant involving ''private'' variables and ''shared'' variables, then it shall not be copied.
 
−
 
 
−
<font color="red">If an invariant involving a ''private'' variable and a ''shared'' variable is used for typing and is not copied, a problem will be detected by the static checker.</font>
 
−
 
 
−
==== 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.
 
−
 
 
−
=== Decomposition of a context in sub-contexts ===
 
−
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 hierarchy of contexts 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.
 
−
<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 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.
 
−
 
 
−
==== 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.
 
−
 
 
−
==== 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 ====
 
−
We will see in this section how to distribute the axioms among the sub-contexts, once the carrier sets and constants have been copied.
 
−
 
 
−
<font color="red">TODO</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 ===
 
−
<font color="red">
 
−
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?
 
−
</font>
 
−
 
 
−
=== Configuration of the decomposition ===
 
−
The end-user shall be asked to parametrize the decomposition.
 
−
 
 
−
* Identifying the event model to be decomposed
 
−
* Identifying the sub-components to be created
 
−
* Specifying how to perform the decomposition (event partition)
 
−
* Asking for invariants and theorems that can be "forgotten" during the decomposition (because they are not required any longer by user)
 
−
 
 
−
<center>
 
−
[[Image:GUI.png]]
 
−
</center>
 
−
 
 
−
=== Execution of the decomposition ===
 
−
* Generating the sub-machines
 
−
* Generating the sub-contexts
 
−
* Actions, menus, buttons
 
−
* New project?
 
−
 
 
−
=== Generation of the proof obligations ===
 
−
<font color="red">TODO</font>
 
−
* Generating the useful proof obligations
 
−
* Not "propagating" useless proof obligations
 
−
 
 
−
== 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 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:
 
−
<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 sub-machine <math>m</math>, <math>(access;partition^{-1})[\{m\}]~</math> is then 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:Decomposition.png]]
 
−
</center>
 
−
 
 
−
A non-decomposed machine has been decomposed in two sub-machines <math>M1</math> and <math>M2</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>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 before, <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>.
 
−
 
 
−
''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".
 
  
−
== Bibliography ==
+
Here, we start from the 'var' handle but of course, we could also have obtained its declaration by any other way (see other examples).
  
−
* 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]).
+
Returned occurrences can then be filtered, as usual.
−
* J.R. Abrial, <font id="ancre_1">''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]).
 
  
 
[[Category:Design]]
 
[[Category:Design]]
−
[[Category:Work in progress]]
 

Latest revision as of 09:31, 10 March 2009

Purpose

The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences allows for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.

Performing queries

The indexer contents are not directly accessible to other plug-ins. Queries are sent through a IIndexQuery object provided by the RodinCore plug-in.

What to query ?

Two types of information can be queried:

  • declarations (IDeclaration)
  • occurrences (IOccurrence)

A declaration is the unique identifier of an entity in the index repository. It consists in a handle of the declared element itself plus its user-defined name. Every occurrence refers to one single declaration.

Several query types can be performed, depending on the starting point:

  • getting the declaration of a given element (as IInternalElement)
  • getting the declarations of elements that match a given user-defined name (as String) in a given file
  • getting the declarations of elements that occur, or could occur, in a given file
  • getting occurrences of a given declaration (this declaration having been retrieved from a previous query)
  • getting occurrences of a given declaration using propagation (see Propagation hereafter )

Thus, a declaration is the key to retrieve occurrences.

As the result might be too coarse, queries can be filtered out using various criterias (see IIndexQuery interface for more details).

Occurrences

An occurrence (IOccurrence) describes a location (IRodinLocation) and a kind of occurrence (IOccurrenceKind) of an element (referred to through its IDeclaration). For example, in Event-B, an occurrence could be:

location
in IAxiom 'a' (handle), in the PREDICATE_ATTRIBUTE, between characters 7 and 12
kind
REFERENCE
declaration
the ICarrierSet 's' (handle), named "set1"

Occurrence kinds are contributed by indexers, no kinds are defined at the indexing system level. See more in Event-B Indexers.

Propagation

Propagation is a way to get occurrences of several declarations, starting from one single declaration. In particular, it addresses cases where various declarations represent the same entity. The problem is that each declaration has separate occurrences. The propagation mechanism allows to get all occurrences of the entity, whatever the underlying declaration.

For example, in Event-B, a variable can be redeclared in a refining machine. In the index repository, each variable has a separate declaration and separate occurrences. However, it might be interesting in some cases to consider occurrences of the concrete variable as a subset of occurrences of the abstract one. The concept here is to 'propagate' the query about the abstract variable to occurrences of the concrete one. This is achievable in this case thanks to event-B propagators.

See more in Event-B Indexers Propagation.

Getting a valid result

The indexing system data is constantly evolving, as long as files get modified. Furthermore, as indexing is performed as a background operation, one cannot guess whether the indexing has completed or not. The system may also be updating its data, making it temporarily incoherent. Thus, the problem arises to ensure that the data is valid and up-to-date.

To that end, a method is provided by the IIndexQuery, that blocks the current thread until all planned files are indexed. Requests performed after that will thus return a valid result and benefit from the most up-to-date version of the data.

Query Examples

Here are a few examples of index queries. They are all implicitly preceded by the following code 

 final IIndexQuery query = RodinCore.makeIndexQuery();
 query.waitUpToDate();

that creates the query object and waits until the index becomes up-to-date.

Occurrences of an element

Input Data:

  • a handle 'var' of an IVariable

To get its declaration 

final IDeclaration declVar = query.getDeclaration(var);

Remember to check for a null return value.

From that declaration, the user-defined name of the variable can be retrieved 

final String userDefinedName = declVar.getName();

To get the occurrences of 'var' 

final Set<IOccurrence> occurrences = query.getOccurrences(declVar);

Homonyms in a file

Input Data:

  • a handle 'file' of an IRodinFile
  • a name "foo"

Goal: getting declarations of all elements named "foo" that occur in 'file'

First, all declarations of all indexed elements that occur in 'file' are retrieved. Then a query filter on the name is used. 

final Set<IDeclaration> declarations = query.getDeclarations(file);
query.filterName(declarations, "foo");

At the end, 'declarations' contains the declarations of all elements named "foo" occurring in 'file'.

Parameters of an event

Input Data:

  • a handle 'file' of an IRodinFile
  • a handle 'evt1' of an IEvent

Goal: getting the declarations of all parameters of 'evt1' 

final Set<IDeclaration> declarations = query.getDeclarations(file);
query.filterType(declarations, IParameter.ELEMENT_TYPE);

final Set<IOccurrence> occurrences = query.getOccurrences(declarations);
query.filterKind(occurrences, EventBPlugin.DECLARATION);

final IInternalLocation evt1Location = RodinCore.getInternalLocation(evt1);
query.filterLocation(occurrences, evt1Location);

final Set<IDeclaration> paramsOfEvt1 = query.getDeclarations(occurrences);

We first get all declarations of elements that occur in 'file', and we filter them so as to keep only declarations of parameters.

We then get all occurrences of those parameters. We want parameters that have a DECLARATION occurrence in 'evt1'. To that aim, two filters are successively applied to the occurrences.

Finally we get the declarations (IDeclaration) associated with the filtered occurrences.

Query with propagation

Input Data:

  • a handle 'var' to a IVariable

Goal: getting all occurrences of 'var' including occurrences in machines that redeclare 'var'. 

final IDeclaration declaration = query.getDeclaration(var);
if (declaration != null) {
   final Set<IOccurrence> propagatedOccs = query.getOccurrences(declaration,
         EventBPlugin.getIdentifierPropagator());
   ...
}

Here, we start from the 'var' handle but of course, we could also have obtained its declaration by any other way (see other examples).

Returned occurrences can then be filtered, as usual.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Event_Model_Decomposition&oldid=5627’