Difference between pages "Element Hierarchy Extension Point & Library" and "Event-B Indexers"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
imported>Laurent
 
Line 1: Line 1:
The UI in Rodin 2.x contains an extension point <tt>org.eventb.ui.editorItems</tt> that groups the both following information:
+
==Purpose==
*the definition of elements and attributes and their hierarchy, and the way they are created
 
*the information needed to correctly display and edit these elements in the various editors and UI components
 
  
It appears obvious that the first information should be defined from an extension that belongs to the Database.
+
Event-B indexers populate the index repository. Currently, indexers are implemented for the following files :
To fullfil the above statement, the current extension point <tt>org.eventb.ui.editorItems</tt> should be split in two.
+
* machine (.bum)
The existing extension point was also heterogenous. Indeed, whereas the element relationships were concerning element types, the attribute relationship were concerning element types and references to UI defined attributes (referring to core attributes).<br>
+
* context (.buc)
There is no need for such an indirection.
 
  
----
 
The proposal should concern :
 
A - Relationship declaration (new extension point)
 
B - API to test these relations and traverse them
 
C - Enforcement of the authorized relations when modifying the DB
 
D - Behaviour while loading a file (including a file with invalid parent-child relations occurrences)
 
E- What about the compatibilty with the file upgrade mechanism?
 
----
 
  
= Some identified difficulties =
+
==Event-B Occurrence Kinds==
  
== Initialization of elements from non UI components ==
+
So far, the following occurrence kinds have been defined :
 +
* DECLARATION : when a variable, a carrier set, ..., is declared
 +
* REFERENCE : when a variable, a carrier set, ..., is referenced (but not modified)
 +
* MODIFICATION : when a variable is modified (e.g., occurs in the left-hand side of an event action)
 +
* REDECLARATION : when a variable, parameter or event is redeclared (refined).
 +
Please notice the distinction between the index repository notion of declaration ({{class|IDeclaration}}) and the Event-B occurrence kind DECLARATION.
  
The following ElementDescRegistry method, shows the dependency between an element creation and the initialization of its attributes with default values.
+
==What Is Indexed==
  
        public <T extends IInternalElement> T createElement(
+
Currently, indexed elements are :
final IInternalElement root, IInternalElement parent,
+
* carrier sets
final IInternalElementType<T> type, final IInternalElement sibling)
+
* constants
throws RodinDBException {
+
* variables
final T newElement = parent.createChild(type, sibling, null);
+
* events
final IAttributeDesc[] attrDesc = getAttributes(type);
+
* parameters
for (IAttributeDesc desc : attrDesc) {
 
desc.getManipulation().setDefaultValue(newElement, null);    // <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<
 
}
 
return newElement;
 
}
 
  
The protocol shall be changed to take into account this initialization outside from the graphical manipulation.
+
Formulas which cannot be parsed are ignored.
Doing the initialization at org.eventb.core level is possible by registering a special "attribute initializer". <br>
 
WARNING : The required attribute is only available for "choice" attributes. Can't it be available for all kind of attributes?
 
  
== Correspondence between UI manipulation and "core" elements ==
+
In the descriptions below, the following notation will be used to specify locations :
What if an element is not defined in the UI but defined in the hierarchy of a given core element?<br>
+
* [element] : internal location
>>> ANSWER : it seems that any contributor to the UI manages the extensions of the datat model. The responsability is thus left to him.<br>
+
* [element/attribute] : attribute location
>>> A element for which there is no UI correspondance will not be displayed.
+
* [element/attribute/begin..end] : attribute substring location
  
== Operation on elements shall be enforced ==
+
===Context Indexer===
 
        private <T extends IInternalElement> OperationCreateElement getCreateElement(
 
IInternalElement parent, IInternalElementType<T> type,
 
IInternalElement sibling, IAttributeValue[] values) {
 
OperationCreateElement op = new OperationCreateElement(
 
createDefaultElement(parent, type, sibling));
 
op.addSubCommande(new ChangeAttribute(values));
 
return op;
 
}
 
  
''The Operation model similar to a kind of transaction mechanism, should be made available from the DB layer.''<br>
+
====Dependencies====
''The relations when using such layer shall be enforced and any invalid operation could be rejected.''
+
* extended contexts
  
= Proposal =
+
====Declarations====
 +
* carrier sets
 +
* constants
  
== Hierarchy between elements ==
+
====Occurrences====
  
The part concerning element definition and hierarchy will go to a dedicated extension point in the database.
+
* DECLARATION of carrier sets [CarrierSet/Identifier]
 +
* DECLARATION of constants [Constant/Identifier]
 +
* REFERENCE of elements in axioms [Axiom/Predicate/b..e]
 +
* REFERENCE of elements in theorems [Theorem/Predicate/b..e]
  
=== A - hierarchy definition ===
+
Example:
  
Here is the definition of such an extension point : org.rodinp.core.dataModel ???  or org.rodinp.core.internalElementHierarchy ???
+
  Ctx
 +
  Sets
 +
    S
 +
  Constants
 +
    C
 +
  Axioms
 +
    axm1 : C ∈ S
  
Configuration Markup:
+
We will end up with the following occurrences :
<!ELEMENT extension ((childRelation | attributeRelation | autoNaming)+)>
 
<!ATTLIST extension
 
point CDATA #REQUIRED
 
id    CDATA #IMPLIED
 
name  CDATA #IMPLIED
 
>
 
 
<!ELEMENT elementRelationship (childType)+>
 
<!ATTLIST elementRelationship
 
parentTypeId CDATA #REQUIRED
 
>
 
parentTypeId - Element type of the parent, must be the unique ID of a Rodin internal element type (see extension point org.rodinp.core.internalElementTypes).
 
 
<!ELEMENT childType EMPTY>
 
<!ATTLIST childType
 
typeId                CDATA #REQUIRED
 
implicitChildProvider CDATA #IMPLIED
 
>
 
typeId - Element type of the child, must be the unique ID of a Rodin internal element type (see extension point org.rodinp.core.internalElementTypes).
 
 
<!ELEMENT attributeRelationship (attributeType)+>
 
<!ATTLIST attributeRelationship
 
elementTypeId CDATA #REQUIRED
 
>
 
elementTypeId - Element type of the element, must be the unique ID of a Rodin internal element type (see extension point org.rodinp.core.internalElementTypes).
 
 
<!ELEMENT attributeType EMPTY>
 
<!ATTLIST attributeType
 
typeId CDATA #REQUIRED
 
class  CDATA #REQUIRED
 
>
 
Describes how to graphically display a Rodin attribute of type boolean.
 
 
attributeTypeId - Id of the Rodin attribute type to which this description applies (see extension point org.rodinp.core.attributeTypes).
 
 
<!ELEMENT autoNaming EMPTY>
 
<!ATTLIST autoNaming
 
elementTypeId          CDATA #REQUIRED
 
attributeDescriptionId CDATA #REQUIRED
 
namePrefix             CDATA #REQUIRED
 
>
 
Describes how to automatically name an element. The autoNaming definition is unique for a given element type.
 
 
elementTypeId - Element type of the element, must be the unique ID of a Rodin internal element type (see extension point org.rodinp.core.internalElementTypes).
 
namePrefix - default prefix to name the element
 
 
The use of such extension point is obvious in org.eventb.core plug-in, as it would complement the extensions of org.rodinp.core.attributeTypes and org.rodinp.core.internalElementTypes.
 
  
=== B - API to declare and test the element/attribute relations and traverse them ===
+
  S :
 +
    DECLARATION in [S/Identifier]
 +
    REFERENCE in [axm1/Predicate/4..5]
 +
  C :
 +
    DECLARATION in [C/Identifer]
 +
    REFERENCE in [axm1/Predicate/0..1]
  
The API for an element : IElementDesc
+
====Exports====
 +
* imported and declared carrier sets
 +
* imported and declared constants
  
public String getID();
+
===Machine Indexer===
 
public List<IAttributeDesc> getAttributeDescriptionss();
 
 
public List<IElementRelationship> getChildRelationships();
 
 
public List<IElementType> getChildTypes();
 
 
public IAttributeDesc getAutoNameAttribute();
 
  
adding the following method to the protocol :
+
====Dependencies====
 +
* refined machines
 +
* seen contexts
  
        public boolean isDirectChildTypeOf(IElementDesc parentElemDesc);
+
====Declarations====
 +
* variables
 +
* events
 +
* parameters
  
The API for an Attribute : IAttributeDesc
+
====Occurrences====
+
* DECLARATION of (local) variables [Variable/Identifier]
        public String getID()
+
* DECLARATION of (local) events [Event/Label]
     
+
* DECLARATION of (local) parameters [Parameter/Identifier]
        public IAttributeManipulation getManipulation();
+
* REDECLARATION of abstract variables in the local variables that redeclare them [Variable/Identifier]
+
* REDECLARATION of abstract events in the local events that refine them [Event/RefinesEvent/Target]
public IAttributeType getAttributeType();
+
* REDECLARATION of abstract parameters in the local parameters that redeclare them [Parameter/Identifier]
 +
* REFERENCE of abstract parameters or variables in witnesses [Witness/Label]
 +
* REFERENCE of elements in invariants [Invariant/Predicate/b..e]
 +
* REFERENCE of elements in theorems [Theorem/Predicate/b..e]
 +
* REFERENCE of elements in variants [Variant/Expression/b..e]
 +
* REFERENCE of elements in guards [Guard/Predicate/b..e]
 +
* REFERENCE of elements in witnesses [Witness/Predicate/b..e]
 +
* REFERENCE of non assigned elements in actions [Action/Assignment/b..e]
 +
* MODIFICATION of assigned elements in actions [Action/Assignment/b..e]
  
== Data model operation ==
+
Example :
The ElementManipulationFacade, support for modifications over the Database, should be provided by the Event-B Core plug-in.<br>
 
The IAttributeManipulation interface should be also provided by the Event-B Core plug-in as it concerns the manipulation done on the attribute in the DB.
 
  
The information about the rendering of an element or an attribute, should not be deduced from the attribute itself (e.g. choiceAttribute vs. toggleAttribute vs. textAttribute), it should be given in the UI.
+
  M1
 +
  VARIABLES
 +
    var1
 +
  INVARIANTS
 +
    inv1 : var1 > 0
 +
  EVENTS
 +
    INITIALISATION
 +
      THEN
 +
        act1 : var1 := 1
  
== UI related information ==
+
After indexing M1, we will have the following occurrences:
The part concerning how to display elements and UI related info will stay in the editorItems extension point and shall point to an element definition and hierachy.<br>
 
Relationships will disappear from the editorItems extension point.
 
  
The interfaces are refactored to become the following :
+
  M1.var1 :
 +
    DECLARATION in [M1.var1/Identifier]
 +
    REFERENCE in [M1.inv1/Predicate/0..4]
 +
    MODIFICATION in [M1.act1/Assignment/0..4]
 +
  M1.INITIALISATION :
 +
    DECLARATION in [M1.INITIALISATION/Label]
  
''NB. IITemDesc disappears as it is cumbersome to provide such interface for a sole method getPrefix(). ''
+
Then, if we add another machine
  
public interface IUIElementDesc extends IItemDesc {
+
  M2
+
  REFINES
        public String getPrefix();
+
    M1
+
  VARIABLES
public String getChildrenSuffix();
+
    var1
+
  EVENTS
public IImageProvider getImageProvider();
+
    INITIALISATION
+
      THEN
public IAttributeDesc atColumn(int i);
+
        act1 : var1 := 1
 
public int getDefaultColumn();
 
 
public boolean isSelectable(int i);
 
 
public String getAutoNamePrefix();
 
 
public IElementPrettyPrinter getPrettyPrinter();
 
 
}
 
  
public interface IUIAttributeDesc extends IItemDesc {
+
we will add the following occurrences :
 
        public String getPrefix();
 
 
public String getSuffix();
 
 
public IEditComposite createWidget();
 
 
public boolean isHorizontalExpand();
 
 
}
 
  
[[Category:Design_proposal]]
+
  M1.var1 :
 +
    REDECLARATION in [M2.var1/Identifier]
 +
  M2.var1 :
 +
    DECLARATION in [M2.var1/Identifier]
 +
    MODIFICATION in [M2.act1/Assignment/0..4]
 +
  M2.INITIALISATION :
 +
    DECLARATION in [M2.INITIALISATION/Label]
 +
 
 +
====Exports====
 +
* imported carrier sets
 +
* imported constants
 +
* local variables
 +
* local events
 +
* local parameters
 +
 
 +
==Propagation==
 +
 
 +
Propagators are defined for :
 +
* events ({{class|EventPropagator}}) to propagate through refines
 +
* parameters ({{class|IdentifierPropagator}}) to propagate through redeclaration
 +
* variables ({{class|IdentifierPropagator}} as well) to propagate through redeclaration
 +
 
 +
In the above example with machines M1 and M2, after both files have been indexed, we can query occurrences of M1.var1.
 +
 
 +
With no propagator, the result would be :
 +
 
 +
  M1.var1 :
 +
    DECLARATION in [M1.var1/Identifier]
 +
    REFERENCE in [M1.inv1/Predicate/0..4]
 +
    MODIFICATION in [M1.act1/Assignment/0..4]
 +
    REDECLARATION in [M2.var1/Identifier]
 +
 
 +
Using the {{class|IdentifierPropagator}}, the result becomes :
 +
 
 +
  M1.var1 (propagated) :
 +
    DECLARATION in [M1.var1/Identfiier]
 +
    REFERENCE in [M1.inv1/Predicate/0..4]
 +
    MODIFICATION in [M1.act1/Assignment/0..4]
 +
    REDECLARATION in [M2.var1/Identifier]
 +
    DECLARATION in [M2.var1/Identifier]
 +
    MODIFICATION in [M2.act1/Assignment/0..4]
 +
 
 +
[[Category:Developer documentation]]

Revision as of 09:46, 10 March 2009

Purpose

Event-B indexers populate the index repository. Currently, indexers are implemented for the following files :

  • machine (.bum)
  • context (.buc)


Event-B Occurrence Kinds

So far, the following occurrence kinds have been defined :

  • DECLARATION : when a variable, a carrier set, ..., is declared
  • REFERENCE : when a variable, a carrier set, ..., is referenced (but not modified)
  • MODIFICATION : when a variable is modified (e.g., occurs in the left-hand side of an event action)
  • REDECLARATION : when a variable, parameter or event is redeclared (refined).

Please notice the distinction between the index repository notion of declaration (IDeclaration) and the Event-B occurrence kind DECLARATION.

What Is Indexed

Currently, indexed elements are :

  • carrier sets
  • constants
  • variables
  • events
  • parameters

Formulas which cannot be parsed are ignored.

In the descriptions below, the following notation will be used to specify locations :

  • [element] : internal location
  • [element/attribute] : attribute location
  • [element/attribute/begin..end] : attribute substring location

Context Indexer

Dependencies

  • extended contexts

Declarations

  • carrier sets
  • constants

Occurrences

  • DECLARATION of carrier sets [CarrierSet/Identifier]
  • DECLARATION of constants [Constant/Identifier]
  • REFERENCE of elements in axioms [Axiom/Predicate/b..e]
  • REFERENCE of elements in theorems [Theorem/Predicate/b..e]

Example:

 Ctx
 Sets
   S
 Constants
   C
 Axioms
   axm1 : C ∈ S

We will end up with the following occurrences :

 S :
   DECLARATION in [S/Identifier]
   REFERENCE in [axm1/Predicate/4..5]
 C :
   DECLARATION in [C/Identifer]
   REFERENCE in [axm1/Predicate/0..1]

Exports

  • imported and declared carrier sets
  • imported and declared constants

Machine Indexer

Dependencies

  • refined machines
  • seen contexts

Declarations

  • variables
  • events
  • parameters

Occurrences

  • DECLARATION of (local) variables [Variable/Identifier]
  • DECLARATION of (local) events [Event/Label]
  • DECLARATION of (local) parameters [Parameter/Identifier]
  • REDECLARATION of abstract variables in the local variables that redeclare them [Variable/Identifier]
  • REDECLARATION of abstract events in the local events that refine them [Event/RefinesEvent/Target]
  • REDECLARATION of abstract parameters in the local parameters that redeclare them [Parameter/Identifier]
  • REFERENCE of abstract parameters or variables in witnesses [Witness/Label]
  • REFERENCE of elements in invariants [Invariant/Predicate/b..e]
  • REFERENCE of elements in theorems [Theorem/Predicate/b..e]
  • REFERENCE of elements in variants [Variant/Expression/b..e]
  • REFERENCE of elements in guards [Guard/Predicate/b..e]
  • REFERENCE of elements in witnesses [Witness/Predicate/b..e]
  • REFERENCE of non assigned elements in actions [Action/Assignment/b..e]
  • MODIFICATION of assigned elements in actions [Action/Assignment/b..e]

Example :

 M1
 VARIABLES
   var1
 INVARIANTS
   inv1 : var1 > 0
 EVENTS
   INITIALISATION
     THEN
       act1 : var1 := 1

After indexing M1, we will have the following occurrences:

 M1.var1 :
   DECLARATION in [M1.var1/Identifier]
   REFERENCE in [M1.inv1/Predicate/0..4]
   MODIFICATION in [M1.act1/Assignment/0..4]
 M1.INITIALISATION :
   DECLARATION in [M1.INITIALISATION/Label]

Then, if we add another machine

 M2
 REFINES
   M1
 VARIABLES
   var1
 EVENTS
   INITIALISATION
     THEN
       act1 : var1 := 1

we will add the following occurrences :

 M1.var1 :
   REDECLARATION in [M2.var1/Identifier]
 M2.var1 :
   DECLARATION in [M2.var1/Identifier]
   MODIFICATION in [M2.act1/Assignment/0..4]
 M2.INITIALISATION :
   DECLARATION in [M2.INITIALISATION/Label]

Exports

  • imported carrier sets
  • imported constants
  • local variables
  • local events
  • local parameters

Propagation

Propagators are defined for :

  • events (EventPropagator) to propagate through refines
  • parameters (IdentifierPropagator) to propagate through redeclaration
  • variables (IdentifierPropagator as well) to propagate through redeclaration

In the above example with machines M1 and M2, after both files have been indexed, we can query occurrences of M1.var1.

With no propagator, the result would be :

 M1.var1 :
   DECLARATION in [M1.var1/Identifier]
   REFERENCE in [M1.inv1/Predicate/0..4]
   MODIFICATION in [M1.act1/Assignment/0..4]
   REDECLARATION in [M2.var1/Identifier]

Using the IdentifierPropagator, the result becomes :

 M1.var1 (propagated) :
   DECLARATION in [M1.var1/Identfiier]
   REFERENCE in [M1.inv1/Predicate/0..4]
   MODIFICATION in [M1.act1/Assignment/0..4]
   REDECLARATION in [M2.var1/Identifier]
   DECLARATION in [M2.var1/Identifier]
   MODIFICATION in [M2.act1/Assignment/0..4]