Difference between revisions of "Talk:Event Model Decomposition"

From Event-B
Jump to: navigation, search
Line 7: Line 7:
 
Best regards,
 
Best regards,
 
Sergey
 
Sergey
 +
 +
 +
 +
----
 +
 +
Dear Sergey
 +
 +
The restriction is there to ensure that the shared variables are not being refined differently in sub-models. This ensures the compositionality of the sub-models. Recently, there is a proposal to encapsulate the shared variables in a separate module, allowing the shared variables to be refined. 
 +
 +
Best regards,
 +
Son

Revision as of 14:15, 10 April 2012

Dear the author of the article,

I do not clearly understand why shared variables and events must have a restriction that they cannot be refined in a sub-model. Suppose, we have a shared variable 's' of type BOOL. After the decomposition, this variable is data-refined with three new variables 's1', 's2' and 's3' such that 's' disappears. In this case we provide a gluing invariant, e.g. s = bool(s1=TRUE or s2=TRUE and s3=TRUE). Although 's' vanishes, we still can use it as the interface between sub-models since we have defined it as a shared variable and it still exists as the communication channel between the sub-models. Furthermore, the glueing invariant forms the precise interface between these sub-models such that it can be used to provide the required value and, therefore, no rule is broken.

Decomposition.jpg

Best regards, Sergey



Dear Sergey

The restriction is there to ensure that the shared variables are not being refined differently in sub-models. This ensures the compositionality of the sub-models. Recently, there is a proposal to encapsulate the shared variables in a separate module, allowing the shared variables to be refined.

Best regards, Son