Generic Event-B EMF extensions - Revision history

Colin: /* Contributing new EMF element types to the Navigator view */

2020-05-30T11:01:56Z

Contributing new EMF element types to the Navigator view

← Older revision		Revision as of 11:01, 30 May 2020
Line 43:		Line 43:

	===Contributing new EMF element types to the Navigator view===		===Contributing new EMF element types to the Navigator view===

			The Event-B EMF extensions framework makes it easy to contribute new types of models to the Event-B navigator.
			You just need to tell the framework some details about your models (as follows) and it does the rest.

	If the EMF element types are contained in a new file type, declare the new file extension using the extension point:		If the EMF element types are contained in a new file type, declare the new file extension using the extension point:
Line 50:		Line 53:
	This tells the extensions plugin to adapt the emf contents of those files to be shown in the Navigator.		This tells the extensions plugin to adapt the emf contents of those files to be shown in the Navigator.

	To ensure the EMF elements are labeled and imaged correctly in the Navigator, declare the adapter factory using the extension point:		To ensure the EMF elements are labeled and imaged correctly in the Navigator, declare the EMF adapter factory to the framework using the extension point:

	ac.soton.eventb.emf.core.extension.navigator.adapterFactories		ac.soton.eventb.emf.core.extension.navigator.adapterFactories

	(Note - ~~use~~ the adapter factory generated by the EMF genmodel in the edit plugin).		(Note - the adapter factory is generated by the EMF genmodel in the edit plugin).

	==Refinement==		==Refinement==

Colin: /* Persistence */

2020-05-30T08:49:42Z

Persistence

← Older revision		Revision as of 08:49, 30 May 2020
Line 2:		Line 2:

	==Persistence==		==Persistence==

			Event-B EMF Models may be persisted in several ways:
			# inside a Rodin file by extending Rodin and the Event-B EMF persistence with new Rodin elements and synchronisers to load and save. (This is how the Event-B EMF core plugin works, except that the Rodin elements for standard Event-B already existed).
			# inside a Rodin file as a String attribute containing XMI, using the SerialisedExtensionSynchroniser. (This is how UML-B diagrams are saved inside Machines)
			# in EMF format as an XMI file.
			# in plain text using the XText framework.

			Here we mainly focus on methods 2 and 3.
			We are also developing method 4. as a text persistence, but this is described elsewhere.
			We do not intend to use method 1 as we do not need Rodin to understand the model (because we translate into standard Machines and Context for verification).

			For method 2, declare your root meta-class to use the ''SerialisedExtensionSynchroniser'' using the extension point ''org.eventb.emf.persistence.synchroniser'' e.g.
			<extension
			point="org.eventb.emf.persistence.synchroniser">
			<emfPackage
			name="Statemachines Package"
			nsURI="http://soton.ac.uk/models/eventb/statemachines/2014">
			<synchroniser
			emf_class="Statemachine"
			name="Statemachine"
			rodin_id="ac.soton.eventb.emf.core.extension.persistence.serialisedExtension"
			synchroniser_class="ac.soton.eventb.emf.core.extension.persistence.SerialisedExtensionSynchroniser">
			</synchroniser>
			</emfPackage>
			</extension>

			For method 3, due to the way the Event-B EMF framework implements references, it is important to save files using certain non-default styles.
			To achieve this, declare the content type of your file as ''ac.soton.eventb.emf.core.extension.persistence.contentType'' using the extension point ''org.eclipse.core.contenttype.contentTypes'' e.g.
			<extension
			point="org.eclipse.core.contenttype.contentTypes">
			<file-association
			content-type="ac.soton.eventb.emf.core.extension.persistence.contentType"
			file-extensions="umlb">
			</file-association>
			</extension>

	==Navigator==		==Navigator==

Colin: /* Contributing new EMF element types to the Navigator view */

2020-05-30T08:05:52Z

Contributing new EMF element types to the Navigator view

← Older revision		Revision as of 08:05, 30 May 2020
Line 13:		Line 13:
	ac.soton.eventb.emf.core.extension.navigator.emfFileExtensions		ac.soton.eventb.emf.core.extension.navigator.emfFileExtensions

	To ensure the EMF elements are ~~shown~~ correctly in the Navigator, declare the adapter factory using the extension point:		This tells the extensions plugin to adapt the emf contents of those files to be shown in the Navigator.

			To ensure the EMF elements are labeled and imaged correctly in the Navigator, declare the adapter factory using the extension point:

	ac.soton.eventb.emf.core.extension.navigator.adapterFactories		ac.soton.eventb.emf.core.extension.navigator.adapterFactories

	(Note - the adapter factory ~~is the one~~ generated by the EMF genmodel in the edit plugin).		(Note - use the adapter factory generated by the EMF genmodel in the edit plugin).

	==Refinement==		==Refinement==

Colin: /* Navigator */

2020-05-30T07:58:55Z

Navigator

← Older revision		Revision as of 07:58, 30 May 2020
Line 4:		Line 4:

	==Navigator==		==Navigator==

			This section describes how to extend the Event-B Navigator to support Event-B EMF extensions.

			===Contributing new EMF element types to the Navigator view===

			If the EMF element types are contained in a new file type, declare the new file extension using the extension point:

			ac.soton.eventb.emf.core.extension.navigator.emfFileExtensions

			To ensure the EMF elements are shown correctly in the Navigator, declare the adapter factory using the extension point:

			ac.soton.eventb.emf.core.extension.navigator.adapterFactories

			(Note - the adapter factory is the one generated by the EMF genmodel in the edit plugin).

	==Refinement==		==Refinement==

Colin: /* Generator */

2020-05-30T06:54:10Z

Generator

← Older revision		Revision as of 06:54, 30 May 2020
Line 30:		Line 30:

	==Generator==		==Generator==

			[THIS SECTION NEEDS REVIEW AND UPDATE -
			Note: The generator is now based on a more generic EMF translator: https://github.com/eventB-Soton/EMF_Translator
			It is adapted to Event-B : https://github.com/eventB-Soton/EventB_Translator_Support
			There is a documentation plugin in the EMF translator source code that describes the necessary extension points and how to contribute a specific translation.]

	A framework to support the implementation of generators is provided. The framework is designed to support the generation of standard Event-B models from higher-level model extensions that are based on the Event-B EMF modelling extensions framework.		A framework to support the implementation of generators is provided. The framework is designed to support the generation of standard Event-B models from higher-level model extensions that are based on the Event-B EMF modelling extensions framework.

Colin: /* Refinement */

2020-05-30T06:48:05Z

Refinement

← Older revision		Revision as of 06:48, 30 May 2020
Line 6:		Line 6:

	==Refinement==		==Refinement==

			[THIS SECTION NEEDS REVIEW AND UPDATE]

	The Rodin platform provides an extension point for contributing behaviour to the 'Refine' action.		The Rodin platform provides an extension point for contributing behaviour to the 'Refine' action.

imported>Colin: /* Implementing Rule Classes */

2015-11-10T15:35:52Z

Implementing Rule Classes

← Older revision		Revision as of 15:35, 10 November 2015
Line 85:		Line 85:
	=== Implementing Rule Classes ===		=== Implementing Rule Classes ===

	Rule classes must implement IRule. It is recommended the rule classes extend ac.soton.eventb.emf.diagrams.generator#AbstractRule which provides some concise constants for the commonly needed containments and defines some default behaviour (always enabled and the ~~target EventB component is~~ the source ~~component)~~.		Rule classes must implement IRule. It is recommended the rule classes extend ac.soton.eventb.emf.diagrams.generator#AbstractRule which provides some concise constants for the commonly needed containments and defines some default behaviour (always enabled and dependencies ok). Note that the rule will only be attempted for the type of source element defined in the extension point. However, this could be defined as an abstract base class to allow the rule to operate on several types of element.

	The rule's fire method must return a list of GenerationDescriptors. The Utility class, Make, provides a convenience method to help construct a GenerationDescriptor from the parent element, the containment feature, the new child and the priority indicator and if needed the editable setting.		A rule has 4 methods:

			* boolean enabled (final EventBElement sourceElement)
			* boolean dependenciesOK(EventBElement sourceElement,List<GenerationDescriptor> generatedElements)
			* boolean fireLate()
			* List<GenerationDescriptor> fire(EventBElement sourceElement, List<GenerationDescriptor> generatedElements)

			The enabled method can be used to restrict when it applies. More than one rule can be defined for the same kind of element allowing the generation to be decomposed in a maintainable way.

			TheDependenciesOK method allows the method to be deferred since the success of rules may depend on what has already been generated. The dependenciesOK method is passed the list of GenerationDescriptors created so far.

			The fireLate method forces the rule to be fired when all other rules have been fired. This is usually used when the rules behaviour depends on what other rules have done.

			The fire method must return a list of GenerationDescriptors describing what should be generated. The Utility class, Make, provides a convenience method to help construct a GenerationDescriptor from the parent element, the containment feature, the new child and the priority indicator and if needed the editable setting.

	Priority may be from 10 to -10, where 1 indicates first in the containment and -10 last in the containment. Elements in the containment that are not (currently) being generated are placed between priorities 10 and 0. Bear in mind that the relative position of different diagrams (extensions)is preserved within each priority band. Also the order of source elements within their containment is preserved within each priority band.		Priority may be from 10 to -10, where 1 indicates first in the containment and -10 last in the containment. Elements in the containment that are not (currently) being generated are placed between priorities 10 and 0. Bear in mind that the relative position of different diagrams (extensions)is preserved within each priority band. Also the order of source elements within their containment is preserved within each priority band.
Line 105:		Line 118:
	where,		where,
	ret is the list to be returned and machine is the parent element containing the invariants to be added to.		ret is the list to be returned and machine is the parent element containing the invariants to be added to.

	Note that the rule will only be attempted for the type of source element defined in the extension point. However, this could be defined as an abstract base class to allow the rule to operate on several types of element. The rules enabled method can be used to restrict when it applies. More than one rule can be defined for the same kind of element allowing the generation to be decomposed in a maintainable way. Since the enablement of rules may depend on what has already been generated, the enabled method is passed the list of GenerationDescriptors created so far.

imported>Colin: /* Implementing Rule Classes */

2015-11-10T13:53:40Z

Implementing Rule Classes

← Older revision		Revision as of 13:53, 10 November 2015
Line 87:		Line 87:
	Rule classes must implement IRule. It is recommended the rule classes extend ac.soton.eventb.emf.diagrams.generator#AbstractRule which provides some concise constants for the commonly needed containments and defines some default behaviour (always enabled and the target EventB component is the source component).		Rule classes must implement IRule. It is recommended the rule classes extend ac.soton.eventb.emf.diagrams.generator#AbstractRule which provides some concise constants for the commonly needed containments and defines some default behaviour (always enabled and the target EventB component is the source component).

	The rule's fire method must return a list of GenerationDescriptors. The Utility class, Make, provides a convenience method to help construct a GenerationDescriptor from the parent element, the containment feature, the new child and the priority indicator.		The rule's fire method must return a list of GenerationDescriptors. The Utility class, Make, provides a convenience method to help construct a GenerationDescriptor from the parent element, the containment feature, the new child and the priority indicator and if needed the editable setting.

			Priority may be from 10 to -10, where 1 indicates first in the containment and -10 last in the containment. Elements in the containment that are not (currently) being generated are placed between priorities 10 and 0. Bear in mind that the relative position of different diagrams (extensions)is preserved within each priority band. Also the order of source elements within their containment is preserved within each priority band.

	Priority may be from 10 to -10, where 1 indicates first in the containment and -10 last in the containment. Elements in the containment that are not (currently) being generated are placed between priorities 10 and 0.
	1 2 3 4 5 6 7 8 9 10 <other content> 0 -1 -2 -3 -4 -5 -6 -7 -8 -9 -10		1 2 3 4 5 6 7 8 9 10 <other content> 0 -1 -2 -3 -4 -5 -6 -7 -8 -9 -10

Line 95:		Line 96:

	A current limitation of the priority scheme is that there are a limited number of priorities. For example, this could be a problem if a rule needs to calculate positions of each element within a collection based on dependencies of the element instance.		A current limitation of the priority scheme is that there are a limited number of priorities. For example, this could be a problem if a rule needs to calculate positions of each element within a collection based on dependencies of the element instance.

			In most cases the generated element should be set as read-only (the default). In this case the element will be deleted and re-generated on each invocation of the generator. The should not change any attributes of the element nor add to its children. In some case, however, it is necessary to generate an element whose contents may be modified by the user. To do this set the editable parameter of the Generation Descriptor. In this case the generated element will not be deleted when the generator is next invoked. The rule must take care not to return another Generation Descriptor if the element has already been generated. It should look for a suitable generated element (to use for adding further generated chldren etc.) and only generate a new one if it doesn't exist.

			Where a tree structure is entirely generated within one rule firing (e.g. an event with guards and actions) it is more efficient to construct the entire event and return a single Generation Descriptor that adds that event. It is also possible to do this by returning separate Generation Descriptors to add the event and each guard and action individually.

	A typical line from a rule class might look like this:		A typical line from a rule class might look like this:

imported>Colin: /* Generator */

2015-11-10T13:36:10Z

Generator

@@ Line 47: / Line 47: @@
 * Define an extension of ac.soton.eventb.emf.diagrams.generator.rule to make the generator framework aware of your generator and its rule classes.
 * Implement your rule classes
 === Implementing Rule Classes ===

imported>Colin: /* Implementing Rule Classes */

2013-01-17T15:35:57Z

Implementing Rule Classes

← Older revision		Revision as of 15:35, 17 January 2013
Line 57:		Line 57:
	1 2 3 4 5 6 7 8 9 10 <other content> 0 -1 -2 -3 -4 -5 -6 -7 -8 -9 -10		1 2 3 4 5 6 7 8 9 10 <other content> 0 -1 -2 -3 -4 -5 -6 -7 -8 -9 -10

	~~[i.e. User elements in the same containment will be placed after priority 1].~~ For example, a basic type invariant that doesn't depend on other variables might be placed at position 1 whereas a theorem or invariant included purely for proof purposes might be placed at position -10.		For example, a basic type invariant that doesn't depend on other variables might be placed at position 1 whereas a theorem or invariant included purely for proof purposes might be placed at position -10.

	A current limitation of the priority scheme is that there are a limited number of priorities. For example, this could be a problem if a rule needs to calculate positions of each element within a collection based on dependencies of the element instance.		A current limitation of the priority scheme is that there are a limited number of priorities. For example, this could be a problem if a rule needs to calculate positions of each element within a collection based on dependencies of the element instance.