Difference between revisions of "Generated Model Elements"

From Event-B
Jump to navigationJump to search
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...)
 
imported>Pascal
 
(4 intermediate revisions by one other user not shown)
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 as generated.
 +
* in Rodin 1.2 and further releases, any internal element can be tagged as generated.
  
 
=== Convention ===
 
=== Convention ===
Line 16: Line 20:
 
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]]
 +
 
 +
In the above example, we just clicked the remove button for 'axm3'.
 +
 
 +
[[Category:Developer documentation]]

Latest revision as of 09:26, 20 November 2009

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 as generated.
  • in Rodin 1.2 and further releases, any internal element can be tagged as generated.

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:

GeneratedElements editor.png

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:

GeneratedElements InfoReadOnly.png

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