Generated Model Elements - Revision history

imported>Pascal: /* Typo */

2009-11-20T09:26:48Z

Typo

← Older revision		Revision as of 09:26, 20 November 2009
Line 2:		Line 2:

	Note:		Note:
	* in Rodin 1.1, only file root elements could be tagged generated.		* in Rodin 1.1, only file root elements could be tagged as generated.
	* in Rodin 1.2 and further releases, any internal element can be tagged generated.		* in Rodin 1.2 and further releases, any internal element can be tagged as generated.

	=== Convention ===		=== Convention ===

imported>Nicolas at 09:22, 20 November 2009

2009-11-20T09:22:14Z

← Older revision		Revision as of 09:22, 20 November 2009
Line 1:		Line 1:
	Various tools generate models (Decomposition, UML-B, ...). Editing a generated model is not recommended, as further model generations will simply override the modifications. Thus, generated models should not be modifiable by editors, and we need a way to tag these models and prevent editing. To that end, a new boolean attribute is defined: 'org.eventb.core.generated'. Tools can put this attribute on any internal element they generate; its presence is checked by editors so they can forbid editing tagged elements.		Various tools generate models (Decomposition, UML-B, ...). Editing a generated model is not recommended, as further model generations will simply override the modifications. Thus, generated models should not be modifiable by editors, and we need a way to tag these models and prevent editing. To that end, a new boolean attribute is defined: 'org.eventb.core.generated'. Tools can put this attribute on any internal element they generate; its presence is checked by editors so they can forbid editing tagged elements.

			Note:
			* in Rodin 1.1, only file root elements could be tagged generated.
			* in Rodin 1.2 and further releases, any internal element can be tagged generated.

	=== Convention ===		=== Convention ===

imported>Nicolas: /* Example */ Added category Developer documentation

2009-10-12T12:59:37Z

Example: Added category Developer documentation

← Older revision		Revision as of 12:59, 12 October 2009
Line 23:		Line 23:

	In the above example, we just clicked the remove button for 'axm3'.		In the above example, we just clicked the remove button for 'axm3'.

			[[Category:Developer documentation]]

imported>Nicolas: /* Example */

2009-10-07T09:01:24Z

Example

← Older revision		Revision as of 09:01, 7 October 2009
Line 21:		Line 21:

	[[Image:GeneratedElements_InfoReadOnly.png\|center]]		[[Image:GeneratedElements_InfoReadOnly.png\|center]]

			In the above example, we just clicked the remove button for 'axm3'.

imported>Nicolas: /* Example */

2009-10-07T08:58:41Z

Example

← Older revision		Revision as of 08:58, 7 October 2009
Line 16:		Line 16:
	Let's see what it looks like when opening a generated model. In the following example, the root element is tagged generated, so all internal elements are read-only:		Let's see what it looks like when opening a generated model. In the following example, the root element is tagged generated, so all internal elements are read-only:

	[[Image:GeneratedElements_editor\|center]]		[[Image:GeneratedElements_editor.png\|center]]

	If we try to modify a text field or click a 'theorem' button, nothing happens. Attempts to add or remove elements fail with a popup message:		If we try to modify a text field or click a 'theorem' button, nothing happens. Attempts to add or remove elements fail with a popup message:

	[[Image:GeneratedElements_InfoReadOnly\|center]]		[[Image:GeneratedElements_InfoReadOnly.png\|center]]

imported>Nicolas: New page: Various tools generate models (Decomposition, UML-B, ...). Editing a generated model is not recommended, as further model generations will simply override the modifications. Thus, generate...

2009-10-07T08:56:24Z

New page: Various tools generate models (Decomposition, UML-B, ...). Editing a generated model is not recommended, as further model generations will simply override the modifications. Thus, generate...

New page

Various tools generate models (Decomposition, UML-B, ...). Editing a generated model is not recommended, as further model generations will simply override the modifications. Thus, generated models should not be modifiable by editors, and we need a way to tag these models and prevent editing. To that end, a new boolean attribute is defined: 'org.eventb.core.generated'. Tools can put this attribute on any internal element they generate; its presence is checked by editors so they can forbid editing tagged elements.

=== Convention ===

The semantics of the 'org.eventb.core.generated' attribute is defined as follows:
* if the attribute is absent, the element is considered not generated
* if the attribute is present with value 'false', idem
* if the attribute is present with value 'true', the attributed element and all its children (recursively) are considered generated

Thus, a given internal element is considered generated if any of the following holds:
* it has the 'org.eventb.core.generated' attribute with value 'true'
* one of its ancestors has the 'org.eventb.core.generated' attribute with value 'true'

=== Example ===

Let's see what it looks like when opening a generated model. In the following example, the root element is tagged generated, so all internal elements are read-only:

[[Image:GeneratedElements_editor|center]]

If we try to modify a text field or click a 'theorem' button, nothing happens. Attempts to add or remove elements fail with a popup message:

[[Image:GeneratedElements_InfoReadOnly|center]]