View source for Talk:Event Model Decomposition

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.

[[Image:Decomposition.jpg|thumb|center|270px]]

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


----

Dear Son,

Thank you! That would be nice to allow for refining the shared variables since many (less formal) languages support refinement of the interface.

Best regards,
Sergey