EMF framework for Event-B - Revision history

Colin: /* Structure Editor */

2020-05-19T13:04:36Z

Structure Editor

← Older revision		Revision as of 13:04, 19 May 2020
Line 166:		Line 166:
	The text editor will be available in two forms. A first class Eclipse editor will offer editing of full machines and contexts. In addition a pop-up editor will be created that can be used by other tools to allow their users text editing of sub-components in machines and contexts. An example is the [[#Structure Editor\|Structure Editor]], which will offer a pop-up text editor allowing the user to edit a single expression or a compound sub-component such as an event.		The text editor will be available in two forms. A first class Eclipse editor will offer editing of full machines and contexts. In addition a pop-up editor will be created that can be used by other tools to allow their users text editing of sub-components in machines and contexts. An example is the [[#Structure Editor\|Structure Editor]], which will offer a pop-up text editor allowing the user to edit a single expression or a compound sub-component such as an event.

	====Structure Editor====		====Rose: Structure Editor====
	EMF provides support to generate structured (e.g. tree, list, table based) editors for models. An adapted version of these editors will allow users to edit machine and context elements within a structure using menu-guided selections. To allow feature-rich editing of elements containing expressions, predicates and substitutions this editor will use the pop-up variant of the [[#Text Editor\|Text Editor]].		EMF provides support to generate structured (e.g. tree, list, table based) editors for models. An adapted version of these editors will allow users to edit machine and context elements within a structure using menu-guided selections. To allow feature-rich editing of elements containing expressions, predicates and substitutions this editor will use the pop-up variant of the [[#Text Editor\|Text Editor]].

imported>Colin at 10:12, 21 May 2018

2018-05-21T10:12:19Z

← Older revision		Revision as of 10:12, 21 May 2018
Line 36:		Line 36:
	''EventBNamedCommentedActionElement'' provides a string attribute, ''action'' (inherited from ''EventBAction''), for an Event-B mathematical substitution.		''EventBNamedCommentedActionElement'' provides a string attribute, ''action'' (inherited from ''EventBAction''), for an Event-B mathematical substitution.

	[[File:EMFcore1abstract.gif\|EMF model, abstract base elements]]		[[File:EMFcore1abstract.gif\|EMF model abstract base elements]]


	====Extensibility Mechanism====		====Extensibility Mechanism====

imported>Colin at 10:10, 21 May 2018

2018-05-21T10:10:58Z

← Older revision		Revision as of 10:10, 21 May 2018
Line 37:		Line 37:

	[[File:EMFcore1abstract.gif\|EMF model, abstract base elements]]		[[File:EMFcore1abstract.gif\|EMF model, abstract base elements]]


	====Extensibility Mechanism====		====Extensibility Mechanism====

imported>Colin: /* Abstract Basis */

2018-05-17T15:08:31Z

Abstract Basis

← Older revision		Revision as of 15:08, 17 May 2018
Line 32:		Line 32:
	''EventBNamedCommentedPredicateElement'' provides a string attribute, ''predicate'' (inherited from ''EventBPredicate''), for an Event-B mathematical predicate. Note that our current need is for all predicate elements to be commented and named.		''EventBNamedCommentedPredicateElement'' provides a string attribute, ''predicate'' (inherited from ''EventBPredicate''), for an Event-B mathematical predicate. Note that our current need is for all predicate elements to be commented and named.

	''EventBNamedCommentedDerivedPredicateElement'' ~~exten ds~~ ''EventBNamedCommentedPredicateElement'' and provides a boolean attribute, ''theorem'' (inherited from ''EventBDerived'' to indicate that the predicate is a theorem that should be derived (from previous predicates in the same container).		''EventBNamedCommentedDerivedPredicateElement'' extends ''EventBNamedCommentedPredicateElement'' and provides a boolean attribute, ''theorem'' (inherited from ''EventBDerived'' to indicate that the predicate is a theorem that should be derived (from previous predicates in the same container).

	''EventBNamedCommentedActionElement'' provides a string attribute, ''action'' (inherited from ''EventBAction''), for an Event-B mathematical substitution.		''EventBNamedCommentedActionElement'' provides a string attribute, ''action'' (inherited from ''EventBAction''), for an Event-B mathematical substitution.

	[[~~Image~~:EMFcore1abstract.gif\|EMF model, abstract base elements]]		[[File:EMFcore1abstract.gif\|EMF model, abstract base elements]]

	====Extensibility Mechanism====		====Extensibility Mechanism====

imported>Colin at 15:02, 17 May 2018

2018-05-17T15:02:33Z

← Older revision		Revision as of 15:02, 17 May 2018
Line 32:		Line 32:
	''EventBNamedCommentedPredicateElement'' provides a string attribute, ''predicate'' (inherited from ''EventBPredicate''), for an Event-B mathematical predicate. Note that our current need is for all predicate elements to be commented and named.		''EventBNamedCommentedPredicateElement'' provides a string attribute, ''predicate'' (inherited from ''EventBPredicate''), for an Event-B mathematical predicate. Note that our current need is for all predicate elements to be commented and named.

	''EventBNamedCommentedDerivedPredicateElement'' ~~extends~~ ''EventBNamedCommentedPredicateElement'' and provides a boolean attribute, ''theorem'' (inherited from ''EventBDerived'' to indicate that the predicate is a theorem that should be derived (from previous predicates in the same container).		''EventBNamedCommentedDerivedPredicateElement'' exten ds ''EventBNamedCommentedPredicateElement'' and provides a boolean attribute, ''theorem'' (inherited from ''EventBDerived'' to indicate that the predicate is a theorem that should be derived (from previous predicates in the same container).

	''EventBNamedCommentedActionElement'' provides a string attribute, ''action'' (inherited from ''EventBAction''), for an Event-B mathematical substitution.		''EventBNamedCommentedActionElement'' provides a string attribute, ''action'' (inherited from ''EventBAction''), for an Event-B mathematical substitution.

imported>Colin: /* Abstract Basis */

2018-05-17T15:01:55Z

Abstract Basis

← Older revision		Revision as of 15:01, 17 May 2018
Line 16:		Line 16:

	====Abstract Basis====		====Abstract Basis====
	The meta-model is built upon a structure of abstract meta-classes. (Abstract meta-classes are ones that cannot be directly instantiated. Their instances are always instances of one of their concrete sub-meta-classes). These abstract meta-classes are useful because they enable a feature to be defined once in the meta-model and be used, via inheritance, by many concrete meta-classes. Apart from making it easier to maintain the meta-model, this makes it possible to write code that is more generic, since it can work on features without knowing which concrete meta-class the instance it is working on belongs to. To easily distinguish abstract meta-classes from concrete ones, we prefix abstract meta-classes with ''EventB''. For abstract classes, we also follow the convention of including within the name, all the features that are inherited by that meta-class. For example, ''EventBNamedCommentedElement'' inherits from ''EventBCommentedElement'' and from ''EventBNamed''. The abstract meta-classes which are to be used to define concrete meta-classes are arranged in a hierarchy. Each feature is contained in a meta-class outside of this hierarchy (e.g. ''EventBNamed''). This provides a flexible choice of how to access model objects, either at a point in the hierarchy to generalise over parts of its structure or via the feature containers to generalise over all elements that may own that feature. (Although currently these are equivalent, this may not always be the case).		The meta-model is built upon a structure of abstract meta-classes. (Abstract meta-classes are ones that cannot be directly instantiated. Their instances are always instances of one of their concrete sub-meta-classes). These abstract meta-classes are useful because they enable a feature to be defined once in the meta-model and be used, via inheritance, by many concrete meta-classes. Apart from making it easier to maintain the meta-model, this makes it possible to write code that is more generic, since it can work on features without knowing which concrete meta-class the instance it is working on belongs to. To easily distinguish abstract meta-classes from concrete ones, we prefix abstract meta-classes with ''EventB''. For abstract classes, we also follow the convention of including within the name, all the features that are inherited by that meta-class. For example, ''EventBNamedCommentedElement'' inherits from ''EventBCommentedElement'' and from ''EventBNamed''. The abstract meta-classes which are to be used to define concrete meta-classes are arranged in a hierarchy. Each feature is contained in a meta-class outside of this hierarchy (e.g. ''EventBNamed''). This provides a flexible choice of how to access model objects, either at a point in the hierarchy to generalise over parts of its structure or via the feature containers to generalise over all elements that may own that feature. (Although currently these are equivalent, this may not always be the case).

	The root of all meta-classes in the Event-B EMF model is the abstract base class, ''EventBObject'' this provides some convenience methods to access containing or contained elements of a specified type and a method to obtain the URL of an element's package. ''EventBObject'' extends the EMF class, ''EObject'' and provides a collection of ''Annotations''. ''Annotations'' (which are similar to Ecore's ''EAnnotations'' ) give a flexible and efficient way to store information that is not part of the main model. For example this is used to store some information contained in the Rodin database, which must be preserved but is not of interest in the EMF modelling tools.		The root of all meta-classes in the Event-B EMF model is the abstract base class, ''EventBObject'' this provides some convenience methods to access containing or contained elements of a specified type and a method to obtain the URL of an element's package. ''EventBObject'' extends the EMF class, ''EObject'' and provides a collection of ''Annotations''. ''Annotations'' (which are similar to Ecore's ''EAnnotations'' ) give a flexible and efficient way to store information that is not part of the main model. For example this is used to store some information contained in the Rodin database, which must be preserved but is not of interest in the EMF modelling tools.

imported>Colin at 15:51, 27 July 2017

2017-07-27T15:51:49Z

← Older revision		Revision as of 15:51, 27 July 2017
Line 2:		Line 2:

	This page describes the core facilities for loading Rodin Event-B models in EMF and the 'hooks' that are provided for making extensions. Further support for extending the Event-B modelling language is available here: [[Generic Event-B EMF extensions]].		This page describes the core facilities for loading Rodin Event-B models in EMF and the 'hooks' that are provided for making extensions. Further support for extending the Event-B modelling language is available here: [[Generic Event-B EMF extensions]].

			A generic EMF to EMF translator is also available. This can be configured to generate Event-B EMF and is used for some more recent Event-B generators. It will eventually replace the generator that only targets Event-B.
			The generic translator can be used between any source-target pair of EMF meta-models. It is described here: [[EMF to EMF model translator]].

imported>Colin at 09:30, 7 July 2017

2017-07-07T09:30:29Z

← Older revision		Revision as of 09:30, 7 July 2017
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}
	''This page ~~is edited by Colin, Alexei~~ and ~~Fabian~~''
			This page describes the core facilities for loading Rodin Event-B models in EMF and the 'hooks' that are provided for making extensions. Further support for extending the Event-B modelling language is available here: [[Generic Event-B EMF extensions]].

imported>TIDTWeb at 09:26, 7 July 2017

2017-07-07T09:26:08Z

← Older revision		Revision as of 09:26, 7 July 2017
Line 188:		Line 188:

	[[Category:Design proposal]]		[[Category:Design proposal]]
			.

imported>Colin: /* Extensibility Mechanism */

2011-12-07T17:43:55Z

Extensibility Mechanism

← Older revision		Revision as of 17:43, 7 December 2011
Line 54:		Line 54:
	* It may be viewed as a child element of the parent. In this case, it should be configured with a synchroniser that extends AbstractSynchroniser.		* It may be viewed as a child element of the parent. In this case, it should be configured with a synchroniser that extends AbstractSynchroniser.

	* If Rodin doesn't need to understand the contents of the extension, the extension element should be configured to use the SerialisedExtensionSynchroniser. In this case the extension will be persisted in EMF XMI format in a single attribute of the generic Rodin Element kind, SerialisedExtension.		* If Rodin doesn't need to understand the contents of the extension, the extension element should be configured to use the SerialisedExtensionSynchroniser. In this case the extension will be persisted in EMF XMI format in a single attribute of the generic Rodin Element kind, SerialisedExtension. For example, this mechanism is used for making diagrammatic modelling extension.


	The following generic fallback mechanisms are also supported:		The following generic fallback mechanisms are also supported:
Line 63:		Line 62:

	[[Image:EMFcore2extensions.gif\|EMF model, extension mechanism]]		[[Image:EMFcore2extensions.gif\|EMF model, extension mechanism]]

			Further support for [[Generic Event-B EMF extensions]] is available.

	====Project====		====Project====